# HG changeset patch
# User haftmann
# Date 1216980214 -7200
# Node ID 25aceefd4786d34af4d1a801eff59b04b6e82299
# Parent  8cedebf555391ef7472eedfa81faad07ad52d0be
added class preorder

diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Bali/Decl.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -5,9 +5,8 @@
 header {* Field, method, interface, and class declarations, whole Java programs
 *}
 
-(** order is significant, because of clash for "var" **)
 theory Decl
-imports Term Table
+imports Term Table (** order is significant, because of clash for "var" **)
 begin
 
 text {*
@@ -64,10 +63,12 @@
            | Public     \<Rightarrow> False)"
 
 definition
-  le_acc_def: "a \<le> (b::acc_modi) \<longleftrightarrow> (a = b) \<or> (a < b)"
+  le_acc_def: "(a :: acc_modi) \<le> b \<longleftrightarrow> a < b \<or> a = b"
 
 instance proof
   fix x y z::acc_modi
+  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
+    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
   {
   show "x \<le> x"               \<spacespace>\<spacespace>    -- reflexivity
     by (auto simp add: le_acc_def)
@@ -85,12 +86,10 @@
       by (unfold le_acc_def) iprover
   qed
   next
-  show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
-    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
-  }
   fix x y:: acc_modi
   show  "x \<le> y \<or> y \<le> x"   
   by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
+  }
 qed
   
 end
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Int.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -187,14 +187,14 @@
 instance int :: linorder
 proof
   fix i j k :: int
-  show "(i < j) = (i \<le> j \<and> i \<noteq> j)"
-    by (simp add: less_int_def)
+  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
+    by (cases i, cases j) (simp add: le)
+  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
+    by (auto simp add: less_int_def dest: antisym) 
   show "i \<le> i"
     by (cases i) (simp add: le)
   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
     by (cases i, cases j, cases k) (simp add: le)
-  show "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
-    by (cases i, cases j) (simp add: le)
   show "i \<le> j \<or> j \<le> i"
     by (cases i, cases j) (simp add: le linorder_linear)
 qed
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Lattices.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -32,8 +32,8 @@
 
 lemma dual_lattice:
   "lower_semilattice (op \<ge>) (op >) sup"
-by unfold_locales
-  (auto simp add: sup_least)
+by (rule lower_semilattice.intro, rule dual_order)
+  (unfold_locales, simp_all add: sup_least)
 
 end
 
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Library/Char_ord.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -35,7 +35,7 @@
     by (auto simp add: nat_of_nibble_eq)
 next
   fix n m :: nibble
-  show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
+  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
     unfolding nibble_less_eq_def nibble_less_def less_le
     by (auto simp add: nat_of_nibble_eq)
 next
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Library/List_lexord.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -23,23 +23,41 @@
 end
 
 instance list :: (order) order
-  apply (intro_classes, unfold list_less_def list_le_def)
-  apply safe
-  apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
-  apply simp
-  apply assumption
-  apply (blast intro: lexord_trans transI order_less_trans)
-  apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
-  apply simp
-  apply (blast intro: lexord_trans transI order_less_trans)
-  done
+proof
+  fix xs :: "'a list"
+  show "xs \<le> xs" by (simp add: list_le_def)
+next
+  fix xs ys zs :: "'a list"
+  assume "xs \<le> ys" and "ys \<le> zs"
+  then show "xs \<le> zs" by (auto simp add: list_le_def list_less_def)
+    (rule lexord_trans, auto intro: transI)
+next
+  fix xs ys :: "'a list"
+  assume "xs \<le> ys" and "ys \<le> xs"
+  then show "xs = ys" apply (auto simp add: list_le_def list_less_def)
+  apply (rule lexord_irreflexive [THEN notE])
+  defer
+  apply (rule lexord_trans) apply (auto intro: transI) done
+next
+  fix xs ys :: "'a list"
+  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" 
+  apply (auto simp add: list_less_def list_le_def)
+  defer
+  apply (rule lexord_irreflexive [THEN notE])
+  apply auto
+  apply (rule lexord_irreflexive [THEN notE])
+  defer
+  apply (rule lexord_trans) apply (auto intro: transI) done
+qed
 
 instance list :: (linorder) linorder
