made natLe{q,ss} constants (yields smaller terms in composition)
authortraytel
Fri Mar 07 23:10:27 2014 +0100 (2014-03-07)
changeset 5601139d5043ce8a3
parent 56010 abf4879d39f1
child 56012 158dc03db8be
made natLe{q,ss} constants (yields smaller terms in composition)
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/Cardinals/Cardinal_Order_Relation.thy
     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}"