src/HOL/TLA/Intensional.thy
author wenzelm
Wed Sep 07 20:22:39 2005 +0200 (2005-09-07)
changeset 17309 c43ed29bd197
parent 14565 c6dc17aab88a
child 21020 9af9ceb16d58
permissions -rw-r--r--
converted to Isar theory format;
wenzelm@17309
     1
(*
wenzelm@17309
     2
    File:        TLA/Intensional.thy
wenzelm@17309
     3
    ID:          $Id$
wenzelm@3807
     4
    Author:      Stephan Merz
wenzelm@6255
     5
    Copyright:   1998 University of Munich
wenzelm@3807
     6
wenzelm@3807
     7
    Theory Name: Intensional
wenzelm@3807
     8
    Logic Image: HOL
wenzelm@3807
     9
wenzelm@3807
    10
Define a framework for "intensional" (possible-world based) logics
wenzelm@3807
    11
on top of HOL, with lifting of constants and functions.
wenzelm@3807
    12
*)
wenzelm@3807
    13
wenzelm@17309
    14
theory Intensional
wenzelm@17309
    15
imports Main
wenzelm@17309
    16
begin
wenzelm@3807
    17
wenzelm@6255
    18
axclass
wenzelm@12338
    19
  world < type
wenzelm@6255
    20
wenzelm@6255
    21
(** abstract syntax **)
wenzelm@3807
    22
wenzelm@3807
    23
types
wenzelm@17309
    24
  ('w,'a) expr = "'w => 'a"               (* intention: 'w::world, 'a::type *)
wenzelm@17309
    25
  'w form = "('w, bool) expr"
wenzelm@3807
    26
wenzelm@3807
    27
consts
wenzelm@17309
    28
  Valid    :: "('w::world) form => bool"
wenzelm@17309
    29
  const    :: "'a => ('w::world, 'a) expr"
wenzelm@17309
    30
  lift     :: "['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr"
wenzelm@17309
    31
  lift2    :: "['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr"
wenzelm@17309
    32
  lift3    :: "['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr"
wenzelm@3807
    33
wenzelm@6255
    34
  (* "Rigid" quantification (logic level) *)
wenzelm@6255
    35
  RAll     :: "('a => ('w::world) form) => 'w form"       (binder "Rall " 10)
wenzelm@6255
    36
  REx      :: "('a => ('w::world) form) => 'w form"       (binder "Rex " 10)
wenzelm@6255
    37
  REx1     :: "('a => ('w::world) form) => 'w form"       (binder "Rex! " 10)
wenzelm@3807
    38
wenzelm@6255
    39
(** concrete syntax **)
wenzelm@3807
    40
wenzelm@6255
    41
nonterminals
wenzelm@6255
    42
  lift
wenzelm@6255
    43
  liftargs
wenzelm@3807
    44
wenzelm@3807
    45
syntax
wenzelm@17309
    46
  ""            :: "id => lift"                          ("_")
wenzelm@17309
    47
  ""            :: "longid => lift"                      ("_")
wenzelm@17309
    48
  ""            :: "var => lift"                         ("_")
wenzelm@17309
    49
  "_applC"      :: "[lift, cargs] => lift"               ("(1_/ _)" [1000, 1000] 999)
wenzelm@17309
    50
  ""            :: "lift => lift"                        ("'(_')")
wenzelm@17309
    51
  "_lambda"     :: "[idts, 'a] => lift"                  ("(3%_./ _)" [0, 3] 3)
wenzelm@17309
    52
  "_constrain"  :: "[lift, type] => lift"                ("(_::_)" [4, 0] 3)
wenzelm@17309
    53
  ""            :: "lift => liftargs"                    ("_")
wenzelm@17309
    54
  "_liftargs"   :: "[lift, liftargs] => liftargs"        ("_,/ _")
wenzelm@17309
    55
  "_Valid"      :: "lift => bool"                        ("(|- _)" 5)
wenzelm@17309
    56
  "_holdsAt"    :: "['a, lift] => bool"                  ("(_ |= _)" [100,10] 10)
wenzelm@6255
    57
wenzelm@6255
    58
  (* Syntax for lifted expressions outside the scope of |- or |= *)