-  apply (intro_classes, unfold list_le_def list_less_def, safe)
-  apply (cut_tac x = x and y = y and  r = "{(a,b). a < b}"  in lexord_linear)
-   apply force
-  apply simp
-  done
+proof
+  fix xs ys :: "'a list"
+  have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}"
+    by (rule lexord_linear) auto
+  then show "xs \<le> ys \<or> ys \<le> xs" 
+    by (auto simp add: list_le_def list_less_def)
+qed
 
 instantiation list :: (linorder) distrib_lattice
 begin
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -778,13 +778,8 @@
 theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
 unfolding le_multiset_def by auto
 
-instance
-apply intro_classes
-   apply (rule mult_less_le)
-  apply (rule mult_le_refl)
- apply (erule mult_le_trans, assumption)
-apply (erule mult_le_antisym, assumption)
-done
+instance proof
+qed (auto simp add: mult_less_le dest: mult_le_antisym elim: mult_le_trans)
 
 end
 
@@ -1101,16 +1096,16 @@
 done
 
 interpretation mset_order: order ["op \<le>#" "op <#"]
-by (auto intro: order.intro mset_le_refl mset_le_antisym
-    mset_le_trans simp: mset_less_def)
+proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
+  mset_le_trans simp: mset_less_def)
 
 interpretation mset_order_cancel_semigroup:
     pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
-by unfold_locales (erule mset_le_mono_add [OF mset_le_refl])
+proof qed (erule mset_le_mono_add [OF mset_le_refl])
 
 interpretation mset_order_semigroup_cancel:
     pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
-by (unfold_locales) simp
+proof qed simp
 
 
 lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Library/Quicksort.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -18,7 +18,7 @@
 by pat_completeness auto
 
 termination by (relation "measure size")
-  (auto simp: length_filter_le [THEN order_class.le_less_trans])
+  (auto simp: length_filter_le [THEN preorder_class.le_less_trans])
 
 lemma quicksort_permutes [simp]:
   "multiset_of (quicksort xs) = multiset_of xs"
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Library/Sublist_Order.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -47,7 +47,7 @@
   using assms by (induct rule: less_eq_list.induct) blast+
 
 definition
-  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys"
+  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
 
 lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
   by (induct rule: ileq_induct) auto
@@ -56,7 +56,7 @@
 
 instance proof
   fix xs ys :: "'a list"
-  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys" unfolding less_list_def ..
+  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
 next
   fix xs :: "'a list"
   show "xs \<le> xs" by (induct xs) (auto intro!: ileq_empty ileq_drop ileq_take)
@@ -140,7 +140,7 @@
   assumes "xs < ys"
   shows "length xs < length ys"
 proof -
-  from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_list_def)
+  from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_le)
   moreover with ileq_length have "length xs \<le> length ys" by auto
   ultimately show ?thesis by (auto intro: ileq_same_length)
 qed
@@ -154,9 +154,9 @@
 lemma ilt_below_empty[simp]: "xs < [] \<Longrightarrow> False"
   by (auto dest: ilt_length)
 lemma ilt_drop: "xs < ys \<Longrightarrow> xs < x # ys"
-  by (unfold less_list_def) (auto intro: ileq_intros)
+  by (unfold less_le) (auto intro: ileq_intros)
 lemma ilt_take: "xs < ys \<Longrightarrow> x # xs < x # ys"
-  by (unfold less_list_def) (auto intro: ileq_intros)
+  by (unfold less_le) (auto intro: ileq_intros)
 lemma ilt_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
   by (induct zs) (auto intro: ilt_drop)
 lemma ilt_take_many: "xs < ys \<Longrightarrow> zs @ xs < zs @ ys"
@@ -168,7 +168,7 @@
 lemma ileq_rev_take: "xs \<le> ys \<Longrightarrow> xs @ [x] \<le> ys @ [x]"
   by (induct rule: ileq_induct) (auto intro: ileq_intros ileq_drop_many)
 lemma ilt_rev_take: "xs < ys \<Longrightarrow> xs @ [x] < ys @ [x]"
-  by (unfold less_list_def) (auto dest: ileq_rev_take)
+  by (unfold less_le) (auto dest: ileq_rev_take)
 lemma ileq_rev_drop: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ [x]"
   by (induct rule: ileq_induct) (auto intro: ileq_intros)
 lemma ileq_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/NSA/StarDef.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -732,7 +732,7 @@
 
 instance star :: (order) order
 apply (intro_classes)
-apply (transfer, rule order_less_le)
+apply (transfer, rule less_le_not_le)
 apply (transfer, rule order_refl)
 apply (transfer, erule (1) order_trans)
 apply (transfer, erule (1) order_antisym)
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Orderings.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -11,13 +11,12 @@
   "~~/src/Provers/order.ML"
 begin
 
