155 |
155 |
156 fun map_comp_tac _ = |
156 fun map_comp_tac _ = |
157 mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer) |
157 mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer) |
158 (map map_comp_of_bnf inners); |
158 (map map_comp_of_bnf inners); |
159 |
159 |
160 fun mk_single_set_natural_tac i _ = |
160 fun mk_single_set_map_tac i _ = |
161 mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer) |
161 mk_comp_set_map_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer) |
162 (collect_set_natural_of_bnf outer) |
162 (collect_set_map_of_bnf outer) |
163 (map ((fn thms => nth thms i) o set_natural_of_bnf) inners); |
163 (map ((fn thms => nth thms i) o set_map_of_bnf) inners); |
164 |
164 |
165 val set_natural_tacs = map mk_single_set_natural_tac (0 upto ilive - 1); |
165 val set_map_tacs = map mk_single_set_map_tac (0 upto ilive - 1); |
166 |
166 |
167 fun bd_card_order_tac _ = |
167 fun bd_card_order_tac _ = |
168 mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer); |
168 mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer); |
169 |
169 |
170 fun bd_cinfinite_tac _ = |
170 fun bd_cinfinite_tac _ = |
175 [] |
175 [] |
176 else |
176 else |
177 map (fn goal => |
177 map (fn goal => |
178 Goal.prove_sorry lthy [] [] goal |
178 Goal.prove_sorry lthy [] [] goal |
179 (fn {context = ctxt, prems = _} => |
179 (fn {context = ctxt, prems = _} => |
180 mk_comp_set_alt_tac ctxt (collect_set_natural_of_bnf outer)) |
180 mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer)) |
181 |> Thm.close_derivation) |
181 |> Thm.close_derivation) |
182 (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt); |
182 (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt); |
183 |
183 |
184 fun map_cong0_tac _ = |
184 fun map_cong0_tac _ = |
185 mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners); |
185 mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners); |
236 |> unfold_thms lthy (basic_thms @ srel_def_of_bnf outer :: map srel_def_of_bnf inners); |
236 |> unfold_thms lthy (basic_thms @ srel_def_of_bnf outer :: map srel_def_of_bnf inners); |
237 in |
237 in |
238 unfold_thms_tac lthy basic_thms THEN rtac thm 1 |
238 unfold_thms_tac lthy basic_thms THEN rtac thm 1 |
239 end; |
239 end; |
240 |
240 |
241 val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac |
241 val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac |
242 bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; |
242 bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; |
243 |
243 |
244 val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; |
244 val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; |
245 |
245 |
246 val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I))) |
246 val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I))) |
255 |> map (`(fn t => Term.add_frees t [])) |
255 |> map (`(fn t => Term.add_frees t [])) |
256 |> minimize_wits |
256 |> minimize_wits |
257 |> map (fn (frees, t) => fold absfree frees t); |
257 |> map (fn (frees, t) => fold absfree frees t); |
258 |
258 |
259 fun wit_tac {context = ctxt, prems = _} = |
259 fun wit_tac {context = ctxt, prems = _} = |
260 mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer) |
260 mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer) |
261 (maps wit_thms_of_bnf inners); |
261 (maps wit_thms_of_bnf inners); |
262 |
262 |
263 val (bnf', lthy') = |
263 val (bnf', lthy') = |
264 bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty |
264 bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty |
265 [] (((((b, mapx), sets), bd), wits), SOME rel) lthy; |
265 [] (((((b, mapx), sets), bd), wits), SOME rel) lthy; |
309 fun map_comp_tac {context = ctxt, prems = _} = |
309 fun map_comp_tac {context = ctxt, prems = _} = |
310 unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
310 unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
311 rtac refl 1; |
311 rtac refl 1; |
312 fun map_cong0_tac {context = ctxt, prems = _} = |
312 fun map_cong0_tac {context = ctxt, prems = _} = |
313 mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf); |
313 mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf); |
314 val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf)); |
314 val set_map_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map_of_bnf bnf)); |
315 fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf); |
315 fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf); |
316 fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf); |
316 fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf); |
317 val set_bd_tacs = |
317 val set_bd_tacs = |
318 map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm) |
318 map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm) |
319 (drop n (set_bd_of_bnf bnf)); |
319 (drop n (set_bd_of_bnf bnf)); |
346 |> unfold_thms lthy (srel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv}); |
346 |> unfold_thms lthy (srel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv}); |
347 in |
347 in |
348 rtac thm 1 |
348 rtac thm 1 |
349 end; |
349 end; |
350 |
350 |
351 val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac |
351 val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac |
352 bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; |
352 bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; |
353 |
353 |
354 val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; |
354 val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; |
355 |
355 |
356 val wits = map (fn t => fold absfree (Term.add_frees t []) t) |
356 val wits = map (fn t => fold absfree (Term.add_frees t []) t) |
403 fun map_comp_tac {context = ctxt, prems = _} = |
403 fun map_comp_tac {context = ctxt, prems = _} = |
404 unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
404 unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN |
405 rtac refl 1; |
405 rtac refl 1; |
406 fun map_cong0_tac {context = ctxt, prems = _} = |
406 fun map_cong0_tac {context = ctxt, prems = _} = |
407 rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); |
407 rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); |
408 val set_natural_tacs = |
408 val set_map_tacs = |
409 if ! quick_and_dirty then |
409 if ! quick_and_dirty then |
410 replicate (n + live) (K all_tac) |
410 replicate (n + live) (K all_tac) |
411 else |
411 else |
412 replicate n (K empty_natural_tac) @ |
412 replicate n (K empty_natural_tac) @ |
413 map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf); |
413 map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf); |
414 fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; |
414 fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; |
415 fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
415 fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
416 val set_bd_tacs = |
416 val set_bd_tacs = |
417 if ! quick_and_dirty then |
417 if ! quick_and_dirty then |
418 replicate (n + live) (K all_tac) |
418 replicate (n + live) (K all_tac) |
433 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
433 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
434 |
434 |
435 fun srel_O_Gr_tac _ = |
435 fun srel_O_Gr_tac _ = |
436 mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm; |
436 mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm; |
437 |
437 |
438 val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac |
438 val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac |
439 bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; |
439 bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; |
440 |
440 |
441 val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
441 val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
442 |
442 |
443 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
443 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
488 |
488 |
489 fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; |
489 fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1; |
490 fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1; |
490 fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1; |
491 fun map_cong0_tac {context = ctxt, prems = _} = |
491 fun map_cong0_tac {context = ctxt, prems = _} = |
492 rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); |
492 rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); |
493 val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf)); |
493 val set_map_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf)); |
494 fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; |
494 fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1; |
495 fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
495 fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1; |
496 val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf)); |
496 val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf)); |
497 |
497 |
498 val in_alt_thm = |
498 val in_alt_thm = |
510 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
510 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf); |
511 |
511 |
512 fun srel_O_Gr_tac _ = |
512 fun srel_O_Gr_tac _ = |
513 mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm; |
513 mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm; |
514 |
514 |
515 val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac |
515 val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac |
516 bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; |
516 bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac; |
517 |
517 |
518 val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
518 val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
519 |
519 |
520 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
520 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
651 fun mk_tac thm {context = ctxt, prems = _} = |
651 fun mk_tac thm {context = ctxt, prems = _} = |
652 (rtac (unfold_all thm) THEN' |
652 (rtac (unfold_all thm) THEN' |
653 SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1; |
653 SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1; |
654 |
654 |
655 val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf)) |
655 val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf)) |
656 (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf)) |
656 (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf)) |
657 (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd) |
657 (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd) |
658 (mk_tac (map_wpull_of_bnf bnf)) |
658 (mk_tac (map_wpull_of_bnf bnf)) |
659 (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf))); |
659 (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf))); |
660 |
660 |
661 val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |
661 val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); |