如何在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} *}