src/HOL/TLA/Intensional.thy
author wenzelm
Fri Jun 26 15:55:44 2015 +0200 (2015-06-26)
changeset 60591 e0b77517f9a9
parent 60588 750c533459b1
child 60592 c9bd1d902f04
permissions -rw-r--r--
more symbols;
eliminated alternative syntax;
     1 (*  Title:      HOL/TLA/Intensional.thy
     2     Author:     Stephan Merz
     3     Copyright:  1998 University of Munich
     4 *)
     5 
     6 section {* A framework for "intensional" (possible-world based) logics
     7   on top of HOL, with lifting of constants and functions *}
     8 
     9 theory Intensional
    10 imports Main
    11 begin
    12 
    13 class world
    14 
    15 (** abstract syntax **)
    16 
    17 type_synonym ('w,'a) expr = "'w \<Rightarrow> 'a"   (* intention: 'w::world, 'a::type *)
    18 type_synonym 'w form = "('w, bool) expr"
    19 
    20 consts
    21   Valid    :: "('w::world) form \<Rightarrow> bool"
    22   const    :: "'a \<Rightarrow> ('w::world, 'a) expr"
    23   lift     :: "['a \<Rightarrow> 'b, ('w::world, 'a) expr] \<Rightarrow> ('w,'b) expr"
    24   lift2    :: "['a \<Rightarrow> 'b \<Rightarrow> 'c, ('w::world,'a) expr, ('w,'b) expr] \<Rightarrow> ('w,'c) expr"
    25   lift3    :: "['a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] \<Rightarrow> ('w,'d) expr"
    26 
    27   (* "Rigid" quantification (logic level) *)
    28   RAll     :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"       (binder "Rall " 10)
    29   REx      :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"       (binder "Rex " 10)
    30   REx1     :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"       (binder "Rex! " 10)
    31 
    32 (** concrete syntax **)
    33 
    34 nonterminal lift and liftargs
    35 
    36 syntax
    37   ""            :: "id \<Rightarrow> lift"                          ("_")
    38   ""            :: "longid \<Rightarrow> lift"                      ("_")
    39   ""            :: "var \<Rightarrow> lift"                         ("_")
    40   "_applC"      :: "[lift, cargs] \<Rightarrow> lift"               ("(1_/ _)" [1000, 1000] 999)
    41   ""            :: "lift \<Rightarrow> lift"                        ("'(_')")
    42   "_lambda"     :: "[idts, 'a] \<Rightarrow> lift"                  ("(3\<lambda>_./ _)" [0, 3] 3)
    43   "_constrain"  :: "[lift, type] \<Rightarrow> lift"                ("(_::_)" [4, 0] 3)
    44   ""            :: "lift \<Rightarrow> liftargs"                    ("_")
    45   "_liftargs"   :: "[lift, liftargs] \<Rightarrow> liftargs"        ("_,/ _")
    46   "_Valid"      :: "lift \<Rightarrow> bool"                        ("(\<turnstile> _)" 5)
    47   "_holdsAt"    :: "['a, lift] \<Rightarrow> bool"                  ("(_ \<Turnstile> _)" [100,10] 10)
    48 
    49   (* Syntax for lifted expressions outside the scope of \<turnstile> or |= *)
    50   "_LIFT"       :: "lift \<Rightarrow> 'a"                          ("LIFT _")
    51 
    52   (* generic syntax for lifted constants and functions *)
    53   "_const"      :: "'a \<Rightarrow> lift"                          ("(#_)" [1000] 999)
    54   "_lift"       :: "['a, lift] \<Rightarrow> lift"                  ("(_<_>)" [1000] 999)
    55   "_lift2"      :: "['a, lift, lift] \<Rightarrow> lift"            ("(_<_,/ _>)" [1000] 999)
    56   "_lift3"      :: "['a, lift, lift, lift] \<Rightarrow> lift"      ("(_<_,/ _,/ _>)" [1000] 999)
    57 
    58   (* concrete syntax for common infix functions: reuse same symbol *)
    59   "_liftEqu"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ =/ _)" [50,51] 50)
    60   "_liftNeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<noteq>/ _)" [50,51] 50)
    61   "_liftNot"    :: "lift \<Rightarrow> lift"                        ("(\<not> _)" [40] 40)
    62   "_liftAnd"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<and>/ _)" [36,35] 35)
    63   "_liftOr"     :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<or>/ _)" [31,30] 30)
    64   "_liftImp"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<longrightarrow>/ _)" [26,25] 25)
    65   "_liftIf"     :: "[lift, lift, lift] \<Rightarrow> lift"          ("(if (_)/ then (_)/ else (_))" 10)
    66   "_liftPlus"   :: "[lift, lift] \<Rightarrow> lift"                ("(_ +/ _)" [66,65] 65)
    67   "_liftMinus"  :: "[lift, lift] \<Rightarrow> lift"                ("(_ -/ _)" [66,65] 65)
    68   "_liftTimes"  :: "[lift, lift] \<Rightarrow> lift"                ("(_ */ _)" [71,70] 70)
    69   "_liftDiv"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ div _)" [71,70] 70)
    70   "_liftMod"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ mod _)" [71,70] 70)
    71   "_liftLess"   :: "[lift, lift] \<Rightarrow> lift"                ("(_/ < _)"  [50, 51] 50)
    72   "_liftLeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<le> _)" [50, 51] 50)
    73   "_liftMem"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<in> _)" [50, 51] 50)
    74   "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<notin> _)" [50, 51] 50)
    75   "_liftFinset" :: "liftargs \<Rightarrow> lift"                    ("{(_)}")
    76   (** TODO: syntax for lifted collection / comprehension **)
    77   "_liftPair"   :: "[lift,liftargs] \<Rightarrow> lift"                   ("(1'(_,/ _'))")
    78   (* infix syntax for list operations *)
    79   "_liftCons" :: "[lift, lift] \<Rightarrow> lift"                  ("(_ #/ _)" [65,66] 65)
    80   "_liftApp"  :: "[lift, lift] \<Rightarrow> lift"                  ("(_ @/ _)" [65,66] 65)
    81   "_liftList" :: "liftargs \<Rightarrow> lift"                      ("[(_)]")
    82 
    83   (* Rigid quantification (syntax level) *)
    84   "_RAll" :: "[idts, lift] \<Rightarrow> lift"                      ("(3\<forall>_./ _)" [0, 10] 10)
    85   "_REx"  :: "[idts, lift] \<Rightarrow> lift"                      ("(3\<exists>_./ _)" [0, 10] 10)
    86   "_REx1" :: "[idts, lift] \<Rightarrow> lift"                      ("(3\<exists>!_./ _)" [0, 10] 10)
    87 
    88 translations
    89   "_const"        == "CONST const"
    90   "_lift"         == "CONST lift"
    91   "_lift2"        == "CONST lift2"
    92   "_lift3"        == "CONST lift3"
    93   "_Valid"        == "CONST Valid"
    94   "_RAll x A"     == "Rall x. A"
    95   "_REx x  A"     == "Rex x. A"
    96   "_REx1 x  A"    == "Rex! x. A"
    97 
    98   "w \<Turnstile> A"        => "A w"
    99   "LIFT A"        => "A::_\<Rightarrow>_"
   100 
   101   "_liftEqu"      == "_lift2 (op =)"
   102   "_liftNeq u v"  == "_liftNot (_liftEqu u v)"
   103   "_liftNot"      == "_lift (CONST Not)"
   104   "_liftAnd"      == "_lift2 (op \<and>)"
   105   "_liftOr"       == "_lift2 (op \<or>)"
   106   "_liftImp"      == "_lift2 (op \<longrightarrow>)"
   107   "_liftIf"       == "_lift3 (CONST If)"
   108   "_liftPlus"     == "_lift2 (op +)"
   109   "_liftMinus"    == "_lift2 (op -)"
   110   "_liftTimes"    == "_lift2 (op *)"
   111   "_liftDiv"      == "_lift2 (op div)"
   112   "_liftMod"      == "_lift2 (op mod)"
   113   "_liftLess"     == "_lift2 (op <)"
   114   "_liftLeq"      == "_lift2 (op \<le>)"
   115   "_liftMem"      == "_lift2 (op \<in>)"
   116   "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
   117   "_liftFinset (_liftargs x xs)"  == "_lift2 (CONST insert) x (_liftFinset xs)"
   118   "_liftFinset x" == "_lift2 (CONST insert) x (_const {})"
   119   "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
   120   "_liftPair"     == "_lift2 (CONST Pair)"
   121   "_liftCons"     == "CONST lift2 (CONST Cons)"
   122   "_liftApp"      == "CONST lift2 (op @)"
   123   "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
   124   "_liftList x"   == "_liftCons x (_const [])"
   125 
   126 
   127 
   128   "w \<Turnstile> \<not>A"       <= "_liftNot A w"
   129   "w \<Turnstile> A \<and> B"    <= "_liftAnd A B w"
   130   "w \<Turnstile> A \<or> B"    <= "_liftOr A B w"
   131   "w \<Turnstile> A \<longrightarrow> B"  <= "_liftImp A B w"
   132   "w \<Turnstile> u = v"    <= "_liftEqu u v w"
   133   "w \<Turnstile> \<forall>x. A"   <= "_RAll x A w"
   134   "w \<Turnstile> \<exists>x. A"   <= "_REx x A w"
   135   "w \<Turnstile> \<exists>!x. A"  <= "_REx1 x A w"
   136 
   137 defs
   138   Valid_def:   "\<turnstile> A    ==  \<forall>w. w \<Turnstile> A"
   139 
   140   unl_con:     "LIFT #c w  ==  c"
   141   unl_lift:    "lift f x w == f (x w)"
   142   unl_lift2:   "LIFT f<x, y> w == f (x w) (y w)"
   143   unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
   144 
   145   unl_Rall:    "w \<Turnstile> \<forall>x. A x  ==  \<forall>x. (w \<Turnstile> A x)"
   146   unl_Rex:     "w \<Turnstile> \<exists>x. A x   ==  \<exists>x. (w \<Turnstile> A x)"
   147   unl_Rex1:    "w \<Turnstile> \<exists>!x. A x  ==  \<exists>!x. (w \<Turnstile> A x)"
   148 
   149 
   150 subsection {* Lemmas and tactics for "intensional" logics. *}
   151 
   152 lemmas intensional_rews [simp] =
   153   unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1
   154 
   155 lemma inteq_reflection: "\<turnstile> x=y  \<Longrightarrow>  (x==y)"
   156   apply (unfold Valid_def unl_lift2)
   157   apply (rule eq_reflection)
   158   apply (rule ext)
   159   apply (erule spec)
   160   done
   161 
   162 lemma intI [intro!]: "(\<And>w. w \<Turnstile> A) \<Longrightarrow> \<turnstile> A"
   163   apply (unfold Valid_def)
   164   apply (rule allI)
   165   apply (erule meta_spec)
   166   done
   167 
   168 lemma intD [dest]: "\<turnstile> A \<Longrightarrow> w \<Turnstile> A"
   169   apply (unfold Valid_def)
   170   apply (erule spec)
   171   done
   172 
   173 (** Lift usual HOL simplifications to "intensional" level. **)
   174 
   175 lemma int_simps:
   176   "\<turnstile> (x=x) = #True"
   177   "\<turnstile> (\<not>#True) = #False"  "\<turnstile> (\<not>#False) = #True"  "\<turnstile> (\<not>\<not> P) = P"
   178   "\<turnstile> ((\<not>P) = P) = #False"  "\<turnstile> (P = (\<not>P)) = #False"
   179   "\<turnstile> (P \<noteq> Q) = (P = (\<not>Q))"
   180   "\<turnstile> (#True=P) = P"  "\<turnstile> (P=#True) = P"
   181   "\<turnstile> (#True \<longrightarrow> P) = P"  "\<turnstile> (#False \<longrightarrow> P) = #True"
   182   "\<turnstile> (P \<longrightarrow> #True) = #True"  "\<turnstile> (P \<longrightarrow> P) = #True"
   183   "\<turnstile> (P \<longrightarrow> #False) = (\<not>P)"  "\<turnstile> (P \<longrightarrow> \<not>P) = (\<not>P)"
   184   "\<turnstile> (P \<and> #True) = P"  "\<turnstile> (#True \<and> P) = P"
   185   "\<turnstile> (P \<and> #False) = #False"  "\<turnstile> (#False \<and> P) = #False"
   186   "\<turnstile> (P \<and> P) = P"  "\<turnstile> (P \<and> \<not>P) = #False"  "\<turnstile> (\<not>P \<and> P) = #False"
   187   "\<turnstile> (P \<or> #True) = #True"  "\<turnstile> (#True \<or> P) = #True"
   188   "\<turnstile> (P \<or> #False) = P"  "\<turnstile> (#False \<or> P) = P"
   189   "\<turnstile> (P \<or> P) = P"  "\<turnstile> (P \<or> \<not>P) = #True"  "\<turnstile> (\<not>P \<or> P) = #True"
   190   "\<turnstile> (\<forall>x. P) = P"  "\<turnstile> (\<exists>x. P) = P"
   191   "\<turnstile> (\<not>Q \<longrightarrow> \<not>P) = (P \<longrightarrow> Q)"
   192   "\<turnstile> (P\<or>Q \<longrightarrow> R) = ((P\<longrightarrow>R)\<and>(Q\<longrightarrow>R))"
   193   apply (unfold Valid_def intensional_rews)
   194   apply blast+
   195   done
   196 
   197 declare int_simps [THEN inteq_reflection, simp]
   198 
   199 lemma TrueW [simp]: "\<turnstile> #True"
   200   by (simp add: Valid_def unl_con)
   201 
   202 
   203 
   204 (* ======== Functions to "unlift" intensional implications into HOL rules ====== *)
   205 
   206 ML {*
   207 (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
   208    \<turnstile> F = G    becomes   F w = G w
   209    \<turnstile> F \<longrightarrow> G  becomes   F w \<longrightarrow> G w
   210 *)
   211 
   212 fun int_unlift ctxt th =
   213   rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
   214 
   215 (* Turn  \<turnstile> F = G  into meta-level rewrite rule  F == G *)
   216 fun int_rewrite ctxt th =
   217   zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection}))
   218 
   219 (* flattening turns "\<longrightarrow>" into "\<Longrightarrow>" and eliminates conjunctions in the
   220    antecedent. For example,
   221 
   222          P & Q \<longrightarrow> (R | S \<longrightarrow> T)    becomes   \<lbrakk> P; Q; R | S \<rbrakk> \<Longrightarrow> T
   223 
   224    Flattening can be useful with "intensional" lemmas (after unlifting).
   225    Naive resolution with mp and conjI may run away because of higher-order
   226    unification, therefore the code is a little awkward.
   227 *)
   228 fun flatten t =
   229   let
   230     (* analogous to RS, but using matching instead of resolution *)
   231     fun matchres tha i thb =
   232       case Seq.chop 2 (Thm.biresolution NONE true [(false,tha)] i thb) of
   233           ([th],_) => th
   234         | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
   235         |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
   236 
   237     (* match tha with some premise of thb *)
   238     fun matchsome tha thb =
   239       let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
   240             | hmatch n = matchres tha n thb handle THM _ => hmatch (n-1)
   241       in hmatch (Thm.nprems_of thb) end
   242 
   243     fun hflatten t =
   244       case Thm.concl_of t of
   245         Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)
   246       | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
   247   in
   248     hflatten t
   249   end
   250 
   251 fun int_use ctxt th =
   252     case Thm.concl_of th of
   253       Const _ $ (Const (@{const_name Valid}, _) $ _) =>
   254               (flatten (int_unlift ctxt th) handle THM _ => th)
   255     | _ => th
   256 *}
   257 
   258 attribute_setup int_unlift =
   259   {* Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of)) *}
   260 attribute_setup int_rewrite =
   261   {* Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of)) *}
   262 attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
   263 attribute_setup int_use =
   264   {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}
   265 
   266 lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)"
   267   by (simp add: Valid_def)
   268 
   269 lemma Not_Rex: "\<turnstile> (\<not> (\<exists>x. F x)) = (\<forall>x. \<not> F x)"
   270   by (simp add: Valid_def)
   271 
   272 end