src/HOL/BNF/More_BNFs.thy
changeset 51782 84e7225f5ab6
parent 51766 f19a4d0ab1bf
child 51836 4d6dcd51dd52
     1.1 --- a/src/HOL/BNF/More_BNFs.thy	Thu Apr 25 18:27:26 2013 +0200
     1.2 +++ b/src/HOL/BNF/More_BNFs.thy	Thu Apr 25 19:18:20 2013 +0200
     1.3 @@ -139,14 +139,9 @@
     1.4        apply (rule card_of_nat)
     1.5        apply (rule Card_order_ctwo)
     1.6        apply (rule card_of_Card_order)
     1.7 -      apply (rule natLeq_Card_order)
     1.8 -      apply (rule disjI1)
     1.9 -      apply (rule ctwo_Cnotzero)
    1.10        apply (rule cexp_mono1)
    1.11        apply (rule ordLeq_csum2)
    1.12        apply (rule Card_order_ctwo)
    1.13 -      apply (rule disjI1)
    1.14 -      apply (rule ctwo_Cnotzero)
    1.15        apply (rule natLeq_Card_order)
    1.16        apply (rule ordIso_ordLeq_trans)
    1.17        apply (rule card_of_Func)
    1.18 @@ -155,14 +150,9 @@
    1.19        apply (rule card_of_nat)
    1.20        apply (rule card_of_Card_order)
    1.21        apply (rule card_of_Card_order)
    1.22 -      apply (rule natLeq_Card_order)
    1.23 -      apply (rule disjI1)
    1.24 -      apply (erule not_emp_czero_notIn_ordIso_Card_order)
    1.25        apply (rule cexp_mono1)
    1.26        apply (rule ordLeq_csum1)
    1.27        apply (rule card_of_Card_order)
    1.28 -      apply (rule disjI1)
    1.29 -      apply (erule not_emp_czero_notIn_ordIso_Card_order)
    1.30        apply (rule natLeq_Card_order)
    1.31        apply (rule card_of_Card_order)
    1.32        apply (rule card_of_Card_order)
    1.33 @@ -405,11 +395,8 @@
    1.34    also have "|{X. X \<subseteq> A \<and> countable X} - {{}}| \<le>o |A| ^c natLeq"
    1.35    using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto
    1.36    also have "|A| ^c natLeq \<le>o ( |A| +c ctwo) ^c natLeq"
    1.37 -  apply(rule cexp_mono1_cone_ordLeq)
    1.38 +  apply(rule cexp_mono1)
    1.39      apply(rule ordLeq_csum1, rule card_of_Card_order)
    1.40 -    apply (rule cone_ordLeq_cexp)
    1.41 -    apply (rule cone_ordLeq_Cnotzero)
    1.42 -    using csum_Cnotzero2 ctwo_Cnotzero apply blast
    1.43      by (rule natLeq_Card_order)
    1.44    finally show ?thesis .
    1.45  qed