0

1 
(* Title: Provers/classical


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


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


7 
theory, etc.


8 


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


10 


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


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


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


14 
the conclusion.


15 
*)


16 


17 
signature CLASSICAL_DATA =


18 
sig


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


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


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


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


23 
val hyp_subst_tacs: (int > tactic) list


24 
end;


25 


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


27 
infix 4 addSIs addSEs addSDs addIs addEs addDs;


28 


29 


30 
signature CLASSICAL =


31 
sig


32 
type claset


33 
val empty_cs: claset


34 
val addDs : claset * thm list > claset


35 
val addEs : claset * thm list > claset


36 
val addIs : claset * thm list > claset


37 
val addSDs: claset * thm list > claset


38 
val addSEs: claset * thm list > claset


39 
val addSIs: claset * thm list > claset


40 
val print_cs: claset > unit


41 
val rep_claset: claset >


42 
{safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list}


43 
val best_tac : claset > int > tactic


44 
val chain_tac : int > tactic


45 
val contr_tac : int > tactic


46 
val eq_mp_tac: int > tactic


47 
val fast_tac : claset > int > tactic


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


49 
val mp_tac: int > tactic


50 
val safe_tac : claset > tactic


51 
val safe_step_tac : claset > int > tactic


52 
val slow_step_tac : claset > int > tactic


53 
val slow_best_tac : claset > int > tactic


54 
val slow_tac : claset > int > tactic


55 
val step_tac : claset > int > tactic


56 
val swapify : thm list > thm list


57 
val swap_res_tac : thm list > int > tactic


58 
val inst_step_tac : claset > int > tactic


59 
end;


60 


61 


62 
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL =


63 
struct


64 


65 
local open Data in


66 


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


68 


69 
val imp_elim = make_elim mp;


70 


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


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


73 


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


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


76 


77 
(*Like mp_tac but instantiates no variables*)


78 
fun eq_mp_tac i = ematch_tac ([not_elim,imp_elim]) i THEN eq_assume_tac i;


79 


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


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


82 


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


84 
trying rules in order. *)


85 
fun swap_res_tac rls =


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


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


88 
end;


89 


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


91 
fun chain_tac i =


92 
eresolve_tac [imp_elim] i THEN


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


94 


95 
(*** Classical rule sets ***)


96 


97 
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;


98 


99 
datatype claset =


100 
CS of {safeIs : thm list,


101 
safeEs : thm list,


102 
hazIs : thm list,


103 
hazEs : thm list,


104 
safe0_netpair : netpair,


105 
safep_netpair : netpair,


106 
haz_netpair : netpair};


107 


108 
fun rep_claset (CS{safeIs,safeEs,hazIs,hazEs,...}) =


109 
{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};


110 


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


112 
assumptions; pairs elims with true; sorts. *)


113 
fun joinrules (intrs,elims) =


114 
sort lessb


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


116 
map (pair false) intrs);


117 


118 
(*Make a claset from the four kinds of rules*)


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


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


121 
take_prefix (fn brl => subgoals_of_brl brl=0)


122 
(joinrules(safeIs, safeEs))


123 
in CS{safeIs = safeIs,


124 
safeEs = safeEs,


125 
hazIs = hazIs,


126 
hazEs = hazEs,


127 
safe0_netpair = build_netpair safe0_brls,


128 
safep_netpair = build_netpair safep_brls,


129 
haz_netpair = build_netpair (joinrules(hazIs, hazEs))}


130 
end;


131 


132 
(*** Manipulation of clasets ***)


133 


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


135 


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


137 
(writeln"Introduction rules"; prths hazIs;


138 
writeln"Safe introduction rules"; prths safeIs;


139 
writeln"Elimination rules"; prths hazEs;


140 
writeln"Safe elimination rules"; prths safeEs;


141 
());


142 


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


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


145 


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


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


148 


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


150 


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


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


153 


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


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


156 


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


158 


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


160 


161 
(*Attack subgoals using safe inferences  matching, not resolution*)


162 
fun safe_step_tac (CS{safe0_netpair,safep_netpair,...}) =


163 
FIRST' [eq_assume_tac,


164 
eq_mp_tac,


165 
bimatch_from_nets_tac safe0_netpair,


166 
FIRST' hyp_subst_tacs,


167 
bimatch_from_nets_tac safep_netpair] ;


168 


169 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*)


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


171 


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


173 
fun inst_step_tac (CS{safe0_netpair,safep_netpair,...}) =


174 
assume_tac APPEND'


175 
contr_tac APPEND'


176 
biresolve_from_nets_tac safe0_netpair APPEND'


177 
biresolve_from_nets_tac safep_netpair;


178 


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


180 
fun step_tac (cs as (CS{haz_netpair,...})) i =


181 
FIRST [safe_tac cs,


182 
inst_step_tac cs i,


183 
biresolve_from_nets_tac haz_netpair i];


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_netpair,...})) i =


188 
safe_tac cs ORELSE


189 
(inst_step_tac cs i APPEND biresolve_from_nets_tac haz_netpair i);


190 


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


192 


193 
(*Dumb but fast*)


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


195 


196 
(*Slower but smarter than fast_tac*)


197 
fun best_tac cs =


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


199 


200 
fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));


201 


202 
fun slow_best_tac cs =


203 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));


204 


205 
end;


206 
end;
