--- 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: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> 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 \<in> I" and "A \<subseteq> F i"
--- 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
--- 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 \<subseteq> A \<and> countable X} - {{}}| \<le>o |A| ^c natLeq"
using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto
also have "|A| ^c natLeq \<le>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
--- 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 = _} =
--- 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
--- 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,
--- 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],
--- 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)));
--- 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'
--- 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) \<longleftrightarrow> A = ({} :: 'a set)"
-unfolding czero_def by (rule iffI[OF card_of_empty2]) (auto simp: card_of_refl)
+ "|A| =o (czero :: 'b rel) \<longleftrightarrow> 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 \<le>o r1" and 2: "p2 \<le>o r2"
- and n1: "Field p1 \<noteq> {} \<or> cone \<le>o r1 ^c r2"
- and n2: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
+ and n: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
shows "p1 ^c p2 \<le>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 \<le>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 \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def by (auto intro: card_of_ordLeqI)
+ thus ?thesis using `p1 ^c p2 \<le>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| \<le>o |Field r1|" and 2: "|Field p2| \<le>o |Field r2|"
@@ -409,7 +419,7 @@
obtain f2 where f2: "inj_on f2 (Field p2)" "f2 ` Field p2 \<subseteq> 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) \<noteq> {}" 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 \<le>o r1" and 2: "p2 \<le>o r2"
- and n1: "Cnotzero p1 \<or> cone \<le>o r1 ^c r2"
- and n2: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
+ and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
shows "p1 ^c p2 \<le>o r1 ^c r2"
-proof (rule cexp_mono'[OF 1 2])
- show "Field p1 \<noteq> {} \<or> cone \<le>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 \<le>o r1"
- and n1: "Cnotzero p1 \<or> cone \<le>o r1 ^c q" and q: "Card_order q"
+ assumes 1: "p1 \<le>o r1" and q: "Card_order q"
shows "p1 ^c q \<le>o r1 ^c q"
-using ordLeq_refl[OF q] by (rule cexp_mono[OF 1 _ n1]) (auto simp: q)
-
-lemma cexp_mono1_Cnotzero: "\<lbrakk>p1 \<le>o r1; Cnotzero p1; Card_order q\<rbrakk> \<Longrightarrow> p1 ^c q \<le>o r1 ^c q"
-by (simp add: cexp_mono1)
-
-lemma cexp_mono1_cone_ordLeq: "\<lbrakk>p1 \<le>o r1; cone \<le>o r1 ^c q; Card_order q\<rbrakk> \<Longrightarrow> p1 ^c q \<le>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 \<le>o r2" and q: "Card_order q"
- and n1: "Field q \<noteq> {} \<or> cone \<le>o q ^c r2"
- and n2: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
+ and n: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
shows "q ^c p2 \<le>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 \<le>o r2" and q: "Card_order q"
- and n1: "Cnotzero q \<or> cone \<le>o q ^c r2"
- and n2: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
+ and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
shows "q ^c p2 \<le>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 \<le>o r2" "Cnotzero q" and n2: "Cnotzero p2"
+ assumes "p2 \<le>o r2" "Card_order q" "Cnotzero p2"
shows "q ^c p2 \<le>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 \<or> cone \<le>o r1 ^c r2" and Cr: "Card_order r2"
- and r1: "Cnotzero r1 \<or> cone \<le>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 \<Longrightarrow> 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 \<or> cone \<le>o r1 ^c q"
- and r1: "Cnotzero r1 \<or> cone \<le>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 \<or> (cone \<le>o q ^c p2 \<and> cone \<le>o q ^c r2) \<Longrightarrow>
- 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 \<le>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)