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