-subsection {* Partial orders *}
+subsection {* Quasi orders *}
 
-class order = ord +
-  assumes less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
+class preorder = ord +
+  assumes less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> (y \<le> x)"
   and order_refl [iff]: "x \<le> x"
   and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
-  assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
 begin
 
 text {* Reflexivity. *}
@@ -27,7 +26,67 @@
 by (erule ssubst) (rule order_refl)
 
 lemma less_irrefl [iff]: "\<not> x < x"
-by (simp add: less_le)
+by (simp add: less_le_not_le)
+
+lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
+unfolding less_le_not_le by blast
+
+
+text {* Asymmetry. *}
+
+lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
+by (simp add: less_le_not_le)
+
+lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
+by (drule less_not_sym, erule contrapos_np) simp
+
+
+text {* Transitivity. *}
+
+lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+by (auto simp add: less_le_not_le intro: order_trans) 
+
+lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+by (auto simp add: less_le_not_le intro: order_trans) 
+
+lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
+by (auto simp add: less_le_not_le intro: order_trans) 
+
+
+text {* Useful for simplification, but too risky to include by default. *}
+
+lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
+by (blast elim: less_asym)
+
+lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
+by (blast elim: less_asym)
+
+
+text {* Transitivity rules for calculational reasoning *}
+
+lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
+by (rule less_asym)
+
+
+text {* Dual order *}
+
+lemma dual_preorder:
+  "preorder (op \<ge>) (op >)"
+by unfold_locales (auto simp add: less_le_not_le intro: order_trans)
+
+end
+
+
+subsection {* Partial orders *}
+
+class order = preorder +
+  assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
+begin
+
+text {* Reflexivity. *}
+
+lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
+by (auto simp add: less_le_not_le intro: antisym)
 
 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
     -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
@@ -36,9 +95,6 @@
 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
 unfolding less_le by blast
 
-lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
-unfolding less_le by blast
-
 
 text {* Useful for simplification, but too risky to include by default. *}
 
@@ -60,12 +116,6 @@
 
 text {* Asymmetry. *}
 
-lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
-by (simp add: less_le antisym)
-
-lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
-by (drule less_not_sym, erule contrapos_np) simp
-
 lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
 by (blast intro: antisym)
 
@@ -76,33 +126,6 @@
 by (erule contrapos_pn, erule subst, rule less_irrefl)
 
 
-text {* Transitivity. *}
-
-lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
-by (simp add: less_le) (blast intro: order_trans antisym)
-
-lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
-by (simp add: less_le) (blast intro: order_trans antisym)
-
-lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
-by (simp add: less_le) (blast intro: order_trans antisym)
-
-
-text {* Useful for simplification, but too risky to include by default. *}
-
-lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
-by (blast elim: less_asym)
-
-lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
-by (blast elim: less_asym)
-
-
-text {* Transitivity rules for calculational reasoning *}
-
-lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
-by (rule less_asym)
-
-
 text {* Least value operator *}
 
 definition (in ord)
@@ -129,8 +152,7 @@
 
 lemma dual_order:
   "order (op \<ge>) (op >)"
-by unfold_locales
-   (simp add: less_le, auto intro: antisym order_trans)
+by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
 
 end
 
@@ -201,8 +223,7 @@
 
 lemma dual_linorder:
   "linorder (op \<ge>) (op >)"
-by unfold_locales
-  (simp add: less_le, auto intro: antisym order_trans simp add: linear)
+by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
 
 
 text {* min/max *}
@@ -557,27 +578,27 @@
 subsection {* Name duplicates *}
 
 lemmas order_less_le = less_le
-lemmas order_eq_refl = order_class.eq_refl
-lemmas order_less_irrefl = order_class.less_irrefl
+lemmas order_eq_refl = preorder_class.eq_refl
+lemmas order_less_irrefl = preorder_class.less_irrefl
 lemmas order_le_less = order_class.le_less
 lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
-lemmas order_less_imp_le = order_class.less_imp_le
+lemmas order_less_imp_le = preorder_class.less_imp_le
 lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
 lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
 lemmas order_neq_le_trans = order_class.neq_le_trans
 lemmas order_le_neq_trans = order_class.le_neq_trans
 
 lemmas order_antisym = antisym
-lemmas order_less_not_sym = order_class.less_not_sym
-lemmas order_less_asym = order_class.less_asym
+lemmas order_less_not_sym = preorder_class.less_not_sym
+lemmas order_less_asym = preorder_class.less_asym
 lemmas order_eq_iff = order_class.eq_iff
 lemmas order_antisym_conv = order_class.antisym_conv
