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