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.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"