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