1.1 --- a/src/HOL/Library/Kleene_Algebra.thy	Tue Sep 28 08:35:00 2010 +0200
     1.2 +++ b/src/HOL/Library/Kleene_Algebra.thy	Tue Sep 28 08:38:20 2010 +0200
     1.3 @@ -483,56 +483,4 @@
     1.4  
     1.5  end
     1.6  
     1.7 -subsection {* A naive algorithm to generate the transitive closure *}
     1.8 -
     1.9 -function (default "\<lambda>x. 0", tailrec, domintros)
    1.10 -  mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"
    1.11 -where
    1.12 -  "mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))"
    1.13 -  by pat_completeness simp
    1.14 -
    1.15 -declare mk_tcl.simps[simp del] (* loops *)
    1.16 -
    1.17 -lemma mk_tcl_code[code]:
    1.18 -  "mk_tcl A X = 
    1.19 -  (let XA = X * A 
    1.20 -  in if XA \<le> X then X else mk_tcl A (X + XA))"
    1.21 -  unfolding mk_tcl.simps[of A X] Let_def ..
    1.22 -
    1.23 -context kleene
    1.24 -begin
    1.25 -
    1.26 -lemma mk_tcl_lemma1: "(X + X * A) * star A = X * star A"
    1.27 -by (metis ka1 left_distrib mult_assoc mult_left_mono ord_simp2 zero_minimum)
    1.28 -
    1.29 -lemma mk_tcl_lemma2: "X * A \<le> X \<Longrightarrow> X * star A = X"
    1.30 -by (rule antisym) (auto simp: star4)
    1.31 -
    1.32  end
    1.33 -
    1.34 -lemma mk_tcl_correctness:
    1.35 -  fixes X :: "'a::kleene"
    1.36 -  assumes "mk_tcl_dom (A, X)"
    1.37 -  shows "mk_tcl A X = X * star A"
    1.38 -  using assms
    1.39 -  by induct (auto simp: mk_tcl_lemma1 mk_tcl_lemma2)
    1.40 -
    1.41 -lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
    1.42 -  by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases)
    1.43 -
    1.44 -lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
    1.45 -  unfolding mk_tcl_def
    1.46 -  by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom])
    1.47 -
    1.48 -text {* We can replace the dom-Condition of the correctness theorem 
    1.49 -  with something executable: *}
    1.50 -
    1.51 -lemma mk_tcl_correctness2:
    1.52 -  fixes A X :: "'a :: {kleene}"
    1.53 -  assumes "mk_tcl A A \<noteq> 0"
    1.54 -  shows "mk_tcl A A = tcl A"
    1.55 -  using assms mk_tcl_default mk_tcl_correctness
    1.56 -  unfolding tcl_def 
    1.57 -  by auto
    1.58 -
    1.59 -end