17481

1 
(* Title: LK/LK0.ML

7093

2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 

17481

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

7093

7 


8 
Structural rules by Soren Heilmann


9 
*)


10 


11 
(** Structural Rules on formulas **)


12 


13 
(*contraction*)


14 


15 
Goal "$H  $E, P, P, $F ==> $H  $E, P, $F";


16 
by (etac contRS 1);


17 
qed "contR";


18 


19 
Goal "$H, P, P, $G  $E ==> $H, P, $G  $E";


20 
by (etac contLS 1);


21 
qed "contL";


22 


23 
(*thinning*)


24 


25 
Goal "$H  $E, $F ==> $H  $E, P, $F";


26 
by (etac thinRS 1);


27 
qed "thinR";


28 


29 
Goal "$H, $G  $E ==> $H, P, $G  $E";


30 
by (etac thinLS 1);


31 
qed "thinL";


32 


33 
(*exchange*)


34 


35 
Goal "$H  $E, Q, P, $F ==> $H  $E, P, Q, $F";


36 
by (etac exchRS 1);


37 
qed "exchR";


38 


39 
Goal "$H, Q, P, $G  $E ==> $H, P, Q, $G  $E";


40 
by (etac exchLS 1);


41 
qed "exchL";


42 


43 
(*Cut and thin, replacing the rightside formula*)

17481

44 
fun cutR_tac (sP: string) i =

7093

45 
res_inst_tac [ ("P",sP) ] cut i THEN rtac thinR i;


46 


47 
(*Cut and thin, replacing the leftside formula*)

17481

48 
fun cutL_tac (sP: string) i =

7093

49 
res_inst_tac [ ("P",sP) ] cut i THEN rtac thinL (i+1);


50 


51 


52 
(** Ifandonlyif rules **)

17481

53 
Goalw [iff_def]

7122

54 
"[ $H,P  $E,Q,$F; $H,Q  $E,P,$F ] ==> $H  $E, P <> Q, $F";


55 
by (REPEAT (ares_tac [conjR,impR] 1));


56 
qed "iffR";


57 

17481

58 
Goalw [iff_def]

7122

59 
"[ $H,$G  $E,P,Q; $H,Q,P,$G  $E ] ==> $H, P <> Q, $G  $E";


60 
by (REPEAT (ares_tac [conjL,impL,basic] 1));


61 
qed "iffL";


62 


63 
Goal "$H  $E, (P <> P), $F";


64 
by (REPEAT (resolve_tac [iffR,basic] 1));


65 
qed "iff_refl";

7093

66 

7122

67 
Goalw [True_def] "$H  $E, True, $F";


68 
by (rtac impR 1);


69 
by (rtac basic 1);


70 
qed "TrueR";

7093

71 

7122

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";

7093

81 


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


83 


84 
Goal "$H, P(x), $G  $E ==> $H, ALL x. P(x), $G  $E";


85 
by (rtac allL 1);


86 
by (etac thinL 1);


87 
qed "allL_thin";


88 


89 
Goal "$H  $E, P(x), $F ==> $H  $E, EX x. P(x), $F";


90 
by (rtac exR 1);


91 
by (etac thinR 1);


92 
qed "exR_thin";


93 


94 


95 
(*The rules of LK*)

17481

96 
val prop_pack = empty_pack add_safes


97 
[basic, refl, TrueR, FalseL,


98 
conjL, conjR, disjL, disjR, impL, impR,

7093

99 
notL, notR, iffL, iffR];


100 

17481

101 
val LK_pack = prop_pack add_safes [allR, exL]

7122

102 
add_unsafes [allL_thin, exR_thin, the_equality];

7093

103 

17481

104 
val LK_dup_pack = prop_pack add_safes [allR, exL]

7122

105 
add_unsafes [allL, exR, the_equality];

7093

106 


107 

7122

108 
pack_ref() := LK_pack;

7093

109 

17481

110 
fun lemma_tac th i =

7093

111 
rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;