-lemmas order_less_trans = order_class.less_trans
-lemmas order_le_less_trans = order_class.le_less_trans
-lemmas order_less_le_trans = order_class.less_le_trans
-lemmas order_less_imp_not_less = order_class.less_imp_not_less
-lemmas order_less_imp_triv = order_class.less_imp_triv
-lemmas order_less_asym' = order_class.less_asym'
+lemmas order_less_trans = preorder_class.less_trans
+lemmas order_le_less_trans = preorder_class.le_less_trans
+lemmas order_less_le_trans = preorder_class.less_le_trans
+lemmas order_less_imp_not_less = preorder_class.less_imp_not_less
+lemmas order_less_imp_triv = preorder_class.less_imp_triv
+lemmas order_less_asym' = preorder_class.less_asym'
 
 lemmas linorder_linear = linear
 lemmas linorder_less_linear = linorder_class.less_linear
@@ -808,7 +829,7 @@
   Note that this list of rules is in reverse order of priorities.
 *}
 
-lemmas order_trans_rules [trans] =
+lemmas [trans] =
   order_less_subst2
   order_less_subst1
   order_le_less_subst2
@@ -825,21 +846,61 @@
   back_subst
   rev_mp
   mp
-  order_neq_le_trans
-  order_le_neq_trans
-  order_less_trans
-  order_less_asym'
-  order_le_less_trans
-  order_less_le_trans
+
+lemmas (in order) [trans] =
+  neq_le_trans
+  le_neq_trans
+
+lemmas (in preorder) [trans] =
+  less_trans
+  less_asym'
+  le_less_trans
+  less_le_trans
   order_trans
-  order_antisym
+
+lemmas (in order) [trans] =
+  antisym
+
+lemmas (in ord) [trans] =
+  ord_le_eq_trans
+  ord_eq_le_trans
+  ord_less_eq_trans
+  ord_eq_less_trans
+
+lemmas [trans] =
+  trans
+
+lemmas order_trans_rules =
+  order_less_subst2
+  order_less_subst1
+  order_le_less_subst2
+  order_le_less_subst1
+  order_less_le_subst2
+  order_less_le_subst1
+  order_subst2
+  order_subst1
+  ord_le_eq_subst
+  ord_eq_le_subst
+  ord_less_eq_subst
+  ord_eq_less_subst
+  forw_subst
+  back_subst
+  rev_mp
+  mp
+  neq_le_trans
+  le_neq_trans
+  less_trans
+  less_asym'
+  le_less_trans
+  less_le_trans
+  order_trans
+  antisym
   ord_le_eq_trans
   ord_eq_le_trans
   ord_less_eq_trans
   ord_eq_less_trans
   trans
 
-
 (* FIXME cleanup *)
 
 text {* These support proving chains of decreasing inequalities
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Real/PReal.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -189,38 +189,37 @@
 
 subsection{*Properties of Ordering*}
 
-lemma preal_le_refl: "w \<le> (w::preal)"
-by (simp add: preal_le_def)
-
-lemma preal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::preal)"
-by (force simp add: preal_le_def)
-
-lemma preal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::preal)"
-apply (simp add: preal_le_def)
-apply (rule Rep_preal_inject [THEN iffD1], blast)
-done
-
-(* Axiom 'order_less_le' of class 'order': *)
-lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: preal_le_def preal_less_def Rep_preal_inject less_le)
-
 instance preal :: order
-  by intro_classes
-    (assumption |
-      rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
+proof
+  fix w :: preal
+  show "w \<le> w" by (simp add: preal_le_def)
+next
+  fix i j k :: preal
+  assume "i \<le> j" and "j \<le> k"
+  then show "i \<le> k" by (simp add: preal_le_def)
+next
+  fix z w :: preal
+  assume "z \<le> w" and "w \<le> z"
+  then show "z = w" by (simp add: preal_le_def Rep_preal_inject)
+next
+  fix z w :: preal
+  show "z < w \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
+  by (auto simp add: preal_le_def preal_less_def Rep_preal_inject)
+qed  
 
 lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
 by (insert preal_imp_psubset_positives, blast)
 
-lemma preal_le_linear: "x <= y | y <= (x::preal)"
-apply (auto simp add: preal_le_def)
-apply (rule ccontr)
-apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal]
+instance preal :: linorder
+proof
+  fix x y :: preal
+  show "x <= y | y <= x"
+    apply (auto simp add: preal_le_def)
+    apply (rule ccontr)
+    apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal]
              elim: order_less_asym)
