summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Sequents/LK0.ML

changeset 17481 | 75166ebb619b |

parent 9259 | 103acc345f75 |

--- a/src/Sequents/LK0.ML Sun Sep 18 14:25:48 2005 +0200 +++ b/src/Sequents/LK0.ML Sun Sep 18 15:20:08 2005 +0200 @@ -1,9 +1,9 @@ -(* Title: LK/LK0 +(* Title: LK/LK0.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -Tactics and lemmas for LK (thanks also to Philippe de Groote) +Tactics and lemmas for LK (thanks also to Philippe de Groote) Structural rules by Soren Heilmann *) @@ -41,21 +41,21 @@ qed "exchL"; (*Cut and thin, replacing the right-side formula*) -fun cutR_tac (sP: string) i = +fun cutR_tac (sP: string) i = res_inst_tac [ ("P",sP) ] cut i THEN rtac thinR i; (*Cut and thin, replacing the left-side formula*) -fun cutL_tac (sP: string) i = +fun cutL_tac (sP: string) i = res_inst_tac [ ("P",sP) ] cut i THEN rtac thinL (i+1); (** If-and-only-if rules **) -Goalw [iff_def] +Goalw [iff_def] "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"; by (REPEAT (ares_tac [conjR,impR] 1)); qed "iffR"; -Goalw [iff_def] +Goalw [iff_def] "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"; by (REPEAT (ares_tac [conjL,impL,basic] 1)); qed "iffL"; @@ -93,31 +93,31 @@ (*The rules of LK*) -val prop_pack = empty_pack add_safes - [basic, refl, TrueR, FalseL, - conjL, conjR, disjL, disjR, impL, impR, +val prop_pack = empty_pack add_safes + [basic, refl, TrueR, FalseL, + conjL, conjR, disjL, disjR, impL, impR, notL, notR, iffL, iffR]; -val LK_pack = prop_pack add_safes [allR, exL] +val LK_pack = prop_pack add_safes [allR, exL] add_unsafes [allL_thin, exR_thin, the_equality]; -val LK_dup_pack = prop_pack add_safes [allR, exL] +val LK_dup_pack = prop_pack add_safes [allR, exL] add_unsafes [allL, exR, the_equality]; pack_ref() := LK_pack; -fun lemma_tac th i = +fun lemma_tac th i = rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i; -val [major,minor] = goal thy +val [major,minor] = goal (the_context ()) "[| $H |- $E, $F, P --> Q; $H |- $E, $F, P |] ==> $H |- $E, Q, $F"; by (rtac (thinRS RS cut) 1 THEN rtac major 1); by (Step_tac 1); by (rtac thinR 1 THEN rtac minor 1); qed "mp_R"; -val [major,minor] = goal thy +val [major,minor] = goal (the_context ()) "[| $H, $G |- $E, P --> Q; $H, $G, Q |- $E |] ==> $H, P, $G |- $E"; by (rtac (thinL RS cut) 1 THEN rtac major 1); by (Step_tac 1); @@ -127,14 +127,14 @@ (** Two rules to generate left- and right- rules from implications **) -val [major,minor] = goal thy +val [major,minor] = goal (the_context ()) "[| |- P --> Q; $H |- $E, $F, P |] ==> $H |- $E, Q, $F"; by (rtac mp_R 1); by (rtac minor 2); by (rtac thinRS 1 THEN rtac (major RS thinLS) 1); qed "R_of_imp"; -val [major,minor] = goal thy +val [major,minor] = goal (the_context ()) "[| |- P --> Q; $H, $G, Q |- $E |] ==> $H, P, $G |- $E"; by (rtac mp_L 1); by (rtac minor 2); @@ -142,7 +142,7 @@ qed "L_of_imp"; (*Can be used to create implications in a subgoal*) -val [prem] = goal thy +val [prem] = goal (the_context ()) "[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F"; by (rtac mp_L 1); by (rtac basic 2); @@ -151,17 +151,17 @@ Goal "|-P&Q ==> |-P"; by (etac (thinR RS cut) 1); -by (Fast_tac 1); +by (Fast_tac 1); qed "conjunct1"; Goal "|-P&Q ==> |-Q"; by (etac (thinR RS cut) 1); -by (Fast_tac 1); +by (Fast_tac 1); qed "conjunct2"; Goal "|- (ALL x. P(x)) ==> |- P(x)"; by (etac (thinR RS cut) 1); -by (Fast_tac 1); +by (Fast_tac 1); qed "spec"; (** Equality **) @@ -189,12 +189,12 @@ (* Two theorms for rewriting only one instance of a definition: the first for definitions of formulae and the second for terms *) -val prems = goal thy "(A == B) ==> |- A <-> B"; +val prems = goal (the_context ()) "(A == B) ==> |- A <-> B"; by (rewrite_goals_tac prems); by (rtac iff_refl 1); qed "def_imp_iff"; -val prems = goal thy "(A == B) ==> |- A = B"; +val prems = goal (the_context ()) "(A == B) ==> |- A = B"; by (rewrite_goals_tac prems); by (rtac refl 1); qed "meta_eq_to_obj_eq";