prefix of class interpretation not mandatory any longer
authorhaftmann
Fri Mar 02 15:43:15 2007 +0100 (2007-03-02)
changeset 2238433a46e6c7f04
parent 22383 01e90256550d
child 22385 cc2be3315e72
prefix of class interpretation not mandatory any longer
NEWS
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/poly/LongDiv.thy
src/HOL/Hyperreal/StarClasses.thy
src/HOL/Lattices.thy
src/HOL/Library/ExecutableRat.thy
src/HOL/Orderings.thy
src/HOL/ex/Classpackage.thy
src/HOL/ex/CodeCollections.thy
     1.1 --- a/NEWS	Fri Mar 02 12:38:58 2007 +0100
     1.2 +++ b/NEWS	Fri Mar 02 15:43:15 2007 +0100
     1.3 @@ -505,6 +505,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
     1.8 +"cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
     1.9 +avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.
    1.10 +
    1.11  * Addes class (axclass + locale) "preorder" as superclass of "order";
    1.12  potential INCOMPATIBILITY: order of proof goals in order/linorder instance
    1.13  proofs changed.
     2.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Fri Mar 02 12:38:58 2007 +0100
     2.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Fri Mar 02 15:43:15 2007 +0100
     2.3 @@ -256,7 +256,7 @@
     2.4  proof (induct n)
     2.5    case 0 show ?case by simp
     2.6  next
     2.7 -  case Suc thus ?case by (simp add: semigroup_add_class.add_assoc) 
     2.8 +  case Suc thus ?case by (simp add: add_assoc) 
     2.9  qed
    2.10  
    2.11  lemma natsum_cong [cong]:
     3.1 --- a/src/HOL/Algebra/poly/LongDiv.thy	Fri Mar 02 12:38:58 2007 +0100
     3.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy	Fri Mar 02 15:43:15 2007 +0100
     3.3 @@ -21,7 +21,7 @@
     3.4     apply (induct_tac m)
     3.5      apply simp
     3.6     apply force
     3.7 -  apply (simp add: ab_semigroup_add_class.add_commute [of m]) 
     3.8 +  apply (simp add: add_commute [of m]) 
     3.9    done
    3.10  
    3.11  lemma SUM_extend_below: 
     4.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 02 12:38:58 2007 +0100
     4.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 02 15:43:15 2007 +0100
     4.3 @@ -318,7 +318,7 @@
     4.4  by (intro_classes, transfer, rule mult_commute)
     4.5  
     4.6  instance star :: (comm_monoid_add) comm_monoid_add
     4.7 -by (intro_classes, transfer, rule comm_monoid_add_class.add_0)
     4.8 +by (intro_classes, transfer, rule comm_monoid_add_class.zero_plus.add_0)
     4.9  
    4.10  instance star :: (monoid_mult) monoid_mult
    4.11  apply (intro_classes)
    4.12 @@ -427,12 +427,12 @@
    4.13  done
    4.14  
    4.15  instance star :: (pordered_comm_semiring) pordered_comm_semiring
    4.16 -by (intro_classes, transfer, rule mult_mono1_class.mult_mono)
    4.17 +by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono)
    4.18  
    4.19  instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
    4.20  
    4.21  instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict
    4.22 -by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.mult_strict_mono)
    4.23 +by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono)
    4.24  
    4.25  instance star :: (pordered_ring) pordered_ring ..
    4.26  instance star :: (lordered_ring) lordered_ring ..
     5.1 --- a/src/HOL/Lattices.thy	Fri Mar 02 12:38:58 2007 +0100
     5.2 +++ b/src/HOL/Lattices.thy	Fri Mar 02 15:43:15 2007 +0100
     5.3 @@ -37,13 +37,13 @@
     5.4  
     5.5  lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
     5.6  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
     5.7 - apply(blast intro:trans)
     5.8 + apply(blast intro: order_trans)
     5.9  apply simp
    5.10  done
    5.11  
    5.12  lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    5.13  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
    5.14 - apply(blast intro:trans)
    5.15 + apply(blast intro: order_trans)
    5.16  apply simp
    5.17  done
    5.18  
    5.19 @@ -51,7 +51,7 @@
    5.20  by(blast intro: inf_greatest)
    5.21  
    5.22  lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    5.23 -by(blast intro: trans)
    5.24 +by(blast intro: order_trans)
    5.25  
    5.26  lemma le_inf_iff [simp]:
    5.27   "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    5.28 @@ -70,13 +70,13 @@
    5.29  
    5.30  lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    5.31  apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
    5.32 - apply(blast intro:trans)
    5.33 + apply(blast intro: order_trans)
    5.34  apply simp
    5.35  done
    5.36  
    5.37  lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    5.38  apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
    5.39 - apply(blast intro:trans)
    5.40 + apply(blast intro: order_trans)
    5.41  apply simp
    5.42  done
    5.43  
    5.44 @@ -84,7 +84,7 @@
    5.45  by(blast intro: sup_least)
    5.46  
    5.47  lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    5.48 -by(blast intro: trans)
    5.49 +by(blast intro: order_trans)
    5.50  
    5.51  lemma ge_sup_conv[simp]:
    5.52   "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
     6.1 --- a/src/HOL/Library/ExecutableRat.thy	Fri Mar 02 12:38:58 2007 +0100
     6.2 +++ b/src/HOL/Library/ExecutableRat.thy	Fri Mar 02 15:43:15 2007 +0100
     6.3 @@ -96,7 +96,7 @@
     6.4    unfolding Fract_of_int_eq rat_number_of_def by simp
     6.5  
     6.6  lemma rat_minus [code func]:
     6.7 -  "(a\<Colon>rat) - b = a + (- b)" unfolding ab_group_add_class.diff_minus ..
     6.8 +  "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus ..
     6.9  
    6.10  lemma rat_divide [code func]:
    6.11    "(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse ..
     7.1 --- a/src/HOL/Orderings.thy	Fri Mar 02 12:38:58 2007 +0100
     7.2 +++ b/src/HOL/Orderings.thy	Fri Mar 02 15:43:15 2007 +0100
     7.3 @@ -73,15 +73,15 @@
     7.4  
     7.5  class preorder = ord +
     7.6    assumes less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
     7.7 -  and refl [iff]: "x \<sqsubseteq> x"
     7.8 -  and trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
     7.9 +  and order_refl [iff]: "x \<sqsubseteq> x"
    7.10 +  and order_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
    7.11  begin
    7.12  
    7.13  text {* Reflexivity. *}
    7.14  
    7.15  lemma eq_refl: "x = y \<Longrightarrow> x \<sqsubseteq> y"
    7.16      -- {* This form is useful with the classical reasoner. *}
    7.17 -  by (erule ssubst) (rule refl)
    7.18 +  by (erule ssubst) (rule order_refl)
    7.19  
    7.20  lemma less_irrefl [iff]: "\<not> x \<sqsubset> x"
    7.21    by (simp add: less_le)
    7.22 @@ -119,7 +119,6 @@
    7.23  
    7.24  end
    7.25  
    7.26 -
    7.27  subsection {* Partial orderings *}
    7.28  
    7.29  class order = preorder + 
    7.30 @@ -147,13 +146,13 @@
    7.31  text {* Transitivity. *}
    7.32  
    7.33  lemma less_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
    7.34 -  by (simp add: less_le) (blast intro: trans antisym)
    7.35 +  by (simp add: less_le) (blast intro: order_trans antisym)
    7.36  
    7.37  lemma le_less_trans: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
    7.38 -  by (simp add: less_le) (blast intro: trans antisym)
    7.39 +  by (simp add: less_le) (blast intro: order_trans antisym)
    7.40  
    7.41  lemma less_le_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z"
    7.42 -  by (simp add: less_le) (blast intro: trans antisym)
    7.43 +  by (simp add: less_le) (blast intro: order_trans antisym)
    7.44  
    7.45  
    7.46  text {* Useful for simplification, but too risky to include by default. *}
    7.47 @@ -189,7 +188,7 @@
    7.48    "\<lbrakk> x \<sqsubseteq> y \<Longrightarrow> P; y \<sqsubseteq> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    7.49    using linear by blast
    7.50  
    7.51 -lemma cases [case_names less equal greater]:
    7.52 +lemma linorder_cases [case_names less equal greater]:
    7.53      "\<lbrakk> x \<sqsubset> y \<Longrightarrow> P; x = y \<Longrightarrow> P; y \<sqsubset> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    7.54    using less_linear by blast
    7.55  
    7.56 @@ -239,13 +238,18 @@
    7.57    max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    7.58    "max a b = (if a \<sqsubseteq> b then b else a)"
    7.59  
    7.60 +end
    7.61 +
    7.62 +context linorder
    7.63 +begin
    7.64 +
    7.65  lemma min_le_iff_disj:
    7.66    "min x y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
    7.67 -  unfolding min_def using linear by (auto intro: trans)
    7.68 +  unfolding min_def using linear by (auto intro: order_trans)
    7.69  
    7.70  lemma le_max_iff_disj:
    7.71    "z \<sqsubseteq> max x y \<longleftrightarrow> z \<sqsubseteq> x \<or> z \<sqsubseteq> y"
    7.72 -  unfolding max_def using linear by (auto intro: trans)
    7.73 +  unfolding max_def using linear by (auto intro: order_trans)
    7.74  
    7.75  lemma min_less_iff_disj:
    7.76    "min x y \<sqsubset> z \<longleftrightarrow> x \<sqsubset> z \<or> y \<sqsubset> z"
    7.77 @@ -276,9 +280,9 @@
    7.78  
    7.79  subsection {* Name duplicates *}
    7.80  
    7.81 -lemmas order_refl [iff] = preorder_class.refl
    7.82 -lemmas order_trans = preorder_class.trans
    7.83 -lemmas order_less_le = preorder_class.less_le
    7.84 +(*lemmas order_refl [iff] = preorder_class.order_refl
    7.85 +lemmas order_trans = preorder_class.order_trans*)
    7.86 +lemmas order_less_le = less_le
    7.87  lemmas order_eq_refl = preorder_class.eq_refl
    7.88  lemmas order_less_irrefl = preorder_class.less_irrefl
    7.89  lemmas order_le_less = preorder_class.le_less
    7.90 @@ -289,7 +293,7 @@
    7.91  lemmas order_neq_le_trans = preorder_class.neq_le_trans
    7.92  lemmas order_le_neq_trans = preorder_class.le_neq_trans
    7.93  
    7.94 -lemmas order_antisym = order_class.antisym
    7.95 +lemmas order_antisym = antisym
    7.96  lemmas order_less_not_sym = order_class.less_not_sym
    7.97  lemmas order_less_asym = order_class.less_asym
    7.98  lemmas order_eq_iff = order_class.eq_iff
    7.99 @@ -302,11 +306,11 @@
   7.100  lemmas order_less_imp_triv = order_class.less_imp_triv
   7.101  lemmas order_less_asym' = order_class.less_asym'
   7.102  
   7.103 -lemmas linorder_linear = linorder_class.linear
   7.104 +lemmas linorder_linear = linear
   7.105  lemmas linorder_less_linear = linorder_class.less_linear
   7.106  lemmas linorder_le_less_linear = linorder_class.le_less_linear
   7.107  lemmas linorder_le_cases = linorder_class.le_cases
   7.108 -lemmas linorder_cases = linorder_class.cases
   7.109 +(*lemmas linorder_cases = linorder_class.linorder_cases*)
   7.110  lemmas linorder_not_less = linorder_class.not_less
   7.111  lemmas linorder_not_le = linorder_class.not_le
   7.112  lemmas linorder_neq_iff = linorder_class.neq_iff
   7.113 @@ -896,7 +900,6 @@
   7.114      "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
   7.115    by (simp add: max_def)
   7.116  
   7.117 -
   7.118  subsection {* Basic ML bindings *}
   7.119  
   7.120  ML {*
     8.1 --- a/src/HOL/ex/Classpackage.thy	Fri Mar 02 12:38:58 2007 +0100
     8.2 +++ b/src/HOL/ex/Classpackage.thy	Fri Mar 02 15:43:15 2007 +0100
     8.3 @@ -103,6 +103,11 @@
     8.4    units :: "'a set" where
     8.5    "units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}"
     8.6  
     8.7 +end
     8.8 +
     8.9 +context monoid
    8.10 +begin
    8.11 +
    8.12  lemma inv_obtain:
    8.13    assumes "x \<in> units"
    8.14    obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
    8.15 @@ -150,6 +155,11 @@
    8.16    npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    8.17    npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
    8.18  
    8.19 +end
    8.20 +
    8.21 +context monoid
    8.22 +begin
    8.23 +
    8.24  abbreviation
    8.25    npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
    8.26    "x \<^loc>\<up> n \<equiv> npow n x"
    8.27 @@ -299,24 +309,24 @@
    8.28  instance * :: (semigroup, semigroup) semigroup
    8.29    mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
    8.30                (x1 \<otimes> y1, x2 \<otimes> y2)"
    8.31 -by default (simp_all add: split_paired_all mult_prod_def semigroup_class.assoc)
    8.32 +by default (simp_all add: split_paired_all mult_prod_def assoc)
    8.33  
    8.34  instance * :: (monoidl, monoidl) monoidl
    8.35    one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
    8.36 -by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoidl_class.neutl)
    8.37 +by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl)
    8.38  
    8.39  instance * :: (monoid, monoid) monoid
    8.40 -by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.neutr)
    8.41 +by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.mult_one.neutr)
    8.42  
    8.43  instance * :: (monoid_comm, monoid_comm) monoid_comm
    8.44 -by default (simp_all add: split_paired_all mult_prod_def monoid_comm_class.comm)
    8.45 +by default (simp_all add: split_paired_all mult_prod_def comm)
    8.46  
    8.47  instance * :: (group, group) group
    8.48    inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
    8.49 -by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def group_class.invl)
    8.50 +by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl)
    8.51  
    8.52  instance * :: (group_comm, group_comm) group_comm
    8.53 -by default (simp_all add: split_paired_all mult_prod_def monoid_comm_class.comm)
    8.54 +by default (simp_all add: split_paired_all mult_prod_def comm)
    8.55  
    8.56  definition
    8.57    "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
     9.1 --- a/src/HOL/ex/CodeCollections.thy	Fri Mar 02 12:38:58 2007 +0100
     9.2 +++ b/src/HOL/ex/CodeCollections.thy	Fri Mar 02 15:43:15 2007 +0100
     9.3 @@ -17,9 +17,6 @@
     9.4  abbreviation (in ord)
     9.5    "sorted \<equiv> abs_sorted less_eq"
     9.6  
     9.7 -abbreviation
     9.8 -  "sorted \<equiv> abs_sorted less_eq"
     9.9 -
    9.10  lemma (in order) sorted_weakening:
    9.11    assumes "sorted (x # xs)"
    9.12    shows "sorted xs"
    9.13 @@ -138,7 +135,7 @@
    9.14  apply (simp_all add: "fin_*_def")
    9.15  apply (unfold split_paired_all)
    9.16  apply (rule product_all)
    9.17 -apply (rule finite_class.member_fin)+
    9.18 +apply (rule member_fin)+
    9.19  done
    9.20  
    9.21  instance option :: (finite) finite
    9.22 @@ -149,7 +146,7 @@
    9.23    proof (cases x)
    9.24      case None then show ?thesis by auto
    9.25    next
    9.26 -    case (Some x) then show ?thesis by (auto intro: finite_class.member_fin)
    9.27 +    case (Some x) then show ?thesis by (auto intro: member_fin)
    9.28    qed
    9.29  qed
    9.30