src/HOL/TLA/Intensional.thy
changeset 6255 db63752140c7
parent 3808 8489375c6198
child 6340 7d5cbd5819a0
     1.1 --- a/src/HOL/TLA/Intensional.thy	Mon Feb 08 13:02:42 1999 +0100
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Mon Feb 08 13:02:56 1999 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (* 
     1.5      File:	 TLA/Intensional.thy
     1.6      Author:      Stephan Merz
     1.7 -    Copyright:   1997 University of Munich
     1.8 +    Copyright:   1998 University of Munich
     1.9  
    1.10      Theory Name: Intensional
    1.11      Logic Image: HOL
    1.12 @@ -10,95 +10,168 @@
    1.13  on top of HOL, with lifting of constants and functions.
    1.14  *)
    1.15  
    1.16 -Intensional  =  Prod +
    1.17 +Intensional  =  Main +
    1.18  
    1.19 -classes
    1.20 -    world < logic    (* Type class of "possible worlds". Concrete types
    1.21 -                        will be provided by children theories. *)
    1.22 +axclass
    1.23 +  world < term
    1.24 +
    1.25 +(** abstract syntax **)
    1.26  
    1.27  types
    1.28 -    ('a,'w) term = "'w => 'a"    (* Intention: 'w::world *)
    1.29 -    'w form = "'w => bool"
    1.30 +  ('w,'a) expr = 'w => 'a               (* intention: 'w::world, 'a::term *)
    1.31 +  'w form = ('w, bool) expr
    1.32  
    1.33  consts
    1.34 -  TrueInt  :: "('w::world form) => prop"             ("(_)" 5)
    1.35 -
    1.36 -  (* Holds at *)
    1.37 -  holdsAt  :: "['w::world, 'w form] => bool"   ("(_ |= _)" [100,9] 8)
    1.38 -
    1.39 -  (* Lifting base functions to "intensional" level *)
    1.40 -  con      :: "'a => ('w::world => 'a)"               ("(#_)" [100] 99)
    1.41 -  lift     :: "['a => 'b, 'w::world => 'a] => ('w => 'b)"  ("(_[_])")
    1.42 -  lift2    :: "['a => ('b => 'c), 'w::world => 'a, 'w => 'b] => ('w => 'c)" ("(_[_,/ _])")
    1.43 -  lift3    :: "['a => 'b => 'c => 'd, 'w::world => 'a, 'w => 'b, 'w => 'c] => ('w => 'd)" ("(_[_,/ _,/ _])")
    1.44 +  Valid    :: ('w::world) form => bool
    1.45 +  const    :: 'a => ('w::world, 'a) expr
    1.46 +  lift     :: ['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr
    1.47 +  lift2    :: ['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr
    1.48 +  lift3    :: ['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr
    1.49  
    1.50 -  (* Lifted infix functions *)
    1.51 -  IntEqu   :: "['w::world => 'a, 'w => 'a] => 'w form"  ("(_ .=/ _)" [50,51] 50)
    1.52 -  IntNeq   :: "['w::world => 'a, 'w => 'a] => 'w form"  ("(_ .~=/ _)" [50,51] 50)
    1.53 -  NotInt   :: "('w::world) form => 'w form"               ("(.~ _)" [40] 40)
    1.54 -  AndInt   :: "[('w::world) form, 'w form] => 'w form"    ("(_ .&/ _)" [36,35] 35)
    1.55 -  OrInt    :: "[('w::world) form, 'w form] => 'w form"    ("(_ .|/ _)" [31,30] 30)
    1.56 -  ImpInt   :: "[('w::world) form, 'w form] => 'w form"    ("(_ .->/ _)" [26,25] 25)
    1.57 -  IfInt    :: "[('w::world) form, ('a,'w) term, ('a,'w) term] => ('a,'w) term" ("(.if (_)/ .then (_)/ .else (_))" 10)
    1.58 -  PlusInt  :: "[('w::world) => ('a::plus), 'w => 'a] => ('w => 'a)"  ("(_ .+/ _)" [66,65] 65)
    1.59 -  MinusInt :: "[('w::world) => ('a::minus), 'w => 'a] => ('w => 'a)"  ("(_ .-/ _)" [66,65] 65)
    1.60 -  TimesInt :: "[('w::world) => ('a::times), 'w => 'a] => ('w => 'a)"  ("(_ .*/ _)" [71,70] 70)
    1.61 +  (* "Rigid" quantification (logic level) *)
    1.62 +  RAll     :: "('a => ('w::world) form) => 'w form"       (binder "Rall " 10)
    1.63 +  REx      :: "('a => ('w::world) form) => 'w form"       (binder "Rex " 10)
    1.64 +  REx1     :: "('a => ('w::world) form) => 'w form"       (binder "Rex! " 10)
    1.65  
    1.66 -  LessInt  :: "['w::world => 'a::ord, 'w => 'a] => 'w form"        ("(_/ .< _)"  [50, 51] 50)
    1.67 -  LeqInt   :: "['w::world => 'a::ord, 'w => 'a] => 'w form"        ("(_/ .<= _)" [50, 51] 50)
    1.68 +(** concrete syntax **)
    1.69  
    1.70 -  (* lifted set membership *)
    1.71 -  memInt   :: "[('a,'w::world) term, ('a set,'w) term] => 'w form"  ("(_/ .: _)" [50, 51] 50)
    1.72 -
    1.73 -  (* "Rigid" quantification *)
    1.74 -  RAll     :: "('a => 'w::world form) => 'w form"     (binder "RALL " 10)
    1.75 -  REx      :: "('a => 'w::world form) => 'w form"     (binder "REX " 10)
    1.76 +nonterminals
    1.77 +  lift
    1.78 +  liftargs
    1.79  
    1.80  syntax
    1.81 -  "@tupleInt"    :: "args => ('a * 'b, 'w) term"  ("(1{[_]})")
    1.82 +  ""            :: id => lift                          ("_")
    1.83 +  ""            :: longid => lift                      ("_")
    1.84 +  ""            :: var => lift                         ("_")
    1.85 +  "_applC"      :: [lift, cargs] => lift               ("(1_/ _)" [1000, 1000] 999)
    1.86 +  ""            :: lift => lift                        ("'(_')")
    1.87 +  "_lambda"     :: [idts, 'a] => lift                  ("(3%_./ _)" [0, 3] 3)
    1.88 +  "_constrain"  :: [lift, type] => lift                ("(_::_)" [4, 0] 3)
    1.89 +  ""            :: lift => liftargs                    ("_")
    1.90 +  "_liftargs"   :: [lift, liftargs] => liftargs        ("_,/ _")
    1.91 +  "_Valid"      :: lift => bool                        ("(|- _)" 5)
    1.92 +  "_holdsAt"    :: ['a, lift] => bool                  ("(_ |= _)" [100,10] 10)
    1.93 +
    1.94 +  (* Syntax for lifted expressions outside the scope of |- or |= *)
    1.95 +  "LIFT"        :: lift => 'a                          ("LIFT _")
    1.96 +
    1.97 +  (* generic syntax for lifted constants and functions *)
    1.98 +  "_const"      :: 'a => lift                          ("(#_)" [1000] 999)
    1.99 +  "_lift"       :: ['a, lift] => lift                  ("(_<_>)" [1000] 999)
   1.100 +  "_lift2"      :: ['a, lift, lift] => lift            ("(_<_,/ _>)" [1000] 999)
   1.101 +  "_lift3"      :: ['a, lift, lift, lift] => lift      ("(_<_,/ _,/ _>)" [1000] 999)
   1.102 +
   1.103 +  (* concrete syntax for common infix functions: reuse same symbol *)
   1.104 +  "_liftEqu"    :: [lift, lift] => lift                ("(_ =/ _)" [50,51] 50)
   1.105 +  "_liftNeq"    :: [lift, lift] => lift                ("(_ ~=/ _)" [50,51] 50)
   1.106 +  "_liftNot"    :: lift => lift                        ("(~ _)" [40] 40)
   1.107 +  "_liftAnd"    :: [lift, lift] => lift                ("(_ &/ _)" [36,35] 35)
   1.108 +  "_liftOr"     :: [lift, lift] => lift                ("(_ |/ _)" [31,30] 30)
   1.109 +  "_liftImp"    :: [lift, lift] => lift                ("(_ -->/ _)" [26,25] 25)
   1.110 +  "_liftIf"     :: [lift, lift, lift] => lift          ("(if (_)/ then (_)/ else (_))" 10)
   1.111 +  "_liftPlus"   :: [lift, lift] => lift                ("(_ +/ _)" [66,65] 65)
   1.112 +  "_liftMinus"  :: [lift, lift] => lift                ("(_ -/ _)" [66,65] 65)
   1.113 +  "_liftTimes"  :: [lift, lift] => lift                ("(_ */ _)" [71,70] 70)
   1.114 +  "_liftDiv"    :: [lift, lift] => lift                ("(_ div _)" [71,70] 70)
   1.115 +  "_liftMod"    :: [lift, lift] => lift                ("(_ mod _)" [71,70] 70)
   1.116 +  "_liftLess"   :: [lift, lift] => lift                ("(_/ < _)"  [50, 51] 50)
   1.117 +  "_liftLeq"    :: [lift, lift] => lift                ("(_/ <= _)" [50, 51] 50)
   1.118 +  "_liftMem"    :: [lift, lift] => lift                ("(_/ : _)" [50, 51] 50)
   1.119 +  "_liftNotMem" :: [lift, lift] => lift                ("(_/ ~: _)" [50, 51] 50)
   1.120 +  "_liftFinset" :: liftargs => lift                    ("{(_)}")
   1.121 +  (** TODO: syntax for lifted collection / comprehension **)
   1.122 +  "_liftPair"   :: [lift,liftargs] => lift                   ("(1'(_,/ _'))")
   1.123 +  (* infix syntax for list operations *)
   1.124 +  "_liftCons" :: [lift, lift] => lift                    ("(_ #/ _)" [65,66] 65)
   1.125 +  "_liftApp"  :: [lift, lift] => lift                    ("(_ @/ _)" [65,66] 65)
   1.126 +  "_liftList" :: liftargs => lift                        ("[(_)]")
   1.127 +
   1.128 +  (* Rigid quantification (syntax level) *)
   1.129 +  "_RAll"  :: [idts, lift] => lift                     ("(3! _./ _)" [0, 10] 10)
   1.130 +  "_REx"   :: [idts, lift] => lift                     ("(3? _./ _)" [0, 10] 10)
   1.131 +  "_REx1"  :: [idts, lift] => lift                     ("(3?! _./ _)" [0, 10] 10)
   1.132 +  "_ARAll" :: [idts, lift] => lift                     ("(3ALL _./ _)" [0, 10] 10)
   1.133 +  "_AREx"  :: [idts, lift] => lift                     ("(3EX _./ _)" [0, 10] 10)
   1.134 +  "_AREx1" :: [idts, lift] => lift                     ("(3EX! _./ _)" [0, 10] 10)
   1.135  
   1.136  translations
   1.137 +  "_const"        == "const"
   1.138 +  "_lift"         == "lift"
   1.139 +  "_lift2"        == "lift2"
   1.140 +  "_lift3"        == "lift3"
   1.141 +  "_Valid"        == "Valid"
   1.142 +  "_RAll x A"     == "Rall x. A"
   1.143 +  "_REx x  A"     == "Rex x. A"
   1.144 +  "_REx1 x  A"    == "Rex! x. A"
   1.145 +  "_ARAll"        => "_RAll"
   1.146 +  "_AREx"         => "_REx"
   1.147 +  "_AREx1"        => "_REx1"
   1.148  
   1.149 -  "{[x,y,z]}"   == "{[x, {[y,z]} ]}"
   1.150 -  "{[x,y]}"     == "Pair [x, y]"
   1.151 -  "{[x]}"       => "x"
   1.152 +  "w |= A"        => "A w"
   1.153 +  "LIFT A"        => "A::_=>_"
   1.154  
   1.155 -  "u .= v" == "op =[u,v]"
   1.156 -  "u .~= v" == ".~(u .= v)"
   1.157 -  ".~ A"   == "Not[A]"
   1.158 -  "A .& B" == "op &[A,B]"
   1.159 -  "A .| B"  == "op |[A,B]"
   1.160 -  "A .-> B" == "op -->[A,B]"
   1.161 -  ".if A .then u .else v" == "If[A,u,v]"
   1.162 -  "u .+ v"  == "op +[u,v]"
   1.163 -  "u .- v" == "op -[u,v]"
   1.164 -  "u .* v" == "op *[u,v]"
   1.165 +  "_liftEqu"      == "_lift2 (op =)"
   1.166 +  "_liftNeq u v"  == "_liftNot (_liftEqu u v)"
   1.167 +  "_liftNot"      == "_lift Not"
   1.168 +  "_liftAnd"      == "_lift2 (op &)"
   1.169 +  "_liftOr"       == "_lift2 (op | )"
   1.170 +  "_liftImp"      == "_lift2 (op -->)"
   1.171 +  "_liftIf"       == "_lift3 If"
   1.172 +  "_liftPlus"     == "_lift2 (op +)"
   1.173 +  "_liftMinus"    == "_lift2 (op -)"
   1.174 +  "_liftTimes"    == "_lift2 (op *)"
   1.175 +  "_liftDiv"      == "_lift2 (op div)"
   1.176 +  "_liftMod"      == "_lift2 (op mod)"
   1.177 +  "_liftLess"     == "_lift2 (op <)"
   1.178 +  "_liftLeq"      == "_lift2 (op <=)"
   1.179 +  "_liftMem"      == "_lift2 (op :)"
   1.180 +  "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
   1.181 +  "_liftFinset (_liftargs x xs)"  == "_lift2 insert x (_liftFinset xs)"
   1.182 +  "_liftFinset x" == "_lift2 insert x (_const {})"
   1.183 +  "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
   1.184 +  "_liftPair"     == "_lift2 Pair"
   1.185 +  "_liftCons"     == "lift2 (op #)"
   1.186 +  "_liftApp"      == "lift2 (op @)"
   1.187 +  "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
   1.188 +  "_liftList x"   == "_liftCons x (_const [])"
   1.189  
   1.190 -  "a .< b"  == "op < [a,b]"
   1.191 -  "a .<= b" == "op <= [a,b]"
   1.192 -  "a .: A"  == "op :[a,A]"
   1.193 +  
   1.194  
   1.195 -  "holdsAt w (lift f x)"      == "lift f x w"
   1.196 -  "holdsAt w (lift2 f x y)"   == "lift2 f x y w"
   1.197 -  "holdsAt w (lift3 f x y z)" == "lift3 f x y z w"
   1.198 -
   1.199 -  "w |= A"              => "A(w)"
   1.200 +  "w |= ~A"       <= "_liftNot A w"
   1.201 +  "w |= A & B"    <= "_liftAnd A B w"
   1.202 +  "w |= A | B"    <= "_liftOr A B w"
   1.203 +  "w |= A --> B"  <= "_liftImp A B w"
   1.204 +  "w |= u = v"    <= "_liftEqu u v w"
   1.205 +  "w |= ! x. A"   <= "_RAll x A w"
   1.206 +  "w |= ? x. A"   <= "_REx x A w"
   1.207 +  "w |= ?! x. A"  <= "_REx1 x A w"
   1.208  
   1.209  syntax (symbols)
   1.210 -  holdsAt  :: "['w::world, 'w form] => bool"   ("(_ \\<Turnstile> _)" [100,9] 8)
   1.211 -
   1.212 +  "_Valid"      :: lift => bool                        ("(\\<turnstile> _)" 5)
   1.213 +  "_holdsAt"    :: ['a, lift] => bool                  ("(_ \\<Turnstile> _)" [100,10] 10)
   1.214 +  "_liftNeq"    :: [lift, lift] => lift                (infixl "\\<noteq>" 50)
   1.215 +  "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
   1.216 +  "_liftAnd"    :: [lift, lift] => lift                (infixr "\\<and>" 35)
   1.217 +  "_liftOr"     :: [lift, lift] => lift                (infixr "\\<or>" 30)
   1.218 +  "_liftImp"    :: [lift, lift] => lift                (infixr "\\<midarrow>\\<rightarrow>" 25)
   1.219 +  "_RAll"       :: [idts, lift] => lift                ("(3\\<forall>_./ _)" [0, 10] 10)
   1.220 +  "_REx"        :: [idts, lift] => lift                ("(3\\<exists>_./ _)" [0, 10] 10)
   1.221 +  "_REx1"       :: [idts, lift] => lift                ("(3\\<exists>!_./ _)" [0, 10] 10)
   1.222 +  "_liftLeq"    :: [lift, lift] => lift                ("(_/ \\<le> _)" [50, 51] 50)
   1.223 +  "_liftMem"    :: [lift, lift] => lift                ("(_/ \\<in> _)" [50, 51] 50)
   1.224 +  "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
   1.225  
   1.226  rules
   1.227 -  inteq_reflection   "(x .= y) ==> (x == y)"
   1.228 +  Valid_def   "|- A    ==  ALL w. w |= A"
   1.229  
   1.230 -  int_valid   "TrueInt(A) == (!! w. w |= A)"
   1.231 +  unl_con     "LIFT #c w  ==  c" 
   1.232 +  unl_lift    "LIFT f<x> w == f (x w)"
   1.233 +  unl_lift2   "LIFT f<x, y> w == f (x w) (y w)"
   1.234 +  unl_lift3   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
   1.235  
   1.236 -  unl_con     "(#c) w == c"             (* constants *)
   1.237 -  unl_lift    "(f[x]) w == f(x w)"
   1.238 -  unl_lift2   "(f[x,y]) w == f (x w) (y w)"
   1.239 -  unl_lift3   "(f[x, y, z]) w == f (x w) (y w) (z w)"
   1.240 +  unl_Rall    "w |= ! x. A x  ==  ! x. (w |= A x)" 
   1.241 +  unl_Rex     "w |= ? x. A x  ==  ? x. (w |= A x)"
   1.242 +  unl_Rex1    "w |= ?! x. A x  ==  ?! x. (w |= A x)"
   1.243 +end
   1.244  
   1.245 -  unl_Rall    "(RALL x. A(x)) w == ALL x. (w |= A(x))"
   1.246 -  unl_Rex     "(REX x. A(x)) w == EX x. (w |= A(x))"
   1.247 -
   1.248 -end
   1.249 +ML