# File LK0.ML

    (*  Title:      LK/LK0.ML
        ID:         $Id: LK0.ML,v 1.4 2005/09/18 13:20:08 wenzelm Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1992  University of Cambridge

    Tactics and lemmas for LK (thanks also to Philippe de Groote)

    Structural rules by Soren Heilmann
    *)

    (** Structural Rules on formulas **)

    (*contraction*)

    Goal "$H |- $E, P, P, $F ==> $H |- $E, P, $F";
    by (etac contRS 1);
    qed "contR";

    Goal "$H, P, P, $G |- $E ==> $H, P, $G |- $E";
    by (etac contLS 1);
    qed "contL";

    (*thinning*)

    Goal "$H |- $E, $F ==> $H |- $E, P, $F";
    by (etac thinRS 1);
    qed "thinR";

    Goal "$H, $G |- $E ==> $H, P, $G |- $E";
    by (etac thinLS 1);
    qed "thinL";

    (*exchange*)

    Goal "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F";
    by (etac exchRS 1);
    qed "exchR";

    Goal "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E";
    by (etac exchLS 1);
    qed "exchL";

    (*Cut and thin, replacing the right-side formula*)
    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 =
        res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);

    (** If-and-only-if rules **)
    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]
        "[| $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";

    Goal "$H |- $E, (P <-> P), $F";
    by (REPEAT (resolve_tac [iffR,basic] 1));
    qed "iff_refl";

    Goalw [True_def] "$H |- $E, True, $F";
    by (rtac impR 1);
    by (rtac basic 1);
    qed "TrueR";

    (*Descriptions*)
    val [p1,p2] = Goal
        "[| $H |- $E, P(a), $F;  !!x. $H, P(x) |- $E, x=a, $F |] \
    \    ==> $H |- $E, (THE x. P(x)) = a, $F";
    by (rtac cut 1);
    by (rtac p2 2);
    by (rtac The 1 THEN rtac thinR 1 THEN rtac exchRS 1 THEN rtac p1 1);
    by (rtac thinR 1 THEN rtac exchRS 1 THEN rtac p2 1);
    qed "the_equality";

    (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)

    Goal "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E";
    by (rtac allL 1);
    by (etac thinL 1);
    qed "allL_thin";

    Goal "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F";
    by (rtac exR 1);
    by (etac thinR 1);
    qed "exR_thin";

    (*The rules of LK*)
    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]
                            add_unsafes [allL_thin, exR_thin, the_equality];

    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 =
        rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;

    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 (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);
    by (rtac thinL 1 THEN rtac minor 1);
    qed "mp_L";

    (** Two rules to generate left- and right- rules from implications **)

    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 (the_context ())
        "[| |- P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
    by (rtac mp_L 1);
    by (rtac minor 2);
    by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
    qed "L_of_imp";

    (*Can be used to create implications in a subgoal*)
    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);
    by (rtac thinR 1 THEN rtac prem 1);
    qed "backwards_impR";

    Goal "|-P&Q ==> |-P";
    by (etac (thinR RS cut) 1);
    by (Fast_tac 1);
    qed "conjunct1";

    Goal "|-P&Q ==> |-Q";
    by (etac (thinR RS cut) 1);
    by (Fast_tac 1);
    qed "conjunct2";

    Goal "|- (ALL x. P(x)) ==> |- P(x)";
    by (etac (thinR RS cut) 1);
    by (Fast_tac 1);
    qed "spec";

    (** Equality **)

    Goal "|- a=b --> b=a";
    by (safe_tac (LK_pack add_safes [subst]) 1);
    qed "sym";

    Goal "|- a=b --> b=c --> a=c";
    by (safe_tac (LK_pack add_safes [subst]) 1);
    qed "trans";

    (* Symmetry of equality in hypotheses *)
    bind_thm ("symL", sym RS L_of_imp);

    (* Symmetry of equality in hypotheses *)
    bind_thm ("symR", sym RS R_of_imp);

    Goal "[| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F";
    by (rtac (trans RS R_of_imp RS mp_R) 1);
    by (ALLGOALS assume_tac);
    qed "transR";

    (* Two theorms for rewriting only one instance of a definition:
       the first for definitions of formulae and the second for terms *)

    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 (the_context ()) "(A == B) ==> |- A = B";
    by (rewrite_goals_tac prems);
    by (rtac refl 1);
    qed "meta_eq_to_obj_eq";