112 

17481

113 
val [major,minor] = goal (the_context ())

7093

114 
"[ $H  $E, $F, P > Q; $H  $E, $F, P ] ==> $H  $E, Q, $F";


115 
by (rtac (thinRS RS cut) 1 THEN rtac major 1);


116 
by (Step_tac 1);


117 
by (rtac thinR 1 THEN rtac minor 1);


118 
qed "mp_R";


119 

17481

120 
val [major,minor] = goal (the_context ())

7093

121 
"[ $H, $G  $E, P > Q; $H, $G, Q  $E ] ==> $H, P, $G  $E";


122 
by (rtac (thinL RS cut) 1 THEN rtac major 1);


123 
by (Step_tac 1);


124 
by (rtac thinL 1 THEN rtac minor 1);


125 
qed "mp_L";


126 


127 


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


129 

17481

130 
val [major,minor] = goal (the_context ())

7093

131 
"[  P > Q; $H  $E, $F, P ] ==> $H  $E, Q, $F";


132 
by (rtac mp_R 1);


133 
by (rtac minor 2);


134 
by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);


135 
qed "R_of_imp";


136 

17481

137 
val [major,minor] = goal (the_context ())

7093

138 
"[  P > Q; $H, $G, Q  $E ] ==> $H, P, $G  $E";


139 
by (rtac mp_L 1);


140 
by (rtac minor 2);


141 
by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);


142 
qed "L_of_imp";


143 


144 
(*Can be used to create implications in a subgoal*)

17481

145 
val [prem] = goal (the_context ())

7093

146 
"[ $H, $G  $E, $F, P > Q ] ==> $H, P, $G  $E, Q, $F";


147 
by (rtac mp_L 1);


148 
by (rtac basic 2);


149 
by (rtac thinR 1 THEN rtac prem 1);


150 
qed "backwards_impR";


151 

9259

152 
Goal "P&Q ==> P";


153 
by (etac (thinR RS cut) 1);

17481

154 
by (Fast_tac 1);

9259

155 
qed "conjunct1";

7093

156 

9259

157 
Goal "P&Q ==> Q";


158 
by (etac (thinR RS cut) 1);

17481

159 
by (Fast_tac 1);

9259

160 
qed "conjunct2";

7093

161 

9259

162 
Goal " (ALL x. P(x)) ==>  P(x)";


163 
by (etac (thinR RS cut) 1);

17481

164 
by (Fast_tac 1);

9259

165 
qed "spec";

7093

166 


167 
(** Equality **)


168 


169 
Goal " a=b > b=a";


170 
by (safe_tac (LK_pack add_safes [subst]) 1);


171 
qed "sym";


172 


173 
Goal " a=b > b=c > a=c";


174 
by (safe_tac (LK_pack add_safes [subst]) 1);


175 
qed "trans";


176 


177 
(* Symmetry of equality in hypotheses *)


178 
bind_thm ("symL", sym RS L_of_imp);


179 


180 
(* Symmetry of equality in hypotheses *)


181 
bind_thm ("symR", sym RS R_of_imp);


182 


183 
Goal "[ $H $E, $F, a=b; $H $E, $F, b=c ] ==> $H $E, a=c, $F";


184 
by (rtac (trans RS R_of_imp RS mp_R) 1);


185 
by (ALLGOALS assume_tac);


186 
qed "transR";

7122

187 


188 


189 
(* Two theorms for rewriting only one instance of a definition:


190 
the first for definitions of formulae and the second for terms *)


191 

17481

192 
val prems = goal (the_context ()) "(A == B) ==>  A <> B";

7122

193 
by (rewrite_goals_tac prems);


194 
by (rtac iff_refl 1);


195 
qed "def_imp_iff";


196 

17481

197 
val prems = goal (the_context ()) "(A == B) ==>  A = B";

7122

198 
by (rewrite_goals_tac prems);


199 
by (rtac refl 1);


200 
qed "meta_eq_to_obj_eq";
