# HG changeset patch # User traytel # Date 1366910300 -7200 # Node ID 84e7225f5ab68359113a4662c122f2b58bbecbaf # Parent 0504e286d66d60911fd7fd24072609ef8a59a6bd removed unnecessary assumptions in some theorems about cardinal exponentiation diff -r 0504e286d66d -r 84e7225f5ab6 src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Thu Apr 25 18:27:26 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Thu Apr 25 19:18:20 2013 +0200 @@ -224,9 +224,7 @@ unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1) lemma cpow_clists_czero: "\A \ Field (cpow (clists r)) - {{}}; |A| =o czero\ \ False" -unfolding cpow_def clists_def -by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric]) - (erule notE, erule ordIso_transitive, rule czero_ordIso) +unfolding cpow_def clists_def card_of_ordIso_czero_iff_empty by auto lemma incl_UNION_I: assumes "i \ I" and "A \ F i" diff -r 0504e286d66d -r 84e7225f5ab6 src/HOL/BNF/Basic_BNFs.thy --- a/src/HOL/BNF/Basic_BNFs.thy Thu Apr 25 18:27:26 2013 +0200 +++ b/src/HOL/BNF/Basic_BNFs.thy Thu Apr 25 19:18:20 2013 +0200 @@ -42,12 +42,6 @@ apply (rule cexp_mono1) apply (rule ordLeq_csum1) apply (rule card_of_Card_order) -apply (rule disjI2) -apply (rule cone_ordLeq_cexp) -apply (rule ordLeq_transitive) -apply (rule cone_ordLeq_ctwo) -apply (rule ordLeq_csum2) -apply (rule Card_order_ctwo) apply (rule natLeq_Card_order) done @@ -277,12 +271,6 @@ apply (rule Cinfinite_Cnotzero) apply (rule conjI[OF _ natLeq_Card_order]) apply (rule natLeq_cinfinite) - apply (rule disjI2) - apply (rule cone_ordLeq_cexp) - apply (rule ordLeq_transitive) - apply (rule cone_ordLeq_ctwo) - apply (rule ordLeq_csum2) - apply (rule Card_order_ctwo) apply (rule notE) apply (rule ctwo_not_czero) apply assumption @@ -378,9 +366,6 @@ apply (rule cexp_mono) apply (rule ordLeq_csum1) apply (rule card_of_Card_order) apply (rule ordLeq_csum2) apply (rule card_of_Card_order) - apply (rule disjI2) apply (rule cone_ordLeq_cexp) - apply (rule ordLeq_transitive) apply (rule cone_ordLeq_ctwo) apply (rule ordLeq_csum2) - apply (rule Card_order_ctwo) apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast apply (rule card_of_Card_order) done diff -r 0504e286d66d -r 84e7225f5ab6 src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Thu Apr 25 18:27:26 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Thu Apr 25 19:18:20 2013 +0200 @@ -139,14 +139,9 @@ apply (rule card_of_nat) apply (rule Card_order_ctwo) apply (rule card_of_Card_order) - apply (rule natLeq_Card_order) - apply (rule disjI1) - apply (rule ctwo_Cnotzero) apply (rule cexp_mono1) apply (rule ordLeq_csum2) apply (rule Card_order_ctwo) - apply (rule disjI1) - apply (rule ctwo_Cnotzero) apply (rule natLeq_Card_order) apply (rule ordIso_ordLeq_trans) apply (rule card_of_Func) @@ -155,14 +150,9 @@ apply (rule card_of_nat) apply (rule card_of_Card_order) apply (rule card_of_Card_order) - apply (rule natLeq_Card_order) - apply (rule disjI1) - apply (erule not_emp_czero_notIn_ordIso_Card_order) apply (rule cexp_mono1) apply (rule ordLeq_csum1) apply (rule card_of_Card_order) - apply (rule disjI1) - apply (erule not_emp_czero_notIn_ordIso_Card_order) apply (rule natLeq_Card_order) apply (rule card_of_Card_order) apply (rule card_of_Card_order) @@ -405,11 +395,8 @@ also have "|{X. X \ A \ countable X} - {{}}| \o |A| ^c natLeq" using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto also have "|A| ^c natLeq \o ( |A| +c ctwo) ^c natLeq" - apply(rule cexp_mono1_cone_ordLeq) + apply(rule cexp_mono1) apply(rule ordLeq_csum1, rule card_of_Card_order) - apply (rule cone_ordLeq_cexp) - apply (rule cone_ordLeq_Cnotzero) - using csum_Cnotzero2 ctwo_Cnotzero apply blast by (rule natLeq_Card_order) finally show ?thesis . qed diff -r 0504e286d66d -r 84e7225f5ab6 src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Thu Apr 25 18:27:26 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Thu Apr 25 19:18:20 2013 +0200 @@ -644,8 +644,8 @@ map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf); val in_bd = @{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf, - @{thm cexp_cong2_Cnotzero} OF [bd_ordIso, if live = 0 then - @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2}, + @{thm cexp_cong2} OF [bd_ordIso, if live = 0 then + @{thm Card_order_ctwo} else @{thm Card_order_csum}, bd_Card_order_of_bnf bnf]]; fun mk_tac thm {context = ctxt, prems = _} = diff -r 0504e286d66d -r 84e7225f5ab6 src/HOL/BNF/Tools/bnf_comp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Apr 25 18:27:26 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Apr 25 19:18:20 2013 +0200 @@ -205,13 +205,9 @@ rtac Card_order_ctwo THEN' (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE' rtac (hd Fbd_Cinfs)) THEN' - rtac disjI1 THEN' - TRY o rtac csum_Cnotzero2 THEN' - rtac ctwo_Cnotzero THEN' rtac Gbd_Card_order THEN' rtac @{thm cexp_cprod} THEN' - TRY o rtac csum_Cnotzero2 THEN' - rtac ctwo_Cnotzero) 1 + rtac @{thm Card_order_csum}) 1 end; val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def @@ -300,13 +296,6 @@ else all_tac) THEN (rtac @{thm csum_com} THEN' rtac bd_Card_order THEN' - rtac disjI1 THEN' - rtac csum_Cnotzero2 THEN' - rtac ctwo_Cnotzero THEN' - rtac disjI1 THEN' - rtac csum_Cnotzero2 THEN' - TRY o rtac csum_Cnotzero1 THEN' - rtac Cnotzero_UNIV THEN' rtac @{thm ordLeq_ordIso_trans} THEN' rtac @{thm cexp_mono1} THEN' rtac ctrans THEN' @@ -322,14 +311,9 @@ ((rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl}) ORELSE' (rtac Card_order_csum THEN' rtac ordLeq_csum2)) THEN' rtac Card_order_ctwo THEN' - rtac disjI1 THEN' - rtac csum_Cnotzero2 THEN' - TRY o rtac csum_Cnotzero1 THEN' - rtac Cnotzero_UNIV THEN' rtac bd_Card_order THEN' rtac @{thm cexp_cprod_ordLeq} THEN' - TRY o rtac csum_Cnotzero2 THEN' - rtac ctwo_Cnotzero THEN' + resolve_tac @{thms Card_order_csum Card_order_ctwo} THEN' rtac @{thm Cinfinite_cprod2} THEN' TRY o rtac csum_Cnotzero1 THEN' rtac Cnotzero_UNIV THEN' @@ -374,8 +358,7 @@ (rtac ordLeq_csum2 THEN' (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) ORELSE (rtac ordLeq_csum2 THEN' rtac Card_order_ctwo) 1) THEN - (rtac disjI1 THEN' TRY o rtac csum_Cnotzero2 THEN' rtac ctwo_Cnotzero - THEN' rtac bd_Card_order) 1; + (rtac bd_Card_order) 1; @@ -399,13 +382,7 @@ FIRST' [rtac card_of_Card_order, rtac Card_order_csum]) ordIso_transitive @{thm csum_assoc} @{thm csum_com} @{thm csum_cong} src dest THEN' - rtac bd_Card_order THEN' - rtac disjI1 THEN' - TRY o rtac csum_Cnotzero2 THEN' - rtac ctwo_Cnotzero THEN' - rtac disjI1 THEN' - TRY o rtac csum_Cnotzero2 THEN' - rtac ctwo_Cnotzero) 1; + rtac bd_Card_order) 1; fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull = (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN diff -r 0504e286d66d -r 84e7225f5ab6 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Apr 25 18:27:26 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Apr 25 19:18:20 2013 +0200 @@ -1082,7 +1082,7 @@ 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 _ csum_Cnotzero2[OF ctwo_Cnotzero]]]})); + cexp_mono2_Cnotzero[OF _ Card_order_csum]]})); val in_sbds = map4 mk_in_sbd ks bd_Card_orders bd_Cnotzeros in_bds; in (lthy, sbd, sbdT, diff -r 0504e286d66d -r 84e7225f5ab6 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Apr 25 18:27:26 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Apr 25 19:18:20 2013 +0200 @@ -462,15 +462,15 @@ rtac ctrans, rtac @{thm card_of_diff}, rtac ordIso_ordLeq_trans, rtac @{thm card_of_Field_ordIso}, rtac @{thm Card_order_cpow}, rtac ordIso_ordLeq_trans, - rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1_Cnotzero}, + rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1}, if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2}, - rtac @{thm Card_order_ctwo}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_clists}, + rtac @{thm Card_order_ctwo}, rtac @{thm Card_order_clists}, rtac @{thm cexp_mono2_Cnotzero}, rtac ordIso_ordLeq_trans, rtac @{thm clists_Cinfinite}, if n = 1 then rtac sbd_Cinfinite else rtac (sbd_Cinfinite RS @{thm Cinfinite_csum1}), rtac ordIso_ordLeq_trans, rtac sbd_sbd, rtac @{thm infinite_ordLeq_cexp}, rtac sbd_Cinfinite, - if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]}, + if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum}, rtac @{thm Cnotzero_clists}, rtac ballI, rtac ordIso_ordLeq_trans, rtac @{thm card_of_Func_Ffunc}, rtac ordIso_ordLeq_trans, rtac @{thm Func_cexp}, @@ -480,26 +480,22 @@ (sbd_Cinfinite RS @{thm Cinfinite_cexp[OF ordLeq_csum2[OF Card_order_ctwo]]} RSN (3, @{thm Un_Cinfinite_bound})))) (fn thm => EVERY' [rtac ctrans, rtac @{thm card_of_image}, rtac thm]) (rev in_sbds), - rtac @{thm cexp_cong1_Cnotzero}, rtac @{thm csum_cong1}, + rtac @{thm cexp_cong1}, rtac @{thm csum_cong1}, REPEAT_DETERM_N m o rtac @{thm csum_cong2}, CONJ_WRAP_GEN' (rtac @{thm csum_cong}) (K (rtac (sbd_Card_order RS @{thm card_of_Field_ordIso}))) in_sbds, rtac sbd_Card_order, - rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, - rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac @{thm ordLeq_ordIso_trans}, etac @{thm clists_bound}, rtac @{thm clists_Cinfinite}, TRY o rtac @{thm Cinfinite_csum1}, rtac sbd_Cinfinite, - rtac disjI2, rtac @{thm cone_ordLeq_cexp}, rtac @{thm cone_ordLeq_cexp}, - rtac ctrans, rtac @{thm cone_ordLeq_ctwo}, rtac @{thm ordLeq_csum2}, - rtac @{thm Card_order_ctwo}, rtac FalseE, etac @{thm cpow_clists_czero}, atac, + rtac FalseE, etac @{thm cpow_clists_czero}, atac, rtac @{thm card_of_Card_order}, rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod}, - rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, - rtac ordIso_ordLeq_trans, rtac @{thm cexp_cong2_Cnotzero}, + rtac @{thm Card_order_csum}, + rtac ordIso_ordLeq_trans, rtac @{thm cexp_cong2}, rtac @{thm ordIso_transitive}, rtac @{thm cprod_cong2}, rtac sbd_sbd, rtac @{thm cprod_infinite}, rtac sbd_Cinfinite, - rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_cprod}, - rtac ctrans, rtac @{thm cexp_mono1_Cnotzero}, + rtac @{thm Card_order_csum}, rtac @{thm Card_order_cprod}, + rtac ctrans, rtac @{thm cexp_mono1}, rtac ordIso_ordLeq_trans, rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1}, rtac @{thm ordIso_transitive}, REPEAT_DETERM_N m o rtac @{thm csum_cong2}, @@ -513,14 +509,13 @@ rtac @{thm csum_com}, rtac @{thm csum_cexp'}, rtac sbd_Cinfinite, if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum}, if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2}, - rtac @{thm Card_order_ctwo}, - rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac sbd_Card_order, + rtac @{thm Card_order_ctwo}, rtac sbd_Card_order, rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod_ordLeq}, - if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]}, + if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum}, rtac sbd_Cinfinite, rtac sbd_Cnotzero, rtac @{thm ordLeq_refl}, rtac sbd_Card_order, rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm infinite_ordLeq_cexp}, rtac sbd_Cinfinite, - if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]}, + if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum}, rtac sbd_Cnotzero, rtac @{thm card_of_mono1}, rtac subsetI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac, @@ -1328,7 +1323,7 @@ rtac @{thm card_of_image}, rtac ordIso_ordLeq_trans, rtac @{thm card_of_ordIso_subst}, rtac @{thm sym[OF proj_image]}, rtac ctrans, rtac @{thm card_of_image}, rtac ctrans, rtac card_of_carT, rtac @{thm cexp_mono2_Cnotzero}, - rtac @{thm cexp_ordLeq_ccexp}, rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, + rtac @{thm cexp_ordLeq_ccexp}, rtac @{thm Card_order_csum}, rtac @{thm Cnotzero_cexp}, rtac sbd_Cnotzero, rtac sbd_Card_order, rtac @{thm card_of_mono1}, rtac subsetI, rtac @{thm image_eqI}, rtac sym, rtac Rep_inverse, REPEAT_DETERM o eresolve_tac [CollectE, conjE], diff -r 0504e286d66d -r 84e7225f5ab6 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Apr 25 18:27:26 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Apr 25 19:18:20 2013 +0200 @@ -552,8 +552,7 @@ 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 _ csum_Cnotzero2[OF ctwo_Cnotzero]]]})); + (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; val sum_bd = Library.foldr1 (uncurry mk_csum) bds; @@ -575,9 +574,7 @@ val Asuc_bd_Cinfinite = suc_bd_Cinfinite RS (basis_Asuc RS @{thm Cinfinite_cexp}); val Asuc_bd_Cnotzero = Asuc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero}; - val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF - ordLess_ctwo_cexp - cexp_mono1_Cnotzero[OF _ ctwo_Cnotzero]]} OF + val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF ordLess_ctwo_cexp cexp_mono1]} OF [suc_bd_Card_order, basis_Asuc, suc_bd_Card_order]; val Asuc_bdT = fst (dest_relT (fastype_of (mk_Asuc_bd As))); diff -r 0504e286d66d -r 84e7225f5ab6 src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Apr 25 18:27:26 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Apr 25 19:18:20 2013 +0200 @@ -312,18 +312,17 @@ fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, etac min_alg, rtac @{thm Un_Cinfinite_bound}, minG_tac, rtac ctrans, rtac @{thm card_of_image}, rtac ctrans, rtac in_bd, rtac ctrans, - rtac @{thm cexp_mono1_Cnotzero}, rtac @{thm csum_mono1}, + rtac @{thm cexp_mono1}, rtac @{thm csum_mono1}, REPEAT_DETERM_N m o rtac @{thm csum_mono2}, CONJ_WRAP_GEN' (rtac @{thm csum_cinfinite_bound}) (K minG_tac) min_algs, REPEAT_DETERM o FIRST' - [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}, rtac Asuc_Cinfinite], - rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac bd_Card_order, - rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1_Cnotzero}, absorbAs_tac, + [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}, + rtac Asuc_Cinfinite, rtac bd_Card_order], + rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1}, absorbAs_tac, rtac @{thm csum_absorb1}, rtac Asuc_Cinfinite, rtac @{thm ctwo_ordLeq_Cinfinite}, rtac Asuc_Cinfinite, rtac bd_Card_order, - rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac Asuc_Cnotzero, rtac @{thm ordIso_imp_ordLeq}, rtac @{thm cexp_cprod_ordLeq}, - TRY o rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac suc_Cinfinite, + resolve_tac @{thms Card_order_csum Card_order_ctwo}, rtac suc_Cinfinite, rtac bd_Cnotzero, rtac @{thm cardSuc_ordLeq}, rtac bd_Card_order, rtac Asuc_Cinfinite]; in (rtac induct THEN' @@ -753,8 +752,8 @@ fun mk_in_bd_tac sum_Card_order sucbd_Cnotzero incl card_of_min_alg = EVERY' [rtac ctrans, rtac @{thm card_of_mono1}, rtac subsetI, etac rev_mp, rtac incl, rtac ctrans, rtac card_of_min_alg, rtac @{thm cexp_mono2_Cnotzero}, - rtac @{thm cardSuc_ordLeq_cpow}, rtac sum_Card_order, rtac @{thm csum_Cnotzero2}, - rtac @{thm ctwo_Cnotzero}, rtac sucbd_Cnotzero] 1; + rtac @{thm cardSuc_ordLeq_cpow}, rtac sum_Card_order, rtac @{thm Card_order_csum}, + rtac sucbd_Cnotzero] 1; fun mk_bd_card_order_tac bd_card_orders = (rtac @{thm card_order_cpow} THEN' diff -r 0504e286d66d -r 84e7225f5ab6 src/HOL/Cardinals/Cardinal_Arithmetic.thy --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Thu Apr 25 18:27:26 2013 +0200 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Thu Apr 25 19:18:20 2013 +0200 @@ -72,8 +72,8 @@ using card_of_empty_ordIso by (simp add: czero_def) lemma card_of_ordIso_czero_iff_empty: - "|A| =o (czero :: 'a rel) \ A = ({} :: 'a set)" -unfolding czero_def by (rule iffI[OF card_of_empty2]) (auto simp: card_of_refl) + "|A| =o (czero :: 'b rel) \ A = ({} :: 'a set)" +unfolding czero_def by (rule iffI[OF card_of_empty2]) (auto simp: card_of_refl card_of_empty_ordIso) (* A "not czero" Cardinal predicate *) abbreviation Cnotzero where @@ -389,8 +389,7 @@ lemma cexp_mono': assumes 1: "p1 \o r1" and 2: "p2 \o r2" - and n1: "Field p1 \ {} \ cone \o r1 ^c r2" - and n2: "Field p2 = {} \ Field r2 = {}" + and n: "Field p2 = {} \ Field r2 = {}" shows "p1 ^c p2 \o r1 ^c r2" proof(cases "Field p1 = {}") case True @@ -399,7 +398,18 @@ by (cases "Field p2 = {}", auto intro: card_of_ordLeqI2 simp: Func_empty) (metis Func_is_emp card_of_empty ex_in_conv) hence "p1 ^c p2 \o cone" by (simp add: Field_card_of cexp_def) - thus ?thesis using True n1 ordLeq_transitive by auto + thus ?thesis + proof (cases "Field p2 = {}") + case True + with n have "Field r2 = {}" . + hence "cone \o r1 ^c r2" unfolding cone_def cexp_def Func_def by (auto intro: card_of_ordLeqI) + thus ?thesis using `p1 ^c p2 \o cone` ordLeq_transitive by auto + next + case False with True have "|Field (p1 ^c p2)| =o czero" + unfolding card_of_ordIso_czero_iff_empty cexp_def Func_is_emp Field_card_of by blast + thus ?thesis unfolding cexp_def card_of_ordIso_czero_iff_empty Field_card_of + by (simp add: card_of_empty) + qed next case False have 1: "|Field p1| \o |Field r1|" and 2: "|Field p2| \o |Field r2|" @@ -409,7 +419,7 @@ obtain f2 where f2: "inj_on f2 (Field p2)" "f2 ` Field p2 \ Field r2" using 2 unfolding card_of_ordLeq[symmetric] by blast have 0: "Func_map (Field p2) f1 f2 ` (Field (r1 ^c r2)) = Field (p1 ^c p2)" - unfolding cexp_def Field_card_of using Func_map_surj[OF f1 f2 n2, symmetric] . + unfolding cexp_def Field_card_of using Func_map_surj[OF f1 f2 n, symmetric] . have 00: "Field (p1 ^c p2) \ {}" unfolding cexp_def Field_card_of Func_is_emp using False by simp show ?thesis @@ -418,57 +428,36 @@ lemma cexp_mono: assumes 1: "p1 \o r1" and 2: "p2 \o r2" - and n1: "Cnotzero p1 \ cone \o r1 ^c r2" - and n2: "p2 =o czero \ r2 =o czero" and card: "Card_order p2" + and n: "p2 =o czero \ r2 =o czero" and card: "Card_order p2" shows "p1 ^c p2 \o r1 ^c r2" -proof (rule cexp_mono'[OF 1 2]) - show "Field p1 \ {} \ cone \o r1 ^c r2" - proof (cases "Cnotzero p1") - case True show ?thesis using Cnotzero_imp_not_empty[OF True] by (rule disjI1) - next - case False with n1 show ?thesis by blast - qed -qed (rule czeroI[OF card, THEN n2, THEN czeroE]) + by (metis (full_types) "1" "2" card cexp_mono' czeroE czeroI n) lemma cexp_mono1: - assumes 1: "p1 \o r1" - and n1: "Cnotzero p1 \ cone \o r1 ^c q" and q: "Card_order q" + assumes 1: "p1 \o r1" and q: "Card_order q" shows "p1 ^c q \o r1 ^c q" -using ordLeq_refl[OF q] by (rule cexp_mono[OF 1 _ n1]) (auto simp: q) - -lemma cexp_mono1_Cnotzero: "\p1 \o r1; Cnotzero p1; Card_order q\ \ p1 ^c q \o r1 ^c q" -by (simp add: cexp_mono1) - -lemma cexp_mono1_cone_ordLeq: "\p1 \o r1; cone \o r1 ^c q; Card_order q\ \ p1 ^c q \o r1 ^c q" -using assms by (simp add: cexp_mono1) +using ordLeq_refl[OF q] by (rule cexp_mono[OF 1]) (auto simp: q) lemma cexp_mono2': assumes 2: "p2 \o r2" and q: "Card_order q" - and n1: "Field q \ {} \ cone \o q ^c r2" - and n2: "Field p2 = {} \ Field r2 = {}" + and n: "Field p2 = {} \ Field r2 = {}" shows "q ^c p2 \o q ^c r2" -using ordLeq_refl[OF q] by (rule cexp_mono'[OF _ 2 n1 n2]) auto +using ordLeq_refl[OF q] by (rule cexp_mono'[OF _ 2 n]) auto lemma cexp_mono2: assumes 2: "p2 \o r2" and q: "Card_order q" - and n1: "Cnotzero q \ cone \o q ^c r2" - and n2: "p2 =o czero \ r2 =o czero" and card: "Card_order p2" + and n: "p2 =o czero \ r2 =o czero" and card: "Card_order p2" shows "q ^c p2 \o q ^c r2" -using ordLeq_refl[OF q] by (rule cexp_mono[OF _ 2 n1 n2 card]) auto +using ordLeq_refl[OF q] by (rule cexp_mono[OF _ 2 n card]) auto lemma cexp_mono2_Cnotzero: - assumes "p2 \o r2" "Cnotzero q" and n2: "Cnotzero p2" + assumes "p2 \o r2" "Card_order q" "Cnotzero p2" shows "q ^c p2 \o q ^c r2" -proof (rule cexp_mono) - assume *: "p2 =o czero" - have False using n2 czeroI czeroE[OF *] by blast - thus "r2 =o czero" by blast -qed (auto simp add: assms ordLeq_refl) +by (metis assms cexp_mono2' czeroI) lemma cexp_cong: assumes 1: "p1 =o r1" and 2: "p2 =o r2" - and p1: "Cnotzero p1 \ cone \o r1 ^c r2" and Cr: "Card_order r2" - and r1: "Cnotzero r1 \ cone \o p1 ^c p2" and Cp: "Card_order p2" + and Cr: "Card_order r2" + and Cp: "Card_order p2" shows "p1 ^c p2 =o r1 ^c r2" proof - obtain f where "bij_betw f (Field p2) (Field r2)" @@ -478,32 +467,16 @@ and p: "r2 =o czero \ p2 =o czero" using 0 Cr Cp czeroE czeroI by auto show ?thesis using 0 1 2 unfolding ordIso_iff_ordLeq - using r p cexp_mono[OF _ _ p1 _ Cp] cexp_mono[OF _ _ r1 _ Cr] - by blast + using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by blast qed lemma cexp_cong1: assumes 1: "p1 =o r1" and q: "Card_order q" - and p1: "Cnotzero p1 \ cone \o r1 ^c q" - and r1: "Cnotzero r1 \ cone \o p1 ^c q" shows "p1 ^c q =o r1 ^c q" -by (rule cexp_cong[OF 1 _ p1 q r1 q]) (rule ordIso_refl[OF q]) - -lemma cexp_cong1_Cnotzero: - assumes "p1 =o r1" "Card_order q" "Cnotzero p1" "Cnotzero r1" - shows "p1 ^c q =o r1 ^c q" -by (rule cexp_cong1, auto simp add: assms) +by (rule cexp_cong[OF 1 _ q q]) (rule ordIso_refl[OF q]) lemma cexp_cong2: - assumes 2: "p2 =o r2" and q: "Card_order q" - and p: "Card_order p2" and r: "Card_order r2" - shows "Cnotzero q \ (cone \o q ^c p2 \ cone \o q ^c r2) \ - q ^c p2 =o q ^c r2" -by (rule cexp_cong[OF _ 2]) (auto simp only: ordIso_refl q p r) - -lemma cexp_cong2_Cnotzero: - assumes 2: "p2 =o r2" and q: "Cnotzero q" - and p: "Card_order p2" + assumes 2: "p2 =o r2" and q: "Card_order q" and p: "Card_order p2" shows "q ^c p2 =o q ^c r2" by (rule cexp_cong[OF _ 2]) (auto simp only: ordIso_refl Card_order_ordIso2[OF p 2] q p) @@ -523,7 +496,7 @@ qed lemma cexp_cprod: - assumes r1: "Cnotzero r1" + assumes r1: "Card_order r1" shows "(r1 ^c r2) ^c r3 =o r1 ^c (r2 *c r3)" (is "?L =o ?R") proof - have "?L =o r1 ^c (r3 *c r2)" @@ -535,7 +508,7 @@ qed lemma cexp_cprod_ordLeq: - assumes r1: "Cnotzero r1" and r2: "Cinfinite r2" + assumes r1: "Card_order r1" and r2: "Cinfinite r2" and r3: "Cnotzero r3" "r3 \o r2" shows "(r1 ^c r2) ^c r3 =o r1 ^c r2" (is "?L =o ?R") proof- @@ -580,14 +553,6 @@ apply (rule cone_ordLeq_Cnotzero) apply (rule assms(1)) apply (rule assms(2)) - apply (rule disjI1) - apply (rule conjI) - apply (rule notI) - apply (erule notE) - apply (rule ordIso_transitive) - apply assumption - apply (rule czero_ordIso) - apply (rule assms(2)) apply (rule notE) apply (rule cone_not_czero) apply assumption @@ -609,8 +574,6 @@ apply (rule assms(2)) apply (rule cexp_mono1) apply (rule assms(1)) - apply (rule disjI1) - apply (rule ctwo_Cnotzero) apply (rule assms(2)) done qed @@ -649,9 +612,6 @@ apply (rule conjunct2) apply (rule assms(1)) apply (rule assms(2)) - apply (simp only: card_of_Card_order czero_def) - apply (rule disjI1) - apply (rule assms(1)) apply (rule cexp_czero) done qed @@ -752,17 +712,6 @@ apply (rule ordLeq_csum1) apply (erule conjunct2) apply assumption -apply (rule disjI2) -apply (rule ordLeq_transitive) -apply (rule cone_ordLeq_ctwo) -apply (rule ordLeq_transitive) -apply assumption -apply (rule ordLeq_cexp1) -apply (rule Cinfinite_Cnotzero) -apply (rule Cinfinite_csum) -apply (rule disjI1) -apply assumption -apply assumption apply (rule notE) apply (rule cinfinite_not_czero[of r1]) apply (erule conjunct1) @@ -772,17 +721,6 @@ apply (rule ordLeq_csum2) apply (erule conjunct2) apply assumption -apply (rule disjI2) -apply (rule ordLeq_transitive) -apply (rule cone_ordLeq_ctwo) -apply (rule ordLeq_transitive) -apply assumption -apply (rule ordLeq_cexp1) -apply (rule Cinfinite_Cnotzero) -apply (rule Cinfinite_csum) -apply (rule disjI1) -apply assumption -apply assumption apply (rule notE) apply (rule cinfinite_not_czero[of r2]) apply (erule conjunct1)