src/HOL/OrderedGroup.thy
changeset 25077 c2ec5e589d78
parent 25062 af5ef0d4d655
child 25090 4a50b958391a
     1.1 --- a/src/HOL/OrderedGroup.thy	Thu Oct 18 09:20:55 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Thu Oct 18 09:20:57 2007 +0200
     1.3 @@ -35,7 +35,6 @@
     1.4  
     1.5  lemma add_left_commute: "a + (b + c) = b + (a + c)"
     1.6    by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
     1.7 -  (*FIXME term_check*)
     1.8  
     1.9  theorems add_ac = add_assoc add_commute add_left_commute
    1.10  
    1.11 @@ -52,7 +51,6 @@
    1.12  
    1.13  lemma mult_left_commute: "a * (b * c) = b * (a * c)"
    1.14    by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
    1.15 -  (*FIXME term_check*)
    1.16  
    1.17  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    1.18  
    1.19 @@ -264,6 +262,38 @@
    1.20    "- (a - b) = b - a"
    1.21    by (simp add: diff_minus add_commute)
    1.22  
    1.23 +lemma add_diff_eq: "a + (b - c) = (a + b) - c"
    1.24 +  by (simp add: diff_minus add_ac)
    1.25 +
    1.26 +lemma diff_add_eq: "(a - b) + c = (a + c) - b"
    1.27 +  by (simp add: diff_minus add_ac)
    1.28 +
    1.29 +lemma diff_eq_eq: "a - b = c \<longleftrightarrow> a = c + b"
    1.30 +  by (auto simp add: diff_minus add_assoc)
    1.31 +
    1.32 +lemma eq_diff_eq: "a = c - b \<longleftrightarrow> a + b = c"
    1.33 +  by (auto simp add: diff_minus add_assoc)
    1.34 +
    1.35 +lemma diff_diff_eq: "(a - b) - c = a - (b + c)"
    1.36 +  by (simp add: diff_minus add_ac)
    1.37 +
    1.38 +lemma diff_diff_eq2: "a - (b - c) = (a + c) - b"
    1.39 +  by (simp add: diff_minus add_ac)
    1.40 +
    1.41 +lemma diff_add_cancel: "a - b + b = a"
    1.42 +  by (simp add: diff_minus add_ac)
    1.43 +
    1.44 +lemma add_diff_cancel: "a + b - b = a"
    1.45 +  by (simp add: diff_minus add_ac)
    1.46 +
    1.47 +lemmas compare_rls =
    1.48 +       diff_minus [symmetric]
    1.49 +       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
    1.50 +       diff_eq_eq eq_diff_eq
    1.51 +
    1.52 +lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
    1.53 +  by (simp add: compare_rls)
    1.54 +
    1.55  end
    1.56  
    1.57  subsection {* (Partially) Ordered Groups *} 
    1.58 @@ -368,6 +398,14 @@
    1.59    "a + c \<le> b + c \<Longrightarrow> a \<le> b"
    1.60    by simp
    1.61  
    1.62 +lemma max_add_distrib_left:
    1.63 +  "max x y + z = max (x + z) (y + z)"
    1.64 +  unfolding max_def by auto
    1.65 +
    1.66 +lemma min_add_distrib_left:
    1.67 +  "min x y + z = min (x + z) (y + z)"
    1.68 +  unfolding min_def by auto
    1.69 +
    1.70  end
    1.71  
    1.72  class pordered_ab_group_add =
    1.73 @@ -388,6 +426,132 @@
    1.74  
    1.75  end
    1.76  
    1.77 +context pordered_ab_group_add
    1.78 +begin
    1.79 +
    1.80 +lemma max_diff_distrib_left:
    1.81 +  shows "max x y - z = max (x - z) (y - z)"
    1.82 +  by (simp add: diff_minus, rule max_add_distrib_left) 
    1.83 +
    1.84 +lemma min_diff_distrib_left:
    1.85 +  shows "min x y - z = min (x - z) (y - z)"
    1.86 +  by (simp add: diff_minus, rule min_add_distrib_left) 
    1.87 +
    1.88 +lemma le_imp_neg_le:
    1.89 +  assumes "a \<le> b"
    1.90 +  shows "-b \<le> -a"
    1.91 +proof -
    1.92 +  have "-a+a \<le> -a+b"
    1.93 +    using `a \<le> b` by (rule add_left_mono) 
    1.94 +  hence "0 \<le> -a+b"
    1.95 +    by simp
    1.96 +  hence "0 + (-b) \<le> (-a + b) + (-b)"
    1.97 +    by (rule add_right_mono) 
    1.98 +  thus ?thesis
    1.99 +    by (simp add: add_assoc)
   1.100 +qed
   1.101 +
   1.102 +lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   1.103 +proof 
   1.104 +  assume "- b \<le> - a"
   1.105 +  hence "- (- a) \<le> - (- b)"
   1.106 +    by (rule le_imp_neg_le)
   1.107 +  thus "a\<le>b" by simp
   1.108 +next
   1.109 +  assume "a\<le>b"
   1.110 +  thus "-b \<le> -a" by (rule le_imp_neg_le)
   1.111 +qed
   1.112 +
   1.113 +lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   1.114 +  by (subst neg_le_iff_le [symmetric], simp)
   1.115 +
   1.116 +lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   1.117 +  by (subst neg_le_iff_le [symmetric], simp)
   1.118 +
   1.119 +lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   1.120 +  by (force simp add: less_le) 
   1.121 +
   1.122 +lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   1.123 +  by (subst neg_less_iff_less [symmetric], simp)
   1.124 +
   1.125 +lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   1.126 +  by (subst neg_less_iff_less [symmetric], simp)
   1.127 +
   1.128 +text{*The next several equations can make the simplifier loop!*}
   1.129 +
   1.130 +lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   1.131 +proof -
   1.132 +  have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   1.133 +  thus ?thesis by simp
   1.134 +qed
   1.135 +
   1.136 +lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   1.137 +proof -
   1.138 +  have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   1.139 +  thus ?thesis by simp
   1.140 +qed
   1.141 +
   1.142 +lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   1.143 +proof -
   1.144 +  have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   1.145 +  have "(- (- a) <= -b) = (b <= - a)" 
   1.146 +    apply (auto simp only: le_less)
   1.147 +    apply (drule mm)
   1.148 +    apply (simp_all)
   1.149 +    apply (drule mm[simplified], assumption)
   1.150 +    done
   1.151 +  then show ?thesis by simp
   1.152 +qed
   1.153 +
   1.154 +lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   1.155 +  by (auto simp add: le_less minus_less_iff)
   1.156 +
   1.157 +lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
   1.158 +proof -
   1.159 +  have  "(a < b) = (a + (- b) < b + (-b))"  
   1.160 +    by (simp only: add_less_cancel_right)
   1.161 +  also have "... =  (a - b < 0)" by (simp add: diff_minus)
   1.162 +  finally show ?thesis .
   1.163 +qed
   1.164 +
   1.165 +lemma diff_less_eq: "a - b < c \<longleftrightarrow> a < c + b"
   1.166 +apply (subst less_iff_diff_less_0 [of a])
   1.167 +apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   1.168 +apply (simp add: diff_minus add_ac)
   1.169 +done
   1.170 +
   1.171 +lemma less_diff_eq: "a < c - b \<longleftrightarrow> a + b < c"
   1.172 +apply (subst less_iff_diff_less_0 [of "plus a b"])
   1.173 +apply (subst less_iff_diff_less_0 [of a])
   1.174 +apply (simp add: diff_minus add_ac)
   1.175 +done
   1.176 +
   1.177 +lemma diff_le_eq: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   1.178 +  by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   1.179 +
   1.180 +lemma le_diff_eq: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   1.181 +  by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   1.182 +
   1.183 +lemmas compare_rls =
   1.184 +       diff_minus [symmetric]
   1.185 +       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   1.186 +       diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   1.187 +       diff_eq_eq eq_diff_eq
   1.188 +
   1.189 +text{*This list of rewrites simplifies (in)equalities by bringing subtractions
   1.190 +  to the top and then moving negative terms to the other side.
   1.191 +  Use with @{text add_ac}*}
   1.192 +lemmas (in -) compare_rls =
   1.193 +       diff_minus [symmetric]
   1.194 +       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   1.195 +       diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   1.196 +       diff_eq_eq eq_diff_eq
   1.197 +
   1.198 +lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
   1.199 +  by (simp add: compare_rls)
   1.200 +
   1.201 +end
   1.202 +
   1.203  class ordered_ab_semigroup_add =
   1.204    linorder + pordered_ab_semigroup_add
   1.205  
   1.206 @@ -416,17 +580,7 @@
   1.207    qed
   1.208  qed
   1.209  
   1.210 --- {* FIXME continue localization here *}
   1.211 -
   1.212 -lemma max_add_distrib_left:
   1.213 -  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
   1.214 -  shows  "(max x y) + z = max (x+z) (y+z)"
   1.215 -by (rule max_of_mono [THEN sym], rule add_le_cancel_right)
   1.216 -
   1.217 -lemma min_add_distrib_left:
   1.218 -  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
   1.219 -  shows  "(min x y) + z = min (x+z) (y+z)"
   1.220 -by (rule min_of_mono [THEN sym], rule add_le_cancel_right)
   1.221 +-- {* FIXME localize the following *}
   1.222  
   1.223  lemma add_increasing:
   1.224    fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
   1.225 @@ -448,147 +602,6 @@
   1.226    shows "[|0\<le>a; b<c|] ==> b < a + c"
   1.227  by (insert add_le_less_mono [of 0 a b c], simp)
   1.228  
   1.229 -lemma max_diff_distrib_left:
   1.230 -  fixes z :: "'a::pordered_ab_group_add"
   1.231 -  shows  "(max x y) - z = max (x-z) (y-z)"
   1.232 -by (simp add: diff_minus, rule max_add_distrib_left) 
   1.233 -
   1.234 -lemma min_diff_distrib_left:
   1.235 -  fixes z :: "'a::pordered_ab_group_add"
   1.236 -  shows  "(min x y) - z = min (x-z) (y-z)"
   1.237 -by (simp add: diff_minus, rule min_add_distrib_left) 
   1.238 -
   1.239 -
   1.240 -subsection {* Ordering Rules for Unary Minus *}
   1.241 -
   1.242 -lemma le_imp_neg_le:
   1.243 -  assumes "a \<le> (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \<le> -a"
   1.244 -proof -
   1.245 -  have "-a+a \<le> -a+b"
   1.246 -    using `a \<le> b` by (rule add_left_mono) 
   1.247 -  hence "0 \<le> -a+b"
   1.248 -    by simp
   1.249 -  hence "0 + (-b) \<le> (-a + b) + (-b)"
   1.250 -    by (rule add_right_mono) 
   1.251 -  thus ?thesis
   1.252 -    by (simp add: add_assoc)
   1.253 -qed
   1.254 -
   1.255 -lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::pordered_ab_group_add))"
   1.256 -proof 
   1.257 -  assume "- b \<le> - a"
   1.258 -  hence "- (- a) \<le> - (- b)"
   1.259 -    by (rule le_imp_neg_le)
   1.260 -  thus "a\<le>b" by simp
   1.261 -next
   1.262 -  assume "a\<le>b"
   1.263 -  thus "-b \<le> -a" by (rule le_imp_neg_le)
   1.264 -qed
   1.265 -
   1.266 -lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::pordered_ab_group_add))"
   1.267 -by (subst neg_le_iff_le [symmetric], simp)
   1.268 -
   1.269 -lemma neg_0_le_iff_le [simp]: "(0 \<le> -a) = (a \<le> (0::'a::pordered_ab_group_add))"
   1.270 -by (subst neg_le_iff_le [symmetric], simp)
   1.271 -
   1.272 -lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::pordered_ab_group_add))"
   1.273 -by (force simp add: order_less_le) 
   1.274 -
   1.275 -lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::pordered_ab_group_add))"
   1.276 -by (subst neg_less_iff_less [symmetric], simp)
   1.277 -
   1.278 -lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::pordered_ab_group_add))"
   1.279 -by (subst neg_less_iff_less [symmetric], simp)
   1.280 -
   1.281 -text{*The next several equations can make the simplifier loop!*}
   1.282 -
   1.283 -lemma less_minus_iff: "(a < - b) = (b < - (a::'a::pordered_ab_group_add))"
   1.284 -proof -
   1.285 -  have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   1.286 -  thus ?thesis by simp
   1.287 -qed
   1.288 -
   1.289 -lemma minus_less_iff: "(- a < b) = (- b < (a::'a::pordered_ab_group_add))"
   1.290 -proof -
   1.291 -  have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   1.292 -  thus ?thesis by simp
   1.293 -qed
   1.294 -
   1.295 -lemma le_minus_iff: "(a \<le> - b) = (b \<le> - (a::'a::pordered_ab_group_add))"
   1.296 -proof -
   1.297 -  have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   1.298 -  have "(- (- a) <= -b) = (b <= - a)" 
   1.299 -    apply (auto simp only: order_le_less)
   1.300 -    apply (drule mm)
   1.301 -    apply (simp_all)
   1.302 -    apply (drule mm[simplified], assumption)
   1.303 -    done
   1.304 -  then show ?thesis by simp
   1.305 -qed
   1.306 -
   1.307 -lemma minus_le_iff: "(- a \<le> b) = (- b \<le> (a::'a::pordered_ab_group_add))"
   1.308 -by (auto simp add: order_le_less minus_less_iff)
   1.309 -
   1.310 -lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::ab_group_add)"
   1.311 -by (simp add: diff_minus add_ac)
   1.312 -
   1.313 -lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::ab_group_add)"
   1.314 -by (simp add: diff_minus add_ac)
   1.315 -
   1.316 -lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::ab_group_add))"
   1.317 -by (auto simp add: diff_minus add_assoc)
   1.318 -
   1.319 -lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::ab_group_add) = c)"
   1.320 -by (auto simp add: diff_minus add_assoc)
   1.321 -
   1.322 -lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::ab_group_add))"
   1.323 -by (simp add: diff_minus add_ac)
   1.324 -
   1.325 -lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::ab_group_add)"
   1.326 -by (simp add: diff_minus add_ac)
   1.327 -
   1.328 -lemma diff_add_cancel: "a - b + b = (a::'a::ab_group_add)"
   1.329 -by (simp add: diff_minus add_ac)
   1.330 -
   1.331 -lemma add_diff_cancel: "a + b - b = (a::'a::ab_group_add)"
   1.332 -by (simp add: diff_minus add_ac)
   1.333 -
   1.334 -text{*Further subtraction laws*}
   1.335 -
   1.336 -lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::pordered_ab_group_add))"
   1.337 -proof -
   1.338 -  have  "(a < b) = (a + (- b) < b + (-b))"  
   1.339 -    by (simp only: add_less_cancel_right)
   1.340 -  also have "... =  (a - b < 0)" by (simp add: diff_minus)
   1.341 -  finally show ?thesis .
   1.342 -qed
   1.343 -
   1.344 -lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::pordered_ab_group_add))"
   1.345 -apply (subst less_iff_diff_less_0 [of a])
   1.346 -apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   1.347 -apply (simp add: diff_minus add_ac)
   1.348 -done
   1.349 -
   1.350 -lemma less_diff_eq: "(a < c-b) = (a + (b::'a::pordered_ab_group_add) < c)"
   1.351 -apply (subst less_iff_diff_less_0 [of "a+b"])
   1.352 -apply (subst less_iff_diff_less_0 [of a])
   1.353 -apply (simp add: diff_minus add_ac)
   1.354 -done
   1.355 -
   1.356 -lemma diff_le_eq: "(a-b \<le> c) = (a \<le> c + (b::'a::pordered_ab_group_add))"
   1.357 -by (auto simp add: order_le_less diff_less_eq diff_add_cancel add_diff_cancel)
   1.358 -
   1.359 -lemma le_diff_eq: "(a \<le> c-b) = (a + (b::'a::pordered_ab_group_add) \<le> c)"
   1.360 -by (auto simp add: order_le_less less_diff_eq diff_add_cancel add_diff_cancel)
   1.361 -
   1.362 -text{*This list of rewrites simplifies (in)equalities by bringing subtractions
   1.363 -  to the top and then moving negative terms to the other side.
   1.364 -  Use with @{text add_ac}*}
   1.365 -lemmas compare_rls =
   1.366 -       diff_minus [symmetric]
   1.367 -       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   1.368 -       diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   1.369 -       diff_eq_eq eq_diff_eq
   1.370  
   1.371  subsection {* Support for reasoning about signs *}
   1.372  
   1.373 @@ -657,14 +670,6 @@
   1.374  apply (erule add_mono, assumption)
   1.375  done
   1.376  
   1.377 -subsection{*Lemmas for the @{text cancel_numerals} simproc*}
   1.378 -
   1.379 -lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::ab_group_add))"
   1.380 -by (simp add: compare_rls)
   1.381 -
   1.382 -lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::pordered_ab_group_add))"
   1.383 -by (simp add: compare_rls)
   1.384 -
   1.385  
   1.386  subsection {* Lattice Ordered (Abelian) Groups *}
   1.387  
   1.388 @@ -979,17 +984,14 @@
   1.389  lemma nprt_neg: "nprt (-x) = - pprt x"
   1.390    by (simp add: pprt_def nprt_def)
   1.391  
   1.392 -lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
   1.393 -by (simp)
   1.394 -
   1.395  lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"
   1.396 -by (simp add: iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_pprt_id] abs_prts)
   1.397 +by (simp add: iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_pprt_id] abs_prts)
   1.398  
   1.399  lemma abs_of_pos: "0 < (x::'a::lordered_ab_group_abs) ==> abs x = x";
   1.400  by (rule abs_of_nonneg, rule order_less_imp_le);
   1.401  
   1.402  lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> abs a = -(a::'a::lordered_ab_group_abs)"
   1.403 -by (simp add: iff2imp[OF le_zero_iff_zero_pprt] iff2imp[OF zero_le_iff_nprt_id] abs_prts)
   1.404 +by (simp add: iffD1[OF le_zero_iff_zero_pprt] iffD1[OF zero_le_iff_nprt_id] abs_prts)
   1.405  
   1.406  lemma abs_of_neg: "(x::'a::lordered_ab_group_abs) <  0 ==> 
   1.407    abs x = - x"
   1.408 @@ -1139,6 +1141,24 @@
   1.409    show ?thesis by (rule le_add_right_mono[OF 2 3])
   1.410  qed
   1.411  
   1.412 +lemma add_mono_thms_ordered_semiring [noatp]:
   1.413 +  fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
   1.414 +  shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
   1.415 +    and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
   1.416 +    and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
   1.417 +    and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
   1.418 +by (rule add_mono, clarify+)+
   1.419 +
   1.420 +lemma add_mono_thms_ordered_field [noatp]:
   1.421 +  fixes i j k :: "'a\<Colon>pordered_cancel_ab_semigroup_add"
   1.422 +  shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
   1.423 +    and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
   1.424 +    and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
   1.425 +    and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
   1.426 +    and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
   1.427 +by (auto intro: add_strict_right_mono add_strict_left_mono
   1.428 +  add_less_le_mono add_le_less_mono add_strict_mono)
   1.429 +
   1.430  
   1.431  subsection {* Tools setup *}
   1.432  
   1.433 @@ -1187,7 +1207,7 @@
   1.434    
   1.435  val thy_ref = Theory.check_thy @{theory};
   1.436  
   1.437 -val T = TFree("'a", ["OrderedGroup.ab_group_add"]);
   1.438 +val T = @{typ "'a\<Colon>ab_group_add"};
   1.439  
   1.440  val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
   1.441