# HG changeset patch # User traytel # Date 1393452569 -3600 # Node ID f2cf7f92c9ac537d36f9cf18be6867799501a8ca # Parent 1f27d75ccf05171ea8a853e60e50a8b045d63ce3 intermediate typedef for the type of the bound (local to lfp) diff -r 1f27d75ccf05 -r f2cf7f92c9ac src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Wed Feb 26 17:14:23 2014 +0100 +++ b/src/HOL/BNF_LFP.thy Wed Feb 26 23:09:29 2014 +0100 @@ -236,6 +236,9 @@ lemma id_transfer: "fun_rel A A id id" unfolding fun_rel_def by simp +lemma ssubst_Pair_rhs: "\(r, s) \ R; s' = s\ \ (r, s') \ R" + by simp + ML_file "Tools/BNF/bnf_lfp_util.ML" ML_file "Tools/BNF/bnf_lfp_tactics.ML" ML_file "Tools/BNF/bnf_lfp.ML" diff -r 1f27d75ccf05 -r f2cf7f92c9ac src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 26 17:14:23 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 26 23:09:29 2014 +0100 @@ -966,10 +966,10 @@ val sum_card_order = mk_sum_card_order bd_card_orders; - val sbd_ordIso = fold_thms lthy [sbd_def] - (@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order]); - val sbd_card_order = fold_thms lthy [sbd_def] - (@{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]); + val sbd_ordIso = @{thm ssubst_Pair_rhs} OF + [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def]; + 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]]; val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite]; val sbd_Card_order = sbd_Cinfinite RS conjunct2; diff -r 1f27d75ccf05 -r f2cf7f92c9ac src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Feb 26 17:14:23 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Feb 26 23:09:29 2014 +0100 @@ -82,6 +82,7 @@ fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs; val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs); + val (dead_params, dead_params') = `(map Term.dest_TFree) (subtract (op =) passiveAs params'); val FTsAs = mk_FTs allAs; val FTsBs = mk_FTs allBs; val FTsCs = mk_FTs allCs; @@ -159,7 +160,6 @@ val bd_Cinfinites = map (fn thm => thm RS @{thm Cinfinite_csum1}) bd0_Cinfinites; val bd_Cnotzeros = map (fn thm => thm RS @{thm Cinfinite_Cnotzero}) bd_Cinfinites; val bd_Cinfinite = hd bd_Cinfinites; - val bd_Cnotzero = hd bd_Cnotzeros; val set_bdss = map2 (fn set_bd0s => fn bd0_Card_order => map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s) @@ -552,32 +552,87 @@ (* bounds *) - val sum_Card_order = if n = 1 then bd_Card_order else @{thm Card_order_csum}; - val sum_Cnotzero = if n = 1 then bd_Cnotzero else bd_Cnotzero RS @{thm csum_Cnotzero1}; - val sum_Cinfinite = if n = 1 then bd_Cinfinite else bd_Cinfinite RS @{thm Cinfinite_csum1}; - fun mk_set_bd_sums i bd_Card_order bds = - if n = 1 then bds - else map (fn thm => bd_Card_order RS mk_ordLeq_csum n i thm) bds; - val set_bd_sumss = map3 mk_set_bd_sums ks bd_Card_orders set_bdss; + 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) = + if n = 1 + then (lthy, sum_bd, hd bd_card_orders, bd_Cinfinite, bd_Card_order, set_bdss, in_bds) + else + let + val sbdT_bind = mk_internal_b sum_bdTN; + + val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) = + typedef (sbdT_bind, dead_params, NoSyn) + (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; + + val sbdT = Type (sbdT_name, dead_params'); + val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT); + + val sbd_bind = mk_internal_b sum_bdN; + val sbd_def_bind = (Thm.def_binding sbd_bind, []); + + val sbd_spec = mk_dir_image sum_bd Abs_sbdT; + + val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) = + lthy + |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec)) + ||> `Local_Theory.restore; + + val phi = Proof_Context.export_morphism lthy_old lthy; + + val sbd_def = Morphism.thm phi sbd_def_free RS meta_eq_to_obj_eq; + 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); - fun mk_in_bd_sum i Co Cnz bd = - if n = 1 then bd - else Cnz RS ((Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl})) RS - (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]})); - val in_bd_sums = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds; + fun mk_sum_Cinfinite [thm] = thm + | mk_sum_Cinfinite (thm :: thms) = + @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms]; + + val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites; + val sum_Card_order = sum_Cinfinite RS conjunct2; + + fun mk_sum_card_order [thm] = thm + | mk_sum_card_order (thm :: thms) = + @{thm card_order_csum} OF [thm, mk_sum_card_order thms]; + + 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 sum_bd = Library.foldr1 (uncurry mk_csum) bds; - val suc_bd = mk_cardSuc sum_bd; + 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; + val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss; + + fun mk_in_bd_sum i Co Cnz bd = + Cnz RS ((@{thm ordLeq_ordIso_trans} OF + [Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl}), sbd_ordIso]) RS + (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) + end; + + val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero}; + val suc_bd = mk_cardSuc sbd; + val field_suc_bd = mk_Field suc_bd; val suc_bdT = fst (dest_relT (fastype_of suc_bd)); fun mk_Asuc_bd [] = mk_cexp ctwo suc_bd | mk_Asuc_bd As = mk_cexp (mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo) suc_bd; - val suc_bd_Card_order = if n = 1 then bd_Card_order RS @{thm cardSuc_Card_order} - else @{thm cardSuc_Card_order[OF Card_order_csum]}; - val suc_bd_Cinfinite = if n = 1 then bd_Cinfinite RS @{thm Cinfinite_cardSuc} - else bd_Cinfinite RS @{thm Cinfinite_cardSuc[OF Cinfinite_csum1]}; + val suc_bd_Card_order = sbd_Card_order RS @{thm cardSuc_Card_order}; + val suc_bd_Cinfinite = sbd_Cinfinite RS @{thm Cinfinite_cardSuc}; val suc_bd_Cnotzero = suc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero}; val suc_bd_worel = suc_bd_Card_order RS @{thm Card_order_wo_rel} val basis_Asuc = if m = 0 then @{thm ordLeq_refl[OF Card_order_ctwo]} @@ -679,8 +734,8 @@ (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction))) (K (mk_min_algs_card_of_tac card_cT card_ct - m suc_bd_worel min_algs_thms in_bd_sums - sum_Card_order sum_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero + m suc_bd_worel min_algs_thms in_sbds + sbd_Card_order sbd_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero suc_bd_Asuc_bd Asuc_bd_Cinfinite))) |> Thm.close_derivation; @@ -741,8 +796,8 @@ val goal = fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_alg min_algs ss)); val alg_min_alg = Goal.prove_sorry lthy [] [] goal - (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sum_Cinfinite - set_bd_sumss min_algs_thms min_algs_mono_thms)) + (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sbd_Cinfinite + set_sbdss min_algs_thms min_algs_mono_thms)) |> Thm.close_derivation; fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] [] @@ -1438,7 +1493,7 @@ fn T => fn lthy => define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads) map_b rel_b set_bs - ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sum_bd), wits), NONE) lthy) + ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), 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; @@ -1586,7 +1641,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 sum_bd set)); + fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd set)); val cphiss = map (map2 mk_cphi Izs) Isetss_by_range; @@ -1598,7 +1653,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) sum_Cinfinite set_bd_sumss; + fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sbd_Cinfinite set_sbdss; val thms = map4 (fn goal => fn ctor_sets => fn induct => fn i => singleton (Proof_Context.export names_lthy lthy) @@ -1705,9 +1760,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 mk_bd_card_order_tac bd_card_orders); + unfold_thms_tac ctxt Ibd_defs THEN rtac sbd_card_order 1); val bd_cinf_tacs = replicate n (fn ctxt => - unfold_thms_tac ctxt Ibd_defs THEN rtac (sum_Cinfinite RS conjunct1) 1); + unfold_thms_tac ctxt Ibd_defs THEN rtac (sbd_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;