Added formalization of size-change principle (experimental).
authorkrauss
Mon Feb 26 21:34:16 2007 +0100 (2007-02-26)
changeset 2235994a794672c8b
parent 22358 4d8a9e3a29f8
child 22360 26ead7ed4f4b
Added formalization of size-change principle (experimental).
src/HOL/IsaMakefile
src/HOL/Library/Graphs.thy
src/HOL/Library/Kleene_Algebras.thy
src/HOL/Library/Library.thy
src/HOL/Library/Library/ROOT.ML
src/HOL/Library/SCT_Definition.thy
src/HOL/Library/SCT_Examples.thy
src/HOL/Library/SCT_Implementation.thy
src/HOL/Library/SCT_Interpretation.thy
src/HOL/Library/SCT_Misc.thy
src/HOL/Library/SCT_Theorem.thy
src/HOL/Library/Size_Change_Termination.thy
src/HOL/Library/size_change_termination.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Feb 26 20:14:52 2007 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Feb 26 21:34:16 2007 +0100
     1.3 @@ -207,7 +207,11 @@
     1.4    Library/Product_ord.thy Library/Char_ord.thy \
     1.5    Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
     1.6    Library/Coinductive_List.thy Library/AssocList.thy \
     1.7 -  Library/Parity.thy Library/GCD.thy Library/Binomial.thy
     1.8 +  Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
     1.9 +  Library/Graphs.thy Library/Kleene_Algebras.thy Library/SCT_Misc.thy \
    1.10 +  Library/SCT_Definition.thy Library/SCT_Theorem.thy Library/SCT_Interpretation.thy \
    1.11 +  Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
    1.12 +  Library/SCT_Examples.thy
    1.13  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
    1.14  
    1.15  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Graphs.thy	Mon Feb 26 21:34:16 2007 +0100
     2.3 @@ -0,0 +1,721 @@
     2.4 +theory Graphs
     2.5 +imports Main SCT_Misc Kleene_Algebras ExecutableSet
     2.6 +begin
     2.7 +
     2.8 +
     2.9 +section {* Basic types, Size Change Graphs *}
    2.10 +
    2.11 +datatype ('a, 'b) graph = 
    2.12 +  Graph "('a \<times> 'b \<times> 'a) set"
    2.13 +
    2.14 +fun dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"
    2.15 +  where "dest_graph (Graph G) = G"
    2.16 +
    2.17 +lemma graph_dest_graph[simp]:
    2.18 +  "Graph (dest_graph G) = G"
    2.19 +  by (cases G) simp
    2.20 +
    2.21 +definition 
    2.22 +  has_edge :: "('n,'e) graph \<Rightarrow> 'n \<Rightarrow> 'e \<Rightarrow> 'n \<Rightarrow> bool"
    2.23 +("_ \<turnstile> _ \<leadsto>\<^bsup>_\<^esup> _")
    2.24 +where
    2.25 +  "has_edge G n e n' = ((n, e, n') \<in> dest_graph G)"
    2.26 +
    2.27 +
    2.28 +
    2.29 +section {* Graph composition *}
    2.30 +
    2.31 +fun grcomp :: "('n, 'e::times) graph \<Rightarrow> ('n, 'e) graph  \<Rightarrow> ('n, 'e) graph"
    2.32 +where
    2.33 +  "grcomp (Graph G) (Graph H) = 
    2.34 +  Graph {(p,b,q) | p b q. 
    2.35 +  (\<exists>k e e'. (p,e,k)\<in>G \<and> (k,e',q)\<in>H \<and> b = e * e')}"
    2.36 +
    2.37 +
    2.38 +declare grcomp.simps[code del]
    2.39 +
    2.40 +
    2.41 +lemma graph_ext:
    2.42 +  assumes "\<And>n e n'. has_edge G n e n' = has_edge H n e n'"
    2.43 +  shows "G = H"
    2.44 +  using prems
    2.45 +  by (cases G, cases H, auto simp:split_paired_all has_edge_def)
    2.46 +
    2.47 +
    2.48 +instance graph :: (type, times) times 
    2.49 +  graph_mult_def: "G * H == grcomp G H" ..
    2.50 +
    2.51 +instance graph :: (type, one) one 
    2.52 +  graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
    2.53 +
    2.54 +instance graph :: (type, type) zero 
    2.55 +  graph_zero_def: "0 == Graph {}" ..
    2.56 +
    2.57 +instance graph :: (type, type) plus 
    2.58 +  graph_plus_def: "G + H == Graph (dest_graph G \<union> dest_graph H)" ..
    2.59 +
    2.60 +
    2.61 +subsection {* Simprules for the graph operations *}
    2.62 +
    2.63 +lemma in_grcomp:
    2.64 +  "has_edge (G * H) p b q
    2.65 +  = (\<exists>k e e'. has_edge G p e k \<and> has_edge H k e' q \<and> b = e * e')"
    2.66 +  by (cases G, cases H) (auto simp:graph_mult_def has_edge_def image_def)
    2.67 +
    2.68 +lemma in_grunit:
    2.69 +  "has_edge 1 p b q = (p = q \<and> b = 1)"
    2.70 +  by (auto simp:graph_one_def has_edge_def)
    2.71 +
    2.72 +lemma in_grplus:
    2.73 +  "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
    2.74 +  by (cases G, cases H, auto simp:has_edge_def graph_plus_def)
    2.75 +
    2.76 +lemma in_grzero:
    2.77 +  "has_edge 0 p b q = False"
    2.78 +  by (simp add:graph_zero_def has_edge_def)
    2.79 +
    2.80 +
    2.81 +instance graph :: (type, semigroup_mult) semigroup_mult
    2.82 +proof
    2.83 +  fix G1 G2 G3 :: "('a,'b) graph"
    2.84 +  
    2.85 +  show "G1 * G2 * G3 = G1 * (G2 * G3)"
    2.86 +  proof (rule graph_ext, rule trans)
    2.87 +    fix p J q
    2.88 +    show "has_edge ((G1 * G2) * G3) p J q =
    2.89 +      (\<exists>G i H j I.
    2.90 +      has_edge G1 p G i
    2.91 +      \<and> has_edge G2 i H j
    2.92 +      \<and> has_edge G3 j I q
    2.93 +      \<and> J = (G * H) * I)"
    2.94 +      by (simp only:in_grcomp) blast
    2.95 +    show "\<dots> = has_edge (G1 * (G2 * G3)) p J q"
    2.96 +      by (simp only:in_grcomp mult_assoc) blast
    2.97 +  qed
    2.98 +qed
    2.99 +
   2.100 +instance graph :: (type, monoid_mult) monoid_mult
   2.101 +proof
   2.102 +  fix G1 G2 G3 :: "('a,'b) graph"
   2.103 +  
   2.104 +  show "1 * G1 = G1" 
   2.105 +    by (rule graph_ext) (auto simp:in_grcomp in_grunit)
   2.106 +  show "G1 * 1 = G1"
   2.107 +    by (rule graph_ext) (auto simp:in_grcomp in_grunit)
   2.108 +qed
   2.109 +
   2.110 +
   2.111 +lemma grcomp_rdist:
   2.112 +  fixes G :: "('a::type, 'b::semigroup_mult) graph"
   2.113 +  shows "G * (H + I) = G * H + G * I"
   2.114 +  by (rule graph_ext, simp add:in_grcomp in_grplus) blast
   2.115 +
   2.116 +lemma grcomp_ldist:
   2.117 +  fixes G :: "('a::type, 'b::semigroup_mult) graph"
   2.118 +  shows "(G + H) * I = G * I + H * I"
   2.119 +  by (rule graph_ext, simp add:in_grcomp in_grplus) blast
   2.120 +
   2.121 +fun grpow :: "nat \<Rightarrow> ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a, 'b) graph"
   2.122 +where
   2.123 +  "grpow 0 A = 1"
   2.124 +| "grpow (Suc n) A = A * (grpow n A)"
   2.125 +
   2.126 +
   2.127 +instance graph :: (type, monoid_mult) recpower 
   2.128 +  graph_pow_def: "A ^ n == grpow n A" 
   2.129 +  by default (simp_all add:graph_pow_def)
   2.130 +
   2.131 +subsection {* Order on Graphs *}
   2.132 +
   2.133 +instance graph :: (type, type) ord 
   2.134 +  graph_leq_def: "G \<le> H == dest_graph G \<subseteq> dest_graph H"
   2.135 +  graph_less_def: "G < H == dest_graph G \<subset> dest_graph H" ..
   2.136 +
   2.137 +instance graph :: (type, type) order
   2.138 +proof
   2.139 +  fix x y z :: "('a,'b) graph"
   2.140 +
   2.141 +  show "x \<le> x" unfolding graph_leq_def ..
   2.142 +  
   2.143 +  from order_trans
   2.144 +  show "\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z" unfolding graph_leq_def .
   2.145 +
   2.146 +  show "\<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" unfolding graph_leq_def 
   2.147 +    by (cases x, cases y) simp
   2.148 +
   2.149 +  show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
   2.150 +    unfolding graph_leq_def graph_less_def
   2.151 +    by (cases x, cases y) auto
   2.152 +qed
   2.153 +
   2.154 +
   2.155 +defs (overloaded)
   2.156 +  Meet_graph_def: "Meet == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
   2.157 +
   2.158 +instance graph :: (type, type) comp_lat
   2.159 +  by default (auto simp:Meet_graph_def is_join_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
   2.160 +
   2.161 +lemma plus_graph_is_join: "is_join ((op +)::('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
   2.162 +  unfolding is_join_def 
   2.163 +proof (intro allI conjI impI)
   2.164 +  fix a b x :: "('a, 'b) graph"
   2.165 +
   2.166 +  show "a \<le> a + b" "b \<le> a + b" "a \<le> x \<and> b \<le> x \<Longrightarrow> a + b \<le> x"
   2.167 +    unfolding graph_leq_def graph_plus_def
   2.168 +    by (cases a, cases b) auto
   2.169 +qed
   2.170 +
   2.171 +lemma plus_is_join:
   2.172 +  "(op +) =
   2.173 +  (join :: ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
   2.174 +  using plus_graph_is_join by (simp add:join_unique)
   2.175 +
   2.176 +instance graph :: (type, monoid_mult) semiring_1
   2.177 +proof
   2.178 +  fix a b c :: "('a, 'b) graph"
   2.179 +
   2.180 +  show "a + b + c = a + (b + c)" 
   2.181 +    and "a + b = b + a" unfolding graph_plus_def
   2.182 +    by auto
   2.183 +
   2.184 +  show "0 + a = a" unfolding graph_zero_def graph_plus_def
   2.185 +    by simp
   2.186 +
   2.187 +  show "0 * a = 0" "a * 0 = 0" unfolding graph_zero_def graph_mult_def
   2.188 +    by (cases a, simp)+
   2.189 +
   2.190 +  show "(a + b) * c = a * c + b * c"
   2.191 +    by (rule graph_ext, simp add:in_grcomp in_grplus) blast
   2.192 +
   2.193 +  show "a * (b + c) = a * b + a * c"
   2.194 +    by (rule graph_ext, simp add:in_grcomp in_grplus) blast
   2.195 +
   2.196 +  show "(0::('a,'b) graph) \<noteq> 1" unfolding graph_zero_def graph_one_def
   2.197 +    by simp
   2.198 +qed
   2.199 +
   2.200 +
   2.201 +instance graph :: (type, monoid_mult) idem_add
   2.202 +proof
   2.203 +  fix a :: "('a, 'b) graph"
   2.204 +  show "a + a = a" unfolding plus_is_join by simp
   2.205 +qed
   2.206 +
   2.207 +
   2.208 +(* define star on graphs *)
   2.209 +
   2.210 +
   2.211 +instance graph :: (type, monoid_mult) star
   2.212 +  graph_star_def: "star G == (SUP n. G ^ n)" ..
   2.213 +
   2.214 +
   2.215 +lemma graph_leqI:
   2.216 +  assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
   2.217 +  shows "G \<le> H"
   2.218 +  using prems
   2.219 +  unfolding graph_leq_def has_edge_def
   2.220 +  by auto
   2.221 +
   2.222 +
   2.223 +lemma in_graph_plusE:
   2.224 +  assumes "has_edge (G + H) n e n'"
   2.225 +  assumes "has_edge G n e n' \<Longrightarrow> P"
   2.226 +  assumes "has_edge H n e n' \<Longrightarrow> P"
   2.227 +  shows P
   2.228 +  using prems
   2.229 +  by (auto simp: in_grplus)
   2.230 +
   2.231 +
   2.232 +
   2.233 +lemma 
   2.234 +  assumes "x \<in> S k"
   2.235 +  shows "x \<in> (\<Union>k. S k)"
   2.236 +  using prems by blast
   2.237 +
   2.238 +lemma graph_union_least:
   2.239 +  assumes "\<And>n. Graph (G n) \<le> C"
   2.240 +  shows "Graph (\<Union>n. G n) \<le> C"
   2.241 +  using prems unfolding graph_leq_def
   2.242 +  by auto
   2.243 +
   2.244 +lemma Sup_graph_eq:
   2.245 +  "(SUP n. Graph (G n)) = Graph (\<Union>n. G n)"
   2.246 +  unfolding SUP_def 
   2.247 +  apply (rule order_antisym)
   2.248 +  apply (rule Sup_least)
   2.249 +  apply auto
   2.250 +  apply (simp add:graph_leq_def)
   2.251 +  apply auto
   2.252 +  apply (rule graph_union_least)
   2.253 +  apply (rule Sup_upper)
   2.254 +  by auto
   2.255 +
   2.256 +lemma has_edge_leq: "has_edge G p b q = (Graph {(p,b,q)} \<le> G)"
   2.257 +  unfolding has_edge_def graph_leq_def
   2.258 +  by (cases G) simp
   2.259 +
   2.260 +
   2.261 +lemma Sup_graph_eq2:
   2.262 +  "(SUP n. G n) = Graph (\<Union>n. dest_graph (G n))"
   2.263 +  using Sup_graph_eq[of "\<lambda>n. dest_graph (G n)", simplified]
   2.264 +  by simp
   2.265 +
   2.266 +lemma in_SUP:
   2.267 +  "has_edge (SUP x. Gs x) p b q = (\<exists>x. has_edge (Gs x) p b q)"
   2.268 +  unfolding Sup_graph_eq2 has_edge_leq graph_leq_def
   2.269 +  by simp
   2.270 +
   2.271 +instance graph :: (type, monoid_mult) kleene_by_comp_lat
   2.272 +proof
   2.273 +  fix a b c :: "('a, 'b) graph"
   2.274 +
   2.275 +  show "a \<le> b \<longleftrightarrow> a + b = b" unfolding graph_leq_def graph_plus_def
   2.276 +    by (cases a, cases b) auto
   2.277 +
   2.278 +  from order_less_le show "a < b \<longleftrightarrow> a \<le> b \<and> a \<noteq> b" .
   2.279 +
   2.280 +  show "a * star b * c = (SUP n. a * b ^ n * c)"
   2.281 +    unfolding graph_star_def
   2.282 +    by (rule graph_ext) (force simp:in_SUP in_grcomp)
   2.283 +qed
   2.284 +
   2.285 +
   2.286 +lemma in_star: 
   2.287 +  "has_edge (star G) a x b = (\<exists>n. has_edge (G ^ n) a x b)"
   2.288 +  by (auto simp:graph_star_def in_SUP)
   2.289 +
   2.290 +lemma tcl_is_SUP:
   2.291 +  "tcl (G::('a::type, 'b::monoid_mult) graph) =
   2.292 +  (SUP n. G ^ (Suc n))"
   2.293 +  unfolding tcl_def 
   2.294 +  using star_cont[of 1 G G]
   2.295 +  by (simp add:power_Suc power_commutes)
   2.296 +
   2.297 +
   2.298 +lemma in_tcl: 
   2.299 +  "has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)"
   2.300 +  apply (auto simp: tcl_is_SUP in_SUP)
   2.301 +  apply (rule_tac x = "n - 1" in exI, auto)
   2.302 +  done
   2.303 +
   2.304 +
   2.305 +
   2.306 +section {* Infinite Paths *}
   2.307 +
   2.308 +types ('n, 'e) ipath = "('n \<times> 'e) sequence"
   2.309 +
   2.310 +definition has_ipath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) ipath \<Rightarrow> bool"
   2.311 +where
   2.312 +  "has_ipath G p = 
   2.313 +  (\<forall>i. has_edge G (fst (p i)) (snd (p i)) (fst (p (Suc i))))"
   2.314 +
   2.315 +
   2.316 +
   2.317 +section {* Finite Paths *}
   2.318 +
   2.319 +types ('n, 'e) fpath = "('n \<times> ('e \<times> 'n) list)"
   2.320 +
   2.321 +inductive2  has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool" 
   2.322 +  for G :: "('n, 'e) graph"
   2.323 +where
   2.324 +  has_fpath_empty: "has_fpath G (n, [])"
   2.325 +| 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)"
   2.326 +
   2.327 +definition 
   2.328 +  "end_node p = 
   2.329 +  (if snd p = [] then fst p else snd (snd p ! (length (snd p) - 1)))"
   2.330 +
   2.331 +definition path_nth :: "('n, 'e) fpath \<Rightarrow> nat \<Rightarrow> ('n \<times> 'e \<times> 'n)"
   2.332 +where
   2.333 +  "path_nth p k = (if k = 0 then fst p else snd (snd p ! (k - 1)), snd p ! k)"
   2.334 +
   2.335 +lemma endnode_nth:
   2.336 +  assumes "length (snd p) = Suc k"
   2.337 +  shows "end_node p = snd (snd (path_nth p k))"
   2.338 +  using prems unfolding end_node_def path_nth_def
   2.339 +  by auto
   2.340 +
   2.341 +lemma path_nth_graph:
   2.342 +  assumes "k < length (snd p)"
   2.343 +  assumes "has_fpath G p"
   2.344 +  shows "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p k)"
   2.345 +  using prems
   2.346 +proof (induct k arbitrary:p)
   2.347 +  case 0 thus ?case 
   2.348 +    unfolding path_nth_def by (auto elim:has_fpath.cases)
   2.349 +next
   2.350 +  case (Suc k p)
   2.351 +
   2.352 +  from `has_fpath G p` show ?case 
   2.353 +  proof (rule has_fpath.cases)
   2.354 +    case goal1 with Suc show ?case by simp
   2.355 +  next
   2.356 +    fix n e n' es
   2.357 +    assume st: "p = (n, (e, n') # es)"
   2.358 +       "G \<turnstile> n \<leadsto>\<^bsup>e\<^esup> n'"
   2.359 +       "has_fpath G (n', es)"
   2.360 +    with Suc
   2.361 +    have "(\<lambda>(n, b, a). G \<turnstile> n \<leadsto>\<^bsup>b\<^esup> a) (path_nth (n', es) k)" by simp
   2.362 +    with st show ?thesis by (cases k, auto simp:path_nth_def)
   2.363 +  qed
   2.364 +qed
   2.365 +
   2.366 +lemma path_nth_connected:
   2.367 +  assumes "Suc k < length (snd p)"
   2.368 +  shows "fst (path_nth p (Suc k)) = snd (snd (path_nth p k))"
   2.369 +  using prems
   2.370 +  unfolding path_nth_def
   2.371 +  by auto
   2.372 +
   2.373 +definition path_loop :: "('n, 'e) fpath \<Rightarrow> ('n, 'e) ipath" ("omega")
   2.374 +where
   2.375 +  "omega p \<equiv> (\<lambda>i. (\<lambda>(n,e,n'). (n,e)) (path_nth p (i mod (length (snd p)))))"
   2.376 +
   2.377 +lemma fst_p0: "fst (path_nth p 0) = fst p"
   2.378 +  unfolding path_nth_def by simp
   2.379 +
   2.380 +lemma path_loop_connect:
   2.381 +  assumes "fst p = end_node p"
   2.382 +  and "0 < length (snd p)" (is "0 < ?l")
   2.383 +  shows "fst (path_nth p (Suc i mod (length (snd p))))
   2.384 +  = snd (snd (path_nth p (i mod length (snd p))))"
   2.385 +  (is "\<dots> = snd (snd (path_nth p ?k))")
   2.386 +proof -
   2.387 +  from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
   2.388 +    by simp
   2.389 +
   2.390 +  show ?thesis 
   2.391 +  proof (cases "Suc ?k < ?l")
   2.392 +    case True
   2.393 +    hence "Suc ?k \<noteq> ?l" by simp
   2.394 +    with path_nth_connected[OF True]
   2.395 +    show ?thesis
   2.396 +      by (simp add:mod_Suc)
   2.397 +  next
   2.398 +    case False 
   2.399 +    with `?k < ?l` have wrap: "Suc ?k = ?l" by simp
   2.400 +
   2.401 +    hence "fst (path_nth p (Suc i mod ?l)) = fst (path_nth p 0)" 
   2.402 +      by (simp add: mod_Suc)
   2.403 +    also from fst_p0 have "\<dots> = fst p" .
   2.404 +    also have "\<dots> = end_node p" .
   2.405 +    also have "\<dots> = snd (snd (path_nth p ?k))" 
   2.406 +      by (auto simp:endnode_nth wrap)
   2.407 +    finally show ?thesis .
   2.408 +  qed
   2.409 +qed
   2.410 +
   2.411 +lemma path_loop_graph:
   2.412 +  assumes "has_fpath G p"
   2.413 +  and loop: "fst p = end_node p"
   2.414 +  and nonempty: "0 < length (snd p)" (is "0 < ?l")
   2.415 +  shows "has_ipath G (omega p)"
   2.416 +proof (auto simp:has_ipath_def)
   2.417 +  fix i 
   2.418 +  from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
   2.419 +    by simp
   2.420 +  with path_nth_graph 
   2.421 +  have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)" .
   2.422 +
   2.423 +  from path_loop_connect[OF loop nonempty] pk_G
   2.424 +  show "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))"
   2.425 +    unfolding path_loop_def has_edge_def split_def
   2.426 +    by simp
   2.427 +qed
   2.428 +
   2.429 +definition prod :: "('n, 'e::monoid_mult) fpath \<Rightarrow> 'e"
   2.430 +where
   2.431 +  "prod p = foldr (op *) (map fst (snd p)) 1"
   2.432 +
   2.433 +lemma prod_simps[simp]:
   2.434 +  "prod (n, []) = 1"
   2.435 +  "prod (n, (e,n')#es) = e * (prod (n',es))"
   2.436 +unfolding prod_def
   2.437 +by simp_all
   2.438 +
   2.439 +lemma power_induces_path:
   2.440 +  assumes a: "has_edge (A ^ k) n G m"
   2.441 +  obtains p 
   2.442 +    where "has_fpath A p"
   2.443 +      and "n = fst p" "m = end_node p"
   2.444 +      and "G = prod p"
   2.445 +      and "k = length (snd p)"
   2.446 +  using a
   2.447 +proof (induct k arbitrary:m n G thesis)
   2.448 +  case (0 m n G)
   2.449 +  let ?p = "(n, [])"
   2.450 +  from 0 have "has_fpath A ?p" "m = end_node ?p" "G = prod ?p"
   2.451 +    by (auto simp:in_grunit end_node_def intro:has_fpath.intros)
   2.452 +  thus ?case using 0 by (auto simp:end_node_def)
   2.453 +next
   2.454 +  case (Suc k m n G)
   2.455 +  hence "has_edge (A * A ^ k) n G m" 
   2.456 +    by (simp add:power_Suc power_commutes)
   2.457 +  then obtain G' H j where 
   2.458 +    a_A: "has_edge A n G' j"
   2.459 +    and H_pow: "has_edge (A ^ k) j H m"
   2.460 +    and [simp]: "G = G' * H"
   2.461 +    by (auto simp:in_grcomp) 
   2.462 +
   2.463 +  from H_pow and Suc
   2.464 +  obtain p
   2.465 +    where p_path: "has_fpath A p"
   2.466 +    and [simp]: "j = fst p" "m = end_node p" "H = prod p" 
   2.467 +    "k = length (snd p)"
   2.468 +    by blast
   2.469 +
   2.470 +  let ?p' = "(n, (G', j)#snd p)"
   2.471 +  from a_A and p_path
   2.472 +  have "has_fpath A ?p'" "m = end_node ?p'" "G = prod ?p'"
   2.473 +    by (auto simp:end_node_def nth.simps intro:has_fpath.intros split:nat.split)
   2.474 +  thus ?case using Suc by auto
   2.475 +qed
   2.476 +
   2.477 +
   2.478 +
   2.479 +
   2.480 +
   2.481 +section {* Sub-Paths *}
   2.482 +
   2.483 +
   2.484 +definition sub_path :: "('n, 'e) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ('n, 'e) fpath"
   2.485 +("(_\<langle>_,_\<rangle>)")
   2.486 +where
   2.487 +  "p\<langle>i,j\<rangle> =
   2.488 +  (fst (p i), map (\<lambda>k. (snd (p k), fst (p (Suc k)))) [i ..< j])"
   2.489 +
   2.490 +
   2.491 +lemma sub_path_is_path: 
   2.492 +  assumes ipath: "has_ipath G p"
   2.493 +  assumes l: "i \<le> j"
   2.494 +  shows "has_fpath G (p\<langle>i,j\<rangle>)"
   2.495 +  using l
   2.496 +proof (induct i rule:inc_induct)
   2.497 +  case 1 show ?case by (auto simp:sub_path_def intro:has_fpath.intros)
   2.498 +next
   2.499 +  case (2 i)
   2.500 +  with ipath upt_rec[of i j]
   2.501 +  show ?case
   2.502 +    by (auto simp:sub_path_def has_ipath_def intro:has_fpath.intros)
   2.503 +qed
   2.504 +
   2.505 +
   2.506 +lemma sub_path_start[simp]:
   2.507 +  "fst (p\<langle>i,j\<rangle>) = fst (p i)"
   2.508 +  by (simp add:sub_path_def)
   2.509 +
   2.510 +lemma nth_upto[simp]: "k < j - i \<Longrightarrow> [i ..< j] ! k = i + k"
   2.511 +  by (induct k) auto
   2.512 +
   2.513 +lemma sub_path_end[simp]:
   2.514 +  "i < j \<Longrightarrow> end_node (p\<langle>i,j\<rangle>) = fst (p j)"
   2.515 +  by (auto simp:sub_path_def end_node_def)
   2.516 +
   2.517 +lemma foldr_map: "foldr f (map g xs) = foldr (f o g) xs"
   2.518 +  by (induct xs) auto
   2.519 +
   2.520 +lemma upto_append[simp]:
   2.521 +  assumes "i \<le> j" "j \<le> k"
   2.522 +  shows "[ i ..< j ] @ [j ..< k] = [i ..< k]"
   2.523 +  using prems and upt_add_eq_append[of i j "k - j"]
   2.524 +  by simp
   2.525 +
   2.526 +lemma foldr_monoid: "foldr (op *) xs 1 * foldr (op *) ys 1
   2.527 +  = foldr (op *) (xs @ ys) (1::'a::monoid_mult)"
   2.528 +  by (induct xs) (auto simp:mult_assoc)
   2.529 +
   2.530 +lemma sub_path_prod:
   2.531 +  assumes "i < j"
   2.532 +  assumes "j < k"
   2.533 +  shows "prod (p\<langle>i,k\<rangle>) = prod (p\<langle>i,j\<rangle>) * prod (p\<langle>j,k\<rangle>)"
   2.534 +  using prems
   2.535 +  unfolding prod_def sub_path_def
   2.536 +  by (simp add:map_compose[symmetric] comp_def)
   2.537 +   (simp only:foldr_monoid map_append[symmetric] upto_append)
   2.538 +
   2.539 +
   2.540 +lemma path_acgpow_aux:
   2.541 +  assumes "length es = l"
   2.542 +  assumes "has_fpath G (n,es)"
   2.543 +  shows "has_edge (G ^ l) n (prod (n,es)) (end_node (n,es))"
   2.544 +using prems
   2.545 +proof (induct l arbitrary:n es)
   2.546 +  case 0 thus ?case
   2.547 +    by (simp add:in_grunit end_node_def) 
   2.548 +next
   2.549 +  case (Suc l n es)
   2.550 +  hence "es \<noteq> []" by auto
   2.551 +  let ?n' = "snd (hd es)"
   2.552 +  let ?es' = "tl es"
   2.553 +  let ?e = "fst (hd es)"
   2.554 +
   2.555 +  from Suc have len: "length ?es' = l" by auto
   2.556 +
   2.557 +  from Suc
   2.558 +  have [simp]: "end_node (n, es) = end_node (?n', ?es')"
   2.559 +    by (cases es) (auto simp:end_node_def nth.simps split:nat.split)
   2.560 +
   2.561 +  from `has_fpath G (n,es)`
   2.562 +  have "has_fpath G (?n', ?es')"
   2.563 +    by (rule has_fpath.cases) (auto intro:has_fpath.intros)
   2.564 +  with Suc len
   2.565 +  have "has_edge (G ^ l) ?n' (prod (?n', ?es')) (end_node (?n', ?es'))"
   2.566 +    by auto
   2.567 +  moreover
   2.568 +  from `es \<noteq> []`
   2.569 +  have "prod (n, es) = ?e * (prod (?n', ?es'))"
   2.570 +    by (cases es) auto
   2.571 +  moreover
   2.572 +  from `has_fpath G (n,es)` have c:"has_edge G n ?e ?n'"
   2.573 +    by (rule has_fpath.cases) (insert `es \<noteq> []`, auto)
   2.574 +
   2.575 +  ultimately
   2.576 +  show ?case
   2.577 +     unfolding power_Suc 
   2.578 +     by (auto simp:in_grcomp)
   2.579 +qed
   2.580 +
   2.581 +
   2.582 +lemma path_acgpow:
   2.583 +   "has_fpath G p
   2.584 +  \<Longrightarrow> has_edge (G ^ length (snd p)) (fst p) (prod p) (end_node p)"
   2.585 +by (cases p)
   2.586 +   (rule path_acgpow_aux[of "snd p" "length (snd p)" _ "fst p", simplified])
   2.587 +
   2.588 +
   2.589 +lemma star_paths:
   2.590 +  "has_edge (star G) a x b =
   2.591 +   (\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p)"
   2.592 +proof
   2.593 +  assume "has_edge (star G) a x b"
   2.594 +  then obtain n where pow: "has_edge (G ^ n) a x b"
   2.595 +    by (auto simp:in_star)
   2.596 +
   2.597 +  then obtain p where
   2.598 +    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
   2.599 +    by (rule power_induces_path)
   2.600 +
   2.601 +  thus "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p"
   2.602 +    by blast
   2.603 +next
   2.604 +  assume "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p"
   2.605 +  then obtain p where
   2.606 +    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
   2.607 +    by blast
   2.608 +
   2.609 +  hence "has_edge (G ^ length (snd p)) a x b"
   2.610 +    by (auto intro:path_acgpow)
   2.611 +
   2.612 +  thus "has_edge (star G) a x b"
   2.613 +    by (auto simp:in_star)
   2.614 +qed
   2.615 +
   2.616 +
   2.617 +lemma plus_paths:
   2.618 +  "has_edge (tcl G) a x b =
   2.619 +   (\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p \<and> 0 < length (snd p))"
   2.620 +proof
   2.621 +  assume "has_edge (tcl G) a x b"
   2.622 +  
   2.623 +  then obtain n where pow: "has_edge (G ^ n) a x b" and "0 < n"
   2.624 +    by (auto simp:in_tcl)
   2.625 +
   2.626 +  from pow obtain p where
   2.627 +    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
   2.628 +    "n = length (snd p)"
   2.629 +    by (rule power_induces_path)
   2.630 +
   2.631 +  with `0 < n`
   2.632 +  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) "
   2.633 +    by blast
   2.634 +next
   2.635 +  assume "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p
   2.636 +    \<and> 0 < length (snd p)"
   2.637 +  then obtain p where
   2.638 +    "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
   2.639 +    "0 < length (snd p)"
   2.640 +    by blast
   2.641 +
   2.642 +  hence "has_edge (G ^ length (snd p)) a x b"
   2.643 +    by (auto intro:path_acgpow)
   2.644 +
   2.645 +  with `0 < length (snd p)`
   2.646 +  show "has_edge (tcl G) a x b"
   2.647 +    by (auto simp:in_tcl)
   2.648 +qed
   2.649 +
   2.650 +
   2.651 +definition
   2.652 +  "contract s p = 
   2.653 +  (\<lambda>i. (fst (p (s i)), prod (p\<langle>s i,s (Suc i)\<rangle>)))"
   2.654 +
   2.655 +lemma ipath_contract:
   2.656 +  assumes [simp]: "increasing s"
   2.657 +  assumes ipath: "has_ipath G p"
   2.658 +  shows "has_ipath (tcl G) (contract s p)"
   2.659 +  unfolding has_ipath_def 
   2.660 +proof
   2.661 +  fix i
   2.662 +  let ?p = "p\<langle>s i,s (Suc i)\<rangle>"
   2.663 +
   2.664 +  from increasing_strict 
   2.665 +	have "fst (p (s (Suc i))) = end_node ?p" by simp
   2.666 +  moreover
   2.667 +  from increasing_strict[of s i "Suc i"] have "snd ?p \<noteq> []"
   2.668 +    by (simp add:sub_path_def)
   2.669 +  moreover
   2.670 +  from ipath increasing_weak[of s] have "has_fpath G ?p"
   2.671 +    by (rule sub_path_is_path) auto
   2.672 +  ultimately
   2.673 +  show "has_edge (tcl G) 
   2.674 +    (fst (contract s p i)) (snd (contract s p i)) (fst (contract s p (Suc i)))"
   2.675 +    unfolding contract_def plus_paths
   2.676 +    by (intro exI) auto
   2.677 +qed
   2.678 +
   2.679 +lemma prod_unfold:
   2.680 +  "i < j \<Longrightarrow> prod (p\<langle>i,j\<rangle>) 
   2.681 +  = snd (p i) * prod (p\<langle>Suc i, j\<rangle>)"
   2.682 +  unfolding prod_def
   2.683 +  by (simp add:sub_path_def upt_rec[of "i" j])
   2.684 +
   2.685 +
   2.686 +lemma sub_path_loop:
   2.687 +  assumes "0 < k"
   2.688 +  assumes k:"k = length (snd loop)"
   2.689 +  assumes loop: "fst loop = end_node loop"
   2.690 +  shows "(omega loop)\<langle>k * i,k * Suc i\<rangle> = loop" (is "?\<omega> = loop")
   2.691 +proof (rule prod_eqI)
   2.692 +  show "fst ?\<omega> = fst loop"
   2.693 +    by (auto simp:path_loop_def path_nth_def split_def k)
   2.694 +  
   2.695 +  show "snd ?\<omega> = snd loop"
   2.696 +  proof (rule nth_equalityI[rule_format])
   2.697 +    show leneq: "length (snd ?\<omega>) = length (snd loop)"
   2.698 +      unfolding sub_path_def k by simp
   2.699 +
   2.700 +    fix j assume "j < length (snd (?\<omega>))"
   2.701 +    with leneq and k have "j < k" by simp
   2.702 +
   2.703 +    have a: "\<And>i. fst (path_nth loop (Suc i mod k))
   2.704 +      = snd (snd (path_nth loop (i mod k)))"
   2.705 +      unfolding k
   2.706 +      apply (rule path_loop_connect[OF loop])
   2.707 +      by (insert prems, auto)
   2.708 +
   2.709 +    from `j < k` 
   2.710 +    show "snd ?\<omega> ! j = snd loop ! j"
   2.711 +      unfolding sub_path_def
   2.712 +      apply (simp add:path_loop_def split_def add_ac)
   2.713 +      apply (simp add:a k[symmetric])
   2.714 +      by (simp add:path_nth_def)
   2.715 +  qed
   2.716 +qed
   2.717 +      
   2.718 +
   2.719 +
   2.720 +
   2.721 +
   2.722 +
   2.723 +
   2.724 +end
   2.725 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Kleene_Algebras.thy	Mon Feb 26 21:34:16 2007 +0100
     3.3 @@ -0,0 +1,471 @@
     3.4 +theory Kleene_Algebras
     3.5 +imports Main 
     3.6 +begin
     3.7 +
     3.8 +text {* A type class of kleene algebras *}
     3.9 +
    3.10 +class star = 
    3.11 +  fixes star :: "'a \<Rightarrow> 'a"
    3.12 +
    3.13 +axclass idem_add \<subseteq> ab_semigroup_add
    3.14 +  add_idem[simp]: "x + x = x"
    3.15 +
    3.16 +lemma add_idem2[simp]: "(x::'a::idem_add) + (x + y) = x + y"
    3.17 +  unfolding add_assoc[symmetric]
    3.18 +  by simp
    3.19 +
    3.20 +axclass order_by_add \<subseteq> idem_add, ord
    3.21 +  order_def: "a \<le> b \<longleftrightarrow> a + b = b"
    3.22 +  strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> a \<noteq> b"
    3.23 +
    3.24 +lemma ord_simp1[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> x + y = y"
    3.25 +  unfolding order_def .
    3.26 +lemma ord_simp2[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> y + x = y"
    3.27 +  unfolding order_def add_commute .
    3.28 +lemma ord_intro: "(x::'a::order_by_add) + y = y \<Longrightarrow> x \<le> y"
    3.29 +  unfolding order_def .
    3.30 +
    3.31 +instance order_by_add \<subseteq> order
    3.32 +proof
    3.33 +  fix x y z :: 'a
    3.34 +  show "x \<le> x" unfolding order_def by simp
    3.35 +
    3.36 +  show "\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z"
    3.37 +  proof (rule ord_intro)
    3.38 +    assume "x \<le> y" "y \<le> z"
    3.39 +
    3.40 +    have "x + z = x + y + z" by (simp add:`y \<le> z` add_assoc)
    3.41 +    also have "\<dots> = y + z" by (simp add:`x \<le> y`)
    3.42 +    also have "\<dots> = z" by (simp add:`y \<le> z`)
    3.43 +    finally show "x + z = z" .
    3.44 +  qed
    3.45 +
    3.46 +  show "\<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" unfolding order_def
    3.47 +    by (simp add:add_commute)
    3.48 +  show "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y" by (fact strict_order_def)
    3.49 +qed
    3.50 +
    3.51 +
    3.52 +axclass pre_kleene \<subseteq> semiring_1, order_by_add
    3.53 +
    3.54 +instance pre_kleene \<subseteq> pordered_semiring
    3.55 +proof
    3.56 +  fix x y z :: 'a
    3.57 +
    3.58 +  assume "x \<le> y"
    3.59 +   
    3.60 +  show "z + x \<le> z + y"
    3.61 +  proof (rule ord_intro)
    3.62 +    have "z + x + (z + y) = x + y + z" by (simp add:add_ac)
    3.63 +    also have "\<dots> = z + y" by (simp add:`x \<le> y` add_ac)
    3.64 +    finally show "z + x + (z + y) = z + y" .
    3.65 +  qed
    3.66 +
    3.67 +  show "z * x \<le> z * y"
    3.68 +  proof (rule ord_intro)
    3.69 +    from `x \<le> y` have "z * (x + y) = z * y" by simp
    3.70 +    thus "z * x + z * y = z * y" by (simp add:right_distrib)
    3.71 +  qed
    3.72 +
    3.73 +  show "x * z \<le> y * z"
    3.74 +  proof (rule ord_intro)
    3.75 +    from `x \<le> y` have "(x + y) * z = y * z" by simp
    3.76 +    thus "x * z + y * z = y * z" by (simp add:left_distrib)
    3.77 +  qed
    3.78 +qed
    3.79 +
    3.80 +axclass kleene \<subseteq> pre_kleene, star
    3.81 +  star1: "1 + a * star a \<le> star a"
    3.82 +  star2: "1 + star a * a \<le> star a"
    3.83 +  star3: "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
    3.84 +  star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
    3.85 +
    3.86 +axclass kleene_by_comp_lat \<subseteq> 
    3.87 +  pre_kleene, comp_lat, recpower, star
    3.88 +
    3.89 +  star_cont: "a * star b * c = (SUP n. a * b ^ n * c)"
    3.90 +
    3.91 +
    3.92 +lemma plus_leI: 
    3.93 +  fixes x :: "'a :: order_by_add"
    3.94 +  shows "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
    3.95 +  unfolding order_def by (simp add:add_assoc)
    3.96 +
    3.97 +
    3.98 +
    3.99 +
   3.100 +lemma le_SUPI':
   3.101 +  fixes l :: "'a :: comp_lat"
   3.102 +  assumes "l \<le> M i"
   3.103 +  shows "l \<le> (SUP i. M i)"
   3.104 +  using prems
   3.105 +  by (rule order_trans) (rule le_SUPI, rule refl)
   3.106 +
   3.107 +
   3.108 +lemma zero_minimum[simp]: "(0::'a::pre_kleene) \<le> x"
   3.109 +  unfolding order_def by simp
   3.110 +
   3.111 +instance kleene_by_comp_lat \<subseteq> kleene
   3.112 +proof
   3.113 +
   3.114 +  fix a x :: 'a
   3.115 +  
   3.116 +  have [simp]: "1 \<le> star a"
   3.117 +    unfolding star_cont[of 1 a 1, simplified] 
   3.118 +    by (rule le_SUPI) (rule power_0[symmetric])
   3.119 +  
   3.120 +  show "1 + a * star a \<le> star a" 
   3.121 +    apply (rule plus_leI, simp)
   3.122 +    apply (simp add:star_cont[of a a 1, simplified])
   3.123 +    apply (simp add:star_cont[of 1 a 1, simplified])
   3.124 +    apply (intro SUP_leI le_SUPI)
   3.125 +    by (rule power_Suc[symmetric])
   3.126 +
   3.127 +  show "1 + star a * a \<le> star a" 
   3.128 +    apply (rule plus_leI, simp)
   3.129 +    apply (simp add:star_cont[of 1 a a, simplified])
   3.130 +    apply (simp add:star_cont[of 1 a 1, simplified])
   3.131 +    apply (intro SUP_leI le_SUPI)
   3.132 +    by (simp add:power_Suc[symmetric] power_commutes)
   3.133 +
   3.134 +  show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
   3.135 +  proof -
   3.136 +    assume a: "a * x \<le> x"
   3.137 +
   3.138 +    {
   3.139 +      fix n
   3.140 +      have "a ^ (Suc n) * x \<le> a ^ n * x"
   3.141 +      proof (induct n)
   3.142 +        case 0 thus ?case by (simp add:a power_Suc)
   3.143 +      next
   3.144 +        case (Suc n)
   3.145 +        hence "a * (a ^ Suc n * x) \<le> a * (a ^ n * x)"
   3.146 +          by (auto intro: mult_mono)
   3.147 +        thus ?case
   3.148 +          by (simp add:power_Suc mult_assoc)
   3.149 +      qed
   3.150 +    }
   3.151 +    note a = this
   3.152 +    
   3.153 +    {
   3.154 +      fix n have "a ^ n * x \<le> x"
   3.155 +      proof (induct n)
   3.156 +        case 0 show ?case by simp
   3.157 +      next
   3.158 +        case (Suc n) with a[of n]
   3.159 +        show ?case by simp
   3.160 +      qed
   3.161 +    }
   3.162 +    note b = this
   3.163 +    
   3.164 +    show "star a * x \<le> x"
   3.165 +      unfolding star_cont[of 1 a x, simplified]
   3.166 +      by (rule SUP_leI) (rule b)
   3.167 +  qed
   3.168 +
   3.169 +  show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *)
   3.170 +  proof -
   3.171 +    assume a: "x * a \<le> x"
   3.172 +
   3.173 +    {
   3.174 +      fix n
   3.175 +      have "x * a ^ (Suc n) \<le> x * a ^ n"
   3.176 +      proof (induct n)
   3.177 +        case 0 thus ?case by (simp add:a power_Suc)
   3.178 +      next
   3.179 +        case (Suc n)
   3.180 +        hence "(x * a ^ Suc n) * a  \<le> (x * a ^ n) * a"
   3.181 +          by (auto intro: mult_mono)
   3.182 +        thus ?case
   3.183 +          by (simp add:power_Suc power_commutes mult_assoc)
   3.184 +      qed
   3.185 +    }
   3.186 +    note a = this
   3.187 +    
   3.188 +    {
   3.189 +      fix n have "x * a ^ n \<le> x"
   3.190 +      proof (induct n)
   3.191 +        case 0 show ?case by simp
   3.192 +      next
   3.193 +        case (Suc n) with a[of n]
   3.194 +        show ?case by simp
   3.195 +      qed
   3.196 +    }
   3.197 +    note b = this
   3.198 +    
   3.199 +    show "x * star a \<le> x"
   3.200 +      unfolding star_cont[of x a 1, simplified]
   3.201 +      by (rule SUP_leI) (rule b)
   3.202 +  qed
   3.203 +qed
   3.204 +
   3.205 +lemma less_add[simp]:  
   3.206 +  fixes a b :: "'a :: order_by_add"
   3.207 +  shows "a \<le> a + b"
   3.208 +  and "b \<le> a + b"
   3.209 +  unfolding order_def 
   3.210 +  by (auto simp:add_ac)
   3.211 +
   3.212 +lemma add_est1:
   3.213 +  fixes a b c :: "'a :: order_by_add"
   3.214 +  assumes a: "a + b \<le> c"
   3.215 +  shows "a \<le> c"
   3.216 +  using less_add(1) a
   3.217 +  by (rule order_trans)
   3.218 +
   3.219 +lemma add_est2:
   3.220 +  fixes a b c :: "'a :: order_by_add"
   3.221 +  assumes a: "a + b \<le> c"
   3.222 +  shows "b \<le> c"
   3.223 +  using less_add(2) a
   3.224 +  by (rule order_trans)
   3.225 +
   3.226 +
   3.227 +lemma star3':
   3.228 +  fixes a b x :: "'a :: kleene"
   3.229 +  assumes a: "b + a * x \<le> x"
   3.230 +  shows "star a * b \<le> x"
   3.231 +proof (rule order_trans)
   3.232 +  from a have "b \<le> x" by (rule add_est1)
   3.233 +  show "star a * b \<le> star a * x"
   3.234 +    by (rule mult_mono) (auto simp:`b \<le> x`)
   3.235 +
   3.236 +  from a have "a * x \<le> x" by (rule add_est2)
   3.237 +  with star3 show "star a * x \<le> x" .
   3.238 +qed
   3.239 +
   3.240 +
   3.241 +lemma star4':
   3.242 +  fixes a b x :: "'a :: kleene"
   3.243 +  assumes a: "b + x * a \<le> x"
   3.244 +  shows "b * star a \<le> x"
   3.245 +proof (rule order_trans)
   3.246 +  from a have "b \<le> x" by (rule add_est1)
   3.247 +  show "b * star a \<le> x * star a"
   3.248 +    by (rule mult_mono) (auto simp:`b \<le> x`)
   3.249 +
   3.250 +  from a have "x * a \<le> x" by (rule add_est2)
   3.251 +  with star4 show "x * star a \<le> x" .
   3.252 +qed
   3.253 +
   3.254 +
   3.255 +lemma star_mono:
   3.256 +  fixes x y :: "'a :: kleene"
   3.257 +  assumes "x \<le> y"
   3.258 +  shows "star x \<le> star y"
   3.259 +  oops
   3.260 +
   3.261 +lemma star_idemp:
   3.262 +  fixes x :: "'a :: kleene"
   3.263 +  shows "star (star x) = star x"
   3.264 +  oops
   3.265 +
   3.266 +lemma zero_star[simp]:
   3.267 +  shows "star (0::'a::kleene) = 1"
   3.268 +  oops
   3.269 +
   3.270 +
   3.271 +lemma star_unfold_left:
   3.272 +  fixes a :: "'a :: kleene"
   3.273 +  shows "1 + a * star a = star a"
   3.274 +proof (rule order_antisym, rule star1)
   3.275 +
   3.276 +  have "1 + a * (1 + a * star a) \<le> 1 + a * star a"
   3.277 +    apply (rule add_mono, rule)
   3.278 +    apply (rule mult_mono, auto)
   3.279 +    apply (rule star1)
   3.280 +    done
   3.281 +
   3.282 +  with star3' have "star a * 1 \<le> 1 + a * star a" .
   3.283 +  thus "star a \<le> 1 + a * star a" by simp
   3.284 +qed
   3.285 +
   3.286 +
   3.287 +lemma star_unfold_right:  
   3.288 +  fixes a :: "'a :: kleene"
   3.289 +  shows "1 + star a * a = star a"
   3.290 +proof (rule order_antisym, rule star2)
   3.291 +
   3.292 +  have "1 + (1 + star a * a) * a \<le> 1 + star a * a"
   3.293 +    apply (rule add_mono, rule)
   3.294 +    apply (rule mult_mono, auto)
   3.295 +    apply (rule star2)
   3.296 +    done
   3.297 +
   3.298 +  with star4' have "1 * star a \<le> 1 + star a * a" .
   3.299 +  thus "star a \<le> 1 + star a * a" by simp
   3.300 +qed
   3.301 +
   3.302 +
   3.303 +
   3.304 +lemma star_commute:
   3.305 +  fixes a b x :: "'a :: kleene"
   3.306 +  assumes a: "a * x = x * b"
   3.307 +  shows "star a * x = x * star b"
   3.308 +proof (rule order_antisym)
   3.309 +
   3.310 +  show "star a * x \<le> x * star b"
   3.311 +  proof (rule star3', rule order_trans)
   3.312 +
   3.313 +    from a have "a * x \<le> x * b" by simp
   3.314 +    hence "a * x * star b \<le> x * b * star b"
   3.315 +      by (rule mult_mono) auto
   3.316 +    thus "x + a * (x * star b) \<le> x + x * b * star b"
   3.317 +      using add_mono by (auto simp: mult_assoc)
   3.318 +
   3.319 +    show "\<dots> \<le> x * star b"
   3.320 +    proof -
   3.321 +      have "x * (1 + b * star b) \<le> x * star b"
   3.322 +        by (rule mult_mono[OF _ star1]) auto
   3.323 +      thus ?thesis
   3.324 +        by (simp add:right_distrib mult_assoc)
   3.325 +    qed
   3.326 +  qed
   3.327 +
   3.328 +  show "x * star b \<le> star a * x"
   3.329 +  proof (rule star4', rule order_trans)
   3.330 +
   3.331 +    from a have b: "x * b \<le> a * x" by simp
   3.332 +    have "star a * x * b \<le> star a * a * x"
   3.333 +      unfolding mult_assoc
   3.334 +      by (rule mult_mono[OF _ b]) auto
   3.335 +    thus "x + star a * x * b \<le> x + star a * a * x"
   3.336 +      using add_mono by auto
   3.337 +
   3.338 +    show "\<dots> \<le> star a * x"
   3.339 +    proof -
   3.340 +      have "(1 + star a * a) * x \<le> star a * x"
   3.341 +        by (rule mult_mono[OF star2]) auto
   3.342 +      thus ?thesis
   3.343 +        by (simp add:left_distrib mult_assoc)
   3.344 +    qed
   3.345 +  qed
   3.346 +qed      
   3.347 +
   3.348 +
   3.349 +
   3.350 +lemma star_assoc:
   3.351 +  fixes c d :: "'a :: kleene"
   3.352 +  shows "star (c * d) * c = c * star (d * c)"
   3.353 +  oops
   3.354 +
   3.355 +lemma star_dist:
   3.356 +  fixes a b :: "'a :: kleene"
   3.357 +  shows "star (a + b) = star a * star (b * star a)"
   3.358 +  oops
   3.359 +
   3.360 +lemma star_one:
   3.361 +  fixes a p p' :: "'a :: kleene"
   3.362 +  assumes "p * p' = 1" and "p' * p = 1"
   3.363 +  shows "p' * star a * p = star (p' * a * p)"
   3.364 +  oops
   3.365 +
   3.366 +
   3.367 +lemma star_zero: 
   3.368 +  "star (0::'a::kleene) = 1"
   3.369 +  by (rule star_unfold_left[of 0, simplified])
   3.370 +
   3.371 +
   3.372 +(* Own lemmas *)
   3.373 +
   3.374 +
   3.375 +lemma x_less_star[simp]: 
   3.376 +  fixes x :: "'a :: kleene"
   3.377 +  shows "x \<le> x * star a"
   3.378 +proof -
   3.379 +  have "x \<le> x * (1 + a * star a)" by (simp add:right_distrib)
   3.380 +  also have "\<dots> = x * star a" by (simp only: star_unfold_left)
   3.381 +  finally show ?thesis .
   3.382 +qed
   3.383 +
   3.384 +subsection {* Transitive Closure *}
   3.385 +
   3.386 +definition 
   3.387 +  "tcl (x::'a::kleene) = star x * x"
   3.388 +
   3.389 +
   3.390 +lemma tcl_zero: 
   3.391 +  "tcl (0::'a::kleene) = 0"
   3.392 +  unfolding tcl_def by simp
   3.393 +
   3.394 +
   3.395 +subsection {* Naive Algorithm to generate the transitive closure *}
   3.396 +
   3.397 +function (default "\<lambda>x. 0", tailrec)
   3.398 +  mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"
   3.399 +where
   3.400 +  "mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))"
   3.401 +  by pat_completeness simp
   3.402 +
   3.403 +declare mk_tcl.simps[simp del] (* loops *)
   3.404 +
   3.405 +lemma mk_tcl_code[code]:
   3.406 +  "mk_tcl A X = 
   3.407 +  (let XA = X * A 
   3.408 +  in if XA \<le> X then X else mk_tcl A (X + XA))"
   3.409 +  unfolding mk_tcl.simps[of A X] Let_def ..
   3.410 +
   3.411 +lemma mk_tcl_lemma1:
   3.412 +  fixes X :: "'a :: kleene"
   3.413 +  shows "(X + X * A) * star A = X * star A"
   3.414 +proof -
   3.415 +  have "A * star A \<le> 1 + A * star A" by simp
   3.416 +  also have "\<dots> = star A" by (simp add:star_unfold_left)
   3.417 +  finally have "star A + A * star A = star A" by simp
   3.418 +  hence "X * (star A + A * star A) = X * star A" by simp
   3.419 +  thus ?thesis by (simp add:left_distrib right_distrib mult_ac)
   3.420 +qed
   3.421 +
   3.422 +lemma mk_tcl_lemma2:
   3.423 +  fixes X :: "'a :: kleene"
   3.424 +  shows "X * A \<le> X \<Longrightarrow> X * star A = X"
   3.425 +  by (rule order_antisym) (auto simp:star4)
   3.426 +
   3.427 +
   3.428 +
   3.429 +
   3.430 +lemma mk_tcl_correctness:
   3.431 +  fixes A X :: "'a :: {kleene}"
   3.432 +  assumes "mk_tcl_dom (A, X)"
   3.433 +  shows "mk_tcl A X = X * star A"
   3.434 +  using prems
   3.435 +  by induct (auto simp:mk_tcl_lemma1 mk_tcl_lemma2)
   3.436 +
   3.437 +lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
   3.438 +  by (rule mk_tcl_graph.induct) (auto intro:accI elim:mk_tcl_rel.cases)
   3.439 +
   3.440 +lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
   3.441 +  unfolding mk_tcl_def
   3.442 +  by (rule fundef_default_value[OF mk_tcl_sum_def graph_implies_dom])
   3.443 +
   3.444 +
   3.445 +text {* We can replace the dom-Condition of the correctness theorem 
   3.446 +  with something executable *}
   3.447 +
   3.448 +lemma mk_tcl_correctness2:
   3.449 +  fixes A X :: "'a :: {kleene}"
   3.450 +  assumes "mk_tcl A A \<noteq> 0"
   3.451 +  shows "mk_tcl A A = tcl A"
   3.452 +  using prems mk_tcl_default mk_tcl_correctness
   3.453 +  unfolding tcl_def 
   3.454 +  by (auto simp:star_commute)
   3.455 +
   3.456 +
   3.457 +
   3.458 +
   3.459 +
   3.460 +end
   3.461 +
   3.462 +
   3.463 +
   3.464 +
   3.465 +
   3.466 +
   3.467 +
   3.468 +
   3.469 +
   3.470 +
   3.471 +
   3.472 +
   3.473 +
   3.474 +
     4.1 --- a/src/HOL/Library/Library.thy	Mon Feb 26 20:14:52 2007 +0100
     4.2 +++ b/src/HOL/Library/Library.thy	Mon Feb 26 21:34:16 2007 +0100
     4.3 @@ -27,6 +27,7 @@
     4.4    Quotient
     4.5    Ramsey
     4.6    State_Monad
     4.7 +  Size_Change_Termination
     4.8    While_Combinator
     4.9    Word
    4.10    Zorn
     5.1 --- a/src/HOL/Library/Library/ROOT.ML	Mon Feb 26 20:14:52 2007 +0100
     5.2 +++ b/src/HOL/Library/Library/ROOT.ML	Mon Feb 26 21:34:16 2007 +0100
     5.3 @@ -3,3 +3,4 @@
     5.4  use_thy "Library";
     5.5  use_thy "List_Prefix";
     5.6  use_thy "List_lexord";
     5.7 +use_thy "SCT_Examples";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Library/SCT_Definition.thy	Mon Feb 26 21:34:16 2007 +0100
     6.3 @@ -0,0 +1,96 @@
     6.4 +theory SCT_Definition
     6.5 +imports Graphs Infinite_Set
     6.6 +begin
     6.7 +
     6.8 +section {* Size-Change Graphs *}
     6.9 +
    6.10 +datatype sedge =
    6.11 +  LESS ("\<down>")
    6.12 +  | LEQ ("\<Down>")
    6.13 +
    6.14 +instance sedge :: times ..
    6.15 +instance sedge :: one ..
    6.16 +
    6.17 +defs (overloaded)
    6.18 +  one_sedge_def: "1 == \<Down>"
    6.19 +  mult_sedge_def:" a * b == (if a = \<down> then \<down> else b)"
    6.20 +
    6.21 +instance sedge :: comm_monoid_mult
    6.22 +proof
    6.23 +  fix a b c :: sedge
    6.24 +  show "a * b * c = a * (b * c)" by (simp add:mult_sedge_def)
    6.25 +  show "1 * a = a" by (simp add:mult_sedge_def one_sedge_def)
    6.26 +  show "a * b = b * a" unfolding mult_sedge_def
    6.27 +    by (cases a, simp) (cases b, auto)
    6.28 +qed
    6.29 +
    6.30 +instance sedge :: finite
    6.31 +proof
    6.32 +  have a: "UNIV = { LESS, LEQ }"
    6.33 +    by auto (case_tac x, auto) (* FIXME *)
    6.34 +  show "finite (UNIV::sedge set)"
    6.35 +    by (simp add:a)
    6.36 +qed
    6.37 +
    6.38 +
    6.39 +types scg = "(nat, sedge) graph"
    6.40 +types acg = "(nat, scg) graph"
    6.41 +
    6.42 +
    6.43 +section {* Size-Change Termination *}
    6.44 +
    6.45 +abbreviation (input)
    6.46 +  "desc P Q == ((\<exists>n.\<forall>i\<ge>n. P i) \<and> (\<exists>\<^sub>\<infinity>i. Q i))"
    6.47 +
    6.48 +abbreviation (input)
    6.49 +  "dsc G i j \<equiv> has_edge G i LESS j"
    6.50 +
    6.51 +abbreviation (input)
    6.52 +  "eq G i j \<equiv> has_edge G i LEQ j"
    6.53 +
    6.54 +abbreviation
    6.55 +  eql :: "scg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
    6.56 +("_ \<turnstile> _ \<leadsto> _")
    6.57 +where
    6.58 +  "eql G i j \<equiv> has_edge G i LESS j \<or> has_edge G i LEQ j"
    6.59 +
    6.60 +
    6.61 +abbreviation (input) descat :: "(nat, scg) ipath \<Rightarrow> nat sequence \<Rightarrow> nat \<Rightarrow> bool"
    6.62 +where
    6.63 +  "descat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))"
    6.64 +
    6.65 +abbreviation (input) eqat :: "(nat, scg) ipath \<Rightarrow> nat sequence \<Rightarrow> nat \<Rightarrow> bool"
    6.66 +where
    6.67 +  "eqat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i))"
    6.68 +
    6.69 +
    6.70 +abbreviation eqlat :: "(nat, scg) ipath \<Rightarrow> nat sequence \<Rightarrow> nat \<Rightarrow> bool"
    6.71 +where
    6.72 +  "eqlat p \<theta> i \<equiv> (has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))
    6.73 +                  \<or> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i)))"
    6.74 +
    6.75 +
    6.76 +definition is_desc_thread :: "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> bool"
    6.77 +where
    6.78 +  "is_desc_thread \<theta> p = ((\<exists>n.\<forall>i\<ge>n. eqlat p \<theta> i) \<and> (\<exists>\<^sub>\<infinity>i. descat p \<theta> i))" 
    6.79 +
    6.80 +definition SCT :: "acg \<Rightarrow> bool"
    6.81 +where
    6.82 +  "SCT \<A> = 
    6.83 +  (\<forall>p. has_ipath \<A> p \<longrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> p))"
    6.84 +
    6.85 +
    6.86 +
    6.87 +definition no_bad_graphs :: "acg \<Rightarrow> bool"
    6.88 +where
    6.89 +  "no_bad_graphs A = 
    6.90 +  (\<forall>n G. has_edge A n G n \<and> G * G = G
    6.91 +  \<longrightarrow> (\<exists>p. has_edge G p LESS p))"
    6.92 +
    6.93 +
    6.94 +definition SCT' :: "acg \<Rightarrow> bool"
    6.95 +where
    6.96 +  "SCT' A = no_bad_graphs (tcl A)"
    6.97 +
    6.98 +
    6.99 +end
   6.100 \ No newline at end of file
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Library/SCT_Examples.thy	Mon Feb 26 21:34:16 2007 +0100
     7.3 @@ -0,0 +1,83 @@
     7.4 +theory SCT_Examples
     7.5 +imports Size_Change_Termination
     7.6 +begin
     7.7 +
     7.8 +
     7.9 +
    7.10 +function f :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    7.11 +where
    7.12 +  "f n 0 = n"
    7.13 +| "f 0 (Suc m) = f (Suc m) m"
    7.14 +| "f (Suc n) (Suc m) = f m n"
    7.15 +by pat_completeness auto
    7.16 +
    7.17 +
    7.18 +termination
    7.19 +  unfolding f_rel_def lfp_const
    7.20 +  apply (rule SCT_on_relations)
    7.21 +  apply (tactic "SCT.abs_rel_tac") (* Build call descriptors *)
    7.22 +  apply (rule ext, rule ext, simp) (* Show that they are correct *)
    7.23 +  apply (tactic "SCT.mk_call_graph") (* Build control graph *)
    7.24 +  apply (rule LJA_apply)                 (* Apply main theorem *)
    7.25 +  apply (simp add:finite_acg_ins finite_acg_empty) (* show finiteness *)
    7.26 +  apply (rule SCT'_exec)
    7.27 +  by eval (* Evaluate to true *)
    7.28 +
    7.29 +
    7.30 +function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
    7.31 +where
    7.32 +  "p m n r = (if r>0 then p m (r - 1) n else
    7.33 +              if n>0 then p r (n - 1) m 
    7.34 +                     else m)"
    7.35 +by pat_completeness auto
    7.36 +
    7.37 +termination
    7.38 +  unfolding p_rel_def lfp_const
    7.39 +  apply (rule SCT_on_relations)
    7.40 +  apply (tactic "SCT.abs_rel_tac") 
    7.41 +  apply (rule ext, rule ext, simp) 
    7.42 +  apply (tactic "SCT.mk_call_graph")
    7.43 +  apply (rule LJA_apply)            
    7.44 +  apply (simp add:finite_acg_ins finite_acg_empty) 
    7.45 +  apply (rule SCT'_exec)
    7.46 +  by eval
    7.47 +
    7.48 +function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
    7.49 +where
    7.50 +  "foo True (Suc n) m = foo True n (Suc m)"
    7.51 +  "foo True 0 m = foo False 0 m"
    7.52 +  "foo False n (Suc m) = foo False (Suc n) m"
    7.53 +  "foo False n 0 = n"
    7.54 +by pat_completeness auto
    7.55 +
    7.56 +termination
    7.57 +  unfolding foo_rel_def lfp_const
    7.58 +  apply (rule SCT_on_relations)
    7.59 +  apply (tactic "SCT.abs_rel_tac") 
    7.60 +  apply (rule ext, rule ext, simp) 
    7.61 +  apply (tactic "SCT.mk_call_graph")
    7.62 +  apply (rule LJA_apply)            
    7.63 +  apply (simp add:finite_acg_ins finite_acg_empty) 
    7.64 +  apply (rule SCT'_exec)
    7.65 +  by eval
    7.66 +
    7.67 +
    7.68 +function (sequential) 
    7.69 +  bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
    7.70 +where
    7.71 +  "bar 0 (Suc n) m = bar m m m"
    7.72 +| "bar k n m = 0"
    7.73 +by pat_completeness auto
    7.74 +
    7.75 +termination
    7.76 +  unfolding bar_rel_def lfp_const
    7.77 +  apply (rule SCT_on_relations)
    7.78 +  apply (tactic "SCT.abs_rel_tac") 
    7.79 +  apply (rule ext, rule ext, simp) 
    7.80 +  apply (tactic "SCT.mk_call_graph")
    7.81 +  apply (rule LJA_apply)            
    7.82 +  apply (simp add:finite_acg_ins finite_acg_empty) 
    7.83 +  by (rule SCT'_empty)
    7.84 +
    7.85 +
    7.86 +end
    7.87 \ No newline at end of file
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Library/SCT_Implementation.thy	Mon Feb 26 21:34:16 2007 +0100
     8.3 @@ -0,0 +1,126 @@
     8.4 +theory SCT_Implementation
     8.5 +imports ExecutableSet SCT_Definition
     8.6 +begin
     8.7 +
     8.8 +fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"
     8.9 +where
    8.10 +  "edges_match ((n, e, m), (n',e',m')) = (m = n')"
    8.11 +
    8.12 +fun connect_edges :: 
    8.13 +  "('n \<times> ('e::times) \<times> 'n) \<times> ('n \<times> 'e \<times> 'n)
    8.14 +  \<Rightarrow> ('n \<times> 'e \<times> 'n)"
    8.15 +where
    8.16 +  "connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')"
    8.17 +
    8.18 +lemma grcomp_code[code]:
    8.19 +  "grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })"
    8.20 +  by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def)
    8.21 +
    8.22 +
    8.23 +definition test_SCT :: "acg \<Rightarrow> bool"
    8.24 +where
    8.25 +  "test_SCT \<A> = 
    8.26 +  (let \<T> = mk_tcl \<A> \<A>
    8.27 +    in (\<T> \<noteq> 0 \<and>
    8.28 +       (\<forall>(n,G,m)\<in>dest_graph \<T>. 
    8.29 +          n \<noteq> m \<or> G * G \<noteq> G \<or> 
    8.30 +         (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS))))"
    8.31 +
    8.32 +
    8.33 +lemma SCT'_exec:
    8.34 +  assumes a: "test_SCT \<A>"
    8.35 +  shows "SCT' \<A>"
    8.36 +proof -
    8.37 +  from mk_tcl_correctness2 a 
    8.38 +  have "mk_tcl \<A> \<A> = tcl \<A>" 
    8.39 +    unfolding test_SCT_def Let_def by auto
    8.40 +  
    8.41 +  with a
    8.42 +  show ?thesis
    8.43 +    unfolding SCT'_def no_bad_graphs_def test_SCT_def Let_def has_edge_def
    8.44 +    by auto
    8.45 +qed
    8.46 +
    8.47 +code_modulename SML
    8.48 +  Implementation Graphs
    8.49 +
    8.50 +lemma [code func]:
    8.51 +  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
    8.52 +  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
    8.53 +  unfolding graph_leq_def graph_less_def by rule+
    8.54 +
    8.55 +lemma [code func]:
    8.56 +  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)"
    8.57 +  unfolding graph_plus_def ..
    8.58 +
    8.59 +lemma [code func]:
    8.60 +  "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H"
    8.61 +  unfolding graph_mult_def ..
    8.62 +
    8.63 +
    8.64 +
    8.65 +lemma SCT'_empty: "SCT' (Graph {})"
    8.66 +  unfolding SCT'_def no_bad_graphs_def graph_zero_def[symmetric]
    8.67 +  tcl_zero
    8.68 +  by (simp add:in_grzero)
    8.69 +
    8.70 +
    8.71 +
    8.72 +subsection {* Witness checking *}
    8.73 +
    8.74 +
    8.75 +definition test_SCT_witness :: "acg \<Rightarrow> acg \<Rightarrow> bool"
    8.76 +where
    8.77 +  "test_SCT_witness A T = 
    8.78 +  (A \<le> T \<and> A * T \<le> T \<and>
    8.79 +       (\<forall>(n,G,m)\<in>dest_graph T. 
    8.80 +          n \<noteq> m \<or> G * G \<noteq> G \<or> 
    8.81 +         (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
    8.82 +
    8.83 +
    8.84 +lemma no_bad_graphs_ucl:
    8.85 +  assumes "A \<le> B"
    8.86 +  assumes "no_bad_graphs B"
    8.87 +  shows "no_bad_graphs A"
    8.88 +using prems
    8.89 +unfolding no_bad_graphs_def has_edge_def graph_leq_def 
    8.90 +by blast
    8.91 +
    8.92 +
    8.93 +
    8.94 +lemma SCT'_witness:
    8.95 +  assumes a: "test_SCT_witness A T"
    8.96 +  shows "SCT' A"
    8.97 +proof -
    8.98 +  from a have "A \<le> T" "A * T \<le> T" by (auto simp:test_SCT_witness_def)
    8.99 +  hence "A + A * T \<le> T" 
   8.100 +    by (subst add_idem[of T, symmetric], rule add_mono)
   8.101 +  with star3' have "tcl A \<le> T" unfolding tcl_def .
   8.102 +  moreover
   8.103 +  from a have "no_bad_graphs T"
   8.104 +    unfolding no_bad_graphs_def test_SCT_witness_def has_edge_def
   8.105 +    by auto
   8.106 +  ultimately
   8.107 +  show ?thesis
   8.108 +    unfolding SCT'_def
   8.109 +    by (rule no_bad_graphs_ucl)
   8.110 +qed
   8.111 +
   8.112 +
   8.113 +code_modulename SML
   8.114 +  Graphs SCT
   8.115 +  Kleene_Algebras SCT
   8.116 +  SCT_Implementation SCT
   8.117 +
   8.118 +code_gen test_SCT (SML -)
   8.119 +
   8.120 +
   8.121 +end
   8.122 +
   8.123 +
   8.124 +
   8.125 +
   8.126 +
   8.127 +
   8.128 +
   8.129 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Library/SCT_Interpretation.thy	Mon Feb 26 21:34:16 2007 +0100
     9.3 @@ -0,0 +1,413 @@
     9.4 +theory SCT_Interpretation
     9.5 +imports Main SCT_Misc SCT_Definition
     9.6 +begin
     9.7 +
     9.8 +
     9.9 +definition
    9.10 +  "idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))"
    9.11 +
    9.12 +lemma not_acc_smaller:
    9.13 +  assumes notacc: "\<not> acc R x"
    9.14 +  shows "\<exists>y. R y x \<and> \<not> acc R y"
    9.15 +proof (rule classical)
    9.16 +  assume "\<not> ?thesis"
    9.17 +  hence "\<And>y. R y x \<Longrightarrow> acc R y" by blast
    9.18 +  with accI have "acc R x" .
    9.19 +  with notacc show ?thesis by contradiction
    9.20 +qed
    9.21 +
    9.22 +lemma non_acc_has_idseq:
    9.23 +  assumes "\<not> acc R x"
    9.24 +  shows "\<exists>s. idseq R s x"
    9.25 +proof -
    9.26 +  
    9.27 +  have	"\<exists>f. \<forall>x. \<not>acc R x \<longrightarrow> R (f x) x \<and> \<not>acc R (f x)"
    9.28 +	by (rule choice, auto simp:not_acc_smaller)
    9.29 +  
    9.30 +  then obtain f where
    9.31 +	in_R: "\<And>x. \<not>acc R x \<Longrightarrow> R (f x) x"
    9.32 +	and nia: "\<And>x. \<not>acc R x \<Longrightarrow> \<not>acc R (f x)"
    9.33 +	by blast
    9.34 +  
    9.35 +  let ?s = "\<lambda>i. (f ^ i) x"
    9.36 +  
    9.37 +  {
    9.38 +	fix i
    9.39 +	have "\<not>acc R (?s i)"
    9.40 +	  by (induct i) (auto simp:nia `\<not>acc R x`)
    9.41 +	hence "R (f (?s i)) (?s i)"
    9.42 +	  by (rule in_R)
    9.43 +  }
    9.44 +  
    9.45 +  hence "idseq R ?s x"
    9.46 +	unfolding idseq_def
    9.47 +	by auto
    9.48 +  
    9.49 +  thus ?thesis by auto
    9.50 +qed
    9.51 +
    9.52 +
    9.53 +
    9.54 +
    9.55 +
    9.56 +types ('a, 'q) cdesc =
    9.57 +  "('q \<Rightarrow> bool) \<times> ('q \<Rightarrow> 'a) \<times>('q \<Rightarrow> 'a)"
    9.58 +
    9.59 +
    9.60 +fun in_cdesc :: "('a, 'q) cdesc \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    9.61 +where
    9.62 +  "in_cdesc (\<Gamma>, r, l) x y = (\<exists>q. x = r q \<and> y = l q \<and> \<Gamma> q)"
    9.63 +
    9.64 +fun mk_rel :: "('a, 'q) cdesc list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    9.65 +where
    9.66 +  "mk_rel [] x y = False"
    9.67 +  "mk_rel (c#cs) x y =
    9.68 +  (in_cdesc c x y \<or> mk_rel cs x y)"
    9.69 +
    9.70 +
    9.71 +lemma some_rd:
    9.72 +  assumes "mk_rel rds x y"
    9.73 +  shows "\<exists>rd\<in>set rds. in_cdesc rd x y"
    9.74 +  using prems
    9.75 +  by (induct rds) (auto simp:in_cdesc_def)
    9.76 +
    9.77 +(* from a value sequence, get a sequence of rds *)
    9.78 +
    9.79 +lemma ex_cs:
    9.80 +  assumes idseq: "idseq (mk_rel rds) s x"
    9.81 +  shows "\<exists>cs. \<forall>i. cs i \<in> set rds \<and> in_cdesc (cs i) (s (Suc i)) (s i)"
    9.82 +proof -
    9.83 +  from idseq
    9.84 +  have a: "\<forall>i. \<exists>rd \<in> set rds. in_cdesc rd (s (Suc i)) (s i)"
    9.85 +	by (auto simp:idseq_def intro:some_rd)
    9.86 +  
    9.87 +  show ?thesis
    9.88 +	by (rule choice) (insert a, blast)
    9.89 +qed
    9.90 +
    9.91 +
    9.92 +
    9.93 +types ('q, 'a) interpr = "('a, 'q) cdesc \<times> (nat \<Rightarrow> 'a \<Rightarrow> nat)"
    9.94 +types 'a measures = "nat \<Rightarrow> 'a \<Rightarrow> nat"
    9.95 +
    9.96 +
    9.97 +fun stepP :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> 
    9.98 +  ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> bool"
    9.99 +where
   9.100 +  "stepP (\<Gamma>1,r1,l1) (\<Gamma>2,r2,l2) m1 m2 R
   9.101 +  = (\<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 
   9.102 +  \<longrightarrow> R (m2 (l2 q\<^isub>2)) ((m1 (l1 q\<^isub>1))))"
   9.103 +
   9.104 +
   9.105 +definition
   9.106 +  decr :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> 
   9.107 +  ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
   9.108 +where
   9.109 +  "decr c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op <)"
   9.110 +
   9.111 +definition
   9.112 +  decreq :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> 
   9.113 +  ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
   9.114 +where
   9.115 +  "decreq c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op \<le>)"
   9.116 +
   9.117 +definition
   9.118 +  no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool"
   9.119 +where
   9.120 +  "no_step c1 c2 = stepP c1 c2 (\<lambda>x. 0) (\<lambda>x. 0) (\<lambda>x y. False)"
   9.121 +
   9.122 +
   9.123 +
   9.124 +lemma decr_in_cdesc:
   9.125 +  assumes	"in_cdesc RD1 y x"
   9.126 +  assumes "in_cdesc RD2 z y"
   9.127 +  assumes "decr RD1 RD2 m1 m2"
   9.128 +  shows "m2 y < m1 x"
   9.129 +  using prems
   9.130 +  by (cases RD1, cases RD2, auto simp:decr_def)
   9.131 +
   9.132 +lemma decreq_in_cdesc:
   9.133 +  assumes	"in_cdesc RD1 y x"
   9.134 +  assumes "in_cdesc RD2 z y"
   9.135 +  assumes "decreq RD1 RD2 m1 m2"
   9.136 +  shows "m2 y \<le> m1 x"
   9.137 +  using prems
   9.138 +  by (cases RD1, cases RD2, auto simp:decreq_def)
   9.139 +
   9.140 +
   9.141 +lemma no_inf_desc_nat_sequence:
   9.142 +  fixes s :: "nat \<Rightarrow> nat"
   9.143 +  assumes leq: "\<And>i. n \<le> i \<Longrightarrow> s (Suc i) \<le> s i"
   9.144 +  assumes less: "\<exists>\<^sub>\<infinity>i. s (Suc i) < s i"
   9.145 +  shows False
   9.146 +proof -
   9.147 +  {
   9.148 +	fix i j:: nat 
   9.149 +	assume "n \<le> i"
   9.150 +	assume "i \<le> j"
   9.151 +	{
   9.152 +	  fix k 
   9.153 +	  have "s (i + k) \<le> s i"
   9.154 +	  proof (induct k)
   9.155 +		case 0 thus ?case by simp
   9.156 +	  next
   9.157 +		case (Suc k)
   9.158 +		with leq[of "i + k"] `n \<le> i`
   9.159 +		show ?case by simp
   9.160 +	  qed
   9.161 +	}
   9.162 +	from this[of "j - i"] `n \<le> i` `i \<le> j`
   9.163 +	have "s j \<le> s i" by auto
   9.164 +  }
   9.165 +  note decr = this
   9.166 +  
   9.167 +  let ?min = "LEAST x. x \<in> range (\<lambda>i. s (n + i))"
   9.168 +  have "?min \<in> range (\<lambda>i. s (n + i))"
   9.169 +	by (rule LeastI) auto
   9.170 +  then obtain k where min: "?min = s (n + k)" by auto
   9.171 +  
   9.172 +  from less 
   9.173 +  obtain k' where "n + k < k'"
   9.174 +	and "s (Suc k') < s k'"
   9.175 +	unfolding INF_nat by auto
   9.176 +  
   9.177 +  with decr[of "n + k" k'] min
   9.178 +  have "s (Suc k') < ?min" by auto
   9.179 +  moreover from `n + k < k'`
   9.180 +  have "s (Suc k') = s (n + (Suc k' - n))" by simp
   9.181 +  ultimately
   9.182 +  show False using not_less_Least by blast
   9.183 +qed
   9.184 +
   9.185 +
   9.186 +
   9.187 +definition
   9.188 +  approx :: "scg \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc 
   9.189 +  \<Rightarrow> 'a measures \<Rightarrow> 'a measures \<Rightarrow> bool"
   9.190 +  where
   9.191 +  "approx G C C' M M'
   9.192 +  = (\<forall>i j. (dsc G i j \<longrightarrow> decr C C' (M i) (M' j))
   9.193 +  \<and>(eq G i j \<longrightarrow> decreq C C' (M i) (M' j)))"
   9.194 +
   9.195 +
   9.196 +
   9.197 +
   9.198 +(* Unfolding "approx" for finite graphs *)
   9.199 +
   9.200 +lemma approx_empty: 
   9.201 +  "approx (Graph {}) c1 c2 ms1 ms2"
   9.202 +  unfolding approx_def has_edge_def dest_graph.simps by simp
   9.203 +
   9.204 +lemma approx_less:
   9.205 +  assumes "stepP c1 c2 (ms1 i) (ms2 j) (op <)"
   9.206 +  assumes "approx (Graph Es) c1 c2 ms1 ms2"
   9.207 +  shows "approx (Graph (insert (i, \<down>, j) Es)) c1 c2 ms1 ms2"
   9.208 +  using prems
   9.209 +  unfolding approx_def has_edge_def dest_graph.simps decr_def
   9.210 +  by auto
   9.211 +
   9.212 +lemma approx_leq:
   9.213 +  assumes "stepP c1 c2 (ms1 i) (ms2 j) (op \<le>)"
   9.214 +  assumes "approx (Graph Es) c1 c2 ms1 ms2"
   9.215 +  shows "approx (Graph (insert (i, \<Down>, j) Es)) c1 c2 ms1 ms2"
   9.216 +  using prems
   9.217 +  unfolding approx_def has_edge_def dest_graph.simps decreq_def
   9.218 +  by auto
   9.219 +
   9.220 +
   9.221 +lemma "approx (Graph {(1, \<down>, 2),(2, \<Down>, 3)}) c1 c2 ms1 ms2"
   9.222 +  apply (intro approx_less approx_leq approx_empty) 
   9.223 +  oops
   9.224 +
   9.225 +
   9.226 +(*
   9.227 +fun
   9.228 +  no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool"
   9.229 +where
   9.230 +  "no_step (\<Gamma>1, r1, l1) (\<Gamma>2, r2, l2) =
   9.231 +  (\<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)"
   9.232 +*)
   9.233 +
   9.234 +lemma no_stepI:
   9.235 +  "stepP c1 c2 m1 m2 (\<lambda>x y. False)
   9.236 +  \<Longrightarrow> no_step c1 c2"
   9.237 +by (cases c1, cases c2) (auto simp: no_step_def)
   9.238 +
   9.239 +definition
   9.240 +  sound_int :: "acg \<Rightarrow> ('a, 'q) cdesc list 
   9.241 +  \<Rightarrow> 'a measures list \<Rightarrow> bool"
   9.242 +where
   9.243 +  "sound_int \<A> RDs M =
   9.244 +  (\<forall>n<length RDs. \<forall>m<length RDs.
   9.245 +  no_step (RDs ! n) (RDs ! m) \<or>
   9.246 +  (\<exists>G. (\<A> \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m) \<and> approx G (RDs ! n) (RDs ! m) (M ! n) (M ! m)))"
   9.247 +
   9.248 +
   9.249 +(* The following are uses by the tactics *)
   9.250 +lemma length_simps: "length [] = 0" "length (x#xs) = Suc (length xs)"
   9.251 +  by auto
   9.252 +
   9.253 +lemma all_less_zero: "\<forall>n<(0::nat). P n"
   9.254 +  by simp
   9.255 +
   9.256 +lemma all_less_Suc:
   9.257 +  assumes Pk: "P k"
   9.258 +  assumes Pn: "\<forall>n<k. P n"
   9.259 +  shows "\<forall>n<Suc k. P n"
   9.260 +proof (intro allI impI)
   9.261 +  fix n assume "n < Suc k"
   9.262 +  show "P n"
   9.263 +  proof (cases "n < k")
   9.264 +    case True with Pn show ?thesis by simp
   9.265 +  next
   9.266 +    case False with `n < Suc k` have "n = k" by simp
   9.267 +    with Pk show ?thesis by simp
   9.268 +  qed
   9.269 +qed
   9.270 +
   9.271 +
   9.272 +lemma step_witness:
   9.273 +  assumes "in_cdesc RD1 y x"
   9.274 +  assumes "in_cdesc RD2 z y"
   9.275 +  shows "\<not> no_step RD1 RD2"
   9.276 +  using prems
   9.277 +  by (cases RD1, cases RD2) (auto simp:no_step_def)
   9.278 +
   9.279 +
   9.280 +theorem SCT_on_relations:
   9.281 +  assumes R: "R = mk_rel RDs"
   9.282 +  assumes sound: "sound_int \<A> RDs M"
   9.283 +  assumes "SCT \<A>"
   9.284 +  shows "\<forall>x. acc R x"
   9.285 +proof (rule, rule classical)
   9.286 +  fix x
   9.287 +  assume "\<not> acc R x"
   9.288 +  with non_acc_has_idseq	
   9.289 +  have "\<exists>s. idseq R s x" .
   9.290 +  then obtain s where "idseq R s x" ..
   9.291 +  hence "\<exists>cs. \<forall>i. cs i \<in> set RDs \<and>
   9.292 +	in_cdesc (cs i) (s (Suc i)) (s i)"
   9.293 +	unfolding R by (rule ex_cs) 
   9.294 +  then obtain cs where
   9.295 +	[simp]: "\<And>i. cs i \<in> set RDs"
   9.296 +	  and ird[simp]: "\<And>i. in_cdesc (cs i) (s (Suc i)) (s i)"
   9.297 +	by blast
   9.298 +  
   9.299 +  let ?cis = "\<lambda>i. index_of RDs (cs i)"
   9.300 +  have "\<forall>i. \<exists>G. (\<A> \<turnstile> ?cis i \<leadsto>\<^bsup>G\<^esup> (?cis (Suc i)))
   9.301 +	\<and> approx G (RDs ! ?cis i) (RDs ! ?cis (Suc i)) 
   9.302 +	(M ! ?cis i) (M ! ?cis (Suc i))" (is "\<forall>i. \<exists>G. ?P i G")
   9.303 +  proof
   9.304 +	fix i
   9.305 +	let ?n = "?cis i" and ?n' = "?cis (Suc i)"
   9.306 +    
   9.307 +	have "in_cdesc (RDs ! ?n) (s (Suc i)) (s i)"
   9.308 +	  "in_cdesc (RDs ! ?n') (s (Suc (Suc i))) (s (Suc i))"
   9.309 +	  by (simp_all add:index_of_member)
   9.310 +	with step_witness
   9.311 + 	have "\<not> no_step (RDs ! ?n) (RDs ! ?n')" .
   9.312 +	moreover have
   9.313 +	  "?n < length RDs" 
   9.314 +	  "?n' < length RDs"
   9.315 +	  by (simp_all add:index_of_length[symmetric])
   9.316 +	ultimately
   9.317 +	obtain G
   9.318 +	  where "\<A> \<turnstile> ?n \<leadsto>\<^bsup>G\<^esup> ?n'"
   9.319 +	  and "approx G (RDs ! ?n) (RDs ! ?n') (M ! ?n) (M ! ?n')"
   9.320 +	  using sound
   9.321 +	  unfolding sound_int_def by auto
   9.322 +    
   9.323 +	thus "\<exists>G. ?P i G" by blast
   9.324 +  qed
   9.325 +  with choice
   9.326 +  have "\<exists>Gs. \<forall>i. ?P i (Gs i)" .
   9.327 +  then obtain Gs where 
   9.328 +	A: "\<And>i. \<A> \<turnstile> ?cis i \<leadsto>\<^bsup>(Gs i)\<^esup> (?cis (Suc i))" 
   9.329 +	and B: "\<And>i. approx (Gs i) (RDs ! ?cis i) (RDs ! ?cis (Suc i)) 
   9.330 +	(M ! ?cis i) (M ! ?cis (Suc i))"
   9.331 +	by blast
   9.332 +  
   9.333 +  let ?p = "\<lambda>i. (?cis i, Gs i)"
   9.334 +  
   9.335 +  from A have "has_ipath \<A> ?p"
   9.336 +	unfolding has_ipath_def
   9.337 +	by auto
   9.338 +  
   9.339 +  with `SCT \<A>` SCT_def 
   9.340 +  obtain th where "is_desc_thread th ?p"
   9.341 +	by auto
   9.342 +  
   9.343 +  then obtain n
   9.344 +	where fr: "\<forall>i\<ge>n. eqlat ?p th i"
   9.345 +	and inf: "\<exists>\<^sub>\<infinity>i. descat ?p th i"
   9.346 +	unfolding is_desc_thread_def by auto
   9.347 +  
   9.348 +  from B
   9.349 +  have approx:
   9.350 +	"\<And>i. approx (Gs i) (cs i) (cs (Suc i)) 
   9.351 +	(M ! ?cis i) (M ! ?cis (Suc i))"
   9.352 +	by (simp add:index_of_member)
   9.353 +  
   9.354 +  let ?seq = "\<lambda>i. (M ! ?cis i) (th i) (s i)"
   9.355 +  
   9.356 +  have "\<And>i. n < i \<Longrightarrow> ?seq (Suc i) \<le> ?seq i"
   9.357 +  proof -
   9.358 +	fix i 
   9.359 +	let ?q1 = "th i" and ?q2 = "th (Suc i)"
   9.360 +	assume "n < i"
   9.361 +	
   9.362 +	with fr	have "eqlat ?p th i" by simp 
   9.363 +	hence "dsc (Gs i) ?q1 ?q2 \<or> eq (Gs i) ?q1 ?q2" 
   9.364 +      by simp
   9.365 +	thus "?seq (Suc i) \<le> ?seq i"
   9.366 +	proof
   9.367 +	  assume "dsc (Gs i) ?q1 ?q2"
   9.368 +	  
   9.369 +	  with approx
   9.370 +	  have a:"decr (cs i) (cs (Suc i)) 
   9.371 +		((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)" 
   9.372 +		unfolding approx_def by auto
   9.373 +      
   9.374 +	  show ?thesis
   9.375 +		apply (rule less_imp_le)
   9.376 +		apply (rule decr_in_cdesc[of _ "s (Suc i)" "s i"])
   9.377 +		by (rule ird a)+
   9.378 +	next
   9.379 +	  assume "eq (Gs i) ?q1 ?q2"
   9.380 +	  
   9.381 +	  with approx
   9.382 +	  have a:"decreq (cs i) (cs (Suc i)) 
   9.383 +		((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)" 
   9.384 +		unfolding approx_def by auto
   9.385 +      
   9.386 +	  show ?thesis
   9.387 +		apply (rule decreq_in_cdesc[of _ "s (Suc i)" "s i"])
   9.388 +		by (rule ird a)+
   9.389 +	qed
   9.390 +  qed
   9.391 +  moreover have "\<exists>\<^sub>\<infinity>i. ?seq (Suc i) < ?seq i" unfolding INF_nat
   9.392 +  proof 
   9.393 +	fix i 
   9.394 +	from inf obtain j where "i < j" and d: "descat ?p th j"
   9.395 +	  unfolding INF_nat by auto
   9.396 +	let ?q1 = "th j" and ?q2 = "th (Suc j)"
   9.397 +	from d have "dsc (Gs j) ?q1 ?q2" by auto
   9.398 +	
   9.399 +	with approx
   9.400 +	have a:"decr (cs j) (cs (Suc j)) 
   9.401 +	  ((M ! ?cis j) ?q1) ((M ! ?cis (Suc j)) ?q2)" 
   9.402 +	  unfolding approx_def by auto
   9.403 +    
   9.404 +	have "?seq (Suc j) < ?seq j"
   9.405 +	  apply (rule decr_in_cdesc[of _ "s (Suc j)" "s j"])
   9.406 +	  by (rule ird a)+
   9.407 +	with `i < j` 
   9.408 +	show "\<exists>j. i < j \<and> ?seq (Suc j) < ?seq j" by auto
   9.409 +  qed
   9.410 +  ultimately have False
   9.411 +    by (rule no_inf_desc_nat_sequence[of "Suc n"]) simp
   9.412 +  thus "acc R x" ..
   9.413 +qed
   9.414 +
   9.415 +
   9.416 +end
   9.417 \ No newline at end of file
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Library/SCT_Misc.thy	Mon Feb 26 21:34:16 2007 +0100
    10.3 @@ -0,0 +1,206 @@
    10.4 +theory SCT_Misc
    10.5 +imports Main
    10.6 +begin
    10.7 +
    10.8 +
    10.9 +subsection {* Searching in lists *}
   10.10 +
   10.11 +fun index_of :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
   10.12 +where
   10.13 +  "index_of [] c = 0"
   10.14 +| "index_of (x#xs) c = (if x = c then 0 else Suc (index_of xs c))"
   10.15 +
   10.16 +lemma index_of_member: 
   10.17 +  "(x \<in> set l) \<Longrightarrow> (l ! index_of l x = x)"
   10.18 +  by (induct l) auto
   10.19 +
   10.20 +lemma index_of_length:
   10.21 +  "(x \<in> set l) = (index_of l x < length l)"
   10.22 +  by (induct l) auto
   10.23 +
   10.24 +
   10.25 +
   10.26 +subsection {* Some reasoning tools *}
   10.27 +
   10.28 +lemma inc_induct[consumes 1]:
   10.29 +  assumes less: "i \<le> j"
   10.30 +  assumes base: "P j"
   10.31 +  assumes step: "\<And>i. \<lbrakk>i < j; P (Suc i)\<rbrakk> \<Longrightarrow> P i"
   10.32 +  shows "P i"
   10.33 +  using less
   10.34 +proof (induct d\<equiv>"j - i" arbitrary: i)
   10.35 +  case (0 i)
   10.36 +  with `i \<le> j` have "i = j" by simp
   10.37 +  with base show ?case by simp
   10.38 +next
   10.39 +  case (Suc d i)
   10.40 +  hence "i < j" "P (Suc i)"
   10.41 +    by simp_all
   10.42 +  thus "P i" by (rule step)
   10.43 +qed
   10.44 +
   10.45 +lemma strict_inc_induct[consumes 1]:
   10.46 +  assumes less: "i < j"
   10.47 +  assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i"
   10.48 +  assumes step: "\<And>i. \<lbrakk>i < j; P (Suc i)\<rbrakk> \<Longrightarrow> P i"
   10.49 +  shows "P i"
   10.50 +  using less
   10.51 +proof (induct d\<equiv>"j - i - 1" arbitrary: i)
   10.52 +  case (0 i)
   10.53 +  with `i < j` have "j = Suc i" by simp
   10.54 +  with base show ?case by simp
   10.55 +next
   10.56 +  case (Suc d i)
   10.57 +  hence "i < j" "P (Suc i)"
   10.58 +    by simp_all
   10.59 +  thus "P i" by (rule step)
   10.60 +qed
   10.61 +
   10.62 +
   10.63 +lemma three_cases:
   10.64 +  assumes "a1 \<Longrightarrow> thesis"
   10.65 +  assumes "a2 \<Longrightarrow> thesis"
   10.66 +  assumes "a3 \<Longrightarrow> thesis"
   10.67 +  assumes "\<And>R. \<lbrakk>a1 \<Longrightarrow> R; a2 \<Longrightarrow> R; a3 \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   10.68 +  shows "thesis"
   10.69 +  using prems
   10.70 +  by auto
   10.71 +
   10.72 +
   10.73 +section {* Sequences *}
   10.74 +
   10.75 +types
   10.76 +  'a sequence = "nat \<Rightarrow> 'a"
   10.77 +
   10.78 +subsection {* Increasing sequences *}
   10.79 +
   10.80 +definition increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
   10.81 +where
   10.82 +  "increasing s = (\<forall>i j. i < j \<longrightarrow> s i < s j)"
   10.83 +
   10.84 +lemma increasing_strict:
   10.85 +  assumes "increasing s"
   10.86 +  assumes "i < j"
   10.87 +  shows "s i < s j"
   10.88 +  using prems
   10.89 +  unfolding increasing_def by simp
   10.90 +
   10.91 +lemma increasing_weak:
   10.92 +  assumes "increasing s"
   10.93 +  assumes "i \<le> j"
   10.94 +  shows "s i \<le> s j"
   10.95 +  using prems increasing_strict[of s i j]
   10.96 +  by (cases "i<j") auto
   10.97 +
   10.98 +lemma increasing_inc:
   10.99 +  assumes [simp]: "increasing s"
  10.100 +  shows "n \<le> s n"
  10.101 +proof (induct n)
  10.102 +  case (Suc n)
  10.103 +  with increasing_strict[of s n "Suc n"]
  10.104 +  show ?case by auto
  10.105 +qed auto
  10.106 +
  10.107 +
  10.108 +lemma increasing_bij:
  10.109 +  assumes [simp]: "increasing s"
  10.110 +  shows "(s i < s j) = (i < j)"
  10.111 +proof
  10.112 +  assume "s i < s j"
  10.113 +  show "i < j"
  10.114 +  proof (rule classical)
  10.115 +    assume "\<not> ?thesis"
  10.116 +    hence "j \<le> i" by arith
  10.117 +    with increasing_weak have "s j \<le> s i" by simp
  10.118 +    with `s i < s j` show ?thesis by simp
  10.119 +  qed
  10.120 +qed (simp add:increasing_strict)
  10.121 +
  10.122 +
  10.123 +
  10.124 +
  10.125 +subsection {* Sections induced by an increasing sequence *}
  10.126 +
  10.127 +abbreviation
  10.128 +  "section s i == {s i ..< s (Suc i)}"
  10.129 +
  10.130 +definition
  10.131 +  "section_of s n = (LEAST i. n < s (Suc i))"
  10.132 +
  10.133 +
  10.134 +lemma section_help:
  10.135 +  assumes [intro, simp]: "increasing s"
  10.136 +  shows "\<exists>i. n < s (Suc i)" 
  10.137 +proof -
  10.138 +  from increasing_inc have "n \<le> s n" .
  10.139 +  also from increasing_strict have "\<dots> < s (Suc n)" by simp
  10.140 +  finally show ?thesis ..
  10.141 +qed
  10.142 +
  10.143 +lemma section_of2:
  10.144 +  assumes "increasing s"
  10.145 +  shows "n < s (Suc (section_of s n))"
  10.146 +  unfolding section_of_def
  10.147 +  by (rule LeastI_ex) (rule section_help)
  10.148 +
  10.149 +
  10.150 +lemma section_of1:
  10.151 +  assumes [simp, intro]: "increasing s"
  10.152 +  assumes "s i \<le> n"
  10.153 +  shows "s (section_of s n) \<le> n"
  10.154 +proof (rule classical)
  10.155 +  let ?m = "section_of s n"
  10.156 +
  10.157 +  assume "\<not> ?thesis"
  10.158 +  hence a: "n < s ?m" by simp
  10.159 +  
  10.160 +  have nonzero: "?m \<noteq> 0"
  10.161 +  proof
  10.162 +    assume "?m = 0"
  10.163 +    from increasing_weak have "s 0 \<le> s i" by simp
  10.164 +    also note `\<dots> \<le> n`
  10.165 +    finally show False using `?m = 0` `n < s ?m` by simp 
  10.166 +  qed
  10.167 +  with a have "n < s (Suc (?m - 1))" by simp
  10.168 +  with Least_le have "?m \<le> ?m - 1"
  10.169 +    unfolding section_of_def .
  10.170 +  with nonzero show ?thesis by simp
  10.171 +qed
  10.172 +
  10.173 +lemma section_of_known: 
  10.174 +  assumes [simp]: "increasing s"
  10.175 +  assumes in_sect: "k \<in> section s i"
  10.176 +  shows "section_of s k = i" (is "?s = i")
  10.177 +proof (rule classical)
  10.178 +  assume "\<not> ?thesis"
  10.179 +
  10.180 +  hence "?s < i \<or> ?s > i" by arith
  10.181 +  thus ?thesis
  10.182 +  proof
  10.183 +    assume "?s < i"
  10.184 +    hence "Suc ?s \<le> i" by simp
  10.185 +    with increasing_weak have "s (Suc ?s) \<le> s i" by simp
  10.186 +    moreover have "k < s (Suc ?s)" using section_of2 by simp
  10.187 +    moreover from in_sect have "s i \<le> k" by simp
  10.188 +    ultimately show ?thesis by simp 
  10.189 +  next
  10.190 +    assume "i < ?s" hence "Suc i \<le> ?s" by simp
  10.191 +    with increasing_weak have "s (Suc i) \<le> s ?s" by simp
  10.192 +    moreover 
  10.193 +    from in_sect have "s i \<le> k" by simp
  10.194 +    with section_of1 have "s ?s \<le> k" by simp
  10.195 +    moreover from in_sect have "k < s (Suc i)" by simp
  10.196 +    ultimately show ?thesis by simp
  10.197 +  qed
  10.198 +qed 
  10.199 +
  10.200 +  
  10.201 +lemma in_section_of: 
  10.202 +  assumes [simp, intro]: "increasing s"
  10.203 +  assumes "s i \<le> k"
  10.204 +  shows "k \<in> section s (section_of s k)"
  10.205 +  using prems
  10.206 +  by (auto intro:section_of1 section_of2)
  10.207 +
  10.208 +
  10.209 +end
  10.210 \ No newline at end of file
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Library/SCT_Theorem.thy	Mon Feb 26 21:34:16 2007 +0100
    11.3 @@ -0,0 +1,1416 @@
    11.4 +theory SCT_Theorem
    11.5 +imports Main Ramsey SCT_Misc SCT_Definition
    11.6 +begin
    11.7 +
    11.8 +
    11.9 +section {* The size change criterion SCT *}
   11.10 +
   11.11 +
   11.12 +definition is_thread :: "nat \<Rightarrow> nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> bool"
   11.13 +where
   11.14 +  "is_thread n \<theta> p = (\<forall>i\<ge>n. eqlat p \<theta> i)"
   11.15 +
   11.16 +definition is_fthread :: 
   11.17 +  "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   11.18 +where
   11.19 +  "is_fthread \<theta> mp i j = (\<forall>k\<in>{i..<j}. eqlat mp \<theta> k)"
   11.20 +
   11.21 +definition is_desc_fthread ::
   11.22 +  "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   11.23 +where
   11.24 +  "is_desc_fthread \<theta> mp i j = 
   11.25 +  (is_fthread \<theta> mp i j \<and>
   11.26 +  (\<exists>k\<in>{i..<j}. descat mp \<theta> k))"
   11.27 +
   11.28 +definition
   11.29 +  "has_fth p i j n m = 
   11.30 +  (\<exists>\<theta>. is_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
   11.31 +
   11.32 +definition
   11.33 +  "has_desc_fth p i j n m = 
   11.34 +  (\<exists>\<theta>. is_desc_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
   11.35 +
   11.36 +
   11.37 +
   11.38 +section {* Bounded graphs and threads *}
   11.39 +
   11.40 +definition 
   11.41 +  "bounded_scg (P::nat) (G::scg) = 
   11.42 +  (\<forall>p e p'. has_edge G p e p' \<longrightarrow> p < P \<and> p' < P)"
   11.43 +
   11.44 +definition
   11.45 +  "bounded_acg P ACG = 
   11.46 +  (\<forall>n G n'. has_edge ACG n G n' \<longrightarrow> n < P \<and> n' < P \<and> bounded_scg P G)"
   11.47 +  
   11.48 +definition
   11.49 +  "bounded_mp P mp = (\<forall>i. bounded_scg P (snd (mp i)))"
   11.50 +
   11.51 +definition (* = finite (range \<theta>) *)
   11.52 +  "bounded_th (P::nat) n \<theta> = (\<forall>i>n. \<theta> i < P)"
   11.53 +
   11.54 +
   11.55 +definition 
   11.56 +  "finite_scg (G::scg) = (\<exists>P. bounded_scg P G)"
   11.57 +
   11.58 +definition
   11.59 +  "finite_acg (A::acg) = (\<exists>P. bounded_acg P A)"
   11.60 +
   11.61 +
   11.62 +lemma "finite (insert x A) = finite A"
   11.63 +by simp
   11.64 +
   11.65 +
   11.66 +lemma finite_scg_finite[simp]: "finite_scg (Graph G) = finite G"
   11.67 +proof
   11.68 +  assume "finite_scg (Graph G)"
   11.69 +  thm bounded_scg_def
   11.70 +  
   11.71 +  then obtain P where bounded: "bounded_scg P (Graph G)" 
   11.72 +    by (auto simp:finite_scg_def)
   11.73 +
   11.74 +  show "finite G"
   11.75 +  proof (rule finite_subset)
   11.76 +    from bounded 
   11.77 +    show "G \<subseteq> {0 .. P - 1} \<times> { LESS, LEQ } \<times> { 0 .. P - 1}"
   11.78 +      apply (auto simp:bounded_scg_def has_edge_def)
   11.79 +      apply force
   11.80 +      apply (case_tac "aa", auto)
   11.81 +      apply force
   11.82 +      done
   11.83 +
   11.84 +    show "finite \<dots>"
   11.85 +      by (auto intro: finite_cartesian_product finite_atLeastAtMost)
   11.86 +  qed
   11.87 +next
   11.88 +
   11.89 +  assume "finite G"
   11.90 +  thus "finite_scg (Graph G)"
   11.91 +  proof induct
   11.92 +    show "finite_scg (Graph {})"
   11.93 +      unfolding finite_scg_def bounded_scg_def has_edge_def by auto
   11.94 +  next
   11.95 +    fix x G 
   11.96 +    assume "finite G" "x \<notin> G" "finite_scg (Graph G)"
   11.97 +    then obtain P
   11.98 +      where bG: "bounded_scg P (Graph G)" 
   11.99 +      by (auto simp:finite_scg_def)
  11.100 +    
  11.101 +    obtain p e p' where x: "x = (p, e, p')" by (cases x, auto)
  11.102 +    
  11.103 +    let ?Q = "max P (max (Suc p) (Suc p'))"
  11.104 +    have "P \<le> ?Q" "Suc p \<le> ?Q" "Suc p' \<le> ?Q" by auto
  11.105 +    with bG
  11.106 +    have "bounded_scg ?Q (Graph (insert x G))" 
  11.107 +      unfolding x bounded_scg_def has_edge_def
  11.108 +      apply simp
  11.109 +      apply (intro allI, elim allE)
  11.110 +      by auto
  11.111 +    thus "finite_scg (Graph (insert x G))"
  11.112 +      by (auto simp:finite_scg_def)
  11.113 +  qed
  11.114 +qed
  11.115 +
  11.116 +
  11.117 +lemma finite_acg_empty:
  11.118 +  "finite_acg (Graph {})"
  11.119 +unfolding finite_acg_def bounded_acg_def has_edge_def
  11.120 +by auto
  11.121 +
  11.122 +
  11.123 +
  11.124 +lemma bounded_scg_up: "bounded_scg P G \<Longrightarrow> P \<le> Q \<Longrightarrow> bounded_scg Q G"
  11.125 +  unfolding bounded_scg_def
  11.126 +  by force
  11.127 +
  11.128 +
  11.129 +lemma bounded_up: "bounded_acg P G \<Longrightarrow> P \<le> Q \<Longrightarrow> bounded_acg Q G"
  11.130 +  unfolding bounded_acg_def 
  11.131 +  apply auto
  11.132 +  apply force+
  11.133 +  apply (rule bounded_scg_up)
  11.134 +  by auto
  11.135 +
  11.136 +lemma bacg_insert:
  11.137 +  assumes "bounded_acg P (Graph A)"
  11.138 +  assumes "n < P" "m < P" "bounded_scg P G"
  11.139 +  shows "bounded_acg P (Graph (insert (n, G, m) A))"
  11.140 +  using prems
  11.141 +  unfolding bounded_acg_def has_edge_def 
  11.142 +  by auto
  11.143 +
  11.144 +lemma finite_acg_ins:
  11.145 +  "finite_acg (Graph (insert (n,G,m) A)) = 
  11.146 +  (finite_scg G \<and> finite_acg (Graph A))" (is "?A = (?B \<and> ?C)")
  11.147 +proof
  11.148 +  assume "?A"
  11.149 +  thus "?B \<and> ?C"
  11.150 +    unfolding finite_acg_def bounded_acg_def finite_scg_def has_edge_def
  11.151 +    by auto
  11.152 +next
  11.153 +  assume "?B \<and> ?C"
  11.154 +  thus ?A
  11.155 +  proof
  11.156 +    assume "?B" "?C"
  11.157 +
  11.158 +    from `?C`
  11.159 +    obtain P where bA: "bounded_acg P (Graph A)" by (auto simp:finite_acg_def)
  11.160 +    from `?B` 
  11.161 +    obtain P' where bG: "bounded_scg P' G" by (auto simp:finite_scg_def)
  11.162 +
  11.163 +    let ?Q = "max (max P P') (max (Suc n) (Suc m))"
  11.164 +    have "P \<le> ?Q" "n < ?Q" "m < ?Q" by auto
  11.165 +    have "bounded_acg ?Q (Graph (insert (n, G, m) A))"
  11.166 +      apply (rule bacg_insert)
  11.167 +      apply (rule bounded_up)
  11.168 +      apply (rule bA)
  11.169 +      apply auto
  11.170 +      apply (rule bounded_scg_up)
  11.171 +      apply (rule bG)
  11.172 +      by auto
  11.173 +    thus "finite_acg (Graph (insert (n, G, m) A))"
  11.174 +      by (auto simp:finite_acg_def)
  11.175 +  qed
  11.176 +qed
  11.177 +
  11.178 +
  11.179 +lemma bounded_mpath:
  11.180 +  assumes "has_ipath acg mp"
  11.181 +  and "bounded_acg P acg"
  11.182 +  shows "bounded_mp P mp"
  11.183 +  using prems
  11.184 +  unfolding bounded_acg_def bounded_mp_def has_ipath_def
  11.185 +  by blast
  11.186 +
  11.187 +lemma bounded_th: 
  11.188 +  assumes th: "is_thread n \<theta> mp"
  11.189 +  and mp: "bounded_mp P mp"
  11.190 +  shows "bounded_th P n \<theta>"
  11.191 +  unfolding bounded_th_def
  11.192 +proof (intro allI impI)
  11.193 +  fix i assume "n < i"
  11.194 +  
  11.195 +  from mp have "bounded_scg P (snd (mp i))" unfolding bounded_mp_def ..
  11.196 +  moreover
  11.197 +  from th `n < i` have "eqlat mp \<theta> i" unfolding is_thread_def by auto
  11.198 +  ultimately
  11.199 +  show "\<theta> i < P" unfolding bounded_scg_def by auto
  11.200 +qed
  11.201 +
  11.202 +
  11.203 +lemma finite_range:
  11.204 +  fixes f :: "nat \<Rightarrow> 'a"
  11.205 +  assumes fin: "finite (range f)"
  11.206 +  shows "\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x"
  11.207 +proof (rule classical)
  11.208 +  assume "\<not>(\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x)"
  11.209 +  hence "\<forall>x. \<exists>j. \<forall>i>j. f i \<noteq> x"
  11.210 +    unfolding INF_nat by blast
  11.211 +  with choice
  11.212 +  have "\<exists>j. \<forall>x. \<forall>i>(j x). f i \<noteq> x" .
  11.213 +  then obtain j where 
  11.214 +    neq: "\<And>x i. j x < i \<Longrightarrow> f i \<noteq> x" by blast
  11.215 +
  11.216 +  from fin have "finite (range (j o f))" 
  11.217 +    by (auto simp:comp_def)
  11.218 +  with finite_nat_bounded
  11.219 +  obtain m where "range (j o f) \<subseteq> {..<m}" by blast
  11.220 +  hence "j (f m) < m" unfolding comp_def by auto
  11.221 +
  11.222 +  with neq[of "f m" m] show ?thesis by blast
  11.223 +qed
  11.224 +
  11.225 +
  11.226 +lemma bounded_th_infinite_visit:
  11.227 +  fixes \<theta> :: "nat sequence"
  11.228 +  assumes b: "bounded_th P n \<theta>"
  11.229 +  shows "\<exists>p. \<exists>\<^sub>\<infinity>i. \<theta> i = p" 
  11.230 +proof -
  11.231 +  have split: "range \<theta> = (\<theta> ` {0 .. n}) \<union> (\<theta> ` {i. n < i})"
  11.232 +    (is "\<dots> = ?A \<union> ?B")
  11.233 +    unfolding image_Un[symmetric] by auto
  11.234 +
  11.235 +  have "finite ?A" by (rule finite_imageI) auto
  11.236 +  moreover
  11.237 +  have "finite ?B"
  11.238 +  proof (rule finite_subset)
  11.239 +    from b
  11.240 +    show "?B \<subseteq> { 0 ..< P }"
  11.241 +      unfolding bounded_th_def
  11.242 +      by auto
  11.243 +    show "finite \<dots>" by auto
  11.244 +  qed
  11.245 +
  11.246 +  ultimately have "finite (range \<theta>)"
  11.247 +    unfolding split by auto
  11.248 +
  11.249 +  with finite_range show ?thesis .
  11.250 +qed
  11.251 +
  11.252 +
  11.253 +lemma bounded_scgcomp:
  11.254 +  "bounded_scg P A 
  11.255 +  \<Longrightarrow> bounded_scg P B 
  11.256 +  \<Longrightarrow> bounded_scg P (A * B)"
  11.257 +  unfolding bounded_scg_def
  11.258 +  by (auto simp:in_grcomp)
  11.259 +
  11.260 +lemma bounded_acgcomp:
  11.261 +  "bounded_acg P A 
  11.262 +  \<Longrightarrow> bounded_acg P B 
  11.263 +  \<Longrightarrow> bounded_acg P (A * B)"
  11.264 +  unfolding bounded_acg_def
  11.265 +  by (auto simp:in_grcomp intro!:bounded_scgcomp) 
  11.266 +
  11.267 +lemma bounded_acgpow:
  11.268 +  "bounded_acg P A
  11.269 +  \<Longrightarrow> bounded_acg P (A ^ (Suc n))"
  11.270 +  by (induct n, simp add:power_Suc) 
  11.271 +   (subst power_Suc, blast intro:bounded_acgcomp)
  11.272 +
  11.273 +lemma bounded_plus:
  11.274 +  assumes b: "bounded_acg P acg"
  11.275 +  shows "bounded_acg P (tcl acg)"
  11.276 +  unfolding bounded_acg_def
  11.277 +proof (intro allI impI conjI)
  11.278 +  fix n G m
  11.279 +  assume "tcl acg \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m"
  11.280 +  then obtain i where "0 < i" and i: "acg ^ i \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m"
  11.281 +    unfolding in_tcl by auto (* FIXME: Disambiguate \<turnstile> Grammar *)
  11.282 +  from b have "bounded_acg P (acg ^ (Suc (i - 1)))"
  11.283 +    by (rule bounded_acgpow)
  11.284 +  with `0 < i` have "bounded_acg P (acg ^ i)" by simp
  11.285 +  with i
  11.286 +  show "n < P" "m < P" "bounded_scg P G"
  11.287 +    unfolding bounded_acg_def
  11.288 +    by auto
  11.289 +qed
  11.290 +
  11.291 +
  11.292 +lemma bounded_scg_def':
  11.293 +  "bounded_scg P G = (\<forall>(p,e,p')\<in>dest_graph G. p < P \<and> p' < P)"
  11.294 +  unfolding bounded_scg_def has_edge_def
  11.295 +  by auto
  11.296 +
  11.297 +
  11.298 +lemma finite_bounded_scg: "finite { G. bounded_scg P G }"
  11.299 +proof (rule finite_subset)
  11.300 +  show "{G. bounded_scg P G} \<subseteq> 
  11.301 +    Graph ` (Pow ({0 .. P - 1} \<times> UNIV \<times> {0 .. P - 1}))"
  11.302 +  proof (rule, simp)
  11.303 +    fix G 
  11.304 +    
  11.305 +    assume b: "bounded_scg P G"
  11.306 +
  11.307 +    show "G \<in> Graph ` Pow ({0..P - Suc 0} \<times> UNIV \<times> {0..P - Suc 0})"
  11.308 +    proof (cases G)
  11.309 +      fix G' assume [simp]: "G = Graph G'"
  11.310 +      
  11.311 +      from b show ?thesis
  11.312 +        by (auto simp:bounded_scg_def' image_def)
  11.313 +    qed
  11.314 +  qed
  11.315 +
  11.316 +  show "finite \<dots>"
  11.317 +    apply (rule finite_imageI)
  11.318 +    apply (unfold finite_Pow_iff)
  11.319 +    by (intro finite_cartesian_product finite_atLeastAtMost 
  11.320 +      finite_class.finite)
  11.321 +qed
  11.322 +
  11.323 +lemma bounded_finite:
  11.324 +  assumes bounded: "bounded_acg P A"
  11.325 +  shows "finite (dest_graph A)"
  11.326 +proof (rule finite_subset)
  11.327 +  
  11.328 +  from bounded
  11.329 +  show "dest_graph A \<subseteq> {0 .. P - 1} \<times> { G. bounded_scg P G } \<times> { 0 .. P - 1}"
  11.330 +    by (auto simp:bounded_acg_def has_edge_def) force+
  11.331 +
  11.332 +  show "finite \<dots>"
  11.333 +    by (intro finite_cartesian_product finite_atLeastAtMost finite_bounded_scg)
  11.334 +qed
  11.335 +
  11.336 +
  11.337 +
  11.338 +section {* Contraction and more *}
  11.339 +
  11.340 +
  11.341 +abbreviation 
  11.342 +  "pdesc P == (fst P, prod P, end_node P)"
  11.343 +
  11.344 +lemma pdesc_acgplus: 
  11.345 +  assumes "has_ipath \<A> p"
  11.346 +  and "i < j"
  11.347 +  shows "has_edge (tcl \<A>) (fst (p\<langle>i,j\<rangle>)) (prod (p\<langle>i,j\<rangle>)) (end_node (p\<langle>i,j\<rangle>))"
  11.348 +  unfolding plus_paths
  11.349 +  apply (rule exI)
  11.350 +  apply (insert prems)  
  11.351 +  by (auto intro:sub_path_is_path[of "\<A>" p i j] simp:sub_path_def)
  11.352 +
  11.353 +
  11.354 +
  11.355 +
  11.356 +lemma combine_fthreads: 
  11.357 +  assumes range: "i < j" "j \<le> k"
  11.358 +  shows 
  11.359 +  "has_fth p i k m r =
  11.360 +  (\<exists>n. has_fth p i j m n \<and> has_fth p j k n r)" (is "?L = ?R")
  11.361 +proof (intro iffI)
  11.362 +  assume "?L"
  11.363 +  then obtain \<theta>
  11.364 +    where "is_fthread \<theta> p i k" 
  11.365 +    and [simp]: "\<theta> i = m" "\<theta> k = r"
  11.366 +    by (auto simp:has_fth_def)
  11.367 +
  11.368 +  with range
  11.369 +  have "is_fthread \<theta> p i j" and "is_fthread \<theta> p j k"
  11.370 +    by (auto simp:is_fthread_def)
  11.371 +  hence "has_fth p i j m (\<theta> j)" and "has_fth p j k (\<theta> j) r"
  11.372 +    by (auto simp:has_fth_def)
  11.373 +  thus "?R" by auto
  11.374 +next
  11.375 +  assume "?R"
  11.376 +  then obtain n \<theta>1 \<theta>2
  11.377 +    where ths: "is_fthread \<theta>1 p i j" "is_fthread \<theta>2 p j k"
  11.378 +    and [simp]: "\<theta>1 i = m" "\<theta>1 j = n" "\<theta>2 j = n" "\<theta>2 k = r"
  11.379 +    by (auto simp:has_fth_def)
  11.380 +
  11.381 +  let ?\<theta> = "(\<lambda>i. if i < j then \<theta>1 i else \<theta>2 i)"
  11.382 +  have "is_fthread ?\<theta> p i k"
  11.383 +    unfolding is_fthread_def
  11.384 +  proof
  11.385 +    fix l assume range: "l \<in> {i..<k}"
  11.386 +    
  11.387 +    show "eqlat p ?\<theta> l"
  11.388 +    proof (cases rule:three_cases)
  11.389 +      assume "Suc l < j"
  11.390 +      with ths range show ?thesis 
  11.391 +	unfolding is_fthread_def Ball_def
  11.392 +	by simp
  11.393 +    next
  11.394 +      assume "Suc l = j"
  11.395 +      hence "l < j" "\<theta>2 (Suc l) = \<theta>1 (Suc l)" by auto
  11.396 +      with ths range show ?thesis 
  11.397 +	unfolding is_fthread_def Ball_def
  11.398 +	by simp
  11.399 +    next
  11.400 +      assume "j \<le> l"
  11.401 +      with ths range show ?thesis 
  11.402 +	unfolding is_fthread_def Ball_def
  11.403 +	by simp
  11.404 +    qed arith
  11.405 +  qed
  11.406 +  moreover 
  11.407 +  have "?\<theta> i = m" "?\<theta> k = r" using range by auto
  11.408 +  ultimately show "has_fth p i k m r" 
  11.409 +    by (auto simp:has_fth_def)
  11.410 +qed 
  11.411 +
  11.412 +
  11.413 +lemma desc_is_fthread:
  11.414 +  "is_desc_fthread \<theta> p i k \<Longrightarrow> is_fthread \<theta> p i k"
  11.415 +  unfolding is_desc_fthread_def
  11.416 +  by simp
  11.417 +
  11.418 +
  11.419 +lemma combine_dfthreads: 
  11.420 +  assumes range: "i < j" "j \<le> k"
  11.421 +  shows 
  11.422 +  "has_desc_fth p i k m r =
  11.423 +  (\<exists>n. (has_desc_fth p i j m n \<and> has_fth p j k n r)
  11.424 +  \<or> (has_fth p i j m n \<and> has_desc_fth p j k n r))" (is "?L = ?R")
  11.425 +proof 
  11.426 +  assume "?L"
  11.427 +  then obtain \<theta>
  11.428 +    where desc: "is_desc_fthread \<theta> p i k" 
  11.429 +    and [simp]: "\<theta> i = m" "\<theta> k = r"
  11.430 +    by (auto simp:has_desc_fth_def)
  11.431 +
  11.432 +  hence "is_fthread \<theta> p i k"
  11.433 +    by (simp add: desc_is_fthread)
  11.434 +  with range have fths: "is_fthread \<theta> p i j" "is_fthread \<theta> p j k"
  11.435 +    unfolding is_fthread_def
  11.436 +    by auto
  11.437 +  hence hfths: "has_fth p i j m (\<theta> j)" "has_fth p j k (\<theta> j) r"
  11.438 +    by (auto simp:has_fth_def)
  11.439 +
  11.440 +  from desc obtain l 
  11.441 +    where "i \<le> l" "l < k"
  11.442 +    and "descat p \<theta> l"
  11.443 +    by (auto simp:is_desc_fthread_def)
  11.444 +
  11.445 +  with fths
  11.446 +  have "is_desc_fthread \<theta> p i j \<or> is_desc_fthread \<theta> p j k"
  11.447 +    unfolding is_desc_fthread_def
  11.448 +    by (cases "l < j") auto
  11.449 +  hence "has_desc_fth p i j m (\<theta> j) \<or> has_desc_fth p j k (\<theta> j) r"
  11.450 +    by (auto simp:has_desc_fth_def)
  11.451 +  with hfths show ?R
  11.452 +    by auto
  11.453 +next
  11.454 +  assume "?R"
  11.455 +  then obtain n \<theta>1 \<theta>2
  11.456 +    where "(is_desc_fthread \<theta>1 p i j \<and> is_fthread \<theta>2 p j k)
  11.457 +    \<or> (is_fthread \<theta>1 p i j \<and> is_desc_fthread \<theta>2 p j k)"
  11.458 +    and [simp]: "\<theta>1 i = m" "\<theta>1 j = n" "\<theta>2 j = n" "\<theta>2 k = r"
  11.459 +    by (auto simp:has_fth_def has_desc_fth_def)
  11.460 +
  11.461 +  hence ths2: "is_fthread \<theta>1 p i j" "is_fthread \<theta>2 p j k"
  11.462 +    and dths: "is_desc_fthread \<theta>1 p i j \<or> is_desc_fthread \<theta>2 p j k"
  11.463 +    by (auto simp:desc_is_fthread)
  11.464 +
  11.465 +  let ?\<theta> = "(\<lambda>i. if i < j then \<theta>1 i else \<theta>2 i)"
  11.466 +  have "is_fthread ?\<theta> p i k"
  11.467 +    unfolding is_fthread_def
  11.468 +  proof
  11.469 +    fix l assume range: "l \<in> {i..<k}"
  11.470 +    
  11.471 +    show "eqlat p ?\<theta> l"
  11.472 +    proof (cases rule:three_cases)
  11.473 +      assume "Suc l < j"
  11.474 +      with ths2 range show ?thesis 
  11.475 +	unfolding is_fthread_def Ball_def
  11.476 +	by simp
  11.477 +    next
  11.478 +      assume "Suc l = j"
  11.479 +      hence "l < j" "\<theta>2 (Suc l) = \<theta>1 (Suc l)" by auto
  11.480 +      with ths2 range show ?thesis 
  11.481 +	unfolding is_fthread_def Ball_def
  11.482 +	by simp
  11.483 +    next
  11.484 +      assume "j \<le> l"
  11.485 +      with ths2 range show ?thesis 
  11.486 +	unfolding is_fthread_def Ball_def
  11.487 +	by simp
  11.488 +    qed arith
  11.489 +  qed
  11.490 +  moreover
  11.491 +  from dths
  11.492 +  have "\<exists>l. i \<le> l \<and> l < k \<and> descat p ?\<theta> l"
  11.493 +  proof
  11.494 +    assume "is_desc_fthread \<theta>1 p i j"
  11.495 +
  11.496 +    then obtain l where range: "i \<le> l" "l < j" and "descat p \<theta>1 l"
  11.497 +      unfolding is_desc_fthread_def Bex_def by auto
  11.498 +    hence "descat p ?\<theta> l" 
  11.499 +      by (cases "Suc l = j", auto)
  11.500 +    with `j \<le> k` and range show ?thesis 
  11.501 +      by (rule_tac x="l" in exI, auto)
  11.502 +  next
  11.503 +    assume "is_desc_fthread \<theta>2 p j k"
  11.504 +    then obtain l where range: "j \<le> l" "l < k" and "descat p \<theta>2 l"
  11.505 +      unfolding is_desc_fthread_def Bex_def by auto
  11.506 +    with `i < j` have "descat p ?\<theta> l" "i \<le> l"
  11.507 +      by auto
  11.508 +    with range show ?thesis 
  11.509 +      by (rule_tac x="l" in exI, auto)
  11.510 +  qed
  11.511 +  ultimately have "is_desc_fthread ?\<theta> p i k"
  11.512 +    by (simp add: is_desc_fthread_def Bex_def)
  11.513 +
  11.514 +  moreover 
  11.515 +  have "?\<theta> i = m" "?\<theta> k = r" using range by auto
  11.516 +
  11.517 +  ultimately show "has_desc_fth p i k m r" 
  11.518 +    by (auto simp:has_desc_fth_def)
  11.519 +qed 
  11.520 +
  11.521 +    
  11.522 +
  11.523 +lemma fth_single:
  11.524 +  "has_fth p i (Suc i) m n = eql (snd (p i)) m n" (is "?L = ?R")
  11.525 +proof 
  11.526 +  assume "?L" thus "?R"
  11.527 +    unfolding is_fthread_def Ball_def has_fth_def
  11.528 +    by auto
  11.529 +next
  11.530 +  let ?\<theta> = "\<lambda>k. if k = i then m else n"
  11.531 +  assume edge: "?R"
  11.532 +  hence "is_fthread ?\<theta> p i (Suc i) \<and> ?\<theta> i = m \<and> ?\<theta> (Suc i) = n"
  11.533 +    unfolding is_fthread_def Ball_def
  11.534 +    by auto
  11.535 +
  11.536 +  thus "?L"
  11.537 +    unfolding has_fth_def 
  11.538 +    by auto
  11.539 +qed
  11.540 +
  11.541 +lemma desc_fth_single:
  11.542 +  "has_desc_fth p i (Suc i) m n = 
  11.543 +  dsc (snd (p i)) m n" (is "?L = ?R")
  11.544 +proof 
  11.545 +  assume "?L" thus "?R"
  11.546 +    unfolding is_desc_fthread_def has_desc_fth_def is_fthread_def
  11.547 +    Bex_def 
  11.548 +    by (elim exE conjE) (case_tac "k = i", auto)
  11.549 +next
  11.550 +  let ?\<theta> = "\<lambda>k. if k = i then m else n"
  11.551 +  assume edge: "?R"
  11.552 +  hence "is_desc_fthread ?\<theta> p i (Suc i) \<and> ?\<theta> i = m \<and> ?\<theta> (Suc i) = n"
  11.553 +    unfolding is_desc_fthread_def is_fthread_def Ball_def Bex_def
  11.554 +    by auto
  11.555 +  thus "?L"
  11.556 +    unfolding has_desc_fth_def 
  11.557 +    by auto
  11.558 +qed
  11.559 +
  11.560 +lemma mk_eql: "(G \<turnstile> m \<leadsto>\<^bsup>e\<^esup> n) \<Longrightarrow> eql G m n"
  11.561 +  by (cases e, auto)
  11.562 +
  11.563 +lemma eql_scgcomp:
  11.564 +  "eql (G * H) m r =
  11.565 +  (\<exists>n. eql G m n \<and> eql H n r)" (is "?L = ?R")
  11.566 +proof
  11.567 +  show "?L \<Longrightarrow> ?R"
  11.568 +    by (auto simp:in_grcomp intro!:mk_eql)
  11.569 +
  11.570 +  assume "?R"
  11.571 +  then obtain n where l: "eql G m n" and r:"eql H n r" by auto
  11.572 +  thus ?L
  11.573 +    by (cases "dsc G m n") (auto simp:in_grcomp mult_sedge_def)
  11.574 +qed
  11.575 +
  11.576 +lemma desc_scgcomp:
  11.577 +  "dsc (G * H) m r =
  11.578 +  (\<exists>n. (dsc G m n \<and> eql H n r) \<or> (eq G m n \<and> dsc H n r))" (is "?L = ?R")
  11.579 +proof
  11.580 +  show "?R \<Longrightarrow> ?L" by (auto simp:in_grcomp mult_sedge_def)
  11.581 +
  11.582 +  assume "?L"
  11.583 +  thus ?R
  11.584 +    by (auto simp:in_grcomp mult_sedge_def)
  11.585 +  (case_tac "e", auto, case_tac "e'", auto)
  11.586 +qed
  11.587 +
  11.588 +
  11.589 +lemma has_fth_unfold:
  11.590 +  assumes "i < j"
  11.591 +  shows "has_fth p i j m n = 
  11.592 +    (\<exists>r. has_fth p i (Suc i) m r \<and> has_fth p (Suc i) j r n)"
  11.593 +    by (rule combine_fthreads) (insert `i < j`, auto)
  11.594 +
  11.595 +lemma has_dfth_unfold:
  11.596 +  assumes range: "i < j"
  11.597 +  shows 
  11.598 +  "has_desc_fth p i j m r =
  11.599 +  (\<exists>n. (has_desc_fth p i (Suc i) m n \<and> has_fth p (Suc i) j n r)
  11.600 +  \<or> (has_fth p i (Suc i) m n \<and> has_desc_fth p (Suc i) j n r))"
  11.601 +  by (rule combine_dfthreads) (insert `i < j`, auto)
  11.602 +
  11.603 +
  11.604 +lemma Lemma7a:
  11.605 +assumes "i \<le> j"
  11.606 +shows
  11.607 +  "has_fth p i j m n = 
  11.608 +  eql (prod (p\<langle>i,j\<rangle>)) m n"
  11.609 +using prems
  11.610 +proof (induct i arbitrary: m rule:inc_induct)
  11.611 +  case 1 show ?case
  11.612 +    unfolding has_fth_def is_fthread_def sub_path_def
  11.613 +    by (auto simp:in_grunit one_sedge_def)
  11.614 +next
  11.615 +  case (2 i)
  11.616 +  note IH = `\<And>m. has_fth p (Suc i) j m n = 
  11.617 +  eql (prod (p\<langle>Suc i,j\<rangle>)) m n`
  11.618 +
  11.619 +  have "has_fth p i j m n 
  11.620 +    = (\<exists>r. has_fth p i (Suc i) m r \<and> has_fth p (Suc i) j r n)"
  11.621 +    by (rule has_fth_unfold[OF `i < j`])
  11.622 +  also have "\<dots> = (\<exists>r. has_fth p i (Suc i) m r 
  11.623 +    \<and> eql (prod (p\<langle>Suc i,j\<rangle>)) r n)"
  11.624 +    by (simp only:IH)
  11.625 +  also have "\<dots> = (\<exists>r. eql (snd (p i)) m r
  11.626 +    \<and> eql (prod (p\<langle>Suc i,j\<rangle>)) r n)"
  11.627 +    by (simp only:fth_single)
  11.628 +  also have "\<dots> = eql (snd (p i) * prod (p\<langle>Suc i,j\<rangle>)) m n"
  11.629 +    by (simp only:eql_scgcomp)
  11.630 +  also have "\<dots> = eql (prod (p\<langle>i,j\<rangle>)) m n"
  11.631 +    by (simp only:prod_unfold[OF `i < j`])
  11.632 +  finally show ?case .
  11.633 +qed
  11.634 +
  11.635 +
  11.636 +lemma Lemma7b:
  11.637 +assumes "i \<le> j"
  11.638 +shows
  11.639 +  "has_desc_fth p i j m n = 
  11.640 +  dsc (prod (p\<langle>i,j\<rangle>)) m n"
  11.641 +using prems
  11.642 +proof (induct i arbitrary: m rule:inc_induct)
  11.643 +  case 1 show ?case
  11.644 +    unfolding has_desc_fth_def is_desc_fthread_def sub_path_def 
  11.645 +    by (auto simp:in_grunit one_sedge_def)
  11.646 +next
  11.647 +  case (2 i)
  11.648 +  thus ?case 
  11.649 +    by (simp only:prod_unfold desc_scgcomp desc_fth_single
  11.650 +    has_dfth_unfold fth_single Lemma7a) auto
  11.651 +qed
  11.652 +
  11.653 +
  11.654 +lemma descat_contract:
  11.655 +  assumes [simp]: "increasing s"
  11.656 +  shows
  11.657 +  "descat (contract s p) \<theta> i = 
  11.658 +  has_desc_fth p (s i) (s (Suc i)) (\<theta> i) (\<theta> (Suc i))"
  11.659 +  by (simp add:Lemma7b increasing_weak contract_def)
  11.660 +
  11.661 +lemma eqlat_contract:
  11.662 +  assumes [simp]: "increasing s"
  11.663 +  shows
  11.664 +  "eqlat (contract s p) \<theta> i = 
  11.665 +  has_fth p (s i) (s (Suc i)) (\<theta> i) (\<theta> (Suc i))"
  11.666 +  by (auto simp:Lemma7a increasing_weak contract_def)
  11.667 +
  11.668 +
  11.669 +subsection {* Connecting threads *}
  11.670 +
  11.671 +definition
  11.672 +  "connect s \<theta>s = (\<lambda>k. \<theta>s (section_of s k) k)"
  11.673 +
  11.674 +
  11.675 +lemma next_in_range:
  11.676 +  assumes [simp]: "increasing s"
  11.677 +  assumes a: "k \<in> section s i"
  11.678 +  shows "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))"
  11.679 +proof -
  11.680 +  from a have "k < s (Suc i)" by simp
  11.681 +  
  11.682 +  hence "Suc k < s (Suc i) \<or> Suc k = s (Suc i)" by arith
  11.683 +  thus ?thesis
  11.684 +  proof
  11.685 +    assume "Suc k < s (Suc i)"
  11.686 +    with a have "Suc k \<in> section s i" by simp
  11.687 +    thus ?thesis ..
  11.688 +  next
  11.689 +    assume eq: "Suc k = s (Suc i)"
  11.690 +    with increasing_strict have "Suc k < s (Suc (Suc i))" by simp
  11.691 +    with eq have "Suc k \<in> section s (Suc i)" by simp
  11.692 +    thus ?thesis ..
  11.693 +  qed
  11.694 +qed
  11.695 +
  11.696 +
  11.697 +
  11.698 +lemma connect_threads:
  11.699 +  assumes [simp]: "increasing s"
  11.700 +  assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
  11.701 +  assumes fth: "is_fthread (\<theta>s i) p (s i) (s (Suc i))"
  11.702 +
  11.703 +  shows
  11.704 +  "is_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
  11.705 +  unfolding is_fthread_def
  11.706 +proof 
  11.707 +  fix k assume krng: "k \<in> section s i"
  11.708 +
  11.709 +  with fth have eqlat: "eqlat p (\<theta>s i) k" 
  11.710 +    unfolding is_fthread_def by simp
  11.711 +
  11.712 +  from krng and next_in_range 
  11.713 +  have "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))" 
  11.714 +    by simp
  11.715 +  thus "eqlat p (connect s \<theta>s) k"
  11.716 +  proof
  11.717 +    assume "Suc k \<in> section s i"
  11.718 +    with krng eqlat show ?thesis
  11.719 +      unfolding connect_def
  11.720 +      by (simp only:section_of_known `increasing s`)
  11.721 +  next
  11.722 +    assume skrng: "Suc k \<in> section s (Suc i)"
  11.723 +    with krng have "Suc k = s (Suc i)" by auto
  11.724 +
  11.725 +    with krng skrng eqlat show ?thesis
  11.726 +      unfolding connect_def
  11.727 +      by (simp only:section_of_known connected[symmetric] `increasing s`)
  11.728 +  qed
  11.729 +qed
  11.730 +
  11.731 +
  11.732 +lemma connect_dthreads:
  11.733 +  assumes inc[simp]: "increasing s"
  11.734 +  assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
  11.735 +  assumes fth: "is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
  11.736 +
  11.737 +  shows
  11.738 +  "is_desc_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
  11.739 +  unfolding is_desc_fthread_def
  11.740 +proof 
  11.741 +  show "is_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
  11.742 +    apply (rule connect_threads)
  11.743 +    apply (insert fth)
  11.744 +    by (auto simp:connected is_desc_fthread_def)
  11.745 +
  11.746 +  from fth
  11.747 +  obtain k where dsc: "descat p (\<theta>s i) k" and krng: "k \<in> section s i"
  11.748 +    unfolding is_desc_fthread_def by blast
  11.749 +  
  11.750 +  from krng and next_in_range 
  11.751 +  have "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))" 
  11.752 +    by simp
  11.753 +  hence "descat p (connect s \<theta>s) k"
  11.754 +  proof
  11.755 +    assume "Suc k \<in> section s i"
  11.756 +    with krng dsc show ?thesis unfolding connect_def
  11.757 +      by (simp only:section_of_known inc)
  11.758 +  next
  11.759 +    assume skrng: "Suc k \<in> section s (Suc i)"
  11.760 +    with krng have "Suc k = s (Suc i)" by auto
  11.761 +
  11.762 +    with krng skrng dsc show ?thesis unfolding connect_def
  11.763 +      by (simp only:section_of_known connected[symmetric] inc)
  11.764 +  qed
  11.765 +  with krng show "\<exists>k\<in>section s i. descat p (connect s \<theta>s) k" ..
  11.766 +qed
  11.767 +
  11.768 +
  11.769 +
  11.770 +lemma mk_inf_thread:
  11.771 +  assumes [simp]: "increasing s"
  11.772 +  assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))"
  11.773 +  shows "is_thread (s (Suc n)) \<theta> p"
  11.774 +  unfolding is_thread_def 
  11.775 +proof (intro allI impI)
  11.776 +  fix j assume st: "s (Suc n) \<le> j"
  11.777 +
  11.778 +  let ?k = "section_of s j"
  11.779 +  from in_section_of st
  11.780 +  have rs: "j \<in> section s ?k" by simp
  11.781 +
  11.782 +  with st have "s (Suc n) < s (Suc ?k)" by simp
  11.783 +  with increasing_bij have "n < ?k" by simp
  11.784 +  with rs and fths[of ?k]
  11.785 +  show "eqlat p \<theta> j" by (simp add:is_fthread_def)
  11.786 +qed
  11.787 +
  11.788 +
  11.789 +lemma mk_inf_desc_thread:
  11.790 +  assumes [simp]: "increasing s"
  11.791 +  assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))"
  11.792 +  assumes fdths: "\<exists>\<^sub>\<infinity>i. is_desc_fthread \<theta> p (s i) (s (Suc i))"
  11.793 +  shows "is_desc_thread \<theta> p"
  11.794 +  unfolding is_desc_thread_def 
  11.795 +proof (intro exI conjI)
  11.796 +
  11.797 +  from mk_inf_thread[of s n] is_thread_def fths
  11.798 +  show "\<forall>i\<ge>s (Suc n). eqlat p \<theta> i" by simp
  11.799 +
  11.800 +  show "\<exists>\<^sub>\<infinity>l. descat p \<theta> l"
  11.801 +    unfolding INF_nat
  11.802 +  proof
  11.803 +    fix i 
  11.804 +    
  11.805 +    let ?k = "section_of s i"
  11.806 +    from fdths obtain j
  11.807 +      where "?k < j" "is_desc_fthread \<theta> p (s j) (s (Suc j))"
  11.808 +      unfolding INF_nat by auto
  11.809 +    then obtain l where "s j \<le> l" and desc: "descat p \<theta> l"
  11.810 +      unfolding is_desc_fthread_def
  11.811 +      by auto
  11.812 +
  11.813 +    have "i < s (Suc ?k)" by (rule section_of2)
  11.814 +    also have "\<dots> \<le> s j" 
  11.815 +      by (rule increasing_weak[of s], assumption)
  11.816 +    (insert `?k < j`, arith)
  11.817 +    also note `\<dots> \<le> l`
  11.818 +    finally have "i < l" .
  11.819 +    with desc
  11.820 +    show "\<exists>l. i < l \<and> descat p \<theta> l" by blast
  11.821 +  qed
  11.822 +qed
  11.823 +
  11.824 +
  11.825 +lemma desc_ex_choice:
  11.826 +  assumes A: "((\<exists>n.\<forall>i\<ge>n. \<exists>x. P x i) \<and> (\<exists>\<^sub>\<infinity>i. \<exists>x. Q x i))"
  11.827 +  and imp: "\<And>x i. Q x i \<Longrightarrow> P x i"
  11.828 +  shows "\<exists>xs. ((\<exists>n.\<forall>i\<ge>n. P (xs i) i) \<and> (\<exists>\<^sub>\<infinity>i. Q (xs i) i))"
  11.829 +  (is "\<exists>xs. ?Ps xs \<and> ?Qs xs")
  11.830 +proof
  11.831 +  let ?w = "\<lambda>i. (if (\<exists>x. Q x i) then (SOME x. Q x i)
  11.832 +                                 else (SOME x. P x i))"
  11.833 +
  11.834 +  from A
  11.835 +  obtain n where P: "\<And>i. n \<le> i \<Longrightarrow> \<exists>x. P x i"
  11.836 +    by auto
  11.837 +  {
  11.838 +    fix i::'a assume "n \<le> i"
  11.839 +
  11.840 +    have "P (?w i) i"
  11.841 +    proof (cases "\<exists>x. Q x i")
  11.842 +      case True
  11.843 +      hence "Q (?w i) i" by (auto intro:someI)
  11.844 +      with imp show "P (?w i) i" .
  11.845 +    next
  11.846 +      case False
  11.847 +      with P[OF `n \<le> i`] show "P (?w i) i" 
  11.848 +        by (auto intro:someI)
  11.849 +    qed
  11.850 +  }
  11.851 +
  11.852 +  hence "?Ps ?w" by (rule_tac x=n in exI) auto
  11.853 +
  11.854 +  moreover
  11.855 +  from A have "\<exists>\<^sub>\<infinity>i. (\<exists>x. Q x i)" ..
  11.856 +  hence "?Qs ?w" by (rule INF_mono) (auto intro:someI)
  11.857 +  ultimately
  11.858 +  show "?Ps ?w \<and> ?Qs ?w" ..
  11.859 +qed
  11.860 +
  11.861 +
  11.862 +
  11.863 +lemma dthreads_join:
  11.864 +  assumes [simp]: "increasing s"
  11.865 +  assumes dthread: "is_desc_thread \<theta> (contract s p)"
  11.866 +  shows "\<exists>\<theta>s. desc (\<lambda>i. is_fthread (\<theta>s i) p (s i) (s (Suc i))
  11.867 +                           \<and> \<theta>s i (s i) = \<theta> i 
  11.868 +                           \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))
  11.869 +                   (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))
  11.870 +                           \<and> \<theta>s i (s i) = \<theta> i 
  11.871 +                           \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))"
  11.872 +    apply (rule desc_ex_choice)
  11.873 +    apply (insert dthread)
  11.874 +    apply (simp only:is_desc_thread_def)
  11.875 +    apply (simp add:eqlat_contract)
  11.876 +    apply (simp add:descat_contract)
  11.877 +    apply (simp only:has_fth_def has_desc_fth_def)
  11.878 +    by (auto simp:is_desc_fthread_def)
  11.879 +
  11.880 +
  11.881 +
  11.882 +lemma INF_drop_prefix:
  11.883 +  "(\<exists>\<^sub>\<infinity>i::nat. i > n \<and> P i) = (\<exists>\<^sub>\<infinity>i. P i)"
  11.884 +  apply (auto simp:INF_nat)
  11.885 +  apply (drule_tac x = "max m n" in spec)
  11.886 +  apply (elim exE conjE)
  11.887 +  apply (rule_tac x = "na" in exI)
  11.888 +  by auto
  11.889 +
  11.890 +
  11.891 +
  11.892 +lemma contract_keeps_threads:
  11.893 +  assumes inc[simp]: "increasing s"
  11.894 +  shows "(\<exists>\<theta>. is_desc_thread \<theta> p) 
  11.895 +  \<longleftrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> (contract s p))"
  11.896 +  (is "?A \<longleftrightarrow> ?B")
  11.897 +proof 
  11.898 +  assume "?A"
  11.899 +  then obtain \<theta> n 
  11.900 +    where fr: "\<forall>i\<ge>n. eqlat p \<theta> i" 
  11.901 +    and ds: "\<exists>\<^sub>\<infinity>i. descat p \<theta> i"
  11.902 +    unfolding is_desc_thread_def 
  11.903 +    by auto
  11.904 +
  11.905 +  let ?c\<theta> = "\<lambda>i. \<theta> (s i)"
  11.906 +
  11.907 +  have "is_desc_thread ?c\<theta> (contract s p)"
  11.908 +    unfolding is_desc_thread_def
  11.909 +  proof (intro exI conjI)
  11.910 +    
  11.911 +    show "\<forall>i\<ge>n. eqlat (contract s p) ?c\<theta> i"
  11.912 +    proof (intro allI impI)
  11.913 +      fix i assume "n \<le> i"
  11.914 +      also have "i \<le> s i" 
  11.915 +	    using increasing_inc by auto
  11.916 +      finally have "n \<le> s i" .
  11.917 +
  11.918 +      with fr have "is_fthread \<theta> p (s i) (s (Suc i))"
  11.919 +	    unfolding is_fthread_def by auto
  11.920 +      hence "has_fth p (s i) (s (Suc i)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
  11.921 +	    unfolding has_fth_def by auto
  11.922 +      with less_imp_le[OF increasing_strict]
  11.923 +      have "eql (prod (p\<langle>s i,s (Suc i)\<rangle>)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
  11.924 +	    by (simp add:Lemma7a)
  11.925 +      thus "eqlat (contract s p) ?c\<theta> i" unfolding contract_def
  11.926 +	    by auto
  11.927 +    qed
  11.928 +
  11.929 +    show "\<exists>\<^sub>\<infinity>i. descat (contract s p) ?c\<theta> i"
  11.930 +      unfolding INF_nat 
  11.931 +    proof 
  11.932 +      fix i
  11.933 +
  11.934 +      let ?K = "section_of s (max (s (Suc i)) n)"
  11.935 +      from `\<exists>\<^sub>\<infinity>i. descat p \<theta> i` obtain j
  11.936 +	    where "s (Suc ?K) < j" "descat p \<theta> j"
  11.937 +	    unfolding INF_nat by blast
  11.938 +      
  11.939 +      let ?L = "section_of s j"
  11.940 +      {
  11.941 +	    fix x assume r: "x \<in> section s ?L"
  11.942 +
  11.943 +	    have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2)
  11.944 +        note `s (Suc ?K) < j`
  11.945 +        also have "j < s (Suc ?L)"
  11.946 +          by (rule section_of2)
  11.947 +        finally have "Suc ?K \<le> ?L"
  11.948 +          by (simp add:increasing_bij)          
  11.949 +	    with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
  11.950 +	    with e1 r have "max (s (Suc i)) n < x" by simp
  11.951 +        
  11.952 +	    hence "(s (Suc i)) < x" "n < x" by auto
  11.953 +      }
  11.954 +      note range_est = this
  11.955 +      
  11.956 +      have "is_desc_fthread \<theta> p (s ?L) (s (Suc ?L))"
  11.957 +	    unfolding is_desc_fthread_def is_fthread_def
  11.958 +      proof
  11.959 +	    show "\<forall>m\<in>section s ?L. eqlat p \<theta> m"
  11.960 +        proof 
  11.961 +          fix m assume "m\<in>section s ?L"
  11.962 +          with range_est(2) have "n < m" . 
  11.963 +          with fr show "eqlat p \<theta> m" by simp
  11.964 +        qed
  11.965 +        
  11.966 +
  11.967 +        from in_section_of inc less_imp_le[OF `s (Suc ?K) < j`]
  11.968 +	    have "j \<in> section s ?L" .
  11.969 +
  11.970 +	    with `descat p \<theta> j`
  11.971 +	    show "\<exists>m\<in>section s ?L. descat p \<theta> m" ..
  11.972 +      qed
  11.973 +      
  11.974 +      with less_imp_le[OF increasing_strict]
  11.975 +      have a: "descat (contract s p) ?c\<theta> ?L"
  11.976 +	    unfolding contract_def Lemma7b[symmetric]
  11.977 +	    by (auto simp:Lemma7b[symmetric] has_desc_fth_def)
  11.978 +      
  11.979 +      have "i < ?L"
  11.980 +      proof (rule classical)
  11.981 +	    assume "\<not> i < ?L" 
  11.982 +	    hence "s ?L < s (Suc i)" 
  11.983 +          by (simp add:increasing_bij)
  11.984 +	    also have "\<dots> < s ?L"
  11.985 +	      by (rule range_est(1)) (simp add:increasing_strict)
  11.986 +	    finally show ?thesis .
  11.987 +      qed
  11.988 +      with a show "\<exists>l. i < l \<and> descat (contract s p) ?c\<theta> l"
  11.989 +        by blast
  11.990 +    qed
  11.991 +  qed
  11.992 +  with exI show "?B" .
  11.993 +next
  11.994 +  assume "?B"
  11.995 +  then obtain \<theta> 
  11.996 +    where dthread: "is_desc_thread \<theta> (contract s p)" ..
  11.997 +
  11.998 +  with dthreads_join inc 
  11.999 +  obtain \<theta>s where ths_spec:
 11.1000 +    "desc (\<lambda>i. is_fthread (\<theta>s i) p (s i) (s (Suc i))
 11.1001 +                  \<and> \<theta>s i (s i) = \<theta> i 
 11.1002 +                  \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))
 11.1003 +          (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))
 11.1004 +                  \<and> \<theta>s i (s i) = \<theta> i 
 11.1005 +                  \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))" 
 11.1006 +    (is "desc ?alw ?inf") 
 11.1007 +    by blast
 11.1008 +
 11.1009 +  then obtain n where fr: "\<forall>i\<ge>n. ?alw i" by blast
 11.1010 +  hence connected: "\<And>i. n < i \<Longrightarrow> \<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
 11.1011 +    by auto
 11.1012 +  
 11.1013 +  let ?j\<theta> = "connect s \<theta>s"
 11.1014 +  
 11.1015 +  from fr ths_spec have ths_spec2:
 11.1016 +    "\<And>i. i > n \<Longrightarrow> is_fthread (\<theta>s i) p (s i) (s (Suc i))"
 11.1017 +    "\<exists>\<^sub>\<infinity>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
 11.1018 +    by (auto intro:INF_mono)
 11.1019 +  
 11.1020 +  have p1: "\<And>i. i > n \<Longrightarrow> is_fthread ?j\<theta> p (s i) (s (Suc i))"
 11.1021 +    by (rule connect_threads) (auto simp:connected ths_spec2)
 11.1022 +  
 11.1023 +  from ths_spec2(2)
 11.1024 +  have "\<exists>\<^sub>\<infinity>i. n < i \<and> is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
 11.1025 +    unfolding INF_drop_prefix .
 11.1026 +  
 11.1027 +  hence p2: "\<exists>\<^sub>\<infinity>i. is_desc_fthread ?j\<theta> p (s i) (s (Suc i))"
 11.1028 +    apply (rule INF_mono)
 11.1029 +    apply (rule connect_dthreads)
 11.1030 +    by (auto simp:connected)
 11.1031 +  
 11.1032 +  with `increasing s` p1
 11.1033 +  have "is_desc_thread ?j\<theta> p" 
 11.1034 +    by (rule mk_inf_desc_thread)
 11.1035 +  with exI show "?A" .
 11.1036 +qed
 11.1037 +
 11.1038 +
 11.1039 +
 11.1040 +lemma repeated_edge:
 11.1041 +  assumes "\<And>i. i > n \<Longrightarrow> dsc (snd (p i)) k k"
 11.1042 +  shows "is_desc_thread (\<lambda>i. k) p"
 11.1043 +  using prems
 11.1044 +  unfolding is_desc_thread_def 
 11.1045 +  apply (auto)
 11.1046 +  apply (rule_tac x="Suc n" in exI, auto)
 11.1047 +  apply (rule INF_mono[where P="\<lambda>i. n < i"])
 11.1048 +  apply (simp only:INF_nat)
 11.1049 +  by auto arith
 11.1050 +
 11.1051 +
 11.1052 +lemma fin_from_inf:
 11.1053 +  assumes "is_thread n \<theta> p"
 11.1054 +  assumes "n < i"
 11.1055 +  assumes "i < j"
 11.1056 +  shows "is_fthread \<theta> p i j"
 11.1057 +  using prems
 11.1058 +  unfolding is_thread_def is_fthread_def 
 11.1059 +  by auto
 11.1060 +
 11.1061 +
 11.1062 +
 11.1063 +section {* Ramsey's Theorem *}
 11.1064 +
 11.1065 +
 11.1066 +definition 
 11.1067 +  "set2pair S = (THE (x,y). x < y \<and> S = {x,y})"
 11.1068 +
 11.1069 +lemma set2pair_conv: 
 11.1070 +  fixes x y :: nat
 11.1071 +  assumes "x < y"
 11.1072 +  shows "set2pair {x, y} = (x, y)"
 11.1073 +  unfolding set2pair_def
 11.1074 +proof (rule the_equality, simp_all only:split_conv split_paired_all)
 11.1075 +  from `x < y` show "x < y \<and> {x,y}={x,y}" by simp
 11.1076 +next
 11.1077 +  fix a b
 11.1078 +  assume a: "a < b \<and> {x, y} = {a, b}"
 11.1079 +  hence "{a, b} = {x, y}" by simp_all
 11.1080 +  hence "(a, b) = (x, y) \<or> (a, b) = (y, x)" 
 11.1081 +    by (cases "x = y") auto
 11.1082 +  thus "(a, b) = (x, y)"
 11.1083 +  proof 
 11.1084 +    assume "(a, b) = (y, x)"
 11.1085 +    with a and `x < y`
 11.1086 +    show ?thesis by auto (* contradiction *)
 11.1087 +  qed
 11.1088 +qed  
 11.1089 +
 11.1090 +definition 
 11.1091 +  "set2list = inv set"
 11.1092 +
 11.1093 +lemma finite_set2list: 
 11.1094 +  assumes [intro]: "finite S" 
 11.1095 +  shows "set (set2list S) = S"
 11.1096 +  unfolding set2list_def 
 11.1097 +proof (rule f_inv_f)
 11.1098 +  from finite_list
 11.1099 +  have "\<exists>l. set l = S" .
 11.1100 +  thus "S \<in> range set"
 11.1101 +    unfolding image_def
 11.1102 +    by auto
 11.1103 +qed
 11.1104 +
 11.1105 +
 11.1106 +corollary RamseyNatpairs:
 11.1107 +  fixes S :: "'a set"
 11.1108 +    and f :: "nat \<times> nat \<Rightarrow> 'a"
 11.1109 +
 11.1110 +  assumes "finite S"
 11.1111 +  and inS: "\<And>x y. x < y \<Longrightarrow> f (x, y) \<in> S"
 11.1112 +
 11.1113 +  obtains T :: "nat set" and s :: "'a"
 11.1114 +  where "infinite T"
 11.1115 +    and "s \<in> S"
 11.1116 +    and "\<And>x y. \<lbrakk>x \<in> T; y \<in> T; x < y\<rbrakk> \<Longrightarrow> f (x, y) = s"
 11.1117 +proof -
 11.1118 +  from `finite S`
 11.1119 +  have "set (set2list S) = S" by (rule finite_set2list)
 11.1120 +  then 
 11.1121 +  obtain l where S: "S = set l" by auto
 11.1122 +  also from set_conv_nth have "\<dots> = {l ! i |i. i < length l}" .
 11.1123 +  finally have "S = {l ! i |i. i < length l}" .
 11.1124 +
 11.1125 +  let ?s = "length l"
 11.1126 +
 11.1127 +  from inS 
 11.1128 +  have index_less: "\<And>x y. x \<noteq> y \<Longrightarrow> index_of l (f (set2pair {x, y})) < ?s"
 11.1129 +  proof -
 11.1130 +    fix x y :: nat
 11.1131 +    assume neq: "x \<noteq> y"
 11.1132 +    have "f (set2pair {x, y}) \<in> S"
 11.1133 +    proof (cases "x < y")
 11.1134 +      case True hence "set2pair {x, y} = (x, y)"
 11.1135 +	by (rule set2pair_conv)
 11.1136 +      with True inS
 11.1137 +      show ?thesis by simp
 11.1138 +    next
 11.1139 +      case False 
 11.1140 +      with neq have y_less: "y < x" by simp
 11.1141 +      have x:"{x,y} = {y,x}" by auto
 11.1142 +      with y_less have "set2pair {x, y} = (y, x)"
 11.1143 +	by (simp add:set2pair_conv)
 11.1144 +      with y_less inS
 11.1145 +      show ?thesis by simp
 11.1146 +    qed
 11.1147 +
 11.1148 +    thus "index_of l (f (set2pair {x, y})) < length l"
 11.1149 +      by (simp add: S index_of_length)
 11.1150 +  qed
 11.1151 +
 11.1152 +  have "\<exists>Y. infinite Y \<and>
 11.1153 +    (\<exists>t. t < ?s \<and>
 11.1154 +         (\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow>
 11.1155 +                      index_of l (f (set2pair {x, y})) = t))"
 11.1156 +    by (rule Ramsey2[of "UNIV::nat set", simplified])
 11.1157 +       (auto simp:index_less)
 11.1158 +  then obtain T i
 11.1159 +    where inf: "infinite T"
 11.1160 +    and "i < length l"
 11.1161 +    and d: "\<And>x y. \<lbrakk>x \<in> T; y\<in>T; x \<noteq> y\<rbrakk>
 11.1162 +    \<Longrightarrow> index_of l (f (set2pair {x, y})) = i"
 11.1163 +    by auto
 11.1164 +
 11.1165 +  have  "l ! i \<in> S" unfolding S
 11.1166 +    by (rule nth_mem)
 11.1167 +  moreover
 11.1168 +  have "\<And>x y. x \<in> T \<Longrightarrow> y\<in>T \<Longrightarrow> x < y
 11.1169 +    \<Longrightarrow> f (x, y) = l ! i"
 11.1170 +  proof -
 11.1171 +    fix x y assume "x \<in> T" "y \<in> T" "x < y"
 11.1172 +    with d have 
 11.1173 +      "index_of l (f (set2pair {x, y})) = i" by auto
 11.1174 +    with `x < y`
 11.1175 +    have "i = index_of l (f (x, y))" 
 11.1176 +      by (simp add:set2pair_conv)
 11.1177 +    with `i < length l`
 11.1178 +    show "f (x, y) = l ! i" 
 11.1179 +      by (auto intro:index_of_member[symmetric] iff:index_of_length)
 11.1180 +  qed
 11.1181 +  moreover note inf
 11.1182 +  ultimately
 11.1183 +  show ?thesis using prems
 11.1184 +    by blast
 11.1185 +qed
 11.1186 +
 11.1187 +
 11.1188 +section {* Main Result *}
 11.1189 +
 11.1190 +
 11.1191 +theorem LJA_Theorem4: 
 11.1192 +  assumes "bounded_acg P \<A>"
 11.1193 +  shows "SCT \<A> \<longleftrightarrow> SCT' \<A>"
 11.1194 +proof
 11.1195 +  assume "SCT \<A>"
 11.1196 +  
 11.1197 +  show "SCT' \<A>"
 11.1198 +  proof (rule classical)
 11.1199 +    assume "\<not> SCT' \<A>"
 11.1200 +    
 11.1201 +    then obtain n G
 11.1202 +      where in_closure: "(tcl \<A>) \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
 11.1203 +      and idemp: "G * G = G"
 11.1204 +      and no_strict_arc: "\<forall>p. \<not>(G \<turnstile> p \<leadsto>\<^bsup>\<down>\<^esup> p)"
 11.1205 +      unfolding SCT'_def no_bad_graphs_def by auto
 11.1206 +    
 11.1207 +    from in_closure obtain k
 11.1208 +      where k_pow: "\<A> ^ k \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
 11.1209 +      and "0 < k"
 11.1210 +      unfolding in_tcl by auto
 11.1211 +	
 11.1212 +    from power_induces_path k_pow
 11.1213 +    obtain loop where loop_props:
 11.1214 +      "has_fpath \<A> loop"
 11.1215 +      "n = fst loop" "n = end_node loop"
 11.1216 +      "G = prod loop" "k = length (snd loop)" . 
 11.1217 +
 11.1218 +    with `0 < k` and path_loop_graph
 11.1219 +    have "has_ipath \<A> (omega loop)" by blast
 11.1220 +    with `SCT \<A>` 
 11.1221 +    have thread: "\<exists>\<theta>. is_desc_thread \<theta> (omega loop)" by (auto simp:SCT_def)
 11.1222 +
 11.1223 +    let ?s = "\<lambda>i. k * i"
 11.1224 +    let ?cp = "\<lambda>i. (n, G)"
 11.1225 +
 11.1226 +    from loop_props have "fst loop = end_node loop" by auto
 11.1227 +    with `0 < k` `k = length (snd loop)`
 11.1228 +    have "\<And>i. (omega loop)\<langle>?s i,?s (Suc i)\<rangle> = loop"
 11.1229 +      by (rule sub_path_loop)
 11.1230 +
 11.1231 +    with `n = fst loop` `G = prod loop` `k = length (snd loop)`
 11.1232 +    have a: "contract ?s (omega loop) = ?cp"
 11.1233 +      unfolding contract_def
 11.1234 +      by (simp add:path_loop_def split_def fst_p0)
 11.1235 +
 11.1236 +    from `0 < k` have "increasing ?s"
 11.1237 +      by (auto simp:increasing_def)
 11.1238 +    with thread have "\<exists>\<theta>. is_desc_thread \<theta> ?cp"
 11.1239 +      unfolding a[symmetric] 
 11.1240 +      by (unfold contract_keeps_threads[symmetric])
 11.1241 +
 11.1242 +    then obtain \<theta> where desc: "is_desc_thread \<theta> ?cp" by auto
 11.1243 +
 11.1244 +    then obtain n where thr: "is_thread n \<theta> ?cp" 
 11.1245 +      unfolding is_desc_thread_def is_thread_def 
 11.1246 +      by auto
 11.1247 +
 11.1248 +    have "bounded_th P n \<theta>" 
 11.1249 +    proof -
 11.1250 +      from `bounded_acg P \<A>`
 11.1251 +      have "bounded_acg P (tcl \<A>)" by (rule bounded_plus)
 11.1252 +      with in_closure have "bounded_scg P G"
 11.1253 +        unfolding bounded_acg_def by simp
 11.1254 +      hence "bounded_mp P ?cp"
 11.1255 +        unfolding bounded_mp_def by simp
 11.1256 +      with thr bounded_th 
 11.1257 +      show ?thesis by auto
 11.1258 +    qed
 11.1259 +    with bounded_th_infinite_visit
 11.1260 +    obtain p where inf_visit: "\<exists>\<^sub>\<infinity>i. \<theta> i = p" by blast
 11.1261 +
 11.1262 +    then obtain i where "n < i" "\<theta> i = p" 
 11.1263 +      by (auto simp:INF_nat)
 11.1264 +
 11.1265 +    from desc
 11.1266 +    have "\<exists>\<^sub>\<infinity>i. descat ?cp \<theta> i"
 11.1267 +      unfolding is_desc_thread_def by auto
 11.1268 +    then obtain j 
 11.1269 +      where "i < j" and "descat ?cp \<theta> j"
 11.1270 +      unfolding INF_nat by auto
 11.1271 +    from inf_visit obtain k where "j < k" "\<theta> k = p"
 11.1272 +      by (auto simp:INF_nat)
 11.1273 +
 11.1274 +    from `i < j` `j < k` `n < i` thr fin_from_inf `descat ?cp \<theta> j`
 11.1275 +    have "is_desc_fthread \<theta> ?cp i k"
 11.1276 +      unfolding is_desc_fthread_def
 11.1277 +      by auto
 11.1278 +
 11.1279 +    with `\<theta> k = p` `\<theta> i = p`
 11.1280 +    have dfth: "has_desc_fth ?cp i k p p"
 11.1281 +      unfolding has_desc_fth_def
 11.1282 +      by auto
 11.1283 +
 11.1284 +    from `i < j` `j < k` have "i < k" by auto
 11.1285 +    hence "prod (?cp\<langle>i, k\<rangle>) = G"
 11.1286 +    proof (induct i rule:strict_inc_induct)
 11.1287 +      case 1 thus ?case by (simp add:sub_path_def)
 11.1288 +    next
 11.1289 +      case (2 i) thus ?case
 11.1290 +	by (simp add:sub_path_def upt_rec[of i k] idemp)
 11.1291 +    qed
 11.1292 +
 11.1293 +    with `i < j` `j < k` dfth Lemma7b
 11.1294 +    have "dsc G p p" by auto
 11.1295 +    with no_strict_arc have False by auto
 11.1296 +    thus ?thesis ..
 11.1297 +  qed
 11.1298 +next
 11.1299 +  assume "SCT' \<A>"
 11.1300 +
 11.1301 +  show "SCT \<A>"
 11.1302 +  proof (rule classical)
 11.1303 +    assume "\<not> SCT \<A>"
 11.1304 +
 11.1305 +    with SCT_def
 11.1306 +    obtain p 
 11.1307 +      where ipath: "has_ipath \<A> p"
 11.1308 +      and no_desc_th: "\<not> (\<exists>\<theta>. is_desc_thread \<theta> p)"
 11.1309 +      by auto
 11.1310 +
 11.1311 +    from `bounded_acg P \<A>`
 11.1312 +    have "finite (dest_graph (tcl \<A>))" (is "finite ?AG")
 11.1313 +      by (intro bounded_finite bounded_plus)
 11.1314 +
 11.1315 +    from pdesc_acgplus[OF ipath]
 11.1316 +    have a: "\<And>x y. x<y \<Longrightarrow> pdesc p\<langle>x,y\<rangle> \<in> dest_graph (tcl \<A>)"
 11.1317 +      unfolding has_edge_def .
 11.1318 +      
 11.1319 +    obtain S G
 11.1320 +      where "infinite S" "G \<in> dest_graph (tcl \<A>)" 
 11.1321 +      and all_G: "\<And>x y. \<lbrakk> x \<in> S; y \<in> S; x < y\<rbrakk> \<Longrightarrow> 
 11.1322 +      pdesc (p\<langle>x,y\<rangle>) = G"
 11.1323 +      apply (rule RamseyNatpairs[of ?AG "\<lambda>(x,y). pdesc p\<langle>x, y\<rangle>"])
 11.1324 +      apply (rule `finite (dest_graph (tcl \<A>))`)
 11.1325 +      by (simp only:split_conv, rule a, auto)
 11.1326 +
 11.1327 +    obtain n H m where
 11.1328 +      G_struct: "G = (n, H, m)" by (cases G) simp
 11.1329 +
 11.1330 +    let ?s = "enumerate S"
 11.1331 +    let ?q = "contract ?s p"
 11.1332 +
 11.1333 +    note all_in_S[simp] = enumerate_in_set[OF `infinite S`]
 11.1334 +	from `infinite S` 
 11.1335 +    have inc[simp]: "increasing ?s" 
 11.1336 +      unfolding increasing_def by (simp add:enumerate_mono)
 11.1337 +    note increasing_bij[OF this, simp]
 11.1338 +      
 11.1339 +    from ipath_contract inc ipath
 11.1340 +    have "has_ipath (tcl \<A>) ?q" .
 11.1341 +
 11.1342 +    from all_G G_struct 
 11.1343 +    have all_H: "\<And>i. (snd (?q i)) = H"
 11.1344 +	  unfolding contract_def 
 11.1345 +      by simp
 11.1346 +    
 11.1347 +    have loop: "(tcl \<A>) \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
 11.1348 +      and idemp: "H * H = H"
 11.1349 +    proof - 
 11.1350 +      let ?i = "?s 0" and ?j = "?s (Suc 0)" and ?k = "?s (Suc (Suc 0))"
 11.1351 +      
 11.1352 +      have "pdesc (p\<langle>?i,?j\<rangle>) = G"
 11.1353 +		and "pdesc (p\<langle>?j,?k\<rangle>) = G"
 11.1354 +		and "pdesc (p\<langle>?i,?k\<rangle>) = G"
 11.1355 +		using all_G 
 11.1356 +		by auto
 11.1357 +	  
 11.1358 +      with G_struct 
 11.1359 +      have "m = end_node (p\<langle>?i,?j\<rangle>)"
 11.1360 +				"n = fst (p\<langle>?j,?k\<rangle>)"
 11.1361 +				and Hs:	"prod (p\<langle>?i,?j\<rangle>) = H"
 11.1362 +				"prod (p\<langle>?j,?k\<rangle>) = H"
 11.1363 +				"prod (p\<langle>?i,?k\<rangle>) = H"
 11.1364 +		by auto
 11.1365 +			
 11.1366 +      hence "m = n" by simp
 11.1367 +      thus "tcl \<A> \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
 11.1368 +		using G_struct `G \<in> dest_graph (tcl \<A>)`
 11.1369 +		by (simp add:has_edge_def)
 11.1370 +	  
 11.1371 +      from sub_path_prod[of ?i ?j ?k p]      
 11.1372 +      show "H * H = H"
 11.1373 +		unfolding Hs by simp
 11.1374 +    qed
 11.1375 +    moreover have "\<And>k. \<not>dsc H k k"
 11.1376 +    proof
 11.1377 +      fix k :: nat assume "dsc H k k"
 11.1378 +      
 11.1379 +      with all_H repeated_edge
 11.1380 +      have "\<exists>\<theta>. is_desc_thread \<theta> ?q" by fast
 11.1381 +	  with inc have "\<exists>\<theta>. is_desc_thread \<theta> p"
 11.1382 +		by (subst contract_keeps_threads) 
 11.1383 +      with no_desc_th
 11.1384 +      show False ..
 11.1385 +    qed
 11.1386 +    ultimately 
 11.1387 +    have False
 11.1388 +      using `SCT' \<A>`[unfolded SCT'_def no_bad_graphs_def]
 11.1389 +      by blast
 11.1390 +    thus ?thesis ..
 11.1391 +  qed
 11.1392 +qed
 11.1393 +
 11.1394 +
 11.1395 +
 11.1396 +lemma LJA_apply:
 11.1397 +  assumes fin: "finite_acg A"
 11.1398 +  assumes "SCT' A"
 11.1399 +  shows "SCT A"
 11.1400 +proof -
 11.1401 +  from fin obtain P where b: "bounded_acg P A"
 11.1402 +    unfolding finite_acg_def ..
 11.1403 +  show ?thesis using LJA_Theorem4[OF b]
 11.1404 +    by simp
 11.1405 +qed
 11.1406 +
 11.1407 +
 11.1408 +
 11.1409 +
 11.1410 +
 11.1411 +
 11.1412 +end
 11.1413 +
 11.1414 +
 11.1415 +
 11.1416 +
 11.1417 +
 11.1418 +
 11.1419 +
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Library/Size_Change_Termination.thy	Mon Feb 26 21:34:16 2007 +0100
    12.3 @@ -0,0 +1,104 @@
    12.4 +theory Size_Change_Termination
    12.5 +imports SCT_Theorem SCT_Interpretation SCT_Implementation 
    12.6 +uses "size_change_termination.ML"
    12.7 +begin
    12.8 +
    12.9 +use "size_change_termination.ML"
   12.10 +
   12.11 +
   12.12 +
   12.13 +section {* Simplifier setup *}
   12.14 +
   12.15 +text {* This is needed to run the SCT algorithm in the simplifier: *}
   12.16 +
   12.17 +lemma setbcomp_simps:
   12.18 +  "{x\<in>{}. P x} = {}"
   12.19 +  "{x\<in>insert y ys. P x} = (if P y then insert y {x\<in>ys. P x} else {x\<in>ys. P x})"
   12.20 +  by auto
   12.21 +
   12.22 +lemma setbcomp_cong:
   12.23 +  "A = B \<Longrightarrow> (\<And>x. P x = Q x) \<Longrightarrow> {x\<in>A. P x} = {x\<in>B. Q x}"
   12.24 +  by auto
   12.25 +
   12.26 +lemma cartprod_simps:
   12.27 +  "{} \<times> A = {}"
   12.28 +  "insert a A \<times> B = Pair a ` B \<union> (A \<times> B)"
   12.29 +  by (auto simp:image_def)
   12.30 +
   12.31 +lemma image_simps:
   12.32 +  "fu ` {} = {}"
   12.33 +  "fu ` insert a A = insert (fu a) (fu ` A)"
   12.34 +  by (auto simp:image_def)
   12.35 +
   12.36 +lemmas union_simps = 
   12.37 +  Un_empty_left Un_empty_right Un_insert_left
   12.38 +  
   12.39 +lemma subset_simps:
   12.40 +  "{} \<subseteq> B"
   12.41 +  "insert a A \<subseteq> B \<equiv> a \<in> B \<and> A \<subseteq> B"
   12.42 +  by auto 
   12.43 +
   12.44 +lemma element_simps:
   12.45 +  "x \<in> {} \<equiv> False"
   12.46 +  "x \<in> insert a A \<equiv> x = a \<or> x \<in> A"
   12.47 +  by auto
   12.48 +
   12.49 +lemma set_eq_simp:
   12.50 +  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" by auto
   12.51 +
   12.52 +lemma ball_simps:
   12.53 +  "\<forall>x\<in>{}. P x \<equiv> True"
   12.54 +  "(\<forall>x\<in>insert a A. P x) \<equiv> P a \<and> (\<forall>x\<in>A. P x)"
   12.55 +by auto
   12.56 +
   12.57 +lemma bex_simps:
   12.58 +  "\<exists>x\<in>{}. P x \<equiv> False"
   12.59 +  "(\<exists>x\<in>insert a A. P x) \<equiv> P a \<or> (\<exists>x\<in>A. P x)"
   12.60 +by auto
   12.61 +
   12.62 +lemmas set_simps =
   12.63 +  setbcomp_simps
   12.64 +  cartprod_simps image_simps union_simps subset_simps
   12.65 +  element_simps set_eq_simp
   12.66 +  ball_simps bex_simps
   12.67 +
   12.68 +lemma sedge_simps:
   12.69 +  "\<down> * x = \<down>"
   12.70 +  "\<Down> * x = x"
   12.71 +  by (auto simp:mult_sedge_def)
   12.72 +
   12.73 +lemmas sctTest_simps =
   12.74 +  simp_thms
   12.75 +  if_True
   12.76 +  if_False
   12.77 +  nat.inject
   12.78 +  nat.distinct
   12.79 +  Pair_eq 
   12.80 +
   12.81 +  grcomp_code 
   12.82 +  edges_match.simps 
   12.83 +  connect_edges.simps 
   12.84 +
   12.85 +  sedge_simps
   12.86 +  sedge.distinct
   12.87 +  set_simps
   12.88 +
   12.89 +  graph_mult_def 
   12.90 +  graph_leq_def
   12.91 +  dest_graph.simps
   12.92 +  graph_plus_def
   12.93 +  graph.inject
   12.94 +  graph_zero_def
   12.95 +
   12.96 +  test_SCT_def
   12.97 +  mk_tcl_code
   12.98 +
   12.99 +  Let_def
  12.100 +  split_conv
  12.101 +
  12.102 +lemmas sctTest_congs = 
  12.103 +  if_weak_cong let_weak_cong setbcomp_cong
  12.104 +
  12.105 +
  12.106 +
  12.107 +end
  12.108 \ No newline at end of file
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Library/size_change_termination.ML	Mon Feb 26 21:34:16 2007 +0100
    13.3 @@ -0,0 +1,881 @@
    13.4 +
    13.5 +structure SCT = struct
    13.6 +
    13.7 +fun matrix [] ys = []
    13.8 +  | matrix (x::xs) ys = map (pair x) ys :: matrix xs ys
    13.9 +
   13.10 +fun map_matrix f xss = map (map f) xss
   13.11 +
   13.12 +val scgT = Sign.read_typ (the_context (), K NONE) "scg"
   13.13 +val acgT = Sign.read_typ (the_context (), K NONE) "acg"
   13.14 +
   13.15 +fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT))
   13.16 +fun graphT nT eT = Type ("Graphs.graph", [nT, eT])
   13.17 +
   13.18 +fun graph_const nT eT = Const ("Graphs.graph.Graph", HOLogic.mk_setT (edgeT nT eT) --> graphT nT eT)
   13.19 +
   13.20 +
   13.21 +val no_step_const = "SCT_Interpretation.no_step"
   13.22 +val no_step_def = thm "SCT_Interpretation.no_step_def"
   13.23 +val no_stepI = thm "SCT_Interpretation.no_stepI"
   13.24 +
   13.25 +fun mk_no_step RD1 RD2 = 
   13.26 +    let val RDT = fastype_of RD1
   13.27 +    in Const (no_step_const, RDT --> RDT --> HOLogic.boolT) $ RD1 $ RD2 end
   13.28 +
   13.29 +val decr_const = "SCT_Interpretation.decr"
   13.30 +val decr_def = thm "SCT_Interpretation.decr_def"
   13.31 +
   13.32 +fun mk_decr RD1 RD2 M1 M2 = 
   13.33 +    let val RDT = fastype_of RD1
   13.34 +      val MT = fastype_of M1
   13.35 +    in Const (decr_const, RDT --> RDT --> MT --> MT --> HOLogic.boolT) $ RD1 $ RD2 $ M1 $ M2 end
   13.36 +
   13.37 +val decreq_const = "SCT_Interpretation.decreq"
   13.38 +val decreq_def = thm "SCT_Interpretation.decreq_def"
   13.39 +
   13.40 +fun mk_decreq RD1 RD2 M1 M2 = 
   13.41 +    let val RDT = fastype_of RD1
   13.42 +      val MT = fastype_of M1
   13.43 +    in Const (decreq_const, RDT --> RDT --> MT --> MT --> HOLogic.boolT) $ RD1 $ RD2 $ M1 $ M2 end
   13.44 +
   13.45 +val stepP_const = "SCT_Interpretation.stepP"
   13.46 +val stepP_def = thm "SCT_Interpretation.stepP.simps"
   13.47 +
   13.48 +fun mk_stepP RD1 RD2 M1 M2 Rel = 
   13.49 +    let val RDT = fastype_of RD1
   13.50 +      val MT = fastype_of M1
   13.51 +    in 
   13.52 +      Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT) 
   13.53 +            $ RD1 $ RD2 $ M1 $ M2 $ Rel 
   13.54 +    end
   13.55 +
   13.56 +val approx_const = "SCT_Interpretation.approx"
   13.57 +val approx_empty = thm "SCT_Interpretation.approx_empty"
   13.58 +val approx_less = thm "SCT_Interpretation.approx_less"
   13.59 +val approx_leq = thm "SCT_Interpretation.approx_leq"
   13.60 +
   13.61 +fun mk_approx G RD1 RD2 Ms1 Ms2 = 
   13.62 +    let val RDT = fastype_of RD1
   13.63 +      val MsT = fastype_of Ms1
   13.64 +    in Const (approx_const, scgT --> RDT --> RDT --> MsT --> MsT --> HOLogic.boolT) $ G $ RD1 $ RD2 $ Ms1 $ Ms2 end
   13.65 +
   13.66 +val sound_int_const = "SCT_Interpretation.sound_int"
   13.67 +val sound_int_def = thm "SCT_Interpretation.sound_int_def"
   13.68 +fun mk_sound_int A RDs M =
   13.69 +    let val RDsT = fastype_of RDs
   13.70 +      val MT = fastype_of M
   13.71 +    in Const (sound_int_const, acgT --> RDsT --> MT --> HOLogic.boolT) $ A $ RDs $ M end
   13.72 +
   13.73 +
   13.74 +val nth_const = "List.nth"
   13.75 +fun mk_nth xs =
   13.76 +    let val lT as Type (_, [T]) = fastype_of xs
   13.77 +    in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end
   13.78 +
   13.79 +
   13.80 +val less_nat_const = Const ("Orderings.less", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
   13.81 +val lesseq_nat_const = Const ("Orderings.less_eq", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
   13.82 +
   13.83 +
   13.84 +(*
   13.85 +val has_edge_const = "Graphs.has_edge"
   13.86 +fun mk_has_edge G n e n' =
   13.87 +    let val nT = fastype_of n and eT = fastype_of e
   13.88 +    in Const (has_edge_const, graphT nT eT --> nT --> eT --> nT --> HOLogic.boolT) $ n $ e $ n' end
   13.89 +*)
   13.90 +
   13.91 +
   13.92 +val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
   13.93 +
   13.94 +val all_less_zero = thm "SCT_Interpretation.all_less_zero"
   13.95 +val all_less_Suc = thm "SCT_Interpretation.all_less_Suc"
   13.96 +
   13.97 +
   13.98 +
   13.99 +(* Lists as finite multisets *)
  13.100 +
  13.101 +(* --> Library *)
  13.102 +fun del_index n [] = []
  13.103 +  | del_index n (x :: xs) =
  13.104 +    if n>0 then x :: del_index (n - 1) xs else xs 
  13.105 +
  13.106 +
  13.107 +fun remove1 eq x [] = []
  13.108 +  | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys
  13.109 +
  13.110 +
  13.111 +fun multi_union eq [] ys = ys
  13.112 +  | multi_union eq (x::xs) ys = x :: multi_union eq xs (remove1 eq x ys)
  13.113 +
  13.114 +
  13.115 +fun dest_ex (Const ("Ex", _) $ Abs (a as (_,T,_))) =
  13.116 +    let
  13.117 +      val (n, body) = Term.dest_abs a
  13.118 +    in
  13.119 +      (Free (n, T), body)
  13.120 +    end
  13.121 +  | dest_ex _ = raise Match
  13.122 +                         
  13.123 +fun dest_all_ex (t as (Const ("Ex",_) $ _)) = 
  13.124 +    let
  13.125 +      val (v,b) = dest_ex t
  13.126 +      val (vs, b') = dest_all_ex b
  13.127 +    in
  13.128 +      (v :: vs, b')
  13.129 +    end
  13.130 +  | dest_all_ex t = ([],t)
  13.131 +
  13.132 +
  13.133 +fun dist_vars [] vs = (assert (null vs) "dist_vars"; [])
  13.134 +  | dist_vars (T::Ts) vs = 
  13.135 +    case find_index (fn v => fastype_of v = T) vs of
  13.136 +      ~1 => Free ("", T) :: dist_vars Ts vs
  13.137 +    |  i => (nth vs i) :: dist_vars Ts (del_index i vs)
  13.138 +
  13.139 +
  13.140 +fun dest_case rebind t =
  13.141 +    let
  13.142 +      val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t
  13.143 +      val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs
  13.144 +    in 
  13.145 +      foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match]
  13.146 +    end
  13.147 +
  13.148 +fun bind_many [] = I
  13.149 +  | bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
  13.150 +
  13.151 +(* Builds relation descriptions from a relation definition *)
  13.152 +fun mk_reldescs (Abs a) = 
  13.153 +    let
  13.154 +      val (_, Abs a') = Term.dest_abs a
  13.155 +      val (_, b) = Term.dest_abs a'
  13.156 +      val cases = HOLogic.dest_disj b
  13.157 +      val (vss, bs) = split_list (map dest_all_ex cases)
  13.158 +      val unionTs = fold (multi_union (op =)) (map (map fastype_of) vss) []
  13.159 +      val rebind = map (bind_many o dist_vars unionTs) vss
  13.160 +                 
  13.161 +      val RDs = map2 dest_case rebind bs
  13.162 +    in
  13.163 +      HOLogic.mk_list (fastype_of (hd RDs)) RDs
  13.164 +    end
  13.165 +
  13.166 +fun abs_rel_tac (st : thm) =
  13.167 +    let
  13.168 +      val thy = theory_of_thm st
  13.169 +      val (def, rd) = HOLogic.dest_eq (HOLogic.dest_Trueprop (hd (prems_of st)))
  13.170 +      val RDs = cterm_of thy (mk_reldescs def)
  13.171 +      val rdvar = Var (the_single (Term.add_vars rd [])) |> cterm_of thy
  13.172 +    in
  13.173 +      Seq.single (cterm_instantiate [(rdvar, RDs)] st)
  13.174 +    end
  13.175 +
  13.176 +
  13.177 +(* very primitive *)
  13.178 +fun measures_of RD =
  13.179 +    let
  13.180 +      val domT = range_type (fastype_of (fst (HOLogic.dest_prod (snd (HOLogic.dest_prod RD)))))
  13.181 +      val measures = LexicographicOrder.mk_base_funs domT
  13.182 +    in
  13.183 +      measures
  13.184 +    end
  13.185 +
  13.186 +
  13.187 +
  13.188 +val mk_number = HOLogic.mk_nat
  13.189 +val dest_number = HOLogic.dest_nat
  13.190 +
  13.191 +fun nums_to i = map mk_number (0 upto (i - 1))
  13.192 +
  13.193 +
  13.194 +fun unfold_then_auto thm = 
  13.195 +    (SIMPSET (unfold_tac [thm]))
  13.196 +      THEN (CLASIMPSET auto_tac)
  13.197 +
  13.198 +val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"]
  13.199 +val nth_ss = (HOL_basic_ss addsimps nth_simps)
  13.200 +val simp_nth_tac = simp_tac nth_ss
  13.201 +
  13.202 +
  13.203 +
  13.204 +fun tabulate_tlist thy l =
  13.205 +    let
  13.206 +      val n = length (HOLogic.dest_list l)
  13.207 +      val table = Inttab.make (map (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) (0 upto n - 1))
  13.208 +    in
  13.209 +      the o Inttab.lookup table
  13.210 +    end
  13.211 +
  13.212 +val get_elem = snd o Logic.dest_equals o prop_of
  13.213 +
  13.214 +
  13.215 +(* Attempt a proof of a given goal *)
  13.216 +
  13.217 +datatype proof_result = 
  13.218 +    Success of thm
  13.219 +  | Stuck of thm
  13.220 +  | Fail
  13.221 +  | False
  13.222 +  | Timeout (* not implemented *)
  13.223 +
  13.224 +fun try_to_prove tactic cgoal =
  13.225 +    case SINGLE tactic (Goal.init cgoal) of
  13.226 +      NONE => Fail
  13.227 +    | SOME st => if Thm.no_prems st 
  13.228 +                 then Success (Goal.finish st)
  13.229 +                 else if prems_of st = [HOLogic.Trueprop $ HOLogic.false_const] then False 
  13.230 +                 else Stuck st
  13.231 +
  13.232 +fun simple_result (Success thm) = SOME thm
  13.233 +  | simple_result _ = NONE
  13.234 +
  13.235 +
  13.236 +fun inst_nums thy i j (t:thm) = 
  13.237 +  instantiate' [] [NONE, NONE, NONE, SOME (cterm_of thy (mk_number i)), NONE, SOME (cterm_of thy (mk_number j))] t
  13.238 +
  13.239 +datatype call_fact =
  13.240 +   NoStep of thm
  13.241 + | Graph of (term * thm)
  13.242 +
  13.243 +fun rand (_ $ t) = t
  13.244 +
  13.245 +fun setup_probe_goal thy domT Dtab Mtab (i, j) =
  13.246 +    let
  13.247 +      val RD1 = get_elem (Dtab i)
  13.248 +      val RD2 = get_elem (Dtab j)
  13.249 +      val Ms1 = get_elem (Mtab i)
  13.250 +      val Ms2 = get_elem (Mtab j)
  13.251 +
  13.252 +      val Mst1 = HOLogic.dest_list (rand Ms1)
  13.253 +      val Mst2 = HOLogic.dest_list (rand Ms2)
  13.254 +
  13.255 +      val mvar1 = Free ("sctmfv1", domT --> HOLogic.natT)
  13.256 +      val mvar2 = Free ("sctmfv2", domT --> HOLogic.natT)
  13.257 +      val relvar = Free ("sctmfrel", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
  13.258 +      val N = length Mst1 and M = length Mst2
  13.259 +      val saved_state = HOLogic.mk_Trueprop (mk_stepP RD1 RD2 mvar1 mvar2 relvar)
  13.260 +                         |> cterm_of thy
  13.261 +                         |> Goal.init
  13.262 +                         |> CLASIMPSET auto_tac |> Seq.hd
  13.263 +                         
  13.264 +      val no_step = saved_state 
  13.265 +                      |> forall_intr (cterm_of thy relvar)
  13.266 +                      |> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const))))
  13.267 +                      |> CLASIMPSET auto_tac |> Seq.hd
  13.268 +
  13.269 +    in
  13.270 +      if Thm.no_prems no_step
  13.271 +      then NoStep (Goal.finish no_step RS no_stepI)
  13.272 +      else
  13.273 +        let
  13.274 +          fun set_m1 i =
  13.275 +              let 
  13.276 +                val M1 = nth Mst1 i
  13.277 +                val with_m1 = saved_state
  13.278 +                                |> forall_intr (cterm_of thy mvar1)
  13.279 +                                |> forall_elim (cterm_of thy M1)
  13.280 +                                |> CLASIMPSET auto_tac |> Seq.hd
  13.281 +
  13.282 +                fun set_m2 j = 
  13.283 +                    let 
  13.284 +                      val M2 = nth Mst2 j
  13.285 +                      val with_m2 = with_m1
  13.286 +                                      |> forall_intr (cterm_of thy mvar2)
  13.287 +                                      |> forall_elim (cterm_of thy M2)
  13.288 +                                      |> CLASIMPSET auto_tac |> Seq.hd
  13.289 +
  13.290 +                      val decr = forall_intr (cterm_of thy relvar)
  13.291 +                                   #> forall_elim (cterm_of thy less_nat_const)
  13.292 +                                   #> CLASIMPSET auto_tac #> Seq.hd
  13.293 +
  13.294 +                      val decreq = forall_intr (cterm_of thy relvar)
  13.295 +                                     #> forall_elim (cterm_of thy lesseq_nat_const)
  13.296 +                                     #> CLASIMPSET auto_tac #> Seq.hd
  13.297 +
  13.298 +                      val thm1 = decr with_m2
  13.299 +                    in
  13.300 +                      if Thm.no_prems thm1 
  13.301 +                      then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm1) 1))
  13.302 +                      else let val thm2 = decreq with_m2 in
  13.303 +                             if Thm.no_prems thm2 
  13.304 +                             then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm2) 1))
  13.305 +                             else all_tac end
  13.306 +                    end
  13.307 +              in set_m2 end
  13.308 +
  13.309 +          val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2)
  13.310 +
  13.311 +          val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1)))
  13.312 +                      THEN (rtac approx_empty 1)
  13.313 +
  13.314 +          val approx_thm = goal 
  13.315 +                    |> cterm_of thy
  13.316 +                    |> Goal.init
  13.317 +                    |> tac |> Seq.hd
  13.318 +                    |> Goal.finish
  13.319 +
  13.320 +          val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm
  13.321 +        in
  13.322 +          Graph (G, approx_thm)
  13.323 +        end
  13.324 +    end
  13.325 +
  13.326 +
  13.327 +
  13.328 +
  13.329 +
  13.330 +fun probe_nostep thy Dtab i j =
  13.331 +    HOLogic.mk_Trueprop (mk_no_step (get_elem (Dtab i)) (get_elem (Dtab j))) 
  13.332 +      |> cterm_of thy
  13.333 +      |> try_to_prove (unfold_then_auto no_step_def)
  13.334 +      |> simple_result
  13.335 +
  13.336 +fun probe_decr thy RD1 RD2 m1 m2 =
  13.337 +    HOLogic.mk_Trueprop (mk_decr RD1 RD2 m1 m2)
  13.338 +      |> cterm_of thy 
  13.339 +      |> try_to_prove (unfold_then_auto decr_def)
  13.340 +      |> simple_result
  13.341 +
  13.342 +fun probe_decreq thy RD1 RD2 m1 m2 =
  13.343 +    HOLogic.mk_Trueprop (mk_decreq RD1 RD2 m1 m2)
  13.344 +      |> cterm_of thy 
  13.345 +      |> try_to_prove (unfold_then_auto decreq_def)
  13.346 +      |> simple_result
  13.347 +
  13.348 +
  13.349 +fun pr_tac (st : thm) = Seq.single (Output.warning (PolyML.makestring st); st)
  13.350 +fun pr_thm (st : thm) = (Output.warning (PolyML.makestring st); st)
  13.351 +
  13.352 +
  13.353 +fun build_approximating_graph thy Dtab Mtab Mss mlens mint nint =
  13.354 +    let 
  13.355 +      val D1 = Dtab mint and D2 = Dtab nint
  13.356 +      val Mst1 = Mtab mint and Mst2 = Mtab nint
  13.357 +
  13.358 +      val RD1 = get_elem D1 and RD2 = get_elem D2
  13.359 +      val Ms1 = get_elem Mst1 and Ms2 = get_elem Mst2
  13.360 +
  13.361 +      val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2)
  13.362 +
  13.363 +      val Ms1 = nth (nth Mss mint) and Ms2 = nth (nth Mss mint)
  13.364 +
  13.365 +      fun add_edge (i,j) = 
  13.366 +          case timeap_msg ("decr(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")")
  13.367 +                          (probe_decr thy RD1 RD2 (Ms1 i)) (Ms2 j) of
  13.368 +            SOME thm => (Output.warning "Success"; (rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac thm 1))
  13.369 +          | NONE => case timeap_msg ("decr(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")")
  13.370 +                                    (probe_decreq thy RD1 RD2 (Ms1 i)) (Ms2 j) of
  13.371 +                      SOME thm => (Output.warning "Success"; (rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac thm 1))
  13.372 +                    | NONE => all_tac
  13.373 +
  13.374 +      val approx_thm =
  13.375 +          goal
  13.376 +            |> cterm_of thy
  13.377 +            |> Goal.init
  13.378 +            |> SINGLE ((EVERY (map add_edge (product (0 upto (nth mlens mint) - 1) (0 upto (nth mlens nint) - 1))))
  13.379 +                       THEN (rtac approx_empty 1))
  13.380 +            |> the
  13.381 +            |> Goal.finish
  13.382 +
  13.383 +      val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm
  13.384 +    in
  13.385 +      (G, approx_thm)
  13.386 +    end
  13.387 +
  13.388 +
  13.389 +
  13.390 +fun prove_call_fact thy Dtab Mtab Mss mlens (m, n) =
  13.391 +    case probe_nostep thy Dtab m n of
  13.392 +      SOME thm => (Output.warning "NoStep"; NoStep thm)
  13.393 +    | NONE => Graph (build_approximating_graph thy Dtab Mtab Mss mlens m n)
  13.394 +
  13.395 +
  13.396 +fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n))
  13.397 +
  13.398 +
  13.399 +fun mk_set T [] = Const ("{}", HOLogic.mk_setT T)
  13.400 +  | mk_set T (x :: xs) = Const ("insert",
  13.401 +      T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $ mk_set T xs
  13.402 +
  13.403 +fun dest_set (Const ("{}", _)) = []
  13.404 +  | dest_set (Const ("insert", _) $ x $ xs) = x :: dest_set xs
  13.405 +
  13.406 +val pr_graph = Sign.string_of_term
  13.407 +
  13.408 +
  13.409 +fun pr_matrix thy = map_matrix (fn Graph (G, _) => pr_graph thy G | _ => "X")
  13.410 +
  13.411 +val in_graph_tac = 
  13.412 +    simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
  13.413 +    THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *)
  13.414 +
  13.415 +fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
  13.416 +  | approx_tac (Graph (G, thm)) =
  13.417 +    rtac disjI2 1 
  13.418 +    THEN rtac exI 1
  13.419 +    THEN rtac conjI 1
  13.420 +    THEN rtac thm 2
  13.421 +    THEN in_graph_tac
  13.422 +
  13.423 +fun all_less_tac [] = rtac all_less_zero 1
  13.424 +  | all_less_tac (t :: ts) = rtac all_less_Suc 1 
  13.425 +                                  THEN simp_nth_tac 1
  13.426 +                                  THEN t 
  13.427 +                                  THEN all_less_tac ts
  13.428 +
  13.429 +
  13.430 +val length_const = "Nat.size"
  13.431 +fun mk_length l = Const (length_const, fastype_of l --> HOLogic.natT) $ l
  13.432 +val length_simps = thms "SCT_Interpretation.length_simps"
  13.433 +
  13.434 +
  13.435 +
  13.436 +fun mk_call_graph (st : thm) =
  13.437 +    let
  13.438 +      val thy = theory_of_thm st
  13.439 +      val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
  13.440 +
  13.441 +      val RDs = HOLogic.dest_list RDlist
  13.442 +      val n = length RDs 
  13.443 +
  13.444 +      val Mss = map measures_of RDs
  13.445 +
  13.446 +      val domT = domain_type (fastype_of (hd (hd Mss)))
  13.447 +
  13.448 +      val mfuns = map (fn Ms => mk_nth (HOLogic.mk_list (fastype_of (hd Ms)) Ms)) Mss
  13.449 +                      |> (fn l => HOLogic.mk_list (fastype_of (hd l)) l)
  13.450 +
  13.451 +      val Dtab = tabulate_tlist thy RDlist
  13.452 +      val Mtab = tabulate_tlist thy mfuns
  13.453 +
  13.454 +      val len_simp = Simplifier.rewrite (HOL_basic_ss addsimps length_simps) (cterm_of thy (mk_length RDlist))
  13.455 +
  13.456 +      val mlens = map length Mss
  13.457 +
  13.458 +      val indices = (n - 1 downto 0)
  13.459 +      val pairs = matrix indices indices
  13.460 +      val parts = map_matrix (fn (n,m) =>
  13.461 +                                 (timeap_msg (string_of_int n ^ "," ^ string_of_int m) 
  13.462 +                                             (setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs
  13.463 +
  13.464 +
  13.465 +      val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^
  13.466 +                                                                            pr_graph thy G ^ ",\n")
  13.467 +                                                     | _ => I) cs) parts ""
  13.468 +      val _ = Output.warning s
  13.469 +  
  13.470 +
  13.471 +      val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs)
  13.472 +                    |> mk_set (edgeT HOLogic.natT scgT)
  13.473 +                    |> curry op $ (graph_const HOLogic.natT scgT)
  13.474 +
  13.475 +
  13.476 +      val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns)
  13.477 +
  13.478 +      val tac = 
  13.479 +          (SIMPSET (unfold_tac [sound_int_def, len_simp]))
  13.480 +            THEN all_less_tac (map (all_less_tac o map approx_tac) parts)
  13.481 +    in
  13.482 +      tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
  13.483 +    end
  13.484 +                  
  13.485 +
  13.486 +
  13.487 +
  13.488 +
  13.489 +
  13.490 +
  13.491 +
  13.492 +
  13.493 +
  13.494 +
  13.495 +
  13.496 +(* Faster implementation of transitive closures *)
  13.497 +
  13.498 +(* sedge: Only relevant edges. Qtrees have separate value for 0 *)
  13.499 +datatype sedge = LESS | LEQ | BOTH
  13.500 +
  13.501 +
  13.502 +
  13.503 +datatype key = KHere | K0 of key | K1 of key
  13.504 +
  13.505 +datatype 'a stree = 
  13.506 +  sLeaf of 'a
  13.507 +  | sBranch of ('a * 'a stree * 'a stree)
  13.508 +
  13.509 +(*
  13.510 +fun lookup (sLeaf x) KHere = x
  13.511 +  | lookup (sBranch x s t) KHere = x
  13.512 +  | lookup (sBranch x s t) (K0 k) = lookup s k
  13.513 +  | lookup (sBranch x s t) (K1 k) = lookup t k
  13.514 +  | lookup _ _ = raise Match
  13.515 +*)
  13.516 +
  13.517 +datatype 'a qtree =
  13.518 +  QEmpty
  13.519 +  | QNode of 'a
  13.520 +  | QQuad of ('a qtree * 'a qtree * 'a qtree * 'a qtree)
  13.521 +
  13.522 +fun qlookup z QEmpty k l = z
  13.523 +  | qlookup z (QNode S) k l = S
  13.524 +  | qlookup z (QQuad (a, b, c, d)) (K0 k) (K0 l) = qlookup z a k l
  13.525 +  | qlookup z (QQuad (a, b, c, d)) (K0 k) (K1 l) = qlookup z b k l
  13.526 +  | qlookup z (QQuad (a, b, c, d)) (K1 k) (K0 l) = qlookup z c k l
  13.527 +  | qlookup z (QQuad (a, b, c, d)) (K1 k) (K1 l) = qlookup z d k l
  13.528 +  | qlookup _ _ _ _ = raise Match
  13.529 +
  13.530 +
  13.531 +
  13.532 +(* Size-change graphs *)
  13.533 +
  13.534 +type
  13.535 +  scg = sedge qtree
  13.536 +
  13.537 +
  13.538 +(* addition of single edges *)
  13.539 +fun add_sedge BOTH _ = BOTH
  13.540 +  | add_sedge LESS LESS = LESS
  13.541 +  | add_sedge LESS _ = BOTH
  13.542 +  | add_sedge LEQ LEQ = LEQ
  13.543 +  | add_sedge LEQ _ = BOTH
  13.544 +
  13.545 +fun mult_sedge LESS _ = LESS
  13.546 +  | mult_sedge _ LESS = LESS
  13.547 +  | mult_sedge LEQ x = x
  13.548 +  | mult_sedge BOTH _ = BOTH
  13.549 +
  13.550 +fun subsumes_edge LESS LESS = true
  13.551 +  | subsumes_edge LEQ _ = true
  13.552 +  | subsumes_edge _ _ = false
  13.553 +
  13.554 +
  13.555 +
  13.556 +
  13.557 +(* subsumes_SCG G H := G contains strictly less estimations than H *)
  13.558 +fun subsumes_SCG (QEmpty : scg) (H : scg) = true
  13.559 +  | subsumes_SCG (QQuad (a, b, c, d)) (QQuad (e,f,g,h)) =
  13.560 +    (subsumes_SCG a e) andalso (subsumes_SCG b f)
  13.561 +    andalso (subsumes_SCG c g) andalso (subsumes_SCG d h)
  13.562 +  | subsumes_SCG (QNode e) (QNode e') = subsumes_edge e e'
  13.563 +  | subsumes_SCG _ QEmpty = false
  13.564 +  | subsumes_SCG _ _ = raise Match
  13.565 +
  13.566 +
  13.567 +(* managing lists of SCGs. *)
  13.568 +
  13.569 +(* 
  13.570 + Graphs are partially ordered. A list of graphs has the invariant that no G,H with G <= H.
  13.571 + To maintain this when adding a new graph G, check 
  13.572 +   (1) G <= H for some H in l => Do nothing
  13.573 +   (2) has to be added. Then, all H <= G can be removed. 
  13.574 +
  13.575 + We can check (2) first, removing all smaller graphs. 
  13.576 + If we could remove at least one, just add G in the end (Invariant!).
  13.577 + Otherwise, check again, if G needs to be added at all. 
  13.578 +
  13.579 + OTOH, doing (1) first is probably better, because it does not produce garbage unless needed.
  13.580 +
  13.581 + The definition is tail-recursive. Order is not preserved (unneccessary).
  13.582 +*)
  13.583 +
  13.584 +
  13.585 +
  13.586 +fun add_scg' G Hs = (* returns a flag indicating if the graph was really added *)
  13.587 +    if exists (fn H => subsumes_SCG H G) Hs then (false, Hs)  (* redundant addition *)
  13.588 +    else (true, G :: remove (uncurry subsumes_SCG) G Hs) (* remove all new redundancy and add G *)
  13.589 +         (* NB: This does the second checks twice :-( *)
  13.590 +
  13.591 +(* Simpler version *)
  13.592 +fun add_scg' G Hs = (not (member (op =) Hs G), insert (op =) G Hs)
  13.593 +
  13.594 +
  13.595 +val add_scg = snd oo add_scg' (* without flag *)
  13.596 +
  13.597 +
  13.598 +
  13.599 +
  13.600 +
  13.601 +(* quadtrees *)
  13.602 +
  13.603 +fun keylen 0 = 0 
  13.604 +  | keylen n = (keylen (n div 2)) + 1
  13.605 +
  13.606 +fun mk_key 0 _  = KHere
  13.607 +  | mk_key l m = if m mod 2 = 0 
  13.608 +                 then K0 (mk_key (l - 1) (m div 2)) 
  13.609 +                 else K1 (mk_key (l - 1) (m div 2)) 
  13.610 +
  13.611 +
  13.612 +fun qupdate f KHere KHere n = f n
  13.613 +  | qupdate f (K0 k) (K0 k') (QQuad (a, b, c, d)) = QQuad (qupdate f k k' a, b, c, d)
  13.614 +  | qupdate f (K0 k) (K1 k') (QQuad (a, b, c, d)) = QQuad (a, qupdate f k k' b, c, d)
  13.615 +  | qupdate f (K1 k) (K0 k') (QQuad (a, b, c, d)) = QQuad (a, b, qupdate f k k' c, d)
  13.616 +  | qupdate f (K1 k) (K1 k') (QQuad (a, b, c, d)) = QQuad (a, b, c, qupdate f k k' d)
  13.617 +
  13.618 +
  13.619 +
  13.620 +
  13.621 +
  13.622 +
  13.623 +
  13.624 +
  13.625 +(* quadtree composition *)
  13.626 +
  13.627 +fun qadd A QEmpty q = q
  13.628 +  | qadd A q QEmpty = q
  13.629 +  | qadd A (QNode s) (QNode t) = QNode (A s t)
  13.630 +  | qadd A (QQuad (a, b, c, d)) (QQuad (e, f, g, h)) =
  13.631 +    QQuad (qadd A a e, qadd A b f, qadd A c g, qadd A d h)
  13.632 +  | qadd _ _ _ = raise Match
  13.633 +
  13.634 +
  13.635 +fun qmult A m QEmpty H = QEmpty
  13.636 +  | qmult A m G QEmpty = QEmpty
  13.637 +  | qmult A m (QNode x) (QNode y) = QNode (m x y)
  13.638 +  | qmult A m (QQuad (a, b, c, d)) (QQuad (e, f, g, h)) = 
  13.639 +    QQuad ((qadd A (qmult A m a e) (qmult A m b g)),
  13.640 +           (qadd A (qmult A m a f) (qmult A m b h)),
  13.641 +           (qadd A (qmult A m c e) (qmult A m d g)),
  13.642 +           (qadd A (qmult A m c f) (qmult A m d h)))
  13.643 +  | qmult _ _ _ _ = raise Match
  13.644 +
  13.645 +
  13.646 +val (mult_scg : scg -> scg -> scg) = qmult add_sedge mult_sedge
  13.647 +
  13.648 +(* Misc notes:
  13.649 +
  13.650 +- When building the tcl: Check on addition and raise FAIL if the property is not true... (pract)
  13.651 +
  13.652 +- Can we reduce subsumption checking by some integer fingerprints?
  13.653 +
  13.654 + Number of edges: LESS(G) LEQ(G)
  13.655 +  G <= H ==> E(G) <= E(H)
  13.656 +  
  13.657 +
  13.658 +
  13.659 +How to check:
  13.660 +
  13.661 +For each pair of adjacent edges: n -> m -> q
  13.662 + compute all product SCGS and check if they are subsumed by something in the tcl.
  13.663 +
  13.664 + all midnode m: all fromnode n: all tonode q: alledges (n,m) e: alledges (m,q) e': subsumes (e*e') (edgs m,q)
  13.665 +
  13.666 + This is still quite a lot of checking... But: no garbage, just inspection. Can probably be done in logic. 
  13.667 +
  13.668 +*)
  13.669 +
  13.670 +
  13.671 +
  13.672 +(* Operations on lists: These preserve the invariants *)
  13.673 +fun SCGs_mult Gs Hs = fold (fn (G,H) => add_scg (mult_scg G H)) (product Gs Hs) []
  13.674 +val SCGs_plus = fold add_scg
  13.675 +
  13.676 +
  13.677 +fun add_scgs Gs Hs = fold_rev (fn G => fn (Xs,As) => 
  13.678 +                                      let val (b, Xs') = add_scg' G Xs
  13.679 +                                      in (Xs', if b then G::As else As) end)
  13.680 +                          Gs (Hs,[])
  13.681 +
  13.682 +(* Transitive Closure for lists of SCGs *)
  13.683 +fun SCGs_tcl Gs =
  13.684 +    let
  13.685 +      fun aux S [] = S
  13.686 +        | aux S (H::HS) =
  13.687 +          let val (S', Ns) = add_scgs (map (mult_scg H) Gs) S
  13.688 +          in aux S' (SCGs_plus Ns HS) end
  13.689 +    in
  13.690 +      aux Gs Gs
  13.691 +    end
  13.692 +
  13.693 +
  13.694 +
  13.695 +(* Kleene algorithm: DP version, with imperative array... *)
  13.696 +
  13.697 +
  13.698 +
  13.699 +
  13.700 +(* Terrible imperative stuff: *)
  13.701 +type matrix = scg list array array
  13.702 +
  13.703 +fun mupdate i j f M = 
  13.704 +    let 
  13.705 +      val row = Array.sub (M, i)
  13.706 +      val x = Array.sub (row, j)
  13.707 +    in 
  13.708 +      Array.update (row, j, f x)
  13.709 +    end
  13.710 +
  13.711 +fun mget i j M = Array.sub(Array.sub(M,i),j)
  13.712 +
  13.713 +fun print_scg (x : scg) = Output.warning (PolyML.makestring x);
  13.714 +
  13.715 +
  13.716 +fun kleene add mult tcl M =
  13.717 +    let
  13.718 +      val n = Array.length M
  13.719 +
  13.720 +      fun update Mkk i j k = 
  13.721 +          let
  13.722 +            val Mik = mget i k M
  13.723 +            val Mkj = mget k j M
  13.724 +          in
  13.725 +            mupdate i j (fn X => X |> add (mult Mik (mult Mkk Mkj))
  13.726 +                                   |> add (mult Mik Mkj))
  13.727 +                    M
  13.728 +          end
  13.729 +
  13.730 +      fun step k () =
  13.731 +          let
  13.732 +            val _ = mupdate k k tcl M
  13.733 +            val Mkk = mget k k M
  13.734 +
  13.735 +            val no_k = filter_out (fn i => i = k) (0 upto (n - 1)) 
  13.736 +            val _ = fold (fn i => fold (fn j => K (update Mkk i j k)) no_k) no_k ()
  13.737 +
  13.738 +            val _ = fold (fn i => K (update Mkk i k k)) no_k ()
  13.739 +
  13.740 +            val _ = fold (fn j => K (update Mkk k j k)) no_k ()
  13.741 +          in
  13.742 +            ()
  13.743 +          end
  13.744 +    in
  13.745 +      fold step (0 upto (n - 1)) ()
  13.746 +    end
  13.747 +
  13.748 +val (SCGs_kleene : matrix -> unit) = kleene SCGs_plus SCGs_mult SCGs_tcl
  13.749 +
  13.750 +
  13.751 +fun andop x y = x andalso y
  13.752 +fun orop x y = x orelse y
  13.753 +
  13.754 +fun array2 n x = Array.tabulate (n, (fn i => Array.array (n, x)))
  13.755 +
  13.756 +(*val bool_kleene = kleene orop andop I
  13.757 +
  13.758 +
  13.759 +fun test_bool () =
  13.760 +    let
  13.761 +      val M = array2 2 false
  13.762 +      val _ = mupdate 0 1 (K true) M
  13.763 +      val _ = mupdate 1 0 (K true) M
  13.764 +      val _ = bool_kleene M
  13.765 +    in
  13.766 +      M
  13.767 +    end
  13.768 +*)
  13.769 +
  13.770 +(* Standard 2-2-Size-change graphs *)
  13.771 +
  13.772 +val swap = QQuad(QEmpty, QNode LEQ,
  13.773 +                 QNode LEQ, QEmpty)
  13.774 +
  13.775 +val swapRTop = QQuad(QNode LESS, QNode LEQ,
  13.776 +                     QNode LEQ, QEmpty)
  13.777 +
  13.778 +val BTopRBot = QQuad(QNode LEQ, QEmpty,
  13.779 +                     QEmpty, QNode LESS)
  13.780 +
  13.781 +val RTopBBot = QQuad(QNode LESS, QEmpty,
  13.782 +                     QEmpty, QNode LEQ)
  13.783 +
  13.784 +val R2Straight = QQuad(QNode LESS, QEmpty,
  13.785 +                       QEmpty, QNode LESS)
  13.786 +
  13.787 +val R3StraightUp = QQuad(QNode LESS, QEmpty,
  13.788 +                         QNode LESS, QNode LESS)
  13.789 +
  13.790 +val R3StraightDn = QQuad(QNode LESS, QNode LESS,
  13.791 +                         QEmpty, QNode LESS)
  13.792 +
  13.793 +
  13.794 +
  13.795 +
  13.796 +val diag = QQuad(QEmpty, QNode LEQ,
  13.797 +                 QEmpty, QEmpty)
  13.798 +
  13.799 +val straight = QQuad(QNode LEQ, QEmpty,
  13.800 +                     QEmpty, QEmpty)
  13.801 +
  13.802 +
  13.803 +
  13.804 +val R467913 = ([R2Straight, R3StraightDn, R3StraightDn] @ replicate 11 R2Straight @ [R3StraightUp, R3StraightUp])
  13.805 +                |> map single
  13.806 +
  13.807 +val swapPos = [(0,8),(0,9),(0,10),(3,4),(3,5),(11,12)]
  13.808 +
  13.809 +val BRPos = (map (pair 5) (0 :: (3 upto 7)))
  13.810 +            @ (map (pair 8) [8,9,11,12,13])
  13.811 +            @ (map (pair 12) [8,9,11,12,13])
  13.812 +
  13.813 +val RBPos = map (pair 10) (3 upto 10)
  13.814 +
  13.815 +fun afold f arr x = Array.foldl (uncurry f) x arr
  13.816 +
  13.817 +fun msize M = afold (afold (curry op + o length)) M 0
  13.818 +
  13.819 +fun TestM () =
  13.820 +    let
  13.821 +      val M = array2 16 ([] : scg list)
  13.822 +      val _ = Array.update (M, 4, Array.fromList R467913)
  13.823 +      val _ = Array.update (M, 6, Array.fromList R467913)
  13.824 +      val _ = Array.update (M, 7, Array.fromList R467913)
  13.825 +      val _ = Array.update (M, 9, Array.fromList R467913)
  13.826 +      val _ = Array.update (M, 13, Array.fromList R467913)
  13.827 +
  13.828 +      val _ = map (fn (i,j) => mupdate i j (K [swap]) M) swapPos
  13.829 +      val _ = map (fn (i,j) => mupdate i j (K [BTopRBot]) M) BRPos
  13.830 +      val _ = map (fn (i,j) => mupdate i j (K [RTopBBot]) M) RBPos
  13.831 +
  13.832 +      val _ = mupdate 1 14 (K [swapRTop]) M
  13.833 +      val _ = mupdate 2 15 (K [swapRTop]) M
  13.834 +
  13.835 +      val G = [QQuad (QNode LEQ, QNode LESS, QEmpty, QNode LESS)]
  13.836 +      val _ = mupdate 5 1 (K G) M
  13.837 +      val _ = mupdate 8 2 (K G) M
  13.838 +      val _ = mupdate 12 2 (K G) M
  13.839 +
  13.840 +      val G = [QQuad (QNode LESS, QEmpty, QNode LESS, QNode LEQ)]
  13.841 +      val _ = mupdate 10 14 (K G) M
  13.842 +
  13.843 +      val G = [QQuad (QEmpty, QNode LEQ, QNode LESS, QNode LESS)]
  13.844 +      val _ = mupdate 14 1 (K G) M
  13.845 +      val _ = mupdate 14 2 (K G) M
  13.846 +      val _ = mupdate 15 1 (K G) M
  13.847 +      val _ = mupdate 15 2 (K G) M
  13.848 +    in
  13.849 +      M
  13.850 +    end
  13.851 +
  13.852 +
  13.853 +
  13.854 +
  13.855 +
  13.856 +fun add_edge x QEmpty = QNode x
  13.857 +  | add_edge x (QNode y) = QNode (add_sedge x y)
  13.858 +
  13.859 +
  13.860 +fun sedge2ML (Const ("SCT_Definition.sedge.LESS", _)) = LESS
  13.861 +  | sedge2ML (Const ("SCT_Definition.sedge.LEQ", _)) = LEQ
  13.862 +
  13.863 +
  13.864 +
  13.865 +
  13.866 +
  13.867 +
  13.868 +
  13.869 +
  13.870 +
  13.871 +
  13.872 +
  13.873 +
  13.874 +
  13.875 +
  13.876 +
  13.877 +
  13.878 +end                   
  13.879 +
  13.880 +
  13.881 +
  13.882 +
  13.883 +
  13.884 +