src/HOL/Library/Kleene_Algebras.thy
 author chaieb Mon Jun 11 11:06:04 2007 +0200 (2007-06-11) changeset 23315 df3a7e9ebadb parent 22665 cf152ff55d16 child 23394 474ff28210c0 permissions -rw-r--r--
tuned Proof
 krauss@22371 ` 1` ```(* Title: HOL/Library/Kleene_Algebras.thy ``` krauss@22371 ` 2` ``` ID: \$Id\$ ``` krauss@22371 ` 3` ``` Author: Alexander Krauss, TU Muenchen ``` krauss@22371 ` 4` ```*) ``` krauss@22371 ` 5` wenzelm@22665 ` 6` ```header "" ``` wenzelm@22665 ` 7` krauss@22359 ` 8` ```theory Kleene_Algebras ``` krauss@22359 ` 9` ```imports Main ``` krauss@22359 ` 10` ```begin ``` krauss@22359 ` 11` krauss@22359 ` 12` ```text {* A type class of kleene algebras *} ``` krauss@22359 ` 13` haftmann@22473 ` 14` ```class star = type + ``` krauss@22359 ` 15` ``` fixes star :: "'a \ 'a" ``` krauss@22359 ` 16` haftmann@22459 ` 17` ```class idem_add = ab_semigroup_add + ``` haftmann@22459 ` 18` ``` assumes add_idem [simp]: "x \<^loc>+ x = x" ``` krauss@22359 ` 19` krauss@22359 ` 20` ```lemma add_idem2[simp]: "(x::'a::idem_add) + (x + y) = x + y" ``` krauss@22359 ` 21` ``` unfolding add_assoc[symmetric] ``` krauss@22359 ` 22` ``` by simp ``` krauss@22359 ` 23` haftmann@22459 ` 24` ```class order_by_add = idem_add + ord + ``` haftmann@22459 ` 25` ``` assumes order_def: "a \ b \ a \<^loc>+ b = b" ``` haftmann@22459 ` 26` ``` assumes strict_order_def: "a \ b \ a \ b \ a \ b" ``` krauss@22359 ` 27` krauss@22359 ` 28` ```lemma ord_simp1[simp]: "(x::'a::order_by_add) \ y \ x + y = y" ``` krauss@22359 ` 29` ``` unfolding order_def . ``` krauss@22359 ` 30` ```lemma ord_simp2[simp]: "(x::'a::order_by_add) \ y \ y + x = y" ``` krauss@22359 ` 31` ``` unfolding order_def add_commute . ``` krauss@22359 ` 32` ```lemma ord_intro: "(x::'a::order_by_add) + y = y \ x \ y" ``` krauss@22359 ` 33` ``` unfolding order_def . ``` krauss@22359 ` 34` krauss@22359 ` 35` ```instance order_by_add \ order ``` krauss@22359 ` 36` ```proof ``` krauss@22359 ` 37` ``` fix x y z :: 'a ``` krauss@22359 ` 38` ``` show "x \ x" unfolding order_def by simp ``` krauss@22359 ` 39` krauss@22359 ` 40` ``` show "\x \ y; y \ z\ \ x \ z" ``` krauss@22359 ` 41` ``` proof (rule ord_intro) ``` krauss@22359 ` 42` ``` assume "x \ y" "y \ z" ``` krauss@22359 ` 43` krauss@22359 ` 44` ``` have "x + z = x + y + z" by (simp add:`y \ z` add_assoc) ``` krauss@22359 ` 45` ``` also have "\ = y + z" by (simp add:`x \ y`) ``` krauss@22359 ` 46` ``` also have "\ = z" by (simp add:`y \ z`) ``` krauss@22359 ` 47` ``` finally show "x + z = z" . ``` krauss@22359 ` 48` ``` qed ``` krauss@22359 ` 49` krauss@22359 ` 50` ``` show "\x \ y; y \ x\ \ x = y" unfolding order_def ``` krauss@22359 ` 51` ``` by (simp add:add_commute) ``` krauss@22359 ` 52` ``` show "x < y \ x \ y \ x \ y" by (fact strict_order_def) ``` krauss@22359 ` 53` ```qed ``` krauss@22359 ` 54` krauss@22359 ` 55` haftmann@22459 ` 56` ```class pre_kleene = semiring_1 + order_by_add ``` krauss@22359 ` 57` krauss@22359 ` 58` ```instance pre_kleene \ pordered_semiring ``` krauss@22359 ` 59` ```proof ``` krauss@22359 ` 60` ``` fix x y z :: 'a ``` krauss@22359 ` 61` krauss@22359 ` 62` ``` assume "x \ y" ``` krauss@22359 ` 63` ``` ``` krauss@22359 ` 64` ``` show "z + x \ z + y" ``` krauss@22359 ` 65` ``` proof (rule ord_intro) ``` krauss@22359 ` 66` ``` have "z + x + (z + y) = x + y + z" by (simp add:add_ac) ``` krauss@22359 ` 67` ``` also have "\ = z + y" by (simp add:`x \ y` add_ac) ``` krauss@22359 ` 68` ``` finally show "z + x + (z + y) = z + y" . ``` krauss@22359 ` 69` ``` qed ``` krauss@22359 ` 70` krauss@22359 ` 71` ``` show "z * x \ z * y" ``` krauss@22359 ` 72` ``` proof (rule ord_intro) ``` krauss@22359 ` 73` ``` from `x \ y` have "z * (x + y) = z * y" by simp ``` krauss@22359 ` 74` ``` thus "z * x + z * y = z * y" by (simp add:right_distrib) ``` krauss@22359 ` 75` ``` qed ``` krauss@22359 ` 76` krauss@22359 ` 77` ``` show "x * z \ y * z" ``` krauss@22359 ` 78` ``` proof (rule ord_intro) ``` krauss@22359 ` 79` ``` from `x \ y` have "(x + y) * z = y * z" by simp ``` krauss@22359 ` 80` ``` thus "x * z + y * z = y * z" by (simp add:left_distrib) ``` krauss@22359 ` 81` ``` qed ``` krauss@22359 ` 82` ```qed ``` krauss@22359 ` 83` haftmann@22459 ` 84` ```class kleene = pre_kleene + star + ``` haftmann@22459 ` 85` ``` assumes star1: "\<^loc>1 \<^loc>+ a \<^loc>* star a \ star a" ``` haftmann@22459 ` 86` ``` and star2: "\<^loc>1 \<^loc>+ star a \<^loc>* a \ star a" ``` haftmann@22459 ` 87` ``` and star3: "a \<^loc>* x \ x \ star a \<^loc>* x \ x" ``` haftmann@22459 ` 88` ``` and star4: "x \<^loc>* a \ x \ x \<^loc>* star a \ x" ``` krauss@22359 ` 89` haftmann@22459 ` 90` ```class kleene_by_complete_lattice = ``` haftmann@22459 ` 91` ``` pre_kleene + complete_lattice + recpower + star + ``` haftmann@22459 ` 92` ``` assumes star_cont: "a \<^loc>* star b \<^loc>* c = (SUP n. a \<^loc>* b ^ n \<^loc>* c)" ``` krauss@22359 ` 93` krauss@22359 ` 94` ```lemma plus_leI: ``` krauss@22359 ` 95` ``` fixes x :: "'a :: order_by_add" ``` krauss@22359 ` 96` ``` shows "x \ z \ y \ z \ x + y \ z" ``` krauss@22359 ` 97` ``` unfolding order_def by (simp add:add_assoc) ``` krauss@22359 ` 98` krauss@22359 ` 99` ```lemma le_SUPI': ``` haftmann@22459 ` 100` ``` fixes l :: "'a :: complete_lattice" ``` krauss@22359 ` 101` ``` assumes "l \ M i" ``` krauss@22359 ` 102` ``` shows "l \ (SUP i. M i)" ``` krauss@22359 ` 103` ``` using prems ``` berghofe@22431 ` 104` ``` by (rule order_trans) (rule le_SUPI [OF UNIV_I]) ``` krauss@22359 ` 105` krauss@22359 ` 106` ```lemma zero_minimum[simp]: "(0::'a::pre_kleene) \ x" ``` krauss@22359 ` 107` ``` unfolding order_def by simp ``` krauss@22359 ` 108` haftmann@22459 ` 109` ```instance kleene_by_complete_lattice \ kleene ``` krauss@22359 ` 110` ```proof ``` krauss@22359 ` 111` krauss@22359 ` 112` ``` fix a x :: 'a ``` krauss@22359 ` 113` ``` ``` krauss@22359 ` 114` ``` have [simp]: "1 \ star a" ``` krauss@22359 ` 115` ``` unfolding star_cont[of 1 a 1, simplified] ``` berghofe@22431 ` 116` ``` by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I]) ``` krauss@22359 ` 117` ``` ``` krauss@22359 ` 118` ``` show "1 + a * star a \ star a" ``` krauss@22359 ` 119` ``` apply (rule plus_leI, simp) ``` krauss@22359 ` 120` ``` apply (simp add:star_cont[of a a 1, simplified]) ``` krauss@22359 ` 121` ``` apply (simp add:star_cont[of 1 a 1, simplified]) ``` berghofe@22431 ` 122` ``` apply (subst power_Suc[symmetric]) ``` berghofe@22431 ` 123` ``` by (intro SUP_leI le_SUPI UNIV_I) ``` krauss@22359 ` 124` krauss@22359 ` 125` ``` show "1 + star a * a \ star a" ``` krauss@22359 ` 126` ``` apply (rule plus_leI, simp) ``` krauss@22359 ` 127` ``` apply (simp add:star_cont[of 1 a a, simplified]) ``` krauss@22359 ` 128` ``` apply (simp add:star_cont[of 1 a 1, simplified]) ``` berghofe@22431 ` 129` ``` by (auto intro: SUP_leI le_SUPI UNIV_I simp add: power_Suc[symmetric] power_commutes) ``` krauss@22359 ` 130` krauss@22359 ` 131` ``` show "a * x \ x \ star a * x \ x" ``` krauss@22359 ` 132` ``` proof - ``` krauss@22359 ` 133` ``` assume a: "a * x \ x" ``` krauss@22359 ` 134` krauss@22359 ` 135` ``` { ``` krauss@22359 ` 136` ``` fix n ``` krauss@22359 ` 137` ``` have "a ^ (Suc n) * x \ a ^ n * x" ``` krauss@22359 ` 138` ``` proof (induct n) ``` krauss@22359 ` 139` ``` case 0 thus ?case by (simp add:a power_Suc) ``` krauss@22359 ` 140` ``` next ``` krauss@22359 ` 141` ``` case (Suc n) ``` krauss@22359 ` 142` ``` hence "a * (a ^ Suc n * x) \ a * (a ^ n * x)" ``` krauss@22359 ` 143` ``` by (auto intro: mult_mono) ``` krauss@22359 ` 144` ``` thus ?case ``` krauss@22359 ` 145` ``` by (simp add:power_Suc mult_assoc) ``` krauss@22359 ` 146` ``` qed ``` krauss@22359 ` 147` ``` } ``` krauss@22359 ` 148` ``` note a = this ``` krauss@22359 ` 149` ``` ``` krauss@22359 ` 150` ``` { ``` krauss@22359 ` 151` ``` fix n have "a ^ n * x \ x" ``` krauss@22359 ` 152` ``` proof (induct n) ``` krauss@22359 ` 153` ``` case 0 show ?case by simp ``` krauss@22359 ` 154` ``` next ``` krauss@22359 ` 155` ``` case (Suc n) with a[of n] ``` krauss@22359 ` 156` ``` show ?case by simp ``` krauss@22359 ` 157` ``` qed ``` krauss@22359 ` 158` ``` } ``` krauss@22359 ` 159` ``` note b = this ``` krauss@22359 ` 160` ``` ``` krauss@22359 ` 161` ``` show "star a * x \ x" ``` krauss@22359 ` 162` ``` unfolding star_cont[of 1 a x, simplified] ``` krauss@22359 ` 163` ``` by (rule SUP_leI) (rule b) ``` krauss@22359 ` 164` ``` qed ``` krauss@22359 ` 165` krauss@22359 ` 166` ``` show "x * a \ x \ x * star a \ x" (* symmetric *) ``` krauss@22359 ` 167` ``` proof - ``` krauss@22359 ` 168` ``` assume a: "x * a \ x" ``` krauss@22359 ` 169` krauss@22359 ` 170` ``` { ``` krauss@22359 ` 171` ``` fix n ``` krauss@22359 ` 172` ``` have "x * a ^ (Suc n) \ x * a ^ n" ``` krauss@22359 ` 173` ``` proof (induct n) ``` krauss@22359 ` 174` ``` case 0 thus ?case by (simp add:a power_Suc) ``` krauss@22359 ` 175` ``` next ``` krauss@22359 ` 176` ``` case (Suc n) ``` krauss@22359 ` 177` ``` hence "(x * a ^ Suc n) * a \ (x * a ^ n) * a" ``` krauss@22359 ` 178` ``` by (auto intro: mult_mono) ``` krauss@22359 ` 179` ``` thus ?case ``` krauss@22359 ` 180` ``` by (simp add:power_Suc power_commutes mult_assoc) ``` krauss@22359 ` 181` ``` qed ``` krauss@22359 ` 182` ``` } ``` krauss@22359 ` 183` ``` note a = this ``` krauss@22359 ` 184` ``` ``` krauss@22359 ` 185` ``` { ``` krauss@22359 ` 186` ``` fix n have "x * a ^ n \ x" ``` krauss@22359 ` 187` ``` proof (induct n) ``` krauss@22359 ` 188` ``` case 0 show ?case by simp ``` krauss@22359 ` 189` ``` next ``` krauss@22359 ` 190` ``` case (Suc n) with a[of n] ``` krauss@22359 ` 191` ``` show ?case by simp ``` krauss@22359 ` 192` ``` qed ``` krauss@22359 ` 193` ``` } ``` krauss@22359 ` 194` ``` note b = this ``` krauss@22359 ` 195` ``` ``` krauss@22359 ` 196` ``` show "x * star a \ x" ``` krauss@22359 ` 197` ``` unfolding star_cont[of x a 1, simplified] ``` krauss@22359 ` 198` ``` by (rule SUP_leI) (rule b) ``` krauss@22359 ` 199` ``` qed ``` krauss@22359 ` 200` ```qed ``` krauss@22359 ` 201` krauss@22359 ` 202` ```lemma less_add[simp]: ``` krauss@22359 ` 203` ``` fixes a b :: "'a :: order_by_add" ``` krauss@22359 ` 204` ``` shows "a \ a + b" ``` krauss@22359 ` 205` ``` and "b \ a + b" ``` krauss@22359 ` 206` ``` unfolding order_def ``` krauss@22359 ` 207` ``` by (auto simp:add_ac) ``` krauss@22359 ` 208` krauss@22359 ` 209` ```lemma add_est1: ``` krauss@22359 ` 210` ``` fixes a b c :: "'a :: order_by_add" ``` krauss@22359 ` 211` ``` assumes a: "a + b \ c" ``` krauss@22359 ` 212` ``` shows "a \ c" ``` krauss@22359 ` 213` ``` using less_add(1) a ``` krauss@22359 ` 214` ``` by (rule order_trans) ``` krauss@22359 ` 215` krauss@22359 ` 216` ```lemma add_est2: ``` krauss@22359 ` 217` ``` fixes a b c :: "'a :: order_by_add" ``` krauss@22359 ` 218` ``` assumes a: "a + b \ c" ``` krauss@22359 ` 219` ``` shows "b \ c" ``` krauss@22359 ` 220` ``` using less_add(2) a ``` krauss@22359 ` 221` ``` by (rule order_trans) ``` krauss@22359 ` 222` krauss@22359 ` 223` krauss@22359 ` 224` ```lemma star3': ``` krauss@22359 ` 225` ``` fixes a b x :: "'a :: kleene" ``` krauss@22359 ` 226` ``` assumes a: "b + a * x \ x" ``` krauss@22359 ` 227` ``` shows "star a * b \ x" ``` krauss@22359 ` 228` ```proof (rule order_trans) ``` krauss@22359 ` 229` ``` from a have "b \ x" by (rule add_est1) ``` krauss@22359 ` 230` ``` show "star a * b \ star a * x" ``` krauss@22359 ` 231` ``` by (rule mult_mono) (auto simp:`b \ x`) ``` krauss@22359 ` 232` krauss@22359 ` 233` ``` from a have "a * x \ x" by (rule add_est2) ``` krauss@22359 ` 234` ``` with star3 show "star a * x \ x" . ``` krauss@22359 ` 235` ```qed ``` krauss@22359 ` 236` krauss@22359 ` 237` krauss@22359 ` 238` ```lemma star4': ``` krauss@22359 ` 239` ``` fixes a b x :: "'a :: kleene" ``` krauss@22359 ` 240` ``` assumes a: "b + x * a \ x" ``` krauss@22359 ` 241` ``` shows "b * star a \ x" ``` krauss@22359 ` 242` ```proof (rule order_trans) ``` krauss@22359 ` 243` ``` from a have "b \ x" by (rule add_est1) ``` krauss@22359 ` 244` ``` show "b * star a \ x * star a" ``` krauss@22359 ` 245` ``` by (rule mult_mono) (auto simp:`b \ x`) ``` krauss@22359 ` 246` krauss@22359 ` 247` ``` from a have "x * a \ x" by (rule add_est2) ``` krauss@22359 ` 248` ``` with star4 show "x * star a \ x" . ``` krauss@22359 ` 249` ```qed ``` krauss@22359 ` 250` krauss@22359 ` 251` krauss@22359 ` 252` ```lemma star_mono: ``` krauss@22359 ` 253` ``` fixes x y :: "'a :: kleene" ``` krauss@22359 ` 254` ``` assumes "x \ y" ``` krauss@22359 ` 255` ``` shows "star x \ star y" ``` krauss@22359 ` 256` ``` oops ``` krauss@22359 ` 257` krauss@22359 ` 258` ```lemma star_idemp: ``` krauss@22359 ` 259` ``` fixes x :: "'a :: kleene" ``` krauss@22359 ` 260` ``` shows "star (star x) = star x" ``` krauss@22359 ` 261` ``` oops ``` krauss@22359 ` 262` krauss@22359 ` 263` ```lemma zero_star[simp]: ``` krauss@22359 ` 264` ``` shows "star (0::'a::kleene) = 1" ``` krauss@22359 ` 265` ``` oops ``` krauss@22359 ` 266` krauss@22359 ` 267` krauss@22359 ` 268` ```lemma star_unfold_left: ``` krauss@22359 ` 269` ``` fixes a :: "'a :: kleene" ``` krauss@22359 ` 270` ``` shows "1 + a * star a = star a" ``` krauss@22359 ` 271` ```proof (rule order_antisym, rule star1) ``` krauss@22359 ` 272` krauss@22359 ` 273` ``` have "1 + a * (1 + a * star a) \ 1 + a * star a" ``` krauss@22359 ` 274` ``` apply (rule add_mono, rule) ``` krauss@22359 ` 275` ``` apply (rule mult_mono, auto) ``` krauss@22359 ` 276` ``` apply (rule star1) ``` krauss@22359 ` 277` ``` done ``` krauss@22359 ` 278` krauss@22359 ` 279` ``` with star3' have "star a * 1 \ 1 + a * star a" . ``` krauss@22359 ` 280` ``` thus "star a \ 1 + a * star a" by simp ``` krauss@22359 ` 281` ```qed ``` krauss@22359 ` 282` krauss@22359 ` 283` krauss@22359 ` 284` ```lemma star_unfold_right: ``` krauss@22359 ` 285` ``` fixes a :: "'a :: kleene" ``` krauss@22359 ` 286` ``` shows "1 + star a * a = star a" ``` krauss@22359 ` 287` ```proof (rule order_antisym, rule star2) ``` krauss@22359 ` 288` krauss@22359 ` 289` ``` have "1 + (1 + star a * a) * a \ 1 + star a * a" ``` krauss@22359 ` 290` ``` apply (rule add_mono, rule) ``` krauss@22359 ` 291` ``` apply (rule mult_mono, auto) ``` krauss@22359 ` 292` ``` apply (rule star2) ``` krauss@22359 ` 293` ``` done ``` krauss@22359 ` 294` krauss@22359 ` 295` ``` with star4' have "1 * star a \ 1 + star a * a" . ``` krauss@22359 ` 296` ``` thus "star a \ 1 + star a * a" by simp ``` krauss@22359 ` 297` ```qed ``` krauss@22359 ` 298` krauss@22359 ` 299` krauss@22359 ` 300` krauss@22359 ` 301` ```lemma star_commute: ``` krauss@22359 ` 302` ``` fixes a b x :: "'a :: kleene" ``` krauss@22359 ` 303` ``` assumes a: "a * x = x * b" ``` krauss@22359 ` 304` ``` shows "star a * x = x * star b" ``` krauss@22359 ` 305` ```proof (rule order_antisym) ``` krauss@22359 ` 306` krauss@22359 ` 307` ``` show "star a * x \ x * star b" ``` krauss@22359 ` 308` ``` proof (rule star3', rule order_trans) ``` krauss@22359 ` 309` krauss@22359 ` 310` ``` from a have "a * x \ x * b" by simp ``` krauss@22359 ` 311` ``` hence "a * x * star b \ x * b * star b" ``` krauss@22359 ` 312` ``` by (rule mult_mono) auto ``` krauss@22359 ` 313` ``` thus "x + a * (x * star b) \ x + x * b * star b" ``` krauss@22359 ` 314` ``` using add_mono by (auto simp: mult_assoc) ``` krauss@22359 ` 315` krauss@22359 ` 316` ``` show "\ \ x * star b" ``` krauss@22359 ` 317` ``` proof - ``` krauss@22359 ` 318` ``` have "x * (1 + b * star b) \ x * star b" ``` krauss@22359 ` 319` ``` by (rule mult_mono[OF _ star1]) auto ``` krauss@22359 ` 320` ``` thus ?thesis ``` krauss@22359 ` 321` ``` by (simp add:right_distrib mult_assoc) ``` krauss@22359 ` 322` ``` qed ``` krauss@22359 ` 323` ``` qed ``` krauss@22359 ` 324` krauss@22359 ` 325` ``` show "x * star b \ star a * x" ``` krauss@22359 ` 326` ``` proof (rule star4', rule order_trans) ``` krauss@22359 ` 327` krauss@22359 ` 328` ``` from a have b: "x * b \ a * x" by simp ``` krauss@22359 ` 329` ``` have "star a * x * b \ star a * a * x" ``` krauss@22359 ` 330` ``` unfolding mult_assoc ``` krauss@22359 ` 331` ``` by (rule mult_mono[OF _ b]) auto ``` krauss@22359 ` 332` ``` thus "x + star a * x * b \ x + star a * a * x" ``` krauss@22359 ` 333` ``` using add_mono by auto ``` krauss@22359 ` 334` krauss@22359 ` 335` ``` show "\ \ star a * x" ``` krauss@22359 ` 336` ``` proof - ``` krauss@22359 ` 337` ``` have "(1 + star a * a) * x \ star a * x" ``` krauss@22359 ` 338` ``` by (rule mult_mono[OF star2]) auto ``` krauss@22359 ` 339` ``` thus ?thesis ``` krauss@22359 ` 340` ``` by (simp add:left_distrib mult_assoc) ``` krauss@22359 ` 341` ``` qed ``` krauss@22359 ` 342` ``` qed ``` krauss@22359 ` 343` ```qed ``` krauss@22359 ` 344` krauss@22359 ` 345` krauss@22359 ` 346` krauss@22359 ` 347` ```lemma star_assoc: ``` krauss@22359 ` 348` ``` fixes c d :: "'a :: kleene" ``` krauss@22359 ` 349` ``` shows "star (c * d) * c = c * star (d * c)" ``` krauss@22359 ` 350` ``` oops ``` krauss@22359 ` 351` krauss@22359 ` 352` ```lemma star_dist: ``` krauss@22359 ` 353` ``` fixes a b :: "'a :: kleene" ``` krauss@22359 ` 354` ``` shows "star (a + b) = star a * star (b * star a)" ``` krauss@22359 ` 355` ``` oops ``` krauss@22359 ` 356` krauss@22359 ` 357` ```lemma star_one: ``` krauss@22359 ` 358` ``` fixes a p p' :: "'a :: kleene" ``` krauss@22359 ` 359` ``` assumes "p * p' = 1" and "p' * p = 1" ``` krauss@22359 ` 360` ``` shows "p' * star a * p = star (p' * a * p)" ``` krauss@22359 ` 361` ``` oops ``` krauss@22359 ` 362` krauss@22359 ` 363` krauss@22359 ` 364` ```lemma star_zero: ``` krauss@22359 ` 365` ``` "star (0::'a::kleene) = 1" ``` krauss@22359 ` 366` ``` by (rule star_unfold_left[of 0, simplified]) ``` krauss@22359 ` 367` krauss@22359 ` 368` krauss@22359 ` 369` ```(* Own lemmas *) ``` krauss@22359 ` 370` krauss@22359 ` 371` krauss@22359 ` 372` ```lemma x_less_star[simp]: ``` krauss@22359 ` 373` ``` fixes x :: "'a :: kleene" ``` krauss@22359 ` 374` ``` shows "x \ x * star a" ``` krauss@22359 ` 375` ```proof - ``` krauss@22359 ` 376` ``` have "x \ x * (1 + a * star a)" by (simp add:right_distrib) ``` krauss@22359 ` 377` ``` also have "\ = x * star a" by (simp only: star_unfold_left) ``` krauss@22359 ` 378` ``` finally show ?thesis . ``` krauss@22359 ` 379` ```qed ``` krauss@22359 ` 380` krauss@22359 ` 381` ```subsection {* Transitive Closure *} ``` krauss@22359 ` 382` krauss@22359 ` 383` ```definition ``` krauss@22359 ` 384` ``` "tcl (x::'a::kleene) = star x * x" ``` krauss@22359 ` 385` krauss@22359 ` 386` krauss@22359 ` 387` ```lemma tcl_zero: ``` krauss@22359 ` 388` ``` "tcl (0::'a::kleene) = 0" ``` krauss@22359 ` 389` ``` unfolding tcl_def by simp ``` krauss@22359 ` 390` krauss@22359 ` 391` krauss@22359 ` 392` ```subsection {* Naive Algorithm to generate the transitive closure *} ``` krauss@22359 ` 393` krauss@22359 ` 394` ```function (default "\x. 0", tailrec) ``` krauss@22359 ` 395` ``` mk_tcl :: "('a::{plus,times,ord,zero}) \ 'a \ 'a" ``` krauss@22359 ` 396` ```where ``` krauss@22359 ` 397` ``` "mk_tcl A X = (if X * A \ X then X else mk_tcl A (X + X * A))" ``` krauss@22359 ` 398` ``` by pat_completeness simp ``` krauss@22359 ` 399` krauss@22359 ` 400` ```declare mk_tcl.simps[simp del] (* loops *) ``` krauss@22359 ` 401` krauss@22359 ` 402` ```lemma mk_tcl_code[code]: ``` krauss@22359 ` 403` ``` "mk_tcl A X = ``` krauss@22359 ` 404` ``` (let XA = X * A ``` krauss@22359 ` 405` ``` in if XA \ X then X else mk_tcl A (X + XA))" ``` krauss@22359 ` 406` ``` unfolding mk_tcl.simps[of A X] Let_def .. ``` krauss@22359 ` 407` krauss@22359 ` 408` ```lemma mk_tcl_lemma1: ``` krauss@22359 ` 409` ``` fixes X :: "'a :: kleene" ``` krauss@22359 ` 410` ``` shows "(X + X * A) * star A = X * star A" ``` krauss@22359 ` 411` ```proof - ``` krauss@22359 ` 412` ``` have "A * star A \ 1 + A * star A" by simp ``` krauss@22359 ` 413` ``` also have "\ = star A" by (simp add:star_unfold_left) ``` krauss@22359 ` 414` ``` finally have "star A + A * star A = star A" by simp ``` krauss@22359 ` 415` ``` hence "X * (star A + A * star A) = X * star A" by simp ``` krauss@22359 ` 416` ``` thus ?thesis by (simp add:left_distrib right_distrib mult_ac) ``` krauss@22359 ` 417` ```qed ``` krauss@22359 ` 418` krauss@22359 ` 419` ```lemma mk_tcl_lemma2: ``` krauss@22359 ` 420` ``` fixes X :: "'a :: kleene" ``` krauss@22359 ` 421` ``` shows "X * A \ X \ X * star A = X" ``` krauss@22359 ` 422` ``` by (rule order_antisym) (auto simp:star4) ``` krauss@22359 ` 423` krauss@22359 ` 424` krauss@22359 ` 425` krauss@22359 ` 426` krauss@22359 ` 427` ```lemma mk_tcl_correctness: ``` krauss@22359 ` 428` ``` fixes A X :: "'a :: {kleene}" ``` krauss@22359 ` 429` ``` assumes "mk_tcl_dom (A, X)" ``` krauss@22359 ` 430` ``` shows "mk_tcl A X = X * star A" ``` krauss@22359 ` 431` ``` using prems ``` krauss@22359 ` 432` ``` by induct (auto simp:mk_tcl_lemma1 mk_tcl_lemma2) ``` krauss@22359 ` 433` krauss@22359 ` 434` ```lemma graph_implies_dom: "mk_tcl_graph x y \ mk_tcl_dom x" ``` krauss@22359 ` 435` ``` by (rule mk_tcl_graph.induct) (auto intro:accI elim:mk_tcl_rel.cases) ``` krauss@22359 ` 436` krauss@22359 ` 437` ```lemma mk_tcl_default: "\ mk_tcl_dom (a,x) \ mk_tcl a x = 0" ``` krauss@22359 ` 438` ``` unfolding mk_tcl_def ``` krauss@22359 ` 439` ``` by (rule fundef_default_value[OF mk_tcl_sum_def graph_implies_dom]) ``` krauss@22359 ` 440` krauss@22359 ` 441` krauss@22359 ` 442` ```text {* We can replace the dom-Condition of the correctness theorem ``` krauss@22359 ` 443` ``` with something executable *} ``` krauss@22359 ` 444` krauss@22359 ` 445` ```lemma mk_tcl_correctness2: ``` krauss@22359 ` 446` ``` fixes A X :: "'a :: {kleene}" ``` krauss@22359 ` 447` ``` assumes "mk_tcl A A \ 0" ``` krauss@22359 ` 448` ``` shows "mk_tcl A A = tcl A" ``` krauss@22359 ` 449` ``` using prems mk_tcl_default mk_tcl_correctness ``` krauss@22359 ` 450` ``` unfolding tcl_def ``` krauss@22359 ` 451` ``` by (auto simp:star_commute) ``` krauss@22359 ` 452` krauss@22359 ` 453` ```end ```