--- a/src/HOL/Library/Kleene_Algebra.thy Tue Sep 28 08:35:00 2010 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy Tue Sep 28 08:38:20 2010 +0200
@@ -483,56 +483,4 @@
end
-subsection {* A naive algorithm to generate the transitive closure *}
-
-function (default "\<lambda>x. 0", tailrec, domintros)
- mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"
-where
- "mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))"
- by pat_completeness simp
-
-declare mk_tcl.simps[simp del] (* loops *)
-
-lemma mk_tcl_code[code]:
- "mk_tcl A X =
- (let XA = X * A
- in if XA \<le> X then X else mk_tcl A (X + XA))"
- unfolding mk_tcl.simps[of A X] Let_def ..
-
-context kleene
-begin
-
-lemma mk_tcl_lemma1: "(X + X * A) * star A = X * star A"
-by (metis ka1 left_distrib mult_assoc mult_left_mono ord_simp2 zero_minimum)
-
-lemma mk_tcl_lemma2: "X * A \<le> X \<Longrightarrow> X * star A = X"
-by (rule antisym) (auto simp: star4)
-
end
-
-lemma mk_tcl_correctness:
- fixes X :: "'a::kleene"
- assumes "mk_tcl_dom (A, X)"
- shows "mk_tcl A X = X * star A"
- using assms
- by induct (auto simp: mk_tcl_lemma1 mk_tcl_lemma2)
-
-lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
- by (rule mk_tcl_graph.induct) (auto intro:accp.accI elim:mk_tcl_rel.cases)
-
-lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
- unfolding mk_tcl_def
- by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom])
-
-text {* We can replace the dom-Condition of the correctness theorem
- with something executable: *}
-
-lemma mk_tcl_correctness2:
- fixes A X :: "'a :: {kleene}"
- assumes "mk_tcl A A \<noteq> 0"
- shows "mk_tcl A A = tcl A"
- using assms mk_tcl_default mk_tcl_correctness
- unfolding tcl_def
- by auto
-
-end