# HG changeset patch # User traytel # Date 1373534183 -7200 # Node ID 7c4b56bac189ff0e622d88d84e5b853512b84d9a # Parent 21774f0b7bc086280fb599fc3aa46a904be230bf some new lemmas towards getting rid of in_bd BNF property; tuned diff -r 21774f0b7bc0 -r 7c4b56bac189 src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Sat Jul 13 12:38:40 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Thu Jul 11 11:16:23 2013 +0200 @@ -16,14 +16,11 @@ lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" unfolding o_def by (auto split: sum.splits) -lemma sum_case_comp_Inl: "sum_case f g \ Inl = f" -unfolding comp_def by simp - lemma sum_case_expand_Inr: "f o Inl = g \ f x = sum_case g (f o Inr) x" by (auto split: sum.splits) lemma sum_case_expand_Inr': "f o Inl = g \ h = f o Inr \ sum_case g h = f" -by (metis sum_case_comp_Inl sum_case_o_inj(2) surjective_sum) +by (metis sum_case_o_inj(1,2) surjective_sum) lemma converse_Times: "(A \ B) ^-1 = B \ A" by auto diff -r 21774f0b7bc0 -r 7c4b56bac189 src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Sat Jul 13 12:38:40 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Thu Jul 11 11:16:23 2013 +0200 @@ -215,6 +215,16 @@ lemma insert_subsetI: "\x \ A; X \ A\ \ insert x X \ A" by auto +lemma If_the_inv_into_in_Func: + "\inj_on g C; g ` C \ A; C \ B \ {x}\ \ + (\i. if i \ A then if i \ g ` C then the_inv_into C g i else x else undefined) \ Func A (B \ {x})" +unfolding Func_def by (auto dest: the_inv_into_into) + +lemma If_the_inv_into_f_f: + "\inj_on g C; g ` C \ A; i \ C\ \ + ((\i. if i \ A then if i \ g ` C then the_inv_into C g i else x else undefined) o g) i = id i" +unfolding Func_def by (auto elim: the_inv_into_f_f) + (*helps resolution*) lemma well_order_induct_imp: "wo_rel r \ (\x. \y. y \ x \ (y, x) \ r \ y \ Field r \ P y \ x \ Field r \ P x) \ diff -r 21774f0b7bc0 -r 7c4b56bac189 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Sat Jul 13 12:38:40 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jul 11 11:16:23 2013 +0200 @@ -2191,7 +2191,7 @@ val dtor_corec_unique_thms = split_conj_thm (split_conj_prems n (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS corec_unique_mor_thm) - |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_comp_Inl} @ + |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @ map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); val ctor_dtor_corec_thms = diff -r 21774f0b7bc0 -r 7c4b56bac189 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sat Jul 13 12:38:40 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Jul 11 11:16:23 2013 +0200 @@ -201,7 +201,7 @@ (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1; fun mk_mor_sum_case_tac ks mor_UNIV = - (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm sum_case_comp_Inl[symmetric]})) ks) 1; + (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm sum_case_o_inj(1)[symmetric]})) ks) 1; fun mk_set_incl_hset_tac def rec_Suc = EVERY' (stac def :: diff -r 21774f0b7bc0 -r 7c4b56bac189 src/HOL/Cardinals/Cardinal_Arithmetic.thy --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Sat Jul 13 12:38:40 2013 +0200 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Thu Jul 11 11:16:23 2013 +0200 @@ -50,6 +50,10 @@ by (simp only: ordIso_refl card_of_Card_order) (*library candidate*) +lemma Field_card_order: "card_order r \ Field r = UNIV" +using card_order_on_Card_order[of UNIV r] by simp + +(*library candidate*) lemma card_of_Times_Plus_distrib: "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|") proof - @@ -59,8 +63,21 @@ qed (*library candidate*) -lemma Field_card_order: "card_order r \ Field r = UNIV" -using card_order_on_Card_order[of UNIV r] by simp +lemma Func_Times_Range: + "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|") +proof - + let ?F = "\fg. (\x. if x \ A then fst (fg x) else undefined, + \x. if x \ A then snd (fg x) else undefined)" + let ?G = "\(f, g) x. if x \ A then (f x, g x) else undefined" + have "bij_betw ?F ?LHS ?RHS" unfolding bij_betw_def inj_on_def + proof safe + fix f g assume "f \ Func A B" "g \ Func A C" + thus "(f, g) \ ?F ` Func A (B \ C)" + by (intro image_eqI[of _ _ "?G (f, g)"]) (auto simp: Func_def) + qed (auto simp: Func_def fun_eq_iff, metis pair_collapse) + thus ?thesis using card_of_ordIso by blast +qed + subsection {* Zero *} @@ -103,7 +120,7 @@ apply (simp only: card_of_empty3) done -subsection {* Infinite cardinals *} +subsection {* (In)finite cardinals *} definition cinfinite where "cinfinite r = infinite (Field r)" @@ -111,6 +128,16 @@ abbreviation Cinfinite where "Cinfinite r \ cinfinite r \ Card_order r" +definition cfinite where + "cfinite r = finite (Field r)" + +abbreviation Cfinite where + "Cfinite r \ cfinite r \ Card_order r" + +lemma Cfinite_ordLess_Cinfinite: "\Cfinite r; Cinfinite s\ \ r o r" @@ -138,6 +165,9 @@ definition csum (infixr "+c" 65) where "r1 +c r2 \ |Field r1 <+> Field r2|" +lemma Field_csum: "Field (r +c s) = Inl ` Field r \ Inr ` Field s" + unfolding csum_def Field_card_of by auto + lemma Card_order_csum: "Card_order (r1 +c r2)" unfolding csum_def by (simp add: card_of_Card_order) @@ -206,6 +236,24 @@ lemma csum_assoc: "(p1 +c p2) +c p3 =o p1 +c p2 +c p3" by (simp only: csum_def Field_card_of card_of_Plus_assoc) +lemma Cfinite_csum: "\Cfinite r; Cfinite s\ \ Cfinite (r +c s)" + unfolding cfinite_def csum_def Field_card_of using card_of_card_order_on by simp + +lemma csum_csum: "(r1 +c r2) +c (r3 +c r4) =o (r1 +c r3) +c (r2 +c r4)" +proof - + have "(r1 +c r2) +c (r3 +c r4) =o r1 +c r2 +c (r3 +c r4)" + by (metis csum_assoc) + also have "r1 +c r2 +c (r3 +c r4) =o r1 +c (r2 +c r3) +c r4" + by (metis csum_assoc csum_cong2 ordIso_symmetric) + also have "r1 +c (r2 +c r3) +c r4 =o r1 +c (r3 +c r2) +c r4" + by (metis csum_com csum_cong1 csum_cong2) + also have "r1 +c (r3 +c r2) +c r4 =o r1 +c r3 +c r2 +c r4" + by (metis csum_assoc csum_cong2 ordIso_symmetric) + also have "r1 +c r3 +c r2 +c r4 =o (r1 +c r3) +c (r2 +c r4)" + by (metis csum_assoc ordIso_symmetric) + finally show ?thesis . +qed + lemma Plus_csum: "|A <+> B| =o |A| +c |B|" by (simp only: csum_def Field_card_of card_of_refl) @@ -221,6 +269,9 @@ lemma Card_order_cone: "Card_order cone" unfolding cone_def by (rule card_of_Card_order) +lemma Cfinite_cone: "Cfinite cone" + unfolding cfinite_def by (simp add: Card_order_cone) + lemma single_cone: "|{x}| =o cone" proof - @@ -754,6 +805,68 @@ ultimately show "|?LHS| \o |?RHS|" using card_of_ordLeq by blast qed +lemma Cfinite_cprod_Cinfinite: "\Cfinite r; Cinfinite s\ \ r *c s \o s" +by (intro cprod_cinfinite_bound) + (auto intro: ordLeq_refl ordLess_imp_ordLeq[OF Cfinite_ordLess_Cinfinite]) + +lemma cprod_cexp: "(r *c s) ^c t =o r ^c t *c s ^c t" + unfolding cprod_def cexp_def Field_card_of by (rule Func_Times_Range) + +lemma cprod_cexp_csum_cexp_Cinfinite: + assumes t: "Cinfinite t" + shows "(r *c s) ^c t \o (r +c s) ^c t" +proof - + have "(r *c s) ^c t \o ((r +c s) ^c ctwo) ^c t" + by (rule cexp_mono1[OF cprod_csum_cexp conjunct2[OF t]]) + also have "((r +c s) ^c ctwo) ^c t =o (r +c s) ^c (ctwo *c t)" + by (rule cexp_cprod[OF Card_order_csum]) + also have "(r +c s) ^c (ctwo *c t) =o (r +c s) ^c (t *c ctwo)" + by (rule cexp_cong2[OF cprod_com Card_order_csum Card_order_cprod]) + also have "(r +c s) ^c (t *c ctwo) =o ((r +c s) ^c t) ^c ctwo" + by (rule ordIso_symmetric[OF cexp_cprod[OF Card_order_csum]]) + also have "((r +c s) ^c t) ^c ctwo =o (r +c s) ^c t" + by (rule cexp_cprod_ordLeq[OF Card_order_csum t ctwo_Cnotzero ctwo_ordLeq_Cinfinite[OF t]]) + finally show ?thesis . +qed + +lemma Cfinite_cexp_Cinfinite: + assumes s: "Cfinite s" and t: "Cinfinite t" + shows "s ^c t \o ctwo ^c t" +proof (cases "s \o ctwo") + case True thus ?thesis using t by (blast intro: cexp_mono1) +next + case False + hence "ctwo \o s" by (metis card_order_on_well_order_on ctwo_Cnotzero ordLeq_total s) + hence "Cnotzero s" by (metis Cnotzero_mono ctwo_Cnotzero s) + hence st: "Cnotzero (s *c t)" by (metis Cinfinite_cprod2 cinfinite_not_czero t) + have "s ^c t \o (ctwo ^c s) ^c t" + using assms by (blast intro: cexp_mono1 ordLess_imp_ordLeq[OF ordLess_ctwo_cexp]) + also have "(ctwo ^c s) ^c t =o ctwo ^c (s *c t)" + by (blast intro: Card_order_ctwo cexp_cprod) + also have "ctwo ^c (s *c t) \o ctwo ^c t" + using assms st by (intro cexp_mono2_Cnotzero Cfinite_cprod_Cinfinite Card_order_ctwo) + finally show ?thesis . +qed + +lemma csum_Cfinite_cexp_Cinfinite: + assumes r: "Card_order r" and s: "Cfinite s" and t: "Cinfinite t" + shows "(r +c s) ^c t \o (r +c ctwo) ^c t" +proof (cases "Cinfinite r") + case True + hence "r +c s =o r" by (intro csum_absorb1 ordLess_imp_ordLeq[OF Cfinite_ordLess_Cinfinite] s) + hence "(r +c s) ^c t =o r ^c t" using t by (blast intro: cexp_cong1) + also have "r ^c t \o (r +c ctwo) ^c t" using t by (blast intro: cexp_mono1 ordLeq_csum1 r) + finally show ?thesis . +next + case False + with r have "Cfinite r" unfolding cinfinite_def cfinite_def by auto + hence "Cfinite (r +c s)" by (intro Cfinite_csum s) + hence "(r +c s) ^c t \o ctwo ^c t" by (intro Cfinite_cexp_Cinfinite t) + also have "ctwo ^c t \o (r +c ctwo) ^c t" using t + by (blast intro: cexp_mono1 ordLeq_csum2 Card_order_ctwo) + finally show ?thesis . +qed + lemma card_of_Sigma_ordLeq_Cinfinite: "\Cinfinite r; |I| \o r; \i \ I. |A i| \o r\ \ |SIGMA i : I. A i| \o r" unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field)