src/Sequents/LK0.ML
changeset 7122 87b233b31889
parent 7093 b2ee0e5d1a7f
child 9259 103acc345f75
     1.1 --- a/src/Sequents/LK0.ML	Wed Jul 28 13:52:59 1999 +0200
     1.2 +++ b/src/Sequents/LK0.ML	Wed Jul 28 13:55:02 1999 +0200
     1.3 @@ -50,18 +50,34 @@
     1.4  
     1.5  
     1.6  (** If-and-only-if rules **)
     1.7 -qed_goalw "iffR" thy [iff_def]
     1.8 -    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
     1.9 - (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
    1.10 +Goalw [iff_def] 
    1.11 +    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F";
    1.12 +by (REPEAT (ares_tac [conjR,impR] 1));
    1.13 +qed "iffR";
    1.14 +
    1.15 +Goalw [iff_def] 
    1.16 +    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E";
    1.17 +by (REPEAT (ares_tac [conjL,impL,basic] 1));
    1.18 +qed "iffL";
    1.19 +
    1.20 +Goal "$H |- $E, (P <-> P), $F";
    1.21 +by (REPEAT (resolve_tac [iffR,basic] 1));
    1.22 +qed "iff_refl";
    1.23  
    1.24 -qed_goalw "iffL" thy [iff_def]
    1.25 -   "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    1.26 - (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
    1.27 +Goalw [True_def] "$H |- $E, True, $F";
    1.28 +by (rtac impR 1);
    1.29 +by (rtac basic 1);
    1.30 +qed "TrueR";
    1.31  
    1.32 -qed_goalw "TrueR" thy [True_def]
    1.33 -    "$H |- $E, True, $F"
    1.34 - (fn _=> [ rtac impR 1, rtac basic 1 ]);
    1.35 -
    1.36 +(*Descriptions*)
    1.37 +val [p1,p2] = Goal
    1.38 +    "[| $H |- $E, P(a), $F;  !!x. $H, P(x) |- $E, x=a, $F |] \
    1.39 +\    ==> $H |- $E, (THE x. P(x)) = a, $F";
    1.40 +by (rtac cut 1);
    1.41 +by (rtac p2 2);
    1.42 +by (rtac The 1 THEN rtac thinR 1 THEN rtac exchRS 1 THEN rtac p1 1);
    1.43 +by (rtac thinR 1 THEN rtac exchRS 1 THEN rtac p2 1);
    1.44 +qed "the_equality";
    1.45  
    1.46  (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
    1.47  
    1.48 @@ -83,17 +99,13 @@
    1.49                   notL, notR, iffL, iffR];
    1.50  
    1.51  val LK_pack = prop_pack add_safes   [allR, exL] 
    1.52 -                        add_unsafes [allL_thin, exR_thin];
    1.53 +                        add_unsafes [allL_thin, exR_thin, the_equality];
    1.54  
    1.55  val LK_dup_pack = prop_pack add_safes   [allR, exL] 
    1.56 -                            add_unsafes [allL, exR];
    1.57 +                            add_unsafes [allL, exR, the_equality];
    1.58  
    1.59  
    1.60 -thm_pack_ref() := LK_pack;
    1.61 -
    1.62 -fun Fast_tac st = fast_tac (thm_pack()) st;
    1.63 -fun Step_tac st = step_tac (thm_pack()) st;
    1.64 -fun Safe_tac st = safe_tac (thm_pack()) st;
    1.65 +pack_ref() := LK_pack;
    1.66  
    1.67  fun lemma_tac th i = 
    1.68      rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
    1.69 @@ -167,3 +179,17 @@
    1.70  by (rtac (trans RS R_of_imp RS mp_R) 1);
    1.71  by (ALLGOALS assume_tac);
    1.72  qed "transR";
    1.73 +
    1.74 +
    1.75 +(* Two theorms for rewriting only one instance of a definition:
    1.76 +   the first for definitions of formulae and the second for terms *)
    1.77 +
    1.78 +val prems = goal thy "(A == B) ==> |- A <-> B";
    1.79 +by (rewrite_goals_tac prems);
    1.80 +by (rtac iff_refl 1);
    1.81 +qed "def_imp_iff";
    1.82 +
    1.83 +val prems = goal thy "(A == B) ==> |- A = B";
    1.84 +by (rewrite_goals_tac prems);
    1.85 +by (rtac refl 1);
    1.86 +qed "meta_eq_to_obj_eq";