--- a/NEWS Fri Mar 02 12:38:58 2007 +0100
+++ b/NEWS Fri Mar 02 15:43:15 2007 +0100
@@ -505,6 +505,10 @@
*** HOL ***
+* Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
+"cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
+avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.
+
* Addes class (axclass + locale) "preorder" as superclass of "order";
potential INCOMPATIBILITY: order of proof goals in order/linorder instance
proofs changed.
--- a/src/HOL/Algebra/abstract/Ring2.thy Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Fri Mar 02 15:43:15 2007 +0100
@@ -256,7 +256,7 @@
proof (induct n)
case 0 show ?case by simp
next
- case Suc thus ?case by (simp add: semigroup_add_class.add_assoc)
+ case Suc thus ?case by (simp add: add_assoc)
qed
lemma natsum_cong [cong]:
--- a/src/HOL/Algebra/poly/LongDiv.thy Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy Fri Mar 02 15:43:15 2007 +0100
@@ -21,7 +21,7 @@
apply (induct_tac m)
apply simp
apply force
- apply (simp add: ab_semigroup_add_class.add_commute [of m])
+ apply (simp add: add_commute [of m])
done
lemma SUM_extend_below:
--- a/src/HOL/Hyperreal/StarClasses.thy Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy Fri Mar 02 15:43:15 2007 +0100
@@ -318,7 +318,7 @@
by (intro_classes, transfer, rule mult_commute)
instance star :: (comm_monoid_add) comm_monoid_add
-by (intro_classes, transfer, rule comm_monoid_add_class.add_0)
+by (intro_classes, transfer, rule comm_monoid_add_class.zero_plus.add_0)
instance star :: (monoid_mult) monoid_mult
apply (intro_classes)
@@ -427,12 +427,12 @@
done
instance star :: (pordered_comm_semiring) pordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.mult_mono)
+by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono)
instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict
-by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.mult_strict_mono)
+by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono)
instance star :: (pordered_ring) pordered_ring ..
instance star :: (lordered_ring) lordered_ring ..
--- a/src/HOL/Lattices.thy Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Lattices.thy Fri Mar 02 15:43:15 2007 +0100
@@ -37,13 +37,13 @@
lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
- apply(blast intro:trans)
+ apply(blast intro: order_trans)
apply simp
done
lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
- apply(blast intro:trans)
+ apply(blast intro: order_trans)
apply simp
done
@@ -51,7 +51,7 @@
by(blast intro: inf_greatest)
lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
-by(blast intro: trans)
+by(blast intro: order_trans)
lemma le_inf_iff [simp]:
"x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
@@ -70,13 +70,13 @@
lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
- apply(blast intro:trans)
+ apply(blast intro: order_trans)
apply simp
done
lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
- apply(blast intro:trans)
+ apply(blast intro: order_trans)
apply simp
done
@@ -84,7 +84,7 @@
by(blast intro: sup_least)
lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
-by(blast intro: trans)
+by(blast intro: order_trans)
lemma ge_sup_conv[simp]:
"x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
--- a/src/HOL/Library/ExecutableRat.thy Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Library/ExecutableRat.thy Fri Mar 02 15:43:15 2007 +0100
@@ -96,7 +96,7 @@
unfolding Fract_of_int_eq rat_number_of_def by simp
lemma rat_minus [code func]:
- "(a\<Colon>rat) - b = a + (- b)" unfolding ab_group_add_class.diff_minus ..
+ "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus ..
lemma rat_divide [code func]:
"(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse ..
--- a/src/HOL/Orderings.thy Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/Orderings.thy Fri Mar 02 15:43:15 2007 +0100
@@ -73,15 +73,15 @@
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 order_refl [iff]: "x \<sqsubseteq> x"
+ and order_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
begin
text {* Reflexivity. *}
lemma eq_refl: "x = y \<Longrightarrow> x \<sqsubseteq> y"
-- {* This form is useful with the classical reasoner. *}
- by (erule ssubst) (rule refl)
+ by (erule ssubst) (rule order_refl)
lemma less_irrefl [iff]: "\<not> x \<sqsubset> x"
by (simp add: less_le)
@@ -119,7 +119,6 @@
end
-
subsection {* Partial orderings *}
class order = preorder +
@@ -147,13 +146,13 @@
text {* Transitivity. *}
lemma less_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
- by (simp add: less_le) (blast intro: trans antisym)
+ by (simp add: less_le) (blast intro: order_trans antisym)
lemma le_less_trans: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
- by (simp add: less_le) (blast intro: trans antisym)
+ by (simp add: less_le) (blast intro: order_trans antisym)
lemma less_le_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
- by (simp add: less_le) (blast intro: trans antisym)
+ by (simp add: less_le) (blast intro: order_trans antisym)
text {* Useful for simplification, but too risky to include by default. *}
@@ -189,7 +188,7 @@
"\<lbrakk> x \<sqsubseteq> y \<Longrightarrow> P; y \<sqsubseteq> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
using linear by blast
-lemma cases [case_names less equal greater]:
+lemma linorder_cases [case_names less equal greater]:
"\<lbrakk> x \<sqsubset> y \<Longrightarrow> P; x = y \<Longrightarrow> P; y \<sqsubset> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
using less_linear by blast
@@ -239,13 +238,18 @@
max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
"max a b = (if a \<sqsubseteq> b then b else a)"
+end
+
+context linorder
+begin
+
lemma min_le_iff_disj:
"min x y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
- unfolding min_def using linear by (auto intro: trans)
+ unfolding min_def using linear by (auto intro: order_trans)
lemma le_max_iff_disj:
"z \<sqsubseteq> max x y \<longleftrightarrow> z \<sqsubseteq> x \<or> z \<sqsubseteq> y"
- unfolding max_def using linear by (auto intro: trans)
+ unfolding max_def using linear by (auto intro: order_trans)
lemma min_less_iff_disj:
"min x y \<sqsubset> z \<longleftrightarrow> x \<sqsubset> z \<or> y \<sqsubset> z"
@@ -276,9 +280,9 @@
subsection {* Name duplicates *}
-lemmas order_refl [iff] = preorder_class.refl
-lemmas order_trans = preorder_class.trans
-lemmas order_less_le = preorder_class.less_le
+(*lemmas order_refl [iff] = preorder_class.order_refl
+lemmas order_trans = preorder_class.order_trans*)
+lemmas order_less_le = 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
@@ -289,7 +293,7 @@
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_antisym = 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
@@ -302,11 +306,11 @@
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_linear = 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_cases = linorder_class.linorder_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
@@ -896,7 +900,6 @@
"(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
by (simp add: max_def)
-
subsection {* Basic ML bindings *}
ML {*
--- a/src/HOL/ex/Classpackage.thy Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/ex/Classpackage.thy Fri Mar 02 15:43:15 2007 +0100
@@ -103,6 +103,11 @@
units :: "'a set" where
"units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}"
+end
+
+context monoid
+begin
+
lemma inv_obtain:
assumes "x \<in> units"
obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
@@ -150,6 +155,11 @@
npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
+end
+
+context monoid
+begin
+
abbreviation
npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
"x \<^loc>\<up> n \<equiv> npow n x"
@@ -299,24 +309,24 @@
instance * :: (semigroup, semigroup) semigroup
mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
(x1 \<otimes> y1, x2 \<otimes> y2)"
-by default (simp_all add: split_paired_all mult_prod_def semigroup_class.assoc)
+by default (simp_all add: split_paired_all mult_prod_def assoc)
instance * :: (monoidl, monoidl) monoidl
one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
-by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoidl_class.neutl)
+by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl)
instance * :: (monoid, monoid) monoid
-by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.neutr)
+by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.mult_one.neutr)
instance * :: (monoid_comm, monoid_comm) monoid_comm
-by default (simp_all add: split_paired_all mult_prod_def monoid_comm_class.comm)
+by default (simp_all add: split_paired_all mult_prod_def comm)
instance * :: (group, group) group
inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
-by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def group_class.invl)
+by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl)
instance * :: (group_comm, group_comm) group_comm
-by default (simp_all add: split_paired_all mult_prod_def monoid_comm_class.comm)
+by default (simp_all add: split_paired_all mult_prod_def comm)
definition
"X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
--- a/src/HOL/ex/CodeCollections.thy Fri Mar 02 12:38:58 2007 +0100
+++ b/src/HOL/ex/CodeCollections.thy Fri Mar 02 15:43:15 2007 +0100
@@ -17,9 +17,6 @@
abbreviation (in ord)
"sorted \<equiv> abs_sorted less_eq"
-abbreviation
- "sorted \<equiv> abs_sorted less_eq"
-
lemma (in order) sorted_weakening:
assumes "sorted (x # xs)"
shows "sorted xs"
@@ -138,7 +135,7 @@
apply (simp_all add: "fin_*_def")
apply (unfold split_paired_all)
apply (rule product_all)
-apply (rule finite_class.member_fin)+
+apply (rule member_fin)+
done
instance option :: (finite) finite
@@ -149,7 +146,7 @@
proof (cases x)
case None then show ?thesis by auto
next
- case (Some x) then show ?thesis by (auto intro: finite_class.member_fin)
+ case (Some x) then show ?thesis by (auto intro: member_fin)
qed
qed