move Kleene_Algebra to Library
authorkrauss
Fri Jul 10 09:24:50 2009 +0200 (2009-07-10)
changeset 319901d4d0b305f16
parent 31989 a290c36e94d6
child 31991 37390299214a
child 31992 f8aed98faae7
child 32037 bed71e0d83e6
move Kleene_Algebra to Library
src/HOL/IsaMakefile
src/HOL/Library/Kleene_Algebra.thy
src/HOL/Library/Library.thy
src/HOL/SizeChange/Graphs.thy
src/HOL/SizeChange/Kleene_Algebras.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Jul 10 07:59:44 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jul 10 09:24:50 2009 +0200
     1.3 @@ -327,7 +327,7 @@
     1.4    Library/Finite_Cartesian_Product.thy \
     1.5    Library/FrechetDeriv.thy Library/Fraction_Field.thy\
     1.6    Library/Fundamental_Theorem_Algebra.thy \
     1.7 -  Library/Inner_Product.thy Library/Lattice_Syntax.thy \
     1.8 +  Library/Inner_Product.thy Library/Kleene_Algebra.thy Library/Lattice_Syntax.thy \
     1.9    Library/Legacy_GCD.thy \
    1.10    Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy Library/State_Monad.thy	\
    1.11    Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
    1.12 @@ -710,7 +710,7 @@
    1.13  
    1.14  HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz
    1.15  
    1.16 -$(LOG)/HOL-SizeChange.gz: $(OUT)/HOL SizeChange/Kleene_Algebras.thy	\
    1.17 +$(LOG)/HOL-SizeChange.gz: $(OUT)/HOL Library/Kleene_Algebra.thy	\
    1.18    SizeChange/Graphs.thy SizeChange/Misc_Tools.thy			\
    1.19    SizeChange/Criterion.thy SizeChange/Correctness.thy			\
    1.20    SizeChange/Interpretation.thy SizeChange/Implementation.thy		\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Kleene_Algebra.thy	Fri Jul 10 09:24:50 2009 +0200
     2.3 @@ -0,0 +1,495 @@
     2.4 +(*  Title:      HOL/Library/Kleene_Algebra.thy
     2.5 +    Author:     Alexander Krauss, TU Muenchen
     2.6 +*)
     2.7 +
     2.8 +header "Kleene Algebra"
     2.9 +
    2.10 +theory Kleene_Algebra
    2.11 +imports Main 
    2.12 +begin
    2.13 +
    2.14 +text {* WARNING: This is work in progress. Expect changes in the future *}
    2.15 +
    2.16 +text {* A type class of Kleene algebras *}
    2.17 +
    2.18 +class star =
    2.19 +  fixes star :: "'a \<Rightarrow> 'a"
    2.20 +
    2.21 +class idem_add = ab_semigroup_add +
    2.22 +  assumes add_idem [simp]: "x + x = x"
    2.23 +begin
    2.24 +
    2.25 +lemma add_idem2[simp]: "(x::'a) + (x + y) = x + y"
    2.26 +unfolding add_assoc[symmetric] by simp
    2.27 +
    2.28 +end
    2.29 +
    2.30 +class order_by_add = idem_add + ord +
    2.31 +  assumes order_def: "a \<le> b \<longleftrightarrow> a + b = b"
    2.32 +  assumes strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
    2.33 +begin
    2.34 +
    2.35 +lemma ord_simp1[simp]: "x \<le> y \<Longrightarrow> x + y = y"
    2.36 +  unfolding order_def .
    2.37 +
    2.38 +lemma ord_simp2[simp]: "x \<le> y \<Longrightarrow> y + x = y"
    2.39 +  unfolding order_def add_commute .
    2.40 +
    2.41 +lemma ord_intro: "x + y = y \<Longrightarrow> x \<le> y"
    2.42 +  unfolding order_def .
    2.43 +
    2.44 +subclass order proof
    2.45 +  fix x y z :: 'a
    2.46 +  show "x \<le> x" unfolding order_def by simp
    2.47 +  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
    2.48 +  proof (rule ord_intro)
    2.49 +    assume "x \<le> y" "y \<le> z"
    2.50 +    have "x + z = x + y + z" by (simp add:`y \<le> z` add_assoc)
    2.51 +    also have "\<dots> = y + z" by (simp add:`x \<le> y`)
    2.52 +    also have "\<dots> = z" by (simp add:`y \<le> z`)
    2.53 +    finally show "x + z = z" .
    2.54 +  qed
    2.55 +  show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" unfolding order_def
    2.56 +    by (simp add: add_commute)
    2.57 +  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" by (fact strict_order_def)
    2.58 +qed
    2.59 +
    2.60 +lemma plus_leI: 
    2.61 +  "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
    2.62 +  unfolding order_def by (simp add: add_assoc)
    2.63 +
    2.64 +lemma less_add[simp]: "a \<le> a + b" "b \<le> a + b"
    2.65 +unfolding order_def by (auto simp:add_ac)
    2.66 +
    2.67 +lemma add_est1: "a + b \<le> c \<Longrightarrow> a \<le> c"
    2.68 +using less_add(1) by (rule order_trans)
    2.69 +
    2.70 +lemma add_est2: "a + b \<le> c \<Longrightarrow> b \<le> c"
    2.71 +using less_add(2) by (rule order_trans)
    2.72 +
    2.73 +end
    2.74 +
    2.75 +class pre_kleene = semiring_1 + order_by_add
    2.76 +begin
    2.77 +
    2.78 +subclass pordered_semiring proof
    2.79 +  fix x y z :: 'a
    2.80 +
    2.81 +  assume "x \<le> y"
    2.82 +   
    2.83 +  show "z + x \<le> z + y"
    2.84 +  proof (rule ord_intro)
    2.85 +    have "z + x + (z + y) = x + y + z" by (simp add:add_ac)
    2.86 +    also have "\<dots> = z + y" by (simp add:`x \<le> y` add_ac)
    2.87 +    finally show "z + x + (z + y) = z + y" .
    2.88 +  qed
    2.89 +
    2.90 +  show "z * x \<le> z * y"
    2.91 +  proof (rule ord_intro)
    2.92 +    from `x \<le> y` have "z * (x + y) = z * y" by simp
    2.93 +    thus "z * x + z * y = z * y" by (simp add:right_distrib)
    2.94 +  qed
    2.95 +
    2.96 +  show "x * z \<le> y * z"
    2.97 +  proof (rule ord_intro)
    2.98 +    from `x \<le> y` have "(x + y) * z = y * z" by simp
    2.99 +    thus "x * z + y * z = y * z" by (simp add:left_distrib)
   2.100 +  qed
   2.101 +qed
   2.102 +
   2.103 +lemma zero_minimum [simp]: "0 \<le> x"
   2.104 +  unfolding order_def by simp
   2.105 +
   2.106 +end
   2.107 +
   2.108 +class kleene = pre_kleene + star +
   2.109 +  assumes star1: "1 + a * star a \<le> star a"
   2.110 +  and star2: "1 + star a * a \<le> star a"
   2.111 +  and star3: "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
   2.112 +  and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
   2.113 +begin
   2.114 +
   2.115 +lemma star3':
   2.116 +  assumes a: "b + a * x \<le> x"
   2.117 +  shows "star a * b \<le> x"
   2.118 +proof (rule order_trans)
   2.119 +  from a have "b \<le> x" by (rule add_est1)
   2.120 +  show "star a * b \<le> star a * x"
   2.121 +    by (rule mult_mono) (auto simp:`b \<le> x`)
   2.122 +
   2.123 +  from a have "a * x \<le> x" by (rule add_est2)
   2.124 +  with star3 show "star a * x \<le> x" .
   2.125 +qed
   2.126 +
   2.127 +lemma star4':
   2.128 +  assumes a: "b + x * a \<le> x"
   2.129 +  shows "b * star a \<le> x"
   2.130 +proof (rule order_trans)
   2.131 +  from a have "b \<le> x" by (rule add_est1)
   2.132 +  show "b * star a \<le> x * star a"
   2.133 +    by (rule mult_mono) (auto simp:`b \<le> x`)
   2.134 +
   2.135 +  from a have "x * a \<le> x" by (rule add_est2)
   2.136 +  with star4 show "x * star a \<le> x" .
   2.137 +qed
   2.138 +
   2.139 +lemma star_unfold_left:
   2.140 +  shows "1 + a * star a = star a"
   2.141 +proof (rule antisym, rule star1)
   2.142 +  have "1 + a * (1 + a * star a) \<le> 1 + a * star a"
   2.143 +    apply (rule add_mono, rule)
   2.144 +    apply (rule mult_mono, auto)
   2.145 +    apply (rule star1)
   2.146 +    done
   2.147 +  with star3' have "star a * 1 \<le> 1 + a * star a" .
   2.148 +  thus "star a \<le> 1 + a * star a" by simp
   2.149 +qed
   2.150 +
   2.151 +lemma star_unfold_right: "1 + star a * a = star a"
   2.152 +proof (rule antisym, rule star2)
   2.153 +  have "1 + (1 + star a * a) * a \<le> 1 + star a * a"
   2.154 +    apply (rule add_mono, rule)
   2.155 +    apply (rule mult_mono, auto)
   2.156 +    apply (rule star2)
   2.157 +    done
   2.158 +  with star4' have "1 * star a \<le> 1 + star a * a" .
   2.159 +  thus "star a \<le> 1 + star a * a" by simp
   2.160 +qed
   2.161 +
   2.162 +lemma star_zero[simp]: "star 0 = 1"
   2.163 +by (fact star_unfold_left[of 0, simplified, symmetric])
   2.164 +
   2.165 +lemma star_one[simp]: "star 1 = 1"
   2.166 +by (metis add_idem2 eq_iff mult_1_right ord_simp2 star3 star_unfold_left)
   2.167 +
   2.168 +lemma one_less_star: "1 \<le> star x"
   2.169 +by (metis less_add(1) star_unfold_left)
   2.170 +
   2.171 +lemma ka1: "x * star x \<le> star x"
   2.172 +by (metis less_add(2) star_unfold_left)
   2.173 +
   2.174 +lemma star_mult_idem[simp]: "star x * star x = star x"
   2.175 +by (metis add_commute add_est1 eq_iff mult_1_right right_distrib star3 star_unfold_left)
   2.176 +
   2.177 +lemma less_star: "x \<le> star x"
   2.178 +by (metis less_add(2) mult_1_right mult_left_mono one_less_star order_trans star_unfold_left zero_minimum)
   2.179 +
   2.180 +lemma star_simulation:
   2.181 +  assumes a: "a * x = x * b"
   2.182 +  shows "star a * x = x * star b"
   2.183 +proof (rule antisym)
   2.184 +  show "star a * x \<le> x * star b"
   2.185 +  proof (rule star3', rule order_trans)
   2.186 +    from a have "a * x \<le> x * b" by simp
   2.187 +    hence "a * x * star b \<le> x * b * star b"
   2.188 +      by (rule mult_mono) auto
   2.189 +    thus "x + a * (x * star b) \<le> x + x * b * star b"
   2.190 +      using add_mono by (auto simp: mult_assoc)
   2.191 +    show "\<dots> \<le> x * star b"
   2.192 +    proof -
   2.193 +      have "x * (1 + b * star b) \<le> x * star b"
   2.194 +        by (rule mult_mono[OF _ star1]) auto
   2.195 +      thus ?thesis
   2.196 +        by (simp add:right_distrib mult_assoc)
   2.197 +    qed
   2.198 +  qed
   2.199 +  show "x * star b \<le> star a * x"
   2.200 +  proof (rule star4', rule order_trans)
   2.201 +    from a have b: "x * b \<le> a * x" by simp
   2.202 +    have "star a * x * b \<le> star a * a * x"
   2.203 +      unfolding mult_assoc
   2.204 +      by (rule mult_mono[OF _ b]) auto
   2.205 +    thus "x + star a * x * b \<le> x + star a * a * x"
   2.206 +      using add_mono by auto
   2.207 +    show "\<dots> \<le> star a * x"
   2.208 +    proof -
   2.209 +      have "(1 + star a * a) * x \<le> star a * x"
   2.210 +        by (rule mult_mono[OF star2]) auto
   2.211 +      thus ?thesis
   2.212 +        by (simp add:left_distrib mult_assoc)
   2.213 +    qed
   2.214 +  qed
   2.215 +qed
   2.216 +
   2.217 +lemma star_slide2[simp]: "star x * x = x * star x"
   2.218 +by (metis star_simulation)
   2.219 +
   2.220 +lemma star_idemp[simp]: "star (star x) = star x"
   2.221 +by (metis add_idem2 eq_iff less_star mult_1_right star3' star_mult_idem star_unfold_left)
   2.222 +
   2.223 +lemma star_slide[simp]: "star (x * y) * x = x * star (y * x)"
   2.224 +by (auto simp: mult_assoc star_simulation)
   2.225 +
   2.226 +lemma star_one':
   2.227 +  assumes "p * p' = 1" "p' * p = 1"
   2.228 +  shows "p' * star a * p = star (p' * a * p)"
   2.229 +proof -
   2.230 +  from assms
   2.231 +  have "p' * star a * p = p' * star (p * p' * a) * p"
   2.232 +    by simp
   2.233 +  also have "\<dots> = p' * p * star (p' * a * p)"
   2.234 +    by (simp add: mult_assoc)
   2.235 +  also have "\<dots> = star (p' * a * p)"
   2.236 +    by (simp add: assms)
   2.237 +  finally show ?thesis .
   2.238 +qed
   2.239 +
   2.240 +lemma x_less_star[simp]: "x \<le> x * star a"
   2.241 +proof -
   2.242 +  have "x \<le> x * (1 + a * star a)" by (simp add: right_distrib)
   2.243 +  also have "\<dots> = x * star a" by (simp only: star_unfold_left)
   2.244 +  finally show ?thesis .
   2.245 +qed
   2.246 +
   2.247 +lemma star_mono:  "x \<le> y \<Longrightarrow>  star x \<le> star y"
   2.248 +by (metis add_commute eq_iff less_star ord_simp2 order_trans star3 star4' star_idemp star_mult_idem x_less_star)
   2.249 +
   2.250 +lemma star_sub: "x \<le> 1 \<Longrightarrow> star x = 1"
   2.251 +by (metis add_commute ord_simp1 star_idemp star_mono star_mult_idem star_one star_unfold_left)
   2.252 +
   2.253 +lemma star_unfold2: "star x * y = y + x * star x * y"
   2.254 +by (subst star_unfold_right[symmetric]) (simp add: mult_assoc left_distrib)
   2.255 +
   2.256 +lemma star_absorb_one[simp]: "star (x + 1) = star x"
   2.257 +by (metis add_commute eq_iff left_distrib less_add(1) less_add(2) mult_1_left mult_assoc star3 star_mono star_mult_idem star_unfold2 x_less_star)
   2.258 +
   2.259 +lemma star_absorb_one'[simp]: "star (1 + x) = star x"
   2.260 +by (subst add_commute) (fact star_absorb_one)
   2.261 +
   2.262 +lemma ka16: "(y * star x) * star (y * star x) \<le> star x * star (y * star x)"
   2.263 +by (metis ka1 less_add(1) mult_assoc order_trans star_unfold2)
   2.264 +
   2.265 +lemma ka16': "(star x * y) * star (star x * y) \<le> star (star x * y) * star x"
   2.266 +by (metis ka1 mult_assoc order_trans star_slide x_less_star)
   2.267 +
   2.268 +lemma ka17: "(x * star x) * star (y * star x) \<le> star x * star (y * star x)"
   2.269 +by (metis ka1 mult_assoc mult_right_mono zero_minimum)
   2.270 +
   2.271 +lemma ka18: "(x * star x) * star (y * star x) + (y * star x) * star (y * star x)
   2.272 +  \<le> star x * star (y * star x)"
   2.273 +by (metis ka16 ka17 left_distrib mult_assoc plus_leI)
   2.274 +
   2.275 +lemma kleene_church_rosser: 
   2.276 +  "star y * star x \<le> star x * star y \<Longrightarrow> star (x + y) \<le> star x * star y"
   2.277 +oops
   2.278 +
   2.279 +lemma star_decomp: "star (a + b) = star a * star (b * star a)"
   2.280 +oops
   2.281 +
   2.282 +lemma ka22: "y * star x \<le> star x * star y \<Longrightarrow>  star y * star x \<le> star x * star y"
   2.283 +by (metis mult_assoc mult_right_mono plus_leI star3' star_mult_idem x_less_star zero_minimum)
   2.284 +
   2.285 +lemma ka23: "star y * star x \<le> star x * star y \<Longrightarrow> y * star x \<le> star x * star y"
   2.286 +by (metis less_star mult_right_mono order_trans zero_minimum)
   2.287 +
   2.288 +lemma ka24: "star (x + y) \<le> star (star x * star y)"
   2.289 +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.290 +
   2.291 +lemma ka25: "star y * star x \<le> star x * star y \<Longrightarrow> star (star y * star x) \<le> star x * star y"
   2.292 +oops
   2.293 +
   2.294 +lemma kleene_bubblesort: "y * x \<le> x * y \<Longrightarrow> star (x + y) \<le> star x * star y"
   2.295 +oops
   2.296 +
   2.297 +end
   2.298 +
   2.299 +subsection {* Complete lattices are Kleene algebras *}
   2.300 +
   2.301 +lemma (in complete_lattice) le_SUPI':
   2.302 +  assumes "l \<le> M i"
   2.303 +  shows "l \<le> (SUP i. M i)"
   2.304 +  using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
   2.305 +
   2.306 +class kleene_by_complete_lattice = pre_kleene
   2.307 +  + complete_lattice + power + star +
   2.308 +  assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
   2.309 +begin
   2.310 +
   2.311 +subclass kleene
   2.312 +proof
   2.313 +  fix a x :: 'a
   2.314 +  
   2.315 +  have [simp]: "1 \<le> star a"
   2.316 +    unfolding star_cont[of 1 a 1, simplified] 
   2.317 +    by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
   2.318 +  
   2.319 +  show "1 + a * star a \<le> star a" 
   2.320 +    apply (rule plus_leI, simp)
   2.321 +    apply (simp add:star_cont[of a a 1, simplified])
   2.322 +    apply (simp add:star_cont[of 1 a 1, simplified])
   2.323 +    apply (subst power_Suc[symmetric])
   2.324 +    by (intro SUP_leI le_SUPI UNIV_I)
   2.325 +
   2.326 +  show "1 + star a * a \<le> star a" 
   2.327 +    apply (rule plus_leI, simp)
   2.328 +    apply (simp add:star_cont[of 1 a a, simplified])
   2.329 +    apply (simp add:star_cont[of 1 a 1, simplified])
   2.330 +    by (auto intro: SUP_leI le_SUPI simp add: power_Suc[symmetric] power_commutes simp del: power_Suc)
   2.331 +
   2.332 +  show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
   2.333 +  proof -
   2.334 +    assume a: "a * x \<le> x"
   2.335 +
   2.336 +    {
   2.337 +      fix n
   2.338 +      have "a ^ (Suc n) * x \<le> a ^ n * x"
   2.339 +      proof (induct n)
   2.340 +        case 0 thus ?case by (simp add: a)
   2.341 +      next
   2.342 +        case (Suc n)
   2.343 +        hence "a * (a ^ Suc n * x) \<le> a * (a ^ n * x)"
   2.344 +          by (auto intro: mult_mono)
   2.345 +        thus ?case
   2.346 +          by (simp add: mult_assoc)
   2.347 +      qed
   2.348 +    }
   2.349 +    note a = this
   2.350 +    
   2.351 +    {
   2.352 +      fix n have "a ^ n * x \<le> x"
   2.353 +      proof (induct n)
   2.354 +        case 0 show ?case by simp
   2.355 +      next
   2.356 +        case (Suc n) with a[of n]
   2.357 +        show ?case by simp
   2.358 +      qed
   2.359 +    }
   2.360 +    note b = this
   2.361 +    
   2.362 +    show "star a * x \<le> x"
   2.363 +      unfolding star_cont[of 1 a x, simplified]
   2.364 +      by (rule SUP_leI) (rule b)
   2.365 +  qed
   2.366 +
   2.367 +  show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *)
   2.368 +  proof -
   2.369 +    assume a: "x * a \<le> x"
   2.370 +
   2.371 +    {
   2.372 +      fix n
   2.373 +      have "x * a ^ (Suc n) \<le> x * a ^ n"
   2.374 +      proof (induct n)
   2.375 +        case 0 thus ?case by (simp add: a)
   2.376 +      next
   2.377 +        case (Suc n)
   2.378 +        hence "(x * a ^ Suc n) * a  \<le> (x * a ^ n) * a"
   2.379 +          by (auto intro: mult_mono)
   2.380 +        thus ?case
   2.381 +          by (simp add: power_commutes mult_assoc)
   2.382 +      qed
   2.383 +    }
   2.384 +    note a = this
   2.385 +    
   2.386 +    {
   2.387 +      fix n have "x * a ^ n \<le> x"
   2.388 +      proof (induct n)
   2.389 +        case 0 show ?case by simp
   2.390 +      next
   2.391 +        case (Suc n) with a[of n]
   2.392 +        show ?case by simp
   2.393 +      qed
   2.394 +    }
   2.395 +    note b = this
   2.396 +    
   2.397 +    show "x * star a \<le> x"
   2.398 +      unfolding star_cont[of x a 1, simplified]
   2.399 +      by (rule SUP_leI) (rule b)
   2.400 +  qed
   2.401 +qed
   2.402 +
   2.403 +end
   2.404 +
   2.405 +
   2.406 +subsection {* Transitive Closure *}
   2.407 +
   2.408 +context kleene
   2.409 +begin
   2.410 +
   2.411 +definition 
   2.412 +  tcl_def:  "tcl x = star x * x"
   2.413 +
   2.414 +lemma tcl_zero: "tcl 0 = 0"
   2.415 +unfolding tcl_def by simp
   2.416 +
   2.417 +lemma tcl_unfold_right: "tcl a = a + tcl a * a"
   2.418 +proof -
   2.419 +  from star_unfold_right[of a]
   2.420 +  have "a * (1 + star a * a) = a * star a" by simp
   2.421 +  from this[simplified right_distrib, simplified]
   2.422 +  show ?thesis
   2.423 +    by (simp add:tcl_def mult_assoc)
   2.424 +qed
   2.425 +
   2.426 +lemma less_tcl: "a \<le> tcl a"
   2.427 +proof -
   2.428 +  have "a \<le> a + tcl a * a" by simp
   2.429 +  also have "\<dots> = tcl a" by (rule tcl_unfold_right[symmetric])
   2.430 +  finally show ?thesis .
   2.431 +qed
   2.432 +
   2.433 +end
   2.434 +
   2.435 +
   2.436 +subsection {* Naive Algorithm to generate the transitive closure *}
   2.437 +
   2.438 +function (default "\<lambda>x. 0", tailrec, domintros)
   2.439 +  mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"
   2.440 +where
   2.441 +  "mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))"
   2.442 +  by pat_completeness simp
   2.443 +
   2.444 +declare mk_tcl.simps[simp del] (* loops *)
   2.445 +
   2.446 +lemma mk_tcl_code[code]:
   2.447 +  "mk_tcl A X = 
   2.448 +  (let XA = X * A 
   2.449 +  in if XA \<le> X then X else mk_tcl A (X + XA))"
   2.450 +  unfolding mk_tcl.simps[of A X] Let_def ..
   2.451 +
   2.452 +context kleene
   2.453 +begin
   2.454 +
   2.455 +lemma mk_tcl_lemma1:
   2.456 +  "(X + X * A) * star A = X * star A"
   2.457 +proof -
   2.458 +  have "A * star A \<le> 1 + A * star A" by simp
   2.459 +  also have "\<dots> = star A" by (simp add:star_unfold_left)
   2.460 +  finally have "star A + A * star A = star A" by simp
   2.461 +  hence "X * (star A + A * star A) = X * star A" by simp
   2.462 +  thus ?thesis by (simp add:left_distrib right_distrib mult_assoc)
   2.463 +qed
   2.464 +
   2.465 +lemma mk_tcl_lemma2:
   2.466 +  shows "X * A \<le> X \<Longrightarrow> X * star A = X"
   2.467 +  by (rule antisym) (auto simp:star4)
   2.468 +
   2.469 +end
   2.470 +
   2.471 +lemma mk_tcl_correctness:
   2.472 +  fixes X :: "'a::kleene"
   2.473 +  assumes "mk_tcl_dom (A, X)"
   2.474 +  shows "mk_tcl A X = X * star A"
   2.475 +  using assms
   2.476 +  by induct (auto simp: mk_tcl_lemma1 mk_tcl_lemma2)
   2.477 +
   2.478 +
   2.479 +lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
   2.480 +  by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases)
   2.481 +
   2.482 +lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
   2.483 +  unfolding mk_tcl_def
   2.484 +  by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom])
   2.485 +
   2.486 +
   2.487 +text {* We can replace the dom-Condition of the correctness theorem 
   2.488 +  with something executable *}
   2.489 +
   2.490 +lemma mk_tcl_correctness2:
   2.491 +  fixes A X :: "'a :: {kleene}"
   2.492 +  assumes "mk_tcl A A \<noteq> 0"
   2.493 +  shows "mk_tcl A A = tcl A"
   2.494 +  using assms mk_tcl_default mk_tcl_correctness
   2.495 +  unfolding tcl_def 
   2.496 +  by auto
   2.497 +
   2.498 +end
     3.1 --- a/src/HOL/Library/Library.thy	Fri Jul 10 07:59:44 2009 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Fri Jul 10 09:24:50 2009 +0200
     3.3 @@ -34,6 +34,7 @@
     3.4    Inner_Product
     3.5    Lattice_Syntax
     3.6    ListVector
     3.7 +  Kleene_Algebra
     3.8    Mapping
     3.9    Multiset
    3.10    Nat_Infinity
     4.1 --- a/src/HOL/SizeChange/Graphs.thy	Fri Jul 10 07:59:44 2009 +0200
     4.2 +++ b/src/HOL/SizeChange/Graphs.thy	Fri Jul 10 09:24:50 2009 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* General Graphs as Sets *}
     4.5  
     4.6  theory Graphs
     4.7 -imports Main Misc_Tools Kleene_Algebras
     4.8 +imports Main Misc_Tools Kleene_Algebra
     4.9  begin
    4.10  
    4.11  subsection {* Basic types, Size Change Graphs *}
     5.1 --- a/src/HOL/SizeChange/Kleene_Algebras.thy	Fri Jul 10 07:59:44 2009 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,494 +0,0 @@
     5.4 -(*  Title:      HOL/Library/Kleene_Algebras.thy
     5.5 -    ID:         $Id$
     5.6 -    Author:     Alexander Krauss, TU Muenchen
     5.7 -*)
     5.8 -
     5.9 -header "Kleene Algebras"
    5.10 -
    5.11 -theory Kleene_Algebras
    5.12 -imports Main 
    5.13 -begin
    5.14 -
    5.15 -text {* A type class of Kleene algebras *}
    5.16 -
    5.17 -class star =
    5.18 -  fixes star :: "'a \<Rightarrow> 'a"
    5.19 -
    5.20 -class idem_add = ab_semigroup_add +
    5.21 -  assumes add_idem [simp]: "x + x = x"
    5.22 -begin
    5.23 -
    5.24 -lemma add_idem2[simp]: "(x::'a) + (x + y) = x + y"
    5.25 -unfolding add_assoc[symmetric] by simp
    5.26 -
    5.27 -end
    5.28 -
    5.29 -class order_by_add = idem_add + ord +
    5.30 -  assumes order_def: "a \<le> b \<longleftrightarrow> a + b = b"
    5.31 -  assumes strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
    5.32 -begin
    5.33 -
    5.34 -lemma ord_simp1[simp]: "x \<le> y \<Longrightarrow> x + y = y"
    5.35 -  unfolding order_def .
    5.36 -
    5.37 -lemma ord_simp2[simp]: "x \<le> y \<Longrightarrow> y + x = y"
    5.38 -  unfolding order_def add_commute .
    5.39 -
    5.40 -lemma ord_intro: "x + y = y \<Longrightarrow> x \<le> y"
    5.41 -  unfolding order_def .
    5.42 -
    5.43 -subclass order proof
    5.44 -  fix x y z :: 'a
    5.45 -  show "x \<le> x" unfolding order_def by simp
    5.46 -  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
    5.47 -  proof (rule ord_intro)
    5.48 -    assume "x \<le> y" "y \<le> z"
    5.49 -    have "x + z = x + y + z" by (simp add:`y \<le> z` add_assoc)
    5.50 -    also have "\<dots> = y + z" by (simp add:`x \<le> y`)
    5.51 -    also have "\<dots> = z" by (simp add:`y \<le> z`)
    5.52 -    finally show "x + z = z" .
    5.53 -  qed
    5.54 -  show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" unfolding order_def
    5.55 -    by (simp add: add_commute)
    5.56 -  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" by (fact strict_order_def)
    5.57 -qed
    5.58 -
    5.59 -lemma plus_leI: 
    5.60 -  "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
    5.61 -  unfolding order_def by (simp add: add_assoc)
    5.62 -
    5.63 -lemma less_add[simp]: "a \<le> a + b" "b \<le> a + b"
    5.64 -unfolding order_def by (auto simp:add_ac)
    5.65 -
    5.66 -lemma add_est1: "a + b \<le> c \<Longrightarrow> a \<le> c"
    5.67 -using less_add(1) by (rule order_trans)
    5.68 -
    5.69 -lemma add_est2: "a + b \<le> c \<Longrightarrow> b \<le> c"
    5.70 -using less_add(2) by (rule order_trans)
    5.71 -
    5.72 -end
    5.73 -
    5.74 -class pre_kleene = semiring_1 + order_by_add
    5.75 -begin
    5.76 -
    5.77 -subclass pordered_semiring proof
    5.78 -  fix x y z :: 'a
    5.79 -
    5.80 -  assume "x \<le> y"
    5.81 -   
    5.82 -  show "z + x \<le> z + y"
    5.83 -  proof (rule ord_intro)
    5.84 -    have "z + x + (z + y) = x + y + z" by (simp add:add_ac)
    5.85 -    also have "\<dots> = z + y" by (simp add:`x \<le> y` add_ac)
    5.86 -    finally show "z + x + (z + y) = z + y" .
    5.87 -  qed
    5.88 -
    5.89 -  show "z * x \<le> z * y"
    5.90 -  proof (rule ord_intro)
    5.91 -    from `x \<le> y` have "z * (x + y) = z * y" by simp
    5.92 -    thus "z * x + z * y = z * y" by (simp add:right_distrib)
    5.93 -  qed
    5.94 -
    5.95 -  show "x * z \<le> y * z"
    5.96 -  proof (rule ord_intro)
    5.97 -    from `x \<le> y` have "(x + y) * z = y * z" by simp
    5.98 -    thus "x * z + y * z = y * z" by (simp add:left_distrib)
    5.99 -  qed
   5.100 -qed
   5.101 -
   5.102 -lemma zero_minimum [simp]: "0 \<le> x"
   5.103 -  unfolding order_def by simp
   5.104 -
   5.105 -end
   5.106 -
   5.107 -class kleene = pre_kleene + star +
   5.108 -  assumes star1: "1 + a * star a \<le> star a"
   5.109 -  and star2: "1 + star a * a \<le> star a"
   5.110 -  and star3: "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
   5.111 -  and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
   5.112 -begin
   5.113 -
   5.114 -lemma star3':
   5.115 -  assumes a: "b + a * x \<le> x"
   5.116 -  shows "star a * b \<le> x"
   5.117 -proof (rule order_trans)
   5.118 -  from a have "b \<le> x" by (rule add_est1)
   5.119 -  show "star a * b \<le> star a * x"
   5.120 -    by (rule mult_mono) (auto simp:`b \<le> x`)
   5.121 -
   5.122 -  from a have "a * x \<le> x" by (rule add_est2)
   5.123 -  with star3 show "star a * x \<le> x" .
   5.124 -qed
   5.125 -
   5.126 -lemma star4':
   5.127 -  assumes a: "b + x * a \<le> x"
   5.128 -  shows "b * star a \<le> x"
   5.129 -proof (rule order_trans)
   5.130 -  from a have "b \<le> x" by (rule add_est1)
   5.131 -  show "b * star a \<le> x * star a"
   5.132 -    by (rule mult_mono) (auto simp:`b \<le> x`)
   5.133 -
   5.134 -  from a have "x * a \<le> x" by (rule add_est2)
   5.135 -  with star4 show "x * star a \<le> x" .
   5.136 -qed
   5.137 -
   5.138 -lemma star_unfold_left:
   5.139 -  shows "1 + a * star a = star a"
   5.140 -proof (rule antisym, rule star1)
   5.141 -  have "1 + a * (1 + a * star a) \<le> 1 + a * star a"
   5.142 -    apply (rule add_mono, rule)
   5.143 -    apply (rule mult_mono, auto)
   5.144 -    apply (rule star1)
   5.145 -    done
   5.146 -  with star3' have "star a * 1 \<le> 1 + a * star a" .
   5.147 -  thus "star a \<le> 1 + a * star a" by simp
   5.148 -qed
   5.149 -
   5.150 -lemma star_unfold_right: "1 + star a * a = star a"
   5.151 -proof (rule antisym, rule star2)
   5.152 -  have "1 + (1 + star a * a) * a \<le> 1 + star a * a"
   5.153 -    apply (rule add_mono, rule)
   5.154 -    apply (rule mult_mono, auto)
   5.155 -    apply (rule star2)
   5.156 -    done
   5.157 -  with star4' have "1 * star a \<le> 1 + star a * a" .
   5.158 -  thus "star a \<le> 1 + star a * a" by simp
   5.159 -qed
   5.160 -
   5.161 -lemma star_zero[simp]: "star 0 = 1"
   5.162 -by (fact star_unfold_left[of 0, simplified, symmetric])
   5.163 -
   5.164 -lemma star_one[simp]: "star 1 = 1"
   5.165 -by (metis add_idem2 eq_iff mult_1_right ord_simp2 star3 star_unfold_left)
   5.166 -
   5.167 -lemma one_less_star: "1 \<le> star x"
   5.168 -by (metis less_add(1) star_unfold_left)
   5.169 -
   5.170 -lemma ka1: "x * star x \<le> star x"
   5.171 -by (metis less_add(2) star_unfold_left)
   5.172 -
   5.173 -lemma star_mult_idem[simp]: "star x * star x = star x"
   5.174 -by (metis add_commute add_est1 eq_iff mult_1_right right_distrib star3 star_unfold_left)
   5.175 -
   5.176 -lemma less_star: "x \<le> star x"
   5.177 -by (metis less_add(2) mult_1_right mult_left_mono one_less_star order_trans star_unfold_left zero_minimum)
   5.178 -
   5.179 -lemma star_simulation:
   5.180 -  assumes a: "a * x = x * b"
   5.181 -  shows "star a * x = x * star b"
   5.182 -proof (rule antisym)
   5.183 -  show "star a * x \<le> x * star b"
   5.184 -  proof (rule star3', rule order_trans)
   5.185 -    from a have "a * x \<le> x * b" by simp
   5.186 -    hence "a * x * star b \<le> x * b * star b"
   5.187 -      by (rule mult_mono) auto
   5.188 -    thus "x + a * (x * star b) \<le> x + x * b * star b"
   5.189 -      using add_mono by (auto simp: mult_assoc)
   5.190 -    show "\<dots> \<le> x * star b"
   5.191 -    proof -
   5.192 -      have "x * (1 + b * star b) \<le> x * star b"
   5.193 -        by (rule mult_mono[OF _ star1]) auto
   5.194 -      thus ?thesis
   5.195 -        by (simp add:right_distrib mult_assoc)
   5.196 -    qed
   5.197 -  qed
   5.198 -  show "x * star b \<le> star a * x"
   5.199 -  proof (rule star4', rule order_trans)
   5.200 -    from a have b: "x * b \<le> a * x" by simp
   5.201 -    have "star a * x * b \<le> star a * a * x"
   5.202 -      unfolding mult_assoc
   5.203 -      by (rule mult_mono[OF _ b]) auto
   5.204 -    thus "x + star a * x * b \<le> x + star a * a * x"
   5.205 -      using add_mono by auto
   5.206 -    show "\<dots> \<le> star a * x"
   5.207 -    proof -
   5.208 -      have "(1 + star a * a) * x \<le> star a * x"
   5.209 -        by (rule mult_mono[OF star2]) auto
   5.210 -      thus ?thesis
   5.211 -        by (simp add:left_distrib mult_assoc)
   5.212 -    qed
   5.213 -  qed
   5.214 -qed
   5.215 -
   5.216 -lemma star_slide2[simp]: "star x * x = x * star x"
   5.217 -by (metis star_simulation)
   5.218 -
   5.219 -lemma star_idemp[simp]: "star (star x) = star x"
   5.220 -by (metis add_idem2 eq_iff less_star mult_1_right star3' star_mult_idem star_unfold_left)
   5.221 -
   5.222 -lemma star_slide[simp]: "star (x * y) * x = x * star (y * x)"
   5.223 -by (auto simp: mult_assoc star_simulation)
   5.224 -
   5.225 -lemma star_one':
   5.226 -  assumes "p * p' = 1" "p' * p = 1"
   5.227 -  shows "p' * star a * p = star (p' * a * p)"
   5.228 -proof -
   5.229 -  from assms
   5.230 -  have "p' * star a * p = p' * star (p * p' * a) * p"
   5.231 -    by simp
   5.232 -  also have "\<dots> = p' * p * star (p' * a * p)"
   5.233 -    by (simp add: mult_assoc)
   5.234 -  also have "\<dots> = star (p' * a * p)"
   5.235 -    by (simp add: assms)
   5.236 -  finally show ?thesis .
   5.237 -qed
   5.238 -
   5.239 -lemma x_less_star[simp]: "x \<le> x * star a"
   5.240 -proof -
   5.241 -  have "x \<le> x * (1 + a * star a)" by (simp add: right_distrib)
   5.242 -  also have "\<dots> = x * star a" by (simp only: star_unfold_left)
   5.243 -  finally show ?thesis .
   5.244 -qed
   5.245 -
   5.246 -lemma star_mono:  "x \<le> y \<Longrightarrow>  star x \<le> star y"
   5.247 -by (metis add_commute eq_iff less_star ord_simp2 order_trans star3 star4' star_idemp star_mult_idem x_less_star)
   5.248 -
   5.249 -lemma star_sub: "x \<le> 1 \<Longrightarrow> star x = 1"
   5.250 -by (metis add_commute ord_simp1 star_idemp star_mono star_mult_idem star_one star_unfold_left)
   5.251 -
   5.252 -lemma star_unfold2: "star x * y = y + x * star x * y"
   5.253 -by (subst star_unfold_right[symmetric]) (simp add: mult_assoc left_distrib)
   5.254 -
   5.255 -lemma star_absorb_one[simp]: "star (x + 1) = star x"
   5.256 -by (metis add_commute eq_iff left_distrib less_add(1) less_add(2) mult_1_left mult_assoc star3 star_mono star_mult_idem star_unfold2 x_less_star)
   5.257 -
   5.258 -lemma star_absorb_one'[simp]: "star (1 + x) = star x"
   5.259 -by (subst add_commute) (fact star_absorb_one)
   5.260 -
   5.261 -lemma ka16: "(y * star x) * star (y * star x) \<le> star x * star (y * star x)"
   5.262 -by (metis ka1 less_add(1) mult_assoc order_trans star_unfold2)
   5.263 -
   5.264 -lemma ka16': "(star x * y) * star (star x * y) \<le> star (star x * y) * star x"
   5.265 -by (metis ka1 mult_assoc order_trans star_slide x_less_star)
   5.266 -
   5.267 -lemma ka17: "(x * star x) * star (y * star x) \<le> star x * star (y * star x)"
   5.268 -by (metis ka1 mult_assoc mult_right_mono zero_minimum)
   5.269 -
   5.270 -lemma ka18: "(x * star x) * star (y * star x) + (y * star x) * star (y * star x)
   5.271 -  \<le> star x * star (y * star x)"
   5.272 -by (metis ka16 ka17 left_distrib mult_assoc plus_leI)
   5.273 -
   5.274 -lemma kleene_church_rosser: 
   5.275 -  "star y * star x \<le> star x * star y \<Longrightarrow> star (x + y) \<le> star x * star y"
   5.276 -oops
   5.277 -
   5.278 -lemma star_decomp: "star (a + b) = star a * star (b * star a)"
   5.279 -oops
   5.280 -
   5.281 -lemma ka22: "y * star x \<le> star x * star y \<Longrightarrow>  star y * star x \<le> star x * star y"
   5.282 -by (metis mult_assoc mult_right_mono plus_leI star3' star_mult_idem x_less_star zero_minimum)
   5.283 -
   5.284 -lemma ka23: "star y * star x \<le> star x * star y \<Longrightarrow> y * star x \<le> star x * star y"
   5.285 -by (metis less_star mult_right_mono order_trans zero_minimum)
   5.286 -
   5.287 -lemma ka24: "star (x + y) \<le> star (star x * star y)"
   5.288 -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)
   5.289 -
   5.290 -lemma ka25: "star y * star x \<le> star x * star y \<Longrightarrow> star (star y * star x) \<le> star x * star y"
   5.291 -oops
   5.292 -
   5.293 -lemma kleene_bubblesort: "y * x \<le> x * y \<Longrightarrow> star (x + y) \<le> star x * star y"
   5.294 -oops
   5.295 -
   5.296 -end
   5.297 -
   5.298 -subsection {* Complete lattices are Kleene algebras *}
   5.299 -
   5.300 -lemma (in complete_lattice) le_SUPI':
   5.301 -  assumes "l \<le> M i"
   5.302 -  shows "l \<le> (SUP i. M i)"
   5.303 -  using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
   5.304 -
   5.305 -class kleene_by_complete_lattice = pre_kleene
   5.306 -  + complete_lattice + power + star +
   5.307 -  assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
   5.308 -begin
   5.309 -
   5.310 -subclass kleene
   5.311 -proof
   5.312 -  fix a x :: 'a
   5.313 -  
   5.314 -  have [simp]: "1 \<le> star a"
   5.315 -    unfolding star_cont[of 1 a 1, simplified] 
   5.316 -    by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
   5.317 -  
   5.318 -  show "1 + a * star a \<le> star a" 
   5.319 -    apply (rule plus_leI, simp)
   5.320 -    apply (simp add:star_cont[of a a 1, simplified])
   5.321 -    apply (simp add:star_cont[of 1 a 1, simplified])
   5.322 -    apply (subst power_Suc[symmetric])
   5.323 -    by (intro SUP_leI le_SUPI UNIV_I)
   5.324 -
   5.325 -  show "1 + star a * a \<le> star a" 
   5.326 -    apply (rule plus_leI, simp)
   5.327 -    apply (simp add:star_cont[of 1 a a, simplified])
   5.328 -    apply (simp add:star_cont[of 1 a 1, simplified])
   5.329 -    by (auto intro: SUP_leI le_SUPI simp add: power_Suc[symmetric] power_commutes simp del: power_Suc)
   5.330 -
   5.331 -  show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
   5.332 -  proof -
   5.333 -    assume a: "a * x \<le> x"
   5.334 -
   5.335 -    {
   5.336 -      fix n
   5.337 -      have "a ^ (Suc n) * x \<le> a ^ n * x"
   5.338 -      proof (induct n)
   5.339 -        case 0 thus ?case by (simp add: a)
   5.340 -      next
   5.341 -        case (Suc n)
   5.342 -        hence "a * (a ^ Suc n * x) \<le> a * (a ^ n * x)"
   5.343 -          by (auto intro: mult_mono)
   5.344 -        thus ?case
   5.345 -          by (simp add: mult_assoc)
   5.346 -      qed
   5.347 -    }
   5.348 -    note a = this
   5.349 -    
   5.350 -    {
   5.351 -      fix n have "a ^ n * x \<le> x"
   5.352 -      proof (induct n)
   5.353 -        case 0 show ?case by simp
   5.354 -      next
   5.355 -        case (Suc n) with a[of n]
   5.356 -        show ?case by simp
   5.357 -      qed
   5.358 -    }
   5.359 -    note b = this
   5.360 -    
   5.361 -    show "star a * x \<le> x"
   5.362 -      unfolding star_cont[of 1 a x, simplified]
   5.363 -      by (rule SUP_leI) (rule b)
   5.364 -  qed
   5.365 -
   5.366 -  show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *)
   5.367 -  proof -
   5.368 -    assume a: "x * a \<le> x"
   5.369 -
   5.370 -    {
   5.371 -      fix n
   5.372 -      have "x * a ^ (Suc n) \<le> x * a ^ n"
   5.373 -      proof (induct n)
   5.374 -        case 0 thus ?case by (simp add: a)
   5.375 -      next
   5.376 -        case (Suc n)
   5.377 -        hence "(x * a ^ Suc n) * a  \<le> (x * a ^ n) * a"
   5.378 -          by (auto intro: mult_mono)
   5.379 -        thus ?case
   5.380 -          by (simp add: power_commutes mult_assoc)
   5.381 -      qed
   5.382 -    }
   5.383 -    note a = this
   5.384 -    
   5.385 -    {
   5.386 -      fix n have "x * a ^ n \<le> x"
   5.387 -      proof (induct n)
   5.388 -        case 0 show ?case by simp
   5.389 -      next
   5.390 -        case (Suc n) with a[of n]
   5.391 -        show ?case by simp
   5.392 -      qed
   5.393 -    }
   5.394 -    note b = this
   5.395 -    
   5.396 -    show "x * star a \<le> x"
   5.397 -      unfolding star_cont[of x a 1, simplified]
   5.398 -      by (rule SUP_leI) (rule b)
   5.399 -  qed
   5.400 -qed
   5.401 -
   5.402 -end
   5.403 -
   5.404 -
   5.405 -subsection {* Transitive Closure *}
   5.406 -
   5.407 -context kleene
   5.408 -begin
   5.409 -
   5.410 -definition 
   5.411 -  tcl_def:  "tcl x = star x * x"
   5.412 -
   5.413 -lemma tcl_zero: "tcl 0 = 0"
   5.414 -unfolding tcl_def by simp
   5.415 -
   5.416 -lemma tcl_unfold_right: "tcl a = a + tcl a * a"
   5.417 -proof -
   5.418 -  from star_unfold_right[of a]
   5.419 -  have "a * (1 + star a * a) = a * star a" by simp
   5.420 -  from this[simplified right_distrib, simplified]
   5.421 -  show ?thesis
   5.422 -    by (simp add:tcl_def mult_assoc)
   5.423 -qed
   5.424 -
   5.425 -lemma less_tcl: "a \<le> tcl a"
   5.426 -proof -
   5.427 -  have "a \<le> a + tcl a * a" by simp
   5.428 -  also have "\<dots> = tcl a" by (rule tcl_unfold_right[symmetric])
   5.429 -  finally show ?thesis .
   5.430 -qed
   5.431 -
   5.432 -end
   5.433 -
   5.434 -
   5.435 -subsection {* Naive Algorithm to generate the transitive closure *}
   5.436 -
   5.437 -function (default "\<lambda>x. 0", tailrec, domintros)
   5.438 -  mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"
   5.439 -where
   5.440 -  "mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))"
   5.441 -  by pat_completeness simp
   5.442 -
   5.443 -declare mk_tcl.simps[simp del] (* loops *)
   5.444 -
   5.445 -lemma mk_tcl_code[code]:
   5.446 -  "mk_tcl A X = 
   5.447 -  (let XA = X * A 
   5.448 -  in if XA \<le> X then X else mk_tcl A (X + XA))"
   5.449 -  unfolding mk_tcl.simps[of A X] Let_def ..
   5.450 -
   5.451 -context kleene
   5.452 -begin
   5.453 -
   5.454 -lemma mk_tcl_lemma1:
   5.455 -  "(X + X * A) * star A = X * star A"
   5.456 -proof -
   5.457 -  have "A * star A \<le> 1 + A * star A" by simp
   5.458 -  also have "\<dots> = star A" by (simp add:star_unfold_left)
   5.459 -  finally have "star A + A * star A = star A" by simp
   5.460 -  hence "X * (star A + A * star A) = X * star A" by simp
   5.461 -  thus ?thesis by (simp add:left_distrib right_distrib mult_assoc)
   5.462 -qed
   5.463 -
   5.464 -lemma mk_tcl_lemma2:
   5.465 -  shows "X * A \<le> X \<Longrightarrow> X * star A = X"
   5.466 -  by (rule antisym) (auto simp:star4)
   5.467 -
   5.468 -end
   5.469 -
   5.470 -lemma mk_tcl_correctness:
   5.471 -  fixes X :: "'a::kleene"
   5.472 -  assumes "mk_tcl_dom (A, X)"
   5.473 -  shows "mk_tcl A X = X * star A"
   5.474 -  using assms
   5.475 -  by induct (auto simp: mk_tcl_lemma1 mk_tcl_lemma2)
   5.476 -
   5.477 -
   5.478 -lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
   5.479 -  by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases)
   5.480 -
   5.481 -lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
   5.482 -  unfolding mk_tcl_def
   5.483 -  by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom])
   5.484 -
   5.485 -
   5.486 -text {* We can replace the dom-Condition of the correctness theorem 
   5.487 -  with something executable *}
   5.488 -
   5.489 -lemma mk_tcl_correctness2:
   5.490 -  fixes A X :: "'a :: {kleene}"
   5.491 -  assumes "mk_tcl A A \<noteq> 0"
   5.492 -  shows "mk_tcl A A = tcl A"
   5.493 -  using assms mk_tcl_default mk_tcl_correctness
   5.494 -  unfolding tcl_def 
   5.495 -  by auto
   5.496 -
   5.497 -end