src/HOL/Cardinals/Cardinal_Order_Relation.thy
changeset 56011 39d5043ce8a3
parent 55174 2e8fe898fa71
child 56191 159b0c88b4a4
     1.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Mar 07 23:09:10 2014 +0100
     1.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Mar 07 23:10:27 2014 +0100
     1.3 @@ -1008,7 +1008,7 @@
     1.4  subsubsection {* First as well-orders *}
     1.5  
     1.6  lemma Field_natLess: "Field natLess = (UNIV::nat set)"
     1.7 -by(unfold Field_def, auto)
     1.8 +by(unfold Field_def natLess_def, auto)
     1.9  
    1.10  lemma natLeq_well_order_on: "well_order_on UNIV natLeq"
    1.11  using natLeq_Well_order Field_natLeq by auto
    1.12 @@ -1018,11 +1018,11 @@
    1.13  
    1.14  lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
    1.15  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
    1.16 -   simp add: Field_natLeq, unfold under_def, auto)
    1.17 +   simp add: Field_natLeq, unfold under_def natLeq_def, auto)
    1.18  
    1.19  lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
    1.20  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
    1.21 -   simp add: Field_natLeq, unfold under_def, auto)
    1.22 +   simp add: Field_natLeq, unfold under_def natLeq_def, auto)
    1.23  
    1.24  lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
    1.25  using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
    1.26 @@ -1052,8 +1052,8 @@
    1.27  "ofilter natLeq A = (A = UNIV \<or> (\<exists>n. A = {0 ..< n}))"
    1.28  proof(rule iffI)
    1.29    assume "ofilter natLeq A"
    1.30 -  hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
    1.31 -  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def under_def)
    1.32 +  hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A" using natLeq_wo_rel
    1.33 +  by(auto simp add: natLeq_def wo_rel.ofilter_def under_def)
    1.34    thus "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
    1.35  next
    1.36    assume "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
    1.37 @@ -1062,7 +1062,7 @@
    1.38  qed
    1.39  
    1.40  lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
    1.41 -unfolding under_def by auto
    1.42 +unfolding under_def natLeq_def by auto
    1.43  
    1.44  lemma natLeq_on_ofilter_less_eq:
    1.45  "n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"