author | wenzelm |
Sat, 28 Jun 2008 22:52:03 +0200 | |
changeset 27388 | 226835ea8d2b |
parent 26939 | 1035c89b4c02 |
child 29265 | 5b4247055bd7 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: FOLP/simp |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
FOLP version of... |
|
7 |
||
8 |
Generic simplifier, suitable for most logics. (from Provers) |
|
9 |
||
10 |
This version allows instantiation of Vars in the subgoal, since the proof |
|
11 |
term must change. |
|
12 |
*) |
|
13 |
||
14 |
signature SIMP_DATA = |
|
15 |
sig |
|
16 |
val case_splits : (thm * string) list |
|
17 |
val dest_red : term -> term * term * term |
|
18 |
val mk_rew_rules : thm -> thm list |
|
19 |
val norm_thms : (thm*thm) list (* [(?x>>norm(?x), norm(?x)>>?x), ...] *) |
|
20 |
val red1 : thm (* ?P>>?Q ==> ?P ==> ?Q *) |
|
21 |
val red2 : thm (* ?P>>?Q ==> ?Q ==> ?P *) |
|
22 |
val refl_thms : thm list |
|
23 |
val subst_thms : thm list (* [ ?a>>?b ==> ?P(?a) ==> ?P(?b), ...] *) |
|
24 |
val trans_thms : thm list |
|
25 |
end; |
|
26 |
||
27 |
||
28 |
infix 4 addrews addcongs delrews delcongs setauto; |
|
29 |
||
30 |
signature SIMP = |
|
31 |
sig |
|
32 |
type simpset |
|
33 |
val empty_ss : simpset |
|
34 |
val addcongs : simpset * thm list -> simpset |
|
35 |
val addrews : simpset * thm list -> simpset |
|
36 |
val delcongs : simpset * thm list -> simpset |
|
37 |
val delrews : simpset * thm list -> simpset |
|
38 |
val dest_ss : simpset -> thm list * thm list |
|
39 |
val print_ss : simpset -> unit |
|
40 |
val setauto : simpset * (int -> tactic) -> simpset |
|
41 |
val ASM_SIMP_CASE_TAC : simpset -> int -> tactic |
|
42 |
val ASM_SIMP_TAC : simpset -> int -> tactic |
|
43 |
val CASE_TAC : simpset -> int -> tactic |
|
44 |
val SIMP_CASE2_TAC : simpset -> int -> tactic |
|
45 |
val SIMP_THM : simpset -> thm -> thm |
|
46 |
val SIMP_TAC : simpset -> int -> tactic |
|
47 |
val SIMP_CASE_TAC : simpset -> int -> tactic |
|
48 |
val mk_congs : theory -> string list -> thm list |
|
49 |
val mk_typed_congs : theory -> (string * string) list -> thm list |
|
50 |
(* temporarily disabled: |
|
51 |
val extract_free_congs : unit -> thm list |
|
52 |
*) |
|
53 |
val tracing : bool ref |
|
54 |
end; |
|
55 |
||
56 |
functor SimpFun (Simp_data: SIMP_DATA) : SIMP = |
|
57 |
struct |
|
58 |
||
19805 | 59 |
local open Simp_data in |
0 | 60 |
|
61 |
(*For taking apart reductions into left, right hand sides*) |
|
62 |
val lhs_of = #2 o dest_red; |
|
63 |
val rhs_of = #3 o dest_red; |
|
64 |
||
65 |
(*** Indexing and filtering of theorems ***) |
|
66 |
||
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21287
diff
changeset
|
67 |
fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2); |
0 | 68 |
|
69 |
(*insert a thm in a discrimination net by its lhs*) |
|
70 |
fun lhs_insert_thm (th,net) = |
|
16800 | 71 |
Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net |
0 | 72 |
handle Net.INSERT => net; |
73 |
||
74 |
(*match subgoal i against possible theorems in the net. |
|
75 |
Similar to match_from_nat_tac, but the net does not contain numbers; |
|
76 |
rewrite rules are not ordered.*) |
|
77 |
fun net_tac net = |
|
78 |
SUBGOAL(fn (prem,i) => |
|
19805 | 79 |
resolve_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i); |
0 | 80 |
|
81 |
(*match subgoal i against possible theorems indexed by lhs in the net*) |
|
82 |
fun lhs_net_tac net = |
|
83 |
SUBGOAL(fn (prem,i) => |
|
1459 | 84 |
biresolve_tac (Net.unify_term net |
19805 | 85 |
(lhs_of (Logic.strip_assums_concl prem))) i); |
0 | 86 |
|
15570 | 87 |
fun nth_subgoal i thm = List.nth(prems_of thm,i-1); |
0 | 88 |
|
19805 | 89 |
fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm); |
0 | 90 |
|
91 |
fun lhs_of_eq i thm = lhs_of(goal_concl i thm) |
|
92 |
and rhs_of_eq i thm = rhs_of(goal_concl i thm); |
|
93 |
||
94 |
fun var_lhs(thm,i) = |
|
95 |
let fun var(Var _) = true |
|
96 |
| var(Abs(_,_,t)) = var t |
|
97 |
| var(f$_) = var f |
|
98 |
| var _ = false; |
|
99 |
in var(lhs_of_eq i thm) end; |
|
100 |
||
101 |
fun contains_op opns = |
|
102 |
let fun contains(Const(s,_)) = s mem opns | |
|
103 |
contains(s$t) = contains s orelse contains t | |
|
104 |
contains(Abs(_,_,t)) = contains t | |
|
105 |
contains _ = false; |
|
106 |
in contains end; |
|
107 |
||
108 |
fun may_match(match_ops,i) = contains_op match_ops o lhs_of_eq i; |
|
109 |
||
110 |
val (normI_thms,normE_thms) = split_list norm_thms; |
|
111 |
||
112 |
(*Get the norm constants from norm_thms*) |
|
113 |
val norms = |
|
114 |
let fun norm thm = |
|
115 |
case lhs_of(concl_of thm) of |
|
1459 | 116 |
Const(n,_)$_ => n |
26928 | 117 |
| _ => (Display.prths normE_thms; error"No constant in lhs of a norm_thm") |
0 | 118 |
in map norm normE_thms end; |
119 |
||
120 |
fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of |
|
1459 | 121 |
Const(s,_)$_ => s mem norms | _ => false; |
0 | 122 |
|
123 |
val refl_tac = resolve_tac refl_thms; |
|
124 |
||
125 |
fun find_res thms thm = |
|
26928 | 126 |
let fun find [] = (Display.prths thms; error"Check Simp_Data") |
6969 | 127 |
| find(th::thms) = thm RS th handle THM _ => find thms |
0 | 128 |
in find thms end; |
129 |
||
130 |
val mk_trans = find_res trans_thms; |
|
131 |
||
132 |
fun mk_trans2 thm = |
|
133 |
let fun mk[] = error"Check transitivity" |
|
6969 | 134 |
| mk(t::ts) = (thm RSN (2,t)) handle THM _ => mk ts |
0 | 135 |
in mk trans_thms end; |
136 |
||
137 |
(*Applies tactic and returns the first resulting state, FAILS if none!*) |
|
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
138 |
fun one_result(tac,thm) = case Seq.pull(tac thm) of |
15531 | 139 |
SOME(thm',_) => thm' |
140 |
| NONE => raise THM("Simplifier: could not continue", 0, [thm]); |
|
0 | 141 |
|
142 |
fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm); |
|
143 |
||
144 |
||
145 |
(**** Adding "NORM" tags ****) |
|
146 |
||
147 |
(*get name of the constant from conclusion of a congruence rule*) |
|
148 |
fun cong_const cong = |
|
149 |
case head_of (lhs_of (concl_of cong)) of |
|
1459 | 150 |
Const(c,_) => c |
151 |
| _ => "" (*a placeholder distinct from const names*); |
|
0 | 152 |
|
153 |
(*true if the term is an atomic proposition (no ==> signs) *) |
|
19805 | 154 |
val atomic = null o Logic.strip_assums_hyp; |
0 | 155 |
|
156 |
(*ccs contains the names of the constants possessing congruence rules*) |
|
157 |
fun add_hidden_vars ccs = |
|
21078 | 158 |
let fun add_hvars tm hvars = case tm of |
1459 | 159 |
Abs(_,_,body) => add_term_vars(body,hvars) |
160 |
| _$_ => let val (f,args) = strip_comb tm |
|
161 |
in case f of |
|
162 |
Const(c,T) => |
|
21078 | 163 |
if member (op =) ccs c |
164 |
then fold_rev add_hvars args hvars |
|
165 |
else add_term_vars (tm, hvars) |
|
166 |
| _ => add_term_vars (tm, hvars) |
|
1459 | 167 |
end |
168 |
| _ => hvars; |
|
0 | 169 |
in add_hvars end; |
170 |
||
171 |
fun add_new_asm_vars new_asms = |
|
21078 | 172 |
let fun itf (tm, at) vars = |
1459 | 173 |
if at then vars else add_term_vars(tm,vars) |
174 |
fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm |
|
175 |
in if length(tml)=length(al) |
|
21078 | 176 |
then fold_rev itf (tml ~~ al) vars |
1459 | 177 |
else vars |
178 |
end |
|
179 |
fun add_vars (tm,vars) = case tm of |
|
180 |
Abs (_,_,body) => add_vars(body,vars) |
|
181 |
| r$s => (case head_of tm of |
|
17325 | 182 |
Const(c,T) => (case AList.lookup (op =) new_asms c of |
15531 | 183 |
NONE => add_vars(r,add_vars(s,vars)) |
184 |
| SOME(al) => add_list(tm,al,vars)) |
|
1459 | 185 |
| _ => add_vars(r,add_vars(s,vars))) |
186 |
| _ => vars |
|
0 | 187 |
in add_vars end; |
188 |
||
189 |
||
190 |
fun add_norms(congs,ccs,new_asms) thm = |
|
191 |
let val thm' = mk_trans2 thm; |
|
192 |
(* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *) |
|
193 |
val nops = nprems_of thm' |
|
194 |
val lhs = rhs_of_eq 1 thm' |
|
195 |
val rhs = lhs_of_eq nops thm' |
|
196 |
val asms = tl(rev(tl(prems_of thm'))) |
|
21078 | 197 |
val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) [] |
0 | 198 |
val hvars = add_new_asm_vars new_asms (rhs,hvars) |
21078 | 199 |
fun it_asms asm hvars = |
1459 | 200 |
if atomic asm then add_new_asm_vars new_asms (asm,hvars) |
201 |
else add_term_frees(asm,hvars) |
|
21078 | 202 |
val hvars = fold_rev it_asms asms hvars |
0 | 203 |
val hvs = map (#1 o dest_Var) hvars |
204 |
val refl1_tac = refl_tac 1 |
|
3537 | 205 |
fun norm_step_tac st = st |> |
206 |
(case head_of(rhs_of_eq 1 st) of |
|
207 |
Var(ixn,_) => if ixn mem hvs then refl1_tac |
|
208 |
else resolve_tac normI_thms 1 ORELSE refl1_tac |
|
209 |
| Const _ => resolve_tac normI_thms 1 ORELSE |
|
210 |
resolve_tac congs 1 ORELSE refl1_tac |
|
211 |
| Free _ => resolve_tac congs 1 ORELSE refl1_tac |
|
212 |
| _ => refl1_tac) |
|
213 |
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac |
|
15531 | 214 |
val SOME(thm'',_) = Seq.pull(add_norm_tac thm') |
0 | 215 |
in thm'' end; |
216 |
||
217 |
fun add_norm_tags congs = |
|
218 |
let val ccs = map cong_const congs |
|
15570 | 219 |
val new_asms = List.filter (exists not o #2) |
1459 | 220 |
(ccs ~~ (map (map atomic o prems_of) congs)); |
0 | 221 |
in add_norms(congs,ccs,new_asms) end; |
222 |
||
223 |
fun normed_rews congs = |
|
19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19876
diff
changeset
|
224 |
let val add_norms = add_norm_tags congs in |
21287 | 225 |
fn thm => Variable.tradeT |
226 |
(K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.thm_context thm) [thm] |
|
0 | 227 |
end; |
228 |
||
1459 | 229 |
fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; |
0 | 230 |
|
231 |
val trans_norms = map mk_trans normE_thms; |
|
232 |
||
233 |
||
234 |
(* SIMPSET *) |
|
235 |
||
236 |
datatype simpset = |
|
1459 | 237 |
SS of {auto_tac: int -> tactic, |
238 |
congs: thm list, |
|
239 |
cong_net: thm Net.net, |
|
240 |
mk_simps: thm -> thm list, |
|
241 |
simps: (thm * thm list) list, |
|
242 |
simp_net: thm Net.net} |
|
0 | 243 |
|
244 |
val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty, |
|
1459 | 245 |
mk_simps=normed_rews[], simps=[], simp_net=Net.empty}; |
0 | 246 |
|
247 |
(** Insertion of congruences and rewrites **) |
|
248 |
||
249 |
(*insert a thm in a thm net*) |
|
21078 | 250 |
fun insert_thm_warn th net = |
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21287
diff
changeset
|
251 |
Net.insert_term Thm.eq_thm_prop (concl_of th, th) net |
0 | 252 |
handle Net.INSERT => |
26928 | 253 |
(writeln"\nDuplicate rewrite or congruence rule:"; Display.print_thm th; |
0 | 254 |
net); |
255 |
||
21078 | 256 |
val insert_thms = fold_rev insert_thm_warn; |
0 | 257 |
|
258 |
fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) = |
|
259 |
let val thms = mk_simps thm |
|
260 |
in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, |
|
21078 | 261 |
simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net} |
0 | 262 |
end; |
263 |
||
15570 | 264 |
val op addrews = Library.foldl addrew; |
0 | 265 |
|
266 |
fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = |
|
267 |
let val congs' = thms @ congs; |
|
268 |
in SS{auto_tac=auto_tac, congs= congs', |
|
21078 | 269 |
cong_net= insert_thms (map mk_trans thms) cong_net, |
0 | 270 |
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} |
271 |
end; |
|
272 |
||
273 |
(** Deletion of congruences and rewrites **) |
|
274 |
||
275 |
(*delete a thm from a thm net*) |
|
21078 | 276 |
fun delete_thm_warn th net = |
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21287
diff
changeset
|
277 |
Net.delete_term Thm.eq_thm_prop (concl_of th, th) net |
0 | 278 |
handle Net.DELETE => |
26928 | 279 |
(writeln"\nNo such rewrite or congruence rule:"; Display.print_thm th; |
0 | 280 |
net); |
281 |
||
21078 | 282 |
val delete_thms = fold_rev delete_thm_warn; |
0 | 283 |
|
284 |
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = |
|
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21287
diff
changeset
|
285 |
let val congs' = fold (remove Thm.eq_thm_prop) thms congs |
0 | 286 |
in SS{auto_tac=auto_tac, congs= congs', |
21078 | 287 |
cong_net= delete_thms (map mk_trans thms) cong_net, |
0 | 288 |
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} |
289 |
end; |
|
290 |
||
291 |
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) = |
|
292 |
let fun find((p as (th,ths))::ps',ps) = |
|
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21287
diff
changeset
|
293 |
if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) |
0 | 294 |
| find([],simps') = (writeln"\nNo such rewrite or congruence rule:"; |
26928 | 295 |
Display.print_thm thm; |
1459 | 296 |
([],simps')) |
0 | 297 |
val (thms,simps') = find(simps,[]) |
298 |
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, |
|
21078 | 299 |
simps = simps', simp_net = delete_thms thms simp_net } |
0 | 300 |
end; |
301 |
||
15570 | 302 |
val op delrews = Library.foldl delrew; |
0 | 303 |
|
304 |
||
305 |
fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) = |
|
306 |
SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, |
|
307 |
simps=simps, simp_net=simp_net}; |
|
308 |
||
309 |
||
310 |
(** Inspection of a simpset **) |
|
311 |
||
312 |
fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps); |
|
313 |
||
314 |
fun print_ss(SS{congs,simps,...}) = |
|
26928 | 315 |
(writeln"Congruences:"; Display.prths congs; |
316 |
writeln"Rewrite Rules:"; Display.prths (map #1 simps); ()); |
|
0 | 317 |
|
318 |
||
319 |
(* Rewriting with conditionals *) |
|
320 |
||
321 |
val (case_thms,case_consts) = split_list case_splits; |
|
322 |
val case_rews = map mk_trans case_thms; |
|
323 |
||
324 |
fun if_rewritable ifc i thm = |
|
325 |
let val tm = goal_concl i thm |
|
1459 | 326 |
fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1) |
327 |
| nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k) |
|
328 |
| nobound(Bound n,j,k) = n < k orelse k+j <= n |
|
329 |
| nobound(_) = true; |
|
330 |
fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al |
|
331 |
fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1) |
|
332 |
| find_if(tm as s$t,j) = let val (f,al) = strip_comb tm in |
|
333 |
case f of Const(c,_) => if c=ifc then check_args(al,j) |
|
334 |
else find_if(s,j) orelse find_if(t,j) |
|
335 |
| _ => find_if(s,j) orelse find_if(t,j) end |
|
336 |
| find_if(_) = false; |
|
0 | 337 |
in find_if(tm,0) end; |
338 |
||
339 |
fun IF1_TAC cong_tac i = |
|
1512 | 340 |
let fun seq_try (ifth::ifths,ifc::ifcs) thm = |
341 |
(COND (if_rewritable ifc i) (DETERM(rtac ifth i)) |
|
342 |
(seq_try(ifths,ifcs))) thm |
|
343 |
| seq_try([],_) thm = no_tac thm |
|
344 |
and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm |
|
1459 | 345 |
and one_subt thm = |
346 |
let val test = has_fewer_prems (nprems_of thm + 1) |
|
1512 | 347 |
fun loop thm = |
348 |
COND test no_tac |
|
349 |
((try_rew THEN DEPTH_FIRST test (refl_tac i)) |
|
350 |
ORELSE (refl_tac i THEN loop)) thm |
|
351 |
in (cong_tac THEN loop) thm end |
|
352 |
in COND (may_match(case_consts,i)) try_rew no_tac end; |
|
0 | 353 |
|
354 |
fun CASE_TAC (SS{cong_net,...}) i = |
|
355 |
let val cong_tac = net_tac cong_net i |
|
356 |
in NORM (IF1_TAC cong_tac) i end; |
|
357 |
||
358 |
(* Rewriting Automaton *) |
|
359 |
||
360 |
datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE |
|
1459 | 361 |
| PROVE | POP_CS | POP_ARTR | IF; |
22578 | 362 |
|
0 | 363 |
fun simp_refl([],_,ss) = ss |
364 |
| simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss) |
|
1459 | 365 |
else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss); |
0 | 366 |
|
367 |
(** Tracing **) |
|
368 |
||
369 |
val tracing = ref false; |
|
370 |
||
371 |
(*Replace parameters by Free variables in P*) |
|
372 |
fun variants_abs ([],P) = P |
|
373 |
| variants_abs ((a,T)::aTs, P) = |
|
20194 | 374 |
variants_abs (aTs, #2 (Syntax.variant_abs(a,T,P))); |
0 | 375 |
|
376 |
(*Select subgoal i from proof state; substitute parameters, for printing*) |
|
377 |
fun prepare_goal i st = |
|
378 |
let val subgi = nth_subgoal i st |
|
19805 | 379 |
val params = rev (Logic.strip_params subgi) |
380 |
in variants_abs (params, Logic.strip_assums_concl subgi) end; |
|
0 | 381 |
|
382 |
(*print lhs of conclusion of subgoal i*) |
|
383 |
fun pr_goal_lhs i st = |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26928
diff
changeset
|
384 |
writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) |
1459 | 385 |
(lhs_of (prepare_goal i st))); |
0 | 386 |
|
387 |
(*print conclusion of subgoal i*) |
|
388 |
fun pr_goal_concl i st = |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26928
diff
changeset
|
389 |
writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st)) |
0 | 390 |
|
391 |
(*print subgoals i to j (inclusive)*) |
|
392 |
fun pr_goals (i,j) st = |
|
393 |
if i>j then () |
|
394 |
else (pr_goal_concl i st; pr_goals (i+1,j) st); |
|
395 |
||
396 |
(*Print rewrite for tracing; i=subgoal#, n=number of new subgoals, |
|
397 |
thm=old state, thm'=new state *) |
|
398 |
fun pr_rew (i,n,thm,thm',not_asms) = |
|
399 |
if !tracing |
|
400 |
then (if not_asms then () else writeln"Assumption used in"; |
|
401 |
pr_goal_lhs i thm; writeln"->"; pr_goal_lhs (i+n) thm'; |
|
1459 | 402 |
if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm') |
0 | 403 |
else (); |
404 |
writeln"" ) |
|
405 |
else (); |
|
406 |
||
407 |
(* Skip the first n hyps of a goal, and return the rest in generalized form *) |
|
408 |
fun strip_varify(Const("==>", _) $ H $ B, n, vs) = |
|
1459 | 409 |
if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs) |
410 |
else strip_varify(B,n-1,vs) |
|
0 | 411 |
| strip_varify(Const("all",_)$Abs(_,T,t), n, vs) = |
1459 | 412 |
strip_varify(t,n,Var(("?",length vs),T)::vs) |
0 | 413 |
| strip_varify _ = []; |
414 |
||
415 |
fun execute(ss,if_fl,auto_tac,cong_tac,net,i,thm) = let |
|
416 |
||
417 |
fun simp_lhs(thm,ss,anet,ats,cs) = |
|
418 |
if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else |
|
419 |
if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs) |
|
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
420 |
else case Seq.pull(cong_tac i thm) of |
15531 | 421 |
SOME(thm',_) => |
1459 | 422 |
let val ps = prems_of thm and ps' = prems_of thm'; |
423 |
val n = length(ps')-length(ps); |
|
19805 | 424 |
val a = length(Logic.strip_assums_hyp(List.nth(ps,i-1))) |
425 |
val l = map (fn p => length(Logic.strip_assums_hyp(p))) |
|
15570 | 426 |
(Library.take(n,Library.drop(i-1,ps'))); |
1459 | 427 |
in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end |
15531 | 428 |
| NONE => (REW::ss,thm,anet,ats,cs); |
0 | 429 |
|
430 |
(*NB: the "Adding rewrites:" trace will look strange because assumptions |
|
431 |
are represented by rules, generalized over their parameters*) |
|
432 |
fun add_asms(ss,thm,a,anet,ats,cs) = |
|
433 |
let val As = strip_varify(nth_subgoal i thm, a, []); |
|
22596 | 434 |
val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As; |
15570 | 435 |
val new_rws = List.concat(map mk_rew_rules thms); |
436 |
val rwrls = map mk_trans (List.concat(map mk_rew_rules thms)); |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
437 |
val anet' = foldr lhs_insert_thm anet rwrls |
0 | 438 |
in if !tracing andalso not(null new_rws) |
26928 | 439 |
then (writeln"Adding rewrites:"; Display.prths new_rws; ()) |
1459 | 440 |
else (); |
441 |
(ss,thm,anet',anet::ats,cs) |
|
0 | 442 |
end; |
443 |
||
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
444 |
fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of |
15531 | 445 |
SOME(thm',seq') => |
1459 | 446 |
let val n = (nprems_of thm') - (nprems_of thm) |
447 |
in pr_rew(i,n,thm,thm',more); |
|
448 |
if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) |
|
449 |
else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), |
|
450 |
thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) |
|
451 |
end |
|
15531 | 452 |
| NONE => if more |
1512 | 453 |
then rew((lhs_net_tac anet i THEN assume_tac i) thm, |
1459 | 454 |
thm,ss,anet,ats,cs,false) |
455 |
else (ss,thm,anet,ats,cs); |
|
0 | 456 |
|
457 |
fun try_true(thm,ss,anet,ats,cs) = |
|
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
458 |
case Seq.pull(auto_tac i thm) of |
15531 | 459 |
SOME(thm',_) => (ss,thm',anet,ats,cs) |
460 |
| NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs |
|
1459 | 461 |
in if !tracing |
462 |
then (writeln"*** Failed to prove precondition. Normal form:"; |
|
463 |
pr_goal_concl i thm; writeln"") |
|
464 |
else (); |
|
465 |
rew(seq,thm0,ss0,anet0,ats0,cs0,more) |
|
466 |
end; |
|
0 | 467 |
|
468 |
fun if_exp(thm,ss,anet,ats,cs) = |
|
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
469 |
case Seq.pull (IF1_TAC (cong_tac i) i thm) of |
15531 | 470 |
SOME(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs) |
471 |
| NONE => (ss,thm,anet,ats,cs); |
|
0 | 472 |
|
473 |
fun step(s::ss, thm, anet, ats, cs) = case s of |
|
1459 | 474 |
MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs) |
475 |
| ASMS(a) => add_asms(ss,thm,a,anet,ats,cs) |
|
476 |
| SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs) |
|
1512 | 477 |
| REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true) |
1459 | 478 |
| REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs) |
479 |
| TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs) |
|
480 |
| PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss |
|
481 |
else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs) |
|
482 |
| POP_ARTR => (ss,thm,hd ats,tl ats,cs) |
|
483 |
| POP_CS => (ss,thm,anet,ats,tl cs) |
|
484 |
| IF => if_exp(thm,ss,anet,ats,cs); |
|
0 | 485 |
|
486 |
fun exec(state as (s::ss, thm, _, _, _)) = |
|
1459 | 487 |
if s=STOP then thm else exec(step(state)); |
0 | 488 |
|
489 |
in exec(ss, thm, Net.empty, [], []) end; |
|
490 |
||
491 |
||
492 |
fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = |
|
493 |
let val cong_tac = net_tac cong_net |
|
1512 | 494 |
in fn i => |
495 |
(fn thm => |
|
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
496 |
if i <= 0 orelse nprems_of thm < i then Seq.empty |
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
497 |
else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm))) |
1512 | 498 |
THEN TRY(auto_tac i) |
0 | 499 |
end; |
500 |
||
501 |
val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false); |
|
502 |
val SIMP_CASE_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],false); |
|
503 |
||
504 |
val ASM_SIMP_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false); |
|
505 |
val ASM_SIMP_CASE_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false); |
|
506 |
||
507 |
val SIMP_CASE2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],true); |
|
508 |
||
509 |
fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = |
|
510 |
let val cong_tac = net_tac cong_net |
|
511 |
in fn thm => let val state = thm RSN (2,red1) |
|
1459 | 512 |
in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end |
0 | 513 |
end; |
514 |
||
515 |
val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false); |
|
516 |
||
517 |
||
518 |
(* Compute Congruence rules for individual constants using the substition |
|
519 |
rules *) |
|
520 |
||
521 |
val subst_thms = map standard subst_thms; |
|
522 |
||
523 |
||
524 |
fun exp_app(0,t) = t |
|
525 |
| exp_app(i,t) = exp_app(i-1,t $ Bound (i-1)); |
|
526 |
||
527 |
fun exp_abs(Type("fun",[T1,T2]),t,i) = |
|
1459 | 528 |
Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1)) |
0 | 529 |
| exp_abs(T,t,i) = exp_app(i,t); |
530 |
||
531 |
fun eta_Var(ixn,T) = exp_abs(T,Var(ixn,T),0); |
|
532 |
||
533 |
||
534 |
fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) = |
|
535 |
let fun xn_list(x,n) = |
|
1459 | 536 |
let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n); |
15570 | 537 |
in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end |
0 | 538 |
val lhs = list_comb(f,xn_list("X",k-1)) |
539 |
val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) |
|
540 |
in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; |
|
541 |
||
16931 | 542 |
fun find_subst sg T = |
0 | 543 |
let fun find (thm::thms) = |
1459 | 544 |
let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm)); |
545 |
val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb] |
|
546 |
val eqT::_ = binder_types cT |
|
16931 | 547 |
in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P) |
1459 | 548 |
else find thms |
549 |
end |
|
15531 | 550 |
| find [] = NONE |
0 | 551 |
in find subst_thms end; |
552 |
||
553 |
fun mk_cong sg (f,aTs,rT) (refl,eq) = |
|
16931 | 554 |
let val k = length aTs; |
0 | 555 |
fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) = |
1459 | 556 |
let val ca = cterm_of sg va |
557 |
and cx = cterm_of sg (eta_Var(("X"^si,0),T)) |
|
558 |
val cb = cterm_of sg vb |
|
559 |
and cy = cterm_of sg (eta_Var(("Y"^si,0),T)) |
|
560 |
val cP = cterm_of sg P |
|
561 |
and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs)) |
|
562 |
in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end; |
|
0 | 563 |
fun mk(c,T::Ts,i,yik) = |
1459 | 564 |
let val si = radixstring(26,"a",i) |
16931 | 565 |
in case find_subst sg T of |
15531 | 566 |
NONE => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik) |
567 |
| SOME s => let val c' = c RSN (2,ri(s,i,si,T,yik)) |
|
1459 | 568 |
in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end |
569 |
end |
|
0 | 570 |
| mk(c,[],_,_) = c; |
571 |
in mk(refl,rev aTs,k-1,[]) end; |
|
572 |
||
573 |
fun mk_cong_type sg (f,T) = |
|
574 |
let val (aTs,rT) = strip_type T; |
|
575 |
fun find_refl(r::rs) = |
|
1459 | 576 |
let val (Const(eq,eqT),_,_) = dest_red(concl_of r) |
16931 | 577 |
in if Sign.typ_instance sg (rT, hd(binder_types eqT)) |
15531 | 578 |
then SOME(r,(eq,body_type eqT)) else find_refl rs |
1459 | 579 |
end |
15531 | 580 |
| find_refl([]) = NONE; |
0 | 581 |
in case find_refl refl_thms of |
15531 | 582 |
NONE => [] | SOME(refl) => [mk_cong sg (f,aTs,rT) refl] |
0 | 583 |
end; |
584 |
||
585 |
fun mk_cong_thy thy f = |
|
22578 | 586 |
let val T = case Sign.const_type thy f of |
15531 | 587 |
NONE => error(f^" not declared") | SOME(T) => T; |
16876 | 588 |
val T' = Logic.incr_tvar 9 T; |
22578 | 589 |
in mk_cong_type thy (Const(f,T'),T') end; |
0 | 590 |
|
15570 | 591 |
fun mk_congs thy = List.concat o map (mk_cong_thy thy); |
0 | 592 |
|
593 |
fun mk_typed_congs thy = |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
594 |
let |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
595 |
fun readfT(f,s) = |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
596 |
let |
24707 | 597 |
val T = Logic.incr_tvar 9 (Syntax.read_typ_global thy s); |
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
598 |
val t = case Sign.const_type thy f of |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
599 |
SOME(_) => Const(f,T) | NONE => Free(f,T) |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
600 |
in (t,T) end |
22578 | 601 |
in List.concat o map (mk_cong_type thy o readfT) end; |
0 | 602 |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
603 |
end; |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
604 |
end; |