--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Fri Mar 07 23:09:10 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Fri Mar 07 23:10:27 2014 +0100
@@ -1144,8 +1144,8 @@
shall be the restrictions of these relations to the numbers smaller than
fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}
-abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
-abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
+definition "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
+definition "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
abbreviation natLeq_on :: "nat \<Rightarrow> (nat * nat) set"
where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"
@@ -1164,47 +1164,47 @@
subsubsection {* First as well-orders *}
lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"
-by(unfold Field_def, auto)
+by(unfold Field_def natLeq_def, auto)
lemma natLeq_Refl: "Refl natLeq"
-unfolding refl_on_def Field_def by auto
+unfolding refl_on_def Field_def natLeq_def by auto
lemma natLeq_trans: "trans natLeq"
-unfolding trans_def by auto
+unfolding trans_def natLeq_def by auto
lemma natLeq_Preorder: "Preorder natLeq"
unfolding preorder_on_def
by (auto simp add: natLeq_Refl natLeq_trans)
lemma natLeq_antisym: "antisym natLeq"
-unfolding antisym_def by auto
+unfolding antisym_def natLeq_def by auto
lemma natLeq_Partial_order: "Partial_order natLeq"
unfolding partial_order_on_def
by (auto simp add: natLeq_Preorder natLeq_antisym)
lemma natLeq_Total: "Total natLeq"
-unfolding total_on_def by auto
+unfolding total_on_def natLeq_def by auto
lemma natLeq_Linear_order: "Linear_order natLeq"
unfolding linear_order_on_def
by (auto simp add: natLeq_Partial_order natLeq_Total)
lemma natLeq_natLess_Id: "natLess = natLeq - Id"
-by auto
+unfolding natLeq_def natLess_def by auto
lemma natLeq_Well_order: "Well_order natLeq"
unfolding well_order_on_def
-using natLeq_Linear_order wf_less natLeq_natLess_Id by auto
+using natLeq_Linear_order wf_less natLeq_natLess_Id natLeq_def natLess_def by auto
lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"
unfolding Field_def by auto
lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"
-unfolding underS_def by auto
+unfolding underS_def natLeq_def by auto
lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
-by force
+unfolding natLeq_def by force
lemma Restr_natLeq2:
"Restr natLeq (underS natLeq n) = natLeq_on n"
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Fri Mar 07 23:09:10 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Fri Mar 07 23:10:27 2014 +0100
@@ -1008,7 +1008,7 @@
subsubsection {* First as well-orders *}
lemma Field_natLess: "Field natLess = (UNIV::nat set)"
-by(unfold Field_def, auto)
+by(unfold Field_def natLess_def, auto)
lemma natLeq_well_order_on: "well_order_on UNIV natLeq"
using natLeq_Well_order Field_natLeq by auto
@@ -1018,11 +1018,11 @@
lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
- simp add: Field_natLeq, unfold under_def, auto)
+ simp add: Field_natLeq, unfold under_def natLeq_def, auto)
lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
- simp add: Field_natLeq, unfold under_def, auto)
+ simp add: Field_natLeq, unfold under_def natLeq_def, auto)
lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
@@ -1052,8 +1052,8 @@
"ofilter natLeq A = (A = UNIV \<or> (\<exists>n. A = {0 ..< n}))"
proof(rule iffI)
assume "ofilter natLeq A"
- hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
- by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def under_def)
+ hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A" using natLeq_wo_rel
+ by(auto simp add: natLeq_def wo_rel.ofilter_def under_def)
thus "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
next
assume "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
@@ -1062,7 +1062,7 @@
qed
lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
-unfolding under_def by auto
+unfolding under_def natLeq_def by auto
lemma natLeq_on_ofilter_less_eq:
"n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"