src/Sequents/LK0.thy
author paulson <lp15@cam.ac.uk>
Mon Jun 11 14:34:17 2018 +0100 (14 months ago)
changeset 68424 02e5a44ffe7d
parent 61386 0a29a984a91b
child 69593 3dda49e08b9d
permissions -rw-r--r--
the last of the infinite product proofs
     1 (*  Title:      Sequents/LK0.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 There may be printing problems if a seqent is in expanded normal form
     6 (eta-expanded, beta-contracted).
     7 *)
     8 
     9 section \<open>Classical First-Order Sequent Calculus\<close>
    10 
    11 theory LK0
    12 imports Sequents
    13 begin
    14 
    15 class "term"
    16 default_sort "term"
    17 
    18 consts
    19 
    20   Trueprop       :: "two_seqi"
    21 
    22   True         :: o
    23   False        :: o
    24   equal        :: "['a,'a] \<Rightarrow> o"     (infixl "=" 50)
    25   Not          :: "o \<Rightarrow> o"           ("\<not> _" [40] 40)
    26   conj         :: "[o,o] \<Rightarrow> o"       (infixr "\<and>" 35)
    27   disj         :: "[o,o] \<Rightarrow> o"       (infixr "\<or>" 30)
    28   imp          :: "[o,o] \<Rightarrow> o"       (infixr "\<longrightarrow>" 25)
    29   iff          :: "[o,o] \<Rightarrow> o"       (infixr "\<longleftrightarrow>" 25)
    30   The          :: "('a \<Rightarrow> o) \<Rightarrow> 'a"  (binder "THE " 10)
    31   All          :: "('a \<Rightarrow> o) \<Rightarrow> o"   (binder "\<forall>" 10)
    32   Ex           :: "('a \<Rightarrow> o) \<Rightarrow> o"   (binder "\<exists>" 10)
    33 
    34 syntax
    35  "_Trueprop"    :: "two_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5)
    36 
    37 parse_translation \<open>[(@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))]\<close>
    38 print_translation \<open>[(@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))]\<close>
    39 
    40 abbreviation
    41   not_equal  (infixl "\<noteq>" 50) where
    42   "x \<noteq> y \<equiv> \<not> (x = y)"
    43 
    44 axiomatization where
    45 
    46   (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
    47 
    48   contRS: "$H \<turnstile> $E, $S, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and
    49   contLS: "$H, $S, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $E" and
    50 
    51   thinRS: "$H \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and
    52   thinLS: "$H, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $E" and
    53 
    54   exchRS: "$H \<turnstile> $E, $R, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $R, $F" and
    55   exchLS: "$H, $R, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $R, $G \<turnstile> $E" and
    56 
    57   cut:   "\<lbrakk>$H \<turnstile> $E, P;  $H, P \<turnstile> $E\<rbrakk> \<Longrightarrow> $H \<turnstile> $E" and
    58 
    59   (*Propositional rules*)
    60 
    61   basic: "$H, P, $G \<turnstile> $E, P, $F" and
    62 
    63   conjR: "\<lbrakk>$H\<turnstile> $E, P, $F;  $H\<turnstile> $E, Q, $F\<rbrakk> \<Longrightarrow> $H\<turnstile> $E, P \<and> Q, $F" and
    64   conjL: "$H, P, Q, $G \<turnstile> $E \<Longrightarrow> $H, P \<and> Q, $G \<turnstile> $E" and
    65 
    66   disjR: "$H \<turnstile> $E, P, Q, $F \<Longrightarrow> $H \<turnstile> $E, P \<or> Q, $F" and
    67   disjL: "\<lbrakk>$H, P, $G \<turnstile> $E;  $H, Q, $G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<or> Q, $G \<turnstile> $E" and
    68 
    69   impR:  "$H, P \<turnstile> $E, Q, $F \<Longrightarrow> $H \<turnstile> $E, P \<longrightarrow> Q, $F" and
    70   impL:  "\<lbrakk>$H,$G \<turnstile> $E,P;  $H, Q, $G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<longrightarrow> Q, $G \<turnstile> $E" and
    71 
    72   notR:  "$H, P \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, \<not> P, $F" and
    73   notL:  "$H, $G \<turnstile> $E, P \<Longrightarrow> $H, \<not> P, $G \<turnstile> $E" and
    74 
    75   FalseL: "$H, False, $G \<turnstile> $E" and
    76 
    77   True_def: "True \<equiv> False \<longrightarrow> False" and
    78   iff_def:  "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)"
    79 
    80 axiomatization where
    81   (*Quantifiers*)
    82 
    83   allR:  "(\<And>x. $H \<turnstile> $E, P(x), $F) \<Longrightarrow> $H \<turnstile> $E, \<forall>x. P(x), $F" and
    84   allL:  "$H, P(x), $G, \<forall>x. P(x) \<turnstile> $E \<Longrightarrow> $H, \<forall>x. P(x), $G \<turnstile> $E" and
    85 
    86   exR:   "$H \<turnstile> $E, P(x), $F, \<exists>x. P(x) \<Longrightarrow> $H \<turnstile> $E, \<exists>x. P(x), $F" and
    87   exL:   "(\<And>x. $H, P(x), $G \<turnstile> $E) \<Longrightarrow> $H, \<exists>x. P(x), $G \<turnstile> $E" and
    88 
    89   (*Equality*)
    90   refl:  "$H \<turnstile> $E, a = a, $F" and
    91   subst: "\<And>G H E. $H(a), $G(a) \<turnstile> $E(a) \<Longrightarrow> $H(b), a=b, $G(b) \<turnstile> $E(b)"
    92 
    93   (* Reflection *)
    94 
    95 axiomatization where
    96   eq_reflection:  "\<turnstile> x = y \<Longrightarrow> (x \<equiv> y)" and
    97   iff_reflection: "\<turnstile> P \<longleftrightarrow> Q \<Longrightarrow> (P \<equiv> Q)"
    98 
    99   (*Descriptions*)
   100 
   101 axiomatization where
   102   The: "\<lbrakk>$H \<turnstile> $E, P(a), $F;  \<And>x.$H, P(x) \<turnstile> $E, x=a, $F\<rbrakk> \<Longrightarrow>
   103          $H \<turnstile> $E, P(THE x. P(x)), $F"
   104 
   105 definition If :: "[o, 'a, 'a] \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" 10)
   106   where "If(P,x,y) \<equiv> THE z::'a. (P \<longrightarrow> z = x) \<and> (\<not> P \<longrightarrow> z = y)"
   107 
   108 
   109 (** Structural Rules on formulas **)
   110 
   111 (*contraction*)
   112 
   113 lemma contR: "$H \<turnstile> $E, P, P, $F \<Longrightarrow> $H \<turnstile> $E, P, $F"
   114   by (rule contRS)
   115 
   116 lemma contL: "$H, P, P, $G \<turnstile> $E \<Longrightarrow> $H, P, $G \<turnstile> $E"
   117   by (rule contLS)
   118 
   119 (*thinning*)
   120 
   121 lemma thinR: "$H \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, P, $F"
   122   by (rule thinRS)
   123 
   124 lemma thinL: "$H, $G \<turnstile> $E \<Longrightarrow> $H, P, $G \<turnstile> $E"
   125   by (rule thinLS)
   126 
   127 (*exchange*)
   128 
   129 lemma exchR: "$H \<turnstile> $E, Q, P, $F \<Longrightarrow> $H \<turnstile> $E, P, Q, $F"
   130   by (rule exchRS)
   131 
   132 lemma exchL: "$H, Q, P, $G \<turnstile> $E \<Longrightarrow> $H, P, Q, $G \<turnstile> $E"
   133   by (rule exchLS)
   134 
   135 ML \<open>
   136 (*Cut and thin, replacing the right-side formula*)
   137 fun cutR_tac ctxt s i =
   138   Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN
   139   resolve_tac ctxt @{thms thinR} i
   140 
   141 (*Cut and thin, replacing the left-side formula*)
   142 fun cutL_tac ctxt s i =
   143   Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN
   144   resolve_tac ctxt @{thms thinL} (i + 1)
   145 \<close>
   146 
   147 
   148 (** If-and-only-if rules **)
   149 lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F;  $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F"
   150   apply (unfold iff_def)
   151   apply (assumption | rule conjR impR)+
   152   done
   153 
   154 lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q;  $H,Q,P,$G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $E"
   155   apply (unfold iff_def)
   156   apply (assumption | rule conjL impL basic)+
   157   done
   158 
   159 lemma iff_refl: "$H \<turnstile> $E, (P \<longleftrightarrow> P), $F"
   160   apply (rule iffR basic)+
   161   done
   162 
   163 lemma TrueR: "$H \<turnstile> $E, True, $F"
   164   apply (unfold True_def)
   165   apply (rule impR)
   166   apply (rule basic)
   167   done
   168 
   169 (*Descriptions*)
   170 lemma the_equality:
   171   assumes p1: "$H \<turnstile> $E, P(a), $F"
   172     and p2: "\<And>x. $H, P(x) \<turnstile> $E, x=a, $F"
   173   shows "$H \<turnstile> $E, (THE x. P(x)) = a, $F"
   174   apply (rule cut)
   175    apply (rule_tac [2] p2)
   176   apply (rule The, rule thinR, rule exchRS, rule p1)
   177   apply (rule thinR, rule exchRS, rule p2)
   178   done
   179 
   180 
   181 (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
   182 
   183 lemma allL_thin: "$H, P(x), $G \<turnstile> $E \<Longrightarrow> $H, \<forall>x. P(x), $G \<turnstile> $E"
   184   apply (rule allL)
   185   apply (erule thinL)
   186   done
   187 
   188 lemma exR_thin: "$H \<turnstile> $E, P(x), $F \<Longrightarrow> $H \<turnstile> $E, \<exists>x. P(x), $F"
   189   apply (rule exR)
   190   apply (erule thinR)
   191   done
   192 
   193 (*The rules of LK*)
   194 
   195 lemmas [safe] =
   196   iffR iffL
   197   notR notL
   198   impR impL
   199   disjR disjL
   200   conjR conjL
   201   FalseL TrueR
   202   refl basic
   203 ML \<open>val prop_pack = Cla.get_pack @{context}\<close>
   204 
   205 lemmas [safe] = exL allR
   206 lemmas [unsafe] = the_equality exR_thin allL_thin
   207 ML \<open>val LK_pack = Cla.get_pack @{context}\<close>
   208 
   209 ML \<open>
   210   val LK_dup_pack =
   211     Cla.put_pack prop_pack @{context}
   212     |> fold_rev Cla.add_safe @{thms allR exL}
   213     |> fold_rev Cla.add_unsafe @{thms allL exR the_equality}
   214     |> Cla.get_pack;
   215 \<close>
   216 
   217 method_setup fast_prop =
   218   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack prop_pack ctxt)))\<close>
   219 
   220 method_setup fast_dup =
   221   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack LK_dup_pack ctxt)))\<close>
   222 
   223 method_setup best_dup =
   224   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack LK_dup_pack ctxt)))\<close>
   225 
   226 method_setup lem = \<open>
   227   Attrib.thm >> (fn th => fn ctxt =>
   228     SIMPLE_METHOD' (fn i =>
   229       resolve_tac ctxt [@{thm thinR} RS @{thm cut}] i THEN
   230       REPEAT (resolve_tac ctxt @{thms thinL} i) THEN
   231       resolve_tac ctxt [th] i))
   232 \<close>
   233 
   234 
   235 lemma mp_R:
   236   assumes major: "$H \<turnstile> $E, $F, P \<longrightarrow> Q"
   237     and minor: "$H \<turnstile> $E, $F, P"
   238   shows "$H \<turnstile> $E, Q, $F"
   239   apply (rule thinRS [THEN cut], rule major)
   240   apply step
   241   apply (rule thinR, rule minor)
   242   done
   243 
   244 lemma mp_L:
   245   assumes major: "$H, $G \<turnstile> $E, P \<longrightarrow> Q"
   246     and minor: "$H, $G, Q \<turnstile> $E"
   247   shows "$H, P, $G \<turnstile> $E"
   248   apply (rule thinL [THEN cut], rule major)
   249   apply step
   250   apply (rule thinL, rule minor)
   251   done
   252 
   253 
   254 (** Two rules to generate left- and right- rules from implications **)
   255 
   256 lemma R_of_imp:
   257   assumes major: "\<turnstile> P \<longrightarrow> Q"
   258     and minor: "$H \<turnstile> $E, $F, P"
   259   shows "$H \<turnstile> $E, Q, $F"
   260   apply (rule mp_R)
   261    apply (rule_tac [2] minor)
   262   apply (rule thinRS, rule major [THEN thinLS])
   263   done
   264 
   265 lemma L_of_imp:
   266   assumes major: "\<turnstile> P \<longrightarrow> Q"
   267     and minor: "$H, $G, Q \<turnstile> $E"
   268   shows "$H, P, $G \<turnstile> $E"
   269   apply (rule mp_L)
   270    apply (rule_tac [2] minor)
   271   apply (rule thinRS, rule major [THEN thinLS])
   272   done
   273 
   274 (*Can be used to create implications in a subgoal*)
   275 lemma backwards_impR:
   276   assumes prem: "$H, $G \<turnstile> $E, $F, P \<longrightarrow> Q"
   277   shows "$H, P, $G \<turnstile> $E, Q, $F"
   278   apply (rule mp_L)
   279    apply (rule_tac [2] basic)
   280   apply (rule thinR, rule prem)
   281   done
   282 
   283 lemma conjunct1: "\<turnstile>P \<and> Q \<Longrightarrow> \<turnstile>P"
   284   apply (erule thinR [THEN cut])
   285   apply fast
   286   done
   287 
   288 lemma conjunct2: "\<turnstile>P \<and> Q \<Longrightarrow> \<turnstile>Q"
   289   apply (erule thinR [THEN cut])
   290   apply fast
   291   done
   292 
   293 lemma spec: "\<turnstile> (\<forall>x. P(x)) \<Longrightarrow> \<turnstile> P(x)"
   294   apply (erule thinR [THEN cut])
   295   apply fast
   296   done
   297 
   298 
   299 (** Equality **)
   300 
   301 lemma sym: "\<turnstile> a = b \<longrightarrow> b = a"
   302   by (safe add!: subst)
   303 
   304 lemma trans: "\<turnstile> a = b \<longrightarrow> b = c \<longrightarrow> a = c"
   305   by (safe add!: subst)
   306 
   307 (* Symmetry of equality in hypotheses *)
   308 lemmas symL = sym [THEN L_of_imp]
   309 
   310 (* Symmetry of equality in hypotheses *)
   311 lemmas symR = sym [THEN R_of_imp]
   312 
   313 lemma transR: "\<lbrakk>$H\<turnstile> $E, $F, a = b;  $H\<turnstile> $E, $F, b=c\<rbrakk> \<Longrightarrow> $H\<turnstile> $E, a = c, $F"
   314   by (rule trans [THEN R_of_imp, THEN mp_R])
   315 
   316 (* Two theorms for rewriting only one instance of a definition:
   317    the first for definitions of formulae and the second for terms *)
   318 
   319 lemma def_imp_iff: "(A \<equiv> B) \<Longrightarrow> \<turnstile> A \<longleftrightarrow> B"
   320   apply unfold
   321   apply (rule iff_refl)
   322   done
   323 
   324 lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> \<turnstile> A = B"
   325   apply unfold
   326   apply (rule refl)
   327   done
   328 
   329 
   330 (** if-then-else rules **)
   331 
   332 lemma if_True: "\<turnstile> (if True then x else y) = x"
   333   unfolding If_def by fast
   334 
   335 lemma if_False: "\<turnstile> (if False then x else y) = y"
   336   unfolding If_def by fast
   337 
   338 lemma if_P: "\<turnstile> P \<Longrightarrow> \<turnstile> (if P then x else y) = x"
   339   apply (unfold If_def)
   340   apply (erule thinR [THEN cut])
   341   apply fast
   342   done
   343 
   344 lemma if_not_P: "\<turnstile> \<not> P \<Longrightarrow> \<turnstile> (if P then x else y) = y"
   345   apply (unfold If_def)
   346   apply (erule thinR [THEN cut])
   347   apply fast
   348   done
   349 
   350 end