1459

1 
(* Title: FOLP/classical

0

2 
ID: $Id$

1459

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1992 University of Cambridge


5 


6 
Like Provers/classical but modified because match_tac is unsuitable for


7 
proof objects.


8 


9 
Theorem prover for classical reasoning, including predicate calculus, set


10 
theory, etc.


11 


12 
Rules must be classified as intr, elim, safe, hazardous.


13 


14 
A rule is unsafe unless it can be applied blindly without harmful results.


15 
For a rule to be safe, its premises and conclusion should be logically


16 
equivalent. There should be no variables in the premises that are not in


17 
the conclusion.


18 
*)


19 


20 
signature CLASSICAL_DATA =


21 
sig

1459

22 
val mp: thm (* [ P>Q; P ] ==> Q *)


23 
val not_elim: thm (* [ ~P; P ] ==> R *)


24 
val swap: thm (* ~P ==> (~Q ==> P) ==> Q *)


25 
val sizef : thm > int (* size function for BEST_FIRST *)

0

26 
val hyp_subst_tacs: (int > tactic) list


27 
end;


28 


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


30 
infix 4 addSIs addSEs addSDs addIs addEs addDs;


31 


32 


33 
signature CLASSICAL =


34 
sig


35 
type claset


36 
val empty_cs: claset


37 
val addDs : claset * thm list > claset


38 
val addEs : claset * thm list > claset


39 
val addIs : claset * thm list > claset


40 
val addSDs: claset * thm list > claset


41 
val addSEs: claset * thm list > claset


42 
val addSIs: claset * thm list > claset


43 
val print_cs: claset > unit


44 
val rep_claset: claset >


45 
{safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list,


46 
safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,


47 
haz_brls: (bool*thm)list}


48 
val best_tac : claset > int > tactic


49 
val contr_tac : int > tactic


50 
val fast_tac : claset > int > tactic


51 
val inst_step_tac : int > tactic


52 
val joinrules : thm list * thm list > (bool * thm) list


53 
val mp_tac: int > tactic


54 
val safe_tac : claset > tactic


55 
val safe_step_tac : claset > int > tactic


56 
val slow_step_tac : claset > int > tactic


57 
val step_tac : claset > int > tactic


58 
val swapify : thm list > thm list


59 
val swap_res_tac : thm list > int > tactic


60 
val uniq_mp_tac: int > tactic


61 
end;


62 


63 


64 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =


65 
struct


66 


67 
local open Data in


68 


69 
(** Useful tactics for classical reasoning **)


70 


71 
val imp_elim = make_elim mp;


72 


73 
(*Solve goal that assumes both P and ~P. *)

1459

74 
val contr_tac = etac not_elim THEN' assume_tac;

0

75 


76 
(*Finds P>Q and P in the assumptions, replaces implication by Q *)


77 
fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i THEN assume_tac i;


78 


79 
(*Like mp_tac but instantiates no variables*)


80 
fun uniq_mp_tac i = ematch_tac ([not_elim,imp_elim]) i THEN uniq_assume_tac i;


81 


82 
(*Creates rules to eliminate ~A, from rules to introduce A*)


83 
fun swapify intrs = intrs RLN (2, [swap]);


84 


85 
(*Uses introduction rules in the normal way, or on negated assumptions,


86 
trying rules in order. *)


87 
fun swap_res_tac rls =


88 
let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap))


89 
in assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls)


90 
end;


91 


92 


93 
(*** Classical rule sets ***)


94 


95 
datatype claset =


96 
CS of {safeIs: thm list,

1459

97 
safeEs: thm list,


98 
hazIs: thm list,


99 
hazEs: thm list,


100 
(*the following are computed from the above*)


101 
safe0_brls: (bool*thm)list,


102 
safep_brls: (bool*thm)list,


103 
haz_brls: (bool*thm)list};

0

104 


105 
fun rep_claset (CS x) = x;


106 


107 
(*For use with biresolve_tac. Combines intrs with swap to catch negated


108 
assumptions. Also pairs elims with true. *)


109 
fun joinrules (intrs,elims) =


110 
map (pair true) (elims @ swapify intrs) @ map (pair false) intrs;


111 


112 
(*Note that allE precedes exI in haz_brls*)


113 
fun make_cs {safeIs,safeEs,hazIs,hazEs} =


114 
let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)


115 
partition (apl(0,op=) o subgoals_of_brl)

4440

116 
(sort (make_ord lessb) (joinrules(safeIs, safeEs)))

0

117 
in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,

1459

118 
safe0_brls=safe0_brls, safep_brls=safep_brls,

4440

119 
haz_brls = sort (make_ord lessb) (joinrules(hazIs, hazEs))}

0

120 
end;


121 


122 
(*** Manipulation of clasets ***)


123 


124 
val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};


125 


126 
fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =


127 
(writeln"Introduction rules"; prths hazIs;


128 
writeln"Safe introduction rules"; prths safeIs;


129 
writeln"Elimination rules"; prths hazEs;


130 
writeln"Safe elimination rules"; prths safeEs;


131 
());


132 


133 
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =


134 
make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};


135 


136 
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths =


137 
make_cs {safeIs=safeIs, safeEs=ths@safeEs, hazIs=hazIs, hazEs=hazEs};


138 


139 
fun cs addSDs ths = cs addSEs (map make_elim ths);


140 


141 
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addIs ths =


142 
make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=ths@hazIs, hazEs=hazEs};


143 


144 
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addEs ths =


145 
make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=ths@hazEs};


146 


147 
fun cs addDs ths = cs addEs (map make_elim ths);


148 


149 
(*** Simple tactics for theorem proving ***)


150 


151 
(*Attack subgoals using safe inferences*)


152 
fun safe_step_tac (CS{safe0_brls,safep_brls,...}) =


153 
FIRST' [uniq_assume_tac,

1459

154 
uniq_mp_tac,


155 
biresolve_tac safe0_brls,


156 
FIRST' hyp_subst_tacs,


157 
biresolve_tac safep_brls] ;

0

158 


159 
(*Repeatedly attack subgoals using safe inferences*)


160 
fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs));


161 


162 
(*These steps could instantiate variables and are therefore unsafe.*)


163 
val inst_step_tac = assume_tac APPEND' contr_tac;


164 


165 
(*Single step for the prover. FAILS unless it makes progress. *)


166 
fun step_tac (cs as (CS{haz_brls,...})) i =


167 
FIRST [safe_tac cs,


168 
inst_step_tac i,


169 
biresolve_tac haz_brls i];


170 


171 
(*** The following tactics all fail unless they solve one goal ***)


172 


173 
(*Dumb but fast*)


174 
fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));


175 


176 
(*Slower but smarter than fast_tac*)


177 
fun best_tac cs =


178 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));


179 


180 
(*Using a "safe" rule to instantiate variables is unsafe. This tactic


181 
allows backtracking from "safe" rules to "unsafe" rules here.*)


182 
fun slow_step_tac (cs as (CS{haz_brls,...})) i =


183 
safe_tac cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);


184 


185 
end;


186 
end;
