# 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 \) \ *p2* (op \)" + star_less_def: "(op <) \ *p2* (op <)" .. + +instance star :: (zero) zero + star_zero_def: "0 \ star_of 0" .. + +instance star :: (one) one + star_one_def: "1 \ star_of 1" .. + +instance star :: (plus) plus + star_add_def: "(op +) \ *f2* (op +)" .. + + +instance star :: (times) times + star_mult_def: "(op *) \ *f2* (op *)" .. -defs (overloaded) - star_zero_def: "0 \ star_of 0" - star_one_def: "1 \ star_of 1" - star_number_def: "number_of b \ star_of (number_of b)" - star_add_def: "(op +) \ *f2* (op +)" - star_diff_def: "(op -) \ *f2* (op -)" +instance star :: (minus) minus star_minus_def: "uminus \ *f* uminus" - star_mult_def: "(op *) \ *f2* (op *)" + star_diff_def: "(op -) \ *f2* (op -)" + star_abs_def: "abs \ *f* abs" .. + +instance star :: (inverse) inverse star_divide_def: "(op /) \ *f2* (op /)" - star_inverse_def: "inverse \ *f* inverse" - star_le_def: "(op \) \ *p2* (op \)" - star_less_def: "(op <) \ *p2* (op <)" - star_abs_def: "abs \ *f* abs" + star_inverse_def: "inverse \ *f* inverse" .. + +instance star :: (number) number + star_number_def: "number_of b \ star_of (number_of b)" .. + +instance star :: ("Divides.div") "Divides.div" star_div_def: "(op div) \ *f2* (op div)" - star_mod_def: "(op mod) \ *f2* (op mod)" - star_power_def: "(op ^) \ \x n. ( *f* (\x. x ^ n)) x" + star_mod_def: "(op mod) \ *f2* (op mod)" .. + +instance star :: (power) power + star_power_def: "(op ^) \ \x n. ( *f* (\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 \ x" +class preorder = ord + + assumes less_le: "x \ y \ x \ y \ x \ y" + and refl [iff]: "x \ x" and trans: "x \ y \ y \ z \ x \ z" - and less_le: "x \ y \ x \ y \ x \ y" begin text {* Reflexivity. *} @@ -122,7 +122,7 @@ subsection {* Partial orderings *} -locale order = preorder + +class order = preorder + assumes antisym: "x \ y \ y \ x \ 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 \ \ 'a\order \ 'a \ bool" "op < \ 'a\order \ 'a \ 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 \ y \ y \ x" begin @@ -290,50 +275,50 @@ end -axclass linorder < order - linorder_linear: "x <= y | y <= x" - -interpretation order: - linorder ["op \ \ 'a\linorder \ 'a \ bool" "op < \ 'a\linorder \ 'a \ 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 \ \ 'a\linorder \ 'a \ 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 \ \ 'a\linorder \ 'a \ 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)