# HG changeset patch
# User krauss
# Date 1285655900 -7200
# Node ID fa94799e3a3b90790aa1fd42e4b52186e17270b3
# Parent  a727e1dab1627a3621e596a3dc0020142ff17227
dropped obsolete mk_tcl

diff -r a727e1dab162 -r fa94799e3a3b src/HOL/Library/Kleene_Algebra.thy
--- 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