src/HOL/Orderings.thy
changeset 51546 2e26df807dc7
parent 51487 f4bfdee99304
child 51579 ec3b78ce0758
     1.1 --- a/src/HOL/Orderings.thy	Tue Mar 26 20:55:21 2013 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Tue Mar 26 21:53:56 2013 +0100
     1.3 @@ -197,10 +197,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -sublocale order < order!: ordering less_eq less
     1.8 -  by default (auto intro: antisym order_trans simp add: less_le)
     1.9 -
    1.10 -sublocale order < dual_order!: ordering greater_eq greater
    1.11 +sublocale order < order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
    1.12    by default (auto intro: antisym order_trans simp add: less_le)
    1.13  
    1.14  context order
    1.15 @@ -210,7 +207,7 @@
    1.16  
    1.17  lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
    1.18      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
    1.19 -by (simp add: less_le) blast
    1.20 +by (fact order.order_iff_strict)
    1.21  
    1.22  lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
    1.23  unfolding less_le by blast
    1.24 @@ -228,10 +225,10 @@
    1.25  text {* Transitivity rules for calculational reasoning *}
    1.26  
    1.27  lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
    1.28 -by (simp add: less_le)
    1.29 +by (fact order.not_eq_order_implies_strict)
    1.30  
    1.31  lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b"
    1.32 -by (simp add: less_le)
    1.33 +by (rule order.not_eq_order_implies_strict)
    1.34  
    1.35  
    1.36  text {* Asymmetry. *}
    1.37 @@ -243,7 +240,7 @@
    1.38  by (blast intro: antisym)
    1.39  
    1.40  lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
    1.41 -by (erule contrapos_pn, erule subst, rule less_irrefl)
    1.42 +by (fact order.strict_implies_not_eq)
    1.43  
    1.44  
    1.45  text {* Least value operator *}
    1.46 @@ -1168,7 +1165,6 @@
    1.47  by (simp add: max_def)
    1.48  
    1.49  
    1.50 -
    1.51  subsection {* (Unique) top and bottom elements *}
    1.52  
    1.53  class bot = order +
    1.54 @@ -1176,8 +1172,7 @@
    1.55    assumes bot_least: "\<bottom> \<le> a"
    1.56  
    1.57  sublocale bot < bot!: ordering_top greater_eq greater bot
    1.58 -proof
    1.59 -qed (fact bot_least)
    1.60 +  by default (fact bot_least)
    1.61  
    1.62  context bot
    1.63  begin
    1.64 @@ -1205,8 +1200,7 @@
    1.65    assumes top_greatest: "a \<le> \<top>"
    1.66  
    1.67  sublocale top < top!: ordering_top less_eq less top
    1.68 -proof
    1.69 -qed (fact top_greatest)
    1.70 +  by default (fact top_greatest)
    1.71  
    1.72  context top
    1.73  begin
    1.74 @@ -1316,6 +1310,7 @@
    1.75  
    1.76  class dense_linorder = inner_dense_linorder + no_top + no_bot
    1.77  
    1.78 +
    1.79  subsection {* Wellorders *}
    1.80  
    1.81  class wellorder = linorder +