author traytel Fri Mar 07 23:10:27 2014 +0100 (2014-03-07) changeset 56011 39d5043ce8a3 parent 56010 abf4879d39f1 child 56012 158dc03db8be
made natLe{q,ss} constants (yields smaller terms in composition)
```     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Mar 07 23:09:10 2014 +0100
1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Fri Mar 07 23:10:27 2014 +0100
1.3 @@ -1144,8 +1144,8 @@
1.4  shall be the restrictions of these relations to the numbers smaller than
1.5  fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}
1.6
1.7 -abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
1.8 -abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
1.9 +definition "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
1.10 +definition "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
1.11
1.12  abbreviation natLeq_on :: "nat \<Rightarrow> (nat * nat) set"
1.13  where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"
1.14 @@ -1164,47 +1164,47 @@
1.15  subsubsection {* First as well-orders *}
1.16
1.17  lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"
1.18 -by(unfold Field_def, auto)
1.19 +by(unfold Field_def natLeq_def, auto)
1.20
1.21  lemma natLeq_Refl: "Refl natLeq"
1.22 -unfolding refl_on_def Field_def by auto
1.23 +unfolding refl_on_def Field_def natLeq_def by auto
1.24
1.25  lemma natLeq_trans: "trans natLeq"
1.26 -unfolding trans_def by auto
1.27 +unfolding trans_def natLeq_def by auto
1.28
1.29  lemma natLeq_Preorder: "Preorder natLeq"
1.30  unfolding preorder_on_def
1.31  by (auto simp add: natLeq_Refl natLeq_trans)
1.32
1.33  lemma natLeq_antisym: "antisym natLeq"
1.34 -unfolding antisym_def by auto
1.35 +unfolding antisym_def natLeq_def by auto
1.36
1.37  lemma natLeq_Partial_order: "Partial_order natLeq"
1.38  unfolding partial_order_on_def
1.39  by (auto simp add: natLeq_Preorder natLeq_antisym)
1.40
1.41  lemma natLeq_Total: "Total natLeq"
1.42 -unfolding total_on_def by auto
1.43 +unfolding total_on_def natLeq_def by auto
1.44
1.45  lemma natLeq_Linear_order: "Linear_order natLeq"
1.46  unfolding linear_order_on_def
1.47  by (auto simp add: natLeq_Partial_order natLeq_Total)
1.48
1.49  lemma natLeq_natLess_Id: "natLess = natLeq - Id"
1.50 -by auto
1.51 +unfolding natLeq_def natLess_def by auto
1.52
1.53  lemma natLeq_Well_order: "Well_order natLeq"
1.54  unfolding well_order_on_def
1.55 -using natLeq_Linear_order wf_less natLeq_natLess_Id by auto
1.56 +using natLeq_Linear_order wf_less natLeq_natLess_Id natLeq_def natLess_def by auto
1.57
1.58  lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"
1.59  unfolding Field_def by auto
1.60
1.61  lemma natLeq_underS_less: "underS natLeq n = {x. x < n}"
1.62 -unfolding underS_def by auto
1.63 +unfolding underS_def natLeq_def by auto
1.64
1.65  lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
1.66 -by force
1.67 +unfolding natLeq_def by force
1.68
1.69  lemma Restr_natLeq2:
1.70  "Restr natLeq (underS natLeq n) = natLeq_on n"
```
```     2.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Mar 07 23:09:10 2014 +0100
2.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Mar 07 23:10:27 2014 +0100
2.3 @@ -1008,7 +1008,7 @@
2.4  subsubsection {* First as well-orders *}
2.5
2.6  lemma Field_natLess: "Field natLess = (UNIV::nat set)"
2.7 -by(unfold Field_def, auto)
2.8 +by(unfold Field_def natLess_def, auto)
2.9
2.10  lemma natLeq_well_order_on: "well_order_on UNIV natLeq"
2.11  using natLeq_Well_order Field_natLeq by auto
2.12 @@ -1018,11 +1018,11 @@
2.13
2.14  lemma natLeq_ofilter_less: "ofilter natLeq {0 ..< n}"
2.15  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
2.16 -   simp add: Field_natLeq, unfold under_def, auto)
2.17 +   simp add: Field_natLeq, unfold under_def natLeq_def, auto)
2.18
2.19  lemma natLeq_ofilter_leq: "ofilter natLeq {0 .. n}"
2.20  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def,
2.21 -   simp add: Field_natLeq, unfold under_def, auto)
2.22 +   simp add: Field_natLeq, unfold under_def natLeq_def, auto)
2.23
2.24  lemma natLeq_UNIV_ofilter: "wo_rel.ofilter natLeq UNIV"
2.25  using natLeq_wo_rel Field_natLeq wo_rel.Field_ofilter[of natLeq] by auto
2.26 @@ -1052,8 +1052,8 @@
2.27  "ofilter natLeq A = (A = UNIV \<or> (\<exists>n. A = {0 ..< n}))"
2.28  proof(rule iffI)
2.29    assume "ofilter natLeq A"
2.30 -  hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A"
2.31 -  by(auto simp add: natLeq_wo_rel wo_rel.ofilter_def under_def)
2.32 +  hence "\<forall>m n. n \<in> A \<and> m \<le> n \<longrightarrow> m \<in> A" using natLeq_wo_rel
2.33 +  by(auto simp add: natLeq_def wo_rel.ofilter_def under_def)
2.34    thus "A = UNIV \<or> (\<exists>n. A = {0 ..< n})" using closed_nat_set_iff by blast
2.35  next
2.36    assume "A = UNIV \<or> (\<exists>n. A = {0 ..< n})"
2.37 @@ -1062,7 +1062,7 @@
2.38  qed
2.39
2.40  lemma natLeq_under_leq: "under natLeq n = {0 .. n}"
2.41 -unfolding under_def by auto
2.42 +unfolding under_def natLeq_def by auto
2.43
2.44  lemma natLeq_on_ofilter_less_eq:
2.45  "n \<le> m \<Longrightarrow> wo_rel.ofilter (natLeq_on m) {0 ..< n}"
```