# HG changeset patch
# User haftmann
# Date 1171443972 -3600
# Node ID f662831459de416bd68815e290e99208c2594210
# Parent  42af94def7650a4d9cc61e52dba69d2118db6d58
added class "preorder"

diff -r 42af94def765 -r f662831459de NEWS
--- a/NEWS	Tue Feb 13 18:26:48 2007 +0100
+++ b/NEWS	Wed Feb 14 10:06:12 2007 +0100
@@ -79,8 +79,6 @@
 
 Reasonable default setup of framework in HOL/Main.
 
-See HOL/ex/Code*.thy for examples.
-
 Theorem attributs for selecting and transforming function equations theorems:
 
     [code fun]:       select a theorem as function equation for a specific constant
@@ -507,6 +505,10 @@
 
 *** HOL ***
 
+* Addes class (axclass + locale) "preorder" as superclass of "order";
+potential INCOMPATIBILITY: order of proof goals in order/linorder instance
+proofs changed.
+
 * Dropped lemma duplicate def_imp_eq in favor of meta_eq_to_obj_eq.
 INCOMPATIBILITY.
 
@@ -517,8 +519,7 @@
 type "'a::size ==> bool"
 
 * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
-dvd" to "Divides.div", "Divides.mod" and "Divides.dvd"
-"Divides.dvd". INCOMPATIBILITY.
+dvd" to "Divides.div", "Divides.mod" and "Divides.dvd". INCOMPATIBILITY.
 
 * Added method "lexicographic_order" automatically synthesizes
 termination relations as lexicographic combinations of size measures
diff -r 42af94def765 -r f662831459de src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Feb 13 18:26:48 2007 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Feb 14 10:06:12 2007 +0100
@@ -2520,7 +2520,7 @@
 using hom_Min_commute[of "op + k" N]
 apply simp apply(rule arg_cong[where f = Min]) apply blast
 apply(simp add:min_def linorder_not_le)
-apply(blast intro:order.antisym order_less_imp_le add_left_mono)
+apply(blast intro:order_class.antisym order_less_imp_le add_left_mono)
 done
 
 lemma add_Max_commute: fixes k::"'a::{pordered_ab_semigroup_add,linorder}"
@@ -2529,7 +2529,7 @@
 using hom_Max_commute[of "op + k" N]
 apply simp apply(rule arg_cong[where f = Max]) apply blast
 apply(simp add:max_def linorder_not_le)
-apply(blast intro:order.antisym order_less_imp_le add_left_mono)
+apply(blast intro:order_class.antisym order_less_imp_le add_left_mono)
 done
 
 
diff -r 42af94def765 -r f662831459de src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Tue Feb 13 18:26:48 2007 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy	Wed Feb 14 10:06:12 2007 +0100
@@ -11,33 +11,41 @@
 
 subsection {* Syntactic classes *}
 
-instance star :: (ord) ord ..
-instance star :: (zero) zero ..
-instance star :: (one) one ..
-instance star :: (plus) plus ..
-instance star :: (times) times ..
-instance star :: (minus) minus ..
-instance star :: (inverse) inverse ..
-instance star :: (number) number ..
-instance star :: ("Divides.div") "Divides.div" ..
-instance star :: (power) power ..
+instance star :: (ord) ord
+  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
+  star_less_def:    "(op <) \<equiv> *p2* (op <)" ..
+
+instance star :: (zero) zero
+  star_zero_def:    "0 \<equiv> star_of 0" ..
+
+instance star :: (one) one
+  star_one_def:     "1 \<equiv> star_of 1" ..
+
+instance star :: (plus) plus
+  star_add_def:     "(op +) \<equiv> *f2* (op +)" ..
+
+
+instance star :: (times) times
+  star_mult_def:    "(op *) \<equiv> *f2* (op *)" ..
 
