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