src/HOL/TLA/Intensional.thy
changeset 3807 82a99b090d9d
child 3808 8489375c6198
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Oct 08 11:50:33 1997 +0200
     1.3 @@ -0,0 +1,101 @@
     1.4 +(* 
     1.5 +    File:	 TLA/Intensional.thy
     1.6 +    Author:      Stephan Merz
     1.7 +    Copyright:   1997 University of Munich
     1.8 +
     1.9 +    Theory Name: Intensional
    1.10 +    Logic Image: HOL
    1.11 +
    1.12 +Define a framework for "intensional" (possible-world based) logics
    1.13 +on top of HOL, with lifting of constants and functions.
    1.14 +*)
    1.15 +
    1.16 +Intensional  =  Prod +
    1.17 +
    1.18 +classes
    1.19 +    world < logic    (* Type class of "possible worlds". Concrete types
    1.20 +                        will be provided by children theories. *)
    1.21 +
    1.22 +types
    1.23 +    ('a,'w) term = "'w => 'a"    (* Intention: 'w::world *)
    1.24 +    'w form = "'w => bool"
    1.25 +
    1.26 +consts
    1.27 +  TrueInt  :: "('w::world form) => prop"             ("(_)" 5)
    1.28 +
    1.29 +  (* Holds at *)
    1.30 +  holdsAt  :: "['w::world, 'w form] => bool"   ("(_ |= _)" [100,9] 8)
    1.31 +
    1.32 +  (* Lifting base functions to "intensional" level *)
    1.33 +  con      :: "'a => ('w::world => 'a)"               ("(#_)" [100] 99)
    1.34 +  lift     :: "['a => 'b, 'w::world => 'a] => ('w => 'b)"  ("(_[_])")
    1.35 +  lift2    :: "['a => ('b => 'c), 'w::world => 'a, 'w => 'b] => ('w => 'c)" ("(_[_,/ _])")
    1.36 +  lift3    :: "['a => 'b => 'c => 'd, 'w::world => 'a, 'w => 'b, 'w => 'c] => ('w => 'd)" ("(_[_,/ _,/ _])")
    1.37 +
    1.38 +  (* Lifted infix functions *)
    1.39 +  IntEqu   :: "['w::world => 'a, 'w => 'a] => 'w form"  ("(_ .=/ _)" [50,51] 50)
    1.40 +  IntNeq   :: "['w::world => 'a, 'w => 'a] => 'w form"  ("(_ .~=/ _)" [50,51] 50)
    1.41 +  NotInt   :: "('w::world) form => 'w form"               ("(.~ _)" [40] 40)
    1.42 +  AndInt   :: "[('w::world) form, 'w form] => 'w form"    ("(_ .&/ _)" [36,35] 35)
    1.43 +  OrInt    :: "[('w::world) form, 'w form] => 'w form"    ("(_ .|/ _)" [31,30] 30)
    1.44 +  ImpInt   :: "[('w::world) form, 'w form] => 'w form"    ("(_ .->/ _)" [26,25] 25)
    1.45 +  IfInt    :: "[('w::world) form, ('a,'w) term, ('a,'w) term] => ('a,'w) term" ("(.if (_)/ .then (_)/ .else (_))" 10)
    1.46 +  PlusInt  :: "[('w::world) => ('a::plus), 'w => 'a] => ('w => 'a)"  ("(_ .+/ _)" [66,65] 65)
    1.47 +  MinusInt :: "[('w::world) => ('a::minus), 'w => 'a] => ('w => 'a)"  ("(_ .-/ _)" [66,65] 65)
    1.48 +  TimesInt :: "[('w::world) => ('a::times), 'w => 'a] => ('w => 'a)"  ("(_ .*/ _)" [71,70] 70)
    1.49 +
    1.50 +  LessInt  :: "['w::world => 'a::ord, 'w => 'a] => 'w form"        ("(_/ .< _)"  [50, 51] 50)
    1.51 +  LeqInt   :: "['w::world => 'a::ord, 'w => 'a] => 'w form"        ("(_/ .<= _)" [50, 51] 50)
    1.52 +
    1.53 +  (* lifted set membership *)
    1.54 +  memInt   :: "[('a,'w::world) term, ('a set,'w) term] => 'w form"  ("(_/ .: _)" [50, 51] 50)
    1.55 +
    1.56 +  (* "Rigid" quantification *)
    1.57 +  RAll     :: "('a => 'w::world form) => 'w form"     (binder "RALL " 10)
    1.58 +  REx      :: "('a => 'w::world form) => 'w form"     (binder "REX " 10)
    1.59 +
    1.60 +syntax
    1.61 +  "@tupleInt"    :: "args => ('a * 'b, 'w) term"  ("(1{[_]})")
    1.62 +
    1.63 +translations
    1.64 +
    1.65 +  "{[x,y,z]}"   == "{[x, {[y,z]} ]}"
    1.66 +  "{[x,y]}"     == "Pair [x, y]"
    1.67 +  "{[x]}"       => "x"
    1.68 +
    1.69 +  "u .= v" == "op =[u,v]"
    1.70 +  "u .~= v" == ".~(u .= v)"
    1.71 +  ".~ A"   == "Not[A]"
    1.72 +  "A .& B" == "op &[A,B]"
    1.73 +  "A .| B"  == "op |[A,B]"
    1.74 +  "A .-> B" == "op -->[A,B]"
    1.75 +  ".if A .then u .else v" == "If[A,u,v]"
    1.76 +  "u .+ v"  == "op +[u,v]"
    1.77 +  "u .- v" == "op -[u,v]"
    1.78 +  "u .* v" == "op *[u,v]"
    1.79 +
    1.80 +  "a .< b"  == "op < [a,b]"
    1.81 +  "a .<= b" == "op <= [a,b]"
    1.82 +  "a .: A"  == "op :[a,A]"
    1.83 +
    1.84 +  "holdsAt w (lift f x)"      == "lift f x w"
    1.85 +  "holdsAt w (lift2 f x y)"   == "lift2 f x y w"
    1.86 +  "holdsAt w (lift3 f x y z)" == "lift3 f x y z w"
    1.87 +
    1.88 +  "w |= A"              => "A(w)"
    1.89 +
    1.90 +rules
    1.91 +  inteq_reflection   "(x .= y) ==> (x == y)"
    1.92 +
    1.93 +  int_valid   "TrueInt(A) == (!! w. w |= A)"
    1.94 +
    1.95 +  unl_con     "(#c) w == c"             (* constants *)
    1.96 +  unl_lift    "(f[x]) w == f(x w)"
    1.97 +  unl_lift2   "(f[x,y]) w == f (x w) (y w)"
    1.98 +  unl_lift3   "(f[x, y, z]) w == f (x w) (y w) (z w)"
    1.99 +
   1.100 +  unl_Rall    "(RALL x. A(x)) w == ALL x. (w |= A(x))"
   1.101 +  unl_Rex     "(REX x. A(x)) w == EX x. (w |= A(x))"
   1.102 +end
   1.103 +
   1.104 +ML