7093

1 
(* Title: LK/LK0


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


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


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*)


44 
fun cutR_tac (sP: string) i =


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


46 


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


48 
fun cutL_tac (sP: string) i =


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


50 


51 


52 
(** Ifandonlyif rules **)

7122

53 
Goalw [iff_def]


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 


58 
Goalw [iff_def]


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*)


96 
val prop_pack = empty_pack add_safes


97 
[basic, refl, TrueR, FalseL,


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


99 
notL, notR, iffL, iffR];


100 


101 
val LK_pack = prop_pack add_safes [allR, exL]

7122

102 
add_unsafes [allL_thin, exR_thin, the_equality];

7093

103 


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 


110 
fun lemma_tac th i =


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


112 


113 
val [major,minor] = goal thy


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 


120 
val [major,minor] = goal thy


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 


130 
val [major,minor] = goal thy


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 


137 
val [major,minor] = goal thy


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*)


145 
val [prem] = goal thy


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 


152 


153 
qed_goal "conjunct1" thy "P&Q ==> P"


154 
(fn [major] => [lemma_tac major 1, Fast_tac 1]);


155 


156 
qed_goal "conjunct2" thy "P&Q ==> Q"


157 
(fn [major] => [lemma_tac major 1, Fast_tac 1]);


158 


159 
qed_goal "spec" thy " (ALL x. P(x)) ==>  P(x)"


160 
(fn [major] => [lemma_tac major 1, Fast_tac 1]);


161 


162 
(** Equality **)


163 


164 
Goal " a=b > b=a";


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


166 
qed "sym";


167 


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


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


170 
qed "trans";


171 


172 
(* Symmetry of equality in hypotheses *)


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


174 


175 
(* Symmetry of equality in hypotheses *)


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


177 


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


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


180 
by (ALLGOALS assume_tac);


181 
qed "transR";

7122

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