自定義Isabelle語法打破現有語法

我試圖生成一個很好的語法來映射關聯列表的值的函數，即我想寫[x ↦ f y | (x ↦ y) ∈ l]爲mapAList f l。我想出了自定義Isabelle語法打破現有語法

syntax 
"_alist_map" :: "['b, pttrn, ('a × 'b) list] ⇒ ('a × 'b) list" 
("[x ↦ _ | '(x ↦ _') ∈ _]")

它的工作原理，但會導致term "(x,y)#[]"告訴我Inner syntax error at "(x , y) # []"和(x的陰影略有不同。

原因似乎一旦x出現在mixfix註釋，它現在總是字面令牌到語法（一個定界符根據ISAR-REF的第7.4.1節），並不再的標識符 - 就像if ... then ... else ...的語法可防止if成爲變量名稱

我可以以某種方式解決此問題嗎？

來源

2014-04-25 Joachim Breitner

只是出於好奇，'mapAList'是否只將'f'映射到'l'的* values *（即對的第二個分量）？看起來，類型化的語法比編寫函數應用程序更麻煩;）您是否有一個可讀性實際提高的示例（我知道這是非常主觀的）。 – chris

我的應用程序中的函數'f'是用特殊的sytnax本身編寫的，即'[| x |]'和'map（λx。[| x |]）'不如'[x↦[| y |] | （x↦y）∈l]' –

我只是做了一個小實驗功能map_alist有希望符合您的mapAList和其定義如下：

fun map_alist :: "('b ⇒ 'c) ⇒ ('a × 'b) list ⇒ ('a × 'c) list" 
where 
    "map_alist f [] = []" | 
    "map_alist f ((x, y) # xs) = (x, f y) # map_alist f xs"

則可以使用現有的語法，看起來有點爲你打算。也許這是一個選擇？

lemma "map_alist f xs = [(x, f y). (x, y) ← xs]" 
    by (induct xs) auto

來源

2014-04-25 13:07:09 chris

關閉，但是如何在我的文檔設置中使用'thm'或antiquotations時如何讓Isabelle打印出漂亮的語法？ –

mixfix註釋中使用的標識符名稱不能再作爲標識符使用，我不知道任何解決方法。因此，您可以選擇一個非標識符符號（如\<xX>或\<mapAListvariable>），並將乳膠輸出設置爲x，將\newcommand{\isasymmapAListvariable}{x}添加到root.tex，而不是使用x作爲變量名稱。

還可以添加\<xX>或\<mapAListvariable>到伊莎貝爾/ JEDIT（優選在$ISABELLE_HOME_USER/etc/symbols）的符號文件併爲其分配一個將被用於在伊莎貝爾/ JEDIT顯示一些的Unicode點。

來源

2014-04-25 15:47:45

自定義Isabelle語法打破現有語法

回答

相關問題