如何在Isabelle中获得ML代码的const值？

Question

我在理论写了一个定义，说：

定义mycmd ::字符串，其中 “mycmd == '' external_executable'”

然后，我需要使用值的mycmd ，这是“external_executable”，在ML代码块为Isabelle_System.bash_output的说法，但我不知道如何获得的mycmd值。有什么建议吗？

谢谢！

Answer 1

我想这是你想要的，即使我真的不明白你想要做什么：

ML {* Thm.concl_of @{thm mycmd_def} 
    |> Term.dest_comb |> snd 
    |> HOLogic.dest_string *} 

和一个更强大的版本（根据定义风格，用“=”或 “==”）：

ML {* Thm.concl_of @{thm mycmd_def} 
    |> (fn x => if fst (dest_Const (fst (strip_comb x))) = @{const_name "Trueprop"} 
    then snd (dest_comb x) else x) 
    |> dest_comb |> snd 
    |> HOLogic.dest_string *} 

Answer 2

要静态评估伊莎贝尔/ ML的伊莎贝尔/ HOL来看，您通常使用@ {}代码antiquotation。在你的例子中，它的读数为ML {* @{code mycmd} *}。 Isabelle将在编译时插入必要的代码以评估mycmd并使用该值。唯一的困难是HOL类型string未连载至ML类型string。因此，您应该在HOL术语中使用类型String.literal并使用它。

这里是你的榜样为Isabelle2014：

definition mycmd :: String.literal where "mycmd == STR ''external_executable''" 
ML {* Isabelle_System.bash_output @{code mycmd} *}