removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)
authorkrauss
Fri Nov 06 13:42:29 2009 +0100 (2009-11-06)
changeset 334690183f9545fa2
parent 33468 91ea7115da1b
child 33470 0c4e48deeefe
child 33498 318acc1c9399
removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)
src/HOL/IsaMakefile
src/HOL/SizeChange/Correctness.thy
src/HOL/SizeChange/Criterion.thy
src/HOL/SizeChange/Examples.thy
src/HOL/SizeChange/Graphs.thy
src/HOL/SizeChange/Implementation.thy
src/HOL/SizeChange/Interpretation.thy
src/HOL/SizeChange/Misc_Tools.thy
src/HOL/SizeChange/ROOT.ML
src/HOL/SizeChange/Size_Change_Termination.thy
src/HOL/SizeChange/document/root.tex
src/HOL/SizeChange/sct.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Nov 06 13:36:46 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Nov 06 13:42:29 2009 +0100
     1.3 @@ -57,7 +57,6 @@
     1.4    HOL-Prolog \
     1.5    HOL-SET_Protocol \
     1.6    HOL-SMT-Examples \
     1.7 -  HOL-SizeChange \
     1.8    HOL-Statespace \
     1.9    HOL-Subst \
    1.10        TLA-Buffer \
    1.11 @@ -766,19 +765,6 @@
    1.12  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
    1.13  
    1.14  
    1.15 -## HOL-SizeChange
    1.16 -
    1.17 -HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz
    1.18 -
    1.19 -$(LOG)/HOL-SizeChange.gz: $(OUT)/HOL Library/Kleene_Algebra.thy	\
    1.20 -  SizeChange/Graphs.thy SizeChange/Misc_Tools.thy			\
    1.21 -  SizeChange/Criterion.thy SizeChange/Correctness.thy			\
    1.22 -  SizeChange/Interpretation.thy SizeChange/Implementation.thy		\
    1.23 -  SizeChange/Size_Change_Termination.thy SizeChange/Examples.thy	\
    1.24 -  SizeChange/sct.ML SizeChange/ROOT.ML
    1.25 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL SizeChange
    1.26 -
    1.27 -
    1.28  ## HOL-Decision_Procs
    1.29  
    1.30  HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz
    1.31 @@ -1443,7 +1429,7 @@
    1.32  		$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz	\
    1.33  		$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz		\
    1.34  		$(LOG)/HOL-SET_Protocol.gz $(LOG)/HOL-SMT-Examples.gz	\
    1.35 -		$(LOG)/HOL-SMT.gz $(LOG)/HOL-SizeChange.gz		\
    1.36 +		$(LOG)/HOL-SMT.gz					\
    1.37  		$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz		\
    1.38  		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
    1.39  		$(LOG)/HOL-W0.gz $(LOG)/HOL-Word-Examples.gz		\
     2.1 --- a/src/HOL/SizeChange/Correctness.thy	Fri Nov 06 13:36:46 2009 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,1450 +0,0 @@
     2.4 -(*  Title:      HOL/Library/SCT_Theorem.thy
     2.5 -    Author:     Alexander Krauss, TU Muenchen
     2.6 -*)
     2.7 -
     2.8 -header "Proof of the Size-Change Principle"
     2.9 -
    2.10 -theory Correctness
    2.11 -imports Main Ramsey Misc_Tools Criterion
    2.12 -begin
    2.13 -
    2.14 -subsection {* Auxiliary definitions *}
    2.15 -
    2.16 -definition is_thread :: "nat \<Rightarrow> 'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> bool"
    2.17 -where
    2.18 -  "is_thread n \<theta> p = (\<forall>i\<ge>n. eqlat p \<theta> i)"
    2.19 -
    2.20 -definition is_fthread :: 
    2.21 -  "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
    2.22 -where
    2.23 -  "is_fthread \<theta> mp i j = (\<forall>k\<in>{i..<j}. eqlat mp \<theta> k)"
    2.24 -
    2.25 -definition is_desc_fthread ::
    2.26 -  "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
    2.27 -where
    2.28 -  "is_desc_fthread \<theta> mp i j = 
    2.29 -  (is_fthread \<theta> mp i j \<and>
    2.30 -  (\<exists>k\<in>{i..<j}. descat mp \<theta> k))"
    2.31 -
    2.32 -definition
    2.33 -  "has_fth p i j n m = 
    2.34 -  (\<exists>\<theta>. is_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
    2.35 -
    2.36 -definition
    2.37 -  "has_desc_fth p i j n m = 
    2.38 -  (\<exists>\<theta>. is_desc_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
    2.39 -
    2.40 -
    2.41 -subsection {* Everything is finite *}
    2.42 -
    2.43 -lemma finite_range:
    2.44 -  fixes f :: "nat \<Rightarrow> 'a"
    2.45 -  assumes fin: "finite (range f)"
    2.46 -  shows "\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x"
    2.47 -proof (rule classical)
    2.48 -  assume "\<not>(\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x)"
    2.49 -  hence "\<forall>x. \<exists>j. \<forall>i>j. f i \<noteq> x"
    2.50 -    unfolding INFM_nat by blast
    2.51 -  with choice
    2.52 -  have "\<exists>j. \<forall>x. \<forall>i>(j x). f i \<noteq> x" .
    2.53 -  then obtain j where 
    2.54 -    neq: "\<And>x i. j x < i \<Longrightarrow> f i \<noteq> x" by blast
    2.55 -
    2.56 -  from fin have "finite (range (j o f))" 
    2.57 -    by (auto simp:comp_def range_composition)
    2.58 -  with finite_nat_bounded
    2.59 -  obtain m where "range (j o f) \<subseteq> {..<m}" by blast
    2.60 -  hence "j (f m) < m" unfolding comp_def by auto
    2.61 -
    2.62 -  with neq[of "f m" m] show ?thesis by blast
    2.63 -qed
    2.64 -
    2.65 -lemma finite_range_ignore_prefix:
    2.66 -  fixes f :: "nat \<Rightarrow> 'a"
    2.67 -  assumes fA: "finite A"
    2.68 -  assumes inA: "\<forall>x\<ge>n. f x \<in> A"
    2.69 -  shows "finite (range f)"
    2.70 -proof -
    2.71 -  have a: "UNIV = {0 ..< (n::nat)} \<union> { x. n \<le> x }" by auto
    2.72 -  have b: "range f = f ` {0 ..< n} \<union> f ` { x. n \<le> x }" 
    2.73 -    (is "\<dots> = ?A \<union> ?B")
    2.74 -    by (unfold a) (simp add:image_Un)
    2.75 -  
    2.76 -  have "finite ?A" by (rule finite_imageI) simp
    2.77 -  moreover
    2.78 -  from inA have "?B \<subseteq> A" by auto
    2.79 -  from this fA have "finite ?B" by (rule finite_subset)
    2.80 -  ultimately show ?thesis using b by simp
    2.81 -qed
    2.82 -
    2.83 -
    2.84 -
    2.85 -
    2.86 -definition 
    2.87 -  "finite_graph G = finite (dest_graph G)"
    2.88 -definition 
    2.89 -  "all_finite G = (\<forall>n H m. has_edge G n H m \<longrightarrow> finite_graph H)"
    2.90 -definition
    2.91 -  "finite_acg A = (finite_graph A \<and> all_finite A)"
    2.92 -definition 
    2.93 -  "nodes G = fst ` dest_graph G \<union> snd ` snd ` dest_graph G"
    2.94 -definition 
    2.95 -  "edges G = fst ` snd ` dest_graph G"
    2.96 -definition 
    2.97 -  "smallnodes G = \<Union>(nodes ` edges G)"
    2.98 -
    2.99 -lemma thread_image_nodes:
   2.100 -  assumes th: "is_thread n \<theta> p"
   2.101 -  shows "\<forall>i\<ge>n. \<theta> i \<in> nodes (snd (p i))"
   2.102 -using prems
   2.103 -unfolding is_thread_def has_edge_def nodes_def
   2.104 -by force
   2.105 -
   2.106 -lemma finite_nodes: "finite_graph G \<Longrightarrow> finite (nodes G)"
   2.107 -  unfolding finite_graph_def nodes_def
   2.108 -  by auto
   2.109 -
   2.110 -lemma nodes_subgraph: "A \<le> B \<Longrightarrow> nodes A \<subseteq> nodes B"
   2.111 -  unfolding graph_leq_def nodes_def
   2.112 -  by auto
   2.113 -
   2.114 -lemma finite_edges: "finite_graph G \<Longrightarrow> finite (edges G)"
   2.115 -  unfolding finite_graph_def edges_def
   2.116 -  by auto
   2.117 -
   2.118 -lemma edges_sum[simp]: "edges (A + B) = edges A \<union> edges B"
   2.119 -  unfolding edges_def graph_plus_def
   2.120 -  by auto
   2.121 -
   2.122 -lemma nodes_sum[simp]: "nodes (A + B) = nodes A \<union> nodes B"
   2.123 -  unfolding nodes_def graph_plus_def
   2.124 -  by auto
   2.125 -
   2.126 -lemma finite_acg_subset:
   2.127 -  "A \<le> B \<Longrightarrow> finite_acg B \<Longrightarrow> finite_acg A"
   2.128 -  unfolding finite_acg_def finite_graph_def all_finite_def
   2.129 -  has_edge_def graph_leq_def
   2.130 -  by (auto elim:finite_subset)
   2.131 -
   2.132 -lemma scg_finite: 
   2.133 -  fixes G :: "'a scg"
   2.134 -  assumes fin: "finite (nodes G)"
   2.135 -  shows "finite_graph G"
   2.136 -  unfolding finite_graph_def
   2.137 -proof (rule finite_subset)
   2.138 -  show "dest_graph G \<subseteq> nodes G \<times> UNIV \<times> nodes G" (is "_ \<subseteq> ?P")
   2.139 -    unfolding nodes_def
   2.140 -    by force
   2.141 -  show "finite ?P"
   2.142 -    by (intro finite_cartesian_product fin finite)
   2.143 -qed
   2.144 -
   2.145 -lemma smallnodes_sum[simp]: 
   2.146 -  "smallnodes (A + B) = smallnodes A \<union> smallnodes B"
   2.147 -  unfolding smallnodes_def 
   2.148 -  by auto
   2.149 -
   2.150 -lemma in_smallnodes:
   2.151 -  fixes A :: "'a acg"
   2.152 -  assumes e: "has_edge A x G y"
   2.153 -  shows "nodes G \<subseteq> smallnodes A"
   2.154 -proof -
   2.155 -  have "fst (snd (x, G, y)) \<in> fst ` snd  ` dest_graph A"
   2.156 -    unfolding has_edge_def
   2.157 -    by (rule imageI)+ (rule e[unfolded has_edge_def])
   2.158 -  then have "G \<in> edges A" 
   2.159 -    unfolding edges_def by simp
   2.160 -  thus ?thesis
   2.161 -    unfolding smallnodes_def
   2.162 -    by blast
   2.163 -qed
   2.164 -
   2.165 -lemma finite_smallnodes:
   2.166 -  assumes fA: "finite_acg A"
   2.167 -  shows "finite (smallnodes A)"
   2.168 -  unfolding smallnodes_def edges_def
   2.169 -proof 
   2.170 -  from fA
   2.171 -  show "finite (nodes ` fst ` snd ` dest_graph A)"
   2.172 -    unfolding finite_acg_def finite_graph_def
   2.173 -    by simp
   2.174 -  
   2.175 -  fix M assume "M \<in> nodes ` fst ` snd ` dest_graph A"
   2.176 -  then obtain n G m  
   2.177 -    where M: "M = nodes G" and nGm: "(n,G,m) \<in> dest_graph A"
   2.178 -    by auto
   2.179 -  
   2.180 -  from fA
   2.181 -  have "all_finite A" unfolding finite_acg_def by simp
   2.182 -  with nGm have "finite_graph G" 
   2.183 -    unfolding all_finite_def has_edge_def by auto
   2.184 -  with finite_nodes 
   2.185 -  show "finite M" 
   2.186 -    unfolding finite_graph_def M .
   2.187 -qed
   2.188 -
   2.189 -lemma nodes_tcl:
   2.190 -  "nodes (tcl A) = nodes A"
   2.191 -proof
   2.192 -  show "nodes A \<subseteq> nodes (tcl A)"
   2.193 -    apply (rule nodes_subgraph)
   2.194 -    by (subst tcl_unfold_right) simp
   2.195 -
   2.196 -  show "nodes (tcl A) \<subseteq> nodes A"
   2.197 -  proof 
   2.198 -    fix x assume "x \<in> nodes (tcl A)"
   2.199 -    then obtain z G y
   2.200 -      where z: "z \<in> dest_graph (tcl A)"
   2.201 -      and dis: "z = (x, G, y) \<or> z = (y, G, x)"
   2.202 -      unfolding nodes_def
   2.203 -      by auto force+
   2.204 -
   2.205 -    from dis
   2.206 -    show "x \<in> nodes A"
   2.207 -    proof
   2.208 -      assume "z = (x, G, y)"
   2.209 -      with z have "has_edge (tcl A) x G y" unfolding has_edge_def by simp
   2.210 -      then obtain n where "n > 0 " and An: "has_edge (A ^ n) x G y"
   2.211 -        unfolding in_tcl by auto
   2.212 -      then obtain n' where "n = Suc n'" by (cases n, auto)
   2.213 -      hence "A ^ n = A * A ^ n'" by (simp add:power_Suc)
   2.214 -      with An obtain e k 
   2.215 -        where "has_edge A x e k" by (auto simp:in_grcomp)
   2.216 -      thus "x \<in> nodes A" unfolding has_edge_def nodes_def 
   2.217 -        by force
   2.218 -    next
   2.219 -      assume "z = (y, G, x)"
   2.220 -      with z have "has_edge (tcl A) y G x" unfolding has_edge_def by simp
   2.221 -      then obtain n where "n > 0 " and An: "has_edge (A ^ n) y G x"
   2.222 -        unfolding in_tcl by auto
   2.223 -      then obtain n' where "n = Suc n'" by (cases n, auto)
   2.224 -      hence "A ^ n = A ^ n' * A" by (simp add:power_Suc power_commutes)
   2.225 -      with An obtain e k 
   2.226 -        where "has_edge A k e x" by (auto simp:in_grcomp)
   2.227 -      thus "x \<in> nodes A" unfolding has_edge_def nodes_def 
   2.228 -        by force
   2.229 -    qed
   2.230 -  qed
   2.231 -qed
   2.232 -
   2.233 -lemma smallnodes_tcl: 
   2.234 -  fixes A :: "'a acg"
   2.235 -  shows "smallnodes (tcl A) = smallnodes A"
   2.236 -proof (intro equalityI subsetI)
   2.237 -  fix n assume "n \<in> smallnodes (tcl A)"
   2.238 -  then obtain x G y where edge: "has_edge (tcl A) x G y" 
   2.239 -    and "n \<in> nodes G"
   2.240 -    unfolding smallnodes_def edges_def has_edge_def 
   2.241 -    by auto
   2.242 -  
   2.243 -  from `n \<in> nodes G`
   2.244 -  have "n \<in> fst ` dest_graph G \<or> n \<in> snd ` snd ` dest_graph G"
   2.245 -    (is "?A \<or> ?B")
   2.246 -    unfolding nodes_def by blast
   2.247 -  thus "n \<in> smallnodes A"
   2.248 -  proof
   2.249 -    assume ?A
   2.250 -    then obtain m e where A: "has_edge G n e m"
   2.251 -      unfolding has_edge_def by auto
   2.252 -
   2.253 -    have "tcl A = A * star A"
   2.254 -      unfolding tcl_def
   2.255 -      by (simp add: star_simulation[of A A A, simplified])
   2.256 -
   2.257 -    with edge
   2.258 -    have "has_edge (A * star A) x G y" by simp
   2.259 -    then obtain H H' z
   2.260 -      where AH: "has_edge A x H z" and G: "G = H * H'"
   2.261 -      by (auto simp:in_grcomp)
   2.262 -    from A
   2.263 -    obtain m' e' where "has_edge H n e' m'"
   2.264 -      by (auto simp:G in_grcomp)
   2.265 -    hence "n \<in> nodes H" unfolding nodes_def has_edge_def 
   2.266 -      by force
   2.267 -    with in_smallnodes[OF AH] show "n \<in> smallnodes A" ..
   2.268 -  next
   2.269 -    assume ?B
   2.270 -    then obtain m e where B: "has_edge G m e n"
   2.271 -      unfolding has_edge_def by auto
   2.272 -
   2.273 -    with edge
   2.274 -    have "has_edge (star A * A) x G y" by (simp add:tcl_def)
   2.275 -    then obtain H H' z
   2.276 -      where AH': "has_edge A z H' y" and G: "G = H * H'"
   2.277 -      by (auto simp:in_grcomp simp del: star_slide2)
   2.278 -    from B
   2.279 -    obtain m' e' where "has_edge H' m' e' n"
   2.280 -      by (auto simp:G in_grcomp)
   2.281 -    hence "n \<in> nodes H'" unfolding nodes_def has_edge_def 
   2.282 -      by force
   2.283 -    with in_smallnodes[OF AH'] show "n \<in> smallnodes A" ..
   2.284 -  qed
   2.285 -next
   2.286 -  fix x assume "x \<in> smallnodes A"
   2.287 -  then show "x \<in> smallnodes (tcl A)"
   2.288 -    by (subst tcl_unfold_right) simp
   2.289 -qed
   2.290 -
   2.291 -lemma finite_nodegraphs:
   2.292 -  assumes F: "finite F"
   2.293 -  shows "finite { G::'a scg. nodes G \<subseteq> F }" (is "finite ?P")
   2.294 -proof (rule finite_subset)
   2.295 -  show "?P \<subseteq> Graph ` (Pow (F \<times> UNIV \<times> F))" (is "?P \<subseteq> ?Q")
   2.296 -  proof
   2.297 -    fix x assume xP: "x \<in> ?P"
   2.298 -    obtain S where x[simp]: "x = Graph S"
   2.299 -      by (cases x) auto
   2.300 -    from xP
   2.301 -    show "x \<in> ?Q"
   2.302 -      apply (simp add:nodes_def)
   2.303 -      apply (rule imageI)
   2.304 -      apply (rule PowI)
   2.305 -      apply force
   2.306 -      done
   2.307 -  qed
   2.308 -  show "finite ?Q"
   2.309 -    by (auto intro:finite_imageI finite_cartesian_product F finite)
   2.310 -qed
   2.311 -
   2.312 -lemma finite_graphI:
   2.313 -  fixes A :: "'a acg"
   2.314 -  assumes fin: "finite (nodes A)" "finite (smallnodes A)"
   2.315 -  shows "finite_graph A"
   2.316 -proof -
   2.317 -  obtain S where A[simp]: "A = Graph S"
   2.318 -    by (cases A) auto
   2.319 -
   2.320 -  have "finite S" 
   2.321 -  proof (rule finite_subset)
   2.322 -    show "S \<subseteq> nodes A \<times> { G::'a scg. nodes G \<subseteq> smallnodes A } \<times> nodes A"
   2.323 -      (is "S \<subseteq> ?T")
   2.324 -    proof
   2.325 -      fix x assume xS: "x \<in> S"
   2.326 -      obtain a b c where x[simp]: "x = (a, b, c)"
   2.327 -        by (cases x) auto
   2.328 -
   2.329 -      then have edg: "has_edge A a b c"
   2.330 -        unfolding has_edge_def using xS
   2.331 -        by simp
   2.332 -
   2.333 -      hence "a \<in> nodes A" "c \<in> nodes A"
   2.334 -        unfolding nodes_def has_edge_def by force+
   2.335 -      moreover
   2.336 -      from edg have "nodes b \<subseteq> smallnodes A" by (rule in_smallnodes)
   2.337 -      hence "b \<in> { G :: 'a scg. nodes G \<subseteq> smallnodes A }" by simp
   2.338 -      ultimately show "x \<in> ?T" by simp
   2.339 -    qed
   2.340 -
   2.341 -    show "finite ?T"
   2.342 -      by (intro finite_cartesian_product fin finite_nodegraphs)
   2.343 -  qed
   2.344 -  thus ?thesis
   2.345 -    unfolding finite_graph_def by simp
   2.346 -qed
   2.347 -
   2.348 -
   2.349 -lemma smallnodes_allfinite:
   2.350 -  fixes A :: "'a acg"
   2.351 -  assumes fin: "finite (smallnodes A)"
   2.352 -  shows "all_finite A"
   2.353 -  unfolding all_finite_def
   2.354 -proof (intro allI impI)
   2.355 -  fix n H m assume "has_edge A n H m"
   2.356 -  then have "nodes H \<subseteq> smallnodes A"
   2.357 -    by (rule in_smallnodes)
   2.358 -  then have "finite (nodes H)" 
   2.359 -    by (rule finite_subset) (rule fin)
   2.360 -  thus "finite_graph H" by (rule scg_finite)
   2.361 -qed
   2.362 -
   2.363 -lemma finite_tcl: 
   2.364 -  fixes A :: "'a acg"
   2.365 -  shows "finite_acg (tcl A) \<longleftrightarrow> finite_acg A"
   2.366 -proof
   2.367 -  assume f: "finite_acg A"
   2.368 -  from f have g: "finite_graph A" and "all_finite A"
   2.369 -    unfolding finite_acg_def by auto
   2.370 -
   2.371 -  from g have "finite (nodes A)" by (rule finite_nodes)
   2.372 -  then have "finite (nodes (tcl A))" unfolding nodes_tcl .
   2.373 -  moreover
   2.374 -  from f have "finite (smallnodes A)" by (rule finite_smallnodes)
   2.375 -  then have fs: "finite (smallnodes (tcl A))" unfolding smallnodes_tcl .
   2.376 -  ultimately
   2.377 -  have "finite_graph (tcl A)" by (rule finite_graphI)
   2.378 -
   2.379 -  moreover from fs have "all_finite (tcl A)"
   2.380 -    by (rule smallnodes_allfinite)
   2.381 -  ultimately show "finite_acg (tcl A)" unfolding finite_acg_def ..
   2.382 -next
   2.383 -  assume a: "finite_acg (tcl A)"
   2.384 -  have "A \<le> tcl A" by (rule less_tcl)
   2.385 -  thus "finite_acg A" using a
   2.386 -    by (rule finite_acg_subset)
   2.387 -qed
   2.388 -
   2.389 -lemma finite_acg_empty: "finite_acg (Graph {})"
   2.390 -  unfolding finite_acg_def finite_graph_def all_finite_def
   2.391 -  has_edge_def
   2.392 -  by simp
   2.393 -
   2.394 -lemma finite_acg_ins: 
   2.395 -  assumes fA: "finite_acg (Graph A)"
   2.396 -  assumes fG: "finite G"
   2.397 -  shows "finite_acg (Graph (insert (a, Graph G, b) A))" 
   2.398 -  using fA fG
   2.399 -  unfolding finite_acg_def finite_graph_def all_finite_def
   2.400 -  has_edge_def
   2.401 -  by auto
   2.402 -
   2.403 -lemmas finite_acg_simps = finite_acg_empty finite_acg_ins finite_graph_def
   2.404 -
   2.405 -subsection {* Contraction and more *}
   2.406 -
   2.407 -abbreviation 
   2.408 -  "pdesc P == (fst P, prod P, end_node P)"
   2.409 -
   2.410 -lemma pdesc_acgplus: 
   2.411 -  assumes "has_ipath \<A> p"
   2.412 -  and "i < j"
   2.413 -  shows "has_edge (tcl \<A>) (fst (p\<langle>i,j\<rangle>)) (prod (p\<langle>i,j\<rangle>)) (end_node (p\<langle>i,j\<rangle>))"
   2.414 -  unfolding plus_paths
   2.415 -  apply (rule exI)
   2.416 -  apply (insert prems)  
   2.417 -  by (auto intro:sub_path_is_path[of "\<A>" p i j] simp:sub_path_def)
   2.418 -
   2.419 -
   2.420 -lemma combine_fthreads: 
   2.421 -  assumes range: "i < j" "j \<le> k"
   2.422 -  shows 
   2.423 -  "has_fth p i k m r =
   2.424 -  (\<exists>n. has_fth p i j m n \<and> has_fth p j k n r)" (is "?L = ?R")
   2.425 -proof (intro iffI)
   2.426 -  assume "?L"
   2.427 -  then obtain \<theta>
   2.428 -    where "is_fthread \<theta> p i k" 
   2.429 -    and [simp]: "\<theta> i = m" "\<theta> k = r"
   2.430 -    by (auto simp:has_fth_def)
   2.431 -
   2.432 -  with range
   2.433 -  have "is_fthread \<theta> p i j" and "is_fthread \<theta> p j k"
   2.434 -    by (auto simp:is_fthread_def)
   2.435 -  hence "has_fth p i j m (\<theta> j)" and "has_fth p j k (\<theta> j) r"
   2.436 -    by (auto simp:has_fth_def)
   2.437 -  thus "?R" by auto
   2.438 -next
   2.439 -  assume "?R"
   2.440 -  then obtain n \<theta>1 \<theta>2
   2.441 -    where ths: "is_fthread \<theta>1 p i j" "is_fthread \<theta>2 p j k"
   2.442 -    and [simp]: "\<theta>1 i = m" "\<theta>1 j = n" "\<theta>2 j = n" "\<theta>2 k = r"
   2.443 -    by (auto simp:has_fth_def)
   2.444 -
   2.445 -  let ?\<theta> = "(\<lambda>i. if i < j then \<theta>1 i else \<theta>2 i)"
   2.446 -  have "is_fthread ?\<theta> p i k"
   2.447 -    unfolding is_fthread_def
   2.448 -  proof
   2.449 -    fix l assume range: "l \<in> {i..<k}"
   2.450 -    
   2.451 -    show "eqlat p ?\<theta> l"
   2.452 -    proof (cases rule:three_cases)
   2.453 -      assume "Suc l < j"
   2.454 -      with ths range show ?thesis 
   2.455 -        unfolding is_fthread_def Ball_def
   2.456 -        by simp
   2.457 -    next
   2.458 -      assume "Suc l = j"
   2.459 -      hence "l < j" "\<theta>2 (Suc l) = \<theta>1 (Suc l)" by auto
   2.460 -      with ths range show ?thesis 
   2.461 -        unfolding is_fthread_def Ball_def
   2.462 -        by simp
   2.463 -    next
   2.464 -      assume "j \<le> l"
   2.465 -      with ths range show ?thesis 
   2.466 -        unfolding is_fthread_def Ball_def
   2.467 -        by simp
   2.468 -    qed arith
   2.469 -  qed
   2.470 -  moreover 
   2.471 -  have "?\<theta> i = m" "?\<theta> k = r" using range by auto
   2.472 -  ultimately show "has_fth p i k m r" 
   2.473 -    by (auto simp:has_fth_def)
   2.474 -qed 
   2.475 -
   2.476 -
   2.477 -lemma desc_is_fthread:
   2.478 -  "is_desc_fthread \<theta> p i k \<Longrightarrow> is_fthread \<theta> p i k"
   2.479 -  unfolding is_desc_fthread_def
   2.480 -  by simp
   2.481 -
   2.482 -
   2.483 -lemma combine_dfthreads: 
   2.484 -  assumes range: "i < j" "j \<le> k"
   2.485 -  shows 
   2.486 -  "has_desc_fth p i k m r =
   2.487 -  (\<exists>n. (has_desc_fth p i j m n \<and> has_fth p j k n r)
   2.488 -  \<or> (has_fth p i j m n \<and> has_desc_fth p j k n r))" (is "?L = ?R")
   2.489 -proof 
   2.490 -  assume "?L"
   2.491 -  then obtain \<theta>
   2.492 -    where desc: "is_desc_fthread \<theta> p i k" 
   2.493 -    and [simp]: "\<theta> i = m" "\<theta> k = r"
   2.494 -    by (auto simp:has_desc_fth_def)
   2.495 -
   2.496 -  hence "is_fthread \<theta> p i k"
   2.497 -    by (simp add: desc_is_fthread)
   2.498 -  with range have fths: "is_fthread \<theta> p i j" "is_fthread \<theta> p j k"
   2.499 -    unfolding is_fthread_def
   2.500 -    by auto
   2.501 -  hence hfths: "has_fth p i j m (\<theta> j)" "has_fth p j k (\<theta> j) r"
   2.502 -    by (auto simp:has_fth_def)
   2.503 -
   2.504 -  from desc obtain l 
   2.505 -    where "i \<le> l" "l < k"
   2.506 -    and "descat p \<theta> l"
   2.507 -    by (auto simp:is_desc_fthread_def)
   2.508 -
   2.509 -  with fths
   2.510 -  have "is_desc_fthread \<theta> p i j \<or> is_desc_fthread \<theta> p j k"
   2.511 -    unfolding is_desc_fthread_def
   2.512 -    by (cases "l < j") auto
   2.513 -  hence "has_desc_fth p i j m (\<theta> j) \<or> has_desc_fth p j k (\<theta> j) r"
   2.514 -    by (auto simp:has_desc_fth_def)
   2.515 -  with hfths show ?R
   2.516 -    by auto
   2.517 -next
   2.518 -  assume "?R"
   2.519 -  then obtain n \<theta>1 \<theta>2
   2.520 -    where "(is_desc_fthread \<theta>1 p i j \<and> is_fthread \<theta>2 p j k)
   2.521 -    \<or> (is_fthread \<theta>1 p i j \<and> is_desc_fthread \<theta>2 p j k)"
   2.522 -    and [simp]: "\<theta>1 i = m" "\<theta>1 j = n" "\<theta>2 j = n" "\<theta>2 k = r"
   2.523 -    by (auto simp:has_fth_def has_desc_fth_def)
   2.524 -
   2.525 -  hence ths2: "is_fthread \<theta>1 p i j" "is_fthread \<theta>2 p j k"
   2.526 -    and dths: "is_desc_fthread \<theta>1 p i j \<or> is_desc_fthread \<theta>2 p j k"
   2.527 -    by (auto simp:desc_is_fthread)
   2.528 -
   2.529 -  let ?\<theta> = "(\<lambda>i. if i < j then \<theta>1 i else \<theta>2 i)"
   2.530 -  have "is_fthread ?\<theta> p i k"
   2.531 -    unfolding is_fthread_def
   2.532 -  proof
   2.533 -    fix l assume range: "l \<in> {i..<k}"
   2.534 -    
   2.535 -    show "eqlat p ?\<theta> l"
   2.536 -    proof (cases rule:three_cases)
   2.537 -      assume "Suc l < j"
   2.538 -      with ths2 range show ?thesis 
   2.539 -        unfolding is_fthread_def Ball_def
   2.540 -        by simp
   2.541 -    next
   2.542 -      assume "Suc l = j"
   2.543 -      hence "l < j" "\<theta>2 (Suc l) = \<theta>1 (Suc l)" by auto
   2.544 -      with ths2 range show ?thesis 
   2.545 -        unfolding is_fthread_def Ball_def
   2.546 -        by simp
   2.547 -    next
   2.548 -      assume "j \<le> l"
   2.549 -      with ths2 range show ?thesis 
   2.550 -        unfolding is_fthread_def Ball_def
   2.551 -        by simp
   2.552 -    qed arith
   2.553 -  qed
   2.554 -  moreover
   2.555 -  from dths
   2.556 -  have "\<exists>l. i \<le> l \<and> l < k \<and> descat p ?\<theta> l"
   2.557 -  proof
   2.558 -    assume "is_desc_fthread \<theta>1 p i j"
   2.559 -
   2.560 -    then obtain l where range: "i \<le> l" "l < j" and "descat p \<theta>1 l"
   2.561 -      unfolding is_desc_fthread_def Bex_def by auto
   2.562 -    hence "descat p ?\<theta> l" 
   2.563 -      by (cases "Suc l = j", auto)
   2.564 -    with `j \<le> k` and range show ?thesis 
   2.565 -      by (rule_tac x="l" in exI, auto)
   2.566 -  next
   2.567 -    assume "is_desc_fthread \<theta>2 p j k"
   2.568 -    then obtain l where range: "j \<le> l" "l < k" and "descat p \<theta>2 l"
   2.569 -      unfolding is_desc_fthread_def Bex_def by auto
   2.570 -    with `i < j` have "descat p ?\<theta> l" "i \<le> l"
   2.571 -      by auto
   2.572 -    with range show ?thesis 
   2.573 -      by (rule_tac x="l" in exI, auto)
   2.574 -  qed
   2.575 -  ultimately have "is_desc_fthread ?\<theta> p i k"
   2.576 -    by (simp add: is_desc_fthread_def Bex_def)
   2.577 -
   2.578 -  moreover 
   2.579 -  have "?\<theta> i = m" "?\<theta> k = r" using range by auto
   2.580 -
   2.581 -  ultimately show "has_desc_fth p i k m r" 
   2.582 -    by (auto simp:has_desc_fth_def)
   2.583 -qed 
   2.584 -
   2.585 -    
   2.586 -
   2.587 -lemma fth_single:
   2.588 -  "has_fth p i (Suc i) m n = eql (snd (p i)) m n" (is "?L = ?R")
   2.589 -proof 
   2.590 -  assume "?L" thus "?R"
   2.591 -    unfolding is_fthread_def Ball_def has_fth_def
   2.592 -    by auto
   2.593 -next
   2.594 -  let ?\<theta> = "\<lambda>k. if k = i then m else n"
   2.595 -  assume edge: "?R"
   2.596 -  hence "is_fthread ?\<theta> p i (Suc i) \<and> ?\<theta> i = m \<and> ?\<theta> (Suc i) = n"
   2.597 -    unfolding is_fthread_def Ball_def
   2.598 -    by auto
   2.599 -
   2.600 -  thus "?L"
   2.601 -    unfolding has_fth_def 
   2.602 -    by auto
   2.603 -qed
   2.604 -
   2.605 -lemma desc_fth_single:
   2.606 -  "has_desc_fth p i (Suc i) m n = 
   2.607 -  dsc (snd (p i)) m n" (is "?L = ?R")
   2.608 -proof 
   2.609 -  assume "?L" thus "?R"
   2.610 -    unfolding is_desc_fthread_def has_desc_fth_def is_fthread_def
   2.611 -    Bex_def 
   2.612 -    by (elim exE conjE) (case_tac "k = i", auto)
   2.613 -next
   2.614 -  let ?\<theta> = "\<lambda>k. if k = i then m else n"
   2.615 -  assume edge: "?R"
   2.616 -  hence "is_desc_fthread ?\<theta> p i (Suc i) \<and> ?\<theta> i = m \<and> ?\<theta> (Suc i) = n"
   2.617 -    unfolding is_desc_fthread_def is_fthread_def Ball_def Bex_def
   2.618 -    by auto
   2.619 -  thus "?L"
   2.620 -    unfolding has_desc_fth_def 
   2.621 -    by auto
   2.622 -qed
   2.623 -
   2.624 -lemma mk_eql: "(G \<turnstile> m \<leadsto>\<^bsup>e\<^esup> n) \<Longrightarrow> eql G m n"
   2.625 -  by (cases e, auto)
   2.626 -
   2.627 -lemma eql_scgcomp:
   2.628 -  "eql (G * H) m r =
   2.629 -  (\<exists>n. eql G m n \<and> eql H n r)" (is "?L = ?R")
   2.630 -proof
   2.631 -  show "?L \<Longrightarrow> ?R"
   2.632 -    by (auto simp:in_grcomp intro!:mk_eql)
   2.633 -
   2.634 -  assume "?R"
   2.635 -  then obtain n where l: "eql G m n" and r:"eql H n r" by auto
   2.636 -  thus ?L
   2.637 -    by (cases "dsc G m n") (auto simp:in_grcomp mult_sedge_def)
   2.638 -qed
   2.639 -
   2.640 -lemma desc_scgcomp:
   2.641 -  "dsc (G * H) m r =
   2.642 -  (\<exists>n. (dsc G m n \<and> eql H n r) \<or> (eqp G m n \<and> dsc H n r))" (is "?L = ?R")
   2.643 -proof
   2.644 -  show "?R \<Longrightarrow> ?L" by (auto simp:in_grcomp mult_sedge_def)
   2.645 -
   2.646 -  assume "?L"
   2.647 -  thus ?R
   2.648 -    by (auto simp:in_grcomp mult_sedge_def)
   2.649 -  (case_tac "e", auto, case_tac "e'", auto)
   2.650 -qed
   2.651 -
   2.652 -
   2.653 -lemma has_fth_unfold:
   2.654 -  assumes "i < j"
   2.655 -  shows "has_fth p i j m n = 
   2.656 -    (\<exists>r. has_fth p i (Suc i) m r \<and> has_fth p (Suc i) j r n)"
   2.657 -    by (rule combine_fthreads) (insert `i < j`, auto)
   2.658 -
   2.659 -lemma has_dfth_unfold:
   2.660 -  assumes range: "i < j"
   2.661 -  shows 
   2.662 -  "has_desc_fth p i j m r =
   2.663 -  (\<exists>n. (has_desc_fth p i (Suc i) m n \<and> has_fth p (Suc i) j n r)
   2.664 -  \<or> (has_fth p i (Suc i) m n \<and> has_desc_fth p (Suc i) j n r))"
   2.665 -  by (rule combine_dfthreads) (insert `i < j`, auto)
   2.666 -
   2.667 -
   2.668 -lemma Lemma7a:
   2.669 - "i \<le> j \<Longrightarrow> has_fth p i j m n = eql (prod (p\<langle>i,j\<rangle>)) m n"
   2.670 -proof (induct i arbitrary: m rule:inc_induct)
   2.671 -  case base show ?case
   2.672 -    unfolding has_fth_def is_fthread_def sub_path_def
   2.673 -    by (auto simp:in_grunit one_sedge_def)
   2.674 -next
   2.675 -  case (step i)
   2.676 -  note IH = `\<And>m. has_fth p (Suc i) j m n = 
   2.677 -  eql (prod (p\<langle>Suc i,j\<rangle>)) m n`
   2.678 -
   2.679 -  have "has_fth p i j m n 
   2.680 -    = (\<exists>r. has_fth p i (Suc i) m r \<and> has_fth p (Suc i) j r n)"
   2.681 -    by (rule has_fth_unfold[OF `i < j`])
   2.682 -  also have "\<dots> = (\<exists>r. has_fth p i (Suc i) m r 
   2.683 -    \<and> eql (prod (p\<langle>Suc i,j\<rangle>)) r n)"
   2.684 -    by (simp only:IH)
   2.685 -  also have "\<dots> = (\<exists>r. eql (snd (p i)) m r
   2.686 -    \<and> eql (prod (p\<langle>Suc i,j\<rangle>)) r n)"
   2.687 -    by (simp only:fth_single)
   2.688 -  also have "\<dots> = eql (snd (p i) * prod (p\<langle>Suc i,j\<rangle>)) m n"
   2.689 -    by (simp only:eql_scgcomp)
   2.690 -  also have "\<dots> = eql (prod (p\<langle>i,j\<rangle>)) m n"
   2.691 -    by (simp only:prod_unfold[OF `i < j`])
   2.692 -  finally show ?case .
   2.693 -qed
   2.694 -
   2.695 -
   2.696 -lemma Lemma7b:
   2.697 -assumes "i \<le> j"
   2.698 -shows
   2.699 -  "has_desc_fth p i j m n = 
   2.700 -  dsc (prod (p\<langle>i,j\<rangle>)) m n"
   2.701 -using prems
   2.702 -proof (induct i arbitrary: m rule:inc_induct)
   2.703 -  case base show ?case
   2.704 -    unfolding has_desc_fth_def is_desc_fthread_def sub_path_def 
   2.705 -    by (auto simp:in_grunit one_sedge_def)
   2.706 -next
   2.707 -  case (step i)
   2.708 -  thus ?case 
   2.709 -    by (simp only:prod_unfold desc_scgcomp desc_fth_single
   2.710 -    has_dfth_unfold fth_single Lemma7a) auto
   2.711 -qed
   2.712 -
   2.713 -
   2.714 -lemma descat_contract:
   2.715 -  assumes [simp]: "increasing s"
   2.716 -  shows
   2.717 -  "descat (contract s p) \<theta> i = 
   2.718 -  has_desc_fth p (s i) (s (Suc i)) (\<theta> i) (\<theta> (Suc i))"
   2.719 -  by (simp add:Lemma7b increasing_weak contract_def)
   2.720 -
   2.721 -lemma eqlat_contract:
   2.722 -  assumes [simp]: "increasing s"
   2.723 -  shows
   2.724 -  "eqlat (contract s p) \<theta> i = 
   2.725 -  has_fth p (s i) (s (Suc i)) (\<theta> i) (\<theta> (Suc i))"
   2.726 -  by (auto simp:Lemma7a increasing_weak contract_def)
   2.727 -
   2.728 -
   2.729 -subsubsection {* Connecting threads *}
   2.730 -
   2.731 -definition
   2.732 -  "connect s \<theta>s = (\<lambda>k. \<theta>s (section_of s k) k)"
   2.733 -
   2.734 -
   2.735 -lemma next_in_range:
   2.736 -  assumes [simp]: "increasing s"
   2.737 -  assumes a: "k \<in> section s i"
   2.738 -  shows "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))"
   2.739 -proof -
   2.740 -  from a have "k < s (Suc i)" by simp
   2.741 -  
   2.742 -  hence "Suc k < s (Suc i) \<or> Suc k = s (Suc i)" by arith
   2.743 -  thus ?thesis
   2.744 -  proof
   2.745 -    assume "Suc k < s (Suc i)"
   2.746 -    with a have "Suc k \<in> section s i" by simp
   2.747 -    thus ?thesis ..
   2.748 -  next
   2.749 -    assume eq: "Suc k = s (Suc i)"
   2.750 -    with increasing_strict have "Suc k < s (Suc (Suc i))" by simp
   2.751 -    with eq have "Suc k \<in> section s (Suc i)" by simp
   2.752 -    thus ?thesis ..
   2.753 -  qed
   2.754 -qed
   2.755 -
   2.756 -
   2.757 -lemma connect_threads:
   2.758 -  assumes [simp]: "increasing s"
   2.759 -  assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
   2.760 -  assumes fth: "is_fthread (\<theta>s i) p (s i) (s (Suc i))"
   2.761 -
   2.762 -  shows
   2.763 -  "is_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
   2.764 -  unfolding is_fthread_def
   2.765 -proof 
   2.766 -  fix k assume krng: "k \<in> section s i"
   2.767 -
   2.768 -  with fth have eqlat: "eqlat p (\<theta>s i) k" 
   2.769 -    unfolding is_fthread_def by simp
   2.770 -
   2.771 -  from krng and next_in_range 
   2.772 -  have "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))" 
   2.773 -    by simp
   2.774 -  thus "eqlat p (connect s \<theta>s) k"
   2.775 -  proof
   2.776 -    assume "Suc k \<in> section s i"
   2.777 -    with krng eqlat show ?thesis
   2.778 -      unfolding connect_def
   2.779 -      by (simp only:section_of_known `increasing s`)
   2.780 -  next
   2.781 -    assume skrng: "Suc k \<in> section s (Suc i)"
   2.782 -    with krng have "Suc k = s (Suc i)" by auto
   2.783 -
   2.784 -    with krng skrng eqlat show ?thesis
   2.785 -      unfolding connect_def
   2.786 -      by (simp only:section_of_known connected[symmetric] `increasing s`)
   2.787 -  qed
   2.788 -qed
   2.789 -
   2.790 -
   2.791 -lemma connect_dthreads:
   2.792 -  assumes inc[simp]: "increasing s"
   2.793 -  assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
   2.794 -  assumes fth: "is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
   2.795 -
   2.796 -  shows
   2.797 -  "is_desc_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
   2.798 -  unfolding is_desc_fthread_def
   2.799 -proof 
   2.800 -  show "is_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
   2.801 -    apply (rule connect_threads)
   2.802 -    apply (insert fth)
   2.803 -    by (auto simp:connected is_desc_fthread_def)
   2.804 -
   2.805 -  from fth
   2.806 -  obtain k where dsc: "descat p (\<theta>s i) k" and krng: "k \<in> section s i"
   2.807 -    unfolding is_desc_fthread_def by blast
   2.808 -  
   2.809 -  from krng and next_in_range 
   2.810 -  have "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))" 
   2.811 -    by simp
   2.812 -  hence "descat p (connect s \<theta>s) k"
   2.813 -  proof
   2.814 -    assume "Suc k \<in> section s i"
   2.815 -    with krng dsc show ?thesis unfolding connect_def
   2.816 -      by (simp only:section_of_known inc)
   2.817 -  next
   2.818 -    assume skrng: "Suc k \<in> section s (Suc i)"
   2.819 -    with krng have "Suc k = s (Suc i)" by auto
   2.820 -
   2.821 -    with krng skrng dsc show ?thesis unfolding connect_def
   2.822 -      by (simp only:section_of_known connected[symmetric] inc)
   2.823 -  qed
   2.824 -  with krng show "\<exists>k\<in>section s i. descat p (connect s \<theta>s) k" ..
   2.825 -qed
   2.826 -
   2.827 -lemma mk_inf_thread:
   2.828 -  assumes [simp]: "increasing s"
   2.829 -  assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))"
   2.830 -  shows "is_thread (s (Suc n)) \<theta> p"
   2.831 -  unfolding is_thread_def 
   2.832 -proof (intro allI impI)
   2.833 -  fix j assume st: "s (Suc n) \<le> j"
   2.834 -
   2.835 -  let ?k = "section_of s j"
   2.836 -  from in_section_of st
   2.837 -  have rs: "j \<in> section s ?k" by simp
   2.838 -
   2.839 -  with st have "s (Suc n) < s (Suc ?k)" by simp
   2.840 -  with increasing_bij have "n < ?k" by simp
   2.841 -  with rs and fths[of ?k]
   2.842 -  show "eqlat p \<theta> j" by (simp add:is_fthread_def)
   2.843 -qed
   2.844 -
   2.845 -
   2.846 -lemma mk_inf_desc_thread:
   2.847 -  assumes [simp]: "increasing s"
   2.848 -  assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))"
   2.849 -  assumes fdths: "\<exists>\<^sub>\<infinity>i. is_desc_fthread \<theta> p (s i) (s (Suc i))"
   2.850 -  shows "is_desc_thread \<theta> p"
   2.851 -  unfolding is_desc_thread_def 
   2.852 -proof (intro exI conjI)
   2.853 -
   2.854 -  from mk_inf_thread[of s n \<theta> p] fths
   2.855 -  show "\<forall>i\<ge>s (Suc n). eqlat p \<theta> i" 
   2.856 -    by (fold is_thread_def) simp
   2.857 -
   2.858 -  show "\<exists>\<^sub>\<infinity>l. descat p \<theta> l"
   2.859 -    unfolding INFM_nat
   2.860 -  proof
   2.861 -    fix i 
   2.862 -    
   2.863 -    let ?k = "section_of s i"
   2.864 -    from fdths obtain j
   2.865 -      where "?k < j" "is_desc_fthread \<theta> p (s j) (s (Suc j))"
   2.866 -      unfolding INFM_nat by auto
   2.867 -    then obtain l where "s j \<le> l" and desc: "descat p \<theta> l"
   2.868 -      unfolding is_desc_fthread_def
   2.869 -      by auto
   2.870 -
   2.871 -    have "i < s (Suc ?k)" by (rule section_of2) simp
   2.872 -    also have "\<dots> \<le> s j"
   2.873 -      by (rule increasing_weak [OF `increasing s`]) (insert `?k < j`, arith)
   2.874 -    also note `\<dots> \<le> l`
   2.875 -    finally have "i < l" .
   2.876 -    with desc
   2.877 -    show "\<exists>l. i < l \<and> descat p \<theta> l" by blast
   2.878 -  qed
   2.879 -qed
   2.880 -
   2.881 -
   2.882 -lemma desc_ex_choice:
   2.883 -  assumes A: "((\<exists>n.\<forall>i\<ge>n. \<exists>x. P x i) \<and> (\<exists>\<^sub>\<infinity>i. \<exists>x. Q x i))"
   2.884 -  and imp: "\<And>x i. Q x i \<Longrightarrow> P x i"
   2.885 -  shows "\<exists>xs. ((\<exists>n.\<forall>i\<ge>n. P (xs i) i) \<and> (\<exists>\<^sub>\<infinity>i. Q (xs i) i))"
   2.886 -  (is "\<exists>xs. ?Ps xs \<and> ?Qs xs")
   2.887 -proof
   2.888 -  let ?w = "\<lambda>i. (if (\<exists>x. Q x i) then (SOME x. Q x i)
   2.889 -                                 else (SOME x. P x i))"
   2.890 -
   2.891 -  from A
   2.892 -  obtain n where P: "\<And>i. n \<le> i \<Longrightarrow> \<exists>x. P x i"
   2.893 -    by auto
   2.894 -  {
   2.895 -    fix i::'a assume "n \<le> i"
   2.896 -
   2.897 -    have "P (?w i) i"
   2.898 -    proof (cases "\<exists>x. Q x i")
   2.899 -      case True
   2.900 -      hence "Q (?w i) i" by (auto intro:someI)
   2.901 -      with imp show "P (?w i) i" .
   2.902 -    next
   2.903 -      case False
   2.904 -      with P[OF `n \<le> i`] show "P (?w i) i" 
   2.905 -        by (auto intro:someI)
   2.906 -    qed
   2.907 -  }
   2.908 -
   2.909 -  hence "?Ps ?w" by (rule_tac x=n in exI) auto
   2.910 -
   2.911 -  moreover
   2.912 -  from A have "\<exists>\<^sub>\<infinity>i. (\<exists>x. Q x i)" ..
   2.913 -  hence "?Qs ?w" by (rule INFM_mono) (auto intro:someI)
   2.914 -  ultimately
   2.915 -  show "?Ps ?w \<and> ?Qs ?w" ..
   2.916 -qed
   2.917 -
   2.918 -
   2.919 -
   2.920 -lemma dthreads_join:
   2.921 -  assumes [simp]: "increasing s"
   2.922 -  assumes dthread: "is_desc_thread \<theta> (contract s p)"
   2.923 -  shows "\<exists>\<theta>s. desc (\<lambda>i. is_fthread (\<theta>s i) p (s i) (s (Suc i))
   2.924 -                           \<and> \<theta>s i (s i) = \<theta> i 
   2.925 -                           \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))
   2.926 -                   (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))
   2.927 -                           \<and> \<theta>s i (s i) = \<theta> i 
   2.928 -                           \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))"
   2.929 -    apply (rule desc_ex_choice)
   2.930 -    apply (insert dthread)
   2.931 -    apply (simp only:is_desc_thread_def)
   2.932 -    apply (simp add:eqlat_contract)
   2.933 -    apply (simp add:descat_contract)
   2.934 -    apply (simp only:has_fth_def has_desc_fth_def)
   2.935 -    by (auto simp:is_desc_fthread_def)
   2.936 -
   2.937 -
   2.938 -
   2.939 -lemma INFM_drop_prefix:
   2.940 -  "(\<exists>\<^sub>\<infinity>i::nat. i > n \<and> P i) = (\<exists>\<^sub>\<infinity>i. P i)"
   2.941 -  apply (auto simp:INFM_nat)
   2.942 -  apply (drule_tac x = "max m n" in spec)
   2.943 -  apply (elim exE conjE)
   2.944 -  apply (rule_tac x = "na" in exI)
   2.945 -  by auto
   2.946 -
   2.947 -
   2.948 -
   2.949 -lemma contract_keeps_threads:
   2.950 -  assumes inc[simp]: "increasing s"
   2.951 -  shows "(\<exists>\<theta>. is_desc_thread \<theta> p) 
   2.952 -  \<longleftrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> (contract s p))"
   2.953 -  (is "?A \<longleftrightarrow> ?B")
   2.954 -proof 
   2.955 -  assume "?A"
   2.956 -  then obtain \<theta> n 
   2.957 -    where fr: "\<forall>i\<ge>n. eqlat p \<theta> i" 
   2.958 -      and ds: "\<exists>\<^sub>\<infinity>i. descat p \<theta> i"
   2.959 -    unfolding is_desc_thread_def 
   2.960 -    by auto
   2.961 -
   2.962 -  let ?c\<theta> = "\<lambda>i. \<theta> (s i)"
   2.963 -
   2.964 -  have "is_desc_thread ?c\<theta> (contract s p)"
   2.965 -    unfolding is_desc_thread_def
   2.966 -  proof (intro exI conjI)
   2.967 -    
   2.968 -    show "\<forall>i\<ge>n. eqlat (contract s p) ?c\<theta> i"
   2.969 -    proof (intro allI impI)
   2.970 -      fix i assume "n \<le> i"
   2.971 -      also have "i \<le> s i" 
   2.972 -        using increasing_inc by auto
   2.973 -      finally have "n \<le> s i" .
   2.974 -
   2.975 -      with fr have "is_fthread \<theta> p (s i) (s (Suc i))"
   2.976 -        unfolding is_fthread_def by auto
   2.977 -      hence "has_fth p (s i) (s (Suc i)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
   2.978 -        unfolding has_fth_def by auto
   2.979 -      with less_imp_le[OF increasing_strict]
   2.980 -      have "eql (prod (p\<langle>s i,s (Suc i)\<rangle>)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
   2.981 -        by (simp add:Lemma7a)
   2.982 -      thus "eqlat (contract s p) ?c\<theta> i" unfolding contract_def
   2.983 -        by auto
   2.984 -    qed
   2.985 -
   2.986 -    show "\<exists>\<^sub>\<infinity>i. descat (contract s p) ?c\<theta> i"
   2.987 -      unfolding INFM_nat 
   2.988 -    proof 
   2.989 -      fix i
   2.990 -
   2.991 -      let ?K = "section_of s (max (s (Suc i)) n)"
   2.992 -      from `\<exists>\<^sub>\<infinity>i. descat p \<theta> i` obtain j
   2.993 -          where "s (Suc ?K) < j" "descat p \<theta> j"
   2.994 -        unfolding INFM_nat by blast
   2.995 -      
   2.996 -      let ?L = "section_of s j"
   2.997 -      {
   2.998 -        fix x assume r: "x \<in> section s ?L"
   2.999 -        
  2.1000 -        have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2) simp
  2.1001 -        note `s (Suc ?K) < j`
  2.1002 -        also have "j < s (Suc ?L)"
  2.1003 -          by (rule section_of2) simp
  2.1004 -        finally have "Suc ?K \<le> ?L"
  2.1005 -          by (simp add:increasing_bij)          
  2.1006 -        with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
  2.1007 -        with e1 r have "max (s (Suc i)) n < x" by simp
  2.1008 -        
  2.1009 -        hence "(s (Suc i)) < x" "n < x" by auto
  2.1010 -      }
  2.1011 -      note range_est = this
  2.1012 -      
  2.1013 -      have "is_desc_fthread \<theta> p (s ?L) (s (Suc ?L))"
  2.1014 -        unfolding is_desc_fthread_def is_fthread_def
  2.1015 -      proof
  2.1016 -        show "\<forall>m\<in>section s ?L. eqlat p \<theta> m"
  2.1017 -        proof 
  2.1018 -          fix m assume "m\<in>section s ?L"
  2.1019 -          with range_est(2) have "n < m" . 
  2.1020 -          with fr show "eqlat p \<theta> m" by simp
  2.1021 -        qed
  2.1022 -
  2.1023 -        from in_section_of inc less_imp_le[OF `s (Suc ?K) < j`]
  2.1024 -        have "j \<in> section s ?L" .
  2.1025 -
  2.1026 -        with `descat p \<theta> j`
  2.1027 -        show "\<exists>m\<in>section s ?L. descat p \<theta> m" ..
  2.1028 -      qed
  2.1029 -      
  2.1030 -      with less_imp_le[OF increasing_strict]
  2.1031 -      have a: "descat (contract s p) ?c\<theta> ?L"
  2.1032 -        unfolding contract_def Lemma7b[symmetric]
  2.1033 -        by (auto simp:Lemma7b[symmetric] has_desc_fth_def)
  2.1034 -      
  2.1035 -      have "i < ?L"
  2.1036 -      proof (rule classical)
  2.1037 -        assume "\<not> i < ?L" 
  2.1038 -        hence "s ?L < s (Suc i)" 
  2.1039 -          by (simp add:increasing_bij)
  2.1040 -        also have "\<dots> < s ?L"
  2.1041 -          by (rule range_est(1)) (simp add:increasing_strict)
  2.1042 -        finally show ?thesis .
  2.1043 -      qed
  2.1044 -      with a show "\<exists>l. i < l \<and> descat (contract s p) ?c\<theta> l"
  2.1045 -        by blast
  2.1046 -    qed
  2.1047 -  qed
  2.1048 -  with exI show "?B" .
  2.1049 -next
  2.1050 -  assume "?B"
  2.1051 -  then obtain \<theta> 
  2.1052 -    where dthread: "is_desc_thread \<theta> (contract s p)" ..
  2.1053 -
  2.1054 -  with dthreads_join inc 
  2.1055 -  obtain \<theta>s where ths_spec:
  2.1056 -    "desc (\<lambda>i. is_fthread (\<theta>s i) p (s i) (s (Suc i))
  2.1057 -                  \<and> \<theta>s i (s i) = \<theta> i 
  2.1058 -                  \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))
  2.1059 -          (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))
  2.1060 -                  \<and> \<theta>s i (s i) = \<theta> i 
  2.1061 -                  \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))" 
  2.1062 -      (is "desc ?alw ?inf") 
  2.1063 -    by blast
  2.1064 -
  2.1065 -  then obtain n where fr: "\<forall>i\<ge>n. ?alw i" by blast
  2.1066 -  hence connected: "\<And>i. n < i \<Longrightarrow> \<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
  2.1067 -    by auto
  2.1068 -  
  2.1069 -  let ?j\<theta> = "connect s \<theta>s"
  2.1070 -  
  2.1071 -  from fr ths_spec have ths_spec2:
  2.1072 -      "\<And>i. i > n \<Longrightarrow> is_fthread (\<theta>s i) p (s i) (s (Suc i))"
  2.1073 -      "\<exists>\<^sub>\<infinity>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
  2.1074 -    by (auto intro:INFM_mono)
  2.1075 -  
  2.1076 -  have p1: "\<And>i. i > n \<Longrightarrow> is_fthread ?j\<theta> p (s i) (s (Suc i))"
  2.1077 -    by (rule connect_threads) (auto simp:connected ths_spec2)
  2.1078 -  
  2.1079 -  from ths_spec2(2)
  2.1080 -  have "\<exists>\<^sub>\<infinity>i. n < i \<and> is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
  2.1081 -    unfolding INFM_drop_prefix .
  2.1082 -  
  2.1083 -  hence p2: "\<exists>\<^sub>\<infinity>i. is_desc_fthread ?j\<theta> p (s i) (s (Suc i))"
  2.1084 -    apply (rule INFM_mono)
  2.1085 -    apply (rule connect_dthreads)
  2.1086 -    by (auto simp:connected)
  2.1087 -  
  2.1088 -  with `increasing s` p1
  2.1089 -  have "is_desc_thread ?j\<theta> p" 
  2.1090 -    by (rule mk_inf_desc_thread)
  2.1091 -  with exI show "?A" .
  2.1092 -qed
  2.1093 -
  2.1094 -
  2.1095 -lemma repeated_edge:
  2.1096 -  assumes "\<And>i. i > n \<Longrightarrow> dsc (snd (p i)) k k"
  2.1097 -  shows "is_desc_thread (\<lambda>i. k) p"
  2.1098 -proof-
  2.1099 -  have th: "\<forall> m. \<exists>na>m. n < na" by arith
  2.1100 -  show ?thesis using prems
  2.1101 -  unfolding is_desc_thread_def 
  2.1102 -  apply (auto)
  2.1103 -  apply (rule_tac x="Suc n" in exI, auto)
  2.1104 -  apply (rule INFM_mono[where P="\<lambda>i. n < i"])
  2.1105 -  apply (simp only:INFM_nat)
  2.1106 -  by (auto simp add: th)
  2.1107 -qed
  2.1108 -
  2.1109 -lemma fin_from_inf:
  2.1110 -  assumes "is_thread n \<theta> p"
  2.1111 -  assumes "n < i"
  2.1112 -  assumes "i < j"
  2.1113 -  shows "is_fthread \<theta> p i j"
  2.1114 -  using prems
  2.1115 -  unfolding is_thread_def is_fthread_def 
  2.1116 -  by auto
  2.1117 -
  2.1118 -
  2.1119 -subsection {* Ramsey's Theorem *}
  2.1120 -
  2.1121 -definition 
  2.1122 -  "set2pair S = (THE (x,y). x < y \<and> S = {x,y})"
  2.1123 -
  2.1124 -lemma set2pair_conv: 
  2.1125 -  fixes x y :: nat
  2.1126 -  assumes "x < y"
  2.1127 -  shows "set2pair {x, y} = (x, y)"
  2.1128 -  unfolding set2pair_def
  2.1129 -proof (rule the_equality, simp_all only:split_conv split_paired_all)
  2.1130 -  from `x < y` show "x < y \<and> {x,y}={x,y}" by simp
  2.1131 -next
  2.1132 -  fix a b
  2.1133 -  assume a: "a < b \<and> {x, y} = {a, b}"
  2.1134 -  hence "{a, b} = {x, y}" by simp_all
  2.1135 -  hence "(a, b) = (x, y) \<or> (a, b) = (y, x)" 
  2.1136 -    by (cases "x = y") auto
  2.1137 -  thus "(a, b) = (x, y)"
  2.1138 -  proof 
  2.1139 -    assume "(a, b) = (y, x)"
  2.1140 -    with a and `x < y`
  2.1141 -    show ?thesis by auto (* contradiction *)
  2.1142 -  qed
  2.1143 -qed  
  2.1144 -
  2.1145 -definition 
  2.1146 -  "set2list = inv set"
  2.1147 -
  2.1148 -lemma finite_set2list: 
  2.1149 -  assumes "finite S" 
  2.1150 -  shows "set (set2list S) = S"
  2.1151 -  unfolding set2list_def 
  2.1152 -proof (rule f_inv_into_f)
  2.1153 -  from `finite S` have "\<exists>l. set l = S"
  2.1154 -    by (rule finite_list)
  2.1155 -  thus "S \<in> range set"
  2.1156 -    unfolding image_def
  2.1157 -    by auto
  2.1158 -qed
  2.1159 -
  2.1160 -
  2.1161 -corollary RamseyNatpairs:
  2.1162 -  fixes S :: "'a set"
  2.1163 -    and f :: "nat \<times> nat \<Rightarrow> 'a"
  2.1164 -
  2.1165 -  assumes "finite S"
  2.1166 -  and inS: "\<And>x y. x < y \<Longrightarrow> f (x, y) \<in> S"
  2.1167 -
  2.1168 -  obtains T :: "nat set" and s :: "'a"
  2.1169 -  where "infinite T"
  2.1170 -    and "s \<in> S"
  2.1171 -    and "\<And>x y. \<lbrakk>x \<in> T; y \<in> T; x < y\<rbrakk> \<Longrightarrow> f (x, y) = s"
  2.1172 -proof -
  2.1173 -  from `finite S`
  2.1174 -  have "set (set2list S) = S" by (rule finite_set2list)
  2.1175 -  then 
  2.1176 -  obtain l where S: "S = set l" by auto
  2.1177 -  also from set_conv_nth have "\<dots> = {l ! i |i. i < length l}" .
  2.1178 -  finally have "S = {l ! i |i. i < length l}" .
  2.1179 -
  2.1180 -  let ?s = "length l"
  2.1181 -
  2.1182 -  from inS 
  2.1183 -  have index_less: "\<And>x y. x \<noteq> y \<Longrightarrow> index_of l (f (set2pair {x, y})) < ?s"
  2.1184 -  proof -
  2.1185 -    fix x y :: nat
  2.1186 -    assume neq: "x \<noteq> y"
  2.1187 -    have "f (set2pair {x, y}) \<in> S"
  2.1188 -    proof (cases "x < y")
  2.1189 -      case True hence "set2pair {x, y} = (x, y)"
  2.1190 -        by (rule set2pair_conv)
  2.1191 -      with True inS
  2.1192 -      show ?thesis by simp
  2.1193 -    next
  2.1194 -      case False 
  2.1195 -      with neq have y_less: "y < x" by simp
  2.1196 -      have x:"{x,y} = {y,x}" by auto
  2.1197 -      with y_less have "set2pair {x, y} = (y, x)"
  2.1198 -        by (simp add:set2pair_conv)
  2.1199 -      with y_less inS
  2.1200 -      show ?thesis by simp
  2.1201 -    qed
  2.1202 -
  2.1203 -    thus "index_of l (f (set2pair {x, y})) < length l"
  2.1204 -      by (simp add: S index_of_length)
  2.1205 -  qed
  2.1206 -
  2.1207 -  have "\<exists>Y. infinite Y \<and>
  2.1208 -    (\<exists>t. t < ?s \<and>
  2.1209 -         (\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow>
  2.1210 -                      index_of l (f (set2pair {x, y})) = t))"
  2.1211 -    by (rule Ramsey2[of "UNIV::nat set", simplified])
  2.1212 -       (auto simp:index_less)
  2.1213 -  then obtain T i
  2.1214 -    where inf: "infinite T"
  2.1215 -    and i: "i < length l"
  2.1216 -    and d: "\<And>x y. \<lbrakk>x \<in> T; y\<in>T; x \<noteq> y\<rbrakk>
  2.1217 -    \<Longrightarrow> index_of l (f (set2pair {x, y})) = i"
  2.1218 -    by auto
  2.1219 -
  2.1220 -  have "l ! i \<in> S" unfolding S using i
  2.1221 -    by (rule nth_mem)
  2.1222 -  moreover
  2.1223 -  have "\<And>x y. x \<in> T \<Longrightarrow> y\<in>T \<Longrightarrow> x < y
  2.1224 -    \<Longrightarrow> f (x, y) = l ! i"
  2.1225 -  proof -
  2.1226 -    fix x y assume "x \<in> T" "y \<in> T" "x < y"
  2.1227 -    with d have 
  2.1228 -      "index_of l (f (set2pair {x, y})) = i" by auto
  2.1229 -    with `x < y`
  2.1230 -    have "i = index_of l (f (x, y))" 
  2.1231 -      by (simp add:set2pair_conv)
  2.1232 -    with `i < length l`
  2.1233 -    show "f (x, y) = l ! i" 
  2.1234 -      by (auto intro:index_of_member[symmetric] iff:index_of_length)
  2.1235 -  qed
  2.1236 -  moreover note inf
  2.1237 -  ultimately
  2.1238 -  show ?thesis using prems
  2.1239 -    by blast
  2.1240 -qed
  2.1241 -
  2.1242 -
  2.1243 -subsection {* Main Result *}
  2.1244 -
  2.1245 -
  2.1246 -theorem LJA_Theorem4: 
  2.1247 -  assumes "finite_acg A"
  2.1248 -  shows "SCT A \<longleftrightarrow> SCT' A"
  2.1249 -proof
  2.1250 -  assume "SCT A"
  2.1251 -  
  2.1252 -  show "SCT' A"
  2.1253 -  proof (rule classical)
  2.1254 -    assume "\<not> SCT' A"
  2.1255 -    
  2.1256 -    then obtain n G
  2.1257 -      where in_closure: "(tcl A) \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
  2.1258 -      and idemp: "G * G = G"
  2.1259 -      and no_strict_arc: "\<forall>p. \<not>(G \<turnstile> p \<leadsto>\<^bsup>\<down>\<^esup> p)"
  2.1260 -      unfolding SCT'_def no_bad_graphs_def by auto
  2.1261 -    
  2.1262 -    from in_closure obtain k
  2.1263 -      where k_pow: "A ^ k \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
  2.1264 -      and "0 < k"
  2.1265 -      unfolding in_tcl by auto
  2.1266 -        
  2.1267 -    from power_induces_path k_pow
  2.1268 -    obtain loop where loop_props:
  2.1269 -      "has_fpath A loop"
  2.1270 -      "n = fst loop" "n = end_node loop"
  2.1271 -      "G = prod loop" "k = length (snd loop)" . 
  2.1272 -
  2.1273 -    with `0 < k` and path_loop_graph
  2.1274 -    have "has_ipath A (omega loop)" by blast
  2.1275 -    with `SCT A` 
  2.1276 -    have thread: "\<exists>\<theta>. is_desc_thread \<theta> (omega loop)" by (auto simp:SCT_def)
  2.1277 -
  2.1278 -    let ?s = "\<lambda>i. k * i"
  2.1279 -    let ?cp = "\<lambda>i::nat. (n, G)"
  2.1280 -
  2.1281 -    from loop_props have "fst loop = end_node loop" by auto
  2.1282 -    with `0 < k` `k = length (snd loop)`
  2.1283 -    have "\<And>i. (omega loop)\<langle>?s i,?s (Suc i)\<rangle> = loop"
  2.1284 -      by (rule sub_path_loop)
  2.1285 -
  2.1286 -    with `n = fst loop` `G = prod loop` `k = length (snd loop)`
  2.1287 -    have a: "contract ?s (omega loop) = ?cp"
  2.1288 -      unfolding contract_def
  2.1289 -      by (simp add:path_loop_def split_def fst_p0)
  2.1290 -
  2.1291 -    from `0 < k` have "increasing ?s"
  2.1292 -      by (auto simp:increasing_def)
  2.1293 -    with thread have "\<exists>\<theta>. is_desc_thread \<theta> ?cp"
  2.1294 -      unfolding a[symmetric] 
  2.1295 -      by (unfold contract_keeps_threads[symmetric])
  2.1296 -
  2.1297 -    then obtain \<theta> where desc: "is_desc_thread \<theta> ?cp" by auto
  2.1298 -
  2.1299 -    then obtain n where thr: "is_thread n \<theta> ?cp" 
  2.1300 -      unfolding is_desc_thread_def is_thread_def 
  2.1301 -      by auto
  2.1302 -
  2.1303 -    have "finite (range \<theta>)"
  2.1304 -    proof (rule finite_range_ignore_prefix)
  2.1305 -      
  2.1306 -      from `finite_acg A`
  2.1307 -      have "finite_acg (tcl A)" by (simp add:finite_tcl)
  2.1308 -      with in_closure have "finite_graph G" 
  2.1309 -        unfolding finite_acg_def all_finite_def by blast
  2.1310 -      thus "finite (nodes G)" by (rule finite_nodes)
  2.1311 -
  2.1312 -      from thread_image_nodes[OF thr]
  2.1313 -      show "\<forall>i\<ge>n. \<theta> i \<in> nodes G" by simp
  2.1314 -    qed
  2.1315 -    with finite_range
  2.1316 -    obtain p where inf_visit: "\<exists>\<^sub>\<infinity>i. \<theta> i = p" by auto
  2.1317 -
  2.1318 -    then obtain i where "n < i" "\<theta> i = p" 
  2.1319 -      by (auto simp:INFM_nat)
  2.1320 -
  2.1321 -    from desc
  2.1322 -    have "\<exists>\<^sub>\<infinity>i. descat ?cp \<theta> i"
  2.1323 -      unfolding is_desc_thread_def by auto
  2.1324 -    then obtain j 
  2.1325 -      where "i < j" and "descat ?cp \<theta> j"
  2.1326 -      unfolding INFM_nat by auto
  2.1327 -    from inf_visit obtain k where "j < k" "\<theta> k = p"
  2.1328 -      by (auto simp:INFM_nat)
  2.1329 -
  2.1330 -    from `i < j` `j < k` `n < i` thr 
  2.1331 -      fin_from_inf[of n \<theta> ?cp]
  2.1332 -      `descat ?cp \<theta> j`
  2.1333 -    have "is_desc_fthread \<theta> ?cp i k"
  2.1334 -      unfolding is_desc_fthread_def
  2.1335 -      by auto
  2.1336 -
  2.1337 -    with `\<theta> k = p` `\<theta> i = p`
  2.1338 -    have dfth: "has_desc_fth ?cp i k p p"
  2.1339 -      unfolding has_desc_fth_def
  2.1340 -      by auto
  2.1341 -
  2.1342 -    from `i < j` `j < k` have "i < k" by auto
  2.1343 -    hence "prod (?cp\<langle>i, k\<rangle>) = G"
  2.1344 -    proof (induct i rule:strict_inc_induct)
  2.1345 -      case base thus ?case by (simp add:sub_path_def)
  2.1346 -    next
  2.1347 -      case (step i) thus ?case
  2.1348 -        by (simp add:sub_path_def upt_rec[of i k] idemp)
  2.1349 -    qed
  2.1350 -
  2.1351 -    with `i < j` `j < k` dfth Lemma7b[of i k ?cp p p]
  2.1352 -    have "dsc G p p" by auto
  2.1353 -    with no_strict_arc have False by auto
  2.1354 -    thus ?thesis ..
  2.1355 -  qed
  2.1356 -next
  2.1357 -  assume "SCT' A"
  2.1358 -
  2.1359 -  show "SCT A"
  2.1360 -  proof (rule classical)
  2.1361 -    assume "\<not> SCT A"
  2.1362 -
  2.1363 -    with SCT_def
  2.1364 -    obtain p 
  2.1365 -      where ipath: "has_ipath A p"
  2.1366 -      and no_desc_th: "\<not> (\<exists>\<theta>. is_desc_thread \<theta> p)"
  2.1367 -      by blast
  2.1368 -
  2.1369 -    from `finite_acg A`
  2.1370 -    have "finite_acg (tcl A)" by (simp add: finite_tcl)
  2.1371 -    hence "finite (dest_graph (tcl A))" (is "finite ?AG")
  2.1372 -      by (simp add: finite_acg_def finite_graph_def)
  2.1373 -
  2.1374 -    from pdesc_acgplus[OF ipath]
  2.1375 -    have a: "\<And>x y. x<y \<Longrightarrow> pdesc p\<langle>x,y\<rangle> \<in> dest_graph (tcl A)"
  2.1376 -      unfolding has_edge_def .
  2.1377 -      
  2.1378 -    obtain S G
  2.1379 -      where "infinite S" "G \<in> dest_graph (tcl A)" 
  2.1380 -      and all_G: "\<And>x y. \<lbrakk> x \<in> S; y \<in> S; x < y\<rbrakk> \<Longrightarrow> 
  2.1381 -      pdesc (p\<langle>x,y\<rangle>) = G"
  2.1382 -      apply (rule RamseyNatpairs[of ?AG "\<lambda>(x,y). pdesc p\<langle>x, y\<rangle>"])
  2.1383 -      apply (rule `finite ?AG`)
  2.1384 -      by (simp only:split_conv, rule a, auto)
  2.1385 -
  2.1386 -    obtain n H m where
  2.1387 -      G_struct: "G = (n, H, m)" by (cases G)
  2.1388 -
  2.1389 -    let ?s = "enumerate S"
  2.1390 -    let ?q = "contract ?s p"
  2.1391 -
  2.1392 -    note all_in_S[simp] = enumerate_in_set[OF `infinite S`]
  2.1393 -        from `infinite S` 
  2.1394 -    have inc[simp]: "increasing ?s" 
  2.1395 -      unfolding increasing_def by (simp add:enumerate_mono)
  2.1396 -    note increasing_bij[OF this, simp]
  2.1397 -      
  2.1398 -    from ipath_contract inc ipath
  2.1399 -    have "has_ipath (tcl A) ?q" .
  2.1400 -
  2.1401 -    from all_G G_struct 
  2.1402 -    have all_H: "\<And>i. (snd (?q i)) = H"
  2.1403 -          unfolding contract_def 
  2.1404 -      by simp
  2.1405 -    
  2.1406 -    have loop: "(tcl A) \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
  2.1407 -      and idemp: "H * H = H"
  2.1408 -    proof - 
  2.1409 -      let ?i = "?s 0" and ?j = "?s (Suc 0)" and ?k = "?s (Suc (Suc 0))"
  2.1410 -      
  2.1411 -      have "pdesc (p\<langle>?i,?j\<rangle>) = G"
  2.1412 -                and "pdesc (p\<langle>?j,?k\<rangle>) = G"
  2.1413 -                and "pdesc (p\<langle>?i,?k\<rangle>) = G"
  2.1414 -                using all_G 
  2.1415 -                by auto
  2.1416 -          
  2.1417 -      with G_struct 
  2.1418 -      have "m = end_node (p\<langle>?i,?j\<rangle>)"
  2.1419 -                                "n = fst (p\<langle>?j,?k\<rangle>)"
  2.1420 -                                and Hs: "prod (p\<langle>?i,?j\<rangle>) = H"
  2.1421 -                                "prod (p\<langle>?j,?k\<rangle>) = H"
  2.1422 -                                "prod (p\<langle>?i,?k\<rangle>) = H"
  2.1423 -                by auto
  2.1424 -                        
  2.1425 -      hence "m = n" by simp
  2.1426 -      thus "tcl A \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
  2.1427 -                using G_struct `G \<in> dest_graph (tcl A)`
  2.1428 -                by (simp add:has_edge_def)
  2.1429 -          
  2.1430 -      from sub_path_prod[of ?i ?j ?k p]      
  2.1431 -      show "H * H = H"
  2.1432 -                unfolding Hs by simp
  2.1433 -    qed
  2.1434 -    moreover have "\<And>k. \<not>dsc H k k"
  2.1435 -    proof
  2.1436 -      fix k :: 'a assume "dsc H k k"
  2.1437 -      
  2.1438 -      with all_H repeated_edge
  2.1439 -      have "\<exists>\<theta>. is_desc_thread \<theta> ?q" by fast
  2.1440 -          with inc have "\<exists>\<theta>. is_desc_thread \<theta> p"
  2.1441 -                by (subst contract_keeps_threads) 
  2.1442 -      with no_desc_th
  2.1443 -      show False ..
  2.1444 -    qed
  2.1445 -    ultimately 
  2.1446 -    have False
  2.1447 -      using `SCT' A`[unfolded SCT'_def no_bad_graphs_def]
  2.1448 -      by blast
  2.1449 -    thus ?thesis ..
  2.1450 -  qed
  2.1451 -qed
  2.1452 -
  2.1453 -end
     3.1 --- a/src/HOL/SizeChange/Criterion.thy	Fri Nov 06 13:36:46 2009 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,111 +0,0 @@
     3.4 -(*  Title:      HOL/Library/SCT_Definition.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Alexander Krauss, TU Muenchen
     3.7 -*)
     3.8 -
     3.9 -header {* The Size-Change Principle (Definition) *}
    3.10 -
    3.11 -theory Criterion
    3.12 -imports Graphs Infinite_Set
    3.13 -begin
    3.14 -
    3.15 -subsection {* Size-Change Graphs *}
    3.16 -
    3.17 -datatype sedge =
    3.18 -    LESS ("\<down>")
    3.19 -  | LEQ ("\<Down>")
    3.20 -
    3.21 -instantiation sedge :: comm_monoid_mult
    3.22 -begin
    3.23 -
    3.24 -definition
    3.25 -  one_sedge_def: "1 = \<Down>"
    3.26 -
    3.27 -definition
    3.28 -  mult_sedge_def:" a * b = (if a = \<down> then \<down> else b)"
    3.29 -
    3.30 -instance  proof
    3.31 -  fix a b c :: sedge
    3.32 -  show "a * b * c = a * (b * c)" by (simp add:mult_sedge_def)
    3.33 -  show "1 * a = a" by (simp add:mult_sedge_def one_sedge_def)
    3.34 -  show "a * b = b * a" unfolding mult_sedge_def
    3.35 -    by (cases a, simp) (cases b, auto)
    3.36 -qed
    3.37 -
    3.38 -end
    3.39 -
    3.40 -lemma sedge_UNIV:
    3.41 -  "UNIV = { LESS, LEQ }"
    3.42 -proof (intro equalityI subsetI)
    3.43 -  fix x show "x \<in> { LESS, LEQ }"
    3.44 -    by (cases x) auto
    3.45 -qed auto
    3.46 -
    3.47 -instance sedge :: finite
    3.48 -proof
    3.49 -  show "finite (UNIV::sedge set)"
    3.50 -  by (simp add: sedge_UNIV)
    3.51 -qed
    3.52 -
    3.53 -
    3.54 -
    3.55 -types 'a scg = "('a, sedge) graph"
    3.56 -types 'a acg = "('a, 'a scg) graph"
    3.57 -
    3.58 -
    3.59 -subsection {* Size-Change Termination *}
    3.60 -
    3.61 -abbreviation (input)
    3.62 -  "desc P Q == ((\<exists>n.\<forall>i\<ge>n. P i) \<and> (\<exists>\<^sub>\<infinity>i. Q i))"
    3.63 -
    3.64 -abbreviation (input)
    3.65 -  "dsc G i j \<equiv> has_edge G i LESS j"
    3.66 -
    3.67 -abbreviation (input)
    3.68 -  "eqp G i j \<equiv> has_edge G i LEQ j"
    3.69 -
    3.70 -abbreviation
    3.71 -  eql :: "'a scg \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    3.72 -("_ \<turnstile> _ \<leadsto> _")
    3.73 -where
    3.74 -  "eql G i j \<equiv> has_edge G i LESS j \<or> has_edge G i LEQ j"
    3.75 -
    3.76 -
    3.77 -abbreviation (input) descat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
    3.78 -where
    3.79 -  "descat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))"
    3.80 -
    3.81 -abbreviation (input) eqat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
    3.82 -where
    3.83 -  "eqat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i))"
    3.84 -
    3.85 -
    3.86 -abbreviation (input) eqlat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
    3.87 -where
    3.88 -  "eqlat p \<theta> i \<equiv> (has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))
    3.89 -                  \<or> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i)))"
    3.90 -
    3.91 -
    3.92 -definition is_desc_thread :: "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> bool"
    3.93 -where
    3.94 -  "is_desc_thread \<theta> p = ((\<exists>n.\<forall>i\<ge>n. eqlat p \<theta> i) \<and> (\<exists>\<^sub>\<infinity>i. descat p \<theta> i))" 
    3.95 -
    3.96 -definition SCT :: "'a acg \<Rightarrow> bool"
    3.97 -where
    3.98 -  "SCT \<A> = 
    3.99 -  (\<forall>p. has_ipath \<A> p \<longrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> p))"
   3.100 -
   3.101 -
   3.102 -
   3.103 -definition no_bad_graphs :: "'a acg \<Rightarrow> bool"
   3.104 -where
   3.105 -  "no_bad_graphs A = 
   3.106 -  (\<forall>n G. has_edge A n G n \<and> G * G = G
   3.107 -  \<longrightarrow> (\<exists>p. has_edge G p LESS p))"
   3.108 -
   3.109 -
   3.110 -definition SCT' :: "'a acg \<Rightarrow> bool"
   3.111 -where
   3.112 -  "SCT' A = no_bad_graphs (tcl A)"
   3.113 -
   3.114 -end
     4.1 --- a/src/HOL/SizeChange/Examples.thy	Fri Nov 06 13:36:46 2009 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,83 +0,0 @@
     4.4 -(*  Title:      HOL/Library/SCT_Examples.thy
     4.5 -    ID:         $Id$
     4.6 -    Author:     Alexander Krauss, TU Muenchen
     4.7 -*)
     4.8 -
     4.9 -header {* Examples for Size-Change Termination *}
    4.10 -
    4.11 -theory Examples
    4.12 -imports Size_Change_Termination
    4.13 -begin
    4.14 -
    4.15 -function f :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    4.16 -where
    4.17 -  "f n 0 = n"
    4.18 -| "f 0 (Suc m) = f (Suc m) m"
    4.19 -| "f (Suc n) (Suc m) = f m n"
    4.20 -by pat_completeness auto
    4.21 -
    4.22 -
    4.23 -termination
    4.24 -  unfolding f_rel_def lfp_const
    4.25 -  apply (rule SCT_on_relations)
    4.26 -  apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *)
    4.27 -  apply (rule ext, rule ext, simp) (* Show that they are correct *)
    4.28 -  apply (tactic "Sct.mk_call_graph @{context}") (* Build control graph *)
    4.29 -  apply (rule SCT_Main)                 (* Apply main theorem *)
    4.30 -  apply (simp add:finite_acg_simps) (* show finiteness *)
    4.31 -  oops (*FIXME by eval*) (* Evaluate to true *)
    4.32 -
    4.33 -function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
    4.34 -where
    4.35 -  "p m n r = (if r>0 then p m (r - 1) n else
    4.36 -              if n>0 then p r (n - 1) m 
    4.37 -                     else m)"
    4.38 -by pat_completeness auto
    4.39 -
    4.40 -termination
    4.41 -  unfolding p_rel_def lfp_const
    4.42 -  apply (rule SCT_on_relations)
    4.43 -  apply (tactic "Sct.abs_rel_tac") 
    4.44 -  apply (rule ext, rule ext, simp) 
    4.45 -  apply (tactic "Sct.mk_call_graph @{context}")
    4.46 -  apply (rule SCT_Main)
    4.47 -  apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
    4.48 -  oops (* FIXME by eval *)
    4.49 -
    4.50 -function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
    4.51 -where
    4.52 -  "foo True (Suc n) m = foo True n (Suc m)"
    4.53 -| "foo True 0 m = foo False 0 m"
    4.54 -| "foo False n (Suc m) = foo False (Suc n) m"
    4.55 -| "foo False n 0 = n"
    4.56 -by pat_completeness auto
    4.57 -
    4.58 -termination
    4.59 -  unfolding foo_rel_def lfp_const
    4.60 -  apply (rule SCT_on_relations)
    4.61 -  apply (tactic "Sct.abs_rel_tac") 
    4.62 -  apply (rule ext, rule ext, simp) 
    4.63 -  apply (tactic "Sct.mk_call_graph @{context}")
    4.64 -  apply (rule SCT_Main)
    4.65 -  apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
    4.66 -  oops (* FIXME by eval *)
    4.67 -
    4.68 -
    4.69 -function (sequential) 
    4.70 -  bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
    4.71 -where
    4.72 -  "bar 0 (Suc n) m = bar m m m"
    4.73 -| "bar k n m = 0"
    4.74 -by pat_completeness auto
    4.75 -
    4.76 -termination
    4.77 -  unfolding bar_rel_def lfp_const
    4.78 -  apply (rule SCT_on_relations)
    4.79 -  apply (tactic "Sct.abs_rel_tac") 
    4.80 -  apply (rule ext, rule ext, simp) 
    4.81 -  apply (tactic "Sct.mk_call_graph @{context}")
    4.82 -  apply (rule SCT_Main)
    4.83 -  apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
    4.84 -  by (simp only:sctTest_simps cong: sctTest_congs)
    4.85 -
    4.86 -end
     5.1 --- a/src/HOL/SizeChange/Graphs.thy	Fri Nov 06 13:36:46 2009 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,768 +0,0 @@
     5.4 -(*  Title:      HOL/Library/Graphs.thy
     5.5 -    Author:     Alexander Krauss, TU Muenchen
     5.6 -*)
     5.7 -
     5.8 -header {* General Graphs as Sets *}
     5.9 -
    5.10 -theory Graphs
    5.11 -imports Main Misc_Tools Kleene_Algebra
    5.12 -begin
    5.13 -
    5.14 -subsection {* Basic types, Size Change Graphs *}
    5.15 -
    5.16 -datatype ('a, 'b) graph = 
    5.17 -  Graph "('a \<times> 'b \<times> 'a) set"
    5.18 -
    5.19 -primrec dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"
    5.20 -  where "dest_graph (Graph G) = G"
    5.21 -
    5.22 -lemma graph_dest_graph[simp]:
    5.23 -  "Graph (dest_graph G) = G"
    5.24 -  by (cases G) simp
    5.25 -
    5.26 -lemma split_graph_all:
    5.27 -  "(\<And>gr. PROP P gr) \<equiv> (\<And>set. PROP P (Graph set))"
    5.28 -proof
    5.29 -  fix set
    5.30 -  assume "\<And>gr. PROP P gr"
    5.31 -  then show "PROP P (Graph set)" .
    5.32 -next
    5.33 -  fix gr
    5.34 -  assume "\<And>set. PROP P (Graph set)"
    5.35 -  then have "PROP P (Graph (dest_graph gr))" .
    5.36 -  then show "PROP P gr" by simp
    5.37 -qed
    5.38 -
    5.39 -definition 
    5.40 -  has_edge :: "('n,'e) graph \<Rightarrow> 'n \<Rightarrow> 'e \<Rightarrow> 'n \<Rightarrow> bool"
    5.41 -("_ \<turnstile> _ \<leadsto>\<^bsup>_\<^esup> _")
    5.42 -where
    5.43 -  "has_edge G n e n' = ((n, e, n') \<in> dest_graph G)"
    5.44 -
    5.45 -
    5.46 -subsection {* Graph composition *}
    5.47 -
    5.48 -fun grcomp :: "('n, 'e::times) graph \<Rightarrow> ('n, 'e) graph  \<Rightarrow> ('n, 'e) graph"
    5.49 -where
    5.50 -  "grcomp (Graph G) (Graph H) = 
    5.51 -  Graph {(p,b,q) | p b q. 
    5.52 -  (\<exists>k e e'. (p,e,k)\<in>G \<and> (k,e',q)\<in>H \<and> b = e * e')}"
    5.53 -
    5.54 -
    5.55 -declare grcomp.simps[code del]
    5.56 -
    5.57 -
    5.58 -lemma graph_ext:
    5.59 -  assumes "\<And>n e n'. has_edge G n e n' = has_edge H n e n'"
    5.60 -  shows "G = H"
    5.61 -  using assms
    5.62 -  by (cases G, cases H) (auto simp:split_paired_all has_edge_def)
    5.63 -
    5.64 -
    5.65 -instantiation graph :: (type, type) comm_monoid_add
    5.66 -begin
    5.67 -
    5.68 -definition
    5.69 -  graph_zero_def: "0 = Graph {}" 
    5.70 -
    5.71 -definition
    5.72 -  graph_plus_def [code del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
    5.73 -
    5.74 -instance proof
    5.75 -  fix x y z :: "('a,'b) graph"
    5.76 -  show "x + y + z = x + (y + z)" 
    5.77 -   and "x + y = y + x" 
    5.78 -   and "0 + x = x"
    5.79 -  unfolding graph_plus_def graph_zero_def by auto
    5.80 -qed
    5.81 -
    5.82 -end
    5.83 -
    5.84 -instantiation graph :: (type, type) "{distrib_lattice, complete_lattice}"
    5.85 -begin
    5.86 -
    5.87 -definition
    5.88 -  graph_leq_def [code del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
    5.89 -
    5.90 -definition
    5.91 -  graph_less_def [code del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
    5.92 -
    5.93 -definition
    5.94 -  [code del]: "bot = Graph {}"
    5.95 -
    5.96 -definition
    5.97 -  [code del]: "top = Graph UNIV"
    5.98 -
    5.99 -definition
   5.100 -  [code del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
   5.101 -
   5.102 -definition
   5.103 -  [code del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
   5.104 -
   5.105 -definition
   5.106 -  Inf_graph_def [code del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
   5.107 -
   5.108 -definition
   5.109 -  Sup_graph_def [code del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
   5.110 -
   5.111 -instance proof
   5.112 -  fix x y z :: "('a,'b) graph"
   5.113 -  fix A :: "('a, 'b) graph set"
   5.114 -
   5.115 -  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
   5.116 -    unfolding graph_leq_def graph_less_def
   5.117 -    by (cases x, cases y) auto
   5.118 -
   5.119 -  show "x \<le> x" unfolding graph_leq_def ..
   5.120 -
   5.121 -  { assume "x \<le> y" "y \<le> z" 
   5.122 -    with order_trans show "x \<le> z"
   5.123 -      unfolding graph_leq_def . }
   5.124 -
   5.125 -  { assume "x \<le> y" "y \<le> x" thus "x = y" 
   5.126 -      unfolding graph_leq_def 
   5.127 -      by (cases x, cases y) simp }
   5.128 -
   5.129 -  show "inf x y \<le> x" "inf x y \<le> y"
   5.130 -    unfolding inf_graph_def graph_leq_def 
   5.131 -    by auto    
   5.132 -  
   5.133 -  { assume "x \<le> y" "x \<le> z" thus "x \<le> inf y z"
   5.134 -      unfolding inf_graph_def graph_leq_def 
   5.135 -      by auto }
   5.136 -
   5.137 -  show "x \<le> sup x y" "y \<le> sup x y"
   5.138 -    unfolding sup_graph_def graph_leq_def graph_plus_def by auto
   5.139 -
   5.140 -  { assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x"
   5.141 -      unfolding sup_graph_def graph_leq_def graph_plus_def by auto }
   5.142 -
   5.143 -  show "bot \<le> x" unfolding graph_leq_def bot_graph_def by simp
   5.144 -
   5.145 -  show "x \<le> top" unfolding graph_leq_def top_graph_def by simp
   5.146 -  
   5.147 -  show "sup x (inf y z) = inf (sup x y) (sup x z)"
   5.148 -    unfolding inf_graph_def sup_graph_def graph_leq_def graph_plus_def by auto
   5.149 -
   5.150 -  { assume "x \<in> A" thus "Inf A \<le> x" 
   5.151 -      unfolding Inf_graph_def graph_leq_def by auto }
   5.152 -
   5.153 -  { assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" thus "z \<le> Inf A"
   5.154 -    unfolding Inf_graph_def graph_leq_def by auto }
   5.155 -
   5.156 -  { assume "x \<in> A" thus "x \<le> Sup A" 
   5.157 -      unfolding Sup_graph_def graph_leq_def by auto }
   5.158 -
   5.159 -  { assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" thus "Sup A \<le> z"
   5.160 -    unfolding Sup_graph_def graph_leq_def by auto }
   5.161 -qed
   5.162 -
   5.163 -end
   5.164 -
   5.165 -lemma in_grplus:
   5.166 -  "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
   5.167 -  by (cases G, cases H, auto simp:has_edge_def graph_plus_def)
   5.168 -
   5.169 -lemma in_grzero:
   5.170 -  "has_edge 0 p b q = False"
   5.171 -  by (simp add:graph_zero_def has_edge_def)
   5.172 -
   5.173 -
   5.174 -subsubsection {* Multiplicative Structure *}
   5.175 -
   5.176 -instantiation graph :: (type, times) mult_zero
   5.177 -begin
   5.178 -
   5.179 -definition
   5.180 -  graph_mult_def [code del]: "G * H = grcomp G H" 
   5.181 -
   5.182 -instance proof
   5.183 -  fix a :: "('a, 'b) graph"
   5.184 -
   5.185 -  show "0 * a = 0" 
   5.186 -    unfolding graph_mult_def graph_zero_def
   5.187 -    by (cases a) (simp add:grcomp.simps)
   5.188 -  show "a * 0 = 0" 
   5.189 -    unfolding graph_mult_def graph_zero_def
   5.190 -    by (cases a) (simp add:grcomp.simps)
   5.191 -qed
   5.192 -
   5.193 -end
   5.194 -
   5.195 -instantiation graph :: (type, one) one 
   5.196 -begin
   5.197 -
   5.198 -definition
   5.199 -  graph_one_def: "1 = Graph { (x, 1, x) |x. True}"
   5.200 -
   5.201 -instance ..
   5.202 -
   5.203 -end
   5.204 -
   5.205 -lemma in_grcomp:
   5.206 -  "has_edge (G * H) p b q
   5.207 -  = (\<exists>k e e'. has_edge G p e k \<and> has_edge H k e' q \<and> b = e * e')"
   5.208 -  by (cases G, cases H) (auto simp:graph_mult_def has_edge_def image_def)
   5.209 -
   5.210 -lemma in_grunit:
   5.211 -  "has_edge 1 p b q = (p = q \<and> b = 1)"
   5.212 -  by (auto simp:graph_one_def has_edge_def)
   5.213 -
   5.214 -instance graph :: (type, semigroup_mult) semigroup_mult
   5.215 -proof
   5.216 -  fix G1 G2 G3 :: "('a,'b) graph"
   5.217 -  
   5.218 -  show "G1 * G2 * G3 = G1 * (G2 * G3)"
   5.219 -  proof (rule graph_ext, rule trans)
   5.220 -    fix p J q
   5.221 -    show "has_edge ((G1 * G2) * G3) p J q =
   5.222 -      (\<exists>G i H j I.
   5.223 -      has_edge G1 p G i
   5.224 -      \<and> has_edge G2 i H j
   5.225 -      \<and> has_edge G3 j I q
   5.226 -      \<and> J = (G * H) * I)"
   5.227 -      by (simp only:in_grcomp) blast
   5.228 -    show "\<dots> = has_edge (G1 * (G2 * G3)) p J q"
   5.229 -      by (simp only:in_grcomp mult_assoc) blast
   5.230 -  qed
   5.231 -qed
   5.232 -
   5.233 -instance graph :: (type, monoid_mult) "{semiring_1, idem_add}"
   5.234 -proof
   5.235 -  fix a b c :: "('a, 'b) graph"
   5.236 -  
   5.237 -  show "1 * a = a" 
   5.238 -    by (rule graph_ext) (auto simp:in_grcomp in_grunit)
   5.239 -  show "a * 1 = a"
   5.240 -    by (rule graph_ext) (auto simp:in_grcomp in_grunit)
   5.241 -
   5.242 -  show "(a + b) * c = a * c + b * c"
   5.243 -    by (rule graph_ext, simp add:in_grcomp in_grplus) blast
   5.244 -
   5.245 -  show "a * (b + c) = a * b + a * c"
   5.246 -    by (rule graph_ext, simp add:in_grcomp in_grplus) blast
   5.247 -
   5.248 -  show "(0::('a,'b) graph) \<noteq> 1" unfolding graph_zero_def graph_one_def
   5.249 -    by simp
   5.250 -
   5.251 -  show "a + a = a" unfolding graph_plus_def by simp
   5.252 -  
   5.253 -qed
   5.254 -
   5.255 -instantiation graph :: (type, monoid_mult) star
   5.256 -begin
   5.257 -
   5.258 -definition
   5.259 -  graph_star_def: "star (G \<Colon> ('a, 'b) graph) = (SUP n. G ^ n)" 
   5.260 -
   5.261 -instance ..
   5.262 -
   5.263 -end
   5.264 -
   5.265 -lemma graph_leqI:
   5.266 -  assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
   5.267 -  shows "G \<le> H"
   5.268 -  using assms
   5.269 -  unfolding graph_leq_def has_edge_def
   5.270 -  by auto
   5.271 -
   5.272 -lemma in_graph_plusE:
   5.273 -  assumes "has_edge (G + H) n e n'"
   5.274 -  assumes "has_edge G n e n' \<Longrightarrow> P"
   5.275 -  assumes "has_edge H n e n' \<Longrightarrow> P"
   5.276 -  shows P
   5.277 -  using assms
   5.278 -  by (auto simp: in_grplus)
   5.279 -
   5.280 -lemma in_graph_compE:
   5.281 -  assumes GH: "has_edge (G * H) n e n'"
   5.282 -  obtains e1 k e2 
   5.283 -  where "has_edge G n e1 k" "has_edge H k e2 n'" "e = e1 * e2"
   5.284 -  using GH
   5.285 -  by (auto simp: in_grcomp)
   5.286 -
   5.287 -lemma 
   5.288 -  assumes "x \<in> S k"
   5.289 -  shows "x \<in> (\<Union>k. S k)"
   5.290 -  using assms by blast
   5.291 -
   5.292 -lemma graph_union_least:
   5.293 -  assumes "\<And>n. Graph (G n) \<le> C"
   5.294 -  shows "Graph (\<Union>n. G n) \<le> C"
   5.295 -  using assms unfolding graph_leq_def
   5.296 -  by auto
   5.297 -
   5.298 -lemma Sup_graph_eq:
   5.299 -  "(SUP n. Graph (G n)) = Graph (\<Union>n. G n)"
   5.300 -proof (rule order_antisym)
   5.301 -  show "(SUP n. Graph (G n)) \<le> Graph (\<Union>n. G n)"
   5.302 -    by  (rule SUP_leI) (auto simp add: graph_leq_def)
   5.303 -
   5.304 -  show "Graph (\<Union>n. G n) \<le> (SUP n. Graph (G n))"
   5.305 -  by (rule graph_union_least, rule le_SUPI', rule) 
   5.306 -qed
   5.307 -
   5.308 -lemma has_edge_leq: "has_edge G p b q = (Graph {(p,b,q)} \<le> G)"
   5.309 -  unfolding has_edge_def graph_leq_def
   5.310 -  by (cases G) simp
   5.311 -
   5.312 -
   5.313 -lemma Sup_graph_eq2:
   5.314 -  "(SUP n. G n) = Graph (\<Union>n. dest_graph (G n))"
   5.315 -  using Sup_graph_eq[of "\<lambda>n. dest_graph (G n)", simplified]
   5.316 -  by simp
   5.317 -
   5.318 -lemma in_SUP:
   5.319 -  "has_edge (SUP x. Gs x) p b q = (\<exists>x. has_edge (Gs x) p b q)"
   5.320 -  unfolding Sup_graph_eq2 has_edge_leq graph_leq_def
   5.321 -  by simp
   5.322 -
   5.323 -instance graph :: (type, monoid_mult) kleene_by_complete_lattice
   5.324 -proof
   5.325 -  fix a b c :: "('a, 'b) graph"
   5.326 -
   5.327 -  show "a \<le> b \<longleftrightarrow> a + b = b" unfolding graph_leq_def graph_plus_def
   5.328 -    by (cases a, cases b) auto
   5.329 -
   5.330 -  from less_le_not_le show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" .
   5.331 -
   5.332 -  show "a * star b * c = (SUP n. a * b ^ n * c)"
   5.333 -    unfolding graph_star_def
   5.334 -    by (rule graph_ext) (force simp:in_SUP in_grcomp)
   5.335 -qed
   5.336 -
   5.337 -
   5.338 -lemma in_star: 
   5.339 -  "has_edge (star G) a x b = (\<exists>n. has_edge (G ^ n) a x b)"
   5.340 -  by (auto simp:graph_star_def in_SUP)
   5.341 -
   5.342 -lemma tcl_is_SUP:
   5.343 -  "tcl (G::('a::type, 'b::monoid_mult) graph) =
   5.344 -  (SUP n. G ^ (Suc n))"
   5.345 -  unfolding tcl_def 
   5.346 -  using star_cont[of 1 G G]
   5.347 -  by (simp add:power_Suc power_commutes)
   5.348 -
   5.349 -
   5.350 -lemma in_tcl: 
   5.351 -  "has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)"
   5.352 -  apply (auto simp: tcl_is_SUP in_SUP simp del: power.simps power_Suc)
   5.353 -  apply (rule_tac x = "n - 1" in exI, auto)
   5.354 -  done
   5.355 -
   5.356 -
   5.357 -subsection {* Infinite Paths *}
   5.358 -
   5.359 -types ('n, 'e) ipath = "('n \<times> 'e) sequence"
   5.360 -
   5.361 -definition has_ipath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) ipath \<Rightarrow> bool"
   5.362 -where
   5.363 -  "has_ipath G p = 
   5.364 -  (\<forall>i. has_edge G (fst (p i)) (snd (p i)) (fst (p (Suc i))))"
   5.365 -
   5.366 -
   5.367 -subsection {* Finite Paths *}
   5.368 -
   5.369 -types ('n, 'e) fpath = "('n \<times> ('e \<times> 'n) list)"
   5.370 -
   5.371 -inductive  has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool" 
   5.372 -  for G :: "('n, 'e) graph"
   5.373 -where
   5.374 -  has_fpath_empty: "has_fpath G (n, [])"
   5.375 -| has_fpath_join: "\<lbrakk>G \<turnstile> n \<leadsto>\<^bsup>e\<^esup> n'; has_fpath G (n', es)\<rbrakk> \<Longrightarrow> has_fpath G (n, (e, n')#es)"
   5.376 -
   5.377 -definition 
   5.378 -  "end_node p = 
   5.379 -  (if snd p = [] then fst p else snd (snd p ! (length (snd p) - 1)))"
   5.380 -
   5.381 -definition path_nth :: "('n, 'e) fpath \<Rightarrow> nat \<Rightarrow> ('n \<times> 'e \<times> 'n)"
   5.382 -where
   5.383 -  "path_nth p k = (if k = 0 then fst p else snd (snd p ! (k - 1)), snd p ! k)"
   5.384 -
   5.385 -lemma endnode_nth:
   5.386 -  assumes "length (snd p) = Suc k"
   5.387 -  shows "end_node p = snd (snd (path_nth p k))"
   5.388 -  using assms unfolding end_node_def path_nth_def
   5.389 -  by auto
   5.390 -
   5.391 -lemma path_nth_graph:
   5.392 -  assumes "k < length (snd p)"
   5.393 -  assumes "has_fpath G p"
   5.394 -  shows "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p k)"
   5.395 -using assms
   5.396 -proof (induct k arbitrary: p)
   5.397 -  case 0 thus ?case 
   5.398 -    unfolding path_nth_def by (auto elim:has_fpath.cases)
   5.399 -next
   5.400 -  case (Suc k p)
   5.401 -
   5.402 -  from `has_fpath G p` show ?case 
   5.403 -  proof (rule has_fpath.cases)
   5.404 -    case goal1 with Suc show ?case by simp
   5.405 -  next
   5.406 -    fix n e n' es
   5.407 -    assume st: "p = (n, (e, n') # es)"
   5.408 -       "G \<turnstile> n \<leadsto>\<^bsup>e\<^esup> n'"
   5.409 -       "has_fpath G (n', es)"
   5.410 -    with Suc
   5.411 -    have "(\<lambda>(n, b, a). G \<turnstile> n \<leadsto>\<^bsup>b\<^esup> a) (path_nth (n', es) k)" by simp
   5.412 -    with st show ?thesis by (cases k, auto simp:path_nth_def)
   5.413 -  qed
   5.414 -qed
   5.415 -
   5.416 -lemma path_nth_connected:
   5.417 -  assumes "Suc k < length (snd p)"
   5.418 -  shows "fst (path_nth p (Suc k)) = snd (snd (path_nth p k))"
   5.419 -  using assms
   5.420 -  unfolding path_nth_def
   5.421 -  by auto
   5.422 -
   5.423 -definition path_loop :: "('n, 'e) fpath \<Rightarrow> ('n, 'e) ipath" ("omega")
   5.424 -where
   5.425 -  "omega p \<equiv> (\<lambda>i. (\<lambda>(n,e,n'). (n,e)) (path_nth p (i mod (length (snd p)))))"
   5.426 -
   5.427 -lemma fst_p0: "fst (path_nth p 0) = fst p"
   5.428 -  unfolding path_nth_def by simp
   5.429 -
   5.430 -lemma path_loop_connect:
   5.431 -  assumes "fst p = end_node p"
   5.432 -  and "0 < length (snd p)" (is "0 < ?l")
   5.433 -  shows "fst (path_nth p (Suc i mod (length (snd p))))
   5.434 -  = snd (snd (path_nth p (i mod length (snd p))))"
   5.435 -  (is "\<dots> = snd (snd (path_nth p ?k))")
   5.436 -proof -
   5.437 -  from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
   5.438 -    by simp
   5.439 -
   5.440 -  show ?thesis 
   5.441 -  proof (cases "Suc ?k < ?l")
   5.442 -    case True
   5.443 -    hence "Suc ?k \<noteq> ?l" by simp
   5.444 -    with path_nth_connected[OF True]
   5.445 -    show ?thesis
   5.446 -      by (simp add:mod_Suc)
   5.447 -  next
   5.448 -    case False 
   5.449 -    with `?k < ?l` have wrap: "Suc ?k = ?l" by simp
   5.450 -
   5.451 -    hence "fst (path_nth p (Suc i mod ?l)) = fst (path_nth p 0)" 
   5.452 -      by (simp add: mod_Suc)
   5.453 -    also from fst_p0 have "\<dots> = fst p" .
   5.454 -    also have "\<dots> = end_node p" by fact
   5.455 -    also have "\<dots> = snd (snd (path_nth p ?k))" 
   5.456 -      by (auto simp: endnode_nth wrap)
   5.457 -    finally show ?thesis .
   5.458 -  qed
   5.459 -qed
   5.460 -
   5.461 -lemma path_loop_graph:
   5.462 -  assumes "has_fpath G p"
   5.463 -  and loop: "fst p = end_node p"
   5.464 -  and nonempty: "0 < length (snd p)" (is "0 < ?l")
   5.465 -  shows "has_ipath G (omega p)"
   5.466 -proof -
   5.467 -  {
   5.468 -    fix i 
   5.469 -    from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
   5.470 -      by simp
   5.471 -    from this and `has_fpath G p`
   5.472 -    have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)"
   5.473 -      by (rule path_nth_graph)
   5.474 -
   5.475 -    from path_loop_connect[OF loop nonempty] pk_G
   5.476 -    have "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))"
   5.477 -      unfolding path_loop_def has_edge_def split_def
   5.478 -      by simp
   5.479 -  }
   5.480 -  then show ?thesis by (auto simp:has_ipath_def)
   5.481 -qed
   5.482 -
   5.483 -definition prod :: "('n, 'e::monoid_mult) fpath \<Rightarrow> 'e"
   5.484 -where
   5.485 -  "prod p = foldr (op *) (map fst (snd p)) 1"
   5.486 -
   5.487 -lemma prod_simps[simp]:
   5.488 -  "prod (n, []) = 1"
   5.489 -  "prod (n, (e,n')#es) = e * (prod (n',es))"
   5.490 -unfolding prod_def
   5.491 -by simp_all
   5.492 -
   5.493 -lemma power_induces_path:
   5.494 -  assumes a: "has_edge (A ^ k) n G m"
   5.495 -  obtains p 
   5.496 -    where "has_fpath A p"
   5.497 -      and "n = fst p" "m = end_node p"
   5.498 -      and "G = prod p"
   5.499 -      and "k = length (snd p)"
   5.500 -  using a
   5.501 -proof (induct k arbitrary:m n G thesis)
   5.502 -  case (0 m n G)
   5.503 -  let ?p = "(n, [])"
   5.504 -  from 0 have "has_fpath A ?p" "m = end_node ?p" "G = prod ?p"
   5.505 -    by (auto simp:in_grunit end_node_def intro:has_fpath.intros)
   5.506 -  thus ?case using 0 by (auto simp:end_node_def)
   5.507 -next
   5.508 -  case (Suc k m n G)
   5.509 -  hence "has_edge (A * A ^ k) n G m" 
   5.510 -    by (simp add:power_Suc power_commutes)
   5.511 -  then obtain G' H j where 
   5.512 -    a_A: "has_edge A n G' j"
   5.513 -    and H_pow: "has_edge (A ^ k) j H m"
   5.514 -    and [simp]: "G = G' * H"
   5.515 -    by (auto simp:in_grcomp) 
   5.516 -
   5.517 -  from H_pow and Suc
   5.518 -  obtain p
   5.519 -    where p_path: "has_fpath A p"
   5.520 -    and [simp]: "j = fst p" "m = end_node p" "H = prod p" 
   5.521 -    "k = length (snd p)"
   5.522 -    by blast
   5.523 -
   5.524 -  let ?p' = "(n, (G', j)#snd p)"
   5.525 -  from a_A and p_path
   5.526 -  have "has_fpath A ?p'" "m = end_node ?p'" "G = prod ?p'"
   5.527 -    by (auto simp:end_node_def nth.simps intro:has_fpath.intros split:nat.split)
   5.528 -  thus ?case using Suc by auto
   5.529 -qed
   5.530 -
   5.531 -
   5.532 -subsection {* Sub-Paths *}
   5.533 -
   5.534 -definition sub_path :: "('n, 'e) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ('n, 'e) fpath"
   5.535 -("(_\<langle>_,_\<rangle>)")
   5.536 -where
   5.537 -  "p\<langle>i,j\<rangle> =
   5.538 -  (fst (p i), map (\<lambda>k. (snd (p k), fst (p (Suc k)))) [i ..< j])"
   5.539 -
   5.540 -
   5.541 -lemma sub_path_is_path: 
   5.542 -  assumes ipath: "has_ipath G p"
   5.543 -  assumes l: "i \<le> j"
   5.544 -  shows "has_fpath G (p\<langle>i,j\<rangle>)"
   5.545 -  using l
   5.546 -proof (induct i rule:inc_induct)
   5.547 -  case base show ?case by (auto simp:sub_path_def intro:has_fpath.intros)
   5.548 -next
   5.549 -  case (step i)
   5.550 -  with ipath upt_rec[of i j]
   5.551 -  show ?case
   5.552 -    by (auto simp:sub_path_def has_ipath_def intro:has_fpath.intros)
   5.553 -qed
   5.554 -
   5.555 -
   5.556 -lemma sub_path_start[simp]:
   5.557 -  "fst (p\<langle>i,j\<rangle>) = fst (p i)"
   5.558 -  by (simp add:sub_path_def)
   5.559 -
   5.560 -lemma nth_upto[simp]: "k < j - i \<Longrightarrow> [i ..< j] ! k = i + k"
   5.561 -  by (induct k) auto
   5.562 -
   5.563 -lemma sub_path_end[simp]:
   5.564 -  "i < j \<Longrightarrow> end_node (p\<langle>i,j\<rangle>) = fst (p j)"
   5.565 -  by (auto simp:sub_path_def end_node_def)
   5.566 -
   5.567 -lemma foldr_map: "foldr f (map g xs) = foldr (f o g) xs"
   5.568 -  by (induct xs) auto
   5.569 -
   5.570 -lemma upto_append[simp]:
   5.571 -  assumes "i \<le> j" "j \<le> k"
   5.572 -  shows "[ i ..< j ] @ [j ..< k] = [i ..< k]"
   5.573 -  using assms and upt_add_eq_append[of i j "k - j"]
   5.574 -  by simp
   5.575 -
   5.576 -lemma foldr_monoid: "foldr (op *) xs 1 * foldr (op *) ys 1
   5.577 -  = foldr (op *) (xs @ ys) (1::'a::monoid_mult)"
   5.578 -  by (induct xs) (auto simp:mult_assoc)
   5.579 -
   5.580 -lemma sub_path_prod:
   5.581 -  assumes "i < j"
   5.582 -  assumes "j < k"
   5.583 -  shows "prod (p\<langle>i,k\<rangle>) = prod (p\<langle>i,j\<rangle>) * prod (p\<langle>j,k\<rangle>)"
   5.584 -  using assms
   5.585 -  unfolding prod_def sub_path_def
   5.586 -  by (simp add:map_compose[symmetric] comp_def)
   5.587 -   (simp only:foldr_monoid map_append[symmetric] upto_append)
   5.588 -
   5.589 -
   5.590 -lemma path_acgpow_aux:
   5.591 -  assumes "length es = l"
   5.592 -  assumes "has_fpath G (n,es)"
   5.593 -  shows "has_edge (G ^ l) n (prod (n,es)) (end_node (n,es))"
   5.594 -using assms
   5.595 -proof (induct l arbitrary:n es)
   5.596 -  case 0 thus ?case
   5.597 -    by (simp add:in_grunit end_node_def) 
   5.598 -next
   5.599 -  case (Suc l n es)
   5.600 -  hence "es \<noteq> []" by auto
   5.601 -  let ?n' = "snd (hd es)"
   5.602 -  let ?es' = "tl es"
   5.603 -  let ?e = "fst (hd es)"
   5.604 -
   5.605 -  from Suc have len: "length ?es' = l" by auto
   5.606 -
   5.607 -  from Suc
   5.608 -  have [simp]: "end_node (n, es) = end_node (?n', ?es')"
   5.609 -    by (cases es) (auto simp:end_node_def nth.simps split:nat.split)
   5.610 -
   5.611 -  from `has_fpath G (n,es)`
   5.612 -  have "has_fpath G (?n', ?es')"
   5.613 -    by (rule has_fpath.cases) (auto intro:has_fpath.intros)
   5.614 -  with Suc len
   5.615 -  have "has_edge (G ^ l) ?n' (prod (?n', ?es')) (end_node (?n', ?es'))"
   5.616 -    by auto
   5.617 -  moreover
   5.618 -  from `es \<noteq> []`
   5.619 -  have "prod (n, es) = ?e * (prod (?n', ?es'))"
   5.620 -    by (cases es) auto
   5.621 -  moreover
   5.622 -  from `has_fpath G (n,es)` have c:"has_edge G n ?e ?n'"
   5.623 -    by (rule has_fpath.cases) (insert `es \<noteq> []`, auto)
   5.624 -
   5.625 -  ultimately
   5.626 -  show ?case
   5.627 -     unfolding power_Suc 
   5.628 -     by (auto simp:in_grcomp)
   5.629 -qed
   5.630 -
   5.631 -
   5.632 -lemma path_acgpow:
   5.633 -   "has_fpath G p
   5.634 -  \<Longrightarrow> has_edge (G ^ length (snd p)) (fst p) (prod p) (end_node p)"
   5.635 -by (cases p)
   5.636 -   (rule path_acgpow_aux[of "snd p" "length (snd p)" _ "fst p", simplified])
   5.637 -
   5.638 -
   5.639 -lemma star_paths:
   5.640 -  "has_edge (star G) a x b =
   5.641 -   (\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p)"
   5.642 -proof
   5.643 -  assume "has_edge (star G) a x b"
   5.644 -  then obtain n where pow: "has_edge (G ^ n) a x b"
   5.645 -    by (auto simp:in_star)
   5.646 -
   5.647 -  then obtain p where
   5.648 -    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
   5.649 -    by (rule power_induces_path)
   5.650 -
   5.651 -  thus "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p"
   5.652 -    by blast
   5.653 -next
   5.654 -  assume "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p"
   5.655 -  then obtain p where
   5.656 -    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
   5.657 -    by blast
   5.658 -
   5.659 -  hence "has_edge (G ^ length (snd p)) a x b"
   5.660 -    by (auto intro:path_acgpow)
   5.661 -
   5.662 -  thus "has_edge (star G) a x b"
   5.663 -    by (auto simp:in_star)
   5.664 -qed
   5.665 -
   5.666 -
   5.667 -lemma plus_paths:
   5.668 -  "has_edge (tcl G) a x b =
   5.669 -   (\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p \<and> 0 < length (snd p))"
   5.670 -proof
   5.671 -  assume "has_edge (tcl G) a x b"
   5.672 -  
   5.673 -  then obtain n where pow: "has_edge (G ^ n) a x b" and "0 < n"
   5.674 -    by (auto simp:in_tcl)
   5.675 -
   5.676 -  from pow obtain p where
   5.677 -    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
   5.678 -    "n = length (snd p)"
   5.679 -    by (rule power_induces_path)
   5.680 -
   5.681 -  with `0 < n`
   5.682 -  show "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p \<and> 0 < length (snd p) "
   5.683 -    by blast
   5.684 -next
   5.685 -  assume "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p
   5.686 -    \<and> 0 < length (snd p)"
   5.687 -  then obtain p where
   5.688 -    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
   5.689 -    "0 < length (snd p)"
   5.690 -    by blast
   5.691 -
   5.692 -  hence "has_edge (G ^ length (snd p)) a x b"
   5.693 -    by (auto intro:path_acgpow)
   5.694 -
   5.695 -  with `0 < length (snd p)`
   5.696 -  show "has_edge (tcl G) a x b"
   5.697 -    by (auto simp:in_tcl)
   5.698 -qed
   5.699 -
   5.700 -
   5.701 -definition
   5.702 -  "contract s p = 
   5.703 -  (\<lambda>i. (fst (p (s i)), prod (p\<langle>s i,s (Suc i)\<rangle>)))"
   5.704 -
   5.705 -lemma ipath_contract:
   5.706 -  assumes [simp]: "increasing s"
   5.707 -  assumes ipath: "has_ipath G p"
   5.708 -  shows "has_ipath (tcl G) (contract s p)"
   5.709 -  unfolding has_ipath_def 
   5.710 -proof
   5.711 -  fix i
   5.712 -  let ?p = "p\<langle>s i,s (Suc i)\<rangle>"
   5.713 -
   5.714 -  from increasing_strict 
   5.715 -  have "fst (p (s (Suc i))) = end_node ?p" by simp
   5.716 -  moreover
   5.717 -  from increasing_strict[of s i "Suc i"] have "snd ?p \<noteq> []"
   5.718 -    by (simp add:sub_path_def)
   5.719 -  moreover
   5.720 -  from ipath increasing_weak[of s] have "has_fpath G ?p"
   5.721 -    by (rule sub_path_is_path) auto
   5.722 -  ultimately
   5.723 -  show "has_edge (tcl G) 
   5.724 -    (fst (contract s p i)) (snd (contract s p i)) (fst (contract s p (Suc i)))"
   5.725 -    unfolding contract_def plus_paths
   5.726 -    by (intro exI) auto
   5.727 -qed
   5.728 -
   5.729 -lemma prod_unfold:
   5.730 -  "i < j \<Longrightarrow> prod (p\<langle>i,j\<rangle>) 
   5.731 -  = snd (p i) * prod (p\<langle>Suc i, j\<rangle>)"
   5.732 -  unfolding prod_def
   5.733 -  by (simp add:sub_path_def upt_rec[of "i" j])
   5.734 -
   5.735 -
   5.736 -lemma sub_path_loop:
   5.737 -  assumes "0 < k"
   5.738 -  assumes k: "k = length (snd loop)"
   5.739 -  assumes loop: "fst loop = end_node loop"
   5.740 -  shows "(omega loop)\<langle>k * i,k * Suc i\<rangle> = loop" (is "?\<omega> = loop")
   5.741 -proof (rule prod_eqI)
   5.742 -  show "fst ?\<omega> = fst loop"
   5.743 -    by (auto simp:path_loop_def path_nth_def split_def k)
   5.744 -
   5.745 -  show "snd ?\<omega> = snd loop"
   5.746 -  proof (rule nth_equalityI[rule_format])
   5.747 -    show leneq: "length (snd ?\<omega>) = length (snd loop)"
   5.748 -      unfolding sub_path_def k by simp
   5.749 -
   5.750 -    fix j assume "j < length (snd (?\<omega>))"
   5.751 -    with leneq and k have "j < k" by simp
   5.752 -
   5.753 -    have a: "\<And>i. fst (path_nth loop (Suc i mod k))
   5.754 -      = snd (snd (path_nth loop (i mod k)))"
   5.755 -      unfolding k
   5.756 -      apply (rule path_loop_connect[OF loop])
   5.757 -      using `0 < k` and k
   5.758 -      apply auto
   5.759 -      done
   5.760 -
   5.761 -    from `j < k` 
   5.762 -    show "snd ?\<omega> ! j = snd loop ! j"
   5.763 -      unfolding sub_path_def
   5.764 -      apply (simp add:path_loop_def split_def add_ac)
   5.765 -      apply (simp add:a k[symmetric])
   5.766 -      apply (simp add:path_nth_def)
   5.767 -      done
   5.768 -  qed
   5.769 -qed
   5.770 -
   5.771 -end
     6.1 --- a/src/HOL/SizeChange/Implementation.thy	Fri Nov 06 13:36:46 2009 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,185 +0,0 @@
     6.4 -(*  Title:      HOL/Library/SCT_Implementation.thy
     6.5 -    ID:         $Id$
     6.6 -    Author:     Alexander Krauss, TU Muenchen
     6.7 -*)
     6.8 -
     6.9 -header {* Implemtation of the SCT criterion *}
    6.10 -
    6.11 -theory Implementation
    6.12 -imports Correctness
    6.13 -begin
    6.14 -
    6.15 -fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"
    6.16 -where
    6.17 -  "edges_match ((n, e, m), (n',e',m')) = (m = n')"
    6.18 -
    6.19 -fun connect_edges :: 
    6.20 -  "('n \<times> ('e::times) \<times> 'n) \<times> ('n \<times> 'e \<times> 'n)
    6.21 -  \<Rightarrow> ('n \<times> 'e \<times> 'n)"
    6.22 -where
    6.23 -  "connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')"
    6.24 -
    6.25 -lemma grcomp_code [code]:
    6.26 -  "grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })"
    6.27 -  by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def)
    6.28 -
    6.29 -
    6.30 -lemma mk_tcl_finite_terminates:
    6.31 -  fixes A :: "'a acg"
    6.32 -  assumes fA: "finite_acg A" 
    6.33 -  shows "mk_tcl_dom (A, A)"
    6.34 -proof -
    6.35 -  from fA have fin_tcl: "finite_acg (tcl A)"
    6.36 -    by (simp add:finite_tcl)
    6.37 -
    6.38 -  hence "finite (dest_graph (tcl A))"
    6.39 -    unfolding finite_acg_def finite_graph_def ..
    6.40 -
    6.41 -  let ?count = "\<lambda>G. card (dest_graph G)"
    6.42 -  let ?N = "?count (tcl A)"
    6.43 -  let ?m = "\<lambda>X. ?N - (?count X)"
    6.44 -
    6.45 -  let ?P = "\<lambda>X. mk_tcl_dom (A, X)"
    6.46 -  
    6.47 -  {
    6.48 -    fix X
    6.49 -    assume "X \<le> tcl A"
    6.50 -    then
    6.51 -    have "mk_tcl_dom (A, X)"
    6.52 -    proof (induct X rule:measure_induct_rule[of ?m])
    6.53 -      case (less X)
    6.54 -      show ?case
    6.55 -      proof (cases "X * A \<le> X")
    6.56 -        case True 
    6.57 -        with mk_tcl.domintros show ?thesis by auto
    6.58 -      next
    6.59 -        case False
    6.60 -        then have l: "X < X + X * A"
    6.61 -          unfolding graph_less_def graph_leq_def graph_plus_def
    6.62 -          by auto
    6.63 -
    6.64 -        from `X \<le> tcl A` 
    6.65 -        have "X * A \<le> tcl A * A" by (simp add:mult_mono)
    6.66 -        also have "\<dots> \<le> A + tcl A * A" by simp
    6.67 -        also have "\<dots> = tcl A" by (simp add:tcl_unfold_right[symmetric])
    6.68 -        finally have "X * A \<le> tcl A" .
    6.69 -        with `X \<le> tcl A` 
    6.70 -        have "X + X * A \<le> tcl A + tcl A"
    6.71 -          by (rule add_mono)
    6.72 -        hence less_tcl: "X + X * A \<le> tcl A" by simp 
    6.73 -        hence "X < tcl A"
    6.74 -          using l `X \<le> tcl A` by auto
    6.75 -
    6.76 -        from less_tcl fin_tcl
    6.77 -        have "finite_acg (X + X * A)" by (rule finite_acg_subset)
    6.78 -        hence "finite (dest_graph (X + X * A))" 
    6.79 -          unfolding finite_acg_def finite_graph_def ..
    6.80 -        
    6.81 -        hence X: "?count X < ?count (X + X * A)"
    6.82 -          using l[simplified graph_less_def graph_leq_def]
    6.83 -          by (rule psubset_card_mono)
    6.84 -        
    6.85 -        have "?count X < ?N" 
    6.86 -          apply (rule psubset_card_mono)
    6.87 -          by fact (rule `X < tcl A`[simplified graph_less_def])
    6.88 -        
    6.89 -        with X have "?m (X + X * A) < ?m X" by arith
    6.90 -        
    6.91 -        from  less.hyps this less_tcl
    6.92 -        have "mk_tcl_dom (A, X + X * A)" .
    6.93 -        with mk_tcl.domintros show ?thesis .
    6.94 -      qed
    6.95 -    qed
    6.96 -  }
    6.97 -  from this less_tcl show ?thesis .
    6.98 -qed
    6.99 -
   6.100 -
   6.101 -lemma mk_tcl_finite_tcl:
   6.102 -  fixes A :: "'a acg"
   6.103 -  assumes fA: "finite_acg A"
   6.104 -  shows "mk_tcl A A = tcl A"
   6.105 -  using mk_tcl_finite_terminates[OF fA]
   6.106 -  by (simp only: tcl_def mk_tcl_correctness star_simulation)
   6.107 -
   6.108 -definition test_SCT :: "nat acg \<Rightarrow> bool"
   6.109 -where
   6.110 -  "test_SCT \<A> = 
   6.111 -  (let \<T> = mk_tcl \<A> \<A>
   6.112 -    in (\<forall>(n,G,m)\<in>dest_graph \<T>. 
   6.113 -          n \<noteq> m \<or> G * G \<noteq> G \<or> 
   6.114 -         (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
   6.115 -
   6.116 -
   6.117 -lemma SCT'_exec:
   6.118 -  assumes fin: "finite_acg A"
   6.119 -  shows "SCT' A = test_SCT A"
   6.120 -  using mk_tcl_finite_tcl[OF fin]
   6.121 -  unfolding test_SCT_def Let_def 
   6.122 -  unfolding SCT'_def no_bad_graphs_def has_edge_def
   6.123 -  by force
   6.124 -
   6.125 -code_modulename SML
   6.126 -  Implementation Graphs
   6.127 -
   6.128 -lemma [code]:
   6.129 -  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
   6.130 -  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
   6.131 -  unfolding graph_leq_def graph_less_def by rule+
   6.132 -
   6.133 -lemma [code]:
   6.134 -  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)"
   6.135 -  unfolding graph_plus_def ..
   6.136 -
   6.137 -lemma [code]:
   6.138 -  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H"
   6.139 -  unfolding graph_mult_def ..
   6.140 -
   6.141 -
   6.142 -
   6.143 -lemma SCT'_empty: "SCT' (Graph {})"
   6.144 -  unfolding SCT'_def no_bad_graphs_def graph_zero_def[symmetric]
   6.145 -  tcl_zero
   6.146 -  by (simp add:in_grzero)
   6.147 -
   6.148 -
   6.149 -
   6.150 -subsection {* Witness checking *}
   6.151 -
   6.152 -definition test_SCT_witness :: "nat acg \<Rightarrow> nat acg \<Rightarrow> bool"
   6.153 -where
   6.154 -  "test_SCT_witness A T = 
   6.155 -  (A \<le> T \<and> A * T \<le> T \<and>
   6.156 -       (\<forall>(n,G,m)\<in>dest_graph T. 
   6.157 -          n \<noteq> m \<or> G * G \<noteq> G \<or> 
   6.158 -         (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
   6.159 -
   6.160 -lemma no_bad_graphs_ucl:
   6.161 -  assumes "A \<le> B"
   6.162 -  assumes "no_bad_graphs B"
   6.163 -  shows "no_bad_graphs A"
   6.164 -  using assms
   6.165 -  unfolding no_bad_graphs_def has_edge_def graph_leq_def 
   6.166 -  by blast
   6.167 -
   6.168 -lemma SCT'_witness:
   6.169 -  assumes a: "test_SCT_witness A T"
   6.170 -  shows "SCT' A"
   6.171 -proof -
   6.172 -  from a have "A \<le> T" "A * T \<le> T" by (auto simp:test_SCT_witness_def)
   6.173 -  hence "A + A * T \<le> T" 
   6.174 -    by (subst add_idem[of T, symmetric], rule add_mono)
   6.175 -  with star3' have "tcl A \<le> T" unfolding tcl_def .
   6.176 -  moreover
   6.177 -  from a have "no_bad_graphs T"
   6.178 -    unfolding no_bad_graphs_def test_SCT_witness_def has_edge_def
   6.179 -    by auto
   6.180 -  ultimately
   6.181 -  show ?thesis
   6.182 -    unfolding SCT'_def
   6.183 -    by (rule no_bad_graphs_ucl)
   6.184 -qed
   6.185 -
   6.186 -(* ML {* @{code test_SCT} *} *)
   6.187 -
   6.188 -end
     7.1 --- a/src/HOL/SizeChange/Interpretation.thy	Fri Nov 06 13:36:46 2009 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,415 +0,0 @@
     7.4 -(*  Title:      HOL/Library/SCT_Interpretation.thy
     7.5 -    ID:         $Id$
     7.6 -    Author:     Alexander Krauss, TU Muenchen
     7.7 -*)
     7.8 -
     7.9 -header {* Applying SCT to function definitions *}
    7.10 -
    7.11 -theory Interpretation
    7.12 -imports Main Misc_Tools Criterion
    7.13 -begin
    7.14 -
    7.15 -definition
    7.16 -  "idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))"
    7.17 -
    7.18 -lemma not_acc_smaller:
    7.19 -  assumes notacc: "\<not> accp R x"
    7.20 -  shows "\<exists>y. R y x \<and> \<not> accp R y"
    7.21 -proof (rule classical)
    7.22 -  assume "\<not> ?thesis"
    7.23 -  hence "\<And>y. R y x \<Longrightarrow> accp R y" by blast
    7.24 -  with accp.accI have "accp R x" .
    7.25 -  with notacc show ?thesis by contradiction
    7.26 -qed
    7.27 -
    7.28 -lemma non_acc_has_idseq:
    7.29 -  assumes "\<not> accp R x"
    7.30 -  shows "\<exists>s. idseq R s x"
    7.31 -proof -
    7.32 -  
    7.33 -  have "\<exists>f. \<forall>x. \<not>accp R x \<longrightarrow> R (f x) x \<and> \<not>accp R (f x)"
    7.34 -    by (rule choice, auto simp:not_acc_smaller)
    7.35 -  
    7.36 -  then obtain f where
    7.37 -    in_R: "\<And>x. \<not>accp R x \<Longrightarrow> R (f x) x"
    7.38 -    and nia: "\<And>x. \<not>accp R x \<Longrightarrow> \<not>accp R (f x)"
    7.39 -    by blast
    7.40 -  
    7.41 -  let ?s = "\<lambda>i. (f ^^ i) x"
    7.42 -  
    7.43 -  {
    7.44 -    fix i
    7.45 -    have "\<not>accp R (?s i)"
    7.46 -      by (induct i) (auto simp:nia `\<not>accp R x`)
    7.47 -    hence "R (f (?s i)) (?s i)"
    7.48 -      by (rule in_R)
    7.49 -  }
    7.50 -  
    7.51 -  hence "idseq R ?s x"
    7.52 -    unfolding idseq_def
    7.53 -    by auto
    7.54 -  
    7.55 -  thus ?thesis by auto
    7.56 -qed
    7.57 -
    7.58 -
    7.59 -
    7.60 -
    7.61 -
    7.62 -types ('a, 'q) cdesc =
    7.63 -  "('q \<Rightarrow> bool) \<times> ('q \<Rightarrow> 'a) \<times>('q \<Rightarrow> 'a)"
    7.64 -
    7.65 -
    7.66 -fun in_cdesc :: "('a, 'q) cdesc \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    7.67 -where
    7.68 -  "in_cdesc (\<Gamma>, r, l) x y = (\<exists>q. x = r q \<and> y = l q \<and> \<Gamma> q)"
    7.69 -
    7.70 -primrec mk_rel :: "('a, 'q) cdesc list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    7.71 -where
    7.72 -  "mk_rel [] x y = False"
    7.73 -| "mk_rel (c#cs) x y =
    7.74 -  (in_cdesc c x y \<or> mk_rel cs x y)"
    7.75 -
    7.76 -
    7.77 -lemma some_rd:
    7.78 -  assumes "mk_rel rds x y"
    7.79 -  shows "\<exists>rd\<in>set rds. in_cdesc rd x y"
    7.80 -  using assms
    7.81 -  by (induct rds) (auto simp:in_cdesc_def)
    7.82 -
    7.83 -(* from a value sequence, get a sequence of rds *)
    7.84 -
    7.85 -lemma ex_cs:
    7.86 -  assumes idseq: "idseq (mk_rel rds) s x"
    7.87 -  shows "\<exists>cs. \<forall>i. cs i \<in> set rds \<and> in_cdesc (cs i) (s (Suc i)) (s i)"
    7.88 -proof -
    7.89 -  from idseq
    7.90 -  have a: "\<forall>i. \<exists>rd \<in> set rds. in_cdesc rd (s (Suc i)) (s i)"
    7.91 -    by (auto simp:idseq_def intro:some_rd)
    7.92 -  
    7.93 -  show ?thesis
    7.94 -    by (rule choice) (insert a, blast)
    7.95 -qed
    7.96 -
    7.97 -
    7.98 -types 'a measures = "nat \<Rightarrow> 'a \<Rightarrow> nat"
    7.99 -
   7.100 -fun stepP :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> 
   7.101 -  ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> bool"
   7.102 -where
   7.103 -  "stepP (\<Gamma>1,r1,l1) (\<Gamma>2,r2,l2) m1 m2 R
   7.104 -  = (\<forall>q\<^isub>1 q\<^isub>2. \<Gamma>1 q\<^isub>1 \<and> \<Gamma>2 q\<^isub>2 \<and> r1 q\<^isub>1 = l2 q\<^isub>2 
   7.105 -  \<longrightarrow> R (m2 (l2 q\<^isub>2)) ((m1 (l1 q\<^isub>1))))"
   7.106 -
   7.107 -
   7.108 -definition
   7.109 -  decr :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> 
   7.110 -  ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
   7.111 -where
   7.112 -  "decr c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op <)"
   7.113 -
   7.114 -definition
   7.115 -  decreq :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> 
   7.116 -  ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
   7.117 -where
   7.118 -  "decreq c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op \<le>)"
   7.119 -
   7.120 -definition
   7.121 -  no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool"
   7.122 -where
   7.123 -  "no_step c1 c2 = stepP c1 c2 (\<lambda>x. 0) (\<lambda>x. 0) (\<lambda>x y. False)"
   7.124 -
   7.125 -
   7.126 -
   7.127 -lemma decr_in_cdesc:
   7.128 -  assumes "in_cdesc RD1 y x"
   7.129 -  assumes "in_cdesc RD2 z y"
   7.130 -  assumes "decr RD1 RD2 m1 m2"
   7.131 -  shows "m2 y < m1 x"
   7.132 -  using assms
   7.133 -  by (cases RD1, cases RD2, auto simp:decr_def)
   7.134 -
   7.135 -lemma decreq_in_cdesc:
   7.136 -  assumes "in_cdesc RD1 y x"
   7.137 -  assumes "in_cdesc RD2 z y"
   7.138 -  assumes "decreq RD1 RD2 m1 m2"
   7.139 -  shows "m2 y \<le> m1 x"
   7.140 -  using assms
   7.141 -  by (cases RD1, cases RD2, auto simp:decreq_def)
   7.142 -
   7.143 -
   7.144 -lemma no_inf_desc_nat_sequence:
   7.145 -  fixes s :: "nat \<Rightarrow> nat"
   7.146 -  assumes leq: "\<And>i. n \<le> i \<Longrightarrow> s (Suc i) \<le> s i"
   7.147 -  assumes less: "\<exists>\<^sub>\<infinity>i. s (Suc i) < s i"
   7.148 -  shows False
   7.149 -proof -
   7.150 -  {
   7.151 -    fix i j:: nat 
   7.152 -    assume "n \<le> i"
   7.153 -    assume "i \<le> j"
   7.154 -    {
   7.155 -      fix k 
   7.156 -      have "s (i + k) \<le> s i"
   7.157 -      proof (induct k)
   7.158 -        case 0 thus ?case by simp
   7.159 -      next
   7.160 -        case (Suc k)
   7.161 -        with leq[of "i + k"] `n \<le> i`
   7.162 -        show ?case by simp
   7.163 -      qed
   7.164 -    }
   7.165 -    from this[of "j - i"] `n \<le> i` `i \<le> j`
   7.166 -    have "s j \<le> s i" by auto
   7.167 -  }
   7.168 -  note decr = this
   7.169 -  
   7.170 -  let ?min = "LEAST x. x \<in> range (\<lambda>i. s (n + i))"
   7.171 -  have "?min \<in> range (\<lambda>i. s (n + i))"
   7.172 -    by (rule LeastI) auto
   7.173 -  then obtain k where min: "?min = s (n + k)" by auto
   7.174 -  
   7.175 -  from less 
   7.176 -  obtain k' where "n + k < k'"
   7.177 -    and "s (Suc k') < s k'"
   7.178 -    unfolding INFM_nat by auto
   7.179 -  
   7.180 -  with decr[of "n + k" k'] min
   7.181 -  have "s (Suc k') < ?min" by auto
   7.182 -  moreover from `n + k < k'`
   7.183 -  have "s (Suc k') = s (n + (Suc k' - n))" by simp
   7.184 -  ultimately
   7.185 -  show False using not_less_Least by blast
   7.186 -qed
   7.187 -
   7.188 -
   7.189 -
   7.190 -definition
   7.191 -  approx :: "nat scg \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc 
   7.192 -  \<Rightarrow> 'a measures \<Rightarrow> 'a measures \<Rightarrow> bool"
   7.193 -  where
   7.194 -  "approx G C C' M M'
   7.195 -  = (\<forall>i j. (dsc G i j \<longrightarrow> decr C C' (M i) (M' j))
   7.196 -  \<and>(eqp G i j \<longrightarrow> decreq C C' (M i) (M' j)))"
   7.197 -
   7.198 -
   7.199 -
   7.200 -
   7.201 -(* Unfolding "approx" for finite graphs *)
   7.202 -
   7.203 -lemma approx_empty: 
   7.204 -  "approx (Graph {}) c1 c2 ms1 ms2"
   7.205 -  unfolding approx_def has_edge_def dest_graph.simps by simp
   7.206 -
   7.207 -lemma approx_less:
   7.208 -  assumes "stepP c1 c2 (ms1 i) (ms2 j) (op <)"
   7.209 -  assumes "approx (Graph Es) c1 c2 ms1 ms2"
   7.210 -  shows "approx (Graph (insert (i, \<down>, j) Es)) c1 c2 ms1 ms2"
   7.211 -  using assms
   7.212 -  unfolding approx_def has_edge_def dest_graph.simps decr_def
   7.213 -  by auto
   7.214 -
   7.215 -lemma approx_leq:
   7.216 -  assumes "stepP c1 c2 (ms1 i) (ms2 j) (op \<le>)"
   7.217 -  assumes "approx (Graph Es) c1 c2 ms1 ms2"
   7.218 -  shows "approx (Graph (insert (i, \<Down>, j) Es)) c1 c2 ms1 ms2"
   7.219 -  using assms
   7.220 -  unfolding approx_def has_edge_def dest_graph.simps decreq_def
   7.221 -  by auto
   7.222 -
   7.223 -
   7.224 -lemma "approx (Graph {(1, \<down>, 2),(2, \<Down>, 3)}) c1 c2 ms1 ms2"
   7.225 -  apply (intro approx_less approx_leq approx_empty) 
   7.226 -  oops
   7.227 -
   7.228 -
   7.229 -(*
   7.230 -fun
   7.231 -  no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool"
   7.232 -where
   7.233 -  "no_step (\<Gamma>1, r1, l1) (\<Gamma>2, r2, l2) =
   7.234 -  (\<forall>q\<^isub>1 q\<^isub>2. \<Gamma>1 q\<^isub>1 \<and> \<Gamma>2 q\<^isub>2 \<and> r1 q\<^isub>1 = l2 q\<^isub>2 \<longrightarrow> False)"
   7.235 -*)
   7.236 -
   7.237 -lemma no_stepI:
   7.238 -  "stepP c1 c2 m1 m2 (\<lambda>x y. False)
   7.239 -  \<Longrightarrow> no_step c1 c2"
   7.240 -by (cases c1, cases c2) (auto simp: no_step_def)
   7.241 -
   7.242 -definition
   7.243 -  sound_int :: "nat acg \<Rightarrow> ('a, 'q) cdesc list 
   7.244 -  \<Rightarrow> 'a measures list \<Rightarrow> bool"
   7.245 -where
   7.246 -  "sound_int \<A> RDs M =
   7.247 -  (\<forall>n<length RDs. \<forall>m<length RDs.
   7.248 -  no_step (RDs ! n) (RDs ! m) \<or>
   7.249 -  (\<exists>G. (\<A> \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m) \<and> approx G (RDs ! n) (RDs ! m) (M ! n) (M ! m)))"
   7.250 -
   7.251 -
   7.252 -(* The following are uses by the tactics *)
   7.253 -lemma length_simps: "length [] = 0" "length (x#xs) = Suc (length xs)"
   7.254 -  by auto
   7.255 -
   7.256 -lemma all_less_zero: "\<forall>n<(0::nat). P n"
   7.257 -  by simp
   7.258 -
   7.259 -lemma all_less_Suc:
   7.260 -  assumes Pk: "P k"
   7.261 -  assumes Pn: "\<forall>n<k. P n"
   7.262 -  shows "\<forall>n<Suc k. P n"
   7.263 -proof (intro allI impI)
   7.264 -  fix n assume "n < Suc k"
   7.265 -  show "P n"
   7.266 -  proof (cases "n < k")
   7.267 -    case True with Pn show ?thesis by simp
   7.268 -  next
   7.269 -    case False with `n < Suc k` have "n = k" by simp
   7.270 -    with Pk show ?thesis by simp
   7.271 -  qed
   7.272 -qed
   7.273 -
   7.274 -
   7.275 -lemma step_witness:
   7.276 -  assumes "in_cdesc RD1 y x"
   7.277 -  assumes "in_cdesc RD2 z y"
   7.278 -  shows "\<not> no_step RD1 RD2"
   7.279 -  using assms
   7.280 -  by (cases RD1, cases RD2) (auto simp:no_step_def)
   7.281 -
   7.282 -
   7.283 -theorem SCT_on_relations:
   7.284 -  assumes R: "R = mk_rel RDs"
   7.285 -  assumes sound: "sound_int \<A> RDs M"
   7.286 -  assumes "SCT \<A>"
   7.287 -  shows "\<forall>x. accp R x"
   7.288 -proof (rule, rule classical)
   7.289 -  fix x
   7.290 -  assume "\<not> accp R x"
   7.291 -  with non_acc_has_idseq
   7.292 -  have "\<exists>s. idseq R s x" .
   7.293 -  then obtain s where "idseq R s x" ..
   7.294 -  hence "\<exists>cs. \<forall>i. cs i \<in> set RDs \<and>
   7.295 -    in_cdesc (cs i) (s (Suc i)) (s i)"
   7.296 -    unfolding R by (rule ex_cs) 
   7.297 -  then obtain cs where
   7.298 -    [simp]: "\<And>i. cs i \<in> set RDs"
   7.299 -      and ird[simp]: "\<And>i. in_cdesc (cs i) (s (Suc i)) (s i)"
   7.300 -    by blast
   7.301 -  
   7.302 -  let ?cis = "\<lambda>i. index_of RDs (cs i)"
   7.303 -  have "\<forall>i. \<exists>G. (\<A> \<turnstile> ?cis i \<leadsto>\<^bsup>G\<^esup> (?cis (Suc i)))
   7.304 -    \<and> approx G (RDs ! ?cis i) (RDs ! ?cis (Suc i)) 
   7.305 -    (M ! ?cis i) (M ! ?cis (Suc i))" (is "\<forall>i. \<exists>G. ?P i G")
   7.306 -  proof
   7.307 -    fix i
   7.308 -    let ?n = "?cis i" and ?n' = "?cis (Suc i)"
   7.309 -    
   7.310 -    have "in_cdesc (RDs ! ?n) (s (Suc i)) (s i)"
   7.311 -      "in_cdesc (RDs ! ?n') (s (Suc (Suc i))) (s (Suc i))"
   7.312 -      by (simp_all add:index_of_member)
   7.313 -    with step_witness
   7.314 -    have "\<not> no_step (RDs ! ?n) (RDs ! ?n')" .
   7.315 -    moreover have
   7.316 -      "?n < length RDs" 
   7.317 -      "?n' < length RDs"
   7.318 -      by (simp_all add:index_of_length[symmetric])
   7.319 -    ultimately
   7.320 -    obtain G
   7.321 -      where "\<A> \<turnstile> ?n \<leadsto>\<^bsup>G\<^esup> ?n'"
   7.322 -      and "approx G (RDs ! ?n) (RDs ! ?n') (M ! ?n) (M ! ?n')"
   7.323 -      using sound
   7.324 -      unfolding sound_int_def by auto
   7.325 -    
   7.326 -    thus "\<exists>G. ?P i G" by blast
   7.327 -  qed
   7.328 -  with choice
   7.329 -  have "\<exists>Gs. \<forall>i. ?P i (Gs i)" .
   7.330 -  then obtain Gs where 
   7.331 -    A: "\<And>i. \<A> \<turnstile> ?cis i \<leadsto>\<^bsup>(Gs i)\<^esup> (?cis (Suc i))" 
   7.332 -    and B: "\<And>i. approx (Gs i) (RDs ! ?cis i) (RDs ! ?cis (Suc i)) 
   7.333 -    (M ! ?cis i) (M ! ?cis (Suc i))"
   7.334 -    by blast
   7.335 -  
   7.336 -  let ?p = "\<lambda>i. (?cis i, Gs i)"
   7.337 -  
   7.338 -  from A have "has_ipath \<A> ?p"
   7.339 -    unfolding has_ipath_def
   7.340 -    by auto
   7.341 -  
   7.342 -  with `SCT \<A>` SCT_def 
   7.343 -  obtain th where "is_desc_thread th ?p"
   7.344 -    by auto
   7.345 -  
   7.346 -  then obtain n
   7.347 -    where fr: "\<forall>i\<ge>n. eqlat ?p th i"
   7.348 -    and inf: "\<exists>\<^sub>\<infinity>i. descat ?p th i"
   7.349 -    unfolding is_desc_thread_def by auto
   7.350 -  
   7.351 -  from B
   7.352 -  have approx:
   7.353 -    "\<And>i. approx (Gs i) (cs i) (cs (Suc i)) 
   7.354 -    (M ! ?cis i) (M ! ?cis (Suc i))"
   7.355 -    by (simp add:index_of_member)
   7.356 -  
   7.357 -  let ?seq = "\<lambda>i. (M ! ?cis i) (th i) (s i)"
   7.358 -  
   7.359 -  have "\<And>i. n < i \<Longrightarrow> ?seq (Suc i) \<le> ?seq i"
   7.360 -  proof -
   7.361 -    fix i 
   7.362 -    let ?q1 = "th i" and ?q2 = "th (Suc i)"
   7.363 -    assume "n < i"
   7.364 -    
   7.365 -    with fr have "eqlat ?p th i" by simp 
   7.366 -    hence "dsc (Gs i) ?q1 ?q2 \<or> eqp (Gs i) ?q1 ?q2" 
   7.367 -      by simp
   7.368 -    thus "?seq (Suc i) \<le> ?seq i"
   7.369 -    proof
   7.370 -      assume "dsc (Gs i) ?q1 ?q2"
   7.371 -      
   7.372 -      with approx
   7.373 -      have a:"decr (cs i) (cs (Suc i)) 
   7.374 -        ((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)" 
   7.375 -        unfolding approx_def by auto
   7.376 -      
   7.377 -      show ?thesis
   7.378 -        apply (rule less_imp_le)
   7.379 -        apply (rule decr_in_cdesc[of _ "s (Suc i)" "s i"])
   7.380 -        by (rule ird a)+
   7.381 -    next
   7.382 -      assume "eqp (Gs i) ?q1 ?q2"
   7.383 -      
   7.384 -      with approx
   7.385 -      have a:"decreq (cs i) (cs (Suc i)) 
   7.386 -        ((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)" 
   7.387 -        unfolding approx_def by auto
   7.388 -      
   7.389 -      show ?thesis
   7.390 -        apply (rule decreq_in_cdesc[of _ "s (Suc i)" "s i"])
   7.391 -        by (rule ird a)+
   7.392 -    qed
   7.393 -  qed
   7.394 -  moreover have "\<exists>\<^sub>\<infinity>i. ?seq (Suc i) < ?seq i" unfolding INFM_nat
   7.395 -  proof 
   7.396 -    fix i 
   7.397 -    from inf obtain j where "i < j" and d: "descat ?p th j"
   7.398 -      unfolding INFM_nat by auto
   7.399 -    let ?q1 = "th j" and ?q2 = "th (Suc j)"
   7.400 -    from d have "dsc (Gs j) ?q1 ?q2" by auto
   7.401 -    
   7.402 -    with approx
   7.403 -    have a:"decr (cs j) (cs (Suc j)) 
   7.404 -      ((M ! ?cis j) ?q1) ((M ! ?cis (Suc j)) ?q2)" 
   7.405 -      unfolding approx_def by auto
   7.406 -    
   7.407 -    have "?seq (Suc j) < ?seq j"
   7.408 -      apply (rule decr_in_cdesc[of _ "s (Suc j)" "s j"])
   7.409 -      by (rule ird a)+
   7.410 -    with `i < j` 
   7.411 -    show "\<exists>j. i < j \<and> ?seq (Suc j) < ?seq j" by auto
   7.412 -  qed
   7.413 -  ultimately have False
   7.414 -    by (rule no_inf_desc_nat_sequence[of "Suc n"]) simp
   7.415 -  thus "accp R x" ..
   7.416 -qed
   7.417 -
   7.418 -end
     8.1 --- a/src/HOL/SizeChange/Misc_Tools.thy	Fri Nov 06 13:36:46 2009 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,173 +0,0 @@
     8.4 -(*  Title:      HOL/Library/SCT_Misc.thy
     8.5 -    ID:         $Id$
     8.6 -    Author:     Alexander Krauss, TU Muenchen
     8.7 -*)
     8.8 -
     8.9 -header {* Miscellaneous Tools for Size-Change Termination *}
    8.10 -
    8.11 -theory Misc_Tools
    8.12 -imports Main
    8.13 -begin
    8.14 -
    8.15 -subsection {* Searching in lists *}
    8.16 -
    8.17 -fun index_of :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
    8.18 -where
    8.19 -  "index_of [] c = 0"
    8.20 -| "index_of (x#xs) c = (if x = c then 0 else Suc (index_of xs c))"
    8.21 -
    8.22 -lemma index_of_member: 
    8.23 -  "(x \<in> set l) \<Longrightarrow> (l ! index_of l x = x)"
    8.24 -  by (induct l) auto
    8.25 -
    8.26 -lemma index_of_length:
    8.27 -  "(x \<in> set l) = (index_of l x < length l)"
    8.28 -  by (induct l) auto
    8.29 -
    8.30 -subsection {* Some reasoning tools *}
    8.31 -
    8.32 -lemma three_cases:
    8.33 -  assumes "a1 \<Longrightarrow> thesis"
    8.34 -  assumes "a2 \<Longrightarrow> thesis"
    8.35 -  assumes "a3 \<Longrightarrow> thesis"
    8.36 -  assumes "\<And>R. \<lbrakk>a1 \<Longrightarrow> R; a2 \<Longrightarrow> R; a3 \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
    8.37 -  shows "thesis"
    8.38 -  using assms
    8.39 -  by auto
    8.40 -
    8.41 -
    8.42 -subsection {* Sequences *}
    8.43 -
    8.44 -types
    8.45 -  'a sequence = "nat \<Rightarrow> 'a"
    8.46 -
    8.47 -
    8.48 -subsubsection {* Increasing sequences *}
    8.49 -
    8.50 -definition
    8.51 -  increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
    8.52 -  "increasing s = (\<forall>i j. i < j \<longrightarrow> s i < s j)"
    8.53 -
    8.54 -lemma increasing_strict:
    8.55 -  assumes "increasing s"
    8.56 -  assumes "i < j"
    8.57 -  shows "s i < s j"
    8.58 -  using assms
    8.59 -  unfolding increasing_def by simp
    8.60 -
    8.61 -lemma increasing_weak:
    8.62 -  assumes "increasing s"
    8.63 -  assumes "i \<le> j"
    8.64 -  shows "s i \<le> s j"
    8.65 -  using assms increasing_strict[of s i j]
    8.66 -  by (cases "i < j") auto
    8.67 -
    8.68 -lemma increasing_inc:
    8.69 -  assumes "increasing s"
    8.70 -  shows "n \<le> s n"
    8.71 -proof (induct n)
    8.72 -  case 0 then show ?case by simp
    8.73 -next
    8.74 -  case (Suc n)
    8.75 -  with increasing_strict [OF `increasing s`, of n "Suc n"]
    8.76 -  show ?case by auto
    8.77 -qed
    8.78 -
    8.79 -lemma increasing_bij:
    8.80 -  assumes [simp]: "increasing s"
    8.81 -  shows "(s i < s j) = (i < j)"
    8.82 -proof
    8.83 -  assume "s i < s j"
    8.84 -  show "i < j"
    8.85 -  proof (rule classical)
    8.86 -    assume "\<not> ?thesis"
    8.87 -    hence "j \<le> i" by arith
    8.88 -    with increasing_weak have "s j \<le> s i" by simp
    8.89 -    with `s i < s j` show ?thesis by simp
    8.90 -  qed
    8.91 -qed (simp add:increasing_strict)
    8.92 -
    8.93 -
    8.94 -subsubsection {* Sections induced by an increasing sequence *}
    8.95 -
    8.96 -abbreviation
    8.97 -  "section s i == {s i ..< s (Suc i)}"
    8.98 -
    8.99 -definition
   8.100 -  "section_of s n = (LEAST i. n < s (Suc i))"
   8.101 -
   8.102 -lemma section_help:
   8.103 -  assumes "increasing s"
   8.104 -  shows "\<exists>i. n < s (Suc i)" 
   8.105 -proof -
   8.106 -  have "n \<le> s n"
   8.107 -    using `increasing s` by (rule increasing_inc)
   8.108 -  also have "\<dots> < s (Suc n)"
   8.109 -    using `increasing s` increasing_strict by simp
   8.110 -  finally show ?thesis ..
   8.111 -qed
   8.112 -
   8.113 -lemma section_of2:
   8.114 -  assumes "increasing s"
   8.115 -  shows "n < s (Suc (section_of s n))"
   8.116 -  unfolding section_of_def
   8.117 -  by (rule LeastI_ex) (rule section_help [OF `increasing s`])
   8.118 -
   8.119 -lemma section_of1:
   8.120 -  assumes [simp, intro]: "increasing s"
   8.121 -  assumes "s i \<le> n"
   8.122 -  shows "s (section_of s n) \<le> n"
   8.123 -proof (rule classical)
   8.124 -  let ?m = "section_of s n"
   8.125 -
   8.126 -  assume "\<not> ?thesis"
   8.127 -  hence a: "n < s ?m" by simp
   8.128 -  
   8.129 -  have nonzero: "?m \<noteq> 0"
   8.130 -  proof
   8.131 -    assume "?m = 0"
   8.132 -    from increasing_weak have "s 0 \<le> s i" by simp
   8.133 -    also note `\<dots> \<le> n`
   8.134 -    finally show False using `?m = 0` `n < s ?m` by simp 
   8.135 -  qed
   8.136 -  with a have "n < s (Suc (?m - 1))" by simp
   8.137 -  with Least_le have "?m \<le> ?m - 1"
   8.138 -    unfolding section_of_def .
   8.139 -  with nonzero show ?thesis by simp
   8.140 -qed
   8.141 -
   8.142 -lemma section_of_known: 
   8.143 -  assumes [simp]: "increasing s"
   8.144 -  assumes in_sect: "k \<in> section s i"
   8.145 -  shows "section_of s k = i" (is "?s = i")
   8.146 -proof (rule classical)
   8.147 -  assume "\<not> ?thesis"
   8.148 -
   8.149 -  hence "?s < i \<or> ?s > i" by arith
   8.150 -  thus ?thesis
   8.151 -  proof
   8.152 -    assume "?s < i"
   8.153 -    hence "Suc ?s \<le> i" by simp
   8.154 -    with increasing_weak have "s (Suc ?s) \<le> s i" by simp
   8.155 -    moreover have "k < s (Suc ?s)" using section_of2 by simp
   8.156 -    moreover from in_sect have "s i \<le> k" by simp
   8.157 -    ultimately show ?thesis by simp 
   8.158 -  next
   8.159 -    assume "i < ?s" hence "Suc i \<le> ?s" by simp
   8.160 -    with increasing_weak have "s (Suc i) \<le> s ?s" by simp
   8.161 -    moreover 
   8.162 -    from in_sect have "s i \<le> k" by simp
   8.163 -    with section_of1 have "s ?s \<le> k" by simp
   8.164 -    moreover from in_sect have "k < s (Suc i)" by simp
   8.165 -    ultimately show ?thesis by simp
   8.166 -  qed
   8.167 -qed 
   8.168 -  
   8.169 -lemma in_section_of: 
   8.170 -  assumes "increasing s"
   8.171 -  assumes "s i \<le> k"
   8.172 -  shows "k \<in> section s (section_of s k)"
   8.173 -  using assms
   8.174 -  by (auto intro:section_of1 section_of2)
   8.175 -
   8.176 -end
     9.1 --- a/src/HOL/SizeChange/ROOT.ML	Fri Nov 06 13:36:46 2009 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,7 +0,0 @@
     9.4 -(*  Title:      HOL/SizeChange/ROOT.ML
     9.5 -    ID:         $Id$
     9.6 -*)
     9.7 -
     9.8 -no_document use_thy "Infinite_Set";
     9.9 -no_document use_thy "Ramsey";
    9.10 -use_thy "Examples";
    10.1 --- a/src/HOL/SizeChange/Size_Change_Termination.thy	Fri Nov 06 13:36:46 2009 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,110 +0,0 @@
    10.4 -(*  Title:      HOL/Library/Size_Change_Termination.thy
    10.5 -    Author:     Alexander Krauss, TU Muenchen
    10.6 -*)
    10.7 -
    10.8 -header "Size-Change Termination"
    10.9 -
   10.10 -theory Size_Change_Termination
   10.11 -imports Correctness Interpretation Implementation 
   10.12 -uses "sct.ML"
   10.13 -begin
   10.14 -
   10.15 -subsection {* Simplifier setup *}
   10.16 -
   10.17 -text {* This is needed to run the SCT algorithm in the simplifier: *}
   10.18 -
   10.19 -lemma setbcomp_simps:
   10.20 -  "{x\<in>{}. P x} = {}"
   10.21 -  "{x\<in>insert y ys. P x} = (if P y then insert y {x\<in>ys. P x} else {x\<in>ys. P x})"
   10.22 -  by auto
   10.23 -
   10.24 -lemma setbcomp_cong:
   10.25 -  "A = B \<Longrightarrow> (\<And>x. P x = Q x) \<Longrightarrow> {x\<in>A. P x} = {x\<in>B. Q x}"
   10.26 -  by auto
   10.27 -
   10.28 -lemma cartprod_simps:
   10.29 -  "{} \<times> A = {}"
   10.30 -  "insert a A \<times> B = Pair a ` B \<union> (A \<times> B)"
   10.31 -  by (auto simp:image_def)
   10.32 -
   10.33 -lemma image_simps:
   10.34 -  "fu ` {} = {}"
   10.35 -  "fu ` insert a A = insert (fu a) (fu ` A)"
   10.36 -  by (auto simp:image_def)
   10.37 -
   10.38 -lemmas union_simps = 
   10.39 -  Un_empty_left Un_empty_right Un_insert_left
   10.40 -  
   10.41 -lemma subset_simps:
   10.42 -  "{} \<subseteq> B"
   10.43 -  "insert a A \<subseteq> B \<equiv> a \<in> B \<and> A \<subseteq> B"
   10.44 -  by auto 
   10.45 -
   10.46 -lemma element_simps:
   10.47 -  "x \<in> {} \<equiv> False"
   10.48 -  "x \<in> insert a A \<equiv> x = a \<or> x \<in> A"
   10.49 -  by auto
   10.50 -
   10.51 -lemma set_eq_simp:
   10.52 -  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" by auto
   10.53 -
   10.54 -lemma ball_simps:
   10.55 -  "\<forall>x\<in>{}. P x \<equiv> True"
   10.56 -  "(\<forall>x\<in>insert a A. P x) \<equiv> P a \<and> (\<forall>x\<in>A. P x)"
   10.57 -by auto
   10.58 -
   10.59 -lemma bex_simps:
   10.60 -  "\<exists>x\<in>{}. P x \<equiv> False"
   10.61 -  "(\<exists>x\<in>insert a A. P x) \<equiv> P a \<or> (\<exists>x\<in>A. P x)"
   10.62 -by auto
   10.63 -
   10.64 -lemmas set_simps =
   10.65 -  setbcomp_simps
   10.66 -  cartprod_simps image_simps union_simps subset_simps
   10.67 -  element_simps set_eq_simp
   10.68 -  ball_simps bex_simps
   10.69 -
   10.70 -lemma sedge_simps:
   10.71 -  "\<down> * x = \<down>"
   10.72 -  "\<Down> * x = x"
   10.73 -  by (auto simp:mult_sedge_def)
   10.74 -
   10.75 -lemmas sctTest_simps =
   10.76 -  simp_thms
   10.77 -  if_True
   10.78 -  if_False
   10.79 -  nat.inject
   10.80 -  nat.distinct
   10.81 -  Pair_eq 
   10.82 -
   10.83 -  grcomp_code 
   10.84 -  edges_match.simps 
   10.85 -  connect_edges.simps 
   10.86 -
   10.87 -  sedge_simps
   10.88 -  sedge.distinct
   10.89 -  set_simps
   10.90 -
   10.91 -  graph_mult_def 
   10.92 -  graph_leq_def
   10.93 -  dest_graph.simps
   10.94 -  graph_plus_def
   10.95 -  graph.inject
   10.96 -  graph_zero_def
   10.97 -
   10.98 -  test_SCT_def
   10.99 -  mk_tcl_code
  10.100 -
  10.101 -  Let_def
  10.102 -  split_conv
  10.103 -
  10.104 -lemmas sctTest_congs = 
  10.105 -  if_weak_cong let_weak_cong setbcomp_cong
  10.106 -
  10.107 -
  10.108 -lemma SCT_Main:
  10.109 -  "finite_acg A \<Longrightarrow> test_SCT A \<Longrightarrow> SCT A"
  10.110 -  using LJA_Theorem4 SCT'_exec
  10.111 -  by auto
  10.112 -
  10.113 -end
    11.1 --- a/src/HOL/SizeChange/document/root.tex	Fri Nov 06 13:36:46 2009 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,28 +0,0 @@
    11.4 -
    11.5 -% $Id$
    11.6 -
    11.7 -\documentclass[11pt,a4paper]{article}
    11.8 -\usepackage{latexsym}
    11.9 -\usepackage{isabelle,isabellesym}
   11.10 -
   11.11 -% this should be the last package used
   11.12 -\usepackage{pdfsetup}
   11.13 -
   11.14 -% urls in roman style, theory text in math-similar italics
   11.15 -\urlstyle{rm}
   11.16 -\isabellestyle{it}
   11.17 -
   11.18 -
   11.19 -\begin{document}
   11.20 -
   11.21 -\title{Size-Change Termination}
   11.22 -\author{Alexander Krauss}
   11.23 -\maketitle
   11.24 -
   11.25 -%\tableofcontents
   11.26 -
   11.27 -\parindent 0pt\parskip 0.5ex
   11.28 -
   11.29 -\input{session}
   11.30 -
   11.31 -\end{document}
    12.1 --- a/src/HOL/SizeChange/sct.ML	Fri Nov 06 13:36:46 2009 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,351 +0,0 @@
    12.4 -(*  Title:      HOL/SizeChange/sct.ML
    12.5 -    Author:     Alexander Krauss, TU Muenchen
    12.6 -
    12.7 -Tactics for size change termination.
    12.8 -*)
    12.9 -signature SCT =
   12.10 -sig
   12.11 -  val abs_rel_tac : tactic
   12.12 -  val mk_call_graph : Proof.context -> tactic
   12.13 -end
   12.14 -
   12.15 -structure Sct : SCT =
   12.16 -struct
   12.17 -
   12.18 -fun matrix [] ys = []
   12.19 -  | matrix (x::xs) ys = map (pair x) ys :: matrix xs ys
   12.20 -
   12.21 -fun map_matrix f xss = map (map f) xss
   12.22 -
   12.23 -val scgT = @{typ "nat scg"}
   12.24 -val acgT = @{typ "nat acg"}
   12.25 -
   12.26 -fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT))
   12.27 -fun graphT nT eT = Type ("Graphs.graph", [nT, eT])
   12.28 -
   12.29 -fun graph_const nT eT = Const ("Graphs.graph.Graph", HOLogic.mk_setT (edgeT nT eT) --> graphT nT eT)
   12.30 -
   12.31 -val stepP_const = "Interpretation.stepP"
   12.32 -val stepP_def = thm "Interpretation.stepP.simps"
   12.33 -
   12.34 -fun mk_stepP RD1 RD2 M1 M2 Rel =
   12.35 -    let val RDT = fastype_of RD1
   12.36 -      val MT = fastype_of M1
   12.37 -    in
   12.38 -      Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT)
   12.39 -            $ RD1 $ RD2 $ M1 $ M2 $ Rel
   12.40 -    end
   12.41 -
   12.42 -val no_stepI = thm "Interpretation.no_stepI"
   12.43 -
   12.44 -val approx_const = "Interpretation.approx"
   12.45 -val approx_empty = thm "Interpretation.approx_empty"
   12.46 -val approx_less = thm "Interpretation.approx_less"
   12.47 -val approx_leq = thm "Interpretation.approx_leq"
   12.48 -
   12.49 -fun mk_approx G RD1 RD2 Ms1 Ms2 =
   12.50 -    let val RDT = fastype_of RD1
   12.51 -      val MsT = fastype_of Ms1
   12.52 -    in Const (approx_const, scgT --> RDT --> RDT --> MsT --> MsT --> HOLogic.boolT) $ G $ RD1 $ RD2 $ Ms1 $ Ms2 end
   12.53 -
   12.54 -val sound_int_const = "Interpretation.sound_int"
   12.55 -val sound_int_def = thm "Interpretation.sound_int_def"
   12.56 -fun mk_sound_int A RDs M =
   12.57 -    let val RDsT = fastype_of RDs
   12.58 -      val MT = fastype_of M
   12.59 -    in Const (sound_int_const, acgT --> RDsT --> MT --> HOLogic.boolT) $ A $ RDs $ M end
   12.60 -
   12.61 -
   12.62 -val nth_const = "List.nth"
   12.63 -fun mk_nth xs =
   12.64 -    let val lT as Type (_, [T]) = fastype_of xs
   12.65 -    in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end
   12.66 -
   12.67 -
   12.68 -val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
   12.69 -
   12.70 -val all_less_zero = thm "Interpretation.all_less_zero"
   12.71 -val all_less_Suc = thm "Interpretation.all_less_Suc"
   12.72 -
   12.73 -(* --> Library? *)
   12.74 -fun del_index n [] = []
   12.75 -  | del_index n (x :: xs) =
   12.76 -    if n>0 then x :: del_index (n - 1) xs else xs
   12.77 -
   12.78 -(* Lists as finite multisets *)
   12.79 -
   12.80 -fun remove1 eq x [] = []
   12.81 -  | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys
   12.82 -
   12.83 -fun multi_union eq [] ys = ys
   12.84 -  | multi_union eq (x::xs) ys = x :: multi_union eq xs (remove1 eq x ys)
   12.85 -
   12.86 -fun dest_ex (Const ("Ex", _) $ Abs (a as (_,T,_))) =
   12.87 -    let
   12.88 -      val (n, body) = Term.dest_abs a
   12.89 -    in
   12.90 -      (Free (n, T), body)
   12.91 -    end
   12.92 -  | dest_ex _ = raise Match
   12.93 -
   12.94 -fun dest_all_ex (t as (Const ("Ex",_) $ _)) =
   12.95 -    let
   12.96 -      val (v,b) = dest_ex t
   12.97 -      val (vs, b') = dest_all_ex b
   12.98 -    in
   12.99 -      (v :: vs, b')
  12.100 -    end
  12.101 -  | dest_all_ex t = ([],t)
  12.102 -
  12.103 -fun dist_vars [] vs = (null vs orelse error "dist_vars"; [])
  12.104 -  | dist_vars (T::Ts) vs =
  12.105 -    case find_index (fn v => fastype_of v = T) vs of
  12.106 -      ~1 => Free ("", T) :: dist_vars Ts vs
  12.107 -    |  i => (nth vs i) :: dist_vars Ts (del_index i vs)
  12.108 -
  12.109 -fun dest_case rebind t =
  12.110 -    let
  12.111 -      val ((_ $ _ $ rhs) :: (_ $ _ $ match) :: guards) = HOLogic.dest_conj t
  12.112 -      val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs
  12.113 -    in
  12.114 -      foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match]
  12.115 -    end
  12.116 -
  12.117 -fun bind_many [] = I
  12.118 -  | bind_many vs = Function_Lib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
  12.119 -
  12.120 -(* Builds relation descriptions from a relation definition *)
  12.121 -fun mk_reldescs (Abs a) =
  12.122 -    let
  12.123 -      val (_, Abs a') = Term.dest_abs a
  12.124 -      val (_, b) = Term.dest_abs a'
  12.125 -      val cases = HOLogic.dest_disj b
  12.126 -      val (vss, bs) = split_list (map dest_all_ex cases)
  12.127 -      val unionTs = fold (multi_union (op =)) (map (map fastype_of) vss) []
  12.128 -      val rebind = map (bind_many o dist_vars unionTs) vss
  12.129 -
  12.130 -      val RDs = map2 dest_case rebind bs
  12.131 -    in
  12.132 -      HOLogic.mk_list (fastype_of (hd RDs)) RDs
  12.133 -    end
  12.134 -
  12.135 -fun abs_rel_tac (st : thm) =
  12.136 -    let
  12.137 -      val thy = theory_of_thm st
  12.138 -      val (def, rd) = HOLogic.dest_eq (HOLogic.dest_Trueprop (hd (prems_of st)))
  12.139 -      val RDs = cterm_of thy (mk_reldescs def)
  12.140 -      val rdvar = Var (the_single (Term.add_vars rd [])) |> cterm_of thy
  12.141 -    in
  12.142 -      Seq.single (cterm_instantiate [(rdvar, RDs)] st)
  12.143 -    end
  12.144 -
  12.145 -
  12.146 -
  12.147 -
  12.148 -
  12.149 -
  12.150 -(* very primitive *)
  12.151 -fun measures_of ctxt RD =
  12.152 -    let
  12.153 -      val domT = range_type (fastype_of (fst (HOLogic.dest_prod (snd (HOLogic.dest_prod RD)))))
  12.154 -      val measures = MeasureFunctions.get_measure_functions ctxt domT
  12.155 -    in
  12.156 -      measures
  12.157 -    end
  12.158 -
  12.159 -val mk_number = HOLogic.mk_nat
  12.160 -val dest_number = HOLogic.dest_nat
  12.161 -
  12.162 -fun nums_to i = map_range mk_number i
  12.163 -
  12.164 -val nth_simps = [@{thm List.nth_Cons_0}, @{thm List.nth_Cons_Suc}]
  12.165 -val nth_ss = (HOL_basic_ss addsimps nth_simps)
  12.166 -val simp_nth_tac = simp_tac nth_ss
  12.167 -
  12.168 -
  12.169 -fun tabulate_tlist thy l =
  12.170 -    let
  12.171 -      val n = length (HOLogic.dest_list l)
  12.172 -      val table = Inttab.make (map_range (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) n)
  12.173 -    in
  12.174 -      the o Inttab.lookup table
  12.175 -    end
  12.176 -
  12.177 -val get_elem = snd o Logic.dest_equals o prop_of
  12.178 -
  12.179 -fun inst_nums thy i j (t:thm) =
  12.180 -  instantiate' [] [NONE, NONE, NONE, SOME (cterm_of thy (mk_number i)), NONE, SOME (cterm_of thy (mk_number j))] t
  12.181 -
  12.182 -datatype call_fact =
  12.183 -   NoStep of thm
  12.184 - | Graph of (term * thm)
  12.185 -
  12.186 -fun rand (_ $ t) = t
  12.187 -
  12.188 -fun setup_probe_goal ctxt domT Dtab Mtab (i, j) =
  12.189 -    let
  12.190 -      val css = clasimpset_of ctxt
  12.191 -      val thy = ProofContext.theory_of ctxt
  12.192 -      val RD1 = get_elem (Dtab i)
  12.193 -      val RD2 = get_elem (Dtab j)
  12.194 -      val Ms1 = get_elem (Mtab i)
  12.195 -      val Ms2 = get_elem (Mtab j)
  12.196 -
  12.197 -      val Mst1 = HOLogic.dest_list (rand Ms1)
  12.198 -      val Mst2 = HOLogic.dest_list (rand Ms2)
  12.199 -
  12.200 -      val mvar1 = Free ("sctmfv1", domT --> HOLogic.natT)
  12.201 -      val mvar2 = Free ("sctmfv2", domT --> HOLogic.natT)
  12.202 -      val relvar = Free ("sctmfrel", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
  12.203 -      val N = length Mst1 and M = length Mst2
  12.204 -      val saved_state = HOLogic.mk_Trueprop (mk_stepP RD1 RD2 mvar1 mvar2 relvar)
  12.205 -                         |> cterm_of thy
  12.206 -                         |> Goal.init
  12.207 -                         |> auto_tac css |> Seq.hd
  12.208 -
  12.209 -      val no_step = saved_state
  12.210 -                      |> forall_intr (cterm_of thy relvar)
  12.211 -                      |> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const))))
  12.212 -                      |> auto_tac css |> Seq.hd
  12.213 -
  12.214 -    in
  12.215 -      if Thm.no_prems no_step
  12.216 -      then NoStep (Goal.finish ctxt no_step RS no_stepI)
  12.217 -      else
  12.218 -        let
  12.219 -          fun set_m1 i =
  12.220 -              let
  12.221 -                val M1 = nth Mst1 i
  12.222 -                val with_m1 = saved_state
  12.223 -                                |> forall_intr (cterm_of thy mvar1)
  12.224 -                                |> forall_elim (cterm_of thy M1)
  12.225 -                                |> auto_tac css |> Seq.hd
  12.226 -
  12.227 -                fun set_m2 j =
  12.228 -                    let
  12.229 -                      val M2 = nth Mst2 j
  12.230 -                      val with_m2 = with_m1
  12.231 -                                      |> forall_intr (cterm_of thy mvar2)
  12.232 -                                      |> forall_elim (cterm_of thy M2)
  12.233 -                                      |> auto_tac css |> Seq.hd
  12.234 -
  12.235 -                      val decr = forall_intr (cterm_of thy relvar)
  12.236 -                                   #> forall_elim (cterm_of thy @{const HOL.less(nat)})
  12.237 -                                   #> auto_tac css #> Seq.hd
  12.238 -
  12.239 -                      val decreq = forall_intr (cterm_of thy relvar)
  12.240 -                                     #> forall_elim (cterm_of thy @{const HOL.less_eq(nat)})
  12.241 -                                     #> auto_tac css #> Seq.hd
  12.242 -
  12.243 -                      val thm1 = decr with_m2
  12.244 -                    in
  12.245 -                      if Thm.no_prems thm1
  12.246 -                      then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish ctxt thm1) 1))
  12.247 -                      else let val thm2 = decreq with_m2 in
  12.248 -                             if Thm.no_prems thm2
  12.249 -                             then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish ctxt thm2) 1))
  12.250 -                             else all_tac end
  12.251 -                    end
  12.252 -              in set_m2 end
  12.253 -
  12.254 -          val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2)
  12.255 -
  12.256 -          val tac = (EVERY (map_range (fn n => EVERY (map_range (set_m1 n) M)) N))
  12.257 -                      THEN (rtac approx_empty 1)
  12.258 -
  12.259 -          val approx_thm = goal
  12.260 -                    |> cterm_of thy
  12.261 -                    |> Goal.init
  12.262 -                    |> tac |> Seq.hd
  12.263 -                    |> Goal.finish ctxt
  12.264 -
  12.265 -          val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm
  12.266 -        in
  12.267 -          Graph (G, approx_thm)
  12.268 -        end
  12.269 -    end
  12.270 -
  12.271 -fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n))
  12.272 -
  12.273 -fun in_graph_tac ctxt =
  12.274 -    simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
  12.275 -    THEN (simp_tac (simpset_of ctxt) 1) (* FIXME reduce simpset *)
  12.276 -
  12.277 -fun approx_tac _ (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
  12.278 -  | approx_tac ctxt (Graph (G, thm)) =
  12.279 -    rtac disjI2 1
  12.280 -    THEN rtac exI 1
  12.281 -    THEN rtac conjI 1
  12.282 -    THEN rtac thm 2
  12.283 -    THEN (in_graph_tac ctxt)
  12.284 -
  12.285 -fun all_less_tac [] = rtac all_less_zero 1
  12.286 -  | all_less_tac (t :: ts) = rtac all_less_Suc 1
  12.287 -                                  THEN simp_nth_tac 1
  12.288 -                                  THEN t
  12.289 -                                  THEN all_less_tac ts
  12.290 -
  12.291 -
  12.292 -fun mk_length l = HOLogic.size_const (fastype_of l) $ l;
  12.293 -val length_simps = thms "Interpretation.length_simps"
  12.294 -
  12.295 -
  12.296 -
  12.297 -fun mk_call_graph ctxt (st : thm) =
  12.298 -    let
  12.299 -      val thy = ProofContext.theory_of ctxt
  12.300 -      val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
  12.301 -
  12.302 -      val RDs = HOLogic.dest_list RDlist
  12.303 -      val n = length RDs
  12.304 -
  12.305 -      val Mss = map (measures_of ctxt) RDs
  12.306 -
  12.307 -      val domT = domain_type (fastype_of (hd (hd Mss)))
  12.308 -
  12.309 -      val mfuns = map (fn Ms => mk_nth (HOLogic.mk_list (fastype_of (hd Ms)) Ms)) Mss
  12.310 -                      |> (fn l => HOLogic.mk_list (fastype_of (hd l)) l)
  12.311 -
  12.312 -      val Dtab = tabulate_tlist thy RDlist
  12.313 -      val Mtab = tabulate_tlist thy mfuns
  12.314 -
  12.315 -      val len_simp = Simplifier.rewrite (HOL_basic_ss addsimps length_simps) (cterm_of thy (mk_length RDlist))
  12.316 -
  12.317 -      val mlens = map length Mss
  12.318 -
  12.319 -      val indices = (n - 1 downto 0)
  12.320 -      val pairs = matrix indices indices
  12.321 -      val parts = map_matrix (fn (n,m) =>
  12.322 -                                 (timeap_msg (string_of_int n ^ "," ^ string_of_int m)
  12.323 -                                             (setup_probe_goal ctxt domT Dtab Mtab) (n,m))) pairs
  12.324 -
  12.325 -
  12.326 -      val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^
  12.327 -                                                                            Syntax.string_of_term ctxt G ^ ",\n")
  12.328 -                                                     | _ => I) cs) parts ""
  12.329 -      val _ = warning s
  12.330 -
  12.331 -
  12.332 -      val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs)
  12.333 -                    |> HOLogic.mk_set (edgeT HOLogic.natT scgT)
  12.334 -                    |> curry op $ (graph_const HOLogic.natT scgT)
  12.335 -
  12.336 -
  12.337 -      val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns)
  12.338 -
  12.339 -      val tac =
  12.340 -          unfold_tac [sound_int_def, len_simp] (simpset_of ctxt)
  12.341 -            THEN all_less_tac (map (all_less_tac o map (approx_tac ctxt)) parts)
  12.342 -    in
  12.343 -      tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
  12.344 -    end
  12.345 -
  12.346 -
  12.347 -end
  12.348 -
  12.349 -
  12.350 -
  12.351 -
  12.352 -
  12.353 -
  12.354 -