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