-done
-
-instance preal :: linorder
-  by intro_classes (rule preal_le_linear)
+    done
+qed
 
 instantiation preal :: distrib_lattice
 begin
@@ -1091,7 +1090,7 @@
 done
 
 lemma less_add_left: "R < (S::preal) ==> R + (S-R) = S"
-by (blast intro: preal_le_anti_sym [OF less_add_left_le1 less_add_left_le2])
+by (blast intro: antisym [OF less_add_left_le1 less_add_left_le2])
 
 lemma less_add_left_Ex: "R < (S::preal) ==> \<exists>D. R + D = S"
 by (fast dest: less_add_left)
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Real/Rational.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -436,8 +436,8 @@
   next
     show "q \<le> q"
       by (induct q) simp
-    show "(q < r) = (q \<le> r \<and> q \<noteq> r)"
-      by (simp only: less_rat_def)
+    show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)"
+      by (induct q, induct r) (auto simp add: le_less mult_commute)
     show "q \<le> r \<or> r \<le> q"
       by (induct q, induct r)
          (simp add: mult_commute, rule linorder_linear)
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Real/RealDef.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -346,14 +346,12 @@
 apply (blast intro: real_trans_lemma)
 done
 
-(* Axiom 'order_less_le' of class 'order': *)
-lemma real_less_le: "((w::real) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: real_less_def)
-
 instance real :: order
