# HG changeset patch
# User traytel
# Date 1394230227 -3600
# Node ID 39d5043ce8a3c5be394fcd389d6118b7a6f41386
# Parent  abf4879d39f1aa71217e576f93607e1f6ac8429a
made natLe{q,ss} constants (yields smaller terms in composition)

diff -r abf4879d39f1 -r 39d5043ce8a3 src/HOL/BNF_Cardinal_Order_Relation.thy
--- 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"
diff -r abf4879d39f1 -r 39d5043ce8a3 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- 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}"