0

1 
(* Title: LK/lk.ML


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.thy (thanks also to Philippe de Groote)


7 
*)


8 


9 
open LK;


10 


11 
(*Higher precedence than := facilitates use of references*)


12 
infix 4 add_safes add_unsafes;


13 


14 
signature LK_RESOLVE =


15 
sig


16 
datatype pack = Pack of thm list * thm list


17 
val add_safes: pack * thm list > pack


18 
val add_unsafes: pack * thm list > pack


19 
val allL_thin: thm


20 
val best_tac: pack > int > tactic


21 
val could_res: term * term > bool


22 
val could_resolve_seq: term * term > bool


23 
val cutL_tac: string > int > tactic


24 
val cutR_tac: string > int > tactic


25 
val conL: thm


26 
val conR: thm


27 
val empty_pack: pack


28 
val exR_thin: thm


29 
val fast_tac: pack > int > tactic


30 
val filseq_resolve_tac: thm list > int > int > tactic


31 
val forms_of_seq: term > term list


32 
val has_prems: int > thm > bool


33 
val iffL: thm


34 
val iffR: thm


35 
val less: thm * thm > bool


36 
val LK_dup_pack: pack


37 
val LK_pack: pack


38 
val pc_tac: pack > int > tactic


39 
val prop_pack: pack


40 
val repeat_goal_tac: pack > int > tactic


41 
val reresolve_tac: thm list > int > tactic


42 
val RESOLVE_THEN: thm list > (int > tactic) > int > tactic


43 
val safe_goal_tac: pack > int > tactic


44 
val step_tac: pack > int > tactic


45 
val symL: thm


46 
val TrueR: thm


47 
end;


48 


49 


50 
structure LK_Resolve : LK_RESOLVE =


51 
struct


52 


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


54 
fun cutR_tac (sP: string) i =


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


56 


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


58 
fun cutL_tac (sP: string) i =


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


60 


61 


62 
(** Ifandonlyif rules **)


63 
val iffR = prove_goalw LK.thy [iff_def]


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


65 
(fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);


66 


67 
val iffL = prove_goalw LK.thy [iff_def]


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


69 
(fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);


70 


71 
val TrueR = prove_goalw LK.thy [True_def]


72 
"$H  $E, True, $F"


73 
(fn _=> [ rtac impR 1, rtac basic 1 ]);


74 


75 


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


77 


78 
val allL_thin = prove_goal LK.thy


79 
"$H, P(x), $G  $E ==> $H, ALL x.P(x), $G  $E"


80 
(fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);


81 


82 
val exR_thin = prove_goal LK.thy


83 
"$H  $E, P(x), $F ==> $H  $E, EX x.P(x), $F"


84 
(fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);


85 


86 
(* Symmetry of equality in hypotheses *)


87 
val symL = prove_goal LK.thy


88 
"$H, $G, B = A  $E ==> $H, A = B, $G  $E"


89 
(fn prems=>


90 
[ (rtac cut 1),


91 
(rtac thinL 2),


92 
(resolve_tac prems 2),


93 
(resolve_tac [basic RS sym] 1) ]);


94 


95 


96 
(**** Theorem Packs ****)


97 


98 
datatype pack = Pack of thm list * thm list;


99 


100 
(*A theorem pack has the form (safe rules, unsafe rules)


101 
An unsafe rule is incomplete or introduces variables in subgoals,


102 
and is tried only when the safe rules are not applicable. *)


103 


104 
fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);


105 


106 
val empty_pack = Pack([],[]);


107 


108 
fun (Pack(safes,unsafes)) add_safes ths =


109 
Pack(sort less (ths@safes), unsafes);


110 


111 
fun (Pack(safes,unsafes)) add_unsafes ths =


112 
Pack(safes, sort less (ths@unsafes));


113 


114 
(*The rules of LK*)


115 
val prop_pack = empty_pack add_safes


116 
[basic, refl, conjL, conjR, disjL, disjR, impL, impR,


117 
notL, notR, iffL, iffR];


118 


119 
val LK_pack = prop_pack add_safes [allR, exL]


120 
add_unsafes [allL_thin, exR_thin];


121 


122 
val LK_dup_pack = prop_pack add_safes [allR, exL]


123 
add_unsafes [allL, exR];


124 


125 


126 


127 
(*Returns the list of all formulas in the sequent*)


128 
fun forms_of_seq (Const("Seqof",_) $ P $ u) = P :: forms_of_seq u


129 
 forms_of_seq (H $ u) = forms_of_seq u