-proof qed
- (assumption |
-  rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+
+proof
+  fix u v :: real
+  show "u < v \<longleftrightarrow> u \<le> v \<and> \<not> v \<le> u" 
+    by (auto simp add: real_less_def intro: real_le_anti_sym)
+qed (assumption | rule real_le_refl real_le_trans real_le_anti_sym)+
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
@@ -361,7 +359,6 @@
 apply (auto simp add: real_le real_zero_def add_ac)
 done
 
-
 instance real :: linorder
   by (intro_classes, rule real_le_linear)
 
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/SizeChange/Graphs.thy
--- a/src/HOL/SizeChange/Graphs.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/SizeChange/Graphs.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -104,7 +104,7 @@
   fix x y z :: "('a,'b) graph"
   fix A :: "('a, 'b) graph set"
 
-  show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
+  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
     unfolding graph_leq_def graph_less_def
     by (cases x, cases y) auto
 
@@ -319,7 +319,7 @@
   show "a \<le> b \<longleftrightarrow> a + b = b" unfolding graph_leq_def graph_plus_def
     by (cases a, cases b) auto
 
-  from order_less_le show "a < b \<longleftrightarrow> a \<le> b \<and> a \<noteq> b" .
+  from less_le_not_le show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" .
 
   show "a * star b * c = (SUP n. a * b ^ n * c)"
     unfolding graph_star_def
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/SizeChange/Kleene_Algebras.thy
--- a/src/HOL/SizeChange/Kleene_Algebras.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -23,40 +23,44 @@
 
 class order_by_add = idem_add + ord +
   assumes order_def: "a \<le> b \<longleftrightarrow> a + b = b"
-  assumes strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> a \<noteq> b"
+  assumes strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
+begin
 
-lemma ord_simp1[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> x + y = y"
-  unfolding order_def .
-lemma ord_simp2[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> y + x = y"
-  unfolding order_def add_commute .
-lemma ord_intro: "(x::'a::order_by_add) + y = y \<Longrightarrow> x \<le> y"
+lemma ord_simp1[simp]: "x \<le> y \<Longrightarrow> x + y = y"
   unfolding order_def .
 
-instance order_by_add \<subseteq> order
-proof
+lemma ord_simp2[simp]: "x \<le> y \<Longrightarrow> y + x = y"
+  unfolding order_def add_commute .
+
+lemma ord_intro: "x + y = y \<Longrightarrow> x \<le> y"
+  unfolding order_def .
+
+subclass order proof
   fix x y z :: 'a
   show "x \<le> x" unfolding order_def by simp
-
-  show "\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z"
+  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
   proof (rule ord_intro)
     assume "x \<le> y" "y \<le> z"
-
     have "x + z = x + y + z" by (simp add:`y \<le> z` add_assoc)
     also have "\<dots> = y + z" by (simp add:`x \<le> y`)
     also have "\<dots> = z" by (simp add:`y \<le> z`)
     finally show "x + z = z" .
   qed
-
-  show "\<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" unfolding order_def
-    by (simp add:add_commute)
-  show "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y" by (fact strict_order_def)
+  show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" unfolding order_def
+    by (simp add: add_commute)
+  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" by (fact strict_order_def)
 qed
 
+lemma plus_leI: 
+  "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
+  unfolding order_def by (simp add: add_assoc)
+
+end
 
 class pre_kleene = semiring_1 + order_by_add
+begin
 
-instance pre_kleene \<subseteq> pordered_semiring
-proof
+subclass pordered_semiring proof
   fix x y z :: 'a
 
   assume "x \<le> y"
@@ -81,6 +85,11 @@
   qed
 qed
 
+lemma zero_minimum [simp]: "0 \<le> x"
+  unfolding order_def by simp
+
+end
+
 class kleene = pre_kleene + star +
   assumes star1: "1 + a * star a \<le> star a"
   and star2: "1 + star a * a \<le> star a"
@@ -90,22 +99,16 @@
 class kleene_by_complete_lattice = pre_kleene
   + complete_lattice + recpower + star +
   assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
+begin
 
-lemma plus_leI: 
-  fixes x :: "'a :: order_by_add"
-  shows "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
-  unfolding order_def by (simp add:add_assoc)
-
-lemma le_SUPI':
-  fixes l :: "'a :: complete_lattice"
+lemma (in complete_lattice) le_SUPI':
   assumes "l \<le> M i"
   shows "l \<le> (SUP i. M i)"
   using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
 
-lemma zero_minimum[simp]: "(0::'a::pre_kleene) \<le> x"
-  unfolding order_def by simp
+end
 
-instance kleene_by_complete_lattice \<subseteq> kleene
+instance kleene_by_complete_lattice < kleene
 proof
 
   fix a x :: 'a
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/UNITY/Guar.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -18,13 +18,12 @@
 
 header{*Guarantees Specifications*}
 
-theory Guar imports Comp begin
+theory Guar
+imports Comp
+begin
 
 instance program :: (type) order
-  by (intro_classes,
-      (assumption | rule component_refl component_trans component_antisym
-                     program_less_le)+)
-
+proof qed (auto simp add: program_less_le dest: component_antisym intro: component_refl component_trans)
 
 text{*Existential and Universal properties.  I formalize the two-program
       case, proving equivalence with Chandy and Sanders's n-ary definitions*}
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/UNITY/ListOrder.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -15,7 +15,9 @@
 
 header {*The Prefix Ordering on Lists*}
 
-theory ListOrder imports Main begin
+theory ListOrder
+imports Main
+begin
 
 inductive_set
   genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
@@ -28,15 +30,21 @@
 
  | append:  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
 
-instance list :: (type)ord ..
+instantiation list :: (type) ord 
+begin
 
-defs
-  prefix_def:        "xs <= zs  ==  (xs,zs) : genPrefix Id"
+definition
+  prefix_def:        "xs <= zs \<longleftrightarrow>  (xs, zs) : genPrefix Id"
 
-  strict_prefix_def: "xs < zs  ==  xs <= zs & xs ~= (zs::'a list)"
-  
+definition
+  strict_prefix_def: "xs < zs  \<longleftrightarrow>  xs \<le> zs \<and> \<not> zs \<le> (xs :: 'a list)"
+
+instance ..  
 
 (*Constants for the <= and >= relations, used below in translations*)
+
+end
+
 constdefs
   Le :: "(nat*nat) set"
     "Le == {(x,y). x <= y}"
@@ -268,13 +276,13 @@
 apply (blast intro: genPrefix_antisym)
 done
 
-lemma prefix_less_le: "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)"
+lemma prefix_less_le_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & \<not> zs \<le> xs)"
 by (unfold strict_prefix_def, auto)
 
 instance list :: (type) order
   by (intro_classes,
       (assumption | rule prefix_refl prefix_trans prefix_antisym
-                     prefix_less_le)+)
+                     prefix_less_le_not_le)+)
 
 (*Monotonicity of "set" operator WRT prefix*)
 lemma set_mono: "xs <= ys ==> set xs <= set ys"
diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Word/WordArith.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -356,7 +356,7 @@
 
 lemma word_sless_alt: "(a <s b) == (sint a < sint b)"
   unfolding word_sle_def word_sless_def
-  by (auto simp add : less_eq_less.less_le)
+  by (auto simp add: less_le)
 
 lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)"
   unfolding unat_def word_le_def