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