src/HOL/TLA/Intensional.thy
author wenzelm
Tue Aug 07 23:24:10 2007 +0200 (2007-08-07)
changeset 24180 9f818139951b
parent 21624 6f79647cf536
child 30528 7173bf123335
permissions -rw-r--r--
tuned ML setup;
     1 (*
     2     File:        TLA/Intensional.thy
     3     ID:          $Id$
     4     Author:      Stephan Merz
     5     Copyright:   1998 University of Munich
     6 *)
     7 
     8 header {* A framework for "intensional" (possible-world based) logics
     9   on top of HOL, with lifting of constants and functions *}
    10 
    11 theory Intensional
    12 imports Main
    13 begin
    14 
    15 axclass
    16   world < type
    17 
    18 (** abstract syntax **)
    19 
    20 types
    21   ('w,'a) expr = "'w => 'a"               (* intention: 'w::world, 'a::type *)
    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   "_ARAll"  :: "[idts, lift] => lift"                    ("(3! _./ _)" [0, 10] 10)
    91   "_AREx"   :: "[idts, lift] => lift"                    ("(3? _./ _)" [0, 10] 10)
    92   "_AREx1"  :: "[idts, lift] => lift"                    ("(3?! _./ _)" [0, 10] 10)
    93   "_RAll" :: "[idts, lift] => lift"                      ("(3ALL _./ _)" [0, 10] 10)
    94   "_REx"  :: "[idts, lift] => lift"                      ("(3EX _./ _)" [0, 10] 10)
    95   "_REx1" :: "[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 Cons"
   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 |= ALL x. A"   <= "_RAll x A w"
   146   "w |= EX x. A"   <= "_REx x A w"
   147   "w |= EX! x. A"  <= "_REx1 x A w"
   148 
   149 syntax (xsymbols)
   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 "\<longrightarrow>" 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   "_liftNeq"    :: "[lift, lift] => lift"                (infixl "\<noteq>" 50)
   166   "_liftNot"    :: "lift => lift"                        ("\<not> _" [40] 40)
   167   "_liftAnd"    :: "[lift, lift] => lift"                (infixr "\<and>" 35)
   168   "_liftOr"     :: "[lift, lift] => lift"                (infixr "\<or>" 30)
   169   "_RAll"       :: "[idts, lift] => lift"                ("(3\<forall>_./ _)" [0, 10] 10)
   170   "_REx"        :: "[idts, lift] => lift"                ("(3\<exists>_./ _)" [0, 10] 10)
   171   "_REx1"       :: "[idts, lift] => lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
   172   "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ \<le> _)" [50, 51] 50)
   173   "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
   174   "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)
   175 
   176 axioms
   177   Valid_def:   "|- A    ==  ALL w. w |= A"
   178 
   179   unl_con:     "LIFT #c w  ==  c"
   180   unl_lift:    "lift f x w == f (x w)"
   181   unl_lift2:   "LIFT f<x, y> w == f (x w) (y w)"
   182   unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
   183 
   184   unl_Rall:    "w |= ALL x. A x  ==  ALL x. (w |= A x)"
   185   unl_Rex:     "w |= EX x. A x   ==  EX x. (w |= A x)"
   186   unl_Rex1:    "w |= EX! x. A x  ==  EX! x. (w |= A x)"
   187 
   188 
   189 subsection {* Lemmas and tactics for "intensional" logics. *}
   190 
   191 lemmas intensional_rews [simp] =
   192   unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1
   193 
   194 lemma inteq_reflection: "|- x=y  ==>  (x==y)"
   195   apply (unfold Valid_def unl_lift2)
   196   apply (rule eq_reflection)
   197   apply (rule ext)
   198   apply (erule spec)
   199   done
   200 
   201 lemma intI [intro!]: "(!!w. w |= A) ==> |- A"
   202   apply (unfold Valid_def)
   203   apply (rule allI)
   204   apply (erule meta_spec)
   205   done
   206 
   207 lemma intD [dest]: "|- A ==> w |= A"
   208   apply (unfold Valid_def)
   209   apply (erule spec)
   210   done
   211 
   212 (** Lift usual HOL simplifications to "intensional" level. **)
   213 
   214 lemma int_simps:
   215   "|- (x=x) = #True"
   216   "|- (~#True) = #False"  "|- (~#False) = #True"  "|- (~~ P) = P"
   217   "|- ((~P) = P) = #False"  "|- (P = (~P)) = #False"
   218   "|- (P ~= Q) = (P = (~Q))"
   219   "|- (#True=P) = P"  "|- (P=#True) = P"
   220   "|- (#True --> P) = P"  "|- (#False --> P) = #True"
   221   "|- (P --> #True) = #True"  "|- (P --> P) = #True"
   222   "|- (P --> #False) = (~P)"  "|- (P --> ~P) = (~P)"
   223   "|- (P & #True) = P"  "|- (#True & P) = P"
   224   "|- (P & #False) = #False"  "|- (#False & P) = #False"
   225   "|- (P & P) = P"  "|- (P & ~P) = #False"  "|- (~P & P) = #False"
   226   "|- (P | #True) = #True"  "|- (#True | P) = #True"
   227   "|- (P | #False) = P"  "|- (#False | P) = P"
   228   "|- (P | P) = P"  "|- (P | ~P) = #True"  "|- (~P | P) = #True"
   229   "|- (! x. P) = P"  "|- (? x. P) = P"
   230   "|- (~Q --> ~P) = (P --> Q)"
   231   "|- (P|Q --> R) = ((P-->R)&(Q-->R))"
   232   apply (unfold Valid_def intensional_rews)
   233   apply blast+
   234   done
   235 
   236 declare int_simps [THEN inteq_reflection, simp]
   237 
   238 lemma TrueW [simp]: "|- #True"
   239   by (simp add: Valid_def unl_con)
   240 
   241 
   242 
   243 (* ======== Functions to "unlift" intensional implications into HOL rules ====== *)
   244 
   245 ML {*
   246 (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
   247    |- F = G    becomes   F w = G w
   248    |- F --> G  becomes   F w --> G w
   249 *)
   250 
   251 fun int_unlift th =
   252   rewrite_rule @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
   253 
   254 (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
   255 fun int_rewrite th =
   256   zero_var_indexes (rewrite_rule @{thms intensional_rews} (th RS @{thm inteq_reflection}))
   257 
   258 (* flattening turns "-->" into "==>" and eliminates conjunctions in the
   259    antecedent. For example,
   260 
   261          P & Q --> (R | S --> T)    becomes   [| P; Q; R | S |] ==> T
   262 
   263    Flattening can be useful with "intensional" lemmas (after unlifting).
   264    Naive resolution with mp and conjI may run away because of higher-order
   265    unification, therefore the code is a little awkward.
   266 *)
   267 fun flatten t =
   268   let
   269     (* analogous to RS, but using matching instead of resolution *)
   270     fun matchres tha i thb =
   271       case Seq.chop 2 (biresolution true [(false,tha)] i thb) of
   272           ([th],_) => th
   273         | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
   274         |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
   275 
   276     (* match tha with some premise of thb *)
   277     fun matchsome tha thb =
   278       let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
   279             | hmatch n = matchres tha n thb handle THM _ => hmatch (n-1)
   280       in hmatch (nprems_of thb) end
   281 
   282     fun hflatten t =
   283         case (concl_of t) of
   284           Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp)
   285         | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
   286   in
   287     hflatten t
   288   end
   289 
   290 fun int_use th =
   291     case (concl_of th) of
   292       Const _ $ (Const ("Intensional.Valid", _) $ _) =>
   293               (flatten (int_unlift th) handle THM _ => th)
   294     | _ => th
   295 *}
   296 
   297 setup {*
   298   Attrib.add_attributes [
   299     ("int_unlift", Attrib.no_args (Thm.rule_attribute (K int_unlift)), ""),
   300     ("int_rewrite", Attrib.no_args (Thm.rule_attribute (K int_rewrite)), ""),
   301     ("flatten", Attrib.no_args (Thm.rule_attribute (K flatten)), ""),
   302     ("int_use", Attrib.no_args (Thm.rule_attribute (K int_use)), "")]
   303 *}
   304 
   305 lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
   306   by (simp add: Valid_def)
   307 
   308 lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)"
   309   by (simp add: Valid_def)
   310 
   311 end