1 (******************************************************************************)
2 (* FILE : rewrite_rules.ml *)
3 (* DESCRIPTION : Using axioms and lemmas as rewrite rules. *)
5 (* READS FILES : <none> *)
6 (* WRITES FILES : <none> *)
8 (* AUTHOR : R.J.Boulton *)
9 (* DATE : 14th May 1991 *)
11 (* LAST MODIFIED : R.J.Boulton *)
12 (* DATE : 15th October 1992 *)
14 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
16 (******************************************************************************)
18 (*----------------------------------------------------------------------------*)
19 (* is_permutative : term -> bool *)
21 (* Determines whether or not an equation is permutative (the left-hand and *)
22 (* right-hand sides are instances of one another). A permutative equation may *)
23 (* cause looping when it is used for rewriting. *)
24 (*----------------------------------------------------------------------------*)
26 let is_permutative tm =
27 try (let (l,r) = dest_eq tm
28 in let bind1 = term_match [] l r
29 and bind2 = term_match [] r l
31 ) with Failure _ -> false;;
34 (*----------------------------------------------------------------------------*)
35 (* lex_smaller_term : term -> term -> bool *)
37 (* Computes whether the first term is `alphabetically' smaller than the *)
38 (* second term. Used to avoid looping when rewriting with permutative rules. *)
40 (* A constant is considered to be smaller than a variable which in turn is *)
41 (* considered to be smaller than an application. Two variables or two *)
42 (* constants are compared alphabetically by name. An application (f1 x1) is *)
43 (* considered to be smaller than another application (f2 x2) if either f1 is *)
44 (* smaller than f2, or f1 equals f2 and x1 is smaller than x2. *)
45 (*----------------------------------------------------------------------------*)
47 let rec lex_smaller_term tm1 tm2 =
49 (if (is_const tm1) then
51 then let (name1,type1) = dest_const tm1
52 and (name2,type2) = dest_const tm2
53 in (if (type1 = type2)
57 else if (is_var tm1) then
58 (if (is_const tm2) then false
60 then let (name1,type1) = dest_var tm1
61 and (name2,type2) = dest_var tm2
62 in (if (type1 = type2)
66 else if (is_comb tm1) then
68 then let (rator1,rand1) = dest_comb tm1
69 and (rator2,rand2) = dest_comb tm2
70 in (lex_smaller_term rator1 rator2) or
71 ((rator1 = rator2) & (lex_smaller_term rand1 rand2))
74 ) with Failure _ -> failwith "lex_smaller_term";;
76 (*----------------------------------------------------------------------------*)
77 (* inst_eq_thm : ((term # term) list # (type # type) list) -> thm -> thm *)
79 (* Instantiates a theorem (possibly having hypotheses) with a binding. *)
80 (* Assumes the conclusion is an equality, so that discharging then undisching *)
81 (* cannot cause parts of the conclusion to be moved into the hypotheses. *)
82 (*----------------------------------------------------------------------------*)
84 let inst_eq_thm (tm_bind,ty_bind) th =
85 let (insts,vars) = List.split tm_bind
86 in (UNDISCH_ALL o (SPECL insts) o (GENL vars) o
87 (INST_TYPE ty_bind) o DISCH_ALL) th;;
89 (*----------------------------------------------------------------------------*)
90 (* applicable_rewrites : term -> thm list *)
92 (* Returns the results of rewriting the term with those rewrite rules that *)
93 (* are applicable to it. A rewrite rule is not applicable if it's permutative *)
94 (* and the rewriting does not produce an alphabetically smaller term. *)
95 (*----------------------------------------------------------------------------*)
97 let applicable_rewrites tm =
98 let applicable_rewrite tm th =
100 in let (_,tm_bind,ty_bind) = term_match [] (lhs conc) tm
101 in let instth = inst_eq_thm (tm_bind,ty_bind) th
102 in if (is_permutative conc)
103 then (let (l,r) = dest_eq (concl instth)
104 in if (lex_smaller_term r l)
108 in mapfilter ((applicable_rewrite tm) o snd) !system_rewrites;;
110 (*----------------------------------------------------------------------------*)
111 (* ARGS_CONV : conv -> conv *)
113 (* Applies a conversion to every argument of an application of the form *)
115 (*----------------------------------------------------------------------------*)
117 let rec ARGS_CONV conv tm =
119 ((RATOR_CONV (ARGS_CONV conv)) THENC (RAND_CONV conv)) tm
120 ) with Failure _ -> ALL_CONV tm;;
122 (*----------------------------------------------------------------------------*)
123 (* assump_inst_hyps : term list -> *)
126 (* ((term # term) list # (type # type) list) *)
128 (* Searches a list of hypotheses for one that matches the specified *)
129 (* assumption such that the variables instantiated are precisely those in the *)
130 (* list of variables given. If such a hypothesis is found, the binding *)
131 (* produced by the match is returned. *)
132 (*----------------------------------------------------------------------------*)
134 let rec assump_inst_hyps vars assump hyps =
135 try(let (_,tm_bind,ty_bind) = term_match [] (hd hyps) assump
136 in let bind = (tm_bind,ty_bind)
137 in if (set_eq vars (map snd (fst bind)))
140 with Failure _ -> try (assump_inst_hyps vars assump (tl hyps))
141 with Failure _ -> failwith "assump_inst_hyps";;
143 (*----------------------------------------------------------------------------*)
144 (* assumps_inst_hyps : term list -> *)
147 (* ((term # term) list # (type # type) list) *)
149 (* Searches a list of hypotheses and a list of assumptions for a pairing that *)
150 (* match (the assumption is an instance of the hypothesis) such that the *)
151 (* variables instantiated are precisely those in the list of variables given. *)
152 (* If such a pair is found, the binding produced by the match is returned. *)
153 (*----------------------------------------------------------------------------*)
155 let rec assumps_inst_hyps vars assumps hyps =
156 try (assump_inst_hyps vars (hd assumps) hyps)
157 with Failure _ -> try (assumps_inst_hyps vars (tl assumps) hyps)
158 with Failure _ -> failwith "assumps_inst_hyps";;
160 (*----------------------------------------------------------------------------*)
161 (* inst_frees_in_hyps : term list -> thm -> thm *)
163 (* Takes a theorem (possibly with hypotheses) and computes a list of *)
164 (* variables that are free in the hypotheses but not in the conclusion. *)
165 (* If this list of variables is empty the original theorem is returned. *)
166 (* The function also takes a list of assumptions as another argument. Once it *)
167 (* has the list of variables it searches for an assumption and a hypothesis *)
168 (* such that the hypothesis matches the assumption binding precisely those *)
169 (* variables in the list. If this is successful the original theorem is *)
170 (* returned having had the variables in the list instantiated. *)
171 (*----------------------------------------------------------------------------*)
173 let inst_frees_in_hyps assumps th =
174 try (let hyps = hyp th
175 in let hyp_frees = setify (flat (map frees hyps))
176 in let vars = subtract hyp_frees (frees (concl th))
179 else let bind = assumps_inst_hyps vars assumps hyps
180 in inst_eq_thm bind th
181 ) with Failure _ -> failwith "inst_frees_in_hyps";;
183 (*----------------------------------------------------------------------------*)
184 (* NOT_IMP_EQ_EQ_EQ_OR = |- (~x ==> (y = y')) = ((y \/ x) = (y' \/ x)) *)
185 (*----------------------------------------------------------------------------*)
187 let NOT_IMP_EQ_EQ_EQ_OR =
189 (`(~x ==> (y = y')) = ((y \/ x) = (y' \/ x))`,
190 BOOL_CASES_TAC `x:bool` THEN
191 BOOL_CASES_TAC `y:bool` THEN
192 BOOL_CASES_TAC `y':bool` THEN
195 (*----------------------------------------------------------------------------*)
196 (* IMP_EQ_EQ_EQ_OR_NOT = |- (x ==> (y = y')) = ((y \/ ~x) = (y' \/ ~x)) *)
197 (*----------------------------------------------------------------------------*)
199 let IMP_EQ_EQ_EQ_OR_NOT =
201 (`(x ==> (y = y')) = ((y \/ ~x) = (y' \/ ~x))`,
202 BOOL_CASES_TAC `x:bool` THEN
203 BOOL_CASES_TAC `y:bool` THEN
204 BOOL_CASES_TAC `y':bool` THEN
207 (*----------------------------------------------------------------------------*)
208 (* NOT_IMP_EQ_OR_EQ_EQ_OR_OR = *)
209 (* |- (~x ==> ((y \/ t) = (y' \/ t))) = ((y \/ (x \/ t)) = (y' \/ (x \/ t))) *)
210 (*----------------------------------------------------------------------------*)
212 let NOT_IMP_EQ_OR_EQ_EQ_OR_OR =
214 (`(~x ==> ((y \/ t) = (y' \/ t))) = ((y \/ (x \/ t)) = (y' \/ (x \/ t)))`,
215 BOOL_CASES_TAC `x:bool` THEN
216 BOOL_CASES_TAC `y:bool` THEN
217 BOOL_CASES_TAC `y':bool` THEN
218 BOOL_CASES_TAC `t:bool` THEN
221 (*----------------------------------------------------------------------------*)
222 (* IMP_EQ_OR_EQ_EQ_OR_NOT_OR = *)
223 (* |- (x ==> ((y \/ t) = (y' \/ t))) = ((y \/ (~x \/ t)) = (y' \/ (~x \/ t))) *)
224 (*----------------------------------------------------------------------------*)
226 let IMP_EQ_OR_EQ_EQ_OR_NOT_OR =
228 (`(x ==> ((y \/ t) = (y' \/ t))) = ((y \/ (~x \/ t)) = (y' \/ (~x \/ t)))`,
229 BOOL_CASES_TAC `x:bool` THEN
230 BOOL_CASES_TAC `y:bool` THEN
231 BOOL_CASES_TAC `y':bool` THEN
232 BOOL_CASES_TAC `t:bool` THEN
235 (*----------------------------------------------------------------------------*)
236 (* IMP_EQ_EQ_EQ_NOT_OR = |- (x ==> (t = t')) = ((~x \/ t) = (~x \/ t')) *)
237 (*----------------------------------------------------------------------------*)
239 let IMP_EQ_EQ_EQ_NOT_OR =
241 (`(x ==> (t = t')) = ((~x \/ t) = (~x \/ t'))`,
242 BOOL_CASES_TAC `x:bool` THEN
243 BOOL_CASES_TAC `t:bool` THEN
244 BOOL_CASES_TAC `t':bool` THEN
247 (*----------------------------------------------------------------------------*)
248 (* IMP_NOT_EQ_EQ_EQ_OR = |- (~x ==> (t = t')) = ((x \/ t) = (x \/ t')) *)
249 (*----------------------------------------------------------------------------*)
251 let IMP_NOT_EQ_EQ_EQ_OR =
253 (`(~x ==> (t = t')) = ((x \/ t) = (x \/ t'))`,
254 BOOL_CASES_TAC `x:bool` THEN
255 BOOL_CASES_TAC `t:bool` THEN
256 BOOL_CASES_TAC `t':bool` THEN
259 (*----------------------------------------------------------------------------*)
260 (* T_OR = |- T \/ t = T *)
261 (* OR_T = |- t \/ T = T *)
262 (* F_OR = |- F \/ t = t *)
263 (* OR_F = |- t \/ F = t *)
264 (*----------------------------------------------------------------------------*)
266 let [T_OR;OR_T;F_OR;OR_F;_] = CONJUNCTS (SPEC_ALL OR_CLAUSES);;
268 (*----------------------------------------------------------------------------*)
269 (* UNDER_DISJ_DISCH : term -> thm -> thm *)
271 (* A, ~x |- y \/ t = y' \/ t A, x |- y \/ t = y' \/ t *)
272 (* ------------------------------- --------------------------------- *)
273 (* A |- y \/ x \/ t = y' \/ x \/ t A |- y \/ ~x \/ t = y' \/ ~x \/ t *)
275 (* A, ~x |- y = y' A, x |- y = y' *)
276 (* --------------------- ----------------------- *)
277 (* A |- y \/ x = y' \/ x A |- y \/ ~x = y' \/ ~x *)
279 (* The function assumes that y is a literal, so it is valid to test the LHS *)
280 (* of the theorem to see if it is a disjunction in order to determine which *)
282 (*----------------------------------------------------------------------------*)
284 let UNDER_DISJ_DISCH tm th =
287 if (is_disj (lhs (concl th)))
289 then NOT_IMP_EQ_OR_EQ_EQ_OR_OR
290 else IMP_EQ_OR_EQ_EQ_OR_NOT_OR
292 then NOT_IMP_EQ_EQ_EQ_OR
293 else IMP_EQ_EQ_EQ_OR_NOT
294 in CONV_RULE (REWR_CONV rewrite) (DISCH tm th)
295 ) with Failure _ -> failwith "UNDER_DISJ_DISCH";;
297 (*----------------------------------------------------------------------------*)
298 (* OVER_DISJ_DISCH : term -> thm -> thm *)
300 (* A, ~x |- t = t' A, x |- t = t' *)
301 (* --------------------- ----------------------- *)
302 (* A |- x \/ t = x \/ t' A |- ~x \/ t = ~x \/ t' *)
303 (*----------------------------------------------------------------------------*)
305 let OVER_DISJ_DISCH tm th =
308 then IMP_NOT_EQ_EQ_EQ_OR
309 else IMP_EQ_EQ_EQ_NOT_OR
310 in CONV_RULE (REWR_CONV rewrite) (DISCH tm th)
311 ) with Failure _ -> failwith "OVER_DISJ_DISCH";;
313 (*----------------------------------------------------------------------------*)
314 (* MULTI_DISJ_DISCH : (term list # term list) -> thm -> thm *)
318 (* MULTI_DISJ_DISCH (["x1"; "x2"],["~x3"; "x4"]) x1, ~x3, x4, x2 |- y = y' *)
320 (* |- ~x1 \/ ~x2 \/ y \/ x3 \/ ~x4 = ~x1 \/ ~x2 \/ y' \/ x3 \/ ~x4 *)
323 (* MULTI_DISJ_DISCH (["x1"; "x2"],["~x3"; "x4"]) x1, ~x3, x4, x2 |- y = F *)
325 (* |- ~x1 \/ ~x2 \/ y \/ x3 \/ ~x4 = ~x1 \/ ~x2 \/ x3 \/ ~x4 *)
328 (* MULTI_DISJ_DISCH (["x1"; "x2"],["~x3"; "x4"]) x1, ~x3, x4, x2 |- y = T *)
330 (* |- ~x1 \/ ~x2 \/ y \/ x3 \/ ~x4 = T *)
331 (*----------------------------------------------------------------------------*)
333 let MULTI_DISJ_DISCH (overs,unders) th =
335 (let th1 = itlist UNDER_DISJ_DISCH unders th
336 in let tm1 = rhs (concl th1)
338 if (try(is_T (fst (dest_disj tm1))) with Failure _ -> false) then
339 (CONV_RULE (RAND_CONV (REWR_CONV T_OR)) th1)
340 else if (try(is_F (fst (dest_disj tm1))) with Failure _ -> false) then
341 (CONV_RULE (RAND_CONV (REWR_CONV F_OR)) th1)
343 in let tm2 = rhs (concl th2)
345 if (is_T tm2) then CONV_RULE (RAND_CONV (REWR_CONV OR_T)) else I
346 in itlist (fun tm th -> rule (OVER_DISJ_DISCH tm th)) overs th2
347 ) with Failure _ -> failwith "MULTI_DISJ_DISCH";;