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