src/Sequents/LK0.thy
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 21588 cd0dc678a205
child 22894 619b270607ac
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
     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   "="          :: "['a,'a] => o"     (infixl 50)
    28   Not          :: "o => o"           ("~ _" [40] 40)
    29   "&"          :: "[o,o] => o"       (infixr 35)
    30   "|"          :: "[o,o] => o"       (infixr 30)
    31   "-->"        :: "[o,o] => o"       (infixr 25)
    32   "<->"        :: "[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   "_not_equal" :: "['a, 'a] => o"              (infixl "~=" 50)
    40 
    41 parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
    42 print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
    43 
    44 translations
    45   "x ~= y"      == "~ (x = y)"
    46 
    47 syntax (xsymbols)
    48   Not           :: "o => o"               ("\<not> _" [40] 40)
    49   "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
    50   "op |"        :: "[o, o] => o"          (infixr "\<or>" 30)
    51   "op -->"      :: "[o, o] => o"          (infixr "\<longrightarrow>" 25)
    52   "op <->"      :: "[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   "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
    60   "op |"        :: "[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 local
   159   val thinR = thm "thinR"
   160   val thinL = thm "thinL"
   161   val cut = thm "cut"
   162 in
   163 
   164 (*Cut and thin, replacing the right-side formula*)
   165 fun cutR_tac s i =
   166   res_inst_tac [ ("P", s) ] cut i  THEN  rtac thinR i
   167 
   168 (*Cut and thin, replacing the left-side formula*)
   169 fun cutL_tac s i =
   170   res_inst_tac [("P", s)] cut i  THEN  rtac thinL (i+1)
   171 
   172 end
   173 *}
   174 
   175 
   176 (** If-and-only-if rules **)
   177 lemma iffR: 
   178     "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
   179   apply (unfold iff_def)
   180   apply (assumption | rule conjR impR)+
   181   done
   182 
   183 lemma iffL: 
   184     "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
   185   apply (unfold iff_def)
   186   apply (assumption | rule conjL impL basic)+
   187   done
   188 
   189 lemma iff_refl: "$H |- $E, (P <-> P), $F"
   190   apply (rule iffR basic)+
   191   done
   192 
   193 lemma TrueR: "$H |- $E, True, $F"
   194   apply (unfold True_def)
   195   apply (rule impR)
   196   apply (rule basic)
   197   done
   198 
   199 (*Descriptions*)
   200 lemma the_equality:
   201   assumes p1: "$H |- $E, P(a), $F"
   202     and p2: "!!x. $H, P(x) |- $E, x=a, $F"
   203   shows "$H |- $E, (THE x. P(x)) = a, $F"
   204   apply (rule cut)
   205    apply (rule_tac [2] p2)
   206   apply (rule The, rule thinR, rule exchRS, rule p1)
   207   apply (rule thinR, rule exchRS, rule p2)
   208   done
   209 
   210 
   211 (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
   212 
   213 lemma allL_thin: "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"
   214   apply (rule allL)
   215   apply (erule thinL)
   216   done
   217 
   218 lemma exR_thin: "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F"
   219   apply (rule exR)
   220   apply (erule thinR)
   221   done
   222 
   223 (*The rules of LK*)
   224 
   225 ML {*
   226 val prop_pack = empty_pack add_safes
   227                 [thm "basic", thm "refl", thm "TrueR", thm "FalseL",
   228                  thm "conjL", thm "conjR", thm "disjL", thm "disjR", thm "impL", thm "impR",
   229                  thm "notL", thm "notR", thm "iffL", thm "iffR"];
   230 
   231 val LK_pack = prop_pack add_safes   [thm "allR", thm "exL"]
   232                         add_unsafes [thm "allL_thin", thm "exR_thin", thm "the_equality"];
   233 
   234 val LK_dup_pack = prop_pack add_safes   [thm "allR", thm "exL"]
   235                             add_unsafes [thm "allL", thm "exR", thm "the_equality"];
   236 
   237 
   238 local
   239   val thinR = thm "thinR"
   240   val thinL = thm "thinL"
   241   val cut = thm "cut"
   242 in
   243 
   244 fun lemma_tac th i =
   245     rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
   246 
   247 end;
   248 *}
   249 
   250 method_setup fast_prop =
   251   {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac prop_pack)) *}
   252   "propositional reasoning"
   253 
   254 method_setup fast =
   255   {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_pack)) *}
   256   "classical reasoning"
   257 
   258 method_setup fast_dup =
   259   {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
   260   "classical reasoning"
   261 
   262 method_setup best =
   263   {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_pack)) *}
   264   "classical reasoning"
   265 
   266 method_setup best_dup =
   267   {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
   268   "classical reasoning"
   269 
   270 
   271 lemma mp_R:
   272   assumes major: "$H |- $E, $F, P --> Q"
   273     and minor: "$H |- $E, $F, P"
   274   shows "$H |- $E, Q, $F"
   275   apply (rule thinRS [THEN cut], rule major)
   276   apply (tactic "step_tac LK_pack 1")
   277   apply (rule thinR, rule minor)
   278   done
   279 
   280 lemma mp_L:
   281   assumes major: "$H, $G |- $E, P --> Q"
   282     and minor: "$H, $G, Q |- $E"
   283   shows "$H, P, $G |- $E"
   284   apply (rule thinL [THEN cut], rule major)
   285   apply (tactic "step_tac LK_pack 1")
   286   apply (rule thinL, rule minor)
   287   done
   288 
   289 
   290 (** Two rules to generate left- and right- rules from implications **)
   291 
   292 lemma R_of_imp:
   293   assumes major: "|- P --> Q"
   294     and minor: "$H |- $E, $F, P"
   295   shows "$H |- $E, Q, $F"
   296   apply (rule mp_R)
   297    apply (rule_tac [2] minor)
   298   apply (rule thinRS, rule major [THEN thinLS])
   299   done
   300 
   301 lemma L_of_imp:
   302   assumes major: "|- P --> Q"
   303     and minor: "$H, $G, Q |- $E"
   304   shows "$H, P, $G |- $E"
   305   apply (rule mp_L)
   306    apply (rule_tac [2] minor)
   307   apply (rule thinRS, rule major [THEN thinLS])
   308   done
   309 
   310 (*Can be used to create implications in a subgoal*)
   311 lemma backwards_impR:
   312   assumes prem: "$H, $G |- $E, $F, P --> Q"
   313   shows "$H, P, $G |- $E, Q, $F"
   314   apply (rule mp_L)
   315    apply (rule_tac [2] basic)
   316   apply (rule thinR, rule prem)
   317   done
   318 
   319 lemma conjunct1: "|-P&Q ==> |-P"
   320   apply (erule thinR [THEN cut])
   321   apply fast
   322   done
   323 
   324 lemma conjunct2: "|-P&Q ==> |-Q"
   325   apply (erule thinR [THEN cut])
   326   apply fast
   327   done
   328 
   329 lemma spec: "|- (ALL x. P(x)) ==> |- P(x)"
   330   apply (erule thinR [THEN cut])
   331   apply fast
   332   done
   333 
   334 
   335 (** Equality **)
   336 
   337 lemma sym: "|- a=b --> b=a"
   338   by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *})
   339 
   340 lemma trans: "|- a=b --> b=c --> a=c"
   341   by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *})
   342 
   343 (* Symmetry of equality in hypotheses *)
   344 lemmas symL = sym [THEN L_of_imp, standard]
   345 
   346 (* Symmetry of equality in hypotheses *)
   347 lemmas symR = sym [THEN R_of_imp, standard]
   348 
   349 lemma transR: "[| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F"
   350   by (rule trans [THEN R_of_imp, THEN mp_R])
   351 
   352 (* Two theorms for rewriting only one instance of a definition:
   353    the first for definitions of formulae and the second for terms *)
   354 
   355 lemma def_imp_iff: "(A == B) ==> |- A <-> B"
   356   apply unfold
   357   apply (rule iff_refl)
   358   done
   359 
   360 lemma meta_eq_to_obj_eq: "(A == B) ==> |- A = B"
   361   apply unfold
   362   apply (rule refl)
   363   done
   364 
   365 
   366 (** if-then-else rules **)
   367 
   368 lemma if_True: "|- (if True then x else y) = x"
   369   unfolding If_def by fast
   370 
   371 lemma if_False: "|- (if False then x else y) = y"
   372   unfolding If_def by fast
   373 
   374 lemma if_P: "|- P ==> |- (if P then x else y) = x"
   375   apply (unfold If_def)
   376   apply (erule thinR [THEN cut])
   377   apply fast
   378   done
   379 
   380 lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y";
   381   apply (unfold If_def)
   382   apply (erule thinR [THEN cut])
   383   apply fast
   384   done
   385 
   386 end