src/HOL/TLA/Intensional.thy
changeset 9517 f58863b1406a
parent 7224 e41e64476f9b
child 12114 a8e860c86252
     1.1 --- a/src/HOL/TLA/Intensional.thy	Thu Aug 03 19:28:37 2000 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Thu Aug 03 19:29:03 2000 +0200
     1.3 @@ -82,17 +82,17 @@
     1.4    (** TODO: syntax for lifted collection / comprehension **)
     1.5    "_liftPair"   :: [lift,liftargs] => lift                   ("(1'(_,/ _'))")
     1.6    (* infix syntax for list operations *)
     1.7 -  "_liftCons" :: [lift, lift] => lift                    ("(_ #/ _)" [65,66] 65)
     1.8 -  "_liftApp"  :: [lift, lift] => lift                    ("(_ @/ _)" [65,66] 65)
     1.9 -  "_liftList" :: liftargs => lift                        ("[(_)]")
    1.10 +  "_liftCons" :: [lift, lift] => lift                  ("(_ #/ _)" [65,66] 65)
    1.11 +  "_liftApp"  :: [lift, lift] => lift                  ("(_ @/ _)" [65,66] 65)
    1.12 +  "_liftList" :: liftargs => lift                      ("[(_)]")
    1.13  
    1.14    (* Rigid quantification (syntax level) *)
    1.15 -  "_RAll"  :: [idts, lift] => lift                     ("(3! _./ _)" [0, 10] 10)
    1.16 -  "_REx"   :: [idts, lift] => lift                     ("(3? _./ _)" [0, 10] 10)
    1.17 -  "_REx1"  :: [idts, lift] => lift                     ("(3?! _./ _)" [0, 10] 10)
    1.18 -  "_ARAll" :: [idts, lift] => lift                     ("(3ALL _./ _)" [0, 10] 10)
    1.19 -  "_AREx"  :: [idts, lift] => lift                     ("(3EX _./ _)" [0, 10] 10)
    1.20 -  "_AREx1" :: [idts, lift] => lift                     ("(3EX! _./ _)" [0, 10] 10)
    1.21 +  "_ARAll"  :: [idts, lift] => lift                    ("(3! _./ _)" [0, 10] 10)
    1.22 +  "_AREx"   :: [idts, lift] => lift                    ("(3? _./ _)" [0, 10] 10)
    1.23 +  "_AREx1"  :: [idts, lift] => lift                    ("(3?! _./ _)" [0, 10] 10)
    1.24 +  "_RAll" :: [idts, lift] => lift                      ("(3ALL _./ _)" [0, 10] 10)
    1.25 +  "_REx"  :: [idts, lift] => lift                      ("(3EX _./ _)" [0, 10] 10)
    1.26 +  "_REx1" :: [idts, lift] => lift                      ("(3EX! _./ _)" [0, 10] 10)
    1.27  
    1.28  translations
    1.29    "_const"        == "const"
    1.30 @@ -142,9 +142,9 @@
    1.31    "w |= A | B"    <= "_liftOr A B w"
    1.32    "w |= A --> B"  <= "_liftImp A B w"
    1.33    "w |= u = v"    <= "_liftEqu u v w"
    1.34 -  "w |= ! x. A"   <= "_RAll x A w"
    1.35 -  "w |= ? x. A"   <= "_REx x A w"
    1.36 -  "w |= ?! x. A"  <= "_REx1 x A w"
    1.37 +  "w |= ALL x. A"   <= "_RAll x A w"
    1.38 +  "w |= EX x. A"   <= "_REx x A w"
    1.39 +  "w |= EX! x. A"  <= "_REx1 x A w"
    1.40  
    1.41  syntax (symbols)
    1.42    "_Valid"      :: lift => bool                        ("(\\<turnstile> _)" 5)
    1.43 @@ -172,7 +172,7 @@
    1.44    unl_lift2   "LIFT f<x, y> w == f (x w) (y w)"
    1.45    unl_lift3   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
    1.46  
    1.47 -  unl_Rall    "w |= ! x. A x  ==  ! x. (w |= A x)" 
    1.48 -  unl_Rex     "w |= ? x. A x  ==  ? x. (w |= A x)"
    1.49 -  unl_Rex1    "w |= ?! x. A x  ==  ?! x. (w |= A x)"
    1.50 +  unl_Rall    "w |= ALL x. A x  ==  ALL x. (w |= A x)" 
    1.51 +  unl_Rex     "w |= EX x. A x   ==  EX x. (w |= A x)"
    1.52 +  unl_Rex1    "w |= EX! x. A x  ==  EX! x. (w |= A x)"
    1.53  end