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