# HG changeset patch # User traytel # Date 1396342960 -7200 # Node ID 949d4c7a86c63b627dfa3eab177f92b8a0a7e293 # Parent b53d78fd25a38822994144e1b4a32649d400f19d more precise BNF bound for datatypes diff -r b53d78fd25a3 -r 949d4c7a86c6 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Apr 01 10:51:29 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Apr 01 11:02:40 2014 +0200 @@ -152,8 +152,6 @@ val bd0_Cinfinites = map bd_Cinfinite_of_bnf bnfs; val set_bd0ss = map set_bd_of_bnf bnfs; - val bd_card_orders = - map (fn thm => @{thm card_order_csum} OF [thm, @{thm card_of_card_order_on}]) bd0_card_orders; val bd_Card_order = @{thm Card_order_csum}; val bd_Card_orders = replicate n bd_Card_order; val bd_Cinfinites = map (fn thm => thm RS @{thm Cinfinite_csum1}) bd0_Cinfinites; @@ -451,9 +449,9 @@ val sum_bd = Library.foldr1 (uncurry mk_csum) bds; val sum_bdT = fst (dest_relT (fastype_of sum_bd)); - val (lthy, sbd, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) = + val (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) = if n = 1 - then (lthy, sum_bd, hd bd_card_orders, bd_Cinfinite, bd_Card_order, set_bdss, in_bds) + then (lthy, sum_bd, bd_Cinfinite, bd_Card_order, set_bdss, in_bds) else let val sbdT_bind = mk_internal_b sum_bdTN; @@ -481,20 +479,15 @@ val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT)); val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info); - val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info); val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites; val sum_Card_order = sum_Cinfinite RS conjunct2; - val sum_card_order = mk_sum_card_order bd_card_orders; val sbd_ordIso = @{thm ssubst_Pair_rhs} OF [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def]; val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite]; val sbd_Card_order = sbd_Cinfinite RS conjunct2; - val sbd_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF - [sbd_def, @{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]]; - fun mk_set_sbd i bd_Card_order bds = map (fn thm => @{thm ordLeq_ordIso_trans} OF [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds; @@ -506,7 +499,7 @@ (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]})); val in_sbds = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds; in - (lthy, sbd, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) + (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) end; val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero}; @@ -1381,12 +1374,67 @@ ctors (0 upto n - 1) witss end; + val (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss) = + if n = 1 + then (lthy, hd bd0s, hd bd0_card_orders, hd bd0_Cinfinites, set_bd0ss) + else + let + val sum_bd0 = Library.foldr1 (uncurry mk_csum) bd0s; + val sum_bd0T = fst (dest_relT (fastype_of sum_bd0)); + + val sbd0T_bind = mk_internal_b (sum_bdTN ^ "0"); + + val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) = + typedef (sbd0T_bind, dead_params, NoSyn) + (HOLogic.mk_UNIV sum_bd0T) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; + + val sbd0T = Type (sbd0T_name, dead_params'); + val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T); + + val sbd0_bind = mk_internal_b (sum_bdN ^ "0"); + val sbd0_def_bind = (Thm.def_binding sbd0_bind, []); + + val sbd0_spec = mk_dir_image sum_bd0 Abs_sbd0T; + + val ((sbd0_free, (_, sbd0_def_free)), (lthy, lthy_old)) = + lthy + |> Local_Theory.define ((sbd0_bind, NoSyn), (sbd0_def_bind, sbd0_spec)) + ||> `Local_Theory.restore; + + val phi = Proof_Context.export_morphism lthy_old lthy; + + val sbd0_def = Morphism.thm phi sbd0_def_free RS meta_eq_to_obj_eq; + val sbd0 = Const (fst (Term.dest_Const (Morphism.term phi sbd0_free)), + mk_relT (`I sbd0T)); + + val Abs_sbd0T_inj = mk_Abs_inj_thm (#Abs_inject sbd0T_loc_info); + val Abs_sbd0T_bij = mk_Abs_bij_thm lthy Abs_sbd0T_inj (#Abs_cases sbd0T_loc_info); + + val sum_Cinfinite = mk_sum_Cinfinite bd0_Cinfinites; + val sum_Card_order = sum_Cinfinite RS conjunct2; + val sum_card_order = mk_sum_card_order bd0_card_orders; + + val sbd0_ordIso = @{thm ssubst_Pair_rhs} OF + [@{thm dir_image} OF [Abs_sbd0T_inj, sum_Card_order], sbd0_def]; + val sbd0_Cinfinite = @{thm Cinfinite_cong} OF [sbd0_ordIso, sum_Cinfinite]; + + val sbd0_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF + [sbd0_def, @{thm card_order_dir_image} OF [Abs_sbd0T_bij, sum_card_order]]; + + fun mk_set_sbd0 i bd0_Card_order bd0s = + map (fn thm => @{thm ordLeq_ordIso_trans} OF + [bd0_Card_order RS mk_ordLeq_csum n i thm, sbd0_ordIso]) bd0s; + val set_sbd0ss = map3 mk_set_sbd0 ks bd0_Card_orders set_bd0ss; + in + (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss) + end; + val (Ibnf_consts, lthy) = fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits => fn T => fn lthy => define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads) map_b rel_b set_bs - ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy) + ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd0), wits), NONE) lthy) bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy; val (_, Iconsts, Iconst_defs, mk_Iconsts) = split_list4 Ibnf_consts; @@ -1426,7 +1474,7 @@ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN mk_map_tac m n foldx map_comp_id map_cong0) |> Thm.close_derivation - |> singleton (Proof_Context.export names_lthy lthy)) + |> singleton (Proof_Context.export names_lthy lthy)) goals ctor_fold_thms map_comp_id_thms map_cong0s; in `(map (fn thm => thm RS @{thm comp_eq_dest})) maps @@ -1536,7 +1584,7 @@ let fun mk_set_bd z bd set = mk_ordLeq (mk_card_of (set $ z)) bd; - fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd set)); + fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd0 set)); val cphiss = map (map2 mk_cphi Izs) Isetss_by_range; @@ -1548,7 +1596,7 @@ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map3 mk_set_bd Izs Ibds sets))) Isetss_by_range; - fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sbd_Cinfinite set_sbdss; + fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sbd0_Cinfinite set_sbd0ss; val thms = map4 (fn goal => fn ctor_sets => fn induct => fn i => Goal.prove_sorry lthy [] [] goal @@ -1656,9 +1704,9 @@ val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) Imap_cong0_thms; val set_map0_tacss = map (map (K o mk_set_map0_tac)) (transpose Iset_Imap0_thmss); val bd_co_tacs = replicate n (fn ctxt => - unfold_thms_tac ctxt Ibd_defs THEN rtac sbd_card_order 1); + unfold_thms_tac ctxt Ibd_defs THEN rtac sbd0_card_order 1); val bd_cinf_tacs = replicate n (fn ctxt => - unfold_thms_tac ctxt Ibd_defs THEN rtac (sbd_Cinfinite RS conjunct1) 1); + unfold_thms_tac ctxt Ibd_defs THEN rtac (sbd0_Cinfinite RS conjunct1) 1); val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose Iset_bd_thmss); val le_rel_OO_tacs = map (fn i => K ((rtac @{thm predicate2I} THEN' etac (le_Irel_OO_thm RS mk_conjunctN n i RS mp)) 1)) ks;