src/HOL/BNF_Cardinal_Order_Relation.thy
 changeset 56011 39d5043ce8a3 parent 55936 f6591f8c629d child 56075 c6d4425f1fdc
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.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.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.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.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.25  lemma natLeq_trans: "trans natLeq"
1.26 -unfolding trans_def by auto
1.27 +unfolding trans_def natLeq_def by auto
1.29  lemma natLeq_Preorder: "Preorder natLeq"
1.30  unfolding preorder_on_def
1.31  by (auto simp add: natLeq_Refl natLeq_trans)
1.33  lemma natLeq_antisym: "antisym natLeq"
1.34 -unfolding antisym_def by auto
1.35 +unfolding antisym_def natLeq_def by auto
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.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.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.49  lemma natLeq_natLess_Id: "natLess = natLeq - Id"
1.50 -by auto
1.51 +unfolding natLeq_def natLess_def by auto
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.58  lemma Field_natLeq_on: "Field (natLeq_on n) = {x. x < n}"
1.59  unfolding Field_def by auto
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.65  lemma Restr_natLeq: "Restr natLeq {x. x < n} = natLeq_on n"
1.66 -by force
1.67 +unfolding natLeq_def by force
1.69  lemma Restr_natLeq2:
1.70  "Restr natLeq (underS natLeq n) = natLeq_on n"