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