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