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