-defs (overloaded)
-  star_zero_def:    "0 \<equiv> star_of 0"
-  star_one_def:     "1 \<equiv> star_of 1"
-  star_number_def:  "number_of b \<equiv> star_of (number_of b)"
-  star_add_def:     "(op +) \<equiv> *f2* (op +)"
-  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
+instance star :: (minus) minus
   star_minus_def:   "uminus \<equiv> *f* uminus"
-  star_mult_def:    "(op *) \<equiv> *f2* (op *)"
+  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
+  star_abs_def:     "abs \<equiv> *f* abs" ..
+
+instance star :: (inverse) inverse
   star_divide_def:  "(op /) \<equiv> *f2* (op /)"
-  star_inverse_def: "inverse \<equiv> *f* inverse"
-  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
-  star_less_def:    "(op <) \<equiv> *p2* (op <)"
-  star_abs_def:     "abs \<equiv> *f* abs"
+  star_inverse_def: "inverse \<equiv> *f* inverse" ..
+
+instance star :: (number) number
+  star_number_def:  "number_of b \<equiv> star_of (number_of b)" ..
+
+instance star :: ("Divides.div") "Divides.div"
   star_div_def:     "(op div) \<equiv> *f2* (op div)"
-  star_mod_def:     "(op mod) \<equiv> *f2* (op mod)"
-  star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
+  star_mod_def:     "(op mod) \<equiv> *f2* (op mod)" ..
+
+instance star :: (power) power
+  star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" ..
 
 lemmas star_class_defs [transfer_unfold] =
   star_zero_def     star_one_def      star_number_def
@@ -202,10 +210,10 @@
 
 instance star :: (order) order
 apply (intro_classes)
+apply (transfer, rule order_less_le)
 apply (transfer, rule order_refl)
 apply (transfer, erule (1) order_trans)
 apply (transfer, erule (1) order_antisym)
-apply (transfer, rule order_less_le)
 done
 
 instance star :: (linorder) linorder
diff -r 42af94def765 -r f662831459de src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Tue Feb 13 18:26:48 2007 +0100
+++ b/src/HOL/Library/List_lexord.thy	Wed Feb 14 10:06:12 2007 +0100
@@ -17,14 +17,14 @@
 
 instance list :: (order) order
   apply (intro_classes, unfold list_ord_defs)
-     apply (rule disjI2, safe)
-    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)
+  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
 
 instance list :: (linorder) linorder
diff -r 42af94def765 -r f662831459de src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Feb 13 18:26:48 2007 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Feb 14 10:06:12 2007 +0100
@@ -665,10 +665,10 @@
 
 instance multiset :: (order) order
   apply intro_classes
-     apply (rule mult_le_refl)
+    apply (rule mult_less_le)
+    apply (rule mult_le_refl)
     apply (erule mult_le_trans, assumption)
-   apply (erule mult_le_antisym, assumption)
-  apply (rule mult_less_le)
+    apply (erule mult_le_antisym, assumption)
   done
 
 
diff -r 42af94def765 -r f662831459de src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Feb 13 18:26:48 2007 +0100
+++ b/src/HOL/Orderings.thy	Wed Feb 14 10:06:12 2007 +0100
@@ -71,10 +71,10 @@
 
 subsection {* Quasiorders (preorders) *}
 
-locale preorder = ord +
-  assumes refl [iff]: "x \<sqsubseteq> x"
+class preorder = ord +
+  assumes less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
+  and refl [iff]: "x \<sqsubseteq> x"
   and trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
-  and less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
 begin
 
 text {* Reflexivity. *}
@@ -122,7 +122,7 @@
 
 subsection {* Partial orderings *}
 
-locale order = preorder + 
+class order = preorder + 
   assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
 
 context order
@@ -174,25 +174,10 @@
 
 end
 
