author | nipkow |
Wed, 09 Jul 2014 11:48:21 +0200 | |
changeset 57537 | 810bc6c41ebd |
parent 56245 | 84fc7dfa3cd4 |
child 58963 | 26bf09b95dda |
permissions | -rw-r--r-- |
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
26939
diff
changeset
|
1 |
(* Title: FOLP/simp.ML |
0 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 1993 University of Cambridge |
|
4 |
||
5 |
FOLP version of... |
|
6 |
||
7 |
Generic simplifier, suitable for most logics. (from Provers) |
|
8 |
||
9 |
This version allows instantiation of Vars in the subgoal, since the proof |
|
10 |
term must change. |
|
11 |
*) |
|
12 |
||
13 |
signature SIMP_DATA = |
|
14 |
sig |
|
15 |
val case_splits : (thm * string) list |
|
16 |
val dest_red : term -> term * term * term |
|
17 |
val mk_rew_rules : thm -> thm list |
|
18 |
val norm_thms : (thm*thm) list (* [(?x>>norm(?x), norm(?x)>>?x), ...] *) |
|
19 |
val red1 : thm (* ?P>>?Q ==> ?P ==> ?Q *) |
|
20 |
val red2 : thm (* ?P>>?Q ==> ?Q ==> ?P *) |
|
21 |
val refl_thms : thm list |
|
22 |
val subst_thms : thm list (* [ ?a>>?b ==> ?P(?a) ==> ?P(?b), ...] *) |
|
23 |
val trans_thms : thm list |
|
24 |
end; |
|
25 |
||
26 |
||
27 |
infix 4 addrews addcongs delrews delcongs setauto; |
|
28 |
||
29 |
signature SIMP = |
|
30 |
sig |
|
31 |
type simpset |
|
32 |
val empty_ss : simpset |
|
33 |
val addcongs : simpset * thm list -> simpset |
|
34 |
val addrews : simpset * thm list -> simpset |
|
35 |
val delcongs : simpset * thm list -> simpset |
|
36 |
val delrews : simpset * thm list -> simpset |
|
37 |
val dest_ss : simpset -> thm list * thm list |
|
38 |
val print_ss : simpset -> unit |
|
39 |
val setauto : simpset * (int -> tactic) -> simpset |
|
40 |
val ASM_SIMP_CASE_TAC : simpset -> int -> tactic |
|
41 |
val ASM_SIMP_TAC : simpset -> int -> tactic |
|
42 |
val CASE_TAC : simpset -> int -> tactic |
|
43 |
val SIMP_CASE2_TAC : simpset -> int -> tactic |
|
44 |
val SIMP_THM : simpset -> thm -> thm |
|
45 |
val SIMP_TAC : simpset -> int -> tactic |
|
46 |
val SIMP_CASE_TAC : simpset -> int -> tactic |
|
47 |
val mk_congs : theory -> string list -> thm list |
|
48 |
val mk_typed_congs : theory -> (string * string) list -> thm list |
|
49 |
(* temporarily disabled: |
|
50 |
val extract_free_congs : unit -> thm list |
|
51 |
*) |
|
32740 | 52 |
val tracing : bool Unsynchronized.ref |
0 | 53 |
end; |
54 |
||
32449 | 55 |
functor SimpFun (Simp_data: SIMP_DATA) : SIMP = |
0 | 56 |
struct |
57 |
||
19805 | 58 |
local open Simp_data in |
0 | 59 |
|
60 |
(*For taking apart reductions into left, right hand sides*) |
|
61 |
val lhs_of = #2 o dest_red; |
|
62 |
val rhs_of = #3 o dest_red; |
|
63 |
||
64 |
(*** Indexing and filtering of theorems ***) |
|
65 |
||
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
21287
diff
changeset
|
66 |
fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2); |
0 | 67 |
|
68 |
(*insert a thm in a discrimination net by its lhs*) |
|
33339 | 69 |
fun lhs_insert_thm th net = |
16800 | 70 |
Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net |
0 | 71 |
handle Net.INSERT => net; |
72 |
||
73 |
(*match subgoal i against possible theorems in the net. |
|
74 |
Similar to match_from_nat_tac, but the net does not contain numbers; |
|
75 |
rewrite rules are not ordered.*) |
|
76 |
fun net_tac net = |
|
32449 | 77 |
SUBGOAL(fn (prem,i) => |
19805 | 78 |
resolve_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i); |
0 | 79 |
|
80 |
(*match subgoal i against possible theorems indexed by lhs in the net*) |
|
81 |
fun lhs_net_tac net = |
|
32449 | 82 |
SUBGOAL(fn (prem,i) => |
1459 | 83 |
biresolve_tac (Net.unify_term net |
19805 | 84 |
(lhs_of (Logic.strip_assums_concl prem))) i); |
0 | 85 |
|
42364 | 86 |
fun nth_subgoal i thm = nth (prems_of thm) (i - 1); |
0 | 87 |
|
19805 | 88 |
fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm); |
0 | 89 |
|
90 |
fun lhs_of_eq i thm = lhs_of(goal_concl i thm) |
|
91 |
and rhs_of_eq i thm = rhs_of(goal_concl i thm); |
|
92 |
||
93 |
fun var_lhs(thm,i) = |
|
94 |
let fun var(Var _) = true |
|
95 |
| var(Abs(_,_,t)) = var t |
|
96 |
| var(f$_) = var f |
|
97 |
| var _ = false; |
|
98 |
in var(lhs_of_eq i thm) end; |
|
99 |
||
100 |
fun contains_op opns = |
|
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36603
diff
changeset
|
101 |
let fun contains(Const(s,_)) = member (op =) opns s | |
0 | 102 |
contains(s$t) = contains s orelse contains t | |
103 |
contains(Abs(_,_,t)) = contains t | |
|
104 |
contains _ = false; |
|
105 |
in contains end; |
|
106 |
||
107 |
fun may_match(match_ops,i) = contains_op match_ops o lhs_of_eq i; |
|
108 |
||
109 |
val (normI_thms,normE_thms) = split_list norm_thms; |
|
110 |
||
111 |
(*Get the norm constants from norm_thms*) |
|
112 |
val norms = |
|
32449 | 113 |
let fun norm thm = |
0 | 114 |
case lhs_of(concl_of thm) of |
1459 | 115 |
Const(n,_)$_ => n |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
116 |
| _ => error "No constant in lhs of a norm_thm" |
0 | 117 |
in map norm normE_thms end; |
118 |
||
119 |
fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of |
|
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36603
diff
changeset
|
120 |
Const(s,_)$_ => member (op =) norms s | _ => false; |
0 | 121 |
|
122 |
val refl_tac = resolve_tac refl_thms; |
|
123 |
||
124 |
fun find_res thms thm = |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
125 |
let fun find [] = error "Check Simp_Data" |
6969 | 126 |
| find(th::thms) = thm RS th handle THM _ => find thms |
0 | 127 |
in find thms end; |
128 |
||
129 |
val mk_trans = find_res trans_thms; |
|
130 |
||
131 |
fun mk_trans2 thm = |
|
132 |
let fun mk[] = error"Check transitivity" |
|
6969 | 133 |
| mk(t::ts) = (thm RSN (2,t)) handle THM _ => mk ts |
0 | 134 |
in mk trans_thms end; |
135 |
||
136 |
(*Applies tactic and returns the first resulting state, FAILS if none!*) |
|
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
137 |
fun one_result(tac,thm) = case Seq.pull(tac thm) of |
15531 | 138 |
SOME(thm',_) => thm' |
139 |
| NONE => raise THM("Simplifier: could not continue", 0, [thm]); |
|
0 | 140 |
|
141 |
fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm); |
|
142 |
||
143 |
||
144 |
(**** Adding "NORM" tags ****) |
|
145 |
||
146 |
(*get name of the constant from conclusion of a congruence rule*) |
|
32449 | 147 |
fun cong_const cong = |
0 | 148 |
case head_of (lhs_of (concl_of cong)) of |
1459 | 149 |
Const(c,_) => c |
150 |
| _ => "" (*a placeholder distinct from const names*); |
|
0 | 151 |
|
152 |
(*true if the term is an atomic proposition (no ==> signs) *) |
|
19805 | 153 |
val atomic = null o Logic.strip_assums_hyp; |
0 | 154 |
|
155 |
(*ccs contains the names of the constants possessing congruence rules*) |
|
156 |
fun add_hidden_vars ccs = |
|
21078 | 157 |
let fun add_hvars tm hvars = case tm of |
44121 | 158 |
Abs(_,_,body) => Misc_Legacy.add_term_vars(body,hvars) |
32449 | 159 |
| _$_ => let val (f,args) = strip_comb tm |
1459 | 160 |
in case f of |
32449 | 161 |
Const(c,T) => |
21078 | 162 |
if member (op =) ccs c |
163 |
then fold_rev add_hvars args hvars |
|
44121 | 164 |
else Misc_Legacy.add_term_vars (tm, hvars) |
165 |
| _ => Misc_Legacy.add_term_vars (tm, hvars) |
|
1459 | 166 |
end |
167 |
| _ => hvars; |
|
0 | 168 |
in add_hvars end; |
169 |
||
170 |
fun add_new_asm_vars new_asms = |
|
21078 | 171 |
let fun itf (tm, at) vars = |
44121 | 172 |
if at then vars else Misc_Legacy.add_term_vars(tm,vars) |
1459 | 173 |
fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm |
174 |
in if length(tml)=length(al) |
|
21078 | 175 |
then fold_rev itf (tml ~~ al) vars |
1459 | 176 |
else vars |
177 |
end |
|
178 |
fun add_vars (tm,vars) = case tm of |
|
179 |
Abs (_,_,body) => add_vars(body,vars) |
|
180 |
| r$s => (case head_of tm of |
|
17325 | 181 |
Const(c,T) => (case AList.lookup (op =) new_asms c of |
15531 | 182 |
NONE => add_vars(r,add_vars(s,vars)) |
183 |
| SOME(al) => add_list(tm,al,vars)) |
|
1459 | 184 |
| _ => add_vars(r,add_vars(s,vars))) |
185 |
| _ => vars |
|
0 | 186 |
in add_vars end; |
187 |
||
188 |
||
189 |
fun add_norms(congs,ccs,new_asms) thm = |
|
190 |
let val thm' = mk_trans2 thm; |
|
191 |
(* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *) |
|
192 |
val nops = nprems_of thm' |
|
193 |
val lhs = rhs_of_eq 1 thm' |
|
194 |
val rhs = lhs_of_eq nops thm' |
|
195 |
val asms = tl(rev(tl(prems_of thm'))) |
|
21078 | 196 |
val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) [] |
0 | 197 |
val hvars = add_new_asm_vars new_asms (rhs,hvars) |
21078 | 198 |
fun it_asms asm hvars = |
1459 | 199 |
if atomic asm then add_new_asm_vars new_asms (asm,hvars) |
44121 | 200 |
else Misc_Legacy.add_term_frees(asm,hvars) |
21078 | 201 |
val hvars = fold_rev it_asms asms hvars |
0 | 202 |
val hvs = map (#1 o dest_Var) hvars |
203 |
val refl1_tac = refl_tac 1 |
|
3537 | 204 |
fun norm_step_tac st = st |> |
32449 | 205 |
(case head_of(rhs_of_eq 1 st) of |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36603
diff
changeset
|
206 |
Var(ixn,_) => if member (op =) hvs ixn then refl1_tac |
32449 | 207 |
else resolve_tac normI_thms 1 ORELSE refl1_tac |
208 |
| Const _ => resolve_tac normI_thms 1 ORELSE |
|
209 |
resolve_tac congs 1 ORELSE refl1_tac |
|
210 |
| Free _ => resolve_tac congs 1 ORELSE refl1_tac |
|
211 |
| _ => refl1_tac) |
|
3537 | 212 |
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac |
15531 | 213 |
val SOME(thm'',_) = Seq.pull(add_norm_tac thm') |
0 | 214 |
in thm'' end; |
215 |
||
216 |
fun add_norm_tags congs = |
|
217 |
let val ccs = map cong_const congs |
|
33317 | 218 |
val new_asms = filter (exists not o #2) |
1459 | 219 |
(ccs ~~ (map (map atomic o prems_of) congs)); |
0 | 220 |
in add_norms(congs,ccs,new_asms) end; |
221 |
||
222 |
fun normed_rews congs = |
|
19925
3f9341831812
eliminated freeze/varify in favour of Variable.import/export/trade;
wenzelm
parents:
19876
diff
changeset
|
223 |
let val add_norms = add_norm_tags congs in |
21287 | 224 |
fn thm => Variable.tradeT |
36603
d5d6111761a6
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
wenzelm
parents:
35021
diff
changeset
|
225 |
(K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.global_thm_context thm) [thm] |
0 | 226 |
end; |
227 |
||
1459 | 228 |
fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; |
0 | 229 |
|
230 |
val trans_norms = map mk_trans normE_thms; |
|
231 |
||
232 |
||
233 |
(* SIMPSET *) |
|
234 |
||
235 |
datatype simpset = |
|
1459 | 236 |
SS of {auto_tac: int -> tactic, |
237 |
congs: thm list, |
|
238 |
cong_net: thm Net.net, |
|
239 |
mk_simps: thm -> thm list, |
|
240 |
simps: (thm * thm list) list, |
|
241 |
simp_net: thm Net.net} |
|
0 | 242 |
|
243 |
val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty, |
|
1459 | 244 |
mk_simps=normed_rews[], simps=[], simp_net=Net.empty}; |
0 | 245 |
|
246 |
(** Insertion of congruences and rewrites **) |
|
247 |
||
248 |
(*insert a thm in a thm net*) |
|
32449 | 249 |
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
|
250 |
Net.insert_term Thm.eq_thm_prop (concl_of th, th) net |
32449 | 251 |
handle Net.INSERT => |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
252 |
(writeln ("Duplicate rewrite or congruence rule:\n" ^ |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
253 |
Display.string_of_thm_without_context th); net); |
0 | 254 |
|
21078 | 255 |
val insert_thms = fold_rev insert_thm_warn; |
0 | 256 |
|
33245 | 257 |
fun addrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = |
0 | 258 |
let val thms = mk_simps thm |
259 |
in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, |
|
21078 | 260 |
simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net} |
0 | 261 |
end; |
262 |
||
33245 | 263 |
fun ss addrews thms = fold addrew thms ss; |
0 | 264 |
|
265 |
fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = |
|
266 |
let val congs' = thms @ congs; |
|
267 |
in SS{auto_tac=auto_tac, congs= congs', |
|
21078 | 268 |
cong_net= insert_thms (map mk_trans thms) cong_net, |
0 | 269 |
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} |
270 |
end; |
|
271 |
||
272 |
(** Deletion of congruences and rewrites **) |
|
273 |
||
274 |
(*delete a thm from a thm net*) |
|
32449 | 275 |
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
|
276 |
Net.delete_term Thm.eq_thm_prop (concl_of th, th) net |
32449 | 277 |
handle Net.DELETE => |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
278 |
(writeln ("No such rewrite or congruence rule:\n" ^ |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
279 |
Display.string_of_thm_without_context th); net); |
0 | 280 |
|
21078 | 281 |
val delete_thms = fold_rev delete_thm_warn; |
0 | 282 |
|
283 |
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
|
284 |
let val congs' = fold (remove Thm.eq_thm_prop) thms congs |
0 | 285 |
in SS{auto_tac=auto_tac, congs= congs', |
21078 | 286 |
cong_net= delete_thms (map mk_trans thms) cong_net, |
0 | 287 |
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net} |
288 |
end; |
|
289 |
||
33245 | 290 |
fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = |
0 | 291 |
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
|
292 |
if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
293 |
| find([],simps') = |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
294 |
(writeln ("No such rewrite or congruence rule:\n" ^ |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
295 |
Display.string_of_thm_without_context thm); ([], simps')) |
0 | 296 |
val (thms,simps') = find(simps,[]) |
297 |
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, |
|
21078 | 298 |
simps = simps', simp_net = delete_thms thms simp_net } |
0 | 299 |
end; |
300 |
||
33245 | 301 |
fun ss delrews thms = fold delrew thms ss; |
0 | 302 |
|
303 |
||
304 |
fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) = |
|
305 |
SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, |
|
306 |
simps=simps, simp_net=simp_net}; |
|
307 |
||
308 |
||
309 |
(** Inspection of a simpset **) |
|
310 |
||
311 |
fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps); |
|
312 |
||
313 |
fun print_ss(SS{congs,simps,...}) = |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
314 |
writeln (cat_lines |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
315 |
(["Congruences:"] @ map Display.string_of_thm_without_context congs @ |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
316 |
["Rewrite Rules:"] @ map (Display.string_of_thm_without_context o #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 = |
|
32449 | 340 |
let fun seq_try (ifth::ifths,ifc::ifcs) thm = |
1512 | 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) |
|
32449 | 347 |
fun loop thm = |
348 |
COND test no_tac |
|
1512 | 349 |
((try_rew THEN DEPTH_FIRST test (refl_tac i)) |
32449 | 350 |
ORELSE (refl_tac i THEN loop)) thm |
1512 | 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 |
||
32740 | 369 |
val tracing = Unsynchronized.ref false; |
0 | 370 |
|
371 |
(*Replace parameters by Free variables in P*) |
|
372 |
fun variants_abs ([],P) = P |
|
373 |
| variants_abs ((a,T)::aTs, P) = |
|
42284 | 374 |
variants_abs (aTs, #2 (Syntax_Trans.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 = |
|
32449 | 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 = |
|
32449 | 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 *) |
|
56245 | 408 |
fun strip_varify(Const(@{const_name Pure.imp}, _) $ 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) |
|
56245 | 411 |
| strip_varify(Const(@{const_name Pure.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',_) => |
33955 | 422 |
let val ps = prems_of thm |
423 |
and ps' = prems_of thm'; |
|
1459 | 424 |
val n = length(ps')-length(ps); |
42364 | 425 |
val a = length(Logic.strip_assums_hyp(nth ps (i - 1))) |
33955 | 426 |
val l = map (length o Logic.strip_assums_hyp) (take n (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, []); |
|
36945 | 434 |
val thms = map (Thm.trivial o cterm_of(Thm.theory_of_thm thm)) As; |
32952 | 435 |
val new_rws = maps mk_rew_rules thms; |
436 |
val rwrls = map mk_trans (maps mk_rew_rules thms); |
|
33339 | 437 |
val anet' = fold_rev lhs_insert_thm rwrls anet; |
0 | 438 |
in if !tracing andalso not(null new_rws) |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
439 |
then writeln (cat_lines |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
30190
diff
changeset
|
440 |
("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws)) |
1459 | 441 |
else (); |
32449 | 442 |
(ss,thm,anet',anet::ats,cs) |
0 | 443 |
end; |
444 |
||
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
445 |
fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of |
15531 | 446 |
SOME(thm',seq') => |
1459 | 447 |
let val n = (nprems_of thm') - (nprems_of thm) |
448 |
in pr_rew(i,n,thm,thm',more); |
|
449 |
if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) |
|
450 |
else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), |
|
451 |
thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) |
|
452 |
end |
|
15531 | 453 |
| NONE => if more |
1512 | 454 |
then rew((lhs_net_tac anet i THEN assume_tac i) thm, |
1459 | 455 |
thm,ss,anet,ats,cs,false) |
456 |
else (ss,thm,anet,ats,cs); |
|
0 | 457 |
|
458 |
fun try_true(thm,ss,anet,ats,cs) = |
|
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
459 |
case Seq.pull(auto_tac i thm) of |
15531 | 460 |
SOME(thm',_) => (ss,thm',anet,ats,cs) |
461 |
| NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs |
|
1459 | 462 |
in if !tracing |
463 |
then (writeln"*** Failed to prove precondition. Normal form:"; |
|
464 |
pr_goal_concl i thm; writeln"") |
|
465 |
else (); |
|
466 |
rew(seq,thm0,ss0,anet0,ats0,cs0,more) |
|
467 |
end; |
|
0 | 468 |
|
469 |
fun if_exp(thm,ss,anet,ats,cs) = |
|
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
470 |
case Seq.pull (IF1_TAC (cong_tac i) i thm) of |
15531 | 471 |
SOME(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs) |
472 |
| NONE => (ss,thm,anet,ats,cs); |
|
0 | 473 |
|
474 |
fun step(s::ss, thm, anet, ats, cs) = case s of |
|
1459 | 475 |
MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs) |
476 |
| ASMS(a) => add_asms(ss,thm,a,anet,ats,cs) |
|
477 |
| SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs) |
|
1512 | 478 |
| REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true) |
1459 | 479 |
| REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs) |
480 |
| TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs) |
|
481 |
| PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss |
|
482 |
else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs) |
|
483 |
| POP_ARTR => (ss,thm,hd ats,tl ats,cs) |
|
484 |
| POP_CS => (ss,thm,anet,ats,tl cs) |
|
485 |
| IF => if_exp(thm,ss,anet,ats,cs); |
|
0 | 486 |
|
487 |
fun exec(state as (s::ss, thm, _, _, _)) = |
|
1459 | 488 |
if s=STOP then thm else exec(step(state)); |
0 | 489 |
|
490 |
in exec(ss, thm, Net.empty, [], []) end; |
|
491 |
||
492 |
||
493 |
fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = |
|
494 |
let val cong_tac = net_tac cong_net |
|
32449 | 495 |
in fn i => |
1512 | 496 |
(fn thm => |
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
497 |
if i <= 0 orelse nprems_of thm < i then Seq.empty |
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
3537
diff
changeset
|
498 |
else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm))) |
1512 | 499 |
THEN TRY(auto_tac i) |
0 | 500 |
end; |
501 |
||
502 |
val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false); |
|
503 |
val SIMP_CASE_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],false); |
|
504 |
||
505 |
val ASM_SIMP_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false); |
|
506 |
val ASM_SIMP_CASE_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false); |
|
507 |
||
508 |
val SIMP_CASE2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],true); |
|
509 |
||
510 |
fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = |
|
511 |
let val cong_tac = net_tac cong_net |
|
512 |
in fn thm => let val state = thm RSN (2,red1) |
|
1459 | 513 |
in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end |
0 | 514 |
end; |
515 |
||
516 |
val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false); |
|
517 |
||
518 |
||
519 |
(* Compute Congruence rules for individual constants using the substition |
|
520 |
rules *) |
|
521 |
||
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33955
diff
changeset
|
522 |
val subst_thms = map Drule.export_without_context subst_thms; |
0 | 523 |
|
524 |
||
525 |
fun exp_app(0,t) = t |
|
526 |
| exp_app(i,t) = exp_app(i-1,t $ Bound (i-1)); |
|
527 |
||
528 |
fun exp_abs(Type("fun",[T1,T2]),t,i) = |
|
1459 | 529 |
Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1)) |
0 | 530 |
| exp_abs(T,t,i) = exp_app(i,t); |
531 |
||
532 |
fun eta_Var(ixn,T) = exp_abs(T,Var(ixn,T),0); |
|
533 |
||
534 |
||
535 |
fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) = |
|
536 |
let fun xn_list(x,n) = |
|
33063 | 537 |
let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1); |
33955 | 538 |
in ListPair.map eta_Var (ixs, take (n+1) Ts) end |
0 | 539 |
val lhs = list_comb(f,xn_list("X",k-1)) |
540 |
val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik) |
|
541 |
in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end; |
|
542 |
||
16931 | 543 |
fun find_subst sg T = |
0 | 544 |
let fun find (thm::thms) = |
1459 | 545 |
let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm)); |
44121 | 546 |
val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (concl_of thm, [])); |
1459 | 547 |
val eqT::_ = binder_types cT |
16931 | 548 |
in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P) |
1459 | 549 |
else find thms |
550 |
end |
|
15531 | 551 |
| find [] = NONE |
0 | 552 |
in find subst_thms end; |
553 |
||
554 |
fun mk_cong sg (f,aTs,rT) (refl,eq) = |
|
16931 | 555 |
let val k = length aTs; |
0 | 556 |
fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) = |
1459 | 557 |
let val ca = cterm_of sg va |
558 |
and cx = cterm_of sg (eta_Var(("X"^si,0),T)) |
|
559 |
val cb = cterm_of sg vb |
|
560 |
and cy = cterm_of sg (eta_Var(("Y"^si,0),T)) |
|
561 |
val cP = cterm_of sg P |
|
562 |
and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs)) |
|
563 |
in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end; |
|
0 | 564 |
fun mk(c,T::Ts,i,yik) = |
1459 | 565 |
let val si = radixstring(26,"a",i) |
16931 | 566 |
in case find_subst sg T of |
15531 | 567 |
NONE => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik) |
568 |
| SOME s => let val c' = c RSN (2,ri(s,i,si,T,yik)) |
|
1459 | 569 |
in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end |
570 |
end |
|
0 | 571 |
| mk(c,[],_,_) = c; |
572 |
in mk(refl,rev aTs,k-1,[]) end; |
|
573 |
||
574 |
fun mk_cong_type sg (f,T) = |
|
575 |
let val (aTs,rT) = strip_type T; |
|
576 |
fun find_refl(r::rs) = |
|
1459 | 577 |
let val (Const(eq,eqT),_,_) = dest_red(concl_of r) |
16931 | 578 |
in if Sign.typ_instance sg (rT, hd(binder_types eqT)) |
15531 | 579 |
then SOME(r,(eq,body_type eqT)) else find_refl rs |
1459 | 580 |
end |
15531 | 581 |
| find_refl([]) = NONE; |
0 | 582 |
in case find_refl refl_thms of |
15531 | 583 |
NONE => [] | SOME(refl) => [mk_cong sg (f,aTs,rT) refl] |
0 | 584 |
end; |
585 |
||
586 |
fun mk_cong_thy thy f = |
|
22578 | 587 |
let val T = case Sign.const_type thy f of |
15531 | 588 |
NONE => error(f^" not declared") | SOME(T) => T; |
16876 | 589 |
val T' = Logic.incr_tvar 9 T; |
22578 | 590 |
in mk_cong_type thy (Const(f,T'),T') end; |
0 | 591 |
|
32952 | 592 |
fun mk_congs thy = maps (mk_cong_thy thy); |
0 | 593 |
|
594 |
fun mk_typed_congs thy = |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
595 |
let |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
596 |
fun readfT(f,s) = |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
597 |
let |
24707 | 598 |
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
|
599 |
val t = case Sign.const_type thy f of |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
600 |
SOME(_) => Const(f,T) | NONE => Free(f,T) |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
601 |
in (t,T) end |
32952 | 602 |
in maps (mk_cong_type thy o readfT) end; |
0 | 603 |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
604 |
end; |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset
|
605 |
end; |