removed unnecessary assumptions in some theorems about cardinal exponentiation
authortraytel
Thu Apr 25 19:18:20 2013 +0200 (2013-04-25)
changeset 5178284e7225f5ab6
parent 51781 0504e286d66d
child 51783 f4a00cdae743
removed unnecessary assumptions in some theorems about cardinal exponentiation
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/Basic_BNFs.thy
src/HOL/BNF/More_BNFs.thy
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_comp_tactics.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
src/HOL/Cardinals/Cardinal_Arithmetic.thy
     1.1 --- a/src/HOL/BNF/BNF_GFP.thy	Thu Apr 25 18:27:26 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Thu Apr 25 19:18:20 2013 +0200
     1.3 @@ -224,9 +224,7 @@
     1.4  unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1)
     1.5  
     1.6  lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
     1.7 -unfolding cpow_def clists_def
     1.8 -by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric])
     1.9 -   (erule notE, erule ordIso_transitive, rule czero_ordIso)
    1.10 +unfolding cpow_def clists_def card_of_ordIso_czero_iff_empty by auto
    1.11  
    1.12  lemma incl_UNION_I:
    1.13  assumes "i \<in> I" and "A \<subseteq> F i"
     2.1 --- a/src/HOL/BNF/Basic_BNFs.thy	Thu Apr 25 18:27:26 2013 +0200
     2.2 +++ b/src/HOL/BNF/Basic_BNFs.thy	Thu Apr 25 19:18:20 2013 +0200
     2.3 @@ -42,12 +42,6 @@
     2.4  apply (rule cexp_mono1)
     2.5  apply (rule ordLeq_csum1)
     2.6  apply (rule card_of_Card_order)
     2.7 -apply (rule disjI2)
     2.8 -apply (rule cone_ordLeq_cexp)
     2.9 -apply (rule ordLeq_transitive)
    2.10 -apply (rule cone_ordLeq_ctwo)
    2.11 -apply (rule ordLeq_csum2)
    2.12 -apply (rule Card_order_ctwo)
    2.13  apply (rule natLeq_Card_order)
    2.14  done
    2.15  
    2.16 @@ -277,12 +271,6 @@
    2.17      apply (rule Cinfinite_Cnotzero)
    2.18      apply (rule conjI[OF _ natLeq_Card_order])
    2.19      apply (rule natLeq_cinfinite)
    2.20 -    apply (rule disjI2)
    2.21 -    apply (rule cone_ordLeq_cexp)
    2.22 -    apply (rule ordLeq_transitive)
    2.23 -    apply (rule cone_ordLeq_ctwo)
    2.24 -    apply (rule ordLeq_csum2)
    2.25 -    apply (rule Card_order_ctwo)
    2.26      apply (rule notE)
    2.27      apply (rule ctwo_not_czero)
    2.28      apply assumption
    2.29 @@ -378,9 +366,6 @@
    2.30      apply (rule cexp_mono)
    2.31       apply (rule ordLeq_csum1) apply (rule card_of_Card_order)
    2.32       apply (rule ordLeq_csum2) apply (rule card_of_Card_order)
    2.33 -     apply (rule disjI2) apply (rule cone_ordLeq_cexp)
    2.34 -      apply (rule ordLeq_transitive) apply (rule cone_ordLeq_ctwo) apply (rule ordLeq_csum2)
    2.35 -      apply (rule Card_order_ctwo)
    2.36       apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast
    2.37       apply (rule card_of_Card_order)
    2.38    done
     3.1 --- a/src/HOL/BNF/More_BNFs.thy	Thu Apr 25 18:27:26 2013 +0200
     3.2 +++ b/src/HOL/BNF/More_BNFs.thy	Thu Apr 25 19:18:20 2013 +0200
     3.3 @@ -139,14 +139,9 @@
     3.4        apply (rule card_of_nat)
     3.5        apply (rule Card_order_ctwo)
     3.6        apply (rule card_of_Card_order)
     3.7 -      apply (rule natLeq_Card_order)
     3.8 -      apply (rule disjI1)
     3.9 -      apply (rule ctwo_Cnotzero)
    3.10        apply (rule cexp_mono1)
    3.11        apply (rule ordLeq_csum2)
    3.12        apply (rule Card_order_ctwo)
    3.13 -      apply (rule disjI1)
    3.14 -      apply (rule ctwo_Cnotzero)
    3.15        apply (rule natLeq_Card_order)
    3.16        apply (rule ordIso_ordLeq_trans)
    3.17        apply (rule card_of_Func)
    3.18 @@ -155,14 +150,9 @@
    3.19        apply (rule card_of_nat)
    3.20        apply (rule card_of_Card_order)
    3.21        apply (rule card_of_Card_order)
    3.22 -      apply (rule natLeq_Card_order)
    3.23 -      apply (rule disjI1)
    3.24 -      apply (erule not_emp_czero_notIn_ordIso_Card_order)
    3.25        apply (rule cexp_mono1)
    3.26        apply (rule ordLeq_csum1)
    3.27        apply (rule card_of_Card_order)
    3.28 -      apply (rule disjI1)
    3.29 -      apply (erule not_emp_czero_notIn_ordIso_Card_order)
    3.30        apply (rule natLeq_Card_order)
    3.31        apply (rule card_of_Card_order)
    3.32        apply (rule card_of_Card_order)
    3.33 @@ -405,11 +395,8 @@
    3.34    also have "|{X. X \<subseteq> A \<and> countable X} - {{}}| \<le>o |A| ^c natLeq"
    3.35    using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto
    3.36    also have "|A| ^c natLeq \<le>o ( |A| +c ctwo) ^c natLeq"
    3.37 -  apply(rule cexp_mono1_cone_ordLeq)
    3.38 +  apply(rule cexp_mono1)
    3.39      apply(rule ordLeq_csum1, rule card_of_Card_order)
    3.40 -    apply (rule cone_ordLeq_cexp)
    3.41 -    apply (rule cone_ordLeq_Cnotzero)
    3.42 -    using csum_Cnotzero2 ctwo_Cnotzero apply blast
    3.43      by (rule natLeq_Card_order)
    3.44    finally show ?thesis .
    3.45  qed
     4.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Apr 25 18:27:26 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Apr 25 19:18:20 2013 +0200
     4.3 @@ -644,8 +644,8 @@
     4.4        map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
     4.5      val in_bd =
     4.6        @{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf,
     4.7 -        @{thm cexp_cong2_Cnotzero} OF [bd_ordIso, if live = 0 then
     4.8 -          @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2},
     4.9 +        @{thm cexp_cong2} OF [bd_ordIso, if live = 0 then
    4.10 +          @{thm Card_order_ctwo} else @{thm Card_order_csum},
    4.11              bd_Card_order_of_bnf bnf]];
    4.12  
    4.13      fun mk_tac thm {context = ctxt, prems = _} =
     5.1 --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Apr 25 18:27:26 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Apr 25 19:18:20 2013 +0200
     5.3 @@ -205,13 +205,9 @@
     5.4       rtac Card_order_ctwo THEN'
     5.5       (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE'
     5.6         rtac (hd Fbd_Cinfs)) THEN'
     5.7 -     rtac disjI1 THEN'
     5.8 -     TRY o rtac csum_Cnotzero2 THEN'
     5.9 -     rtac ctwo_Cnotzero THEN'
    5.10       rtac Gbd_Card_order THEN'
    5.11       rtac @{thm cexp_cprod} THEN'
    5.12 -     TRY o rtac csum_Cnotzero2 THEN'
    5.13 -     rtac ctwo_Cnotzero) 1
    5.14 +     rtac @{thm Card_order_csum}) 1
    5.15    end;
    5.16  
    5.17  val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
    5.18 @@ -300,13 +296,6 @@
    5.19    else all_tac) THEN
    5.20    (rtac @{thm csum_com} THEN'
    5.21    rtac bd_Card_order THEN'
    5.22 -  rtac disjI1 THEN'
    5.23 -  rtac csum_Cnotzero2 THEN'
    5.24 -  rtac ctwo_Cnotzero THEN'
    5.25 -  rtac disjI1 THEN'
    5.26 -  rtac csum_Cnotzero2 THEN'
    5.27 -  TRY o rtac csum_Cnotzero1 THEN'
    5.28 -  rtac Cnotzero_UNIV THEN'
    5.29    rtac @{thm ordLeq_ordIso_trans} THEN'
    5.30    rtac @{thm cexp_mono1} THEN'
    5.31    rtac ctrans THEN'
    5.32 @@ -322,14 +311,9 @@
    5.33    ((rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl}) ORELSE'
    5.34      (rtac Card_order_csum THEN' rtac ordLeq_csum2)) THEN'
    5.35    rtac Card_order_ctwo THEN'
    5.36 -  rtac disjI1 THEN'
    5.37 -  rtac csum_Cnotzero2 THEN'
    5.38 -  TRY o rtac csum_Cnotzero1 THEN'
    5.39 -  rtac Cnotzero_UNIV THEN'
    5.40    rtac bd_Card_order THEN'
    5.41    rtac @{thm cexp_cprod_ordLeq} THEN'
    5.42 -  TRY o rtac csum_Cnotzero2 THEN'
    5.43 -  rtac ctwo_Cnotzero THEN'
    5.44 +  resolve_tac @{thms Card_order_csum Card_order_ctwo} THEN'
    5.45    rtac @{thm Cinfinite_cprod2} THEN'
    5.46    TRY o rtac csum_Cnotzero1 THEN'
    5.47    rtac Cnotzero_UNIV THEN'
    5.48 @@ -374,8 +358,7 @@
    5.49    (rtac ordLeq_csum2 THEN'
    5.50    (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) ORELSE
    5.51    (rtac ordLeq_csum2 THEN' rtac Card_order_ctwo) 1) THEN
    5.52 -  (rtac disjI1 THEN' TRY o rtac csum_Cnotzero2 THEN' rtac ctwo_Cnotzero
    5.53 -   THEN' rtac bd_Card_order) 1;
    5.54 +  (rtac bd_Card_order) 1;
    5.55  
    5.56  
    5.57  
    5.58 @@ -399,13 +382,7 @@
    5.59        FIRST' [rtac card_of_Card_order, rtac Card_order_csum])
    5.60      ordIso_transitive @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
    5.61      src dest THEN'
    5.62 -  rtac bd_Card_order THEN'
    5.63 -  rtac disjI1 THEN'
    5.64 -  TRY o rtac csum_Cnotzero2 THEN'
    5.65 -  rtac ctwo_Cnotzero THEN'
    5.66 -  rtac disjI1 THEN'
    5.67 -  TRY o rtac csum_Cnotzero2 THEN'
    5.68 -  rtac ctwo_Cnotzero) 1;
    5.69 +  rtac bd_Card_order) 1;
    5.70  
    5.71  fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
    5.72    (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN
     6.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Apr 25 18:27:26 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Apr 25 19:18:20 2013 +0200
     6.3 @@ -1082,7 +1082,7 @@
     6.4              Cnz RS ((@{thm ordLeq_ordIso_trans} OF
     6.5                [(Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl})), sbd_ordIso]) RS
     6.6                (bd RS @{thm ordLeq_transitive[OF _
     6.7 -                cexp_mono2_Cnotzero[OF _ csum_Cnotzero2[OF ctwo_Cnotzero]]]}));
     6.8 +                cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
     6.9            val in_sbds = map4 mk_in_sbd ks bd_Card_orders bd_Cnotzeros in_bds;
    6.10         in
    6.11           (lthy, sbd, sbdT,
     7.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Apr 25 18:27:26 2013 +0200
     7.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Apr 25 19:18:20 2013 +0200
     7.3 @@ -462,15 +462,15 @@
     7.4        rtac ctrans, rtac @{thm card_of_diff},
     7.5        rtac ordIso_ordLeq_trans, rtac @{thm card_of_Field_ordIso},
     7.6        rtac @{thm Card_order_cpow}, rtac ordIso_ordLeq_trans,
     7.7 -      rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1_Cnotzero},
     7.8 +      rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1},
     7.9        if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
    7.10 -      rtac @{thm Card_order_ctwo}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_clists},
    7.11 +      rtac @{thm Card_order_ctwo}, rtac @{thm Card_order_clists},
    7.12        rtac @{thm cexp_mono2_Cnotzero}, rtac ordIso_ordLeq_trans,
    7.13        rtac @{thm clists_Cinfinite},
    7.14        if n = 1 then rtac sbd_Cinfinite else rtac (sbd_Cinfinite RS @{thm Cinfinite_csum1}),
    7.15        rtac ordIso_ordLeq_trans, rtac sbd_sbd, rtac @{thm infinite_ordLeq_cexp},
    7.16        rtac sbd_Cinfinite,
    7.17 -      if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
    7.18 +      if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
    7.19        rtac @{thm Cnotzero_clists},
    7.20        rtac ballI, rtac ordIso_ordLeq_trans, rtac @{thm card_of_Func_Ffunc},
    7.21        rtac ordIso_ordLeq_trans, rtac @{thm Func_cexp},
    7.22 @@ -480,26 +480,22 @@
    7.23            (sbd_Cinfinite RS @{thm Cinfinite_cexp[OF ordLeq_csum2[OF Card_order_ctwo]]}
    7.24          RSN (3, @{thm Un_Cinfinite_bound}))))
    7.25          (fn thm => EVERY' [rtac ctrans, rtac @{thm card_of_image}, rtac thm]) (rev in_sbds),
    7.26 -      rtac @{thm cexp_cong1_Cnotzero}, rtac @{thm csum_cong1},
    7.27 +      rtac @{thm cexp_cong1}, rtac @{thm csum_cong1},
    7.28        REPEAT_DETERM_N m o rtac @{thm csum_cong2},
    7.29        CONJ_WRAP_GEN' (rtac @{thm csum_cong})
    7.30          (K (rtac (sbd_Card_order RS @{thm card_of_Field_ordIso}))) in_sbds,
    7.31        rtac sbd_Card_order,
    7.32 -      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
    7.33 -      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
    7.34        rtac @{thm ordLeq_ordIso_trans}, etac @{thm clists_bound},
    7.35        rtac @{thm clists_Cinfinite}, TRY o rtac @{thm Cinfinite_csum1}, rtac sbd_Cinfinite,
    7.36 -      rtac disjI2, rtac @{thm cone_ordLeq_cexp}, rtac @{thm cone_ordLeq_cexp},
    7.37 -      rtac ctrans, rtac @{thm cone_ordLeq_ctwo}, rtac @{thm ordLeq_csum2},
    7.38 -      rtac @{thm Card_order_ctwo}, rtac FalseE, etac @{thm cpow_clists_czero}, atac,
    7.39 +      rtac FalseE, etac @{thm cpow_clists_czero}, atac,
    7.40        rtac @{thm card_of_Card_order},
    7.41        rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod},
    7.42 -      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
    7.43 -      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cong2_Cnotzero},
    7.44 +      rtac @{thm Card_order_csum},
    7.45 +      rtac ordIso_ordLeq_trans, rtac @{thm cexp_cong2},
    7.46        rtac @{thm ordIso_transitive}, rtac @{thm cprod_cong2}, rtac sbd_sbd,
    7.47        rtac @{thm cprod_infinite}, rtac sbd_Cinfinite,
    7.48 -      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_cprod},
    7.49 -      rtac ctrans, rtac @{thm cexp_mono1_Cnotzero},
    7.50 +      rtac @{thm Card_order_csum}, rtac @{thm Card_order_cprod},
    7.51 +      rtac ctrans, rtac @{thm cexp_mono1},
    7.52        rtac ordIso_ordLeq_trans, rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1},
    7.53        rtac @{thm ordIso_transitive},
    7.54        REPEAT_DETERM_N m o rtac @{thm csum_cong2},
    7.55 @@ -513,14 +509,13 @@
    7.56        rtac @{thm csum_com}, rtac @{thm csum_cexp'}, rtac sbd_Cinfinite,
    7.57        if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
    7.58        if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2},
    7.59 -      rtac @{thm Card_order_ctwo},
    7.60 -      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac sbd_Card_order,
    7.61 +      rtac @{thm Card_order_ctwo}, rtac sbd_Card_order,
    7.62        rtac ordIso_ordLeq_trans, rtac @{thm cexp_cprod_ordLeq},
    7.63 -      if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
    7.64 +      if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
    7.65        rtac sbd_Cinfinite, rtac sbd_Cnotzero, rtac @{thm ordLeq_refl}, rtac sbd_Card_order,
    7.66        rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm infinite_ordLeq_cexp},
    7.67        rtac sbd_Cinfinite,
    7.68 -      if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]},
    7.69 +      if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
    7.70        rtac sbd_Cnotzero,
    7.71        rtac @{thm card_of_mono1}, rtac subsetI,
    7.72        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac,
    7.73 @@ -1328,7 +1323,7 @@
    7.74        rtac @{thm card_of_image}, rtac ordIso_ordLeq_trans,
    7.75        rtac @{thm card_of_ordIso_subst}, rtac @{thm sym[OF proj_image]}, rtac ctrans,
    7.76        rtac @{thm card_of_image}, rtac ctrans, rtac card_of_carT, rtac @{thm cexp_mono2_Cnotzero},
    7.77 -      rtac @{thm cexp_ordLeq_ccexp},  rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero},
    7.78 +      rtac @{thm cexp_ordLeq_ccexp}, rtac @{thm Card_order_csum},
    7.79        rtac @{thm Cnotzero_cexp}, rtac sbd_Cnotzero, rtac sbd_Card_order,
    7.80        rtac @{thm card_of_mono1}, rtac subsetI, rtac @{thm image_eqI}, rtac sym,
    7.81        rtac Rep_inverse, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
     8.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Apr 25 18:27:26 2013 +0200
     8.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Apr 25 19:18:20 2013 +0200
     8.3 @@ -552,8 +552,7 @@
     8.4      fun mk_in_bd_sum i Co Cnz bd =
     8.5        if n = 1 then bd
     8.6        else Cnz RS ((Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl})) RS
     8.7 -        (bd RS @{thm ordLeq_transitive[OF _
     8.8 -          cexp_mono2_Cnotzero[OF _ csum_Cnotzero2[OF ctwo_Cnotzero]]]}));
     8.9 +        (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
    8.10      val in_bd_sums = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
    8.11  
    8.12      val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
    8.13 @@ -575,9 +574,7 @@
    8.14      val Asuc_bd_Cinfinite = suc_bd_Cinfinite RS (basis_Asuc RS @{thm Cinfinite_cexp});
    8.15      val Asuc_bd_Cnotzero = Asuc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
    8.16  
    8.17 -    val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF
    8.18 -      ordLess_ctwo_cexp
    8.19 -      cexp_mono1_Cnotzero[OF _ ctwo_Cnotzero]]} OF
    8.20 +    val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF ordLess_ctwo_cexp cexp_mono1]} OF
    8.21        [suc_bd_Card_order, basis_Asuc, suc_bd_Card_order];
    8.22  
    8.23      val Asuc_bdT = fst (dest_relT (fastype_of (mk_Asuc_bd As)));
     9.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Apr 25 18:27:26 2013 +0200
     9.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Apr 25 19:18:20 2013 +0200
     9.3 @@ -312,18 +312,17 @@
     9.4      fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac @{thm ordIso_ordLeq_trans},
     9.5        rtac @{thm card_of_ordIso_subst}, etac min_alg, rtac @{thm Un_Cinfinite_bound},
     9.6        minG_tac, rtac ctrans, rtac @{thm card_of_image}, rtac ctrans, rtac in_bd, rtac ctrans,
     9.7 -      rtac @{thm cexp_mono1_Cnotzero}, rtac @{thm csum_mono1},
     9.8 +      rtac @{thm cexp_mono1}, rtac @{thm csum_mono1},
     9.9        REPEAT_DETERM_N m o rtac @{thm csum_mono2},
    9.10        CONJ_WRAP_GEN' (rtac @{thm csum_cinfinite_bound}) (K minG_tac) min_algs,
    9.11        REPEAT_DETERM o FIRST'
    9.12 -        [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}, rtac Asuc_Cinfinite],
    9.13 -      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac bd_Card_order,
    9.14 -      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1_Cnotzero}, absorbAs_tac,
    9.15 +        [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum},
    9.16 +        rtac Asuc_Cinfinite, rtac bd_Card_order],
    9.17 +      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1}, absorbAs_tac,
    9.18        rtac @{thm csum_absorb1}, rtac Asuc_Cinfinite, rtac @{thm ctwo_ordLeq_Cinfinite},
    9.19        rtac Asuc_Cinfinite, rtac bd_Card_order,
    9.20 -      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac Asuc_Cnotzero,
    9.21        rtac @{thm ordIso_imp_ordLeq}, rtac @{thm cexp_cprod_ordLeq},
    9.22 -      TRY o rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac suc_Cinfinite,
    9.23 +      resolve_tac @{thms Card_order_csum Card_order_ctwo}, rtac suc_Cinfinite,
    9.24        rtac bd_Cnotzero, rtac @{thm cardSuc_ordLeq}, rtac bd_Card_order, rtac Asuc_Cinfinite];
    9.25    in
    9.26      (rtac induct THEN'
    9.27 @@ -753,8 +752,8 @@
    9.28  fun mk_in_bd_tac sum_Card_order sucbd_Cnotzero incl card_of_min_alg =
    9.29    EVERY' [rtac ctrans, rtac @{thm card_of_mono1}, rtac subsetI, etac rev_mp,
    9.30      rtac incl, rtac ctrans, rtac card_of_min_alg, rtac @{thm cexp_mono2_Cnotzero},
    9.31 -    rtac @{thm cardSuc_ordLeq_cpow}, rtac sum_Card_order, rtac @{thm csum_Cnotzero2},
    9.32 -    rtac @{thm ctwo_Cnotzero}, rtac sucbd_Cnotzero] 1;
    9.33 +    rtac @{thm cardSuc_ordLeq_cpow}, rtac sum_Card_order, rtac @{thm Card_order_csum},
    9.34 +    rtac sucbd_Cnotzero] 1;
    9.35  
    9.36  fun mk_bd_card_order_tac bd_card_orders =
    9.37    (rtac @{thm card_order_cpow} THEN'
    10.1 --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Thu Apr 25 18:27:26 2013 +0200
    10.2 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Thu Apr 25 19:18:20 2013 +0200
    10.3 @@ -72,8 +72,8 @@
    10.4  using card_of_empty_ordIso by (simp add: czero_def)
    10.5  
    10.6  lemma card_of_ordIso_czero_iff_empty:
    10.7 -  "|A| =o (czero :: 'a rel) \<longleftrightarrow> A = ({} :: 'a set)"
    10.8 -unfolding czero_def by (rule iffI[OF card_of_empty2]) (auto simp: card_of_refl)
    10.9 +  "|A| =o (czero :: 'b rel) \<longleftrightarrow> A = ({} :: 'a set)"
   10.10 +unfolding czero_def by (rule iffI[OF card_of_empty2]) (auto simp: card_of_refl card_of_empty_ordIso)
   10.11  
   10.12  (* A "not czero" Cardinal predicate *)
   10.13  abbreviation Cnotzero where
   10.14 @@ -389,8 +389,7 @@
   10.15  
   10.16  lemma cexp_mono':
   10.17    assumes 1: "p1 \<le>o r1" and 2: "p2 \<le>o r2"
   10.18 -  and n1: "Field p1 \<noteq> {} \<or> cone \<le>o r1 ^c r2"
   10.19 -  and n2: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
   10.20 +  and n: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
   10.21    shows "p1 ^c p2 \<le>o r1 ^c r2"
   10.22  proof(cases "Field p1 = {}")
   10.23    case True
   10.24 @@ -399,7 +398,18 @@
   10.25      by (cases "Field p2 = {}", auto intro: card_of_ordLeqI2 simp: Func_empty)
   10.26         (metis Func_is_emp card_of_empty ex_in_conv)
   10.27    hence "p1 ^c p2 \<le>o cone" by (simp add: Field_card_of cexp_def)
   10.28 -  thus ?thesis using True n1 ordLeq_transitive by auto
   10.29 +  thus ?thesis
   10.30 +  proof (cases "Field p2 = {}")
   10.31 +    case True
   10.32 +    with n have "Field r2 = {}" .
   10.33 +    hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def by (auto intro: card_of_ordLeqI)
   10.34 +    thus ?thesis using `p1 ^c p2 \<le>o cone` ordLeq_transitive by auto
   10.35 +  next
   10.36 +    case False with True have "|Field (p1 ^c p2)| =o czero"
   10.37 +      unfolding card_of_ordIso_czero_iff_empty cexp_def Func_is_emp Field_card_of by blast
   10.38 +    thus ?thesis unfolding cexp_def card_of_ordIso_czero_iff_empty Field_card_of
   10.39 +      by (simp add: card_of_empty)
   10.40 +  qed
   10.41  next
   10.42    case False
   10.43    have 1: "|Field p1| \<le>o |Field r1|" and 2: "|Field p2| \<le>o |Field r2|"
   10.44 @@ -409,7 +419,7 @@
   10.45    obtain f2 where f2: "inj_on f2 (Field p2)" "f2 ` Field p2 \<subseteq> Field r2"
   10.46      using 2 unfolding card_of_ordLeq[symmetric] by blast
   10.47    have 0: "Func_map (Field p2) f1 f2 ` (Field (r1 ^c r2)) = Field (p1 ^c p2)"
   10.48 -    unfolding cexp_def Field_card_of using Func_map_surj[OF f1 f2 n2, symmetric] .
   10.49 +    unfolding cexp_def Field_card_of using Func_map_surj[OF f1 f2 n, symmetric] .
   10.50    have 00: "Field (p1 ^c p2) \<noteq> {}" unfolding cexp_def Field_card_of Func_is_emp
   10.51      using False by simp
   10.52    show ?thesis
   10.53 @@ -418,57 +428,36 @@
   10.54  
   10.55  lemma cexp_mono:
   10.56    assumes 1: "p1 \<le>o r1" and 2: "p2 \<le>o r2"
   10.57 -  and n1: "Cnotzero p1 \<or> cone \<le>o r1 ^c r2"
   10.58 -  and n2: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
   10.59 +  and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
   10.60    shows "p1 ^c p2 \<le>o r1 ^c r2"
   10.61 -proof (rule cexp_mono'[OF 1 2])
   10.62 -  show "Field p1 \<noteq> {} \<or> cone \<le>o r1 ^c r2"
   10.63 -  proof (cases "Cnotzero p1")
   10.64 -    case True show ?thesis using Cnotzero_imp_not_empty[OF True] by (rule disjI1)
   10.65 -  next
   10.66 -    case False with n1 show ?thesis by blast
   10.67 -  qed
   10.68 -qed (rule czeroI[OF card, THEN n2, THEN czeroE])
   10.69 +  by (metis (full_types) "1" "2" card cexp_mono' czeroE czeroI n)
   10.70  
   10.71  lemma cexp_mono1:
   10.72 -  assumes 1: "p1 \<le>o r1"
   10.73 -  and n1: "Cnotzero p1 \<or> cone \<le>o r1 ^c q" and q: "Card_order q"
   10.74 +  assumes 1: "p1 \<le>o r1" and q: "Card_order q"
   10.75    shows "p1 ^c q \<le>o r1 ^c q"
   10.76 -using ordLeq_refl[OF q] by (rule cexp_mono[OF 1 _ n1]) (auto simp: q)
   10.77 -
   10.78 -lemma cexp_mono1_Cnotzero: "\<lbrakk>p1 \<le>o r1; Cnotzero p1; Card_order q\<rbrakk> \<Longrightarrow> p1 ^c q \<le>o r1 ^c q"
   10.79 -by (simp add: cexp_mono1)
   10.80 -
   10.81 -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"
   10.82 -using assms by (simp add: cexp_mono1)
   10.83 +using ordLeq_refl[OF q] by (rule cexp_mono[OF 1]) (auto simp: q)
   10.84  
   10.85  lemma cexp_mono2':
   10.86    assumes 2: "p2 \<le>o r2" and q: "Card_order q"
   10.87 -  and n1: "Field q \<noteq> {} \<or> cone \<le>o q ^c r2"
   10.88 -  and n2: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
   10.89 +  and n: "Field p2 = {} \<Longrightarrow> Field r2 = {}"
   10.90    shows "q ^c p2 \<le>o q ^c r2"
   10.91 -using ordLeq_refl[OF q] by (rule cexp_mono'[OF _ 2 n1 n2]) auto
   10.92 +using ordLeq_refl[OF q] by (rule cexp_mono'[OF _ 2 n]) auto
   10.93  
   10.94  lemma cexp_mono2:
   10.95    assumes 2: "p2 \<le>o r2" and q: "Card_order q"
   10.96 -  and n1: "Cnotzero q \<or> cone \<le>o q ^c r2"
   10.97 -  and n2: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
   10.98 +  and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2"
   10.99    shows "q ^c p2 \<le>o q ^c r2"
  10.100 -using ordLeq_refl[OF q] by (rule cexp_mono[OF _ 2 n1 n2 card]) auto
  10.101 +using ordLeq_refl[OF q] by (rule cexp_mono[OF _ 2 n card]) auto
  10.102  
  10.103  lemma cexp_mono2_Cnotzero:
  10.104 -  assumes "p2 \<le>o r2" "Cnotzero q" and n2: "Cnotzero p2"
  10.105 +  assumes "p2 \<le>o r2" "Card_order q" "Cnotzero p2"
  10.106    shows "q ^c p2 \<le>o q ^c r2"
  10.107 -proof (rule cexp_mono)
  10.108 -  assume *: "p2 =o czero"
  10.109 -  have False using n2 czeroI czeroE[OF *] by blast
  10.110 -  thus "r2 =o czero" by blast
  10.111 -qed (auto simp add: assms ordLeq_refl)
  10.112 +by (metis assms cexp_mono2' czeroI)
  10.113  
  10.114  lemma cexp_cong:
  10.115    assumes 1: "p1 =o r1" and 2: "p2 =o r2"
  10.116 -  and p1: "Cnotzero p1 \<or> cone \<le>o r1 ^c r2" and Cr: "Card_order r2"
  10.117 -  and r1: "Cnotzero r1 \<or> cone \<le>o p1 ^c p2" and Cp: "Card_order p2"
  10.118 +  and Cr: "Card_order r2"
  10.119 +  and Cp: "Card_order p2"
  10.120    shows "p1 ^c p2 =o r1 ^c r2"
  10.121  proof -
  10.122    obtain f where "bij_betw f (Field p2) (Field r2)"
  10.123 @@ -478,32 +467,16 @@
  10.124      and p: "r2 =o czero \<Longrightarrow> p2 =o czero"
  10.125       using 0 Cr Cp czeroE czeroI by auto
  10.126    show ?thesis using 0 1 2 unfolding ordIso_iff_ordLeq
  10.127 -    using r p cexp_mono[OF _ _ p1 _ Cp] cexp_mono[OF _ _ r1 _ Cr]
  10.128 -    by blast
  10.129 +    using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by blast
  10.130  qed
  10.131  
  10.132  lemma cexp_cong1:
  10.133    assumes 1: "p1 =o r1" and q: "Card_order q"
  10.134 -  and p1: "Cnotzero p1 \<or> cone \<le>o r1 ^c q"
  10.135 -  and r1: "Cnotzero r1 \<or> cone \<le>o p1 ^c q"
  10.136    shows "p1 ^c q =o r1 ^c q"
  10.137 -by (rule cexp_cong[OF 1 _ p1 q r1 q]) (rule ordIso_refl[OF q])
  10.138 -
  10.139 -lemma cexp_cong1_Cnotzero:
  10.140 -  assumes "p1 =o r1" "Card_order q" "Cnotzero p1" "Cnotzero r1"
  10.141 -  shows "p1 ^c q =o r1 ^c q"
  10.142 -by (rule cexp_cong1, auto simp add: assms)
  10.143 +by (rule cexp_cong[OF 1 _ q q]) (rule ordIso_refl[OF q])
  10.144  
  10.145  lemma cexp_cong2:
  10.146 -  assumes 2: "p2 =o r2" and q: "Card_order q"
  10.147 -  and p: "Card_order p2" and r: "Card_order r2"
  10.148 -  shows "Cnotzero q \<or> (cone \<le>o q ^c p2 \<and> cone \<le>o q ^c r2) \<Longrightarrow>
  10.149 -    q ^c p2 =o q ^c r2"
  10.150 -by (rule cexp_cong[OF _ 2]) (auto simp only: ordIso_refl q p r)
  10.151 -
  10.152 -lemma cexp_cong2_Cnotzero:
  10.153 -  assumes 2: "p2 =o r2" and q: "Cnotzero q"
  10.154 -  and p: "Card_order p2"
  10.155 +  assumes 2: "p2 =o r2" and q: "Card_order q" and p: "Card_order p2"
  10.156    shows "q ^c p2 =o q ^c r2"
  10.157  by (rule cexp_cong[OF _ 2]) (auto simp only: ordIso_refl Card_order_ordIso2[OF p 2] q p)
  10.158  
  10.159 @@ -523,7 +496,7 @@
  10.160  qed
  10.161  
  10.162  lemma cexp_cprod:
  10.163 -  assumes r1: "Cnotzero r1"
  10.164 +  assumes r1: "Card_order r1"
  10.165    shows "(r1 ^c r2) ^c r3 =o r1 ^c (r2 *c r3)" (is "?L =o ?R")
  10.166  proof -
  10.167    have "?L =o r1 ^c (r3 *c r2)"
  10.168 @@ -535,7 +508,7 @@
  10.169  qed
  10.170  
  10.171  lemma cexp_cprod_ordLeq:
  10.172 -  assumes r1: "Cnotzero r1" and r2: "Cinfinite r2"
  10.173 +  assumes r1: "Card_order r1" and r2: "Cinfinite r2"
  10.174    and r3: "Cnotzero r3" "r3 \<le>o r2"
  10.175    shows "(r1 ^c r2) ^c r3 =o r1 ^c r2" (is "?L =o ?R")
  10.176  proof-
  10.177 @@ -580,14 +553,6 @@
  10.178      apply (rule cone_ordLeq_Cnotzero)
  10.179      apply (rule assms(1))
  10.180      apply (rule assms(2))
  10.181 -    apply (rule disjI1)
  10.182 -    apply (rule conjI)
  10.183 -    apply (rule notI)
  10.184 -    apply (erule notE)
  10.185 -    apply (rule ordIso_transitive)
  10.186 -    apply assumption
  10.187 -    apply (rule czero_ordIso)
  10.188 -    apply (rule assms(2))
  10.189      apply (rule notE)
  10.190      apply (rule cone_not_czero)
  10.191      apply assumption
  10.192 @@ -609,8 +574,6 @@
  10.193      apply (rule assms(2))
  10.194      apply (rule cexp_mono1)
  10.195      apply (rule assms(1))
  10.196 -    apply (rule disjI1)
  10.197 -    apply (rule ctwo_Cnotzero)
  10.198      apply (rule assms(2))
  10.199    done
  10.200  qed
  10.201 @@ -649,9 +612,6 @@
  10.202      apply (rule conjunct2)
  10.203      apply (rule assms(1))
  10.204      apply (rule assms(2))
  10.205 -    apply (simp only: card_of_Card_order czero_def)
  10.206 -    apply (rule disjI1)
  10.207 -    apply (rule assms(1))
  10.208      apply (rule cexp_czero)
  10.209    done
  10.210  qed
  10.211 @@ -752,17 +712,6 @@
  10.212  apply (rule ordLeq_csum1)
  10.213  apply (erule conjunct2)
  10.214  apply assumption
  10.215 -apply (rule disjI2)
  10.216 -apply (rule ordLeq_transitive)
  10.217 -apply (rule cone_ordLeq_ctwo)
  10.218 -apply (rule ordLeq_transitive)
  10.219 -apply assumption
  10.220 -apply (rule ordLeq_cexp1)
  10.221 -apply (rule Cinfinite_Cnotzero)
  10.222 -apply (rule Cinfinite_csum)
  10.223 -apply (rule disjI1)
  10.224 -apply assumption
  10.225 -apply assumption
  10.226  apply (rule notE)
  10.227  apply (rule cinfinite_not_czero[of r1])
  10.228  apply (erule conjunct1)
  10.229 @@ -772,17 +721,6 @@
  10.230  apply (rule ordLeq_csum2)
  10.231  apply (erule conjunct2)
  10.232  apply assumption
  10.233 -apply (rule disjI2)
  10.234 -apply (rule ordLeq_transitive)
  10.235 -apply (rule cone_ordLeq_ctwo)
  10.236 -apply (rule ordLeq_transitive)
  10.237 -apply assumption
  10.238 -apply (rule ordLeq_cexp1)
  10.239 -apply (rule Cinfinite_Cnotzero)
  10.240 -apply (rule Cinfinite_csum)
  10.241 -apply (rule disjI1)
  10.242 -apply assumption
  10.243 -apply assumption
  10.244  apply (rule notE)
  10.245  apply (rule cinfinite_not_czero[of r2])
  10.246  apply (erule conjunct1)