-axclass order < ord
-  order_refl [iff]: "x <= x"
-  order_trans: "x <= y ==> y <= z ==> x <= z"
-  order_antisym: "x <= y ==> y <= x ==> x = y"
-  order_less_le: "(x < y) = (x <= y & x ~= y)"
-
-interpretation order:
-  order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"]
-apply unfold_locales
-apply (rule order_refl)
-apply (erule (1) order_trans)
-apply (rule order_less_le)
-apply (erule (1) order_antisym)
-done
-
 
 subsection {* Linear (total) orders *}
 
-locale linorder = order +
+class linorder = order +
   assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
 begin
 
@@ -290,50 +275,50 @@
 
 end
 
-axclass linorder < order
-  linorder_linear: "x <= y | y <= x"
-
-interpretation order:
-  linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool"]
-  by unfold_locales (rule linorder_linear)
-
 
 subsection {* Name duplicates *}
 
-lemmas order_eq_refl [where 'b = "?'a::order"] = order.eq_refl
-lemmas order_less_irrefl [where 'b = "?'a::order"] = order.less_irrefl
-lemmas order_le_less [where 'b = "?'a::order"] = order.le_less
-lemmas order_le_imp_less_or_eq [where 'b = "?'a::order"] = order.le_imp_less_or_eq
-lemmas order_less_imp_le [where 'b = "?'a::order"] = order.less_imp_le
-lemmas order_less_not_sym [where 'b = "?'a::order"] = order.less_not_sym
-lemmas order_less_asym [where 'b = "?'a::order"] = order.less_asym
-lemmas order_eq_iff [where 'b = "?'a::order"] = order.eq_iff
-lemmas order_antisym_conv [where 'b = "?'a::order"] = order.antisym_conv
-lemmas less_imp_neq [where 'b = "?'a::order"] = order.less_imp_neq
-lemmas order_less_trans [where 'b = "?'a::order"] = order.less_trans
-lemmas order_le_less_trans [where 'b = "?'a::order"] = order.le_less_trans
-lemmas order_less_le_trans [where 'b = "?'a::order"] = order.less_le_trans
-lemmas order_less_imp_not_less [where 'b = "?'a::order"] = order.less_imp_not_less
-lemmas order_less_imp_triv [where 'b = "?'a::order"] = order.less_imp_triv
-lemmas order_less_imp_not_eq [where 'b = "?'a::order"] = order.less_imp_not_eq
-lemmas order_less_imp_not_eq2 [where 'b = "?'a::order"] = order.less_imp_not_eq2
-lemmas order_neq_le_trans [where 'b = "?'a::order"] = order.neq_le_trans
-lemmas order_le_neq_trans [where 'b = "?'a::order"] = order.le_neq_trans
-lemmas order_less_asym' [where 'b = "?'a::order"] = order.less_asym'
-lemmas linorder_less_linear [where 'b = "?'a::linorder"] = order.less_linear
-lemmas linorder_le_less_linear [where 'b = "?'a::linorder"] = order.le_less_linear
-lemmas linorder_le_cases [where 'b = "?'a::linorder"] = order.le_cases
-lemmas linorder_cases [where 'b = "?'a::linorder"] = order.cases
-lemmas linorder_not_less [where 'b = "?'a::linorder"] = order.not_less
-lemmas linorder_not_le [where 'b = "?'a::linorder"] = order.not_le
-lemmas linorder_neq_iff [where 'b = "?'a::linorder"] = order.neq_iff
-lemmas linorder_neqE [where 'b = "?'a::linorder"] = order.neqE
-lemmas linorder_antisym_conv1 [where 'b = "?'a::linorder"] = order.antisym_conv1
-lemmas linorder_antisym_conv2 [where 'b = "?'a::linorder"] = order.antisym_conv2
-lemmas linorder_antisym_conv3 [where 'b = "?'a::linorder"] = order.antisym_conv3
-lemmas leI [where 'b = "?'a::linorder"] = order.leI
-lemmas leD [where 'b = "?'a::linorder"] = order.leD
-lemmas not_leE [where 'b = "?'a::linorder"] = order.not_leE
+lemmas order_refl [iff] = preorder_class.refl
+lemmas order_trans = preorder_class.trans
+lemmas order_less_le = preorder_class.less_le
+lemmas order_eq_refl = preorder_class.eq_refl
+lemmas order_less_irrefl = preorder_class.less_irrefl
+lemmas order_le_less = preorder_class.le_less
+lemmas order_le_imp_less_or_eq = preorder_class.le_imp_less_or_eq
+lemmas order_less_imp_le = preorder_class.less_imp_le
+lemmas order_less_imp_not_eq = preorder_class.less_imp_not_eq
+lemmas order_less_imp_not_eq2 = preorder_class.less_imp_not_eq2
+lemmas order_neq_le_trans = preorder_class.neq_le_trans
+lemmas order_le_neq_trans = preorder_class.le_neq_trans
+
+lemmas order_antisym = order_class.antisym
+lemmas order_less_not_sym = order_class.less_not_sym
+lemmas order_less_asym = order_class.less_asym
+lemmas order_eq_iff = order_class.eq_iff
+lemmas order_antisym_conv = order_class.antisym_conv
+lemmas less_imp_neq = order_class.less_imp_neq
+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 linorder_linear = linorder_class.linear
+lemmas linorder_less_linear = linorder_class.less_linear
+lemmas linorder_le_less_linear = linorder_class.le_less_linear
+lemmas linorder_le_cases = linorder_class.le_cases
+lemmas linorder_cases = linorder_class.cases
+lemmas linorder_not_less = linorder_class.not_less
+lemmas linorder_not_le = linorder_class.not_le
+lemmas linorder_neq_iff = linorder_class.neq_iff
+lemmas linorder_neqE = linorder_class.neqE
+lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
+lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
+lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
+lemmas leI = linorder_class.leI
+lemmas leD = linorder_class.leD
+lemmas not_leE = linorder_class.not_leE
 
 
 subsection {* Reasoning tools setup *}
@@ -866,24 +851,22 @@
   max :: "['a::ord, 'a] => 'a"
   "max a b == (if a <= b then b else a)"
 
-hide const order.less_eq_less.max order.less_eq_less.min  (* FIXME !? *)
-
 lemma min_linorder:
   "linorder.min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min"
-  by (rule+) (simp add: min_def order.min_def)
+  by rule+ (simp add: min_def linorder_class.min_def)
 
 lemma max_linorder:
   "linorder.max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = max"
-  by (rule+) (simp add: max_def order.max_def)
+  by rule+ (simp add: max_def linorder_class.max_def)
 
-lemmas min_le_iff_disj = order.min_le_iff_disj [where 'b = "?'a::linorder", unfolded min_linorder]
-lemmas le_max_iff_disj = order.le_max_iff_disj [where 'b = "?'a::linorder", unfolded max_linorder]
-lemmas min_less_iff_disj = order.min_less_iff_disj [where 'b = "?'a::linorder", unfolded min_linorder]
-lemmas less_max_iff_disj = order.less_max_iff_disj [where 'b = "?'a::linorder", unfolded max_linorder]
-lemmas min_less_iff_conj [simp] = order.min_less_iff_conj [where 'b = "?'a::linorder", unfolded min_linorder]
-lemmas max_less_iff_conj [simp] = order.max_less_iff_conj [where 'b = "?'a::linorder", unfolded max_linorder]
-lemmas split_min = order.split_min [where 'b = "?'a::linorder", unfolded min_linorder]
-lemmas split_max = order.split_max [where 'b = "?'a::linorder", unfolded max_linorder]
+lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded min_linorder]
+lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded max_linorder]
+lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded min_linorder]
+lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded max_linorder]
+lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded min_linorder]
+lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded max_linorder]
+lemmas split_min = linorder_class.split_min [unfolded min_linorder]
+lemmas split_max = linorder_class.split_max [unfolded max_linorder]
 
 lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
   by (simp add: min_def)