0

1 
(* Title: FOLP/classical


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


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


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


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 chain_tac : int > tactic


50 
val contr_tac : int > tactic


51 
val fast_tac : claset > int > tactic


52 
val inst_step_tac : int > tactic


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


54 
val mp_tac: int > tactic


55 
val safe_tac : claset > tactic


56 
val safe_step_tac : claset > int > tactic


57 
val slow_step_tac : claset > int > tactic


58 
val step_tac : claset > int > tactic


59 
val swapify : thm list > thm list


60 
val swap_res_tac : thm list > int > tactic


61 
val uniq_mp_tac: int > tactic


62 
end;


63 


64 


65 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =


66 
struct


67 


68 
local open Data in


69 


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


71 


72 
val imp_elim = make_elim mp;


73 


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


75 
val contr_tac = eresolve_tac [not_elim] THEN' assume_tac;


76 


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


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


79 


80 
(*Like mp_tac but instantiates no variables*)


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


82 


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


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


85 


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


87 
trying rules in order. *)


88 
fun swap_res_tac rls =


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


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


91 
end;


92 


93 
(*Given assumption P>Q, reduces subgoal Q to P [deletes the implication!] *)


94 
fun chain_tac i =


95 
eresolve_tac [imp_elim] i THEN


96 
(assume_tac (i+1) ORELSE contr_tac (i+1));


97 


98 
(*** Classical rule sets ***)


99 


100 
datatype claset =


101 
CS of {safeIs: thm list,


102 
safeEs: thm list,


103 
hazIs: thm list,


104 
hazEs: thm list,


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


106 
safe0_brls: (bool*thm)list,


107 
safep_brls: (bool*thm)list,


108 
haz_brls: (bool*thm)list};


109 


110 
fun rep_claset (CS x) = x;


111 


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


113 
assumptions. Also pairs elims with true. *)


114 
fun joinrules (intrs,elims) =


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


116 


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


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


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


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


121 
(sort lessb (joinrules(safeIs, safeEs)))


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


123 
safe0_brls=safe0_brls, safep_brls=safep_brls,


124 
haz_brls = sort lessb (joinrules(hazIs, hazEs))}


125 
end;


126 


127 
(*** Manipulation of clasets ***)


128 


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


130 


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


132 
(writeln"Introduction rules"; prths hazIs;


133 
writeln"Safe introduction rules"; prths safeIs;


134 
writeln"Elimination rules"; prths hazEs;


135 
writeln"Safe elimination rules"; prths safeEs;


136 
());


137 


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


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


140 


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


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


143 


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


145 


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


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


148 


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


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


151 


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


153 


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


155 


156 
(*Attack subgoals using safe inferences*)


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


158 
FIRST' [uniq_assume_tac,


159 
uniq_mp_tac,


160 
biresolve_tac safe0_brls,


161 
FIRST' hyp_subst_tacs,


162 
biresolve_tac safep_brls] ;


163 


164 
(*Repeatedly attack subgoals using safe inferences*)


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


166 


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


168 
val inst_step_tac = assume_tac APPEND' contr_tac;


169 


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


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


172 
FIRST [safe_tac cs,


173 
inst_step_tac i,


174 
biresolve_tac haz_brls i];


175 


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


177 


178 
(*Dumb but fast*)


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


180 


181 
(*Slower but smarter than fast_tac*)


182 
fun best_tac cs =


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


184 


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


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


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


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


189 


190 
end;


191 
end;