wenzelm@17309
    59
  "LIFT"        :: "lift => 'a"                          ("LIFT _")
wenzelm@6255
    60
wenzelm@6255
    61
  (* generic syntax for lifted constants and functions *)
wenzelm@17309
    62
  "_const"      :: "'a => lift"                          ("(#_)" [1000] 999)
wenzelm@17309
    63
  "_lift"       :: "['a, lift] => lift"                  ("(_<_>)" [1000] 999)
wenzelm@17309
    64
  "_lift2"      :: "['a, lift, lift] => lift"            ("(_<_,/ _>)" [1000] 999)
wenzelm@17309
    65
  "_lift3"      :: "['a, lift, lift, lift] => lift"      ("(_<_,/ _,/ _>)" [1000] 999)
wenzelm@6255
    66
wenzelm@6255
    67
  (* concrete syntax for common infix functions: reuse same symbol *)
wenzelm@17309
    68
  "_liftEqu"    :: "[lift, lift] => lift"                ("(_ =/ _)" [50,51] 50)
wenzelm@17309
    69
  "_liftNeq"    :: "[lift, lift] => lift"                ("(_ ~=/ _)" [50,51] 50)
wenzelm@17309
    70
  "_liftNot"    :: "lift => lift"                        ("(~ _)" [40] 40)
wenzelm@17309
    71
  "_liftAnd"    :: "[lift, lift] => lift"                ("(_ &/ _)" [36,35] 35)
wenzelm@17309
    72
  "_liftOr"     :: "[lift, lift] => lift"                ("(_ |/ _)" [31,30] 30)
wenzelm@17309
    73
  "_liftImp"    :: "[lift, lift] => lift"                ("(_ -->/ _)" [26,25] 25)
wenzelm@17309
    74
  "_liftIf"     :: "[lift, lift, lift] => lift"          ("(if (_)/ then (_)/ else (_))" 10)
wenzelm@17309
    75
  "_liftPlus"   :: "[lift, lift] => lift"                ("(_ +/ _)" [66,65] 65)
wenzelm@17309
    76
  "_liftMinus"  :: "[lift, lift] => lift"                ("(_ -/ _)" [66,65] 65)
wenzelm@17309
    77
  "_liftTimes"  :: "[lift, lift] => lift"                ("(_ */ _)" [71,70] 70)
wenzelm@17309
    78
  "_liftDiv"    :: "[lift, lift] => lift"                ("(_ div _)" [71,70] 70)
wenzelm@17309
    79
  "_liftMod"    :: "[lift, lift] => lift"                ("(_ mod _)" [71,70] 70)
wenzelm@17309
    80
  "_liftLess"   :: "[lift, lift] => lift"                ("(_/ < _)"  [50, 51] 50)
wenzelm@17309
    81
  "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ <= _)" [50, 51] 50)
wenzelm@17309
    82
  "_liftMem"    :: "[lift, lift] => lift"                ("(_/ : _)" [50, 51] 50)
wenzelm@17309
    83
  "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ ~: _)" [50, 51] 50)
wenzelm@17309
    84
  "_liftFinset" :: "liftargs => lift"                    ("{(_)}")
wenzelm@6255
    85
  (** TODO: syntax for lifted collection / comprehension **)
wenzelm@17309
    86
  "_liftPair"   :: "[lift,liftargs] => lift"                   ("(1'(_,/ _'))")
wenzelm@6255
    87
  (* infix syntax for list operations *)
wenzelm@17309
    88
  "_liftCons" :: "[lift, lift] => lift"                  ("(_ #/ _)" [65,66] 65)
wenzelm@17309
    89
  "_liftApp"  :: "[lift, lift] => lift"                  ("(_ @/ _)" [65,66] 65)
wenzelm@17309
    90
  "_liftList" :: "liftargs => lift"                      ("[(_)]")
wenzelm@6255
    91
wenzelm@6255
    92
  (* Rigid quantification (syntax level) *)
wenzelm@17309
    93
  "_ARAll"  :: "[idts, lift] => lift"                    ("(3! _./ _)" [0, 10] 10)
