added class preorder
authorhaftmann
Fri Jul 25 12:03:34 2008 +0200 (2008-07-25)
changeset 2768225aceefd4786
parent 27681 8cedebf55539
child 27683 add9a605d562
added class preorder
src/HOL/Bali/Decl.thy
src/HOL/Int.thy
src/HOL/Lattices.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Quicksort.thy
src/HOL/Library/Sublist_Order.thy
src/HOL/NSA/StarDef.thy
src/HOL/Orderings.thy
src/HOL/Real/PReal.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/SizeChange/Graphs.thy
src/HOL/SizeChange/Kleene_Algebras.thy
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/ListOrder.thy
src/HOL/Word/WordArith.thy
     1.1 --- a/src/HOL/Bali/Decl.thy	Fri Jul 25 12:03:32 2008 +0200
     1.2 +++ b/src/HOL/Bali/Decl.thy	Fri Jul 25 12:03:34 2008 +0200
     1.3 @@ -5,9 +5,8 @@
     1.4  header {* Field, method, interface, and class declarations, whole Java programs
     1.5  *}
     1.6  
     1.7 -(** order is significant, because of clash for "var" **)
     1.8  theory Decl
     1.9 -imports Term Table
    1.10 +imports Term Table (** order is significant, because of clash for "var" **)
    1.11  begin
    1.12  
    1.13  text {*
    1.14 @@ -64,10 +63,12 @@
    1.15             | Public     \<Rightarrow> False)"
    1.16  
    1.17  definition
    1.18 -  le_acc_def: "a \<le> (b::acc_modi) \<longleftrightarrow> (a = b) \<or> (a < b)"
    1.19 +  le_acc_def: "(a :: acc_modi) \<le> b \<longleftrightarrow> a < b \<or> a = b"
    1.20  
    1.21  instance proof
    1.22    fix x y z::acc_modi
    1.23 +  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
    1.24 +    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
    1.25    {
    1.26    show "x \<le> x"               \<spacespace>\<spacespace>    -- reflexivity
    1.27      by (auto simp add: le_acc_def)
    1.28 @@ -85,12 +86,10 @@
    1.29        by (unfold le_acc_def) iprover
    1.30    qed
    1.31    next
    1.32 -  show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
    1.33 -    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
    1.34 -  }
    1.35    fix x y:: acc_modi
    1.36    show  "x \<le> y \<or> y \<le> x"   
    1.37    by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
    1.38 +  }
    1.39  qed
    1.40    
    1.41  end
     2.1 --- a/src/HOL/Int.thy	Fri Jul 25 12:03:32 2008 +0200
     2.2 +++ b/src/HOL/Int.thy	Fri Jul 25 12:03:34 2008 +0200
     2.3 @@ -187,14 +187,14 @@
     2.4  instance int :: linorder
     2.5  proof
     2.6    fix i j k :: int
     2.7 -  show "(i < j) = (i \<le> j \<and> i \<noteq> j)"
     2.8 -    by (simp add: less_int_def)
     2.9 +  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
    2.10 +    by (cases i, cases j) (simp add: le)
    2.11 +  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
    2.12 +    by (auto simp add: less_int_def dest: antisym) 
    2.13    show "i \<le> i"
    2.14      by (cases i) (simp add: le)
    2.15    show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
    2.16      by (cases i, cases j, cases k) (simp add: le)
    2.17 -  show "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
    2.18 -    by (cases i, cases j) (simp add: le)
    2.19    show "i \<le> j \<or> j \<le> i"
    2.20      by (cases i, cases j) (simp add: le linorder_linear)
    2.21  qed
     3.1 --- a/src/HOL/Lattices.thy	Fri Jul 25 12:03:32 2008 +0200
     3.2 +++ b/src/HOL/Lattices.thy	Fri Jul 25 12:03:34 2008 +0200
     3.3 @@ -32,8 +32,8 @@
     3.4  
     3.5  lemma dual_lattice:
     3.6    "lower_semilattice (op \<ge>) (op >) sup"
     3.7 -by unfold_locales
     3.8 -  (auto simp add: sup_least)
     3.9 +by (rule lower_semilattice.intro, rule dual_order)
    3.10 +  (unfold_locales, simp_all add: sup_least)
    3.11  
    3.12  end
    3.13  
     4.1 --- a/src/HOL/Library/Char_ord.thy	Fri Jul 25 12:03:32 2008 +0200
     4.2 +++ b/src/HOL/Library/Char_ord.thy	Fri Jul 25 12:03:34 2008 +0200
     4.3 @@ -35,7 +35,7 @@
     4.4      by (auto simp add: nat_of_nibble_eq)
     4.5  next
     4.6    fix n m :: nibble
     4.7 -  show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
     4.8 +  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
     4.9      unfolding nibble_less_eq_def nibble_less_def less_le
    4.10      by (auto simp add: nat_of_nibble_eq)
    4.11  next
     5.1 --- a/src/HOL/Library/List_lexord.thy	Fri Jul 25 12:03:32 2008 +0200
     5.2 +++ b/src/HOL/Library/List_lexord.thy	Fri Jul 25 12:03:34 2008 +0200
     5.3 @@ -23,23 +23,41 @@
     5.4  end
     5.5  
     5.6  instance list :: (order) order
     5.7 -  apply (intro_classes, unfold list_less_def list_le_def)
     5.8 -  apply safe
     5.9 -  apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    5.10 -  apply simp
    5.11 -  apply assumption
    5.12 -  apply (blast intro: lexord_trans transI order_less_trans)
    5.13 -  apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    5.14 -  apply simp
    5.15 -  apply (blast intro: lexord_trans transI order_less_trans)
    5.16 -  done
    5.17 +proof
    5.18 +  fix xs :: "'a list"
    5.19 +  show "xs \<le> xs" by (simp add: list_le_def)
    5.20 +next
    5.21 +  fix xs ys zs :: "'a list"
    5.22 +  assume "xs \<le> ys" and "ys \<le> zs"
    5.23 +  then show "xs \<le> zs" by (auto simp add: list_le_def list_less_def)
    5.24 +    (rule lexord_trans, auto intro: transI)
    5.25 +next
    5.26 +  fix xs ys :: "'a list"
    5.27 +  assume "xs \<le> ys" and "ys \<le> xs"
    5.28 +  then show "xs = ys" apply (auto simp add: list_le_def list_less_def)
    5.29 +  apply (rule lexord_irreflexive [THEN notE])
    5.30 +  defer
    5.31 +  apply (rule lexord_trans) apply (auto intro: transI) done
    5.32 +next
    5.33 +  fix xs ys :: "'a list"
    5.34 +  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" 
    5.35 +  apply (auto simp add: list_less_def list_le_def)
    5.36 +  defer
    5.37 +  apply (rule lexord_irreflexive [THEN notE])
    5.38 +  apply auto
    5.39 +  apply (rule lexord_irreflexive [THEN notE])
    5.40 +  defer
    5.41 +  apply (rule lexord_trans) apply (auto intro: transI) done
    5.42 +qed
    5.43  
    5.44  instance list :: (linorder) linorder
    5.45 -  apply (intro_classes, unfold list_le_def list_less_def, safe)
    5.46 -  apply (cut_tac x = x and y = y and  r = "{(a,b). a < b}"  in lexord_linear)
    5.47 -   apply force
    5.48 -  apply simp
    5.49 -  done
    5.50 +proof
    5.51 +  fix xs ys :: "'a list"
    5.52 +  have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}"
    5.53 +    by (rule lexord_linear) auto
    5.54 +  then show "xs \<le> ys \<or> ys \<le> xs" 
    5.55 +    by (auto simp add: list_le_def list_less_def)
    5.56 +qed
    5.57  
    5.58  instantiation list :: (linorder) distrib_lattice
    5.59  begin
     6.1 --- a/src/HOL/Library/Multiset.thy	Fri Jul 25 12:03:32 2008 +0200
     6.2 +++ b/src/HOL/Library/Multiset.thy	Fri Jul 25 12:03:34 2008 +0200
     6.3 @@ -778,13 +778,8 @@
     6.4  theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
     6.5  unfolding le_multiset_def by auto
     6.6  
     6.7 -instance
     6.8 -apply intro_classes
     6.9 -   apply (rule mult_less_le)
    6.10 -  apply (rule mult_le_refl)
    6.11 - apply (erule mult_le_trans, assumption)
    6.12 -apply (erule mult_le_antisym, assumption)
    6.13 -done
    6.14 +instance proof
    6.15 +qed (auto simp add: mult_less_le dest: mult_le_antisym elim: mult_le_trans)
    6.16  
    6.17  end
    6.18  
    6.19 @@ -1101,16 +1096,16 @@
    6.20  done
    6.21  
    6.22  interpretation mset_order: order ["op \<le>#" "op <#"]
    6.23 -by (auto intro: order.intro mset_le_refl mset_le_antisym
    6.24 -    mset_le_trans simp: mset_less_def)
    6.25 +proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
    6.26 +  mset_le_trans simp: mset_less_def)
    6.27  
    6.28  interpretation mset_order_cancel_semigroup:
    6.29      pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
    6.30 -by unfold_locales (erule mset_le_mono_add [OF mset_le_refl])
    6.31 +proof qed (erule mset_le_mono_add [OF mset_le_refl])
    6.32  
    6.33  interpretation mset_order_semigroup_cancel:
    6.34      pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
    6.35 -by (unfold_locales) simp
    6.36 +proof qed simp
    6.37  
    6.38  
    6.39  lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
     7.1 --- a/src/HOL/Library/Quicksort.thy	Fri Jul 25 12:03:32 2008 +0200
     7.2 +++ b/src/HOL/Library/Quicksort.thy	Fri Jul 25 12:03:34 2008 +0200
     7.3 @@ -18,7 +18,7 @@
     7.4  by pat_completeness auto
     7.5  
     7.6  termination by (relation "measure size")
     7.7 -  (auto simp: length_filter_le [THEN order_class.le_less_trans])
     7.8 +  (auto simp: length_filter_le [THEN preorder_class.le_less_trans])
     7.9  
    7.10  lemma quicksort_permutes [simp]:
    7.11    "multiset_of (quicksort xs) = multiset_of xs"
     8.1 --- a/src/HOL/Library/Sublist_Order.thy	Fri Jul 25 12:03:32 2008 +0200
     8.2 +++ b/src/HOL/Library/Sublist_Order.thy	Fri Jul 25 12:03:34 2008 +0200
     8.3 @@ -47,7 +47,7 @@
     8.4    using assms by (induct rule: less_eq_list.induct) blast+
     8.5  
     8.6  definition
     8.7 -  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys"
     8.8 +  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
     8.9  
    8.10  lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
    8.11    by (induct rule: ileq_induct) auto
    8.12 @@ -56,7 +56,7 @@
    8.13  
    8.14  instance proof
    8.15    fix xs ys :: "'a list"
    8.16 -  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys" unfolding less_list_def ..
    8.17 +  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
    8.18  next
    8.19    fix xs :: "'a list"
    8.20    show "xs \<le> xs" by (induct xs) (auto intro!: ileq_empty ileq_drop ileq_take)
    8.21 @@ -140,7 +140,7 @@
    8.22    assumes "xs < ys"
    8.23    shows "length xs < length ys"
    8.24  proof -
    8.25 -  from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_list_def)
    8.26 +  from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_le)
    8.27    moreover with ileq_length have "length xs \<le> length ys" by auto
    8.28    ultimately show ?thesis by (auto intro: ileq_same_length)
    8.29  qed
    8.30 @@ -154,9 +154,9 @@
    8.31  lemma ilt_below_empty[simp]: "xs < [] \<Longrightarrow> False"
    8.32    by (auto dest: ilt_length)
    8.33  lemma ilt_drop: "xs < ys \<Longrightarrow> xs < x # ys"
    8.34 -  by (unfold less_list_def) (auto intro: ileq_intros)
    8.35 +  by (unfold less_le) (auto intro: ileq_intros)
    8.36  lemma ilt_take: "xs < ys \<Longrightarrow> x # xs < x # ys"
    8.37 -  by (unfold less_list_def) (auto intro: ileq_intros)
    8.38 +  by (unfold less_le) (auto intro: ileq_intros)
    8.39  lemma ilt_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
    8.40    by (induct zs) (auto intro: ilt_drop)
    8.41  lemma ilt_take_many: "xs < ys \<Longrightarrow> zs @ xs < zs @ ys"
    8.42 @@ -168,7 +168,7 @@
    8.43  lemma ileq_rev_take: "xs \<le> ys \<Longrightarrow> xs @ [x] \<le> ys @ [x]"
    8.44    by (induct rule: ileq_induct) (auto intro: ileq_intros ileq_drop_many)
    8.45  lemma ilt_rev_take: "xs < ys \<Longrightarrow> xs @ [x] < ys @ [x]"
    8.46 -  by (unfold less_list_def) (auto dest: ileq_rev_take)
    8.47 +  by (unfold less_le) (auto dest: ileq_rev_take)
    8.48  lemma ileq_rev_drop: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ [x]"
    8.49    by (induct rule: ileq_induct) (auto intro: ileq_intros)
    8.50  lemma ileq_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
     9.1 --- a/src/HOL/NSA/StarDef.thy	Fri Jul 25 12:03:32 2008 +0200
     9.2 +++ b/src/HOL/NSA/StarDef.thy	Fri Jul 25 12:03:34 2008 +0200
     9.3 @@ -732,7 +732,7 @@
     9.4  
     9.5  instance star :: (order) order
     9.6  apply (intro_classes)
     9.7 -apply (transfer, rule order_less_le)
     9.8 +apply (transfer, rule less_le_not_le)
     9.9  apply (transfer, rule order_refl)
    9.10  apply (transfer, erule (1) order_trans)
    9.11  apply (transfer, erule (1) order_antisym)
    10.1 --- a/src/HOL/Orderings.thy	Fri Jul 25 12:03:32 2008 +0200
    10.2 +++ b/src/HOL/Orderings.thy	Fri Jul 25 12:03:34 2008 +0200
    10.3 @@ -11,13 +11,12 @@
    10.4    "~~/src/Provers/order.ML"
    10.5  begin
    10.6  
    10.7 -subsection {* Partial orders *}
    10.8 +subsection {* Quasi orders *}
    10.9  
   10.10 -class order = ord +
   10.11 -  assumes less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
   10.12 +class preorder = ord +
   10.13 +  assumes less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> (y \<le> x)"
   10.14    and order_refl [iff]: "x \<le> x"
   10.15    and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
   10.16 -  assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
   10.17  begin
   10.18  
   10.19  text {* Reflexivity. *}
   10.20 @@ -27,7 +26,67 @@
   10.21  by (erule ssubst) (rule order_refl)
   10.22  
   10.23  lemma less_irrefl [iff]: "\<not> x < x"
   10.24 -by (simp add: less_le)
   10.25 +by (simp add: less_le_not_le)
   10.26 +
   10.27 +lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
   10.28 +unfolding less_le_not_le by blast
   10.29 +
   10.30 +
   10.31 +text {* Asymmetry. *}
   10.32 +
   10.33 +lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
   10.34 +by (simp add: less_le_not_le)
   10.35 +
   10.36 +lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
   10.37 +by (drule less_not_sym, erule contrapos_np) simp
   10.38 +
   10.39 +
   10.40 +text {* Transitivity. *}
   10.41 +
   10.42 +lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
   10.43 +by (auto simp add: less_le_not_le intro: order_trans) 
   10.44 +
   10.45 +lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
   10.46 +by (auto simp add: less_le_not_le intro: order_trans) 
   10.47 +
   10.48 +lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
   10.49 +by (auto simp add: less_le_not_le intro: order_trans) 
   10.50 +
   10.51 +
   10.52 +text {* Useful for simplification, but too risky to include by default. *}
   10.53 +
   10.54 +lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
   10.55 +by (blast elim: less_asym)
   10.56 +
   10.57 +lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
   10.58 +by (blast elim: less_asym)
   10.59 +
   10.60 +
   10.61 +text {* Transitivity rules for calculational reasoning *}
   10.62 +
   10.63 +lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
   10.64 +by (rule less_asym)
   10.65 +
   10.66 +
   10.67 +text {* Dual order *}
   10.68 +
   10.69 +lemma dual_preorder:
   10.70 +  "preorder (op \<ge>) (op >)"
   10.71 +by unfold_locales (auto simp add: less_le_not_le intro: order_trans)
   10.72 +
   10.73 +end
   10.74 +
   10.75 +
   10.76 +subsection {* Partial orders *}
   10.77 +
   10.78 +class order = preorder +
   10.79 +  assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
   10.80 +begin
   10.81 +
   10.82 +text {* Reflexivity. *}
   10.83 +
   10.84 +lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
   10.85 +by (auto simp add: less_le_not_le intro: antisym)
   10.86  
   10.87  lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
   10.88      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
   10.89 @@ -36,9 +95,6 @@
   10.90  lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
   10.91  unfolding less_le by blast
   10.92  
   10.93 -lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
   10.94 -unfolding less_le by blast
   10.95 -
   10.96  
   10.97  text {* Useful for simplification, but too risky to include by default. *}
   10.98  
   10.99 @@ -60,12 +116,6 @@
  10.100  
  10.101  text {* Asymmetry. *}
  10.102  
  10.103 -lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
  10.104 -by (simp add: less_le antisym)
  10.105 -
  10.106 -lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
  10.107 -by (drule less_not_sym, erule contrapos_np) simp
  10.108 -
  10.109  lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
  10.110  by (blast intro: antisym)
  10.111  
  10.112 @@ -76,33 +126,6 @@
  10.113  by (erule contrapos_pn, erule subst, rule less_irrefl)
  10.114  
  10.115  
  10.116 -text {* Transitivity. *}
  10.117 -
  10.118 -lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
  10.119 -by (simp add: less_le) (blast intro: order_trans antisym)
  10.120 -
  10.121 -lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
  10.122 -by (simp add: less_le) (blast intro: order_trans antisym)
  10.123 -
  10.124 -lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
  10.125 -by (simp add: less_le) (blast intro: order_trans antisym)
  10.126 -
  10.127 -
  10.128 -text {* Useful for simplification, but too risky to include by default. *}
  10.129 -
  10.130 -lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
  10.131 -by (blast elim: less_asym)
  10.132 -
  10.133 -lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
  10.134 -by (blast elim: less_asym)
  10.135 -
  10.136 -
  10.137 -text {* Transitivity rules for calculational reasoning *}
  10.138 -
  10.139 -lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
  10.140 -by (rule less_asym)
  10.141 -
  10.142 -
  10.143  text {* Least value operator *}
  10.144  
  10.145  definition (in ord)
  10.146 @@ -129,8 +152,7 @@
  10.147  
  10.148  lemma dual_order:
  10.149    "order (op \<ge>) (op >)"
  10.150 -by unfold_locales
  10.151 -   (simp add: less_le, auto intro: antisym order_trans)
  10.152 +by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
  10.153  
  10.154  end
  10.155  
  10.156 @@ -201,8 +223,7 @@
  10.157  
  10.158  lemma dual_linorder:
  10.159    "linorder (op \<ge>) (op >)"
  10.160 -by unfold_locales
  10.161 -  (simp add: less_le, auto intro: antisym order_trans simp add: linear)
  10.162 +by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
  10.163  
  10.164  
  10.165  text {* min/max *}
  10.166 @@ -557,27 +578,27 @@
  10.167  subsection {* Name duplicates *}
  10.168  
  10.169  lemmas order_less_le = less_le
  10.170 -lemmas order_eq_refl = order_class.eq_refl
  10.171 -lemmas order_less_irrefl = order_class.less_irrefl
  10.172 +lemmas order_eq_refl = preorder_class.eq_refl
  10.173 +lemmas order_less_irrefl = preorder_class.less_irrefl
  10.174  lemmas order_le_less = order_class.le_less
  10.175  lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
  10.176 -lemmas order_less_imp_le = order_class.less_imp_le
  10.177 +lemmas order_less_imp_le = preorder_class.less_imp_le
  10.178  lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
  10.179  lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
  10.180  lemmas order_neq_le_trans = order_class.neq_le_trans
  10.181  lemmas order_le_neq_trans = order_class.le_neq_trans
  10.182  
  10.183  lemmas order_antisym = antisym
  10.184 -lemmas order_less_not_sym = order_class.less_not_sym
  10.185 -lemmas order_less_asym = order_class.less_asym
  10.186 +lemmas order_less_not_sym = preorder_class.less_not_sym
  10.187 +lemmas order_less_asym = preorder_class.less_asym
  10.188  lemmas order_eq_iff = order_class.eq_iff
  10.189  lemmas order_antisym_conv = order_class.antisym_conv
  10.190 -lemmas order_less_trans = order_class.less_trans
  10.191 -lemmas order_le_less_trans = order_class.le_less_trans
  10.192 -lemmas order_less_le_trans = order_class.less_le_trans
  10.193 -lemmas order_less_imp_not_less = order_class.less_imp_not_less
  10.194 -lemmas order_less_imp_triv = order_class.less_imp_triv
  10.195 -lemmas order_less_asym' = order_class.less_asym'
  10.196 +lemmas order_less_trans = preorder_class.less_trans
  10.197 +lemmas order_le_less_trans = preorder_class.le_less_trans
  10.198 +lemmas order_less_le_trans = preorder_class.less_le_trans
  10.199 +lemmas order_less_imp_not_less = preorder_class.less_imp_not_less
  10.200 +lemmas order_less_imp_triv = preorder_class.less_imp_triv
  10.201 +lemmas order_less_asym' = preorder_class.less_asym'
  10.202  
  10.203  lemmas linorder_linear = linear
  10.204  lemmas linorder_less_linear = linorder_class.less_linear
  10.205 @@ -808,7 +829,7 @@
  10.206    Note that this list of rules is in reverse order of priorities.
  10.207  *}
  10.208  
  10.209 -lemmas order_trans_rules [trans] =
  10.210 +lemmas [trans] =
  10.211    order_less_subst2
  10.212    order_less_subst1
  10.213    order_le_less_subst2
  10.214 @@ -825,21 +846,61 @@
  10.215    back_subst
  10.216    rev_mp
  10.217    mp
  10.218 -  order_neq_le_trans
  10.219 -  order_le_neq_trans
  10.220 -  order_less_trans
  10.221 -  order_less_asym'
  10.222 -  order_le_less_trans
  10.223 -  order_less_le_trans
  10.224 +
  10.225 +lemmas (in order) [trans] =
  10.226 +  neq_le_trans
  10.227 +  le_neq_trans
  10.228 +
  10.229 +lemmas (in preorder) [trans] =
  10.230 +  less_trans
  10.231 +  less_asym'
  10.232 +  le_less_trans
  10.233 +  less_le_trans
  10.234    order_trans
  10.235 -  order_antisym
  10.236 +
  10.237 +lemmas (in order) [trans] =
  10.238 +  antisym
  10.239 +
  10.240 +lemmas (in ord) [trans] =
  10.241 +  ord_le_eq_trans
  10.242 +  ord_eq_le_trans
  10.243 +  ord_less_eq_trans
  10.244 +  ord_eq_less_trans
  10.245 +
  10.246 +lemmas [trans] =
  10.247 +  trans
  10.248 +
  10.249 +lemmas order_trans_rules =
  10.250 +  order_less_subst2
  10.251 +  order_less_subst1
  10.252 +  order_le_less_subst2
  10.253 +  order_le_less_subst1
  10.254 +  order_less_le_subst2
  10.255 +  order_less_le_subst1
  10.256 +  order_subst2
  10.257 +  order_subst1
  10.258 +  ord_le_eq_subst
  10.259 +  ord_eq_le_subst
  10.260 +  ord_less_eq_subst
  10.261 +  ord_eq_less_subst
  10.262 +  forw_subst
  10.263 +  back_subst
  10.264 +  rev_mp
  10.265 +  mp
  10.266 +  neq_le_trans
  10.267 +  le_neq_trans
  10.268 +  less_trans
  10.269 +  less_asym'
  10.270 +  le_less_trans
  10.271 +  less_le_trans
  10.272 +  order_trans
  10.273 +  antisym
  10.274    ord_le_eq_trans
  10.275    ord_eq_le_trans
  10.276    ord_less_eq_trans
  10.277    ord_eq_less_trans
  10.278    trans
  10.279  
  10.280 -
  10.281  (* FIXME cleanup *)
  10.282  
  10.283  text {* These support proving chains of decreasing inequalities
    11.1 --- a/src/HOL/Real/PReal.thy	Fri Jul 25 12:03:32 2008 +0200
    11.2 +++ b/src/HOL/Real/PReal.thy	Fri Jul 25 12:03:34 2008 +0200
    11.3 @@ -189,38 +189,37 @@
    11.4  
    11.5  subsection{*Properties of Ordering*}
    11.6  
    11.7 -lemma preal_le_refl: "w \<le> (w::preal)"
    11.8 -by (simp add: preal_le_def)
    11.9 -
   11.10 -lemma preal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::preal)"
   11.11 -by (force simp add: preal_le_def)
   11.12 -
   11.13 -lemma preal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::preal)"
   11.14 -apply (simp add: preal_le_def)
   11.15 -apply (rule Rep_preal_inject [THEN iffD1], blast)
   11.16 -done
   11.17 -
   11.18 -(* Axiom 'order_less_le' of class 'order': *)
   11.19 -lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
   11.20 -by (simp add: preal_le_def preal_less_def Rep_preal_inject less_le)
   11.21 -
   11.22  instance preal :: order
   11.23 -  by intro_classes
   11.24 -    (assumption |
   11.25 -      rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
   11.26 +proof
   11.27 +  fix w :: preal
   11.28 +  show "w \<le> w" by (simp add: preal_le_def)
   11.29 +next
   11.30 +  fix i j k :: preal
   11.31 +  assume "i \<le> j" and "j \<le> k"
   11.32 +  then show "i \<le> k" by (simp add: preal_le_def)
   11.33 +next
   11.34 +  fix z w :: preal
   11.35 +  assume "z \<le> w" and "w \<le> z"
   11.36 +  then show "z = w" by (simp add: preal_le_def Rep_preal_inject)
   11.37 +next
   11.38 +  fix z w :: preal
   11.39 +  show "z < w \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
   11.40 +  by (auto simp add: preal_le_def preal_less_def Rep_preal_inject)
   11.41 +qed  
   11.42  
   11.43  lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
   11.44  by (insert preal_imp_psubset_positives, blast)
   11.45  
   11.46 -lemma preal_le_linear: "x <= y | y <= (x::preal)"
   11.47 -apply (auto simp add: preal_le_def)
   11.48 -apply (rule ccontr)
   11.49 -apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal]
   11.50 +instance preal :: linorder
   11.51 +proof
   11.52 +  fix x y :: preal
   11.53 +  show "x <= y | y <= x"
   11.54 +    apply (auto simp add: preal_le_def)
   11.55 +    apply (rule ccontr)
   11.56 +    apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal]
   11.57               elim: order_less_asym)
   11.58 -done
   11.59 -
   11.60 -instance preal :: linorder
   11.61 -  by intro_classes (rule preal_le_linear)
   11.62 +    done
   11.63 +qed
   11.64  
   11.65  instantiation preal :: distrib_lattice
   11.66  begin
   11.67 @@ -1091,7 +1090,7 @@
   11.68  done
   11.69  
   11.70  lemma less_add_left: "R < (S::preal) ==> R + (S-R) = S"
   11.71 -by (blast intro: preal_le_anti_sym [OF less_add_left_le1 less_add_left_le2])
   11.72 +by (blast intro: antisym [OF less_add_left_le1 less_add_left_le2])
   11.73  
   11.74  lemma less_add_left_Ex: "R < (S::preal) ==> \<exists>D. R + D = S"
   11.75  by (fast dest: less_add_left)
    12.1 --- a/src/HOL/Real/Rational.thy	Fri Jul 25 12:03:32 2008 +0200
    12.2 +++ b/src/HOL/Real/Rational.thy	Fri Jul 25 12:03:34 2008 +0200
    12.3 @@ -436,8 +436,8 @@
    12.4    next
    12.5      show "q \<le> q"
    12.6        by (induct q) simp
    12.7 -    show "(q < r) = (q \<le> r \<and> q \<noteq> r)"
    12.8 -      by (simp only: less_rat_def)
    12.9 +    show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)"
   12.10 +      by (induct q, induct r) (auto simp add: le_less mult_commute)
   12.11      show "q \<le> r \<or> r \<le> q"
   12.12        by (induct q, induct r)
   12.13           (simp add: mult_commute, rule linorder_linear)
    13.1 --- a/src/HOL/Real/RealDef.thy	Fri Jul 25 12:03:32 2008 +0200
    13.2 +++ b/src/HOL/Real/RealDef.thy	Fri Jul 25 12:03:34 2008 +0200
    13.3 @@ -346,14 +346,12 @@
    13.4  apply (blast intro: real_trans_lemma)
    13.5  done
    13.6  
    13.7 -(* Axiom 'order_less_le' of class 'order': *)
    13.8 -lemma real_less_le: "((w::real) < z) = (w \<le> z & w \<noteq> z)"
    13.9 -by (simp add: real_less_def)
   13.10 -
   13.11  instance real :: order
   13.12 -proof qed
   13.13 - (assumption |
   13.14 -  rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+
   13.15 +proof
   13.16 +  fix u v :: real
   13.17 +  show "u < v \<longleftrightarrow> u \<le> v \<and> \<not> v \<le> u" 
   13.18 +    by (auto simp add: real_less_def intro: real_le_anti_sym)
   13.19 +qed (assumption | rule real_le_refl real_le_trans real_le_anti_sym)+
   13.20  
   13.21  (* Axiom 'linorder_linear' of class 'linorder': *)
   13.22  lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
   13.23 @@ -361,7 +359,6 @@
   13.24  apply (auto simp add: real_le real_zero_def add_ac)
   13.25  done
   13.26  
   13.27 -
   13.28  instance real :: linorder
   13.29    by (intro_classes, rule real_le_linear)
   13.30  
    14.1 --- a/src/HOL/SizeChange/Graphs.thy	Fri Jul 25 12:03:32 2008 +0200
    14.2 +++ b/src/HOL/SizeChange/Graphs.thy	Fri Jul 25 12:03:34 2008 +0200
    14.3 @@ -104,7 +104,7 @@
    14.4    fix x y z :: "('a,'b) graph"
    14.5    fix A :: "('a, 'b) graph set"
    14.6  
    14.7 -  show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
    14.8 +  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
    14.9      unfolding graph_leq_def graph_less_def
   14.10      by (cases x, cases y) auto
   14.11  
   14.12 @@ -319,7 +319,7 @@
   14.13    show "a \<le> b \<longleftrightarrow> a + b = b" unfolding graph_leq_def graph_plus_def
   14.14      by (cases a, cases b) auto
   14.15  
   14.16 -  from order_less_le show "a < b \<longleftrightarrow> a \<le> b \<and> a \<noteq> b" .
   14.17 +  from less_le_not_le show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" .
   14.18  
   14.19    show "a * star b * c = (SUP n. a * b ^ n * c)"
   14.20      unfolding graph_star_def
    15.1 --- a/src/HOL/SizeChange/Kleene_Algebras.thy	Fri Jul 25 12:03:32 2008 +0200
    15.2 +++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Fri Jul 25 12:03:34 2008 +0200
    15.3 @@ -23,40 +23,44 @@
    15.4  
    15.5  class order_by_add = idem_add + ord +
    15.6    assumes order_def: "a \<le> b \<longleftrightarrow> a + b = b"
    15.7 -  assumes strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> a \<noteq> b"
    15.8 +  assumes strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
    15.9 +begin
   15.10  
   15.11 -lemma ord_simp1[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> x + y = y"
   15.12 -  unfolding order_def .
   15.13 -lemma ord_simp2[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> y + x = y"
   15.14 -  unfolding order_def add_commute .
   15.15 -lemma ord_intro: "(x::'a::order_by_add) + y = y \<Longrightarrow> x \<le> y"
   15.16 +lemma ord_simp1[simp]: "x \<le> y \<Longrightarrow> x + y = y"
   15.17    unfolding order_def .
   15.18  
   15.19 -instance order_by_add \<subseteq> order
   15.20 -proof
   15.21 +lemma ord_simp2[simp]: "x \<le> y \<Longrightarrow> y + x = y"
   15.22 +  unfolding order_def add_commute .
   15.23 +
   15.24 +lemma ord_intro: "x + y = y \<Longrightarrow> x \<le> y"
   15.25 +  unfolding order_def .
   15.26 +
   15.27 +subclass order proof
   15.28    fix x y z :: 'a
   15.29    show "x \<le> x" unfolding order_def by simp
   15.30 -
   15.31 -  show "\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z"
   15.32 +  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
   15.33    proof (rule ord_intro)
   15.34      assume "x \<le> y" "y \<le> z"
   15.35 -
   15.36      have "x + z = x + y + z" by (simp add:`y \<le> z` add_assoc)
   15.37      also have "\<dots> = y + z" by (simp add:`x \<le> y`)
   15.38      also have "\<dots> = z" by (simp add:`y \<le> z`)
   15.39      finally show "x + z = z" .
   15.40    qed
   15.41 -
   15.42 -  show "\<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" unfolding order_def
   15.43 -    by (simp add:add_commute)
   15.44 -  show "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y" by (fact strict_order_def)
   15.45 +  show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" unfolding order_def
   15.46 +    by (simp add: add_commute)
   15.47 +  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" by (fact strict_order_def)
   15.48  qed
   15.49  
   15.50 +lemma plus_leI: 
   15.51 +  "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
   15.52 +  unfolding order_def by (simp add: add_assoc)
   15.53 +
   15.54 +end
   15.55  
   15.56  class pre_kleene = semiring_1 + order_by_add
   15.57 +begin
   15.58  
   15.59 -instance pre_kleene \<subseteq> pordered_semiring
   15.60 -proof
   15.61 +subclass pordered_semiring proof
   15.62    fix x y z :: 'a
   15.63  
   15.64    assume "x \<le> y"
   15.65 @@ -81,6 +85,11 @@
   15.66    qed
   15.67  qed
   15.68  
   15.69 +lemma zero_minimum [simp]: "0 \<le> x"
   15.70 +  unfolding order_def by simp
   15.71 +
   15.72 +end
   15.73 +
   15.74  class kleene = pre_kleene + star +
   15.75    assumes star1: "1 + a * star a \<le> star a"
   15.76    and star2: "1 + star a * a \<le> star a"
   15.77 @@ -90,22 +99,16 @@
   15.78  class kleene_by_complete_lattice = pre_kleene
   15.79    + complete_lattice + recpower + star +
   15.80    assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
   15.81 +begin
   15.82  
   15.83 -lemma plus_leI: 
   15.84 -  fixes x :: "'a :: order_by_add"
   15.85 -  shows "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
   15.86 -  unfolding order_def by (simp add:add_assoc)
   15.87 -
   15.88 -lemma le_SUPI':
   15.89 -  fixes l :: "'a :: complete_lattice"
   15.90 +lemma (in complete_lattice) le_SUPI':
   15.91    assumes "l \<le> M i"
   15.92    shows "l \<le> (SUP i. M i)"
   15.93    using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
   15.94  
   15.95 -lemma zero_minimum[simp]: "(0::'a::pre_kleene) \<le> x"
   15.96 -  unfolding order_def by simp
   15.97 +end
   15.98  
   15.99 -instance kleene_by_complete_lattice \<subseteq> kleene
  15.100 +instance kleene_by_complete_lattice < kleene
  15.101  proof
  15.102  
  15.103    fix a x :: 'a
    16.1 --- a/src/HOL/UNITY/Guar.thy	Fri Jul 25 12:03:32 2008 +0200
    16.2 +++ b/src/HOL/UNITY/Guar.thy	Fri Jul 25 12:03:34 2008 +0200
    16.3 @@ -18,13 +18,12 @@
    16.4  
    16.5  header{*Guarantees Specifications*}
    16.6  
    16.7 -theory Guar imports Comp begin
    16.8 +theory Guar
    16.9 +imports Comp
   16.10 +begin
   16.11  
   16.12  instance program :: (type) order
   16.13 -  by (intro_classes,
   16.14 -      (assumption | rule component_refl component_trans component_antisym
   16.15 -                     program_less_le)+)
   16.16 -
   16.17 +proof qed (auto simp add: program_less_le dest: component_antisym intro: component_refl component_trans)
   16.18  
   16.19  text{*Existential and Universal properties.  I formalize the two-program
   16.20        case, proving equivalence with Chandy and Sanders's n-ary definitions*}
    17.1 --- a/src/HOL/UNITY/ListOrder.thy	Fri Jul 25 12:03:32 2008 +0200
    17.2 +++ b/src/HOL/UNITY/ListOrder.thy	Fri Jul 25 12:03:34 2008 +0200
    17.3 @@ -15,7 +15,9 @@
    17.4  
    17.5  header {*The Prefix Ordering on Lists*}
    17.6  
    17.7 -theory ListOrder imports Main begin
    17.8 +theory ListOrder
    17.9 +imports Main
   17.10 +begin
   17.11  
   17.12  inductive_set
   17.13    genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
   17.14 @@ -28,15 +30,21 @@
   17.15  
   17.16   | append:  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
   17.17  
   17.18 -instance list :: (type)ord ..
   17.19 +instantiation list :: (type) ord 
   17.20 +begin
   17.21  
   17.22 -defs
   17.23 -  prefix_def:        "xs <= zs  ==  (xs,zs) : genPrefix Id"
   17.24 +definition
   17.25 +  prefix_def:        "xs <= zs \<longleftrightarrow>  (xs, zs) : genPrefix Id"
   17.26  
   17.27 -  strict_prefix_def: "xs < zs  ==  xs <= zs & xs ~= (zs::'a list)"
   17.28 -  
   17.29 +definition
   17.30 +  strict_prefix_def: "xs < zs  \<longleftrightarrow>  xs \<le> zs \<and> \<not> zs \<le> (xs :: 'a list)"
   17.31 +
   17.32 +instance ..  
   17.33  
   17.34  (*Constants for the <= and >= relations, used below in translations*)
   17.35 +
   17.36 +end
   17.37 +
   17.38  constdefs
   17.39    Le :: "(nat*nat) set"
   17.40      "Le == {(x,y). x <= y}"
   17.41 @@ -268,13 +276,13 @@
   17.42  apply (blast intro: genPrefix_antisym)
   17.43  done
   17.44  
   17.45 -lemma prefix_less_le: "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)"
   17.46 +lemma prefix_less_le_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & \<not> zs \<le> xs)"
   17.47  by (unfold strict_prefix_def, auto)
   17.48  
   17.49  instance list :: (type) order
   17.50    by (intro_classes,
   17.51        (assumption | rule prefix_refl prefix_trans prefix_antisym
   17.52 -                     prefix_less_le)+)
   17.53 +                     prefix_less_le_not_le)+)
   17.54  
   17.55  (*Monotonicity of "set" operator WRT prefix*)
   17.56  lemma set_mono: "xs <= ys ==> set xs <= set ys"
    18.1 --- a/src/HOL/Word/WordArith.thy	Fri Jul 25 12:03:32 2008 +0200
    18.2 +++ b/src/HOL/Word/WordArith.thy	Fri Jul 25 12:03:34 2008 +0200
    18.3 @@ -356,7 +356,7 @@
    18.4  
    18.5  lemma word_sless_alt: "(a <s b) == (sint a < sint b)"
    18.6    unfolding word_sle_def word_sless_def
    18.7 -  by (auto simp add : less_eq_less.less_le)
    18.8 +  by (auto simp add: less_le)
    18.9  
   18.10  lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)"
   18.11    unfolding unat_def word_le_def