# HG changeset patch # User blanchet # Date 1393847299 -3600 # Node ID 3d40cf74726cac496e1874614cbfe382c8432704 # Parent 7f229b0212fe3b581b9b1e05268bc14475f151ce optimize cardinal bounds involving natLeq (omega) diff -r 7f229b0212fe -r 3d40cf74726c src/HOL/BNF_Cardinal_Arithmetic.thy --- a/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Mar 03 03:13:45 2014 +0100 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Mar 03 12:48:19 2014 +0100 @@ -199,7 +199,7 @@ "Cinfinite r1 \ Cinfinite r2 \ Cinfinite (r1 +c r2)" unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of) -lemma Cinfinite_csum_strong: +lemma Cinfinite_csum_weak: "\Cinfinite r1; Cinfinite r2\ \ Cinfinite (r1 +c r2)" by (erule Cinfinite_csum1) @@ -335,6 +335,9 @@ lemma cprod_mono2: "p2 \o r2 \ q *c p2 \o q *c r2" by (simp only: cprod_def ordLeq_Times_mono2) +lemma cprod_mono: "\p1 \o r1; p2 \o r2\ \ p1 *c p2 \o r1 *c r2" +by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2]) + lemma ordLeq_cprod2: "\Cnotzero p1; Card_order p2\ \ p2 \o p1 *c p2" unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI) @@ -347,6 +350,15 @@ lemma Cinfinite_cprod2: "\Cnotzero r1; Cinfinite r2\ \ Cinfinite (r1 *c r2)" by (blast intro: cinfinite_cprod2 Card_order_cprod) +lemma cprod_cong: "\p1 =o r1; p2 =o r2\ \ p1 *c p2 =o r1 *c r2" +by (metis cprod_mono ordIso_iff_ordLeq) + +lemma cprod_cong1: "\p1 =o r1\ \ p1 *c p2 =o r1 *c p2" +by (metis cprod_mono1 ordIso_iff_ordLeq) + +lemma cprod_cong2: "p2 =o r2 \ q *c p2 =o q *c r2" +by (metis cprod_mono2 ordIso_iff_ordLeq) + lemma cprod_com: "p1 *c p2 =o p2 *c p1" by (simp only: cprod_def card_of_Times_commute) @@ -514,6 +526,9 @@ unfolding cinfinite_def cprod_def by (rule Card_order_Times_infinite[THEN conjunct1]) (blast intro: czeroI)+ +lemma cprod_infinite: "Cinfinite r \ r *c r =o r" +using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast + lemma cexp_cprod_ordLeq: assumes r1: "Card_order r1" and r2: "Cinfinite r2" and r3: "Cnotzero r3" "r3 \o r2" diff -r 7f229b0212fe -r 3d40cf74726c src/HOL/BNF_Comp.thy --- a/src/HOL/BNF_Comp.thy Mon Mar 03 03:13:45 2014 +0100 +++ b/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:19 2014 +0100 @@ -128,6 +128,12 @@ end +lemma csum_dup: "cinfinite r \ Card_order r \ p +c p' =o r +c r \ p +c p' =o r" +by (metis csum_absorb2' ordIso_transitive ordLeq_refl) + +lemma cprod_dup: "cinfinite r \ Card_order r \ p *c p' =o r *c r \ p *c p' =o r" +by (metis cprod_infinite ordIso_transitive) + ML_file "Tools/BNF/bnf_comp_tactics.ML" ML_file "Tools/BNF/bnf_comp.ML" diff -r 7f229b0212fe -r 3d40cf74726c src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Mon Mar 03 03:13:45 2014 +0100 +++ b/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:19 2014 +0100 @@ -251,10 +251,10 @@ unfolding vimage2p_def by auto lemma id_transfer: "fun_rel A A id id" -unfolding fun_rel_def by simp + unfolding fun_rel_def by simp lemma ssubst_Pair_rhs: "\(r, s) \ R; s' = s\ \ (r, s') \ R" - by simp + by (rule ssubst) ML_file "Tools/BNF/bnf_lfp_util.ML" ML_file "Tools/BNF/bnf_lfp_tactics.ML" diff -r 7f229b0212fe -r 3d40cf74726c src/HOL/Cardinals/Cardinal_Arithmetic.thy --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Mar 03 03:13:45 2014 +0100 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Mar 03 12:48:19 2014 +0100 @@ -66,18 +66,10 @@ unfolding cprod_def cone_def Field_card_of by (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton]) -lemma cprod_cong2: "p2 =o r2 \ q *c p2 =o q *c r2" -by (simp only: cprod_def ordIso_Times_cong2) lemma ordLeq_cprod1: "\Card_order p1; Cnotzero p2\ \ p1 \o p1 *c p2" unfolding cprod_def by (metis Card_order_Times1 czeroI) -lemma cprod_infinite: "Cinfinite r \ r *c r =o r" -using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast - -lemma cprod_mono: "\p1 \o r1; p2 \o r2\ \ p1 *c p2 \o r1 *c r2" - by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2]) - subsection {* Exponentiation *} diff -r 7f229b0212fe -r 3d40cf74726c src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 03 03:13:45 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 03 12:48:19 2014 +0100 @@ -95,6 +95,10 @@ val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE; in Envir.expand_term get end; +fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u] + | is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u] + | is_sum_prod_natLeq t = (t = @{term natLeq}); + fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) = let val olive = live_of_bnf outer; @@ -170,6 +174,20 @@ (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*) val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd; + val (bd', bd_ordIso_natLeq_thm_opt) = + if is_sum_prod_natLeq bd then + let + val bd' = @{term natLeq}; + val bd_bd' = HOLogic.mk_prod (bd, bd'); + val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd')); + val goal = HOLogic.mk_Trueprop (HOLogic.mk_mem (bd_bd', ordIso)); + in + (bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac) + |> Thm.close_derivation)) + end + else + (bd, NONE); + fun map_id0_tac _ = mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer) (map map_id0_of_bnf inners); @@ -220,7 +238,7 @@ map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1); in map2 (fn set_alt => fn single_set_bds => fn ctxt => - mk_comp_set_bd_tac ctxt set_alt single_set_bds) + mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_thm_opt set_alt single_set_bds) set_alt_thms single_set_bd_thmss end; @@ -278,7 +296,7 @@ val (bnf', lthy') = bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty - Binding.empty [] ((((((b, CCA), mapx), sets), bd), wits), SOME rel) lthy; + Binding.empty [] ((((((b, CCA), mapx), sets), bd'), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; diff -r 7f229b0212fe -r 3d40cf74726c src/HOL/Tools/BNF/bnf_comp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Mon Mar 03 03:13:45 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Mon Mar 03 12:48:19 2014 +0100 @@ -15,7 +15,7 @@ val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic val mk_comp_set_alt_tac: Proof.context -> thm -> tactic - val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic + val mk_comp_set_bd_tac: Proof.context -> thm option -> thm -> thm list -> tactic val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic @@ -31,6 +31,7 @@ val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic val mk_simple_wit_tac: thm list -> tactic + val bd_ordIso_natLeq_tac: tactic end; structure BNF_Comp_Tactics : BNF_COMP_TACTICS = @@ -45,7 +46,6 @@ val trans_o_apply = @{thm trans[OF o_apply]}; - (* Composition *) fun mk_comp_set_alt_tac ctxt collect_set_map = @@ -101,6 +101,7 @@ end; fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order = + rtac @{thm natLeq_card_order} 1 ORELSE let val (card_orders, last_card_order) = split_last Fbd_card_orders; fun gen_before thm = rtac @{thm card_order_csum} THEN' rtac thm; @@ -111,14 +112,15 @@ end; fun mk_comp_bd_cinfinite_tac Fbd_cinfinite Gbd_cinfinite = - (rtac @{thm cinfinite_cprod} THEN' + (rtac @{thm natLeq_cinfinite} ORELSE' + rtac @{thm cinfinite_cprod} THEN' ((K (TRY ((rtac @{thm cinfinite_csum} THEN' rtac disjI1) 1)) THEN' ((rtac @{thm cinfinite_csum} THEN' rtac disjI1 THEN' rtac Fbd_cinfinite) ORELSE' rtac Fbd_cinfinite)) ORELSE' rtac Fbd_cinfinite) THEN' rtac Gbd_cinfinite) 1; -fun mk_comp_set_bd_tac ctxt comp_set_alt Gset_Fset_bds = +fun mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds = let val (bds, last_bd) = split_last Gset_Fset_bds; fun gen_before bd = @@ -127,6 +129,9 @@ rtac bd; fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1}; in + (case bd_ordIso_natLeq_opt of + SOME thm => rtac (thm RS rotate_prems 1 @{thm ordLeq_ordIso_trans}) 1 + | NONE => all_tac) THEN unfold_thms_tac ctxt [comp_set_alt] THEN rtac @{thm comp_set_bd_Union_o_collect} 1 THEN unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN @@ -168,7 +173,6 @@ (etac FalseE ORELSE' atac))) 1); - (* Kill operation *) fun mk_kill_map_cong0_tac ctxt n m map_cong0 = @@ -187,7 +191,6 @@ REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1)); - (* Lift operation *) val empty_natural_tac = rtac @{thm empty_natural} 1; @@ -206,7 +209,6 @@ REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1)); - (* Permute operation *) fun mk_permute_in_alt_tac src dest = @@ -214,6 +216,9 @@ mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong} dest src) 1; + +(* Miscellaneous *) + fun mk_le_rel_OO_tac outer_le_rel_OO outer_rel_mono inner_le_rel_OOs = EVERY' (map rtac (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1; @@ -222,4 +227,13 @@ fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms)); +val csum_thms = + @{thms csum_cong1 csum_cong2 csum_cong csum_dup[OF natLeq_cinfinite natLeq_Card_order]}; +val cprod_thms = + @{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]}; + +val bd_ordIso_natLeq_tac = + HEADGOAL (REPEAT_DETERM o resolve_tac + (@{thm ordIso_refl[OF natLeq_Card_order]} :: csum_thms @ cprod_thms)); + end; diff -r 7f229b0212fe -r 3d40cf74726c src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 03:13:45 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 12:48:19 2014 +0100 @@ -32,6 +32,8 @@ val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer + val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list + val IITN: string val LevN: string val algN: string @@ -164,7 +166,8 @@ val mk_sum_caseN: int -> int -> thm val mk_sum_caseN_balanced: int -> int -> thm - val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list + val mk_sum_Cinfinite: thm list -> thm + val mk_sum_card_order: thm list -> thm val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> @@ -474,6 +477,12 @@ Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)}, right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k; +fun mk_sum_Cinfinite [thm] = thm + | mk_sum_Cinfinite (thm :: thms) = @{thm Cinfinite_csum_weak} OF [thm, mk_sum_Cinfinite thms]; + +fun mk_sum_card_order [thm] = thm + | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms]; + fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy = let val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels; diff -r 7f229b0212fe -r 3d40cf74726c src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 03 03:13:45 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 03 12:48:19 2014 +0100 @@ -953,17 +953,8 @@ 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_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 diff -r 7f229b0212fe -r 3d40cf74726c src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 03 03:13:45 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 03 12:48:19 2014 +0100 @@ -587,17 +587,8 @@ 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_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