removed Kleene_Algebra because of superior AFP entry; authors agreed
authornipkow
Thu May 29 16:13:47 2014 +0200 (2014-05-29)
changeset 5711270395c65c0e3
parent 57111 de33f3965ca6
child 57114 f00a299fa522
removed Kleene_Algebra because of superior AFP entry; authors agreed
NEWS
src/HOL/Library/Kleene_Algebra.thy
src/HOL/Library/Library.thy
     1.1 --- a/NEWS	Thu May 29 11:11:22 2014 +0200
     1.2 +++ b/NEWS	Thu May 29 16:13:47 2014 +0200
     1.3 @@ -755,6 +755,8 @@
     1.4  
     1.5      * Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
     1.6  
     1.7 +* Library/Kleene-Algebra was removed because AFP/Kleene_Algebra subsumes it.
     1.8 +
     1.9  *** Scala ***
    1.10  
    1.11  * The signature and semantics of Document.Snapshot.cumulate_markup /
     2.1 --- a/src/HOL/Library/Kleene_Algebra.thy	Thu May 29 11:11:22 2014 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,485 +0,0 @@
     2.4 -(*  Title:      HOL/Library/Kleene_Algebra.thy
     2.5 -    Author:     Alexander Krauss, TU Muenchen
     2.6 -    Author:     Tjark Weber, University of Cambridge
     2.7 -*)
     2.8 -
     2.9 -header {* Kleene Algebras *}
    2.10 -
    2.11 -theory Kleene_Algebra
    2.12 -imports Main 
    2.13 -begin
    2.14 -
    2.15 -text {* WARNING: This is work in progress. Expect changes in the future. *}
    2.16 -
    2.17 -text {* Various lemmas correspond to entries in a database of theorems
    2.18 -  about Kleene algebras and related structures maintained by Peter
    2.19 -  H\"ofner: see
    2.20 -  @{url "http://www.informatik.uni-augsburg.de/~hoefnepe/kleene_db/lemmas/index.html"}. *}
    2.21 -
    2.22 -subsection {* Preliminaries *}
    2.23 -
    2.24 -text {* A class where addition is idempotent. *}
    2.25 -
    2.26 -class idem_add = plus +
    2.27 -  assumes add_idem [simp]: "x + x = x"
    2.28 -
    2.29 -text {* A class of idempotent abelian semigroups (written additively). *}
    2.30 -
    2.31 -class idem_ab_semigroup_add = ab_semigroup_add + idem_add
    2.32 -begin
    2.33 -
    2.34 -lemma add_idem2 [simp]: "x + (x + y) = x + y"
    2.35 -unfolding add_assoc[symmetric] by simp
    2.36 -
    2.37 -lemma add_idem3 [simp]: "x + (y + x) = x + y"
    2.38 -by (simp add: add_commute)
    2.39 -
    2.40 -end
    2.41 -
    2.42 -text {* A class where order is defined in terms of addition. *}
    2.43 -
    2.44 -class order_by_add = plus + ord +
    2.45 -  assumes order_def: "x \<le> y \<longleftrightarrow> x + y = y"
    2.46 -  assumes strict_order_def: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    2.47 -begin
    2.48 -
    2.49 -lemma ord_simp [simp]: "x \<le> y \<Longrightarrow> x + y = y"
    2.50 -  unfolding order_def .
    2.51 -
    2.52 -lemma ord_intro: "x + y = y \<Longrightarrow> x \<le> y"
    2.53 -  unfolding order_def .
    2.54 -
    2.55 -end
    2.56 -
    2.57 -text {* A class of idempotent abelian semigroups (written additively)
    2.58 -  where order is defined in terms of addition. *}
    2.59 -
    2.60 -class ordered_idem_ab_semigroup_add = idem_ab_semigroup_add + order_by_add
    2.61 -begin
    2.62 -
    2.63 -lemma ord_simp2 [simp]: "x \<le> y \<Longrightarrow> y + x = y"
    2.64 -  unfolding order_def add_commute .
    2.65 -
    2.66 -subclass order proof
    2.67 -  fix x y z :: 'a
    2.68 -  show "x \<le> x"
    2.69 -    unfolding order_def by simp
    2.70 -  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
    2.71 -    unfolding order_def by (metis add_assoc)
    2.72 -  show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
    2.73 -    unfolding order_def by (simp add: add_commute)
    2.74 -  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    2.75 -    by (fact strict_order_def)
    2.76 -qed
    2.77 -
    2.78 -subclass ordered_ab_semigroup_add proof
    2.79 -  fix a b c :: 'a
    2.80 -  assume "a \<le> b" show "c + a \<le> c + b"
    2.81 -  proof (rule ord_intro)
    2.82 -    have "c + a + (c + b) = a + b + c" by (simp add: add_ac)
    2.83 -    also have "\<dots> = c + b" by (simp add: `a \<le> b` add_ac)
    2.84 -    finally show "c + a + (c + b) = c + b" .
    2.85 -  qed
    2.86 -qed
    2.87 -
    2.88 -lemma plus_leI [simp]: 
    2.89 -  "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
    2.90 -  unfolding order_def by (simp add: add_assoc)
    2.91 -
    2.92 -lemma less_add [simp]: "x \<le> x + y" "y \<le> x + y"
    2.93 -unfolding order_def by (auto simp: add_ac)
    2.94 -
    2.95 -lemma add_est1 [elim]: "x + y \<le> z \<Longrightarrow> x \<le> z"
    2.96 -using less_add(1) by (rule order_trans)
    2.97 -
    2.98 -lemma add_est2 [elim]: "x + y \<le> z \<Longrightarrow> y \<le> z"
    2.99 -using less_add(2) by (rule order_trans)
   2.100 -
   2.101 -lemma add_supremum: "(x + y \<le> z) = (x \<le> z \<and> y \<le> z)"
   2.102 -by auto
   2.103 -
   2.104 -end
   2.105 -
   2.106 -text {* A class of commutative monoids (written additively) where
   2.107 -  order is defined in terms of addition. *}
   2.108 -
   2.109 -class ordered_comm_monoid_add = comm_monoid_add + order_by_add
   2.110 -begin
   2.111 -
   2.112 -lemma zero_minimum [simp]: "0 \<le> x"
   2.113 -unfolding order_def by simp
   2.114 -
   2.115 -end
   2.116 -
   2.117 -text {* A class of idempotent commutative monoids (written additively)
   2.118 -  where order is defined in terms of addition. *}
   2.119 -
   2.120 -class ordered_idem_comm_monoid_add = ordered_comm_monoid_add + idem_add
   2.121 -begin
   2.122 -
   2.123 -subclass ordered_idem_ab_semigroup_add ..
   2.124 -
   2.125 -lemma sum_is_zero: "(x + y = 0) = (x = 0 \<and> y = 0)"
   2.126 -by (simp add: add_supremum eq_iff)
   2.127 -
   2.128 -end
   2.129 -
   2.130 -subsection {* A class of Kleene algebras *}
   2.131 -
   2.132 -text {* Class @{text pre_kleene} provides all operations of Kleene
   2.133 -  algebras except for the Kleene star. *}
   2.134 -
   2.135 -class pre_kleene = semiring_1 + idem_add + order_by_add
   2.136 -begin
   2.137 -
   2.138 -subclass ordered_idem_comm_monoid_add ..
   2.139 -
   2.140 -subclass ordered_semiring proof
   2.141 -  fix a b c :: 'a
   2.142 -  assume "a \<le> b"
   2.143 -
   2.144 -  show "c * a \<le> c * b"
   2.145 -  proof (rule ord_intro)
   2.146 -    from `a \<le> b` have "c * (a + b) = c * b" by simp
   2.147 -    thus "c * a + c * b = c * b" by (simp add: distrib_left)
   2.148 -  qed
   2.149 -
   2.150 -  show "a * c \<le> b * c"
   2.151 -  proof (rule ord_intro)
   2.152 -    from `a \<le> b` have "(a + b) * c = b * c" by simp
   2.153 -    thus "a * c + b * c = b * c" by (simp add: distrib_right)
   2.154 -  qed
   2.155 -qed
   2.156 -
   2.157 -end
   2.158 -
   2.159 -text {* A class that provides a star operator. *}
   2.160 -
   2.161 -class star =
   2.162 -  fixes star :: "'a \<Rightarrow> 'a"
   2.163 -
   2.164 -text {* Finally, a class of Kleene algebras. *}
   2.165 -
   2.166 -class kleene = pre_kleene + star +
   2.167 -  assumes star1: "1 + a * star a \<le> star a"
   2.168 -  and star2: "1 + star a * a \<le> star a"
   2.169 -  and star3: "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
   2.170 -  and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
   2.171 -begin
   2.172 -
   2.173 -lemma star3' [simp]:
   2.174 -  assumes a: "b + a * x \<le> x"
   2.175 -  shows "star a * b \<le> x"
   2.176 -by (metis assms less_add mult_left_mono order_trans star3 zero_minimum)
   2.177 -
   2.178 -lemma star4' [simp]:
   2.179 -  assumes a: "b + x * a \<le> x"
   2.180 -  shows "b * star a \<le> x"
   2.181 -by (metis assms less_add mult_right_mono order_trans star4 zero_minimum)
   2.182 -
   2.183 -lemma star_unfold_left: "1 + a * star a = star a"
   2.184 -proof (rule antisym, rule star1)
   2.185 -  have "1 + a * (1 + a * star a) \<le> 1 + a * star a"
   2.186 -    by (metis add_left_mono mult_left_mono star1 zero_minimum)
   2.187 -  with star3' have "star a * 1 \<le> 1 + a * star a" .
   2.188 -  thus "star a \<le> 1 + a * star a" by simp
   2.189 -qed
   2.190 -
   2.191 -lemma star_unfold_right: "1 + star a * a = star a"
   2.192 -proof (rule antisym, rule star2)
   2.193 -  have "1 + (1 + star a * a) * a \<le> 1 + star a * a"
   2.194 -    by (metis add_left_mono mult_right_mono star2 zero_minimum)
   2.195 -  with star4' have "1 * star a \<le> 1 + star a * a" .
   2.196 -  thus "star a \<le> 1 + star a * a" by simp
   2.197 -qed
   2.198 -
   2.199 -lemma star_zero [simp]: "star 0 = 1"
   2.200 -by (fact star_unfold_left[of 0, simplified, symmetric])
   2.201 -
   2.202 -lemma star_one [simp]: "star 1 = 1"
   2.203 -by (metis add_idem2 eq_iff mult_1_right ord_simp2 star3 star_unfold_left)
   2.204 -
   2.205 -lemma one_less_star [simp]: "1 \<le> star x"
   2.206 -by (metis less_add(1) star_unfold_left)
   2.207 -
   2.208 -lemma ka1 [simp]: "x * star x \<le> star x"
   2.209 -by (metis less_add(2) star_unfold_left)
   2.210 -
   2.211 -lemma star_mult_idem [simp]: "star x * star x = star x"
   2.212 -by (metis add_commute add_est1 eq_iff mult_1_right distrib_left star3 star_unfold_left)
   2.213 -
   2.214 -lemma less_star [simp]: "x \<le> star x"
   2.215 -by (metis less_add(2) mult_1_right mult_left_mono one_less_star order_trans star_unfold_left zero_minimum)
   2.216 -
   2.217 -lemma star_simulation_leq_1:
   2.218 -  assumes a: "a * x \<le> x * b"
   2.219 -  shows "star a * x \<le> x * star b"
   2.220 -proof (rule star3', rule order_trans)
   2.221 -  from a have "a * x * star b \<le> x * b * star b"
   2.222 -    by (rule mult_right_mono) simp
   2.223 -  thus "x + a * (x * star b) \<le> x + x * b * star b"
   2.224 -    using add_left_mono by (auto simp: mult_assoc)
   2.225 -  show "\<dots> \<le> x * star b"
   2.226 -    by (metis add_supremum ka1 mult.right_neutral mult_assoc mult_left_mono one_less_star zero_minimum)
   2.227 -qed
   2.228 -
   2.229 -lemma star_simulation_leq_2:
   2.230 -  assumes a: "x * a \<le> b * x"
   2.231 -  shows "x * star a \<le> star b * x"
   2.232 -proof (rule star4', rule order_trans)
   2.233 -  from a have "star b * x * a \<le> star b * b * x"
   2.234 -    by (metis mult_assoc mult_left_mono zero_minimum)
   2.235 -  thus "x + star b * x * a \<le> x + star b * b * x"
   2.236 -    using add_mono by auto
   2.237 -  show "\<dots> \<le> star b * x"
   2.238 -    by (metis add_supremum distrib_right less_add mult.left_neutral mult_assoc mult_right_mono star_unfold_right zero_minimum)
   2.239 -qed
   2.240 -
   2.241 -lemma star_simulation [simp]:
   2.242 -  assumes a: "a * x = x * b"
   2.243 -  shows "star a * x = x * star b"
   2.244 -by (metis antisym assms order_refl star_simulation_leq_1 star_simulation_leq_2)
   2.245 -
   2.246 -lemma star_slide2 [simp]: "star x * x = x * star x"
   2.247 -by (metis star_simulation)
   2.248 -
   2.249 -lemma star_idemp [simp]: "star (star x) = star x"
   2.250 -by (metis add_idem2 eq_iff less_star mult_1_right star3' star_mult_idem star_unfold_left)
   2.251 -
   2.252 -lemma star_slide [simp]: "star (x * y) * x = x * star (y * x)"
   2.253 -by (metis mult_assoc star_simulation)
   2.254 -
   2.255 -lemma star_one':
   2.256 -  assumes "p * p' = 1" "p' * p = 1"
   2.257 -  shows "p' * star a * p = star (p' * a * p)"
   2.258 -proof -
   2.259 -  from assms
   2.260 -  have "p' * star a * p = p' * star (p * p' * a) * p"
   2.261 -    by simp
   2.262 -  also have "\<dots> = p' * p * star (p' * a * p)"
   2.263 -    by (simp add: mult_assoc)
   2.264 -  also have "\<dots> = star (p' * a * p)"
   2.265 -    by (simp add: assms)
   2.266 -  finally show ?thesis .
   2.267 -qed
   2.268 -
   2.269 -lemma x_less_star [simp]: "x \<le> x * star a"
   2.270 -by (metis mult.right_neutral mult_left_mono one_less_star zero_minimum)
   2.271 -
   2.272 -lemma star_mono [simp]: "x \<le> y \<Longrightarrow> star x \<le> star y"
   2.273 -by (metis add_commute eq_iff less_star ord_simp2 order_trans star3 star4' star_idemp star_mult_idem x_less_star)
   2.274 -
   2.275 -lemma star_sub: "x \<le> 1 \<Longrightarrow> star x = 1"
   2.276 -by (metis add_commute ord_simp star_idemp star_mono star_mult_idem star_one star_unfold_left)
   2.277 -
   2.278 -lemma star_unfold2: "star x * y = y + x * star x * y"
   2.279 -by (subst star_unfold_right[symmetric]) (simp add: mult_assoc distrib_right)
   2.280 -
   2.281 -lemma star_absorb_one [simp]: "star (x + 1) = star x"
   2.282 -by (metis add_commute eq_iff distrib_right less_add mult_1_left mult_assoc star3 star_mono star_mult_idem star_unfold2 x_less_star)
   2.283 -
   2.284 -lemma star_absorb_one' [simp]: "star (1 + x) = star x"
   2.285 -by (subst add_commute) (fact star_absorb_one)
   2.286 -
   2.287 -lemma ka16: "(y * star x) * star (y * star x) \<le> star x * star (y * star x)"
   2.288 -by (metis ka1 less_add(1) mult_assoc order_trans star_unfold2)
   2.289 -
   2.290 -lemma ka16': "(star x * y) * star (star x * y) \<le> star (star x * y) * star x"
   2.291 -by (metis ka1 mult_assoc order_trans star_slide x_less_star)
   2.292 -
   2.293 -lemma ka17: "(x * star x) * star (y * star x) \<le> star x * star (y * star x)"
   2.294 -by (metis ka1 mult_assoc mult_right_mono zero_minimum)
   2.295 -
   2.296 -lemma ka18: "(x * star x) * star (y * star x) + (y * star x) * star (y * star x)
   2.297 -  \<le> star x * star (y * star x)"
   2.298 -by (metis ka16 ka17 distrib_right mult_assoc plus_leI)
   2.299 -
   2.300 -lemma star_decomp: "star (x + y) = star x * star (y * star x)"
   2.301 -proof (rule antisym)
   2.302 -  have "1 + (x + y) * star x * star (y * star x) \<le>
   2.303 -    1 + x * star x * star (y * star x) + y * star x * star (y * star x)"
   2.304 -    by (metis add_commute add_left_commute eq_iff distrib_right mult_assoc)
   2.305 -  also have "\<dots> \<le> star x * star (y * star x)"
   2.306 -    by (metis add_commute add_est1 add_left_commute ka18 plus_leI star_unfold_left x_less_star)
   2.307 -  finally show "star (x + y) \<le> star x * star (y * star x)"
   2.308 -    by (metis mult_1_right mult_assoc star3')
   2.309 -next
   2.310 -  show "star x * star (y * star x) \<le> star (x + y)"
   2.311 -    by (metis add_assoc add_est1 add_est2 add_left_commute less_star mult_mono'
   2.312 -      star_absorb_one star_absorb_one' star_idemp star_mono star_mult_idem zero_minimum)
   2.313 -qed
   2.314 -
   2.315 -lemma ka22: "y * star x \<le> star x * star y \<Longrightarrow>  star y * star x \<le> star x * star y"
   2.316 -by (metis mult_assoc mult_right_mono plus_leI star3' star_mult_idem x_less_star zero_minimum)
   2.317 -
   2.318 -lemma ka23: "star y * star x \<le> star x * star y \<Longrightarrow> y * star x \<le> star x * star y"
   2.319 -by (metis less_star mult_right_mono order_trans zero_minimum)
   2.320 -
   2.321 -lemma ka24: "star (x + y) \<le> star (star x * star y)"
   2.322 -by (metis add_est1 add_est2 less_add(1) mult_assoc order_def plus_leI star_absorb_one star_mono star_slide2 star_unfold2 star_unfold_left x_less_star)
   2.323 -
   2.324 -lemma ka25: "star y * star x \<le> star x * star y \<Longrightarrow> star (star y * star x) \<le> star x * star y"
   2.325 -proof -
   2.326 -  assume "star y * star x \<le> star x * star y"
   2.327 -  hence "\<forall>x\<^sub>1. star y * (star x * x\<^sub>1) \<le> star x * (star y * x\<^sub>1)" by (metis mult_assoc mult_right_mono zero_minimum)
   2.328 -  hence "star y * (star x * star y) \<le> star x * star y" by (metis star_mult_idem)
   2.329 -  hence "\<exists>x\<^sub>1. star (star y * star x) * star x\<^sub>1 \<le> star x * star y" by (metis star_decomp star_idemp star_simulation_leq_2 star_slide)
   2.330 -  hence "\<exists>x\<^sub>1\<ge>star (star y * star x). x\<^sub>1 \<le> star x * star y" by (metis x_less_star)
   2.331 -  thus "star (star y * star x) \<le> star x * star y" by (metis order_trans)
   2.332 -qed
   2.333 -
   2.334 -lemma church_rosser: 
   2.335 -  "star y * star x \<le> star x * star y \<Longrightarrow> star (x + y) \<le> star x * star y"
   2.336 -by (metis add_commute ka24 ka25 order_trans)
   2.337 -
   2.338 -lemma kleene_bubblesort: "y * x \<le> x * y \<Longrightarrow> star (x + y) \<le> star x * star y"
   2.339 -by (metis church_rosser star_simulation_leq_1 star_simulation_leq_2)
   2.340 -
   2.341 -lemma ka27: "star (x + star y) = star (x + y)"
   2.342 -by (metis add_commute star_decomp star_idemp)
   2.343 -
   2.344 -lemma ka28: "star (star x + star y) = star (x + y)"
   2.345 -by (metis add_commute ka27)
   2.346 -
   2.347 -lemma ka29: "(y * (1 + x) \<le> (1 + x) * star y) = (y * x \<le> (1 + x) * star y)"
   2.348 -by (metis add_supremum distrib_right less_add(1) less_star mult.left_neutral mult.right_neutral order_trans distrib_left)
   2.349 -
   2.350 -lemma ka30: "star x * star y \<le> star (x + y)"
   2.351 -by (metis mult_left_mono star_decomp star_mono x_less_star zero_minimum)
   2.352 -
   2.353 -lemma simple_simulation: "x * y = 0 \<Longrightarrow> star x * y = y"
   2.354 -by (metis mult.right_neutral mult_zero_right star_simulation star_zero)
   2.355 -
   2.356 -lemma ka32: "star (x * y) = 1 + x * star (y * x) * y"
   2.357 -by (metis mult_assoc star_slide star_unfold_left)
   2.358 -
   2.359 -lemma ka33: "x * y + 1 \<le> y \<Longrightarrow> star x \<le> y"
   2.360 -by (metis add_commute mult.right_neutral star3')
   2.361 -
   2.362 -end
   2.363 -
   2.364 -subsection {* Complete lattices are Kleene algebras *}
   2.365 -
   2.366 -lemma (in complete_lattice) SUP_upper':
   2.367 -  assumes "l \<le> M i"
   2.368 -  shows "l \<le> (SUP i. M i)"
   2.369 -  using assms by (rule order_trans) (rule SUP_upper [OF UNIV_I])
   2.370 -
   2.371 -class kleene_by_complete_lattice = pre_kleene
   2.372 -  + complete_lattice + power + star +
   2.373 -  assumes star_cont: "a * star b * c = SUPREMUM UNIV (\<lambda>n. a * b ^ n * c)"
   2.374 -begin
   2.375 -
   2.376 -subclass kleene
   2.377 -proof
   2.378 -  fix a x :: 'a
   2.379 -  
   2.380 -  have [simp]: "1 \<le> star a"
   2.381 -    unfolding star_cont[of 1 a 1, simplified] 
   2.382 -    by (subst power_0[symmetric]) (rule SUP_upper [OF UNIV_I])
   2.383 -
   2.384 -  have "a * star a \<le> star a"
   2.385 -    using star_cont[of a a 1] star_cont[of 1 a 1]
   2.386 -    by (auto simp add: power_Suc[symmetric] simp del: power_Suc
   2.387 -      intro: SUP_least SUP_upper)
   2.388 -
   2.389 -  then show "1 + a * star a \<le> star a"
   2.390 -    by simp
   2.391 -
   2.392 -  then show "1 + star a * a \<le> star a"
   2.393 -    using star_cont[of a a 1] star_cont[of 1 a a]
   2.394 -    by (simp add: power_commutes)
   2.395 -
   2.396 -  show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
   2.397 -  proof -
   2.398 -    assume a: "a * x \<le> x"
   2.399 -
   2.400 -    {
   2.401 -      fix n
   2.402 -      have "a ^ (Suc n) * x \<le> a ^ n * x"
   2.403 -      proof (induct n)
   2.404 -        case 0 thus ?case by (simp add: a)
   2.405 -      next
   2.406 -        case (Suc n)
   2.407 -        hence "a * (a ^ Suc n * x) \<le> a * (a ^ n * x)"
   2.408 -          by (auto intro: mult_mono)
   2.409 -        thus ?case
   2.410 -          by (simp add: mult_assoc)
   2.411 -      qed
   2.412 -    }
   2.413 -    note a = this
   2.414 -    
   2.415 -    {
   2.416 -      fix n have "a ^ n * x \<le> x"
   2.417 -      proof (induct n)
   2.418 -        case 0 show ?case by simp
   2.419 -      next
   2.420 -        case (Suc n) with a[of n]
   2.421 -        show ?case by simp
   2.422 -      qed
   2.423 -    }
   2.424 -    note b = this
   2.425 -    
   2.426 -    show "star a * x \<le> x"
   2.427 -      unfolding star_cont[of 1 a x, simplified]
   2.428 -      by (rule SUP_least) (rule b)
   2.429 -  qed
   2.430 -
   2.431 -  show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *)
   2.432 -  proof -
   2.433 -    assume a: "x * a \<le> x"
   2.434 -
   2.435 -    {
   2.436 -      fix n
   2.437 -      have "x * a ^ (Suc n) \<le> x * a ^ n"
   2.438 -      proof (induct n)
   2.439 -        case 0 thus ?case by (simp add: a)
   2.440 -      next
   2.441 -        case (Suc n)
   2.442 -        hence "(x * a ^ Suc n) * a  \<le> (x * a ^ n) * a"
   2.443 -          by (auto intro: mult_mono)
   2.444 -        thus ?case
   2.445 -          by (simp add: power_commutes mult_assoc)
   2.446 -      qed
   2.447 -    }
   2.448 -    note a = this
   2.449 -    
   2.450 -    {
   2.451 -      fix n have "x * a ^ n \<le> x"
   2.452 -      proof (induct n)
   2.453 -        case 0 show ?case by simp
   2.454 -      next
   2.455 -        case (Suc n) with a[of n]
   2.456 -        show ?case by simp
   2.457 -      qed
   2.458 -    }
   2.459 -    note b = this
   2.460 -    
   2.461 -    show "x * star a \<le> x"
   2.462 -      unfolding star_cont[of x a 1, simplified]
   2.463 -      by (rule SUP_least) (rule b)
   2.464 -  qed
   2.465 -qed
   2.466 -
   2.467 -end
   2.468 -
   2.469 -subsection {* Transitive closure *}
   2.470 -
   2.471 -context kleene
   2.472 -begin
   2.473 -
   2.474 -definition
   2.475 -  tcl_def: "tcl x = star x * x"
   2.476 -
   2.477 -lemma tcl_zero: "tcl 0 = 0"
   2.478 -unfolding tcl_def by simp
   2.479 -
   2.480 -lemma tcl_unfold_right: "tcl a = a + tcl a * a"
   2.481 -by (metis star_slide2 star_unfold2 tcl_def)
   2.482 -
   2.483 -lemma less_tcl: "a \<le> tcl a"
   2.484 -by (metis star_slide2 tcl_def x_less_star)
   2.485 -
   2.486 -end
   2.487 -
   2.488 -end
     3.1 --- a/src/HOL/Library/Library.thy	Thu May 29 11:11:22 2014 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Thu May 29 16:13:47 2014 +0200
     3.3 @@ -34,7 +34,6 @@
     3.4    Lattice_Syntax
     3.5    ListVector
     3.6    Lubs_Glbs
     3.7 -  Kleene_Algebra
     3.8    Mapping
     3.9    Monad_Syntax
    3.10    Multiset