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