48 fun cutL_tac (sP: string) i = |
48 fun cutL_tac (sP: string) i = |
49 res_inst_tac [ ("P",sP) ] cut i THEN rtac thinL (i+1); |
49 res_inst_tac [ ("P",sP) ] cut i THEN rtac thinL (i+1); |
50 |
50 |
51 |
51 |
52 (** If-and-only-if rules **) |
52 (** If-and-only-if rules **) |
53 qed_goalw "iffR" thy [iff_def] |
53 Goalw [iff_def] |
54 "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F" |
54 "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"; |
55 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]); |
55 by (REPEAT (ares_tac [conjR,impR] 1)); |
|
56 qed "iffR"; |
56 |
57 |
57 qed_goalw "iffL" thy [iff_def] |
58 Goalw [iff_def] |
58 "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E" |
59 "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"; |
59 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]); |
60 by (REPEAT (ares_tac [conjL,impL,basic] 1)); |
|
61 qed "iffL"; |
60 |
62 |
61 qed_goalw "TrueR" thy [True_def] |
63 Goal "$H |- $E, (P <-> P), $F"; |
62 "$H |- $E, True, $F" |
64 by (REPEAT (resolve_tac [iffR,basic] 1)); |
63 (fn _=> [ rtac impR 1, rtac basic 1 ]); |
65 qed "iff_refl"; |
64 |
66 |
|
67 Goalw [True_def] "$H |- $E, True, $F"; |
|
68 by (rtac impR 1); |
|
69 by (rtac basic 1); |
|
70 qed "TrueR"; |
|
71 |
|
72 (*Descriptions*) |
|
73 val [p1,p2] = Goal |
|
74 "[| $H |- $E, P(a), $F; !!x. $H, P(x) |- $E, x=a, $F |] \ |
|
75 \ ==> $H |- $E, (THE x. P(x)) = a, $F"; |
|
76 by (rtac cut 1); |
|
77 by (rtac p2 2); |
|
78 by (rtac The 1 THEN rtac thinR 1 THEN rtac exchRS 1 THEN rtac p1 1); |
|
79 by (rtac thinR 1 THEN rtac exchRS 1 THEN rtac p2 1); |
|
80 qed "the_equality"; |
65 |
81 |
66 (** Weakened quantifier rules. Incomplete, they let the search terminate.**) |
82 (** Weakened quantifier rules. Incomplete, they let the search terminate.**) |
67 |
83 |
68 Goal "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"; |
84 Goal "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"; |
69 by (rtac allL 1); |
85 by (rtac allL 1); |
81 [basic, refl, TrueR, FalseL, |
97 [basic, refl, TrueR, FalseL, |
82 conjL, conjR, disjL, disjR, impL, impR, |
98 conjL, conjR, disjL, disjR, impL, impR, |
83 notL, notR, iffL, iffR]; |
99 notL, notR, iffL, iffR]; |
84 |
100 |
85 val LK_pack = prop_pack add_safes [allR, exL] |
101 val LK_pack = prop_pack add_safes [allR, exL] |
86 add_unsafes [allL_thin, exR_thin]; |
102 add_unsafes [allL_thin, exR_thin, the_equality]; |
87 |
103 |
88 val LK_dup_pack = prop_pack add_safes [allR, exL] |
104 val LK_dup_pack = prop_pack add_safes [allR, exL] |
89 add_unsafes [allL, exR]; |
105 add_unsafes [allL, exR, the_equality]; |
90 |
106 |
91 |
107 |
92 thm_pack_ref() := LK_pack; |
108 pack_ref() := LK_pack; |
93 |
|
94 fun Fast_tac st = fast_tac (thm_pack()) st; |
|
95 fun Step_tac st = step_tac (thm_pack()) st; |
|
96 fun Safe_tac st = safe_tac (thm_pack()) st; |
|
97 |
109 |
98 fun lemma_tac th i = |
110 fun lemma_tac th i = |
99 rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i; |
111 rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i; |
100 |
112 |
101 val [major,minor] = goal thy |
113 val [major,minor] = goal thy |
165 |
177 |
166 Goal "[| $H|- $E, $F, a=b; $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F"; |
178 Goal "[| $H|- $E, $F, a=b; $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F"; |
167 by (rtac (trans RS R_of_imp RS mp_R) 1); |
179 by (rtac (trans RS R_of_imp RS mp_R) 1); |
168 by (ALLGOALS assume_tac); |
180 by (ALLGOALS assume_tac); |
169 qed "transR"; |
181 qed "transR"; |
|
182 |
|
183 |
|
184 (* Two theorms for rewriting only one instance of a definition: |
|
185 the first for definitions of formulae and the second for terms *) |
|
186 |
|
187 val prems = goal thy "(A == B) ==> |- A <-> B"; |
|
188 by (rewrite_goals_tac prems); |
|
189 by (rtac iff_refl 1); |
|
190 qed "def_imp_iff"; |
|
191 |
|
192 val prems = goal thy "(A == B) ==> |- A = B"; |
|
193 by (rewrite_goals_tac prems); |
|
194 by (rtac refl 1); |
|
195 qed "meta_eq_to_obj_eq"; |