45 thm foo.size_eqvt |
46 thm foo.size_eqvt |
46 thm foo.supports |
47 thm foo.supports |
47 thm foo.fsupp |
48 thm foo.fsupp |
48 thm foo.supp |
49 thm foo.supp |
49 thm foo.fresh |
50 thm foo.fresh |
|
51 thm foo.size |
50 |
52 |
51 ML {* |
|
52 |
|
53 open Function_Lib |
|
54 |
|
55 type rec_call_info = int * (string * typ) list * term list * term list |
|
56 |
|
57 datatype scheme_case = SchemeCase of |
|
58 {bidx : int, |
|
59 qs: (string * typ) list, |
|
60 oqnames: string list, |
|
61 gs: term list, |
|
62 lhs: term list, |
|
63 rs: rec_call_info list} |
|
64 |
|
65 datatype scheme_branch = SchemeBranch of |
|
66 {P : term, |
|
67 xs: (string * typ) list, |
|
68 ws: (string * typ) list, |
|
69 Cs: term list} |
|
70 |
|
71 datatype ind_scheme = IndScheme of |
|
72 {T: typ, (* sum of products *) |
|
73 branches: scheme_branch list, |
|
74 cases: scheme_case list} |
|
75 |
|
76 val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize} |
|
77 val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify} |
|
78 |
|
79 fun meta thm = thm RS eq_reflection |
|
80 |
|
81 val sum_prod_conv = Raw_Simplifier.rewrite true |
|
82 (map meta (@{thm split_conv} :: @{thms sum.cases})) |
|
83 |
|
84 fun term_conv thy cv t = |
|
85 cv (cterm_of thy t) |
|
86 |> prop_of |> Logic.dest_equals |> snd |
|
87 |
|
88 fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)) |
|
89 |
|
90 fun dest_hhf ctxt t = |
|
91 let |
|
92 val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt |
|
93 in |
|
94 (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) |
|
95 end |
|
96 |
|
97 fun mk_scheme' ctxt cases concl = |
|
98 let |
|
99 fun mk_branch concl = |
|
100 let |
|
101 val _ = tracing ("concl:\n" ^ Syntax.string_of_term ctxt concl) |
|
102 val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl |
|
103 val (P, xs) = strip_comb Pxs |
|
104 val _ = tracing ("xs: " ^ commas (map @{make_string} xs)) |
|
105 val _ = map dest_Free xs |
|
106 val _ = tracing ("done") |
|
107 in |
|
108 SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs } |
|
109 end |
|
110 |
|
111 val (branches, cases') = (* correction *) |
|
112 case Logic.dest_conjunctions concl of |
|
113 [conc] => |
|
114 let |
|
115 val _ $ Pxs = Logic.strip_assums_concl conc |
|
116 val (P, _) = strip_comb Pxs |
|
117 val (cases', conds) = |
|
118 take_prefix (Term.exists_subterm (curry op aconv P)) cases |
|
119 val concl' = fold_rev (curry Logic.mk_implies) conds conc |
|
120 in |
|
121 ([mk_branch concl'], cases') |
|
122 end |
|
123 | concls => (map mk_branch concls, cases) |
|
124 |
|
125 fun mk_case premise = |
|
126 let |
|
127 val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise |
|
128 val (P, lhs) = strip_comb Plhs |
|
129 |
|
130 fun bidx Q = |
|
131 find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches |
|
132 |
|
133 fun mk_rcinfo pr = |
|
134 let |
|
135 val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr |
|
136 val (P', rcs) = strip_comb Phyp |
|
137 in |
|
138 (bidx P', Gvs, Gas, rcs) |
|
139 end |
|
140 |
|
141 fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches |
|
142 |
|
143 val (gs, rcprs) = |
|
144 take_prefix (not o Term.exists_subterm is_pred) prems |
|
145 in |
|
146 SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), |
|
147 gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs} |
|
148 end |
|
149 |
|
150 fun PT_of (SchemeBranch { xs, ...}) = |
|
151 foldr1 HOLogic.mk_prodT (map snd xs) |
|
152 |
|
153 val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches) |
|
154 in |
|
155 IndScheme {T=ST, cases=map mk_case cases', branches=branches } |
|
156 end |
|
157 |
|
158 fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx = |
|
159 let |
|
160 val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx |
|
161 val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases |
|
162 |
|
163 val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] |
|
164 val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) |
|
165 val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs |
|
166 |
|
167 fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = |
|
168 HOLogic.mk_Trueprop Pbool |
|
169 |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l))) |
|
170 (xs' ~~ lhs) |
|
171 |> fold_rev (curry Logic.mk_implies) gs |
|
172 |> fold_rev mk_forall_rename (oqnames ~~ map Free qs) |
|
173 in |
|
174 HOLogic.mk_Trueprop Pbool |
|
175 |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases |
|
176 |> fold_rev (curry Logic.mk_implies) Cs' |
|
177 |> fold_rev (Logic.all o Free) ws |
|
178 |> fold_rev mk_forall_rename (map fst xs ~~ xs') |
|
179 |> mk_forall_rename ("P", Pbool) |
|
180 end |
|
181 |
|
182 fun mk_wf R (IndScheme {T, ...}) = |
|
183 HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R) |
|
184 |
|
185 fun mk_ineqs R (IndScheme {T, cases, branches}) = |
|
186 let |
|
187 fun inject i ts = |
|
188 SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts) |
|
189 |
|
190 val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *) |
|
191 |
|
192 fun mk_pres bdx args = |
|
193 let |
|
194 val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx |
|
195 fun replace (x, v) t = betapply (lambda (Free x) t, v) |
|
196 val Cs' = map (fold replace (xs ~~ args)) Cs |
|
197 val cse = |
|
198 HOLogic.mk_Trueprop thesis |
|
199 |> fold_rev (curry Logic.mk_implies) Cs' |
|
200 |> fold_rev (Logic.all o Free) ws |
|
201 in |
|
202 Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis) |
|
203 end |
|
204 |
|
205 fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = |
|
206 let |
|
207 fun g (bidx', Gvs, Gas, rcarg) = |
|
208 let val export = |
|
209 fold_rev (curry Logic.mk_implies) Gas |
|
210 #> fold_rev (curry Logic.mk_implies) gs |
|
211 #> fold_rev (Logic.all o Free) Gvs |
|
212 #> fold_rev mk_forall_rename (oqnames ~~ map Free qs) |
|
213 in |
|
214 (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R) |
|
215 |> HOLogic.mk_Trueprop |
|
216 |> export, |
|
217 mk_pres bidx' rcarg |
|
218 |> export |
|
219 |> Logic.all thesis) |
|
220 end |
|
221 in |
|
222 map g rs |
|
223 end |
|
224 in |
|
225 map f cases |
|
226 end |
|
227 |
|
228 |
|
229 fun mk_ind_goal thy branches = |
|
230 let |
|
231 fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) = |
|
232 HOLogic.mk_Trueprop (list_comb (P, map Free xs)) |
|
233 |> fold_rev (curry Logic.mk_implies) Cs |
|
234 |> fold_rev (Logic.all o Free) ws |
|
235 |> term_conv thy ind_atomize |
|
236 |> Object_Logic.drop_judgment thy |
|
237 |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs)) |
|
238 in |
|
239 SumTree.mk_sumcases HOLogic.boolT (map brnch branches) |
|
240 end |
|
241 |
|
242 fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss |
|
243 (IndScheme {T, cases=scases, branches}) = |
|
244 let |
|
245 val n = length branches |
|
246 val scases_idx = map_index I scases |
|
247 |
|
248 fun inject i ts = |
|
249 SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts) |
|
250 val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches) |
|
251 |
|
252 val thy = ProofContext.theory_of ctxt |
|
253 val cert = cterm_of thy |
|
254 |
|
255 val P_comp = mk_ind_goal thy branches |
|
256 |
|
257 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
|
258 val ihyp = Term.all T $ Abs ("z", T, |
|
259 Logic.mk_implies |
|
260 (HOLogic.mk_Trueprop ( |
|
261 Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) |
|
262 $ (HOLogic.pair_const T T $ Bound 0 $ x) |
|
263 $ R), |
|
264 HOLogic.mk_Trueprop (P_comp $ Bound 0))) |
|
265 |> cert |
|
266 |
|
267 val aihyp = Thm.assume ihyp |
|
268 |
|
269 (* Rule for case splitting along the sum types *) |
|
270 val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches |
|
271 val pats = map_index (uncurry inject) xss |
|
272 val sum_split_rule = |
|
273 Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats) |
|
274 |
|
275 fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = |
|
276 let |
|
277 val fxs = map Free xs |
|
278 val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) |
|
279 |
|
280 val C_hyps = map (cert #> Thm.assume) Cs |
|
281 |
|
282 val (relevant_cases, ineqss') = |
|
283 (scases_idx ~~ ineqss) |
|
284 |> filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) |
|
285 |> split_list |
|
286 |
|
287 fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press = |
|
288 let |
|
289 val case_hyps = |
|
290 map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs) |
|
291 |
|
292 val cqs = map (cert o Free) qs |
|
293 val ags = map (Thm.assume o cert) gs |
|
294 |
|
295 val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps) |
|
296 val sih = full_simplify replace_x_ss aihyp |
|
297 |
|
298 fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = |
|
299 let |
|
300 val cGas = map (Thm.assume o cert) Gas |
|
301 val cGvs = map (cert o Free) Gvs |
|
302 val import = fold Thm.forall_elim (cqs @ cGvs) |
|
303 #> fold Thm.elim_implies (ags @ cGas) |
|
304 val ipres = pres |
|
305 |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs))) |
|
306 |> import |
|
307 in |
|
308 sih |
|
309 |> Thm.forall_elim (cert (inject idx rcargs)) |
|
310 |> Thm.elim_implies (import ineq) (* Psum rcargs *) |
|
311 |> Conv.fconv_rule sum_prod_conv |
|
312 |> Conv.fconv_rule ind_rulify |
|
313 |> (fn th => th COMP ipres) (* P rs *) |
|
314 |> fold_rev (Thm.implies_intr o cprop_of) cGas |
|
315 |> fold_rev Thm.forall_intr cGvs |
|
316 end |
|
317 |
|
318 val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *) |
|
319 |
|
320 val step = HOLogic.mk_Trueprop (list_comb (P, lhs)) |
|
321 |> fold_rev (curry Logic.mk_implies o prop_of) P_recs |
|
322 |> fold_rev (curry Logic.mk_implies) gs |
|
323 |> fold_rev (Logic.all o Free) qs |
|
324 |> cert |
|
325 |
|
326 val Plhs_to_Pxs_conv = |
|
327 foldl1 (uncurry Conv.combination_conv) |
|
328 (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps) |
|
329 |
|
330 val res = Thm.assume step |
|
331 |> fold Thm.forall_elim cqs |
|
332 |> fold Thm.elim_implies ags |
|
333 |> fold Thm.elim_implies P_recs (* P lhs *) |
|
334 |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *) |
|
335 |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps) |
|
336 |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) |
|
337 in |
|
338 (res, (cidx, step)) |
|
339 end |
|
340 |
|
341 val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss') |
|
342 |
|
343 val bstep = complete_thm |
|
344 |> Thm.forall_elim (cert (list_comb (P, fxs))) |
|
345 |> fold (Thm.forall_elim o cert) (fxs @ map Free ws) |
|
346 |> fold Thm.elim_implies C_hyps |
|
347 |> fold Thm.elim_implies cases (* P xs *) |
|
348 |> fold_rev (Thm.implies_intr o cprop_of) C_hyps |
|
349 |> fold_rev (Thm.forall_intr o cert o Free) ws |
|
350 |
|
351 val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) |
|
352 |> Goal.init |
|
353 |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) |
|
354 THEN CONVERSION ind_rulify 1) |
|
355 |> Seq.hd |
|
356 |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) |
|
357 |> Goal.finish ctxt |
|
358 |> Thm.implies_intr (cprop_of branch_hyp) |
|
359 |> fold_rev (Thm.forall_intr o cert) fxs |
|
360 in |
|
361 (Pxs, steps) |
|
362 end |
|
363 |
|
364 val (branches, steps) = |
|
365 map_index prove_branch (branches ~~ (complete_thms ~~ pats)) |
|
366 |> split_list |> apsnd flat |
|
367 |
|
368 val istep = sum_split_rule |
|
369 |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches |
|
370 |> Thm.implies_intr ihyp |
|
371 |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *) |
|
372 |
|
373 val induct_rule = |
|
374 @{thm "wf_induct_rule"} |
|
375 |> (curry op COMP) wf_thm |
|
376 |> (curry op COMP) istep |
|
377 |
|
378 val steps_sorted = map snd (sort (int_ord o pairself fst) steps) |
|
379 in |
|
380 (steps_sorted, induct_rule) |
|
381 end |
|
382 |
|
383 |
|
384 fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = |
|
385 (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) => |
|
386 let |
|
387 val (ctxt', _, cases, concl) = dest_hhf ctxt t |
|
388 val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl |
|
389 val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' |
|
390 val R = Free (Rn, mk_relT ST) |
|
391 val x = Free (xn, ST) |
|
392 val cert = cterm_of (ProofContext.theory_of ctxt) |
|
393 |
|
394 val ineqss = mk_ineqs R scheme |
|
395 |> map (map (pairself (Thm.assume o cert))) |
|
396 val complete = |
|
397 map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches) |
|
398 val wf_thm = mk_wf R scheme |> cert |> Thm.assume |
|
399 |
|
400 val (descent, pres) = split_list (flat ineqss) |
|
401 val newgoals = complete @ pres @ wf_thm :: descent |
|
402 |
|
403 val (steps, indthm) = |
|
404 mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme |
|
405 |
|
406 fun project (i, SchemeBranch {xs, ...}) = |
|
407 let |
|
408 val inst = (foldr1 HOLogic.mk_prod (map Free xs)) |
|
409 |> SumTree.mk_inj ST (length branches) (i + 1) |
|
410 |> cert |
|
411 in |
|
412 indthm |
|
413 |> Drule.instantiate' [] [SOME inst] |
|
414 |> simplify SumTree.sumcase_split_ss |
|
415 |> Conv.fconv_rule ind_rulify |
|
416 end |
|
417 |
|
418 val res = Conjunction.intr_balanced (map_index project branches) |
|
419 |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps) |
|
420 |> Drule.generalize ([], [Rn]) |
|
421 |
|
422 val nbranches = length branches |
|
423 val npres = length pres |
|
424 in |
|
425 Thm.compose_no_flatten false (res, length newgoals) i |
|
426 THEN term_tac (i + nbranches + npres) |
|
427 THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches)))) |
|
428 THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i))) |
|
429 end)) |
|
430 |
|
431 |
|
432 fun induction_schema_tac ctxt = |
|
433 mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; |
|
434 |
|
435 *} |
|
436 |
|
437 ML {* |
|
438 val trm1 = @{prop "P1 &&& P2 &&& P3"} |
|
439 val trm2 = @{prop "(P1 &&& P2) &&& P3 &&& P4"} |
|
440 *} |
|
441 |
|
442 ML {* |
|
443 Logic.dest_conjunctions trm2 |
|
444 *} |
|
445 |
|
446 lemma |
|
447 shows "P1" "P2" "P4" |
|
448 oops |
|
449 |
|
450 lemma |
|
451 shows "P1" "P2" "P3" "P4" |
|
452 oops |
|
453 |
|
454 lemma strong_induct: |
|
455 fixes c :: "'a :: fs" |
|
456 and assg :: assg and trm :: trm |
|
457 assumes a0: "\<And>name c. P1 c (Var name)" |
|
458 and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)" |
|
459 and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)" |
|
460 and a3: "\<And>a1 t1 a2 t2 c. |
|
461 \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; \<And>d. P2 c a1; \<And>d. P1 d t1; \<And>d. P2 d a2; \<And>d. P1 d t2\<rbrakk> |
|
462 \<Longrightarrow> P1 c (Let1 a1 t1 a2 t2)" |
|
463 and a4: "\<And>n1 n2 t1 t2 c. |
|
464 \<lbrakk>({atom n1} \<union> {atom n2}) \<sharp>* c; \<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (Let2 n1 n2 t1 t2)" |
|
465 and a5: "\<And>c. P2 c As_Nil" |
|
466 and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)" |
|
467 shows "P1 c trm" "P2 c assg" |
|
468 apply(raw_tactic {* induction_schema_tac @{context} @{thms assms} *}) |
|
469 apply(rule_tac y="trm" and c="c" in foo.strong_exhaust(1)) |
|
470 apply(simp_all)[5] |
|
471 apply(rule_tac ya="assg" in foo.strong_exhaust(2)) |
|
472 apply(simp_all)[2] |
|
473 apply(relation "measure (sum_case (size o snd) (size o snd))") |
|
474 apply(simp_all add: foo.size) |
|
475 done |
|
476 |
53 |
477 end |
54 end |
478 |
55 |
479 |
56 |
480 |
57 |