130 
 forms_of_seq _ = [];


131 


132 
(*Tests whether two sequences (left or right sides) could be resolved.


133 
seqp is a premise (subgoal), seqc is a conclusion of an objectrule.


134 
Assumes each formula in seqc is surrounded by sequence variables


135 
 checks that each concl formula looks like some subgoal formula.


136 
It SHOULD check order as well, using recursion rather than forall/exists*)


137 
fun could_res (seqp,seqc) =


138 
forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc))


139 
(forms_of_seq seqp))


140 
(forms_of_seq seqc);


141 


142 
(*Tests whether two sequents GH could be resolved, comparing each side.*)


143 
fun could_resolve_seq (prem,conc) =


144 
case (prem,conc) of


145 
(_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),


146 
_ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>


147 
could_res (leftp,leftc) andalso could_res (rightp,rightc)


148 
 _ => false;


149 


150 


151 
(*Like filt_resolve_tac, using could_resolve_seq


152 
Much faster than resolve_tac when there are many rules.


153 
Resolve subgoal i using the rules, unless more than maxr are compatible. *)


154 
fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>


155 
let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)


156 
in if length rls > maxr then no_tac else resolve_tac rls i


157 
end);


158 


159 


160 
(*Predicate: does the rule have n premises? *)


161 
fun has_prems n rule = (nprems_of rule = n);


162 


163 
(*Continuationstyle tactical for resolution.


164 
The list of rules is partitioned into 0, 1, 2 premises.


165 
The resulting tactic, gtac, tries to resolve with rules.


166 
If successful, it recursively applies nextac to the new subgoals only.


167 
Else fails. (Treatment of goals due to Ph. de Groote)


168 
Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)


169 


170 
(*Takes rule lists separated in to 0, 1, 2, >2 premises.


171 
The abstraction over state prevents needless divergence in recursion.


172 
The 9999 should be a parameter, to delay treatment of flexible goals. *)


173 
fun RESOLVE_THEN rules =


174 
let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;


175 
fun tac nextac i = STATE (fn state =>


176 
filseq_resolve_tac rls0 9999 i


177 
ORELSE


178 
(DETERM(filseq_resolve_tac rls1 9999 i) THEN TRY(nextac i))


179 
ORELSE


180 
(DETERM(filseq_resolve_tac rls2 9999 i) THEN TRY(nextac(i+1))


181 
THEN TRY(nextac i)) )


182 
in tac end;


183 


184 


185 
(*repeated resolution applied to the designated goal*)


186 
fun reresolve_tac rules =


187 
let val restac = RESOLVE_THEN rules; (*preprocessing done now*)


188 
fun gtac i = restac gtac i


189 
in gtac end;


190 


191 
(*tries the safe rules repeatedly before the unsafe rules. *)


192 
fun repeat_goal_tac (Pack(safes,unsafes)) =


193 
let val restac = RESOLVE_THEN safes


194 
and lastrestac = RESOLVE_THEN unsafes;


195 
fun gtac i = restac gtac i ORELSE lastrestac gtac i


196 
in gtac end;


197 


198 


199 
(*Tries safe rules only*)


200 
fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;


201 


202 
(*Tries a safe rule or else a unsafe rule. Singlestep for tracing. *)


203 
fun step_tac (thm_pack as Pack(safes,unsafes)) =


204 
safe_goal_tac thm_pack ORELSE'


205 
filseq_resolve_tac unsafes 9999;


206 


207 


208 
(* Tactic for reducing a goal, using Predicate Calculus rules.


209 
A decision procedure for Propositional Calculus, it is incomplete


210 
for PredicateCalculus because of allL_thin and exR_thin.


211 
Fails if it can do nothing. *)


212 
fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1));


213 


214 
(*The following two tactics are analogous to those provided by


215 
Provers/classical. In fact, pc_tac is usually FASTER than fast_tac!*)


216 
fun fast_tac thm_pack =


217 
SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1));


218 


219 
fun best_tac thm_pack =


220 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm)


221 
(step_tac thm_pack 1));


222 


223 
(** Contraction. Useful since some rules are not complete. **)


224 


225 
val conR = prove_goal LK.thy


226 
"$H  $E, P, $F, P ==> $H  $E, P, $F"


227 
(fn prems=>


228 
[ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);


229 


230 
val conL = prove_goal LK.thy


231 
"$H, P, $G, P  $E ==> $H, P, $G  $E"


232 
(fn prems=>


233 
[ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);


234 


235 
end;


236 


237 
open LK_Resolve;
