# HG changeset patch
# User krauss
# Date 1182268849 -7200
# Node ID b73a6b72f706613ad0655df357311e6c4ae34d67
# Parent  9dad8095bd430b510a469a0acd7ed42e69056c40
generalized proofs so that call graphs can have any node type.

diff -r 9dad8095bd43 -r b73a6b72f706 src/HOL/Library/Graphs.thy
--- a/src/HOL/Library/Graphs.thy	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/Graphs.thy	Tue Jun 19 18:00:49 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""   (* FIXME proper header *)
+header {* General Graphs as Sets *}
 
 theory Graphs
 imports Main SCT_Misc Kleene_Algebras ExecutableSet
@@ -215,7 +215,6 @@
     unfolding graph_pow_def by simp_all
 qed
 
-
 lemma graph_leqI:
   assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
   shows "G \<le> H"
@@ -223,7 +222,6 @@
   unfolding graph_leq_def has_edge_def
   by auto
 
-
 lemma in_graph_plusE:
   assumes "has_edge (G + H) n e n'"
   assumes "has_edge G n e n' \<Longrightarrow> P"
@@ -232,6 +230,13 @@
   using assms
   by (auto simp: in_grplus)
 
+lemma in_graph_compE:
+  assumes GH: "has_edge (G * H) n e n'"
+  obtains e1 k e2 
+  where "has_edge G n e1 k" "has_edge H k e2 n'" "e = e1 * e2"
+  using GH
+  by (auto simp: in_grcomp)
+
 lemma 
   assumes "x \<in> S k"
   shows "x \<in> (\<Union>k. S k)"
diff -r 9dad8095bd43 -r b73a6b72f706 src/HOL/Library/Kleene_Algebras.thy
--- a/src/HOL/Library/Kleene_Algebras.thy	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/Kleene_Algebras.thy	Tue Jun 19 18:00:49 2007 +0200
@@ -382,15 +382,29 @@
 definition 
   "tcl (x::'a::kleene) = star x * x"
 
-
 lemma tcl_zero: 
   "tcl (0::'a::kleene) = 0"
   unfolding tcl_def by simp
 
+lemma tcl_unfold_right: "tcl a = a + tcl a * a"
+proof -
+  from star_unfold_right[of a]
+  have "a * (1 + star a * a) = a * star a" by simp
+  from this[simplified right_distrib, simplified]
+  show ?thesis
+    by (simp add:tcl_def star_commute mult_ac)
+qed
+
+lemma less_tcl: "a \<le> tcl a"
+proof -
+  have "a \<le> a + tcl a * a" by simp
+  also have "\<dots> = tcl a" by (rule tcl_unfold_right[symmetric])
+  finally show ?thesis .
+qed
 
 subsection {* Naive Algorithm to generate the transitive closure *}
 
-function (default "\<lambda>x. 0", tailrec)
+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))"
diff -r 9dad8095bd43 -r b73a6b72f706 src/HOL/Library/SCT_Definition.thy
--- a/src/HOL/Library/SCT_Definition.thy	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/SCT_Definition.thy	Tue Jun 19 18:00:49 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""   (* FIXME proper header *)
+header {* The Size-Change Principle (Definition) *}
 
 theory SCT_Definition
 imports Graphs Infinite_Set
@@ -32,7 +32,10 @@
 
 lemma sedge_UNIV:
   "UNIV = { LESS, LEQ }"
-  by auto (case_tac x, auto) (*FIXME*)
+proof (intro equalityI subsetI)
+  fix x show "x \<in> { LESS, LEQ }"
+    by (cases x) auto
+qed auto
 
 instance sedge :: finite
 proof
@@ -43,8 +46,8 @@
 lemmas [code func] = sedge_UNIV
 
 
-types scg = "(nat, sedge) graph"
-types acg = "(nat, scg) graph"
+types 'a scg = "('a, sedge) graph"
+types 'a acg = "('a, 'a scg) graph"
 
 
 subsection {* Size-Change Termination *}
@@ -59,46 +62,46 @@
   "eq G i j \<equiv> has_edge G i LEQ j"
 
 abbreviation
-  eql :: "scg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  eql :: "'a scg \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
 ("_ \<turnstile> _ \<leadsto> _")
 where
   "eql G i j \<equiv> has_edge G i LESS j \<or> has_edge G i LEQ j"
 
 
-abbreviation (input) descat :: "(nat, scg) ipath \<Rightarrow> nat sequence \<Rightarrow> nat \<Rightarrow> bool"
+abbreviation (input) descat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
 where
   "descat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))"
 
-abbreviation (input) eqat :: "(nat, scg) ipath \<Rightarrow> nat sequence \<Rightarrow> nat \<Rightarrow> bool"
+abbreviation (input) eqat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
 where
   "eqat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i))"
 
 
-abbreviation eqlat :: "(nat, scg) ipath \<Rightarrow> nat sequence \<Rightarrow> nat \<Rightarrow> bool"
+abbreviation (input) eqlat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
 where
   "eqlat p \<theta> i \<equiv> (has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))
                   \<or> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i)))"
 
 
-definition is_desc_thread :: "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> bool"
+definition is_desc_thread :: "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> bool"
 where
   "is_desc_thread \<theta> p = ((\<exists>n.\<forall>i\<ge>n. eqlat p \<theta> i) \<and> (\<exists>\<^sub>\<infinity>i. descat p \<theta> i))" 
 
-definition SCT :: "acg \<Rightarrow> bool"
+definition SCT :: "'a acg \<Rightarrow> bool"
 where
   "SCT \<A> = 
   (\<forall>p. has_ipath \<A> p \<longrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> p))"
 
 
 
-definition no_bad_graphs :: "acg \<Rightarrow> bool"
+definition no_bad_graphs :: "'a acg \<Rightarrow> bool"
 where
   "no_bad_graphs A = 
   (\<forall>n G. has_edge A n G n \<and> G * G = G
   \<longrightarrow> (\<exists>p. has_edge G p LESS p))"
 
 
-definition SCT' :: "acg \<Rightarrow> bool"
+definition SCT' :: "'a acg \<Rightarrow> bool"
 where
   "SCT' A = no_bad_graphs (tcl A)"
 
diff -r 9dad8095bd43 -r b73a6b72f706 src/HOL/Library/SCT_Examples.thy
--- a/src/HOL/Library/SCT_Examples.thy	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/SCT_Examples.thy	Tue Jun 19 18:00:49 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""   (* FIXME proper header *)
+header {* Examples for Size-Change Termination *}
 
 theory SCT_Examples
 imports Size_Change_Termination
