80 "_liftNotMem" :: [lift, lift] => lift ("(_/ ~: _)" [50, 51] 50) |
80 "_liftNotMem" :: [lift, lift] => lift ("(_/ ~: _)" [50, 51] 50) |
81 "_liftFinset" :: liftargs => lift ("{(_)}") |
81 "_liftFinset" :: liftargs => lift ("{(_)}") |
82 (** TODO: syntax for lifted collection / comprehension **) |
82 (** TODO: syntax for lifted collection / comprehension **) |
83 "_liftPair" :: [lift,liftargs] => lift ("(1'(_,/ _'))") |
83 "_liftPair" :: [lift,liftargs] => lift ("(1'(_,/ _'))") |
84 (* infix syntax for list operations *) |
84 (* infix syntax for list operations *) |
85 "_liftCons" :: [lift, lift] => lift ("(_ #/ _)" [65,66] 65) |
85 "_liftCons" :: [lift, lift] => lift ("(_ #/ _)" [65,66] 65) |
86 "_liftApp" :: [lift, lift] => lift ("(_ @/ _)" [65,66] 65) |
86 "_liftApp" :: [lift, lift] => lift ("(_ @/ _)" [65,66] 65) |
87 "_liftList" :: liftargs => lift ("[(_)]") |
87 "_liftList" :: liftargs => lift ("[(_)]") |
88 |
88 |
89 (* Rigid quantification (syntax level) *) |
89 (* Rigid quantification (syntax level) *) |
90 "_RAll" :: [idts, lift] => lift ("(3! _./ _)" [0, 10] 10) |
90 "_ARAll" :: [idts, lift] => lift ("(3! _./ _)" [0, 10] 10) |
91 "_REx" :: [idts, lift] => lift ("(3? _./ _)" [0, 10] 10) |
91 "_AREx" :: [idts, lift] => lift ("(3? _./ _)" [0, 10] 10) |
92 "_REx1" :: [idts, lift] => lift ("(3?! _./ _)" [0, 10] 10) |
92 "_AREx1" :: [idts, lift] => lift ("(3?! _./ _)" [0, 10] 10) |
93 "_ARAll" :: [idts, lift] => lift ("(3ALL _./ _)" [0, 10] 10) |
93 "_RAll" :: [idts, lift] => lift ("(3ALL _./ _)" [0, 10] 10) |
94 "_AREx" :: [idts, lift] => lift ("(3EX _./ _)" [0, 10] 10) |
94 "_REx" :: [idts, lift] => lift ("(3EX _./ _)" [0, 10] 10) |
95 "_AREx1" :: [idts, lift] => lift ("(3EX! _./ _)" [0, 10] 10) |
95 "_REx1" :: [idts, lift] => lift ("(3EX! _./ _)" [0, 10] 10) |
96 |
96 |
97 translations |
97 translations |
98 "_const" == "const" |
98 "_const" == "const" |
99 "_lift" == "lift" |
99 "_lift" == "lift" |
100 "_lift2" == "lift2" |
100 "_lift2" == "lift2" |
140 "w |= ~A" <= "_liftNot A w" |
140 "w |= ~A" <= "_liftNot A w" |
141 "w |= A & B" <= "_liftAnd A B w" |
141 "w |= A & B" <= "_liftAnd A B w" |
142 "w |= A | B" <= "_liftOr A B w" |
142 "w |= A | B" <= "_liftOr A B w" |
143 "w |= A --> B" <= "_liftImp A B w" |
143 "w |= A --> B" <= "_liftImp A B w" |
144 "w |= u = v" <= "_liftEqu u v w" |
144 "w |= u = v" <= "_liftEqu u v w" |
145 "w |= ! x. A" <= "_RAll x A w" |
145 "w |= ALL x. A" <= "_RAll x A w" |
146 "w |= ? x. A" <= "_REx x A w" |
146 "w |= EX x. A" <= "_REx x A w" |
147 "w |= ?! x. A" <= "_REx1 x A w" |
147 "w |= EX! x. A" <= "_REx1 x A w" |
148 |
148 |
149 syntax (symbols) |
149 syntax (symbols) |
150 "_Valid" :: lift => bool ("(\\<turnstile> _)" 5) |
150 "_Valid" :: lift => bool ("(\\<turnstile> _)" 5) |
151 "_holdsAt" :: ['a, lift] => bool ("(_ \\<Turnstile> _)" [100,10] 10) |
151 "_holdsAt" :: ['a, lift] => bool ("(_ \\<Turnstile> _)" [100,10] 10) |
152 "_liftNeq" :: [lift, lift] => lift (infixl "\\<noteq>" 50) |
152 "_liftNeq" :: [lift, lift] => lift (infixl "\\<noteq>" 50) |
170 unl_con "LIFT #c w == c" |
170 unl_con "LIFT #c w == c" |
171 unl_lift "LIFT f<x> w == f (x w)" |
171 unl_lift "LIFT f<x> w == f (x w)" |
172 unl_lift2 "LIFT f<x, y> w == f (x w) (y w)" |
172 unl_lift2 "LIFT f<x, y> w == f (x w) (y w)" |
173 unl_lift3 "LIFT f<x, y, z> w == f (x w) (y w) (z w)" |
173 unl_lift3 "LIFT f<x, y, z> w == f (x w) (y w) (z w)" |
174 |
174 |
175 unl_Rall "w |= ! x. A x == ! x. (w |= A x)" |
175 unl_Rall "w |= ALL x. A x == ALL x. (w |= A x)" |
176 unl_Rex "w |= ? x. A x == ? x. (w |= A x)" |
176 unl_Rex "w |= EX x. A x == EX x. (w |= A x)" |
177 unl_Rex1 "w |= ?! x. A x == ?! x. (w |= A x)" |
177 unl_Rex1 "w |= EX! x. A x == EX! x. (w |= A x)" |
178 end |
178 end |