wenzelm@17309
    94
  "_AREx"   :: "[idts, lift] => lift"                    ("(3? _./ _)" [0, 10] 10)
wenzelm@17309
    95
  "_AREx1"  :: "[idts, lift] => lift"                    ("(3?! _./ _)" [0, 10] 10)
wenzelm@17309
    96
  "_RAll" :: "[idts, lift] => lift"                      ("(3ALL _./ _)" [0, 10] 10)
wenzelm@17309
    97
  "_REx"  :: "[idts, lift] => lift"                      ("(3EX _./ _)" [0, 10] 10)
wenzelm@17309
    98
  "_REx1" :: "[idts, lift] => lift"                      ("(3EX! _./ _)" [0, 10] 10)
wenzelm@3807
    99
wenzelm@3807
   100
translations
wenzelm@6255
   101
  "_const"        == "const"
wenzelm@6255
   102
  "_lift"         == "lift"
wenzelm@6255
   103
  "_lift2"        == "lift2"
wenzelm@6255
   104
  "_lift3"        == "lift3"
wenzelm@6255
   105
  "_Valid"        == "Valid"
wenzelm@6255
   106
  "_RAll x A"     == "Rall x. A"
wenzelm@6255
   107
  "_REx x  A"     == "Rex x. A"
wenzelm@6255
   108
  "_REx1 x  A"    == "Rex! x. A"
wenzelm@6255
   109
  "_ARAll"        => "_RAll"
wenzelm@6255
   110
  "_AREx"         => "_REx"
wenzelm@6255
   111
  "_AREx1"        => "_REx1"
wenzelm@3807
   112
wenzelm@6255
   113
  "w |= A"        => "A w"
wenzelm@6255
   114
  "LIFT A"        => "A::_=>_"
wenzelm@3807
   115
wenzelm@6255
   116
  "_liftEqu"      == "_lift2 (op =)"
wenzelm@6255
   117
  "_liftNeq u v"  == "_liftNot (_liftEqu u v)"
wenzelm@6255
   118
  "_liftNot"      == "_lift Not"
wenzelm@6255
   119
  "_liftAnd"      == "_lift2 (op &)"
wenzelm@6255
   120
  "_liftOr"       == "_lift2 (op | )"
wenzelm@6255
   121
  "_liftImp"      == "_lift2 (op -->)"
wenzelm@6255
   122
  "_liftIf"       == "_lift3 If"
wenzelm@6255
   123
  "_liftPlus"     == "_lift2 (op +)"
wenzelm@6255
   124
  "_liftMinus"    == "_lift2 (op -)"
wenzelm@6255
   125
  "_liftTimes"    == "_lift2 (op *)"
wenzelm@6255
   126
  "_liftDiv"      == "_lift2 (op div)"
wenzelm@6255
   127
  "_liftMod"      == "_lift2 (op mod)"
wenzelm@6255
   128
  "_liftLess"     == "_lift2 (op <)"
wenzelm@6255
   129
  "_liftLeq"      == "_lift2 (op <=)"
wenzelm@6255
   130
  "_liftMem"      == "_lift2 (op :)"
wenzelm@6255
   131
  "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
wenzelm@6255
   132
  "_liftFinset (_liftargs x xs)"  == "_lift2 insert x (_liftFinset xs)"
wenzelm@6255
   133
  "_liftFinset x" == "_lift2 insert x (_const {})"
wenzelm@6255
   134
  "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
wenzelm@6255
   135
  "_liftPair"     == "_lift2 Pair"
wenzelm@7224
   136
  "_liftCons"     == "lift2 Cons"
wenzelm@6255
   137
  "_liftApp"      == "lift2 (op @)"
wenzelm@6255
   138
  "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
wenzelm@6255
   139
  "_liftList x"   == "_liftCons x (_const [])"
wenzelm@3807
   140
wenzelm@17309
   141
wenzelm@3807
   142
wenzelm@6255
   143
  "w |= ~A"       <= "_liftNot A w"
wenzelm@6255
   144
  "w |= A & B"    <= "_liftAnd A B w"
wenzelm@6255
   145
  "w |= A | B"    <= "_liftOr A B w"
wenzelm@6255
   146
  "w |= A --> B"  <= "_liftImp A B w"