@@ -23,9 +23,8 @@
   apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *)
   apply (rule ext, rule ext, simp) (* Show that they are correct *)
   apply (tactic "Sct.mk_call_graph") (* Build control graph *)
-  apply (rule LJA_apply)                 (* Apply main theorem *)
-  apply (simp add:finite_acg_ins finite_acg_empty) (* show finiteness *)
-  apply (rule SCT'_exec)
+  apply (rule SCT_Main)                 (* Apply main theorem *)
+  apply (simp add:finite_acg_simps) (* show finiteness *)
   by eval (* Evaluate to true *)
 
 function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -41,10 +40,9 @@
   apply (tactic "Sct.abs_rel_tac") 
   apply (rule ext, rule ext, simp) 
   apply (tactic "Sct.mk_call_graph")
-  apply (rule LJA_apply)            
-  apply (simp add:finite_acg_ins finite_acg_empty) 
-  apply (rule SCT'_exec)
-  by eval
+  apply (rule SCT_Main)
+  apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
+  by eval 
 
 function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
 where
@@ -60,10 +58,10 @@
   apply (tactic "Sct.abs_rel_tac") 
   apply (rule ext, rule ext, simp) 
   apply (tactic "Sct.mk_call_graph")
-  apply (rule LJA_apply)            
-  apply (simp add:finite_acg_ins finite_acg_empty) 
-  apply (rule SCT'_exec)
-  by eval
+  apply (rule SCT_Main)
+  apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
+  by eval 
+
 
 function (sequential) 
   bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -78,8 +76,8 @@
   apply (tactic "Sct.abs_rel_tac") 
   apply (rule ext, rule ext, simp) 
   apply (tactic "Sct.mk_call_graph")
-  apply (rule LJA_apply)            
-  apply (simp add:finite_acg_ins finite_acg_empty) 
-  by (rule SCT'_empty)
+  apply (rule SCT_Main)
+  apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
+  by (simp only:sctTest_simps cong: sctTest_congs)
 
 end
diff -r 9dad8095bd43 -r b73a6b72f706 src/HOL/Library/SCT_Implementation.thy
--- a/src/HOL/Library/SCT_Implementation.thy	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/SCT_Implementation.thy	Tue Jun 19 18:00:49 2007 +0200
@@ -3,10 +3,10 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""   (* FIXME proper header *)
+header {* Implemtation of the SCT criterion *}
 
 theory SCT_Implementation
-imports ExecutableSet SCT_Definition
+imports ExecutableSet SCT_Definition SCT_Theorem
 begin
 
 fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"
@@ -23,29 +23,101 @@
   "grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })"
   by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def)
 
-definition test_SCT :: "acg \<Rightarrow> bool"
+
+lemma mk_tcl_finite_terminates:
+  fixes A :: "'a acg"
+  assumes fA: "finite_acg A" 
+  shows "mk_tcl_dom (A, A)"
+proof -
+  from fA have fin_tcl: "finite_acg (tcl A)"
+    by (simp add:finite_tcl)
+
+  hence "finite (dest_graph (tcl A))"
+    unfolding finite_acg_def finite_graph_def ..
+
+  let ?count = "\<lambda>G. card (dest_graph G)"
+  let ?N = "?count (tcl A)"
+  let ?m = "\<lambda>X. ?N - (?count X)"
+
+  let ?P = "\<lambda>X. mk_tcl_dom (A, X)"
+  
+  {
+    fix X
+    assume "X \<le> tcl A"
+    then
+    have "mk_tcl_dom (A, X)"
+    proof (induct X rule:measure_induct_rule[of ?m])
+      case (less X)
+      show ?case
+      proof (cases "X * A \<le> X")
+        case True 
+        with mk_tcl.domintros show ?thesis by auto
+      next
+        case False
+        then have l: "X < X + X * A"
+          unfolding graph_less_def graph_leq_def graph_plus_def
+          by auto
+
+        from `X \<le> tcl A` 
+        have "X * A \<le> tcl A * A" by (simp add:mult_mono)
+        also have "\<dots> \<le> A + tcl A * A" by simp
+        also have "\<dots> = tcl A" by (simp add:tcl_unfold_right[symmetric])
+        finally have "X * A \<le> tcl A" .
+        with `X \<le> tcl A` 
+        have "X + X * A \<le> tcl A + tcl A"
+          by (rule add_mono)
+        hence less_tcl: "X + X * A \<le> tcl A" by simp 
+        hence "X < tcl A"
+          using l `X \<le> tcl A` by auto
+
+        from less_tcl fin_tcl
+        have "finite_acg (X + X * A)" by (rule finite_acg_subset)
+        hence "finite (dest_graph (X + X * A))" 
+          unfolding finite_acg_def finite_graph_def ..
+        
+        hence X: "?count X < ?count (X + X * A)"
+          using l[simplified graph_less_def graph_leq_def]
+          by (rule psubset_card_mono)
+        
+        have "?count X < ?N" 
+          apply (rule psubset_card_mono)
+          by fact (rule `X < tcl A`[simplified graph_less_def])
+        
+        with X have "?m (X + X * A) < ?m X" by arith
+        
+        from  less.hyps this less_tcl
+        have "mk_tcl_dom (A, X + X * A)" .
+        with mk_tcl.domintros show ?thesis .
+      qed
+    qed
+  }
+  from this less_tcl show ?thesis .
+qed
+
+
+lemma mk_tcl_finite_tcl:
+  fixes A :: "'a acg"
+  assumes fA: "finite_acg A"
+  shows "mk_tcl A A = tcl A"
+  using mk_tcl_finite_terminates[OF fA]
+  by (simp only: tcl_def mk_tcl_correctness star_commute)
+
+definition test_SCT :: "nat acg \<Rightarrow> bool"
 where
   "test_SCT \<A> = 
   (let \<T> = mk_tcl \<A> \<A>
-    in (\<T> \<noteq> 0 \<and>
-       (\<forall>(n,G,m)\<in>dest_graph \<T>. 
+    in (\<forall>(n,G,m)\<in>dest_graph \<T>. 
           n \<noteq> m \<or> G * G \<noteq> G \<or> 
-         (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS))))"
+         (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
 
 
 lemma SCT'_exec:
-  assumes a: "test_SCT \<A>"
-  shows "SCT' \<A>"
-proof -
-  from mk_tcl_correctness2 a 
-  have "mk_tcl \<A> \<A> = tcl \<A>" 
-    unfolding test_SCT_def Let_def by auto
-  
-  with a
-  show ?thesis
-    unfolding SCT'_def no_bad_graphs_def test_SCT_def Let_def has_edge_def
-    by auto
-qed
+  assumes fin: "finite_acg A"
+  shows "SCT' A = test_SCT A"
+  using mk_tcl_finite_tcl[OF fin]
+  unfolding test_SCT_def Let_def 
+  unfolding SCT'_def no_bad_graphs_def has_edge_def
+  by force
 
 code_modulename SML
   Implementation Graphs
@@ -75,7 +147,7 @@
 subsection {* Witness checking *}
 
 
-definition test_SCT_witness :: "acg \<Rightarrow> acg \<Rightarrow> bool"
+definition test_SCT_witness :: "nat acg \<Rightarrow> nat acg \<Rightarrow> bool"
 where
   "test_SCT_witness A T = 
   (A \<le> T \<and> A * T \<le> T \<and>
diff -r 9dad8095bd43 -r b73a6b72f706 src/HOL/Library/SCT_Interpretation.thy
--- a/src/HOL/Library/SCT_Interpretation.thy	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/SCT_Interpretation.thy	Tue Jun 19 18:00:49 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""   (* FIXME proper header *)
+header {* Applying SCT to function definitions *}
 
 theory SCT_Interpretation
 imports Main SCT_Misc SCT_Definition
@@ -92,11 +92,8 @@
 qed
 
 
-
-types ('q, 'a) interpr = "('a, 'q) cdesc \<times> (nat \<Rightarrow> 'a \<Rightarrow> nat)"
 types 'a measures = "nat \<Rightarrow> 'a \<Rightarrow> nat"
 
-
 fun stepP :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> 
   ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> bool"
 where
@@ -188,7 +185,7 @@
 
 
 definition
-  approx :: "scg \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc 
+  approx :: "nat scg \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc 
   \<Rightarrow> 'a measures \<Rightarrow> 'a measures \<Rightarrow> bool"
   where
   "approx G C C' M M'
@@ -240,7 +237,7 @@
 by (cases c1, cases c2) (auto simp: no_step_def)
 
 definition
-  sound_int :: "acg \<Rightarrow> ('a, 'q) cdesc list 
+  sound_int :: "nat acg \<Rightarrow> ('a, 'q) cdesc list 
   \<Rightarrow> 'a measures list \<Rightarrow> bool"
 where
   "sound_int \<A> RDs M =
diff -r 9dad8095bd43 -r b73a6b72f706 src/HOL/Library/SCT_Misc.thy
--- a/src/HOL/Library/SCT_Misc.thy	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/SCT_Misc.thy	Tue Jun 19 18:00:49 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""   (* FIXME proper header *)
+header {* Miscellaneous Tools for Size-Change Termination *}
 
 theory SCT_Misc   (* FIXME proper name *)
 imports Main
diff -r 9dad8095bd43 -r b73a6b72f706 src/HOL/Library/SCT_Theorem.thy
--- a/src/HOL/Library/SCT_Theorem.thy	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/SCT_Theorem.thy	Tue Jun 19 18:00:49 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""   (* FIXME proper header *)
+header "Proof of the Size-Change Principle"
 
 theory SCT_Theorem
 imports Main Ramsey SCT_Misc SCT_Definition
@@ -11,17 +11,17 @@
 
 subsection {* The size change criterion SCT *}
 
-definition is_thread :: "nat \<Rightarrow> nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> bool"
+definition is_thread :: "nat \<Rightarrow> 'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> bool"
 where
   "is_thread n \<theta> p = (\<forall>i\<ge>n. eqlat p \<theta> i)"
 
 definition is_fthread :: 
-  "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
 where
   "is_fthread \<theta> mp i j = (\<forall>k\<in>{i..<j}. eqlat mp \<theta> k)"
 
 definition is_desc_fthread ::
-  "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
 where
   "is_desc_fthread \<theta> mp i j = 
   (is_fthread \<theta> mp i j \<and>
@@ -36,163 +36,7 @@
   (\<exists>\<theta>. is_desc_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
 
 
-subsection {* Bounded graphs and threads *}
-
-definition 
-  "bounded_scg (P::nat) (G::scg) = 
-  (\<forall>p e p'. has_edge G p e p' \<longrightarrow> p < P \<and> p' < P)"
-
-definition
-  "bounded_acg P ACG = 
-  (\<forall>n G n'. has_edge ACG n G n' \<longrightarrow> n < P \<and> n' < P \<and> bounded_scg P G)"
-  
-definition
-  "bounded_mp P mp = (\<forall>i. bounded_scg P (snd (mp i)))"
-
-definition (* = finite (range \<theta>) *)
-  "bounded_th (P::nat) n \<theta> = (\<forall>i>n. \<theta> i < P)"
-
-definition 
-  "finite_scg (G::scg) = (\<exists>P. bounded_scg P G)"
-
-definition
-  "finite_acg (A::acg) = (\<exists>P. bounded_acg P A)"
-
-lemma "finite (insert x A) = finite A"
-by simp
-
-
-lemma finite_scg_finite[simp]: "finite_scg (Graph G) = finite G"
-proof
-  assume "finite_scg (Graph G)"
-  thm bounded_scg_def
-  
-  then obtain P where bounded: "bounded_scg P (Graph G)" 
-    by (auto simp:finite_scg_def)
-
-  show "finite G"
-  proof (rule finite_subset)
-    from bounded 
-    show "G \<subseteq> {0 .. P - 1} \<times> { LESS, LEQ } \<times> { 0 .. P - 1}"
-      apply (auto simp:bounded_scg_def has_edge_def)
-      apply force
-      apply (case_tac "aa", auto)
-      apply force
-      done
-
-    show "finite \<dots>"
-      by (auto intro: finite_cartesian_product finite_atLeastAtMost)
-  qed
-next
-  assume "finite G"
-  thus "finite_scg (Graph G)"
-  proof induct
-    show "finite_scg (Graph {})"
-      unfolding finite_scg_def bounded_scg_def has_edge_def by auto
-  next
-    fix x G 
-    assume "finite G" "x \<notin> G" "finite_scg (Graph G)"
-    then obtain P
-      where bG: "bounded_scg P (Graph G)" 
-      by (auto simp:finite_scg_def)
-    
-    obtain p e p' where x: "x = (p, e, p')" by (cases x, auto)
-    
-    let ?Q = "max P (max (Suc p) (Suc p'))"
-    have "P \<le> ?Q" "Suc p \<le> ?Q" "Suc p' \<le> ?Q" by auto
-    with bG
-    have "bounded_scg ?Q (Graph (insert x G))" 
-      unfolding x bounded_scg_def has_edge_def
-      apply simp
-      apply (intro allI, elim allE)
-      by auto
-    thus "finite_scg (Graph (insert x G))"
-      by (auto simp:finite_scg_def)
-  qed
-qed
-
-lemma finite_acg_empty:
-  "finite_acg (Graph {})"
-unfolding finite_acg_def bounded_acg_def has_edge_def
-by auto
-
-lemma bounded_scg_up: "bounded_scg P G \<Longrightarrow> P \<le> Q \<Longrightarrow> bounded_scg Q G"
-  unfolding bounded_scg_def
-  by force
-
-lemma bounded_up: "bounded_acg P G \<Longrightarrow> P \<le> Q \<Longrightarrow> bounded_acg Q G"
-  unfolding bounded_acg_def 
-  apply auto
-  apply force+
-  apply (rule bounded_scg_up)
-  by auto
-
-lemma bacg_insert:
-  assumes "bounded_acg P (Graph A)"
-  assumes "n < P" "m < P" "bounded_scg P G"
-  shows "bounded_acg P (Graph (insert (n, G, m) A))"
-  using prems
-  unfolding bounded_acg_def has_edge_def 
-  by auto
-
-lemma finite_acg_ins:
-  "finite_acg (Graph (insert (n,G,m) A)) = 
-  (finite_scg G \<and> finite_acg (Graph A))" (is "?A = (?B \<and> ?C)")
-proof
-  assume "?A"
-  thus "?B \<and> ?C"
-    unfolding finite_acg_def bounded_acg_def finite_scg_def has_edge_def
-    by auto
-next
-  assume "?B \<and> ?C"
-  thus ?A
-  proof
-    assume "?B" "?C"
-
-    from `?C`
-    obtain P where bA: "bounded_acg P (Graph A)" by (auto simp:finite_acg_def)
-    from `?B` 
-    obtain P' where bG: "bounded_scg P' G" by (auto simp:finite_scg_def)
-
-    let ?Q = "max (max P P') (max (Suc n) (Suc m))"
-    have "P \<le> ?Q" "n < ?Q" "m < ?Q" by auto
-    have "bounded_acg ?Q (Graph (insert (n, G, m) A))"
-      apply (rule bacg_insert)
-      apply (rule bounded_up)
-      apply (rule bA)
-      apply auto
-      apply (rule bounded_scg_up)
-      apply (rule bG)
-      by auto
-    thus "finite_acg (Graph (insert (n, G, m) A))"
-      by (auto simp:finite_acg_def)
-  qed
-qed
-
-
-lemma bounded_mpath:
-  assumes "has_ipath acg mp"
-  and "bounded_acg P acg"
-  shows "bounded_mp P mp"
-  using prems
-  unfolding bounded_acg_def bounded_mp_def has_ipath_def
-  by blast
-
-lemma bounded_th: 
-  assumes th: "is_thread n \<theta> mp"
-  and mp: "bounded_mp P mp"
-  shows "bounded_th P n \<theta>"
-  unfolding bounded_th_def
-proof (intro allI impI)
-  fix i assume "n < i"
-  
-  from mp have "bounded_scg P (snd (mp i))" unfolding bounded_mp_def ..
-  moreover
-  from th `n < i` have "eqlat mp \<theta> i" unfolding is_thread_def by auto
-  ultimately
-  show "\<theta> i < P" unfolding bounded_scg_def by auto
-qed
-
+subsection {* Everything is finite *}
 
 lemma finite_range:
   fixes f :: "nat \<Rightarrow> 'a"
@@ -216,117 +60,345 @@
   with neq[of "f m" m] show ?thesis by blast
 qed
 
-
-lemma bounded_th_infinite_visit:
-  fixes \<theta> :: "nat sequence"
-  assumes b: "bounded_th P n \<theta>"
-  shows "\<exists>p. \<exists>\<^sub>\<infinity>i. \<theta> i = p" 
+lemma finite_range_ignore_prefix:
+  fixes f :: "nat \<Rightarrow> 'a"
+  assumes fA: "finite A"
+  assumes inA: "\<forall>x\<ge>n. f x \<in> A"
+  shows "finite (range f)"
 proof -
-  have split: "range \<theta> = (\<theta> ` {0 .. n}) \<union> (\<theta> ` {i. n < i})"
+  have a: "UNIV = {0 ..< (n::nat)} \<union> { x. n \<le> x }" by auto
+  have b: "range f = f ` {0 ..< n} \<union> f ` { x. n \<le> x }" 
     (is "\<dots> = ?A \<union> ?B")
-    unfolding image_Un[symmetric] by auto
-
-  have "finite ?A" by (rule finite_imageI) auto
+    by (unfold a) (simp add:image_Un)
+  
+  have "finite ?A" by (rule finite_imageI) simp
   moreover
-  have "finite ?B"
-  proof (rule finite_subset)
-    from b
-    show "?B \<subseteq> { 0 ..< P }"
-      unfolding bounded_th_def
-      by auto
-    show "finite \<dots>" by auto
-  qed
-
-  ultimately have "finite (range \<theta>)"
-    unfolding split by auto
-
-  with finite_range show ?thesis .
+  from inA have "?B \<subseteq> A" by auto
+  from this fA have "finite ?B" by (rule finite_subset)
+  ultimately show ?thesis using b by simp
 qed
 
 
-lemma bounded_scgcomp:
-  "bounded_scg P A 
-  \<Longrightarrow> bounded_scg P B 
-  \<Longrightarrow> bounded_scg P (A * B)"
-  unfolding bounded_scg_def
-  by (auto simp:in_grcomp)
+
+
+definition 
+  "finite_graph G = finite (dest_graph G)"
+definition 
+  "all_finite G = (\<forall>n H m. has_edge G n H m \<longrightarrow> finite_graph H)"
+definition
+  "finite_acg A = (finite_graph A \<and> all_finite A)"
+definition 
+  "nodes G = fst ` dest_graph G \<union> snd ` snd ` dest_graph G"
+definition 
+  "edges G = fst ` snd ` dest_graph G"
+definition 
+  "smallnodes G = \<Union>(nodes ` edges G)"
+
+lemma thread_image_nodes:
+  assumes th: "is_thread n \<theta> p"
+  shows "\<forall>i\<ge>n. \<theta> i \<in> nodes (snd (p i))"
+using prems
+unfolding is_thread_def has_edge_def nodes_def
+by force
+
+lemma finite_nodes: "finite_graph G \<Longrightarrow> finite (nodes G)"
+  unfolding finite_graph_def nodes_def
+  by auto
+
+lemma nodes_subgraph: "A \<le> B \<Longrightarrow> nodes A \<subseteq> nodes B"
+  unfolding graph_leq_def nodes_def
+  by auto
+
+lemma finite_edges: "finite_graph G \<Longrightarrow> finite (edges G)"
+  unfolding finite_graph_def edges_def
+  by auto
+
+lemma edges_sum[simp]: "edges (A + B) = edges A \<union> edges B"
+  unfolding edges_def graph_plus_def
+  by auto
+
+lemma nodes_sum[simp]: "nodes (A + B) = nodes A \<union> nodes B"
+  unfolding nodes_def graph_plus_def
+  by auto
+
+lemma finite_acg_subset:
+  "A \<le> B \<Longrightarrow> finite_acg B \<Longrightarrow> finite_acg A"
+  unfolding finite_acg_def finite_graph_def all_finite_def
+  has_edge_def graph_leq_def
+  by (auto elim:finite_subset)
 
-lemma bounded_acgcomp:
-  "bounded_acg P A 
-  \<Longrightarrow> bounded_acg P B 
-  \<Longrightarrow> bounded_acg P (A * B)"
-  unfolding bounded_acg_def
-  by (auto simp:in_grcomp intro!:bounded_scgcomp) 
+lemma scg_finite: 
+  fixes G :: "'a scg"
+  assumes fin: "finite (nodes G)"
+  shows "finite_graph G"
+  unfolding finite_graph_def
+proof (rule finite_subset)
+  show "dest_graph G \<subseteq> nodes G \<times> UNIV \<times> nodes G" (is "_ \<subseteq> ?P")
+    unfolding nodes_def
+    by force
+  show "finite ?P"
+    by (intro finite_cartesian_product fin finite)
+qed
+
+lemma smallnodes_sum[simp]: 
+  "smallnodes (A + B) = smallnodes A \<union> smallnodes B"
+  unfolding smallnodes_def 
+  by auto
+
+lemma in_smallnodes:
+  fixes A :: "'a acg"
+  assumes e: "has_edge A x G y"
+  shows "nodes G \<subseteq> smallnodes A"
+proof -
+  have "fst (snd (x, G, y)) \<in> fst ` snd  ` dest_graph A"
+    unfolding has_edge_def
+    by (rule imageI)+ (rule e[unfolded has_edge_def])
+  then have "G \<in> edges A" 
+    unfolding edges_def by simp
+  thus ?thesis
+    unfolding smallnodes_def
+    by blast
+qed
+
+lemma finite_smallnodes:
+  assumes fA: "finite_acg A"
+  shows "finite (smallnodes A)"
+  unfolding smallnodes_def edges_def
+proof 
+  from fA
+  show "finite (nodes ` fst ` snd ` dest_graph A)"
+    unfolding finite_acg_def finite_graph_def
+    by simp
+  
+  fix M assume "M \<in> nodes ` fst ` snd ` dest_graph A"
+  then obtain n G m  
+    where M: "M = nodes G" and nGm: "(n,G,m) \<in> dest_graph A"
+    by auto
+  
+  from fA
+  have "all_finite A" unfolding finite_acg_def by simp
+  with nGm have "finite_graph G" 
+    unfolding all_finite_def has_edge_def by auto
+  with finite_nodes 
+  show "finite M" 
+    unfolding finite_graph_def M .
+qed
+
+lemma nodes_tcl:
+  "nodes (tcl A) = nodes A"
+proof
+  show "nodes A \<subseteq> nodes (tcl A)"
+    apply (rule nodes_subgraph)
+    by (subst tcl_unfold_right) simp
+
+  show "nodes (tcl A) \<subseteq> nodes A"
+  proof 
+    fix x assume "x \<in> nodes (tcl A)"
+    then obtain z G y
+      where z: "z \<in> dest_graph (tcl A)"
+      and dis: "z = (x, G, y) \<or> z = (y, G, x)"
+      unfolding nodes_def
+      by auto force+
 
-lemma bounded_acgpow:
-  "bounded_acg P A
-  \<Longrightarrow> bounded_acg P (A ^ (Suc n))"
-  by (induct n, simp add:power_Suc) 
-   (subst power_Suc, blast intro:bounded_acgcomp)
+    from dis
+    show "x \<in> nodes A"
+    proof
+      assume "z = (x, G, y)"
+      with z have "has_edge (tcl A) x G y" unfolding has_edge_def by simp
+      then obtain n where "n > 0 " and An: "has_edge (A ^ n) x G y"
+        unfolding in_tcl by auto
+      then obtain n' where "n = Suc n'" by (cases n, auto)
+      hence "A ^ n = A * A ^ n'" by (simp add:power_Suc)
+      with An obtain e k 
+        where "has_edge A x e k" by (auto simp:in_grcomp)
+      thus "x \<in> nodes A" unfolding has_edge_def nodes_def 
+        by force
+    next
+      assume "z = (y, G, x)"
+      with z have "has_edge (tcl A) y G x" unfolding has_edge_def by simp
+      then obtain n where "n > 0 " and An: "has_edge (A ^ n) y G x"
+        unfolding in_tcl by auto
+      then obtain n' where "n = Suc n'" by (cases n, auto)
+      hence "A ^ n = A ^ n' * A" by (simp add:power_Suc power_commutes)
+      with An obtain e k 
+        where "has_edge A k e x" by (auto simp:in_grcomp)
+      thus "x \<in> nodes A" unfolding has_edge_def nodes_def 
+        by force
+    qed
+  qed
+qed
+
+lemma smallnodes_tcl: 
+  fixes A :: "'a acg"
+  shows "smallnodes (tcl A) = smallnodes A"
+proof (intro equalityI subsetI)
+  fix n assume "n \<in> smallnodes (tcl A)"
+  then obtain x G y where edge: "has_edge (tcl A) x G y" 
+    and "n \<in> nodes G"
+    unfolding smallnodes_def edges_def has_edge_def 
+    by auto
+  
+  from `n \<in> nodes G`
+  have "n \<in> fst ` dest_graph G \<or> n \<in> snd ` snd ` dest_graph G"
+    (is "?A \<or> ?B")
+    unfolding nodes_def by blast
+  thus "n \<in> smallnodes A"
+  proof
+    assume ?A
+    then obtain m e where A: "has_edge G n e m"
+      unfolding has_edge_def by auto
+
+    have "tcl A = A * star A"
+      unfolding tcl_def
+      by (simp add: star_commute[of A A A, simplified])
+
+    with edge
+    have "has_edge (A * star A) x G y" by simp
+    then obtain H H' z
+      where AH: "has_edge A x H z" and G: "G = H * H'"
+      by (auto simp:in_grcomp)
+    from A
+    obtain m' e' where "has_edge H n e' m'"
+      by (auto simp:G in_grcomp)
+    hence "n \<in> nodes H" unfolding nodes_def has_edge_def 
+      by force
+    with in_smallnodes[OF AH] show "n \<in> smallnodes A" ..
+  next
+    assume ?B
+    then obtain m e where B: "has_edge G m e n"
+      unfolding has_edge_def by auto
 
-lemma bounded_plus:
-  assumes b: "bounded_acg P acg"
-  shows "bounded_acg P (tcl acg)"
-  unfolding bounded_acg_def
-proof (intro allI impI conjI)
-  fix n G m
-  assume "tcl acg \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m"
-  then obtain i where "0 < i" and i: "acg ^ i \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m"
-    unfolding in_tcl by auto (* FIXME: Disambiguate \<turnstile> Grammar *)
-  from b have "bounded_acg P (acg ^ (Suc (i - 1)))"
-    by (rule bounded_acgpow)
-  with `0 < i` have "bounded_acg P (acg ^ i)" by simp
-  with i
-  show "n < P" "m < P" "bounded_scg P G"
-    unfolding bounded_acg_def
-    by auto
+    with edge
+    have "has_edge (star A * A) x G y" by (simp add:tcl_def)
+    then obtain H H' z
+      where AH': "has_edge A z H' y" and G: "G = H * H'"
+      by (auto simp:in_grcomp)
+    from B
+    obtain m' e' where "has_edge H' m' e' n"
+      by (auto simp:G in_grcomp)
+    hence "n \<in> nodes H'" unfolding nodes_def has_edge_def 
+      by force
+    with in_smallnodes[OF AH'] show "n \<in> smallnodes A" ..
+  qed
+next
+  fix x assume "x \<in> smallnodes A"
+  then show "x \<in> smallnodes (tcl A)"
+    by (subst tcl_unfold_right) simp
+qed
+
+lemma finite_nodegraphs:
+  assumes F: "finite F"
+  shows "finite { G::'a scg. nodes G \<subseteq> F }" (is "finite ?P")
+proof (rule finite_subset)
+  show "?P \<subseteq> Graph ` (Pow (F \<times> UNIV \<times> F))" (is "?P \<subseteq> ?Q")
+  proof
+    fix x assume xP: "x \<in> ?P"
+    obtain S where x[simp]: "x = Graph S"
+      by (cases x) auto
+    from xP
+    show "x \<in> ?Q"
+      apply (simp add:nodes_def)
+      apply (rule imageI)
+      apply (rule PowI)
+      apply force
+      done
+  qed
+  show "finite ?Q"
+    by (auto intro:finite_imageI finite_cartesian_product F finite)
+qed
+
+lemma finite_graphI:
+  fixes A :: "'a acg"
+  assumes fin: "finite (nodes A)" "finite (smallnodes A)"
+  shows "finite_graph A"
+proof -
+  obtain S where A[simp]: "A = Graph S"
+    by (cases A) auto
+
+  have "finite S" 
+  proof (rule finite_subset)
+    show "S \<subseteq> nodes A \<times> { G::'a scg. nodes G \<subseteq> smallnodes A } \<times> nodes A"
+      (is "S \<subseteq> ?T")
+    proof
+      fix x assume xS: "x \<in> S"
+      obtain a b c where x[simp]: "x = (a, b, c)"
+        by (cases x) auto
+
+      then have edg: "has_edge A a b c"
+        unfolding has_edge_def using xS
+        by simp
+
+      hence "a \<in> nodes A" "c \<in> nodes A"
+        unfolding nodes_def has_edge_def by force+
+      moreover
+      from edg have "nodes b \<subseteq> smallnodes A" by (rule in_smallnodes)
+      hence "b \<in> { G :: 'a scg. nodes G \<subseteq> smallnodes A }" by simp
+      ultimately show "x \<in> ?T" by simp
+    qed
+
+    show "finite ?T"
+      by (intro finite_cartesian_product fin finite_nodegraphs)
+  qed
+  thus ?thesis
+    unfolding finite_graph_def by simp
 qed
 
 
-lemma bounded_scg_def':
-  "bounded_scg P G = (\<forall>(p,e,p')\<in>dest_graph G. p < P \<and> p' < P)"
-  unfolding bounded_scg_def has_edge_def
+lemma smallnodes_allfinite:
+  fixes A :: "'a acg"
+  assumes fin: "finite (smallnodes A)"
+  shows "all_finite A"
+  unfolding all_finite_def
+proof (intro allI impI)
+  fix n H m assume "has_edge A n H m"
+  then have "nodes H \<subseteq> smallnodes A"
+    by (rule in_smallnodes)
+  then have "finite (nodes H)" 
+    by (rule finite_subset) (rule fin)
+  thus "finite_graph H" by (rule scg_finite)
+qed
+
+lemma finite_tcl: 
+  fixes A :: "'a acg"
+  shows "finite_acg (tcl A) \<longleftrightarrow> finite_acg A"
+proof
+  assume f: "finite_acg A"
+  from f have g: "finite_graph A" and "all_finite A"
+    unfolding finite_acg_def by auto
+
+  from g have "finite (nodes A)" by (rule finite_nodes)
+  then have "finite (nodes (tcl A))" unfolding nodes_tcl .
+  moreover
+  from f have "finite (smallnodes A)" by (rule finite_smallnodes)
+  then have fs: "finite (smallnodes (tcl A))" unfolding smallnodes_tcl .
+  ultimately
+  have "finite_graph (tcl A)" by (rule finite_graphI)
+
+  moreover from fs have "all_finite (tcl A)"
+    by (rule smallnodes_allfinite)
+  ultimately show "finite_acg (tcl A)" unfolding finite_acg_def ..
+next
+  assume a: "finite_acg (tcl A)"
+  have "A \<le> tcl A" by (rule less_tcl)
+  thus "finite_acg A" using a
+    by (rule finite_acg_subset)
+qed
+
+lemma finite_acg_empty: "finite_acg (Graph {})"
+  unfolding finite_acg_def finite_graph_def all_finite_def
+  has_edge_def
+  by simp
+
+lemma finite_acg_ins: 
+  assumes fA: "finite_acg (Graph A)"
+  assumes fG: "finite G"
+  shows "finite_acg (Graph (insert (a, Graph G, b) A))" 
+  using fA fG
+  unfolding finite_acg_def finite_graph_def all_finite_def
+  has_edge_def
   by auto
 
-
-lemma finite_bounded_scg: "finite { G. bounded_scg P G }"
-proof (rule finite_subset)
-  show "{G. bounded_scg P G} \<subseteq> 
-    Graph ` (Pow ({0 .. P - 1} \<times> UNIV \<times> {0 .. P - 1}))"
-  proof (rule, simp)
-    fix G 
-    
-    assume b: "bounded_scg P G"
-
-    show "G \<in> Graph ` Pow ({0..P - Suc 0} \<times> UNIV \<times> {0..P - Suc 0})"
-    proof (cases G)
-      fix G' assume [simp]: "G = Graph G'"
-      
-      from b show ?thesis
-        by (auto simp:bounded_scg_def' image_def)
-    qed
-  qed
-
-  show "finite \<dots>"
-    apply (rule finite_imageI)
-    apply (unfold finite_Pow_iff)
-    by (intro finite_cartesian_product finite_atLeastAtMost 
-      finite_class.finite)
-qed
-
-lemma bounded_finite:
-  assumes bounded: "bounded_acg P A"
-  shows "finite (dest_graph A)"
-proof (rule finite_subset)
-  
-  from bounded
-  show "dest_graph A \<subseteq> {0 .. P - 1} \<times> { G. bounded_scg P G } \<times> { 0 .. P - 1}"
-    by (auto simp:bounded_acg_def has_edge_def) force+
-
-  show "finite \<dots>"
-    by (intro finite_cartesian_product finite_atLeastAtMost finite_bounded_scg)
-qed
-
+lemmas finite_acg_simps = finite_acg_empty finite_acg_ins finite_graph_def
 
 subsection {* Contraction and more *}
 
@@ -750,8 +822,6 @@
   with krng show "\<exists>k\<in>section s i. descat p (connect s \<theta>s) k" ..
 qed
 
-
-
 lemma mk_inf_thread:
   assumes [simp]: "increasing s"
   assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))"
@@ -779,8 +849,9 @@
   unfolding is_desc_thread_def 
 proof (intro exI conjI)
 
-  from mk_inf_thread[of s n] is_thread_def fths
-  show "\<forall>i\<ge>s (Suc n). eqlat p \<theta> i" by simp
+  from mk_inf_thread[of s n \<theta> p] fths
+  show "\<forall>i\<ge>s (Suc n). eqlat p \<theta> i" 
+    by (fold is_thread_def) simp
 
   show "\<exists>\<^sub>\<infinity>l. descat p \<theta> l"
     unfolding INF_nat
@@ -1169,40 +1240,41 @@
 
 subsection {* Main Result *}
 
+
 theorem LJA_Theorem4: 
-  assumes "bounded_acg P \<A>"
-  shows "SCT \<A> \<longleftrightarrow> SCT' \<A>"
+  assumes "finite_acg A"
+  shows "SCT A \<longleftrightarrow> SCT' A"
 proof
-  assume "SCT \<A>"
+  assume "SCT A"
   
-  show "SCT' \<A>"
+  show "SCT' A"
   proof (rule classical)
-    assume "\<not> SCT' \<A>"
+    assume "\<not> SCT' A"
     
     then obtain n G
-      where in_closure: "(tcl \<A>) \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
+      where in_closure: "(tcl A) \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
       and idemp: "G * G = G"
       and no_strict_arc: "\<forall>p. \<not>(G \<turnstile> p \<leadsto>\<^bsup>\<down>\<^esup> p)"
       unfolding SCT'_def no_bad_graphs_def by auto
     
     from in_closure obtain k
-      where k_pow: "\<A> ^ k \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
+      where k_pow: "A ^ k \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
       and "0 < k"
       unfolding in_tcl by auto
 	
     from power_induces_path k_pow
     obtain loop where loop_props:
-      "has_fpath \<A> loop"
+      "has_fpath A loop"
       "n = fst loop" "n = end_node loop"
       "G = prod loop" "k = length (snd loop)" . 
 
     with `0 < k` and path_loop_graph
-    have "has_ipath \<A> (omega loop)" by blast
-    with `SCT \<A>` 
+    have "has_ipath A (omega loop)" by blast
+    with `SCT A` 
     have thread: "\<exists>\<theta>. is_desc_thread \<theta> (omega loop)" by (auto simp:SCT_def)
 
     let ?s = "\<lambda>i. k * i"
-    let ?cp = "\<lambda>i. (n, G)"
+    let ?cp = "\<lambda>i::nat. (n, G)"
 
     from loop_props have "fst loop = end_node loop" by auto
     with `0 < k` `k = length (snd loop)`
@@ -1226,19 +1298,20 @@
       unfolding is_desc_thread_def is_thread_def 
       by auto
 
-    have "bounded_th P n \<theta>" 
-    proof -
-      from `bounded_acg P \<A>`
-      have "bounded_acg P (tcl \<A>)" by (rule bounded_plus)
-      with in_closure have "bounded_scg P G"
-        unfolding bounded_acg_def by simp
-      hence "bounded_mp P ?cp"
-        unfolding bounded_mp_def by simp
-      with thr bounded_th 
-      show ?thesis by auto
+    have "finite (range \<theta>)"
+    proof (rule finite_range_ignore_prefix)
+      
+      from `finite_acg A`
+      have "finite_acg (tcl A)" by (simp add:finite_tcl)
+      with in_closure have "finite_graph G" 
+        unfolding finite_acg_def all_finite_def by blast
+      thus "finite (nodes G)" by (rule finite_nodes)
+
+      from thread_image_nodes[OF thr]
+      show "\<forall>i\<ge>n. \<theta> i \<in> nodes G" by simp
     qed
-    with bounded_th_infinite_visit
-    obtain p where inf_visit: "\<exists>\<^sub>\<infinity>i. \<theta> i = p" by blast
+    with finite_range
+    obtain p where inf_visit: "\<exists>\<^sub>\<infinity>i. \<theta> i = p" by auto
 
     then obtain i where "n < i" "\<theta> i = p" 
       by (auto simp:INF_nat)
@@ -1252,7 +1325,9 @@
     from inf_visit obtain k where "j < k" "\<theta> k = p"
       by (auto simp:INF_nat)
 
-    from `i < j` `j < k` `n < i` thr fin_from_inf `descat ?cp \<theta> j`
+    from `i < j` `j < k` `n < i` thr 
+      fin_from_inf[of n \<theta> ?cp]
+      `descat ?cp \<theta> j`
     have "is_desc_fthread \<theta> ?cp i k"
       unfolding is_desc_fthread_def
       by auto
@@ -1271,38 +1346,39 @@
 	by (simp add:sub_path_def upt_rec[of i k] idemp)
     qed
 
-    with `i < j` `j < k` dfth Lemma7b
+    with `i < j` `j < k` dfth Lemma7b[of i k ?cp p p]
     have "dsc G p p" by auto
     with no_strict_arc have False by auto
     thus ?thesis ..
   qed
 next
-  assume "SCT' \<A>"
+  assume "SCT' A"
 
-  show "SCT \<A>"
+  show "SCT A"
   proof (rule classical)
-    assume "\<not> SCT \<A>"
+    assume "\<not> SCT A"
 
     with SCT_def
     obtain p 
-      where ipath: "has_ipath \<A> p"
+      where ipath: "has_ipath A p"
       and no_desc_th: "\<not> (\<exists>\<theta>. is_desc_thread \<theta> p)"
-      by auto
+      by blast
 
-    from `bounded_acg P \<A>`
-    have "finite (dest_graph (tcl \<A>))" (is "finite ?AG")
-      by (intro bounded_finite bounded_plus)
+    from `finite_acg A`
+    have "finite_acg (tcl A)" by (simp add: finite_tcl)
+    hence "finite (dest_graph (tcl A))" (is "finite ?AG")
+      by (simp add: finite_acg_def finite_graph_def)
 
     from pdesc_acgplus[OF ipath]
-    have a: "\<And>x y. x<y \<Longrightarrow> pdesc p\<langle>x,y\<rangle> \<in> dest_graph (tcl \<A>)"
+    have a: "\<And>x y. x<y \<Longrightarrow> pdesc p\<langle>x,y\<rangle> \<in> dest_graph (tcl A)"
       unfolding has_edge_def .
       
     obtain S G
-      where "infinite S" "G \<in> dest_graph (tcl \<A>)" 
+      where "infinite S" "G \<in> dest_graph (tcl A)" 
       and all_G: "\<And>x y. \<lbrakk> x \<in> S; y \<in> S; x < y\<rbrakk> \<Longrightarrow> 
       pdesc (p\<langle>x,y\<rangle>) = G"
       apply (rule RamseyNatpairs[of ?AG "\<lambda>(x,y). pdesc p\<langle>x, y\<rangle>"])
-      apply (rule `finite (dest_graph (tcl \<A>))`)
+      apply (rule `finite ?AG`)
       by (simp only:split_conv, rule a, auto)
 
     obtain n H m where
@@ -1318,14 +1394,14 @@
     note increasing_bij[OF this, simp]
       
     from ipath_contract inc ipath
-    have "has_ipath (tcl \<A>) ?q" .
+    have "has_ipath (tcl A) ?q" .
 
     from all_G G_struct 
     have all_H: "\<And>i. (snd (?q i)) = H"
 	  unfolding contract_def 
       by simp
     
-    have loop: "(tcl \<A>) \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
+    have loop: "(tcl A) \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
       and idemp: "H * H = H"
     proof - 
       let ?i = "?s 0" and ?j = "?s (Suc 0)" and ?k = "?s (Suc (Suc 0))"
@@ -1345,8 +1421,8 @@
 		by auto
 			
       hence "m = n" by simp
-      thus "tcl \<A> \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
-		using G_struct `G \<in> dest_graph (tcl \<A>)`
+      thus "tcl A \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
+		using G_struct `G \<in> dest_graph (tcl A)`
 		by (simp add:has_edge_def)
 	  
       from sub_path_prod[of ?i ?j ?k p]      
@@ -1355,7 +1431,7 @@
     qed
     moreover have "\<And>k. \<not>dsc H k k"
     proof
-      fix k :: nat assume "dsc H k k"
+      fix k :: 'a assume "dsc H k k"
       
       with all_H repeated_edge
       have "\<exists>\<theta>. is_desc_thread \<theta> ?q" by fast
@@ -1366,22 +1442,10 @@
     qed
     ultimately 
     have False
-      using `SCT' \<A>`[unfolded SCT'_def no_bad_graphs_def]
+      using `SCT' A`[unfolded SCT'_def no_bad_graphs_def]
       by blast
     thus ?thesis ..
   qed
 qed
 
-
-lemma LJA_apply:
-  assumes fin: "finite_acg A"
-  assumes "SCT' A"
-  shows "SCT A"
-proof -
-  from fin obtain P where b: "bounded_acg P A"
-    unfolding finite_acg_def ..
-  show ?thesis using LJA_Theorem4[OF b] and `SCT' A`
-    by simp
-qed
-
 end
diff -r 9dad8095bd43 -r b73a6b72f706 src/HOL/Library/Size_Change_Termination.thy
--- a/src/HOL/Library/Size_Change_Termination.thy	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/Size_Change_Termination.thy	Tue Jun 19 18:00:49 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""   (* FIXME proper header *)
+header "Size-Change Termination"
 
 theory Size_Change_Termination
 imports SCT_Theorem SCT_Interpretation SCT_Implementation 
@@ -102,4 +102,10 @@
 lemmas sctTest_congs = 
   if_weak_cong let_weak_cong setbcomp_cong
 
+
+lemma SCT_Main:
+  "finite_acg A \<Longrightarrow> test_SCT A \<Longrightarrow> SCT A"
+  using LJA_Theorem4 SCT'_exec
+  by auto
+
 end
diff -r 9dad8095bd43 -r b73a6b72f706 src/HOL/Library/sct.ML
--- a/src/HOL/Library/sct.ML	Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/sct.ML	Tue Jun 19 18:00:49 2007 +0200
@@ -18,8 +18,8 @@
 
 fun map_matrix f xss = map (map f) xss
 
-val scgT = @{typ scg}
-val acgT = @{typ acg}
+val scgT = @{typ "nat scg"}
+val acgT = @{typ "nat acg"}
 
 fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT))
 fun graphT nT eT = Type ("Graphs.graph", [nT, eT])