equal
deleted
inserted
replaced
250 val goal = mk_Trueprop_eq (var_set', set); |
250 val goal = mk_Trueprop_eq (var_set', set); |
251 fun tac {context = ctxt, prems = _} = |
251 fun tac {context = ctxt, prems = _} = |
252 mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer); |
252 mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer); |
253 val set'_eq_set = |
253 val set'_eq_set = |
254 Goal.prove (*no sorry*) names_lthy [] [] goal tac |
254 Goal.prove (*no sorry*) names_lthy [] [] goal tac |
255 |> Thm.close_derivation; |
255 |> Thm.close_derivation \<^here>; |
256 val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set))); |
256 val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set))); |
257 in |
257 in |
258 (set', set'_eq_set) |
258 (set', set'_eq_set) |
259 end; |
259 end; |
260 |
260 |
272 val bd_bd' = HOLogic.mk_prod (bd, bd'); |
272 val bd_bd' = HOLogic.mk_prod (bd, bd'); |
273 val ordIso = Const (\<^const_name>\<open>ordIso\<close>, HOLogic.mk_setT (fastype_of bd_bd')); |
273 val ordIso = Const (\<^const_name>\<open>ordIso\<close>, HOLogic.mk_setT (fastype_of bd_bd')); |
274 val goal = mk_Trueprop_mem (bd_bd', ordIso); |
274 val goal = mk_Trueprop_mem (bd_bd', ordIso); |
275 in |
275 in |
276 (bd', SOME (Goal.prove_sorry lthy [] [] goal (bd_ordIso_natLeq_tac o #context) |
276 (bd', SOME (Goal.prove_sorry lthy [] [] goal (bd_ordIso_natLeq_tac o #context) |
277 |> Thm.close_derivation)) |
277 |> Thm.close_derivation \<^here>)) |
278 end |
278 end |
279 else |
279 else |
280 (bd, NONE); |
280 (bd, NONE); |
281 |
281 |
282 fun map_id0_tac ctxt = |
282 fun map_id0_tac ctxt = |
306 else |
306 else |
307 map (fn goal => |
307 map (fn goal => |
308 Goal.prove_sorry lthy [] [] goal |
308 Goal.prove_sorry lthy [] [] goal |
309 (fn {context = ctxt, prems = _} => |
309 (fn {context = ctxt, prems = _} => |
310 mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer)) |
310 mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer)) |
311 |> Thm.close_derivation) |
311 |> Thm.close_derivation \<^here>) |
312 (map2 (curry mk_Trueprop_eq) sets sets_alt); |
312 (map2 (curry mk_Trueprop_eq) sets sets_alt); |
313 |
313 |
314 fun map_cong0_tac ctxt = |
314 fun map_cong0_tac ctxt = |
315 mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer) |
315 mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer) |
316 (map map_cong0_of_bnf inners); |
316 (map map_cong0_of_bnf inners); |
340 val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA; |
340 val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA; |
341 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
341 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
342 in |
342 in |
343 Goal.prove_sorry lthy [] [] goal |
343 Goal.prove_sorry lthy [] [] goal |
344 (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms) |
344 (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms) |
345 |> Thm.close_derivation |
345 |> Thm.close_derivation \<^here> |
346 end; |
346 end; |
347 |
347 |
348 fun le_rel_OO_tac ctxt = mk_le_rel_OO_tac ctxt (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer) |
348 fun le_rel_OO_tac ctxt = mk_le_rel_OO_tac ctxt (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer) |
349 (map le_rel_OO_of_bnf inners); |
349 (map le_rel_OO_of_bnf inners); |
350 |
350 |
463 val inx = mk_in Asets sets T; |
463 val inx = mk_in Asets sets T; |
464 val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T; |
464 val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T; |
465 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
465 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
466 in |
466 in |
467 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => |
467 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => |
468 kill_in_alt_tac ctxt) |> Thm.close_derivation |
468 kill_in_alt_tac ctxt) |> Thm.close_derivation \<^here> |
469 end; |
469 end; |
470 |
470 |
471 fun le_rel_OO_tac ctxt = |
471 fun le_rel_OO_tac ctxt = |
472 EVERY' [rtac ctxt @{thm ord_le_eq_trans}, rtac ctxt (le_rel_OO_of_bnf bnf)] 1 THEN |
472 EVERY' [rtac ctxt @{thm ord_le_eq_trans}, rtac ctxt (le_rel_OO_of_bnf bnf)] 1 THEN |
473 unfold_thms_tac ctxt @{thms eq_OO} THEN rtac ctxt refl 1; |
473 unfold_thms_tac ctxt @{thms eq_OO} THEN rtac ctxt refl 1; |
577 val inx = mk_in Asets sets T; |
577 val inx = mk_in Asets sets T; |
578 val in_alt = mk_in (drop n Asets) bnf_sets T; |
578 val in_alt = mk_in (drop n Asets) bnf_sets T; |
579 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
579 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
580 in |
580 in |
581 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => lift_in_alt_tac ctxt) |
581 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => lift_in_alt_tac ctxt) |
582 |> Thm.close_derivation |
582 |> Thm.close_derivation \<^here> |
583 end; |
583 end; |
584 |
584 |
585 fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1; |
585 fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1; |
586 |
586 |
587 fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm; |
587 fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm; |
665 val in_alt = mk_in (unpermute Asets) bnf_sets T; |
665 val in_alt = mk_in (unpermute Asets) bnf_sets T; |
666 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
666 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); |
667 in |
667 in |
668 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => |
668 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => |
669 mk_permute_in_alt_tac ctxt src dest) |
669 mk_permute_in_alt_tac ctxt src dest) |
670 |> Thm.close_derivation |
670 |> Thm.close_derivation \<^here> |
671 end; |
671 end; |
672 |
672 |
673 fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1; |
673 fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1; |
674 |
674 |
675 fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm; |
675 fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm; |