--- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue Dec 17 15:15:59 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue Dec 17 15:44:10 2013 +0100
@@ -2236,10 +2236,6 @@
val timer = time (timer "map functions for the new codatatypes");
- val bd = mk_cexp sbd sbd;
-
- val timer = time (timer "bounds for the new codatatypes");
-
val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks;
val setss_by_bnf' = map (fn i => map2 (mk_hset dtor's i) ls passiveBs) ks;
val setss_by_range = transpose setss_by_bnf;
@@ -2476,8 +2472,8 @@
val set_nat_tacss =
map2 (map2 (K oo mk_set_map0_tac)) hset_defss (transpose col_natural_thmss);
- val bd_co_tacs = replicate n (K (mk_bd_card_order_tac sbd_card_order));
- val bd_cinf_tacs = replicate n (K (mk_bd_cinfinite_tac sbd_Cinfinite));
+ val bd_co_tacs = replicate n (K (rtac sbd_card_order 1));
+ val bd_cinf_tacs = replicate n (K (rtac (sbd_Cinfinite RS conjunct1) 1));
val set_bd_tacss =
map2 (map2 (K oo mk_set_bd_tac sbd_Cinfinite)) hset_defss (transpose col_bd_thmss);
@@ -2682,7 +2678,7 @@
fn T => fn (thms, wits) => fn lthy =>
bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b
rel_b set_bs
- ((((((b, T), fold_rev Term.absfree fs' mapx), sets), bd), wits), NONE) lthy
+ ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy
|> register_bnf (Local_Theory.full_name lthy b))
tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Tue Dec 17 15:15:59 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Tue Dec 17 15:44:10 2013 +0100
@@ -11,8 +11,6 @@
sig
val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list ->
thm list list -> tactic
- val mk_bd_card_order_tac: thm -> tactic
- val mk_bd_cinfinite_tac: thm -> tactic
val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
@@ -1134,16 +1132,8 @@
fun mk_set_bd_tac sbd_Cinfinite hset_def col_bd =
EVERY' (map rtac [ordIso_ordLeq_trans, @{thm card_of_ordIso_subst}, hset_def,
- ctrans, @{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat},
- @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
- @{thm infinite_ordLeq_cexp}, sbd_Cinfinite]) 1;
-
-fun mk_bd_card_order_tac sbd_card_order =
- EVERY' (map rtac [@{thm card_order_cexp}, sbd_card_order, sbd_card_order]) 1;
-
-fun mk_bd_cinfinite_tac sbd_Cinfinite =
- EVERY' (map rtac [@{thm cinfinite_cexp}, @{thm ctwo_ordLeq_Cinfinite},
- sbd_Cinfinite, sbd_Cinfinite]) 1;
+ @{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat},
+ @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite]) 1;
fun mk_pickWP_assms_tac set_incl_hsets set_incl_hins map_eq =
let
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Tue Dec 17 15:15:59 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue Dec 17 15:44:10 2013 +0100
@@ -1497,14 +1497,6 @@
val timer = time (timer "map functions for the new datatypes");
- val bd = mk_cpow sum_bd;
- val bd_Cinfinite = sum_Cinfinite RS @{thm Cinfinite_cpow};
- fun mk_cpow_bd thm = @{thm ordLeq_transitive} OF
- [thm, sum_Card_order RS @{thm cpow_greater_eq}];
- val set_bd_cpowss = map (map mk_cpow_bd) set_bd_sumss;
-
- val timer = time (timer "bounds for the new datatypes");
-
val ls = 1 upto m;
val setsss = map (mk_setss o mk_set_Ts) passiveAs;
val map_setss = map (fn T => map2 (fn Ds =>
@@ -1602,7 +1594,7 @@
val set_bd_thmss =
let
- fun mk_set_bd z set = mk_ordLeq (mk_card_of (set $ z)) bd;
+ fun mk_set_bd z set = mk_ordLeq (mk_card_of (set $ z)) sum_bd;
fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z set));
@@ -1616,7 +1608,7 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 mk_set_bd Izs sets))) setss_by_range;
- fun mk_tac induct = mk_set_bd_tac m (rtac induct) bd_Cinfinite set_bd_cpowss;
+ fun mk_tac induct = mk_set_bd_tac m (rtac induct) sum_Cinfinite set_bd_sumss;
val thms =
map4 (fn goal => fn ctor_sets => fn induct => fn i =>
singleton (Proof_Context.export names_lthy lthy)
@@ -1707,7 +1699,7 @@
val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
val set_nat_tacss = map (map (K o mk_set_map0_tac)) (transpose set_map0_thmss);
val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
- val bd_cinf_tacs = replicate n (K (rtac (bd_Cinfinite RS conjunct1) 1));
+ val bd_cinf_tacs = replicate n (K (rtac (sum_Cinfinite RS conjunct1) 1));
val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose set_bd_thmss);
val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
@@ -1753,7 +1745,7 @@
fn T => fn wits => fn lthy =>
bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
map_b rel_b set_bs
- ((((((b, T), fold_rev Term.absfree fs' mapx), sets), bd), wits), NONE)
+ ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sum_bd), wits), NONE)
lthy
|> register_bnf (Local_Theory.full_name lthy b))
tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Tue Dec 17 15:15:59 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Tue Dec 17 15:44:10 2013 +0100
@@ -728,8 +728,7 @@
EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
fun mk_bd_card_order_tac bd_card_orders =
- (rtac @{thm card_order_cpow} THEN'
- CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders) 1;
+ CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders 1;
fun mk_wpull_tac wpull =
EVERY' [rtac ssubst, rtac @{thm wpull_def}, rtac allI, rtac allI,