# HG changeset patch # User traytel # Date 1387291450 -3600 # Node ID c99f0fdb08863fa47f024aec2a4fee6a860ec467 # Parent 641ea768f53514b793a313a8d53dc018e9d7ddc9 tighter bnf bounds for (co)datatypes diff -r 641ea768f535 -r c99f0fdb0886 src/HOL/BNF/Tools/bnf_gfp.ML --- 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; diff -r 641ea768f535 -r c99f0fdb0886 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- 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 diff -r 641ea768f535 -r c99f0fdb0886 src/HOL/BNF/Tools/bnf_lfp.ML --- 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; diff -r 641ea768f535 -r c99f0fdb0886 src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- 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,