--- a/src/HOL/TLA/Intensional.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/TLA/Intensional.thy Fri Sep 20 19:51:08 2024 +0200
@@ -33,11 +33,11 @@
where unl_lift3: "lift3 f x y z w \<equiv> f (x w) (y w) (z w)"
(* "Rigid" quantification (logic level) *)
-definition RAll :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rall " 10)
+definition RAll :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder \<open>Rall \<close> 10)
where unl_Rall: "(Rall x. A x) w \<equiv> \<forall>x. A x w"
-definition REx :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex " 10)
+definition REx :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder \<open>Rex \<close> 10)
where unl_Rex: "(Rex x. A x) w \<equiv> \<exists>x. A x w"
-definition REx1 :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex! " 10)
+definition REx1 :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder \<open>Rex! \<close> 10)
where unl_Rex1: "(Rex! x. A x) w \<equiv> \<exists>!x. A x w"
@@ -46,56 +46,56 @@
nonterminal lift and liftargs
syntax
- "" :: "id \<Rightarrow> lift" ("_")
- "" :: "longid \<Rightarrow> lift" ("_")
- "" :: "var \<Rightarrow> lift" ("_")
- "_applC" :: "[lift, cargs] \<Rightarrow> lift" ("(1_/ _)" [1000, 1000] 999)
- "" :: "lift \<Rightarrow> lift" ("'(_')")
- "_lambda" :: "[idts, 'a] \<Rightarrow> lift" ("(3\<lambda>_./ _)" [0, 3] 3)
- "_constrain" :: "[lift, type] \<Rightarrow> lift" ("(_::_)" [4, 0] 3)
- "" :: "lift \<Rightarrow> liftargs" ("_")
- "_liftargs" :: "[lift, liftargs] \<Rightarrow> liftargs" ("_,/ _")
- "_Valid" :: "lift \<Rightarrow> bool" ("(\<turnstile> _)" 5)
- "_holdsAt" :: "['a, lift] \<Rightarrow> bool" ("(_ \<Turnstile> _)" [100,10] 10)
+ "" :: "id \<Rightarrow> lift" (\<open>_\<close>)
+ "" :: "longid \<Rightarrow> lift" (\<open>_\<close>)
+ "" :: "var \<Rightarrow> lift" (\<open>_\<close>)
+ "_applC" :: "[lift, cargs] \<Rightarrow> lift" (\<open>(1_/ _)\<close> [1000, 1000] 999)
+ "" :: "lift \<Rightarrow> lift" (\<open>'(_')\<close>)
+ "_lambda" :: "[idts, 'a] \<Rightarrow> lift" (\<open>(3\<lambda>_./ _)\<close> [0, 3] 3)
+ "_constrain" :: "[lift, type] \<Rightarrow> lift" (\<open>(_::_)\<close> [4, 0] 3)
+ "" :: "lift \<Rightarrow> liftargs" (\<open>_\<close>)
+ "_liftargs" :: "[lift, liftargs] \<Rightarrow> liftargs" (\<open>_,/ _\<close>)
+ "_Valid" :: "lift \<Rightarrow> bool" (\<open>(\<turnstile> _)\<close> 5)
+ "_holdsAt" :: "['a, lift] \<Rightarrow> bool" (\<open>(_ \<Turnstile> _)\<close> [100,10] 10)
(* Syntax for lifted expressions outside the scope of \<turnstile> or |= *)
- "_LIFT" :: "lift \<Rightarrow> 'a" ("LIFT _")
+ "_LIFT" :: "lift \<Rightarrow> 'a" (\<open>LIFT _\<close>)
(* generic syntax for lifted constants and functions *)
- "_const" :: "'a \<Rightarrow> lift" ("(#_)" [1000] 999)
- "_lift" :: "['a, lift] \<Rightarrow> lift" ("(_<_>)" [1000] 999)
- "_lift2" :: "['a, lift, lift] \<Rightarrow> lift" ("(_<_,/ _>)" [1000] 999)
- "_lift3" :: "['a, lift, lift, lift] \<Rightarrow> lift" ("(_<_,/ _,/ _>)" [1000] 999)
+ "_const" :: "'a \<Rightarrow> lift" (\<open>(#_)\<close> [1000] 999)
+ "_lift" :: "['a, lift] \<Rightarrow> lift" (\<open>(_<_>)\<close> [1000] 999)
+ "_lift2" :: "['a, lift, lift] \<Rightarrow> lift" (\<open>(_<_,/ _>)\<close> [1000] 999)
+ "_lift3" :: "['a, lift, lift, lift] \<Rightarrow> lift" (\<open>(_<_,/ _,/ _>)\<close> [1000] 999)
(* concrete syntax for common infix functions: reuse same symbol *)
- "_liftEqu" :: "[lift, lift] \<Rightarrow> lift" ("(_ =/ _)" [50,51] 50)
- "_liftNeq" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<noteq>/ _)" [50,51] 50)
- "_liftNot" :: "lift \<Rightarrow> lift" ("(\<not> _)" [40] 40)
- "_liftAnd" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<and>/ _)" [36,35] 35)
- "_liftOr" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<or>/ _)" [31,30] 30)
- "_liftImp" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<longrightarrow>/ _)" [26,25] 25)
- "_liftIf" :: "[lift, lift, lift] \<Rightarrow> lift" ("(if (_)/ then (_)/ else (_))" 10)
- "_liftPlus" :: "[lift, lift] \<Rightarrow> lift" ("(_ +/ _)" [66,65] 65)
- "_liftMinus" :: "[lift, lift] \<Rightarrow> lift" ("(_ -/ _)" [66,65] 65)
- "_liftTimes" :: "[lift, lift] \<Rightarrow> lift" ("(_ */ _)" [71,70] 70)
- "_liftDiv" :: "[lift, lift] \<Rightarrow> lift" ("(_ div _)" [71,70] 70)
- "_liftMod" :: "[lift, lift] \<Rightarrow> lift" ("(_ mod _)" [71,70] 70)
- "_liftLess" :: "[lift, lift] \<Rightarrow> lift" ("(_/ < _)" [50, 51] 50)
- "_liftLeq" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<le> _)" [50, 51] 50)
- "_liftMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<in> _)" [50, 51] 50)
- "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<notin> _)" [50, 51] 50)
- "_liftFinset" :: "liftargs \<Rightarrow> lift" ("{(_)}")
+ "_liftEqu" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ =/ _)\<close> [50,51] 50)
+ "_liftNeq" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ \<noteq>/ _)\<close> [50,51] 50)
+ "_liftNot" :: "lift \<Rightarrow> lift" (\<open>(\<not> _)\<close> [40] 40)
+ "_liftAnd" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ \<and>/ _)\<close> [36,35] 35)
+ "_liftOr" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ \<or>/ _)\<close> [31,30] 30)
+ "_liftImp" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ \<longrightarrow>/ _)\<close> [26,25] 25)
+ "_liftIf" :: "[lift, lift, lift] \<Rightarrow> lift" (\<open>(if (_)/ then (_)/ else (_))\<close> 10)
+ "_liftPlus" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ +/ _)\<close> [66,65] 65)
+ "_liftMinus" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ -/ _)\<close> [66,65] 65)
+ "_liftTimes" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ */ _)\<close> [71,70] 70)
+ "_liftDiv" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ div _)\<close> [71,70] 70)
+ "_liftMod" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ mod _)\<close> [71,70] 70)
+ "_liftLess" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_/ < _)\<close> [50, 51] 50)
+ "_liftLeq" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_/ \<le> _)\<close> [50, 51] 50)
+ "_liftMem" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_/ \<in> _)\<close> [50, 51] 50)
+ "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_/ \<notin> _)\<close> [50, 51] 50)
+ "_liftFinset" :: "liftargs \<Rightarrow> lift" (\<open>{(_)}\<close>)
(** TODO: syntax for lifted collection / comprehension **)
- "_liftPair" :: "[lift,liftargs] \<Rightarrow> lift" ("(1'(_,/ _'))")
+ "_liftPair" :: "[lift,liftargs] \<Rightarrow> lift" (\<open>(1'(_,/ _'))\<close>)
(* infix syntax for list operations *)
- "_liftCons" :: "[lift, lift] \<Rightarrow> lift" ("(_ #/ _)" [65,66] 65)
- "_liftApp" :: "[lift, lift] \<Rightarrow> lift" ("(_ @/ _)" [65,66] 65)
- "_liftList" :: "liftargs \<Rightarrow> lift" ("[(_)]")
+ "_liftCons" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ #/ _)\<close> [65,66] 65)
+ "_liftApp" :: "[lift, lift] \<Rightarrow> lift" (\<open>(_ @/ _)\<close> [65,66] 65)
+ "_liftList" :: "liftargs \<Rightarrow> lift" (\<open>[(_)]\<close>)
(* Rigid quantification (syntax level) *)
- "_RAll" :: "[idts, lift] \<Rightarrow> lift" ("(3\<forall>_./ _)" [0, 10] 10)
- "_REx" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>_./ _)" [0, 10] 10)
- "_REx1" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>!_./ _)" [0, 10] 10)
+ "_RAll" :: "[idts, lift] \<Rightarrow> lift" (\<open>(3\<forall>_./ _)\<close> [0, 10] 10)
+ "_REx" :: "[idts, lift] \<Rightarrow> lift" (\<open>(3\<exists>_./ _)\<close> [0, 10] 10)
+ "_REx1" :: "[idts, lift] \<Rightarrow> lift" (\<open>(3\<exists>!_./ _)\<close> [0, 10] 10)
translations
"_const" == "CONST const"