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