wenzelm@6255
   147
  "w |= u = v"    <= "_liftEqu u v w"
wenzelm@9517
   148
  "w |= ALL x. A"   <= "_RAll x A w"
wenzelm@9517
   149
  "w |= EX x. A"   <= "_REx x A w"
wenzelm@9517
   150
  "w |= EX! x. A"  <= "_REx1 x A w"
wenzelm@3807
   151
wenzelm@12114
   152
syntax (xsymbols)
wenzelm@17309
   153
  "_Valid"      :: "lift => bool"                        ("(\<turnstile> _)" 5)
wenzelm@17309
   154
  "_holdsAt"    :: "['a, lift] => bool"                  ("(_ \<Turnstile> _)" [100,10] 10)
wenzelm@17309
   155
  "_liftNeq"    :: "[lift, lift] => lift"                (infixl "\<noteq>" 50)
wenzelm@17309
   156
  "_liftNot"    :: "lift => lift"                        ("\<not> _" [40] 40)
wenzelm@17309
   157
  "_liftAnd"    :: "[lift, lift] => lift"                (infixr "\<and>" 35)
wenzelm@17309
   158
  "_liftOr"     :: "[lift, lift] => lift"                (infixr "\<or>" 30)
wenzelm@17309
   159
  "_liftImp"    :: "[lift, lift] => lift"                (infixr "\<longrightarrow>" 25)
wenzelm@17309
   160
  "_RAll"       :: "[idts, lift] => lift"                ("(3\<forall>_./ _)" [0, 10] 10)
wenzelm@17309
   161
  "_REx"        :: "[idts, lift] => lift"                ("(3\<exists>_./ _)" [0, 10] 10)
wenzelm@17309
   162
  "_REx1"       :: "[idts, lift] => lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
wenzelm@17309
   163
  "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ \<le> _)" [50, 51] 50)
wenzelm@17309
   164
  "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
wenzelm@17309
   165
  "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)
wenzelm@3808
   166
wenzelm@6340
   167
syntax (HTML output)
wenzelm@17309
   168
  "_liftNeq"    :: "[lift, lift] => lift"                (infixl "\<noteq>" 50)
wenzelm@17309
   169
  "_liftNot"    :: "lift => lift"                        ("\<not> _" [40] 40)
wenzelm@17309
   170
  "_liftAnd"    :: "[lift, lift] => lift"                (infixr "\<and>" 35)
wenzelm@17309
   171
  "_liftOr"     :: "[lift, lift] => lift"                (infixr "\<or>" 30)
wenzelm@17309
   172
  "_RAll"       :: "[idts, lift] => lift"                ("(3\<forall>_./ _)" [0, 10] 10)
wenzelm@17309
   173
  "_REx"        :: "[idts, lift] => lift"                ("(3\<exists>_./ _)" [0, 10] 10)
wenzelm@17309
   174
  "_REx1"       :: "[idts, lift] => lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
wenzelm@17309
   175
  "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ \<le> _)" [50, 51] 50)
wenzelm@17309
   176
  "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
wenzelm@17309
   177
  "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)
wenzelm@6340
   178
wenzelm@17309
   179
axioms
wenzelm@17309
   180
  Valid_def:   "|- A    ==  ALL w. w |= A"
wenzelm@17309
   181
wenzelm@17309
   182
  unl_con:     "LIFT #c w  ==  c"
wenzelm@17309
   183
  unl_lift:    "LIFT f<x> w == f (x w)"
wenzelm@17309
   184
  unl_lift2:   "LIFT f<x, y> w == f (x w) (y w)"
wenzelm@17309
   185
  unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
wenzelm@3807
   186
wenzelm@17309
   187
  unl_Rall:    "w |= ALL x. A x  ==  ALL x. (w |= A x)"
wenzelm@17309
   188
  unl_Rex:     "w |= EX x. A x   ==  EX x. (w |= A x)"
wenzelm@17309
   189
  unl_Rex1:    "w |= EX! x. A x  ==  EX! x. (w |= A x)"
wenzelm@3807
   190
wenzelm@17309
   191
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17309
   192
wenzelm@6255
   193
end