src/HOL/TLA/Intensional.thy
author wenzelm
Wed Oct 08 11:50:33 1997 +0200 (1997-10-08)
changeset 3807 82a99b090d9d
child 3808 8489375c6198
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;
     1 (* 
     2     File:	 TLA/Intensional.thy
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     Theory Name: Intensional
     7     Logic Image: HOL
     8 
     9 Define a framework for "intensional" (possible-world based) logics
    10 on top of HOL, with lifting of constants and functions.
    11 *)
    12 
    13 Intensional  =  Prod +
    14 
    15 classes
    16     world < logic    (* Type class of "possible worlds". Concrete types
    17                         will be provided by children theories. *)
    18 
    19 types
    20     ('a,'w) term = "'w => 'a"    (* Intention: 'w::world *)
    21     'w form = "'w => bool"
    22 
    23 consts
    24   TrueInt  :: "('w::world form) => prop"             ("(_)" 5)
    25 
    26   (* Holds at *)
    27   holdsAt  :: "['w::world, 'w form] => bool"   ("(_ |= _)" [100,9] 8)
    28 
    29   (* Lifting base functions to "intensional" level *)
    30   con      :: "'a => ('w::world => 'a)"               ("(#_)" [100] 99)
    31   lift     :: "['a => 'b, 'w::world => 'a] => ('w => 'b)"  ("(_[_])")
    32   lift2    :: "['a => ('b => 'c), 'w::world => 'a, 'w => 'b] => ('w => 'c)" ("(_[_,/ _])")
    33   lift3    :: "['a => 'b => 'c => 'd, 'w::world => 'a, 'w => 'b, 'w => 'c] => ('w => 'd)" ("(_[_,/ _,/ _])")
    34 
    35   (* Lifted infix functions *)
    36   IntEqu   :: "['w::world => 'a, 'w => 'a] => 'w form"  ("(_ .=/ _)" [50,51] 50)
    37   IntNeq   :: "['w::world => 'a, 'w => 'a] => 'w form"  ("(_ .~=/ _)" [50,51] 50)
    38   NotInt   :: "('w::world) form => 'w form"               ("(.~ _)" [40] 40)
    39   AndInt   :: "[('w::world) form, 'w form] => 'w form"    ("(_ .&/ _)" [36,35] 35)
    40   OrInt    :: "[('w::world) form, 'w form] => 'w form"    ("(_ .|/ _)" [31,30] 30)
    41   ImpInt   :: "[('w::world) form, 'w form] => 'w form"    ("(_ .->/ _)" [26,25] 25)
    42   IfInt    :: "[('w::world) form, ('a,'w) term, ('a,'w) term] => ('a,'w) term" ("(.if (_)/ .then (_)/ .else (_))" 10)
    43   PlusInt  :: "[('w::world) => ('a::plus), 'w => 'a] => ('w => 'a)"  ("(_ .+/ _)" [66,65] 65)
    44   MinusInt :: "[('w::world) => ('a::minus), 'w => 'a] => ('w => 'a)"  ("(_ .-/ _)" [66,65] 65)
    45   TimesInt :: "[('w::world) => ('a::times), 'w => 'a] => ('w => 'a)"  ("(_ .*/ _)" [71,70] 70)
    46 
    47   LessInt  :: "['w::world => 'a::ord, 'w => 'a] => 'w form"        ("(_/ .< _)"  [50, 51] 50)
    48   LeqInt   :: "['w::world => 'a::ord, 'w => 'a] => 'w form"        ("(_/ .<= _)" [50, 51] 50)
    49 
    50   (* lifted set membership *)
    51   memInt   :: "[('a,'w::world) term, ('a set,'w) term] => 'w form"  ("(_/ .: _)" [50, 51] 50)
    52 
    53   (* "Rigid" quantification *)
    54   RAll     :: "('a => 'w::world form) => 'w form"     (binder "RALL " 10)
    55   REx      :: "('a => 'w::world form) => 'w form"     (binder "REX " 10)
    56 
    57 syntax
    58   "@tupleInt"    :: "args => ('a * 'b, 'w) term"  ("(1{[_]})")
    59 
    60 translations
    61 
    62   "{[x,y,z]}"   == "{[x, {[y,z]} ]}"
    63   "{[x,y]}"     == "Pair [x, y]"
    64   "{[x]}"       => "x"
    65 
    66   "u .= v" == "op =[u,v]"
    67   "u .~= v" == ".~(u .= v)"
    68   ".~ A"   == "Not[A]"
    69   "A .& B" == "op &[A,B]"
    70   "A .| B"  == "op |[A,B]"
    71   "A .-> B" == "op -->[A,B]"
    72   ".if A .then u .else v" == "If[A,u,v]"
    73   "u .+ v"  == "op +[u,v]"
    74   "u .- v" == "op -[u,v]"
    75   "u .* v" == "op *[u,v]"
    76 
    77   "a .< b"  == "op < [a,b]"
    78   "a .<= b" == "op <= [a,b]"
    79   "a .: A"  == "op :[a,A]"
    80 
    81   "holdsAt w (lift f x)"      == "lift f x w"
    82   "holdsAt w (lift2 f x y)"   == "lift2 f x y w"
    83   "holdsAt w (lift3 f x y z)" == "lift3 f x y z w"
    84 
    85   "w |= A"              => "A(w)"
    86 
    87 rules
    88   inteq_reflection   "(x .= y) ==> (x == y)"
    89 
    90   int_valid   "TrueInt(A) == (!! w. w |= A)"
    91 
    92   unl_con     "(#c) w == c"             (* constants *)
    93   unl_lift    "(f[x]) w == f(x w)"
    94   unl_lift2   "(f[x,y]) w == f (x w) (y w)"
    95   unl_lift3   "(f[x, y, z]) w == f (x w) (y w) (z w)"
    96 
    97   unl_Rall    "(RALL x. A(x)) w == ALL x. (w |= A(x))"
    98   unl_Rex     "(REX x. A(x)) w == EX x. (w |= A(x))"
    99 end
   100 
   101 ML