Added formalization of size-change principle (experimental).
--- a/src/HOL/IsaMakefile Mon Feb 26 20:14:52 2007 +0100
+++ b/src/HOL/IsaMakefile Mon Feb 26 21:34:16 2007 +0100
@@ -207,7 +207,11 @@
Library/Product_ord.thy Library/Char_ord.thy \
Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
Library/Coinductive_List.thy Library/AssocList.thy \
- Library/Parity.thy Library/GCD.thy Library/Binomial.thy
+ Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
+ Library/Graphs.thy Library/Kleene_Algebras.thy Library/SCT_Misc.thy \
+ Library/SCT_Definition.thy Library/SCT_Theorem.thy Library/SCT_Interpretation.thy \
+ Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
+ Library/SCT_Examples.thy
@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Graphs.thy Mon Feb 26 21:34:16 2007 +0100
@@ -0,0 +1,721 @@
+theory Graphs
+imports Main SCT_Misc Kleene_Algebras ExecutableSet
+begin
+
+
+section {* Basic types, Size Change Graphs *}
+
+datatype ('a, 'b) graph =
+ Graph "('a \<times> 'b \<times> 'a) set"
+
+fun dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"
+ where "dest_graph (Graph G) = G"
+
+lemma graph_dest_graph[simp]:
+ "Graph (dest_graph G) = G"
+ by (cases G) simp
+
+definition
+ has_edge :: "('n,'e) graph \<Rightarrow> 'n \<Rightarrow> 'e \<Rightarrow> 'n \<Rightarrow> bool"
+("_ \<turnstile> _ \<leadsto>\<^bsup>_\<^esup> _")
+where
+ "has_edge G n e n' = ((n, e, n') \<in> dest_graph G)"
+
+
+
+section {* Graph composition *}
+
+fun grcomp :: "('n, 'e::times) graph \<Rightarrow> ('n, 'e) graph \<Rightarrow> ('n, 'e) graph"
+where
+ "grcomp (Graph G) (Graph H) =
+ Graph {(p,b,q) | p b q.
+ (\<exists>k e e'. (p,e,k)\<in>G \<and> (k,e',q)\<in>H \<and> b = e * e')}"
+
+
+declare grcomp.simps[code del]
+
+
+lemma graph_ext:
+ assumes "\<And>n e n'. has_edge G n e n' = has_edge H n e n'"
+ shows "G = H"
+ using prems
+ by (cases G, cases H, auto simp:split_paired_all has_edge_def)
+
+
+instance graph :: (type, times) times
+ graph_mult_def: "G * H == grcomp G H" ..
+
+instance graph :: (type, one) one
+ graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
+
+instance graph :: (type, type) zero
+ graph_zero_def: "0 == Graph {}" ..
+
+instance graph :: (type, type) plus
+ graph_plus_def: "G + H == Graph (dest_graph G \<union> dest_graph H)" ..
+
+
+subsection {* Simprules for the graph operations *}
+
+lemma in_grcomp:
+ "has_edge (G * H) p b q
+ = (\<exists>k e e'. has_edge G p e k \<and> has_edge H k e' q \<and> b = e * e')"
+ by (cases G, cases H) (auto simp:graph_mult_def has_edge_def image_def)
+
+lemma in_grunit:
+ "has_edge 1 p b q = (p = q \<and> b = 1)"
+ by (auto simp:graph_one_def has_edge_def)
+
+lemma in_grplus:
+ "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
+ by (cases G, cases H, auto simp:has_edge_def graph_plus_def)
+
+lemma in_grzero:
+ "has_edge 0 p b q = False"
+ by (simp add:graph_zero_def has_edge_def)
+
+
+instance graph :: (type, semigroup_mult) semigroup_mult
+proof
+ fix G1 G2 G3 :: "('a,'b) graph"
+
+ show "G1 * G2 * G3 = G1 * (G2 * G3)"
+ proof (rule graph_ext, rule trans)
+ fix p J q
+ show "has_edge ((G1 * G2) * G3) p J q =
+ (\<exists>G i H j I.
+ has_edge G1 p G i
+ \<and> has_edge G2 i H j
+ \<and> has_edge G3 j I q
+ \<and> J = (G * H) * I)"
+ by (simp only:in_grcomp) blast
+ show "\<dots> = has_edge (G1 * (G2 * G3)) p J q"
+ by (simp only:in_grcomp mult_assoc) blast
+ qed
+qed
+
+instance graph :: (type, monoid_mult) monoid_mult
+proof
+ fix G1 G2 G3 :: "('a,'b) graph"
+
+ show "1 * G1 = G1"
+ by (rule graph_ext) (auto simp:in_grcomp in_grunit)
+ show "G1 * 1 = G1"
+ by (rule graph_ext) (auto simp:in_grcomp in_grunit)
+qed
+
+
+lemma grcomp_rdist:
+ fixes G :: "('a::type, 'b::semigroup_mult) graph"
+ shows "G * (H + I) = G * H + G * I"
+ by (rule graph_ext, simp add:in_grcomp in_grplus) blast
+
+lemma grcomp_ldist:
+ fixes G :: "('a::type, 'b::semigroup_mult) graph"
+ shows "(G + H) * I = G * I + H * I"
+ by (rule graph_ext, simp add:in_grcomp in_grplus) blast
+
+fun grpow :: "nat \<Rightarrow> ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a, 'b) graph"
+where
+ "grpow 0 A = 1"
+| "grpow (Suc n) A = A * (grpow n A)"
+
+
+instance graph :: (type, monoid_mult) recpower
+ graph_pow_def: "A ^ n == grpow n A"
+ by default (simp_all add:graph_pow_def)
+
+subsection {* Order on Graphs *}
+
+instance graph :: (type, type) ord
+ graph_leq_def: "G \<le> H == dest_graph G \<subseteq> dest_graph H"
+ graph_less_def: "G < H == dest_graph G \<subset> dest_graph H" ..
+
+instance graph :: (type, type) order
+proof
+ fix x y z :: "('a,'b) graph"
+
+ show "x \<le> x" unfolding graph_leq_def ..
+
+ from order_trans
+ show "\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z" unfolding graph_leq_def .
+
+ show "\<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" unfolding graph_leq_def
+ by (cases x, cases y) simp
+
+ show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
+ unfolding graph_leq_def graph_less_def
+ by (cases x, cases y) auto
+qed
+
+
+defs (overloaded)
+ Meet_graph_def: "Meet == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
+
+instance graph :: (type, type) comp_lat
+ by default (auto simp:Meet_graph_def is_join_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
+
+lemma plus_graph_is_join: "is_join ((op +)::('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
+ unfolding is_join_def
+proof (intro allI conjI impI)
+ fix a b x :: "('a, 'b) graph"
+
+ show "a \<le> a + b" "b \<le> a + b" "a \<le> x \<and> b \<le> x \<Longrightarrow> a + b \<le> x"
+ unfolding graph_leq_def graph_plus_def
+ by (cases a, cases b) auto
+qed
+
+lemma plus_is_join:
+ "(op +) =
+ (join :: ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
+ using plus_graph_is_join by (simp add:join_unique)
+
+instance graph :: (type, monoid_mult) semiring_1
+proof
+ fix a b c :: "('a, 'b) graph"
+
+ show "a + b + c = a + (b + c)"
+ and "a + b = b + a" unfolding graph_plus_def
+ by auto
+
+ show "0 + a = a" unfolding graph_zero_def graph_plus_def
+ by simp
+
+ show "0 * a = 0" "a * 0 = 0" unfolding graph_zero_def graph_mult_def
+ by (cases a, simp)+
+
+ show "(a + b) * c = a * c + b * c"
+ by (rule graph_ext, simp add:in_grcomp in_grplus) blast
+
+ show "a * (b + c) = a * b + a * c"
+ by (rule graph_ext, simp add:in_grcomp in_grplus) blast
+
+ show "(0::('a,'b) graph) \<noteq> 1" unfolding graph_zero_def graph_one_def
+ by simp
+qed
+
+
+instance graph :: (type, monoid_mult) idem_add
+proof
+ fix a :: "('a, 'b) graph"
+ show "a + a = a" unfolding plus_is_join by simp
+qed
+
+
+(* define star on graphs *)
+
+
+instance graph :: (type, monoid_mult) star
+ graph_star_def: "star G == (SUP n. G ^ n)" ..
+
+
+lemma graph_leqI:
+ assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
+ shows "G \<le> H"
+ using prems
+ unfolding graph_leq_def has_edge_def
+ by auto
+
+
+lemma in_graph_plusE:
+ assumes "has_edge (G + H) n e n'"
+ assumes "has_edge G n e n' \<Longrightarrow> P"
+ assumes "has_edge H n e n' \<Longrightarrow> P"
+ shows P
+ using prems
+ by (auto simp: in_grplus)
+
+
+
+lemma
+ assumes "x \<in> S k"
+ shows "x \<in> (\<Union>k. S k)"
+ using prems by blast
+
+lemma graph_union_least:
+ assumes "\<And>n. Graph (G n) \<le> C"
+ shows "Graph (\<Union>n. G n) \<le> C"
+ using prems unfolding graph_leq_def
+ by auto
+
+lemma Sup_graph_eq:
+ "(SUP n. Graph (G n)) = Graph (\<Union>n. G n)"
+ unfolding SUP_def
+ apply (rule order_antisym)
+ apply (rule Sup_least)
+ apply auto
+ apply (simp add:graph_leq_def)
+ apply auto
+ apply (rule graph_union_least)
+ apply (rule Sup_upper)
+ by auto
+
+lemma has_edge_leq: "has_edge G p b q = (Graph {(p,b,q)} \<le> G)"
+ unfolding has_edge_def graph_leq_def
+ by (cases G) simp
+
+
+lemma Sup_graph_eq2:
+ "(SUP n. G n) = Graph (\<Union>n. dest_graph (G n))"
+ using Sup_graph_eq[of "\<lambda>n. dest_graph (G n)", simplified]
+ by simp
+
+lemma in_SUP:
+ "has_edge (SUP x. Gs x) p b q = (\<exists>x. has_edge (Gs x) p b q)"
+ unfolding Sup_graph_eq2 has_edge_leq graph_leq_def
+ by simp
+
+instance graph :: (type, monoid_mult) kleene_by_comp_lat
+proof
+ fix a b c :: "('a, 'b) graph"
+
+ show "a \<le> b \<longleftrightarrow> a + b = b" unfolding graph_leq_def graph_plus_def
+ by (cases a, cases b) auto
+
+ from order_less_le show "a < b \<longleftrightarrow> a \<le> b \<and> a \<noteq> b" .
+
+ show "a * star b * c = (SUP n. a * b ^ n * c)"
+ unfolding graph_star_def
+ by (rule graph_ext) (force simp:in_SUP in_grcomp)
+qed
+
+
+lemma in_star:
+ "has_edge (star G) a x b = (\<exists>n. has_edge (G ^ n) a x b)"
+ by (auto simp:graph_star_def in_SUP)
+
+lemma tcl_is_SUP:
+ "tcl (G::('a::type, 'b::monoid_mult) graph) =
+ (SUP n. G ^ (Suc n))"
+ unfolding tcl_def
+ using star_cont[of 1 G G]
+ by (simp add:power_Suc power_commutes)
+
+
+lemma in_tcl:
+ "has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)"
+ apply (auto simp: tcl_is_SUP in_SUP)
+ apply (rule_tac x = "n - 1" in exI, auto)
+ done
+
+
+
+section {* Infinite Paths *}
+
+types ('n, 'e) ipath = "('n \<times> 'e) sequence"
+
+definition has_ipath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) ipath \<Rightarrow> bool"
+where
+ "has_ipath G p =
+ (\<forall>i. has_edge G (fst (p i)) (snd (p i)) (fst (p (Suc i))))"
+
+
+
+section {* Finite Paths *}
+
+types ('n, 'e) fpath = "('n \<times> ('e \<times> 'n) list)"
+
+inductive2 has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool"
+ for G :: "('n, 'e) graph"
+where
+ has_fpath_empty: "has_fpath G (n, [])"
+| 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)"
+
+definition
+ "end_node p =
+ (if snd p = [] then fst p else snd (snd p ! (length (snd p) - 1)))"
+
+definition path_nth :: "('n, 'e) fpath \<Rightarrow> nat \<Rightarrow> ('n \<times> 'e \<times> 'n)"
+where
+ "path_nth p k = (if k = 0 then fst p else snd (snd p ! (k - 1)), snd p ! k)"
+
+lemma endnode_nth:
+ assumes "length (snd p) = Suc k"
+ shows "end_node p = snd (snd (path_nth p k))"
+ using prems unfolding end_node_def path_nth_def
+ by auto
+
+lemma path_nth_graph:
+ assumes "k < length (snd p)"
+ assumes "has_fpath G p"
+ shows "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p k)"
+ using prems
+proof (induct k arbitrary:p)
+ case 0 thus ?case
+ unfolding path_nth_def by (auto elim:has_fpath.cases)
+next
+ case (Suc k p)
+
+ from `has_fpath G p` show ?case
+ proof (rule has_fpath.cases)
+ case goal1 with Suc show ?case by simp
+ next
+ fix n e n' es
+ assume st: "p = (n, (e, n') # es)"
+ "G \<turnstile> n \<leadsto>\<^bsup>e\<^esup> n'"
+ "has_fpath G (n', es)"
+ with Suc
+ have "(\<lambda>(n, b, a). G \<turnstile> n \<leadsto>\<^bsup>b\<^esup> a) (path_nth (n', es) k)" by simp
+ with st show ?thesis by (cases k, auto simp:path_nth_def)
+ qed
+qed
+
+lemma path_nth_connected:
+ assumes "Suc k < length (snd p)"
+ shows "fst (path_nth p (Suc k)) = snd (snd (path_nth p k))"
+ using prems
+ unfolding path_nth_def
+ by auto
+
+definition path_loop :: "('n, 'e) fpath \<Rightarrow> ('n, 'e) ipath" ("omega")
+where
+ "omega p \<equiv> (\<lambda>i. (\<lambda>(n,e,n'). (n,e)) (path_nth p (i mod (length (snd p)))))"
+
+lemma fst_p0: "fst (path_nth p 0) = fst p"
+ unfolding path_nth_def by simp
+
+lemma path_loop_connect:
+ assumes "fst p = end_node p"
+ and "0 < length (snd p)" (is "0 < ?l")
+ shows "fst (path_nth p (Suc i mod (length (snd p))))
+ = snd (snd (path_nth p (i mod length (snd p))))"
+ (is "\<dots> = snd (snd (path_nth p ?k))")
+proof -
+ from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
+ by simp
+
+ show ?thesis
+ proof (cases "Suc ?k < ?l")
+ case True
+ hence "Suc ?k \<noteq> ?l" by simp
+ with path_nth_connected[OF True]
+ show ?thesis
+ by (simp add:mod_Suc)
+ next
+ case False
+ with `?k < ?l` have wrap: "Suc ?k = ?l" by simp
+
+ hence "fst (path_nth p (Suc i mod ?l)) = fst (path_nth p 0)"
+ by (simp add: mod_Suc)
+ also from fst_p0 have "\<dots> = fst p" .
+ also have "\<dots> = end_node p" .
+ also have "\<dots> = snd (snd (path_nth p ?k))"
+ by (auto simp:endnode_nth wrap)
+ finally show ?thesis .
+ qed
+qed
+
+lemma path_loop_graph:
+ assumes "has_fpath G p"
+ and loop: "fst p = end_node p"
+ and nonempty: "0 < length (snd p)" (is "0 < ?l")
+ shows "has_ipath G (omega p)"
+proof (auto simp:has_ipath_def)
+ fix i
+ from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
+ by simp
+ with path_nth_graph
+ have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)" .
+
+ from path_loop_connect[OF loop nonempty] pk_G
+ show "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))"
+ unfolding path_loop_def has_edge_def split_def
+ by simp
+qed
+
+definition prod :: "('n, 'e::monoid_mult) fpath \<Rightarrow> 'e"
+where
+ "prod p = foldr (op *) (map fst (snd p)) 1"
+
+lemma prod_simps[simp]:
+ "prod (n, []) = 1"
+ "prod (n, (e,n')#es) = e * (prod (n',es))"
+unfolding prod_def
+by simp_all
+
+lemma power_induces_path:
+ assumes a: "has_edge (A ^ k) n G m"
+ obtains p
+ where "has_fpath A p"
+ and "n = fst p" "m = end_node p"
+ and "G = prod p"
+ and "k = length (snd p)"
+ using a
+proof (induct k arbitrary:m n G thesis)
+ case (0 m n G)
+ let ?p = "(n, [])"
+ from 0 have "has_fpath A ?p" "m = end_node ?p" "G = prod ?p"
+ by (auto simp:in_grunit end_node_def intro:has_fpath.intros)
+ thus ?case using 0 by (auto simp:end_node_def)
+next
+ case (Suc k m n G)
+ hence "has_edge (A * A ^ k) n G m"
+ by (simp add:power_Suc power_commutes)
+ then obtain G' H j where
+ a_A: "has_edge A n G' j"
+ and H_pow: "has_edge (A ^ k) j H m"
+ and [simp]: "G = G' * H"
+ by (auto simp:in_grcomp)
+
+ from H_pow and Suc
+ obtain p
+ where p_path: "has_fpath A p"
+ and [simp]: "j = fst p" "m = end_node p" "H = prod p"
+ "k = length (snd p)"
+ by blast
+
+ let ?p' = "(n, (G', j)#snd p)"
+ from a_A and p_path
+ have "has_fpath A ?p'" "m = end_node ?p'" "G = prod ?p'"
+ by (auto simp:end_node_def nth.simps intro:has_fpath.intros split:nat.split)
+ thus ?case using Suc by auto
+qed
+
+
+
+
+
+section {* Sub-Paths *}
+
+
+definition sub_path :: "('n, 'e) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ('n, 'e) fpath"
+("(_\<langle>_,_\<rangle>)")
+where
+ "p\<langle>i,j\<rangle> =
+ (fst (p i), map (\<lambda>k. (snd (p k), fst (p (Suc k)))) [i ..< j])"
+
+
+lemma sub_path_is_path:
+ assumes ipath: "has_ipath G p"
+ assumes l: "i \<le> j"
+ shows "has_fpath G (p\<langle>i,j\<rangle>)"
+ using l
+proof (induct i rule:inc_induct)
+ case 1 show ?case by (auto simp:sub_path_def intro:has_fpath.intros)
+next
+ case (2 i)
+ with ipath upt_rec[of i j]
+ show ?case
+ by (auto simp:sub_path_def has_ipath_def intro:has_fpath.intros)
+qed
+
+
+lemma sub_path_start[simp]:
+ "fst (p\<langle>i,j\<rangle>) = fst (p i)"
+ by (simp add:sub_path_def)
+
+lemma nth_upto[simp]: "k < j - i \<Longrightarrow> [i ..< j] ! k = i + k"
+ by (induct k) auto
+
+lemma sub_path_end[simp]:
+ "i < j \<Longrightarrow> end_node (p\<langle>i,j\<rangle>) = fst (p j)"
+ by (auto simp:sub_path_def end_node_def)
+
+lemma foldr_map: "foldr f (map g xs) = foldr (f o g) xs"
+ by (induct xs) auto
+
+lemma upto_append[simp]:
+ assumes "i \<le> j" "j \<le> k"
+ shows "[ i ..< j ] @ [j ..< k] = [i ..< k]"
+ using prems and upt_add_eq_append[of i j "k - j"]
+ by simp
+
+lemma foldr_monoid: "foldr (op *) xs 1 * foldr (op *) ys 1
+ = foldr (op *) (xs @ ys) (1::'a::monoid_mult)"
+ by (induct xs) (auto simp:mult_assoc)
+
+lemma sub_path_prod:
+ assumes "i < j"
+ assumes "j < k"
+ shows "prod (p\<langle>i,k\<rangle>) = prod (p\<langle>i,j\<rangle>) * prod (p\<langle>j,k\<rangle>)"
+ using prems
+ unfolding prod_def sub_path_def
+ by (simp add:map_compose[symmetric] comp_def)
+ (simp only:foldr_monoid map_append[symmetric] upto_append)
+
+
+lemma path_acgpow_aux:
+ assumes "length es = l"
+ assumes "has_fpath G (n,es)"
+ shows "has_edge (G ^ l) n (prod (n,es)) (end_node (n,es))"
+using prems
+proof (induct l arbitrary:n es)
+ case 0 thus ?case
+ by (simp add:in_grunit end_node_def)
+next
+ case (Suc l n es)
+ hence "es \<noteq> []" by auto
+ let ?n' = "snd (hd es)"
+ let ?es' = "tl es"
+ let ?e = "fst (hd es)"
+
+ from Suc have len: "length ?es' = l" by auto
+
+ from Suc
+ have [simp]: "end_node (n, es) = end_node (?n', ?es')"
+ by (cases es) (auto simp:end_node_def nth.simps split:nat.split)
+
+ from `has_fpath G (n,es)`
+ have "has_fpath G (?n', ?es')"
+ by (rule has_fpath.cases) (auto intro:has_fpath.intros)
+ with Suc len
+ have "has_edge (G ^ l) ?n' (prod (?n', ?es')) (end_node (?n', ?es'))"
+ by auto
+ moreover
+ from `es \<noteq> []`
+ have "prod (n, es) = ?e * (prod (?n', ?es'))"
+ by (cases es) auto
+ moreover
+ from `has_fpath G (n,es)` have c:"has_edge G n ?e ?n'"
+ by (rule has_fpath.cases) (insert `es \<noteq> []`, auto)
+
+ ultimately
+ show ?case
+ unfolding power_Suc
+ by (auto simp:in_grcomp)
+qed
+
+
+lemma path_acgpow:
+ "has_fpath G p
+ \<Longrightarrow> has_edge (G ^ length (snd p)) (fst p) (prod p) (end_node p)"
+by (cases p)
+ (rule path_acgpow_aux[of "snd p" "length (snd p)" _ "fst p", simplified])
+
+
+lemma star_paths:
+ "has_edge (star G) a x b =
+ (\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p)"
+proof
+ assume "has_edge (star G) a x b"
+ then obtain n where pow: "has_edge (G ^ n) a x b"
+ by (auto simp:in_star)
+
+ then obtain p where
+ "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
+ by (rule power_induces_path)
+
+ thus "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p"
+ by blast
+next
+ assume "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p"
+ then obtain p where
+ "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
+ by blast
+
+ hence "has_edge (G ^ length (snd p)) a x b"
+ by (auto intro:path_acgpow)
+
+ thus "has_edge (star G) a x b"
+ by (auto simp:in_star)
+qed
+
+
+lemma plus_paths:
+ "has_edge (tcl G) a x b =
+ (\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p \<and> 0 < length (snd p))"
+proof
+ assume "has_edge (tcl G) a x b"
+
+ then obtain n where pow: "has_edge (G ^ n) a x b" and "0 < n"
+ by (auto simp:in_tcl)
+
+ from pow obtain p where
+ "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
+ "n = length (snd p)"
+ by (rule power_induces_path)
+
+ with `0 < n`
+ 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) "
+ by blast
+next
+ assume "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p
+ \<and> 0 < length (snd p)"
+ then obtain p where
+ "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p"
+ "0 < length (snd p)"
+ by blast
+
+ hence "has_edge (G ^ length (snd p)) a x b"
+ by (auto intro:path_acgpow)
+
+ with `0 < length (snd p)`
+ show "has_edge (tcl G) a x b"
+ by (auto simp:in_tcl)
+qed
+
+
+definition
+ "contract s p =
+ (\<lambda>i. (fst (p (s i)), prod (p\<langle>s i,s (Suc i)\<rangle>)))"
+
+lemma ipath_contract:
+ assumes [simp]: "increasing s"
+ assumes ipath: "has_ipath G p"
+ shows "has_ipath (tcl G) (contract s p)"
+ unfolding has_ipath_def
+proof
+ fix i
+ let ?p = "p\<langle>s i,s (Suc i)\<rangle>"
+
+ from increasing_strict
+ have "fst (p (s (Suc i))) = end_node ?p" by simp
+ moreover
+ from increasing_strict[of s i "Suc i"] have "snd ?p \<noteq> []"
+ by (simp add:sub_path_def)
+ moreover
+ from ipath increasing_weak[of s] have "has_fpath G ?p"
+ by (rule sub_path_is_path) auto
+ ultimately
+ show "has_edge (tcl G)
+ (fst (contract s p i)) (snd (contract s p i)) (fst (contract s p (Suc i)))"
+ unfolding contract_def plus_paths
+ by (intro exI) auto
+qed
+
+lemma prod_unfold:
+ "i < j \<Longrightarrow> prod (p\<langle>i,j\<rangle>)
+ = snd (p i) * prod (p\<langle>Suc i, j\<rangle>)"
+ unfolding prod_def
+ by (simp add:sub_path_def upt_rec[of "i" j])
+
+
+lemma sub_path_loop:
+ assumes "0 < k"
+ assumes k:"k = length (snd loop)"
+ assumes loop: "fst loop = end_node loop"
+ shows "(omega loop)\<langle>k * i,k * Suc i\<rangle> = loop" (is "?\<omega> = loop")
+proof (rule prod_eqI)
+ show "fst ?\<omega> = fst loop"
+ by (auto simp:path_loop_def path_nth_def split_def k)
+
+ show "snd ?\<omega> = snd loop"
+ proof (rule nth_equalityI[rule_format])
+ show leneq: "length (snd ?\<omega>) = length (snd loop)"
+ unfolding sub_path_def k by simp
+
+ fix j assume "j < length (snd (?\<omega>))"
+ with leneq and k have "j < k" by simp
+
+ have a: "\<And>i. fst (path_nth loop (Suc i mod k))
+ = snd (snd (path_nth loop (i mod k)))"
+ unfolding k
+ apply (rule path_loop_connect[OF loop])
+ by (insert prems, auto)
+
+ from `j < k`
+ show "snd ?\<omega> ! j = snd loop ! j"
+ unfolding sub_path_def
+ apply (simp add:path_loop_def split_def add_ac)
+ apply (simp add:a k[symmetric])
+ by (simp add:path_nth_def)
+ qed
+qed
+
+
+
+
+
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Kleene_Algebras.thy Mon Feb 26 21:34:16 2007 +0100
@@ -0,0 +1,471 @@
+theory Kleene_Algebras
+imports Main
+begin
+
+text {* A type class of kleene algebras *}
+
+class star =
+ fixes star :: "'a \<Rightarrow> 'a"
+
+axclass idem_add \<subseteq> ab_semigroup_add
+ add_idem[simp]: "x + x = x"
+
+lemma add_idem2[simp]: "(x::'a::idem_add) + (x + y) = x + y"
+ unfolding add_assoc[symmetric]
+ by simp
+
+axclass order_by_add \<subseteq> idem_add, ord
+ order_def: "a \<le> b \<longleftrightarrow> a + b = b"
+ strict_order_def: "a < b \<longleftrightarrow> a \<le> b \<and> a \<noteq> b"
+
+lemma ord_simp1[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> x + y = y"
+ unfolding order_def .
+lemma ord_simp2[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> y + x = y"
+ unfolding order_def add_commute .
+lemma ord_intro: "(x::'a::order_by_add) + y = y \<Longrightarrow> x \<le> y"
+ unfolding order_def .
+
+instance order_by_add \<subseteq> order
+proof
+ fix x y z :: 'a
+ show "x \<le> x" unfolding order_def by simp
+
+ show "\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z"
+ proof (rule ord_intro)
+ assume "x \<le> y" "y \<le> z"
+
+ have "x + z = x + y + z" by (simp add:`y \<le> z` add_assoc)
+ also have "\<dots> = y + z" by (simp add:`x \<le> y`)
+ also have "\<dots> = z" by (simp add:`y \<le> z`)
+ finally show "x + z = z" .
+ qed
+
+ show "\<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" unfolding order_def
+ by (simp add:add_commute)
+ show "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y" by (fact strict_order_def)
+qed
+
+
+axclass pre_kleene \<subseteq> semiring_1, order_by_add
+
+instance pre_kleene \<subseteq> pordered_semiring
+proof
+ fix x y z :: 'a
+
+ assume "x \<le> y"
+
+ show "z + x \<le> z + y"
+ proof (rule ord_intro)
+ have "z + x + (z + y) = x + y + z" by (simp add:add_ac)
+ also have "\<dots> = z + y" by (simp add:`x \<le> y` add_ac)
+ finally show "z + x + (z + y) = z + y" .
+ qed
+
+ show "z * x \<le> z * y"
+ proof (rule ord_intro)
+ from `x \<le> y` have "z * (x + y) = z * y" by simp
+ thus "z * x + z * y = z * y" by (simp add:right_distrib)
+ qed
+
+ show "x * z \<le> y * z"
+ proof (rule ord_intro)
+ from `x \<le> y` have "(x + y) * z = y * z" by simp
+ thus "x * z + y * z = y * z" by (simp add:left_distrib)
+ qed
+qed
+
+axclass kleene \<subseteq> pre_kleene, star
+ star1: "1 + a * star a \<le> star a"
+ star2: "1 + star a * a \<le> star a"
+ star3: "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
+ star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
+
+axclass kleene_by_comp_lat \<subseteq>
+ pre_kleene, comp_lat, recpower, star
+
+ star_cont: "a * star b * c = (SUP n. a * b ^ n * c)"
+
+
+lemma plus_leI:
+ fixes x :: "'a :: order_by_add"
+ shows "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x + y \<le> z"
+ unfolding order_def by (simp add:add_assoc)
+
+
+
+
+lemma le_SUPI':
+ fixes l :: "'a :: comp_lat"
+ assumes "l \<le> M i"
+ shows "l \<le> (SUP i. M i)"
+ using prems
+ by (rule order_trans) (rule le_SUPI, rule refl)
+
+
+lemma zero_minimum[simp]: "(0::'a::pre_kleene) \<le> x"
+ unfolding order_def by simp
+
+instance kleene_by_comp_lat \<subseteq> kleene
+proof
+
+ fix a x :: 'a
+
+ have [simp]: "1 \<le> star a"
+ unfolding star_cont[of 1 a 1, simplified]
+ by (rule le_SUPI) (rule power_0[symmetric])
+
+ show "1 + a * star a \<le> star a"
+ apply (rule plus_leI, simp)
+ apply (simp add:star_cont[of a a 1, simplified])
+ apply (simp add:star_cont[of 1 a 1, simplified])
+ apply (intro SUP_leI le_SUPI)
+ by (rule power_Suc[symmetric])
+
+ show "1 + star a * a \<le> star a"
+ apply (rule plus_leI, simp)
+ apply (simp add:star_cont[of 1 a a, simplified])
+ apply (simp add:star_cont[of 1 a 1, simplified])
+ apply (intro SUP_leI le_SUPI)
+ by (simp add:power_Suc[symmetric] power_commutes)
+
+ show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
+ proof -
+ assume a: "a * x \<le> x"
+
+ {
+ fix n
+ have "a ^ (Suc n) * x \<le> a ^ n * x"
+ proof (induct n)
+ case 0 thus ?case by (simp add:a power_Suc)
+ next
+ case (Suc n)
+ hence "a * (a ^ Suc n * x) \<le> a * (a ^ n * x)"
+ by (auto intro: mult_mono)
+ thus ?case
+ by (simp add:power_Suc mult_assoc)
+ qed
+ }
+ note a = this
+
+ {
+ fix n have "a ^ n * x \<le> x"
+ proof (induct n)
+ case 0 show ?case by simp
+ next
+ case (Suc n) with a[of n]
+ show ?case by simp
+ qed
+ }
+ note b = this
+
+ show "star a * x \<le> x"
+ unfolding star_cont[of 1 a x, simplified]
+ by (rule SUP_leI) (rule b)
+ qed
+
+ show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *)
+ proof -
+ assume a: "x * a \<le> x"
+
+ {
+ fix n
+ have "x * a ^ (Suc n) \<le> x * a ^ n"
+ proof (induct n)
+ case 0 thus ?case by (simp add:a power_Suc)
+ next
+ case (Suc n)
+ hence "(x * a ^ Suc n) * a \<le> (x * a ^ n) * a"
+ by (auto intro: mult_mono)
+ thus ?case
+ by (simp add:power_Suc power_commutes mult_assoc)
+ qed
+ }
+ note a = this
+
+ {
+ fix n have "x * a ^ n \<le> x"
+ proof (induct n)
+ case 0 show ?case by simp
+ next
+ case (Suc n) with a[of n]
+ show ?case by simp
+ qed
+ }
+ note b = this
+
+ show "x * star a \<le> x"
+ unfolding star_cont[of x a 1, simplified]
+ by (rule SUP_leI) (rule b)
+ qed
+qed
+
+lemma less_add[simp]:
+ fixes a b :: "'a :: order_by_add"
+ shows "a \<le> a + b"
+ and "b \<le> a + b"
+ unfolding order_def
+ by (auto simp:add_ac)
+
+lemma add_est1:
+ fixes a b c :: "'a :: order_by_add"
+ assumes a: "a + b \<le> c"
+ shows "a \<le> c"
+ using less_add(1) a
+ by (rule order_trans)
+
+lemma add_est2:
+ fixes a b c :: "'a :: order_by_add"
+ assumes a: "a + b \<le> c"
+ shows "b \<le> c"
+ using less_add(2) a
+ by (rule order_trans)
+
+
+lemma star3':
+ fixes a b x :: "'a :: kleene"
+ assumes a: "b + a * x \<le> x"
+ shows "star a * b \<le> x"
+proof (rule order_trans)
+ from a have "b \<le> x" by (rule add_est1)
+ show "star a * b \<le> star a * x"
+ by (rule mult_mono) (auto simp:`b \<le> x`)
+
+ from a have "a * x \<le> x" by (rule add_est2)
+ with star3 show "star a * x \<le> x" .
+qed
+
+
+lemma star4':
+ fixes a b x :: "'a :: kleene"
+ assumes a: "b + x * a \<le> x"
+ shows "b * star a \<le> x"
+proof (rule order_trans)
+ from a have "b \<le> x" by (rule add_est1)
+ show "b * star a \<le> x * star a"
+ by (rule mult_mono) (auto simp:`b \<le> x`)
+
+ from a have "x * a \<le> x" by (rule add_est2)
+ with star4 show "x * star a \<le> x" .
+qed
+
+
+lemma star_mono:
+ fixes x y :: "'a :: kleene"
+ assumes "x \<le> y"
+ shows "star x \<le> star y"
+ oops
+
+lemma star_idemp:
+ fixes x :: "'a :: kleene"
+ shows "star (star x) = star x"
+ oops
+
+lemma zero_star[simp]:
+ shows "star (0::'a::kleene) = 1"
+ oops
+
+
+lemma star_unfold_left:
+ fixes a :: "'a :: kleene"
+ shows "1 + a * star a = star a"
+proof (rule order_antisym, rule star1)
+
+ have "1 + a * (1 + a * star a) \<le> 1 + a * star a"
+ apply (rule add_mono, rule)
+ apply (rule mult_mono, auto)
+ apply (rule star1)
+ done
+
+ with star3' have "star a * 1 \<le> 1 + a * star a" .
+ thus "star a \<le> 1 + a * star a" by simp
+qed
+
+
+lemma star_unfold_right:
+ fixes a :: "'a :: kleene"
+ shows "1 + star a * a = star a"
+proof (rule order_antisym, rule star2)
+
+ have "1 + (1 + star a * a) * a \<le> 1 + star a * a"
+ apply (rule add_mono, rule)
+ apply (rule mult_mono, auto)
+ apply (rule star2)
+ done
+
+ with star4' have "1 * star a \<le> 1 + star a * a" .
+ thus "star a \<le> 1 + star a * a" by simp
+qed
+
+
+
+lemma star_commute:
+ fixes a b x :: "'a :: kleene"
+ assumes a: "a * x = x * b"
+ shows "star a * x = x * star b"
+proof (rule order_antisym)
+
+ show "star a * x \<le> x * star b"
+ proof (rule star3', rule order_trans)
+
+ from a have "a * x \<le> x * b" by simp
+ hence "a * x * star b \<le> x * b * star b"
+ by (rule mult_mono) auto
+ thus "x + a * (x * star b) \<le> x + x * b * star b"
+ using add_mono by (auto simp: mult_assoc)
+
+ show "\<dots> \<le> x * star b"
+ proof -
+ have "x * (1 + b * star b) \<le> x * star b"
+ by (rule mult_mono[OF _ star1]) auto
+ thus ?thesis
+ by (simp add:right_distrib mult_assoc)
+ qed
+ qed
+
+ show "x * star b \<le> star a * x"
+ proof (rule star4', rule order_trans)
+
+ from a have b: "x * b \<le> a * x" by simp
+ have "star a * x * b \<le> star a * a * x"
+ unfolding mult_assoc
+ by (rule mult_mono[OF _ b]) auto
+ thus "x + star a * x * b \<le> x + star a * a * x"
+ using add_mono by auto
+
+ show "\<dots> \<le> star a * x"
+ proof -
+ have "(1 + star a * a) * x \<le> star a * x"
+ by (rule mult_mono[OF star2]) auto
+ thus ?thesis
+ by (simp add:left_distrib mult_assoc)
+ qed
+ qed
+qed
+
+
+
+lemma star_assoc:
+ fixes c d :: "'a :: kleene"
+ shows "star (c * d) * c = c * star (d * c)"
+ oops
+
+lemma star_dist:
+ fixes a b :: "'a :: kleene"
+ shows "star (a + b) = star a * star (b * star a)"
+ oops
+
+lemma star_one:
+ fixes a p p' :: "'a :: kleene"
+ assumes "p * p' = 1" and "p' * p = 1"
+ shows "p' * star a * p = star (p' * a * p)"
+ oops
+
+
+lemma star_zero:
+ "star (0::'a::kleene) = 1"
+ by (rule star_unfold_left[of 0, simplified])
+
+
+(* Own lemmas *)
+
+
+lemma x_less_star[simp]:
+ fixes x :: "'a :: kleene"
+ shows "x \<le> x * star a"
+proof -
+ have "x \<le> x * (1 + a * star a)" by (simp add:right_distrib)
+ also have "\<dots> = x * star a" by (simp only: star_unfold_left)
+ finally show ?thesis .
+qed
+
+subsection {* Transitive Closure *}
+
+definition
+ "tcl (x::'a::kleene) = star x * x"
+
+
+lemma tcl_zero:
+ "tcl (0::'a::kleene) = 0"
+ unfolding tcl_def by simp
+
+
+subsection {* Naive Algorithm to generate the transitive closure *}
+
+function (default "\<lambda>x. 0", tailrec)
+ mk_tcl :: "('a::{plus,times,ord,zero}) \<Rightarrow> 'a \<Rightarrow> 'a"
+where
+ "mk_tcl A X = (if X * A \<le> X then X else mk_tcl A (X + X * A))"
+ by pat_completeness simp
+
+declare mk_tcl.simps[simp del] (* loops *)
+
+lemma mk_tcl_code[code]:
+ "mk_tcl A X =
+ (let XA = X * A
+ in if XA \<le> X then X else mk_tcl A (X + XA))"
+ unfolding mk_tcl.simps[of A X] Let_def ..
+
+lemma mk_tcl_lemma1:
+ fixes X :: "'a :: kleene"
+ shows "(X + X * A) * star A = X * star A"
+proof -
+ have "A * star A \<le> 1 + A * star A" by simp
+ also have "\<dots> = star A" by (simp add:star_unfold_left)
+ finally have "star A + A * star A = star A" by simp
+ hence "X * (star A + A * star A) = X * star A" by simp
+ thus ?thesis by (simp add:left_distrib right_distrib mult_ac)
+qed
+
+lemma mk_tcl_lemma2:
+ fixes X :: "'a :: kleene"
+ shows "X * A \<le> X \<Longrightarrow> X * star A = X"
+ by (rule order_antisym) (auto simp:star4)
+
+
+
+
+lemma mk_tcl_correctness:
+ fixes A X :: "'a :: {kleene}"
+ assumes "mk_tcl_dom (A, X)"
+ shows "mk_tcl A X = X * star A"
+ using prems
+ by induct (auto simp:mk_tcl_lemma1 mk_tcl_lemma2)
+
+lemma graph_implies_dom: "mk_tcl_graph x y \<Longrightarrow> mk_tcl_dom x"
+ by (rule mk_tcl_graph.induct) (auto intro:accI elim:mk_tcl_rel.cases)
+
+lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
+ unfolding mk_tcl_def
+ by (rule fundef_default_value[OF mk_tcl_sum_def graph_implies_dom])
+
+
+text {* We can replace the dom-Condition of the correctness theorem
+ with something executable *}
+
+lemma mk_tcl_correctness2:
+ fixes A X :: "'a :: {kleene}"
+ assumes "mk_tcl A A \<noteq> 0"
+ shows "mk_tcl A A = tcl A"
+ using prems mk_tcl_default mk_tcl_correctness
+ unfolding tcl_def
+ by (auto simp:star_commute)
+
+
+
+
+
+end
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- a/src/HOL/Library/Library.thy Mon Feb 26 20:14:52 2007 +0100
+++ b/src/HOL/Library/Library.thy Mon Feb 26 21:34:16 2007 +0100
@@ -27,6 +27,7 @@
Quotient
Ramsey
State_Monad
+ Size_Change_Termination
While_Combinator
Word
Zorn
--- a/src/HOL/Library/Library/ROOT.ML Mon Feb 26 20:14:52 2007 +0100
+++ b/src/HOL/Library/Library/ROOT.ML Mon Feb 26 21:34:16 2007 +0100
@@ -3,3 +3,4 @@
use_thy "Library";
use_thy "List_Prefix";
use_thy "List_lexord";
+use_thy "SCT_Examples";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/SCT_Definition.thy Mon Feb 26 21:34:16 2007 +0100
@@ -0,0 +1,96 @@
+theory SCT_Definition
+imports Graphs Infinite_Set
+begin
+
+section {* Size-Change Graphs *}
+
+datatype sedge =
+ LESS ("\<down>")
+ | LEQ ("\<Down>")
+
+instance sedge :: times ..
+instance sedge :: one ..
+
+defs (overloaded)
+ one_sedge_def: "1 == \<Down>"
+ mult_sedge_def:" a * b == (if a = \<down> then \<down> else b)"
+
+instance sedge :: comm_monoid_mult
+proof
+ fix a b c :: sedge
+ show "a * b * c = a * (b * c)" by (simp add:mult_sedge_def)
+ show "1 * a = a" by (simp add:mult_sedge_def one_sedge_def)
+ show "a * b = b * a" unfolding mult_sedge_def
+ by (cases a, simp) (cases b, auto)
+qed
+
+instance sedge :: finite
+proof
+ have a: "UNIV = { LESS, LEQ }"
+ by auto (case_tac x, auto) (* FIXME *)
+ show "finite (UNIV::sedge set)"
+ by (simp add:a)
+qed
+
+
+types scg = "(nat, sedge) graph"
+types acg = "(nat, scg) graph"
+
+
+section {* Size-Change Termination *}
+
+abbreviation (input)
+ "desc P Q == ((\<exists>n.\<forall>i\<ge>n. P i) \<and> (\<exists>\<^sub>\<infinity>i. Q i))"
+
+abbreviation (input)
+ "dsc G i j \<equiv> has_edge G i LESS j"
+
+abbreviation (input)
+ "eq G i j \<equiv> has_edge G i LEQ j"
+
+abbreviation
+ eql :: "scg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+("_ \<turnstile> _ \<leadsto> _")
+where
+ "eql G i j \<equiv> has_edge G i LESS j \<or> has_edge G i LEQ j"
+
+
+abbreviation (input) descat :: "(nat, scg) ipath \<Rightarrow> nat sequence \<Rightarrow> nat \<Rightarrow> bool"
+where
+ "descat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))"
+
+abbreviation (input) eqat :: "(nat, scg) ipath \<Rightarrow> nat sequence \<Rightarrow> nat \<Rightarrow> bool"
+where
+ "eqat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i))"
+
+
+abbreviation eqlat :: "(nat, scg) ipath \<Rightarrow> nat sequence \<Rightarrow> nat \<Rightarrow> bool"
+where
+ "eqlat p \<theta> i \<equiv> (has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))
+ \<or> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i)))"
+
+
+definition is_desc_thread :: "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> bool"
+where
+ "is_desc_thread \<theta> p = ((\<exists>n.\<forall>i\<ge>n. eqlat p \<theta> i) \<and> (\<exists>\<^sub>\<infinity>i. descat p \<theta> i))"
+
+definition SCT :: "acg \<Rightarrow> bool"
+where
+ "SCT \<A> =
+ (\<forall>p. has_ipath \<A> p \<longrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> p))"
+
+
+
+definition no_bad_graphs :: "acg \<Rightarrow> bool"
+where
+ "no_bad_graphs A =
+ (\<forall>n G. has_edge A n G n \<and> G * G = G
+ \<longrightarrow> (\<exists>p. has_edge G p LESS p))"
+
+
+definition SCT' :: "acg \<Rightarrow> bool"
+where
+ "SCT' A = no_bad_graphs (tcl A)"
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/SCT_Examples.thy Mon Feb 26 21:34:16 2007 +0100
@@ -0,0 +1,83 @@
+theory SCT_Examples
+imports Size_Change_Termination
+begin
+
+
+
+function f :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "f n 0 = n"
+| "f 0 (Suc m) = f (Suc m) m"
+| "f (Suc n) (Suc m) = f m n"
+by pat_completeness auto
+
+
+termination
+ unfolding f_rel_def lfp_const
+ apply (rule SCT_on_relations)
+ apply (tactic "SCT.abs_rel_tac") (* Build call descriptors *)
+ apply (rule ext, rule ext, simp) (* Show that they are correct *)
+ apply (tactic "SCT.mk_call_graph") (* Build control graph *)
+ apply (rule LJA_apply) (* Apply main theorem *)
+ apply (simp add:finite_acg_ins finite_acg_empty) (* show finiteness *)
+ apply (rule SCT'_exec)
+ by eval (* Evaluate to true *)
+
+
+function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "p m n r = (if r>0 then p m (r - 1) n else
+ if n>0 then p r (n - 1) m
+ else m)"
+by pat_completeness auto
+
+termination
+ unfolding p_rel_def lfp_const
+ apply (rule SCT_on_relations)
+ apply (tactic "SCT.abs_rel_tac")
+ apply (rule ext, rule ext, simp)
+ apply (tactic "SCT.mk_call_graph")
+ apply (rule LJA_apply)
+ apply (simp add:finite_acg_ins finite_acg_empty)
+ apply (rule SCT'_exec)
+ by eval
+
+function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "foo True (Suc n) m = foo True n (Suc m)"
+ "foo True 0 m = foo False 0 m"
+ "foo False n (Suc m) = foo False (Suc n) m"
+ "foo False n 0 = n"
+by pat_completeness auto
+
+termination
+ unfolding foo_rel_def lfp_const
+ apply (rule SCT_on_relations)
+ apply (tactic "SCT.abs_rel_tac")
+ apply (rule ext, rule ext, simp)
+ apply (tactic "SCT.mk_call_graph")
+ apply (rule LJA_apply)
+ apply (simp add:finite_acg_ins finite_acg_empty)
+ apply (rule SCT'_exec)
+ by eval
+
+
+function (sequential)
+ bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "bar 0 (Suc n) m = bar m m m"
+| "bar k n m = 0"
+by pat_completeness auto
+
+termination
+ unfolding bar_rel_def lfp_const
+ apply (rule SCT_on_relations)
+ apply (tactic "SCT.abs_rel_tac")
+ apply (rule ext, rule ext, simp)
+ apply (tactic "SCT.mk_call_graph")
+ apply (rule LJA_apply)
+ apply (simp add:finite_acg_ins finite_acg_empty)
+ by (rule SCT'_empty)
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/SCT_Implementation.thy Mon Feb 26 21:34:16 2007 +0100
@@ -0,0 +1,126 @@
+theory SCT_Implementation
+imports ExecutableSet SCT_Definition
+begin
+
+fun edges_match :: "('n \<times> 'e \<times> 'n) \<times> ('n \<times> 'e \<times> 'n) \<Rightarrow> bool"
+where
+ "edges_match ((n, e, m), (n',e',m')) = (m = n')"
+
+fun connect_edges ::
+ "('n \<times> ('e::times) \<times> 'n) \<times> ('n \<times> 'e \<times> 'n)
+ \<Rightarrow> ('n \<times> 'e \<times> 'n)"
+where
+ "connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')"
+
+lemma grcomp_code[code]:
+ "grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })"
+ by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def)
+
+
+definition test_SCT :: "acg \<Rightarrow> bool"
+where
+ "test_SCT \<A> =
+ (let \<T> = mk_tcl \<A> \<A>
+ in (\<T> \<noteq> 0 \<and>
+ (\<forall>(n,G,m)\<in>dest_graph \<T>.
+ n \<noteq> m \<or> G * G \<noteq> G \<or>
+ (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS))))"
+
+
+lemma SCT'_exec:
+ assumes a: "test_SCT \<A>"
+ shows "SCT' \<A>"
+proof -
+ from mk_tcl_correctness2 a
+ have "mk_tcl \<A> \<A> = tcl \<A>"
+ unfolding test_SCT_def Let_def by auto
+
+ with a
+ show ?thesis
+ unfolding SCT'_def no_bad_graphs_def test_SCT_def Let_def has_edge_def
+ by auto
+qed
+
+code_modulename SML
+ Implementation Graphs
+
+lemma [code func]:
+ "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
+ "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
+ unfolding graph_leq_def graph_less_def by rule+
+
+lemma [code func]:
+ "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)"
+ unfolding graph_plus_def ..
+
+lemma [code func]:
+ "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H"
+ unfolding graph_mult_def ..
+
+
+
+lemma SCT'_empty: "SCT' (Graph {})"
+ unfolding SCT'_def no_bad_graphs_def graph_zero_def[symmetric]
+ tcl_zero
+ by (simp add:in_grzero)
+
+
+
+subsection {* Witness checking *}
+
+
+definition test_SCT_witness :: "acg \<Rightarrow> acg \<Rightarrow> bool"
+where
+ "test_SCT_witness A T =
+ (A \<le> T \<and> A * T \<le> T \<and>
+ (\<forall>(n,G,m)\<in>dest_graph T.
+ n \<noteq> m \<or> G * G \<noteq> G \<or>
+ (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
+
+
+lemma no_bad_graphs_ucl:
+ assumes "A \<le> B"
+ assumes "no_bad_graphs B"
+ shows "no_bad_graphs A"
+using prems
+unfolding no_bad_graphs_def has_edge_def graph_leq_def
+by blast
+
+
+
+lemma SCT'_witness:
+ assumes a: "test_SCT_witness A T"
+ shows "SCT' A"
+proof -
+ from a have "A \<le> T" "A * T \<le> T" by (auto simp:test_SCT_witness_def)
+ hence "A + A * T \<le> T"
+ by (subst add_idem[of T, symmetric], rule add_mono)
+ with star3' have "tcl A \<le> T" unfolding tcl_def .
+ moreover
+ from a have "no_bad_graphs T"
+ unfolding no_bad_graphs_def test_SCT_witness_def has_edge_def
+ by auto
+ ultimately
+ show ?thesis
+ unfolding SCT'_def
+ by (rule no_bad_graphs_ucl)
+qed
+
+
+code_modulename SML
+ Graphs SCT
+ Kleene_Algebras SCT
+ SCT_Implementation SCT
+
+code_gen test_SCT (SML -)
+
+
+end
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/SCT_Interpretation.thy Mon Feb 26 21:34:16 2007 +0100
@@ -0,0 +1,413 @@
+theory SCT_Interpretation
+imports Main SCT_Misc SCT_Definition
+begin
+
+
+definition
+ "idseq R s x = (s 0 = x \<and> (\<forall>i. R (s (Suc i)) (s i)))"
+
+lemma not_acc_smaller:
+ assumes notacc: "\<not> acc R x"
+ shows "\<exists>y. R y x \<and> \<not> acc R y"
+proof (rule classical)
+ assume "\<not> ?thesis"
+ hence "\<And>y. R y x \<Longrightarrow> acc R y" by blast
+ with accI have "acc R x" .
+ with notacc show ?thesis by contradiction
+qed
+
+lemma non_acc_has_idseq:
+ assumes "\<not> acc R x"
+ shows "\<exists>s. idseq R s x"
+proof -
+
+ have "\<exists>f. \<forall>x. \<not>acc R x \<longrightarrow> R (f x) x \<and> \<not>acc R (f x)"
+ by (rule choice, auto simp:not_acc_smaller)
+
+ then obtain f where
+ in_R: "\<And>x. \<not>acc R x \<Longrightarrow> R (f x) x"
+ and nia: "\<And>x. \<not>acc R x \<Longrightarrow> \<not>acc R (f x)"
+ by blast
+
+ let ?s = "\<lambda>i. (f ^ i) x"
+
+ {
+ fix i
+ have "\<not>acc R (?s i)"
+ by (induct i) (auto simp:nia `\<not>acc R x`)
+ hence "R (f (?s i)) (?s i)"
+ by (rule in_R)
+ }
+
+ hence "idseq R ?s x"
+ unfolding idseq_def
+ by auto
+
+ thus ?thesis by auto
+qed
+
+
+
+
+
+types ('a, 'q) cdesc =
+ "('q \<Rightarrow> bool) \<times> ('q \<Rightarrow> 'a) \<times>('q \<Rightarrow> 'a)"
+
+
+fun in_cdesc :: "('a, 'q) cdesc \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ "in_cdesc (\<Gamma>, r, l) x y = (\<exists>q. x = r q \<and> y = l q \<and> \<Gamma> q)"
+
+fun mk_rel :: "('a, 'q) cdesc list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ "mk_rel [] x y = False"
+ "mk_rel (c#cs) x y =
+ (in_cdesc c x y \<or> mk_rel cs x y)"
+
+
+lemma some_rd:
+ assumes "mk_rel rds x y"
+ shows "\<exists>rd\<in>set rds. in_cdesc rd x y"
+ using prems
+ by (induct rds) (auto simp:in_cdesc_def)
+
+(* from a value sequence, get a sequence of rds *)
+
+lemma ex_cs:
+ assumes idseq: "idseq (mk_rel rds) s x"
+ shows "\<exists>cs. \<forall>i. cs i \<in> set rds \<and> in_cdesc (cs i) (s (Suc i)) (s i)"
+proof -
+ from idseq
+ have a: "\<forall>i. \<exists>rd \<in> set rds. in_cdesc rd (s (Suc i)) (s i)"
+ by (auto simp:idseq_def intro:some_rd)
+
+ show ?thesis
+ by (rule choice) (insert a, blast)
+qed
+
+
+
+types ('q, 'a) interpr = "('a, 'q) cdesc \<times> (nat \<Rightarrow> 'a \<Rightarrow> nat)"
+types 'a measures = "nat \<Rightarrow> 'a \<Rightarrow> nat"
+
+
+fun stepP :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow>
+ ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> bool"
+where
+ "stepP (\<Gamma>1,r1,l1) (\<Gamma>2,r2,l2) m1 m2 R
+ = (\<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> R (m2 (l2 q\<^isub>2)) ((m1 (l1 q\<^isub>1))))"
+
+
+definition
+ decr :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow>
+ ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
+where
+ "decr c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op <)"
+
+definition
+ decreq :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow>
+ ('a \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
+where
+ "decreq c1 c2 m1 m2 = stepP c1 c2 m1 m2 (op \<le>)"
+
+definition
+ no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool"
+where
+ "no_step c1 c2 = stepP c1 c2 (\<lambda>x. 0) (\<lambda>x. 0) (\<lambda>x y. False)"
+
+
+
+lemma decr_in_cdesc:
+ assumes "in_cdesc RD1 y x"
+ assumes "in_cdesc RD2 z y"
+ assumes "decr RD1 RD2 m1 m2"
+ shows "m2 y < m1 x"
+ using prems
+ by (cases RD1, cases RD2, auto simp:decr_def)
+
+lemma decreq_in_cdesc:
+ assumes "in_cdesc RD1 y x"
+ assumes "in_cdesc RD2 z y"
+ assumes "decreq RD1 RD2 m1 m2"
+ shows "m2 y \<le> m1 x"
+ using prems
+ by (cases RD1, cases RD2, auto simp:decreq_def)
+
+
+lemma no_inf_desc_nat_sequence:
+ fixes s :: "nat \<Rightarrow> nat"
+ assumes leq: "\<And>i. n \<le> i \<Longrightarrow> s (Suc i) \<le> s i"
+ assumes less: "\<exists>\<^sub>\<infinity>i. s (Suc i) < s i"
+ shows False
+proof -
+ {
+ fix i j:: nat
+ assume "n \<le> i"
+ assume "i \<le> j"
+ {
+ fix k
+ have "s (i + k) \<le> s i"
+ proof (induct k)
+ case 0 thus ?case by simp
+ next
+ case (Suc k)
+ with leq[of "i + k"] `n \<le> i`
+ show ?case by simp
+ qed
+ }
+ from this[of "j - i"] `n \<le> i` `i \<le> j`
+ have "s j \<le> s i" by auto
+ }
+ note decr = this
+
+ let ?min = "LEAST x. x \<in> range (\<lambda>i. s (n + i))"
+ have "?min \<in> range (\<lambda>i. s (n + i))"
+ by (rule LeastI) auto
+ then obtain k where min: "?min = s (n + k)" by auto
+
+ from less
+ obtain k' where "n + k < k'"
+ and "s (Suc k') < s k'"
+ unfolding INF_nat by auto
+
+ with decr[of "n + k" k'] min
+ have "s (Suc k') < ?min" by auto
+ moreover from `n + k < k'`
+ have "s (Suc k') = s (n + (Suc k' - n))" by simp
+ ultimately
+ show False using not_less_Least by blast
+qed
+
+
+
+definition
+ approx :: "scg \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc
+ \<Rightarrow> 'a measures \<Rightarrow> 'a measures \<Rightarrow> bool"
+ where
+ "approx G C C' M M'
+ = (\<forall>i j. (dsc G i j \<longrightarrow> decr C C' (M i) (M' j))
+ \<and>(eq G i j \<longrightarrow> decreq C C' (M i) (M' j)))"
+
+
+
+
+(* Unfolding "approx" for finite graphs *)
+
+lemma approx_empty:
+ "approx (Graph {}) c1 c2 ms1 ms2"
+ unfolding approx_def has_edge_def dest_graph.simps by simp
+
+lemma approx_less:
+ assumes "stepP c1 c2 (ms1 i) (ms2 j) (op <)"
+ assumes "approx (Graph Es) c1 c2 ms1 ms2"
+ shows "approx (Graph (insert (i, \<down>, j) Es)) c1 c2 ms1 ms2"
+ using prems
+ unfolding approx_def has_edge_def dest_graph.simps decr_def
+ by auto
+
+lemma approx_leq:
+ assumes "stepP c1 c2 (ms1 i) (ms2 j) (op \<le>)"
+ assumes "approx (Graph Es) c1 c2 ms1 ms2"
+ shows "approx (Graph (insert (i, \<Down>, j) Es)) c1 c2 ms1 ms2"
+ using prems
+ unfolding approx_def has_edge_def dest_graph.simps decreq_def
+ by auto
+
+
+lemma "approx (Graph {(1, \<down>, 2),(2, \<Down>, 3)}) c1 c2 ms1 ms2"
+ apply (intro approx_less approx_leq approx_empty)
+ oops
+
+
+(*
+fun
+ no_step :: "('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> bool"
+where
+ "no_step (\<Gamma>1, r1, l1) (\<Gamma>2, r2, l2) =
+ (\<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)"
+*)
+
+lemma no_stepI:
+ "stepP c1 c2 m1 m2 (\<lambda>x y. False)
+ \<Longrightarrow> no_step c1 c2"
+by (cases c1, cases c2) (auto simp: no_step_def)
+
+definition
+ sound_int :: "acg \<Rightarrow> ('a, 'q) cdesc list
+ \<Rightarrow> 'a measures list \<Rightarrow> bool"
+where
+ "sound_int \<A> RDs M =
+ (\<forall>n<length RDs. \<forall>m<length RDs.
+ no_step (RDs ! n) (RDs ! m) \<or>
+ (\<exists>G. (\<A> \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m) \<and> approx G (RDs ! n) (RDs ! m) (M ! n) (M ! m)))"
+
+
+(* The following are uses by the tactics *)
+lemma length_simps: "length [] = 0" "length (x#xs) = Suc (length xs)"
+ by auto
+
+lemma all_less_zero: "\<forall>n<(0::nat). P n"
+ by simp
+
+lemma all_less_Suc:
+ assumes Pk: "P k"
+ assumes Pn: "\<forall>n<k. P n"
+ shows "\<forall>n<Suc k. P n"
+proof (intro allI impI)
+ fix n assume "n < Suc k"
+ show "P n"
+ proof (cases "n < k")
+ case True with Pn show ?thesis by simp
+ next
+ case False with `n < Suc k` have "n = k" by simp
+ with Pk show ?thesis by simp
+ qed
+qed
+
+
+lemma step_witness:
+ assumes "in_cdesc RD1 y x"
+ assumes "in_cdesc RD2 z y"
+ shows "\<not> no_step RD1 RD2"
+ using prems
+ by (cases RD1, cases RD2) (auto simp:no_step_def)
+
+
+theorem SCT_on_relations:
+ assumes R: "R = mk_rel RDs"
+ assumes sound: "sound_int \<A> RDs M"
+ assumes "SCT \<A>"
+ shows "\<forall>x. acc R x"
+proof (rule, rule classical)
+ fix x
+ assume "\<not> acc R x"
+ with non_acc_has_idseq
+ have "\<exists>s. idseq R s x" .
+ then obtain s where "idseq R s x" ..
+ hence "\<exists>cs. \<forall>i. cs i \<in> set RDs \<and>
+ in_cdesc (cs i) (s (Suc i)) (s i)"
+ unfolding R by (rule ex_cs)
+ then obtain cs where
+ [simp]: "\<And>i. cs i \<in> set RDs"
+ and ird[simp]: "\<And>i. in_cdesc (cs i) (s (Suc i)) (s i)"
+ by blast
+
+ let ?cis = "\<lambda>i. index_of RDs (cs i)"
+ have "\<forall>i. \<exists>G. (\<A> \<turnstile> ?cis i \<leadsto>\<^bsup>G\<^esup> (?cis (Suc i)))
+ \<and> approx G (RDs ! ?cis i) (RDs ! ?cis (Suc i))
+ (M ! ?cis i) (M ! ?cis (Suc i))" (is "\<forall>i. \<exists>G. ?P i G")
+ proof
+ fix i
+ let ?n = "?cis i" and ?n' = "?cis (Suc i)"
+
+ have "in_cdesc (RDs ! ?n) (s (Suc i)) (s i)"
+ "in_cdesc (RDs ! ?n') (s (Suc (Suc i))) (s (Suc i))"
+ by (simp_all add:index_of_member)
+ with step_witness
+ have "\<not> no_step (RDs ! ?n) (RDs ! ?n')" .
+ moreover have
+ "?n < length RDs"
+ "?n' < length RDs"
+ by (simp_all add:index_of_length[symmetric])
+ ultimately
+ obtain G
+ where "\<A> \<turnstile> ?n \<leadsto>\<^bsup>G\<^esup> ?n'"
+ and "approx G (RDs ! ?n) (RDs ! ?n') (M ! ?n) (M ! ?n')"
+ using sound
+ unfolding sound_int_def by auto
+
+ thus "\<exists>G. ?P i G" by blast
+ qed
+ with choice
+ have "\<exists>Gs. \<forall>i. ?P i (Gs i)" .
+ then obtain Gs where
+ A: "\<And>i. \<A> \<turnstile> ?cis i \<leadsto>\<^bsup>(Gs i)\<^esup> (?cis (Suc i))"
+ and B: "\<And>i. approx (Gs i) (RDs ! ?cis i) (RDs ! ?cis (Suc i))
+ (M ! ?cis i) (M ! ?cis (Suc i))"
+ by blast
+
+ let ?p = "\<lambda>i. (?cis i, Gs i)"
+
+ from A have "has_ipath \<A> ?p"
+ unfolding has_ipath_def
+ by auto
+
+ with `SCT \<A>` SCT_def
+ obtain th where "is_desc_thread th ?p"
+ by auto
+
+ then obtain n
+ where fr: "\<forall>i\<ge>n. eqlat ?p th i"
+ and inf: "\<exists>\<^sub>\<infinity>i. descat ?p th i"
+ unfolding is_desc_thread_def by auto
+
+ from B
+ have approx:
+ "\<And>i. approx (Gs i) (cs i) (cs (Suc i))
+ (M ! ?cis i) (M ! ?cis (Suc i))"
+ by (simp add:index_of_member)
+
+ let ?seq = "\<lambda>i. (M ! ?cis i) (th i) (s i)"
+
+ have "\<And>i. n < i \<Longrightarrow> ?seq (Suc i) \<le> ?seq i"
+ proof -
+ fix i
+ let ?q1 = "th i" and ?q2 = "th (Suc i)"
+ assume "n < i"
+
+ with fr have "eqlat ?p th i" by simp
+ hence "dsc (Gs i) ?q1 ?q2 \<or> eq (Gs i) ?q1 ?q2"
+ by simp
+ thus "?seq (Suc i) \<le> ?seq i"
+ proof
+ assume "dsc (Gs i) ?q1 ?q2"
+
+ with approx
+ have a:"decr (cs i) (cs (Suc i))
+ ((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)"
+ unfolding approx_def by auto
+
+ show ?thesis
+ apply (rule less_imp_le)
+ apply (rule decr_in_cdesc[of _ "s (Suc i)" "s i"])
+ by (rule ird a)+
+ next
+ assume "eq (Gs i) ?q1 ?q2"
+
+ with approx
+ have a:"decreq (cs i) (cs (Suc i))
+ ((M ! ?cis i) ?q1) ((M ! ?cis (Suc i)) ?q2)"
+ unfolding approx_def by auto
+
+ show ?thesis
+ apply (rule decreq_in_cdesc[of _ "s (Suc i)" "s i"])
+ by (rule ird a)+
+ qed
+ qed
+ moreover have "\<exists>\<^sub>\<infinity>i. ?seq (Suc i) < ?seq i" unfolding INF_nat
+ proof
+ fix i
+ from inf obtain j where "i < j" and d: "descat ?p th j"
+ unfolding INF_nat by auto
+ let ?q1 = "th j" and ?q2 = "th (Suc j)"
+ from d have "dsc (Gs j) ?q1 ?q2" by auto
+
+ with approx
+ have a:"decr (cs j) (cs (Suc j))
+ ((M ! ?cis j) ?q1) ((M ! ?cis (Suc j)) ?q2)"
+ unfolding approx_def by auto
+
+ have "?seq (Suc j) < ?seq j"
+ apply (rule decr_in_cdesc[of _ "s (Suc j)" "s j"])
+ by (rule ird a)+
+ with `i < j`
+ show "\<exists>j. i < j \<and> ?seq (Suc j) < ?seq j" by auto
+ qed
+ ultimately have False
+ by (rule no_inf_desc_nat_sequence[of "Suc n"]) simp
+ thus "acc R x" ..
+qed
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/SCT_Misc.thy Mon Feb 26 21:34:16 2007 +0100
@@ -0,0 +1,206 @@
+theory SCT_Misc
+imports Main
+begin
+
+
+subsection {* Searching in lists *}
+
+fun index_of :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
+where
+ "index_of [] c = 0"
+| "index_of (x#xs) c = (if x = c then 0 else Suc (index_of xs c))"
+
+lemma index_of_member:
+ "(x \<in> set l) \<Longrightarrow> (l ! index_of l x = x)"
+ by (induct l) auto
+
+lemma index_of_length:
+ "(x \<in> set l) = (index_of l x < length l)"
+ by (induct l) auto
+
+
+
+subsection {* Some reasoning tools *}
+
+lemma inc_induct[consumes 1]:
+ assumes less: "i \<le> j"
+ assumes base: "P j"
+ assumes step: "\<And>i. \<lbrakk>i < j; P (Suc i)\<rbrakk> \<Longrightarrow> P i"
+ shows "P i"
+ using less
+proof (induct d\<equiv>"j - i" arbitrary: i)
+ case (0 i)
+ with `i \<le> j` have "i = j" by simp
+ with base show ?case by simp
+next
+ case (Suc d i)
+ hence "i < j" "P (Suc i)"
+ by simp_all
+ thus "P i" by (rule step)
+qed
+
+lemma strict_inc_induct[consumes 1]:
+ assumes less: "i < j"
+ assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i"
+ assumes step: "\<And>i. \<lbrakk>i < j; P (Suc i)\<rbrakk> \<Longrightarrow> P i"
+ shows "P i"
+ using less
+proof (induct d\<equiv>"j - i - 1" arbitrary: i)
+ case (0 i)
+ with `i < j` have "j = Suc i" by simp
+ with base show ?case by simp
+next
+ case (Suc d i)
+ hence "i < j" "P (Suc i)"
+ by simp_all
+ thus "P i" by (rule step)
+qed
+
+
+lemma three_cases:
+ assumes "a1 \<Longrightarrow> thesis"
+ assumes "a2 \<Longrightarrow> thesis"
+ assumes "a3 \<Longrightarrow> thesis"
+ assumes "\<And>R. \<lbrakk>a1 \<Longrightarrow> R; a2 \<Longrightarrow> R; a3 \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ shows "thesis"
+ using prems
+ by auto
+
+
+section {* Sequences *}
+
+types
+ 'a sequence = "nat \<Rightarrow> 'a"
+
+subsection {* Increasing sequences *}
+
+definition increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
+where
+ "increasing s = (\<forall>i j. i < j \<longrightarrow> s i < s j)"
+
+lemma increasing_strict:
+ assumes "increasing s"
+ assumes "i < j"
+ shows "s i < s j"
+ using prems
+ unfolding increasing_def by simp
+
+lemma increasing_weak:
+ assumes "increasing s"
+ assumes "i \<le> j"
+ shows "s i \<le> s j"
+ using prems increasing_strict[of s i j]
+ by (cases "i<j") auto
+
+lemma increasing_inc:
+ assumes [simp]: "increasing s"
+ shows "n \<le> s n"
+proof (induct n)
+ case (Suc n)
+ with increasing_strict[of s n "Suc n"]
+ show ?case by auto
+qed auto
+
+
+lemma increasing_bij:
+ assumes [simp]: "increasing s"
+ shows "(s i < s j) = (i < j)"
+proof
+ assume "s i < s j"
+ show "i < j"
+ proof (rule classical)
+ assume "\<not> ?thesis"
+ hence "j \<le> i" by arith
+ with increasing_weak have "s j \<le> s i" by simp
+ with `s i < s j` show ?thesis by simp
+ qed
+qed (simp add:increasing_strict)
+
+
+
+
+subsection {* Sections induced by an increasing sequence *}
+
+abbreviation
+ "section s i == {s i ..< s (Suc i)}"
+
+definition
+ "section_of s n = (LEAST i. n < s (Suc i))"
+
+
+lemma section_help:
+ assumes [intro, simp]: "increasing s"
+ shows "\<exists>i. n < s (Suc i)"
+proof -
+ from increasing_inc have "n \<le> s n" .
+ also from increasing_strict have "\<dots> < s (Suc n)" by simp
+ finally show ?thesis ..
+qed
+
+lemma section_of2:
+ assumes "increasing s"
+ shows "n < s (Suc (section_of s n))"
+ unfolding section_of_def
+ by (rule LeastI_ex) (rule section_help)
+
+
+lemma section_of1:
+ assumes [simp, intro]: "increasing s"
+ assumes "s i \<le> n"
+ shows "s (section_of s n) \<le> n"
+proof (rule classical)
+ let ?m = "section_of s n"
+
+ assume "\<not> ?thesis"
+ hence a: "n < s ?m" by simp
+
+ have nonzero: "?m \<noteq> 0"
+ proof
+ assume "?m = 0"
+ from increasing_weak have "s 0 \<le> s i" by simp
+ also note `\<dots> \<le> n`
+ finally show False using `?m = 0` `n < s ?m` by simp
+ qed
+ with a have "n < s (Suc (?m - 1))" by simp
+ with Least_le have "?m \<le> ?m - 1"
+ unfolding section_of_def .
+ with nonzero show ?thesis by simp
+qed
+
+lemma section_of_known:
+ assumes [simp]: "increasing s"
+ assumes in_sect: "k \<in> section s i"
+ shows "section_of s k = i" (is "?s = i")
+proof (rule classical)
+ assume "\<not> ?thesis"
+
+ hence "?s < i \<or> ?s > i" by arith
+ thus ?thesis
+ proof
+ assume "?s < i"
+ hence "Suc ?s \<le> i" by simp
+ with increasing_weak have "s (Suc ?s) \<le> s i" by simp
+ moreover have "k < s (Suc ?s)" using section_of2 by simp
+ moreover from in_sect have "s i \<le> k" by simp
+ ultimately show ?thesis by simp
+ next
+ assume "i < ?s" hence "Suc i \<le> ?s" by simp
+ with increasing_weak have "s (Suc i) \<le> s ?s" by simp
+ moreover
+ from in_sect have "s i \<le> k" by simp
+ with section_of1 have "s ?s \<le> k" by simp
+ moreover from in_sect have "k < s (Suc i)" by simp
+ ultimately show ?thesis by simp
+ qed
+qed
+
+
+lemma in_section_of:
+ assumes [simp, intro]: "increasing s"
+ assumes "s i \<le> k"
+ shows "k \<in> section s (section_of s k)"
+ using prems
+ by (auto intro:section_of1 section_of2)
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/SCT_Theorem.thy Mon Feb 26 21:34:16 2007 +0100
@@ -0,0 +1,1416 @@
+theory SCT_Theorem
+imports Main Ramsey SCT_Misc SCT_Definition
+begin
+
+
+section {* The size change criterion SCT *}
+
+
+definition is_thread :: "nat \<Rightarrow> nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> bool"
+where
+ "is_thread n \<theta> p = (\<forall>i\<ge>n. eqlat p \<theta> i)"
+
+definition is_fthread ::
+ "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+where
+ "is_fthread \<theta> mp i j = (\<forall>k\<in>{i..<j}. eqlat mp \<theta> k)"
+
+definition is_desc_fthread ::
+ "nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+where
+ "is_desc_fthread \<theta> mp i j =
+ (is_fthread \<theta> mp i j \<and>
+ (\<exists>k\<in>{i..<j}. descat mp \<theta> k))"
+
+definition
+ "has_fth p i j n m =
+ (\<exists>\<theta>. is_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
+
+definition
+ "has_desc_fth p i j n m =
+ (\<exists>\<theta>. is_desc_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
+
+
+
+section {* Bounded graphs and threads *}
+
+definition
+ "bounded_scg (P::nat) (G::scg) =
+ (\<forall>p e p'. has_edge G p e p' \<longrightarrow> p < P \<and> p' < P)"
+
+definition
+ "bounded_acg P ACG =
+ (\<forall>n G n'. has_edge ACG n G n' \<longrightarrow> n < P \<and> n' < P \<and> bounded_scg P G)"
+
+definition
+ "bounded_mp P mp = (\<forall>i. bounded_scg P (snd (mp i)))"
+
+definition (* = finite (range \<theta>) *)
+ "bounded_th (P::nat) n \<theta> = (\<forall>i>n. \<theta> i < P)"
+
+
+definition
+ "finite_scg (G::scg) = (\<exists>P. bounded_scg P G)"
+
+definition
+ "finite_acg (A::acg) = (\<exists>P. bounded_acg P A)"
+
+
+lemma "finite (insert x A) = finite A"
+by simp
+
+
+lemma finite_scg_finite[simp]: "finite_scg (Graph G) = finite G"
+proof
+ assume "finite_scg (Graph G)"
+ thm bounded_scg_def
+
+ then obtain P where bounded: "bounded_scg P (Graph G)"
+ by (auto simp:finite_scg_def)
+
+ show "finite G"
+ proof (rule finite_subset)
+ from bounded
+ show "G \<subseteq> {0 .. P - 1} \<times> { LESS, LEQ } \<times> { 0 .. P - 1}"
+ apply (auto simp:bounded_scg_def has_edge_def)
+ apply force
+ apply (case_tac "aa", auto)
+ apply force
+ done
+
+ show "finite \<dots>"
+ by (auto intro: finite_cartesian_product finite_atLeastAtMost)
+ qed
+next
+
+ assume "finite G"
+ thus "finite_scg (Graph G)"
+ proof induct
+ show "finite_scg (Graph {})"
+ unfolding finite_scg_def bounded_scg_def has_edge_def by auto
+ next
+ fix x G
+ assume "finite G" "x \<notin> G" "finite_scg (Graph G)"
+ then obtain P
+ where bG: "bounded_scg P (Graph G)"
+ by (auto simp:finite_scg_def)
+
+ obtain p e p' where x: "x = (p, e, p')" by (cases x, auto)
+
+ let ?Q = "max P (max (Suc p) (Suc p'))"
+ have "P \<le> ?Q" "Suc p \<le> ?Q" "Suc p' \<le> ?Q" by auto
+ with bG
+ have "bounded_scg ?Q (Graph (insert x G))"
+ unfolding x bounded_scg_def has_edge_def
+ apply simp
+ apply (intro allI, elim allE)
+ by auto
+ thus "finite_scg (Graph (insert x G))"
+ by (auto simp:finite_scg_def)
+ qed
+qed
+
+
+lemma finite_acg_empty:
+ "finite_acg (Graph {})"
+unfolding finite_acg_def bounded_acg_def has_edge_def
+by auto
+
+
+
+lemma bounded_scg_up: "bounded_scg P G \<Longrightarrow> P \<le> Q \<Longrightarrow> bounded_scg Q G"
+ unfolding bounded_scg_def
+ by force
+
+
+lemma bounded_up: "bounded_acg P G \<Longrightarrow> P \<le> Q \<Longrightarrow> bounded_acg Q G"
+ unfolding bounded_acg_def
+ apply auto
+ apply force+
+ apply (rule bounded_scg_up)
+ by auto
+
+lemma bacg_insert:
+ assumes "bounded_acg P (Graph A)"
+ assumes "n < P" "m < P" "bounded_scg P G"
+ shows "bounded_acg P (Graph (insert (n, G, m) A))"
+ using prems
+ unfolding bounded_acg_def has_edge_def
+ by auto
+
+lemma finite_acg_ins:
+ "finite_acg (Graph (insert (n,G,m) A)) =
+ (finite_scg G \<and> finite_acg (Graph A))" (is "?A = (?B \<and> ?C)")
+proof
+ assume "?A"
+ thus "?B \<and> ?C"
+ unfolding finite_acg_def bounded_acg_def finite_scg_def has_edge_def
+ by auto
+next
+ assume "?B \<and> ?C"
+ thus ?A
+ proof
+ assume "?B" "?C"
+
+ from `?C`
+ obtain P where bA: "bounded_acg P (Graph A)" by (auto simp:finite_acg_def)
+ from `?B`
+ obtain P' where bG: "bounded_scg P' G" by (auto simp:finite_scg_def)
+
+ let ?Q = "max (max P P') (max (Suc n) (Suc m))"
+ have "P \<le> ?Q" "n < ?Q" "m < ?Q" by auto
+ have "bounded_acg ?Q (Graph (insert (n, G, m) A))"
+ apply (rule bacg_insert)
+ apply (rule bounded_up)
+ apply (rule bA)
+ apply auto
+ apply (rule bounded_scg_up)
+ apply (rule bG)
+ by auto
+ thus "finite_acg (Graph (insert (n, G, m) A))"
+ by (auto simp:finite_acg_def)
+ qed
+qed
+
+
+lemma bounded_mpath:
+ assumes "has_ipath acg mp"
+ and "bounded_acg P acg"
+ shows "bounded_mp P mp"
+ using prems
+ unfolding bounded_acg_def bounded_mp_def has_ipath_def
+ by blast
+
+lemma bounded_th:
+ assumes th: "is_thread n \<theta> mp"
+ and mp: "bounded_mp P mp"
+ shows "bounded_th P n \<theta>"
+ unfolding bounded_th_def
+proof (intro allI impI)
+ fix i assume "n < i"
+
+ from mp have "bounded_scg P (snd (mp i))" unfolding bounded_mp_def ..
+ moreover
+ from th `n < i` have "eqlat mp \<theta> i" unfolding is_thread_def by auto
+ ultimately
+ show "\<theta> i < P" unfolding bounded_scg_def by auto
+qed
+
+
+lemma finite_range:
+ fixes f :: "nat \<Rightarrow> 'a"
+ assumes fin: "finite (range f)"
+ shows "\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x"
+proof (rule classical)
+ assume "\<not>(\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x)"
+ hence "\<forall>x. \<exists>j. \<forall>i>j. f i \<noteq> x"
+ unfolding INF_nat by blast
+ with choice
+ have "\<exists>j. \<forall>x. \<forall>i>(j x). f i \<noteq> x" .
+ then obtain j where
+ neq: "\<And>x i. j x < i \<Longrightarrow> f i \<noteq> x" by blast
+
+ from fin have "finite (range (j o f))"
+ by (auto simp:comp_def)
+ with finite_nat_bounded
+ obtain m where "range (j o f) \<subseteq> {..<m}" by blast
+ hence "j (f m) < m" unfolding comp_def by auto
+
+ with neq[of "f m" m] show ?thesis by blast
+qed
+
+
+lemma bounded_th_infinite_visit:
+ fixes \<theta> :: "nat sequence"
+ assumes b: "bounded_th P n \<theta>"
+ shows "\<exists>p. \<exists>\<^sub>\<infinity>i. \<theta> i = p"
+proof -
+ have split: "range \<theta> = (\<theta> ` {0 .. n}) \<union> (\<theta> ` {i. n < i})"
+ (is "\<dots> = ?A \<union> ?B")
+ unfolding image_Un[symmetric] by auto
+
+ have "finite ?A" by (rule finite_imageI) auto
+ moreover
+ have "finite ?B"
+ proof (rule finite_subset)
+ from b
+ show "?B \<subseteq> { 0 ..< P }"
+ unfolding bounded_th_def
+ by auto
+ show "finite \<dots>" by auto
+ qed
+
+ ultimately have "finite (range \<theta>)"
+ unfolding split by auto
+
+ with finite_range show ?thesis .
+qed
+
+
+lemma bounded_scgcomp:
+ "bounded_scg P A
+ \<Longrightarrow> bounded_scg P B
+ \<Longrightarrow> bounded_scg P (A * B)"
+ unfolding bounded_scg_def
+ by (auto simp:in_grcomp)
+
+lemma bounded_acgcomp:
+ "bounded_acg P A
+ \<Longrightarrow> bounded_acg P B
+ \<Longrightarrow> bounded_acg P (A * B)"
+ unfolding bounded_acg_def
+ by (auto simp:in_grcomp intro!:bounded_scgcomp)
+
+lemma bounded_acgpow:
+ "bounded_acg P A
+ \<Longrightarrow> bounded_acg P (A ^ (Suc n))"
+ by (induct n, simp add:power_Suc)
+ (subst power_Suc, blast intro:bounded_acgcomp)
+
+lemma bounded_plus:
+ assumes b: "bounded_acg P acg"
+ shows "bounded_acg P (tcl acg)"
+ unfolding bounded_acg_def
+proof (intro allI impI conjI)
+ fix n G m
+ assume "tcl acg \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m"
+ then obtain i where "0 < i" and i: "acg ^ i \<turnstile> n \<leadsto>\<^bsup>G\<^esup> m"
+ unfolding in_tcl by auto (* FIXME: Disambiguate \<turnstile> Grammar *)
+ from b have "bounded_acg P (acg ^ (Suc (i - 1)))"
+ by (rule bounded_acgpow)
+ with `0 < i` have "bounded_acg P (acg ^ i)" by simp
+ with i
+ show "n < P" "m < P" "bounded_scg P G"
+ unfolding bounded_acg_def
+ by auto
+qed
+
+
+lemma bounded_scg_def':
+ "bounded_scg P G = (\<forall>(p,e,p')\<in>dest_graph G. p < P \<and> p' < P)"
+ unfolding bounded_scg_def has_edge_def
+ by auto
+
+
+lemma finite_bounded_scg: "finite { G. bounded_scg P G }"
+proof (rule finite_subset)
+ show "{G. bounded_scg P G} \<subseteq>
+ Graph ` (Pow ({0 .. P - 1} \<times> UNIV \<times> {0 .. P - 1}))"
+ proof (rule, simp)
+ fix G
+
+ assume b: "bounded_scg P G"
+
+ show "G \<in> Graph ` Pow ({0..P - Suc 0} \<times> UNIV \<times> {0..P - Suc 0})"
+ proof (cases G)
+ fix G' assume [simp]: "G = Graph G'"
+
+ from b show ?thesis
+ by (auto simp:bounded_scg_def' image_def)
+ qed
+ qed
+
+ show "finite \<dots>"
+ apply (rule finite_imageI)
+ apply (unfold finite_Pow_iff)
+ by (intro finite_cartesian_product finite_atLeastAtMost
+ finite_class.finite)
+qed
+
+lemma bounded_finite:
+ assumes bounded: "bounded_acg P A"
+ shows "finite (dest_graph A)"
+proof (rule finite_subset)
+
+ from bounded
+ show "dest_graph A \<subseteq> {0 .. P - 1} \<times> { G. bounded_scg P G } \<times> { 0 .. P - 1}"
+ by (auto simp:bounded_acg_def has_edge_def) force+
+
+ show "finite \<dots>"
+ by (intro finite_cartesian_product finite_atLeastAtMost finite_bounded_scg)
+qed
+
+
+
+section {* Contraction and more *}
+
+
+abbreviation
+ "pdesc P == (fst P, prod P, end_node P)"
+
+lemma pdesc_acgplus:
+ assumes "has_ipath \<A> p"
+ and "i < j"
+ shows "has_edge (tcl \<A>) (fst (p\<langle>i,j\<rangle>)) (prod (p\<langle>i,j\<rangle>)) (end_node (p\<langle>i,j\<rangle>))"
+ unfolding plus_paths
+ apply (rule exI)
+ apply (insert prems)
+ by (auto intro:sub_path_is_path[of "\<A>" p i j] simp:sub_path_def)
+
+
+
+
+lemma combine_fthreads:
+ assumes range: "i < j" "j \<le> k"
+ shows
+ "has_fth p i k m r =
+ (\<exists>n. has_fth p i j m n \<and> has_fth p j k n r)" (is "?L = ?R")
+proof (intro iffI)
+ assume "?L"
+ then obtain \<theta>
+ where "is_fthread \<theta> p i k"
+ and [simp]: "\<theta> i = m" "\<theta> k = r"
+ by (auto simp:has_fth_def)
+
+ with range
+ have "is_fthread \<theta> p i j" and "is_fthread \<theta> p j k"
+ by (auto simp:is_fthread_def)
+ hence "has_fth p i j m (\<theta> j)" and "has_fth p j k (\<theta> j) r"
+ by (auto simp:has_fth_def)
+ thus "?R" by auto
+next
+ assume "?R"
+ then obtain n \<theta>1 \<theta>2
+ where ths: "is_fthread \<theta>1 p i j" "is_fthread \<theta>2 p j k"
+ and [simp]: "\<theta>1 i = m" "\<theta>1 j = n" "\<theta>2 j = n" "\<theta>2 k = r"
+ by (auto simp:has_fth_def)
+
+ let ?\<theta> = "(\<lambda>i. if i < j then \<theta>1 i else \<theta>2 i)"
+ have "is_fthread ?\<theta> p i k"
+ unfolding is_fthread_def
+ proof
+ fix l assume range: "l \<in> {i..<k}"
+
+ show "eqlat p ?\<theta> l"
+ proof (cases rule:three_cases)
+ assume "Suc l < j"
+ with ths range show ?thesis
+ unfolding is_fthread_def Ball_def
+ by simp
+ next
+ assume "Suc l = j"
+ hence "l < j" "\<theta>2 (Suc l) = \<theta>1 (Suc l)" by auto
+ with ths range show ?thesis
+ unfolding is_fthread_def Ball_def
+ by simp
+ next
+ assume "j \<le> l"
+ with ths range show ?thesis
+ unfolding is_fthread_def Ball_def
+ by simp
+ qed arith
+ qed
+ moreover
+ have "?\<theta> i = m" "?\<theta> k = r" using range by auto
+ ultimately show "has_fth p i k m r"
+ by (auto simp:has_fth_def)
+qed
+
+
+lemma desc_is_fthread:
+ "is_desc_fthread \<theta> p i k \<Longrightarrow> is_fthread \<theta> p i k"
+ unfolding is_desc_fthread_def
+ by simp
+
+
+lemma combine_dfthreads:
+ assumes range: "i < j" "j \<le> k"
+ shows
+ "has_desc_fth p i k m r =
+ (\<exists>n. (has_desc_fth p i j m n \<and> has_fth p j k n r)
+ \<or> (has_fth p i j m n \<and> has_desc_fth p j k n r))" (is "?L = ?R")
+proof
+ assume "?L"
+ then obtain \<theta>
+ where desc: "is_desc_fthread \<theta> p i k"
+ and [simp]: "\<theta> i = m" "\<theta> k = r"
+ by (auto simp:has_desc_fth_def)
+
+ hence "is_fthread \<theta> p i k"
+ by (simp add: desc_is_fthread)
+ with range have fths: "is_fthread \<theta> p i j" "is_fthread \<theta> p j k"
+ unfolding is_fthread_def
+ by auto
+ hence hfths: "has_fth p i j m (\<theta> j)" "has_fth p j k (\<theta> j) r"
+ by (auto simp:has_fth_def)
+
+ from desc obtain l
+ where "i \<le> l" "l < k"
+ and "descat p \<theta> l"
+ by (auto simp:is_desc_fthread_def)
+
+ with fths
+ have "is_desc_fthread \<theta> p i j \<or> is_desc_fthread \<theta> p j k"
+ unfolding is_desc_fthread_def
+ by (cases "l < j") auto
+ hence "has_desc_fth p i j m (\<theta> j) \<or> has_desc_fth p j k (\<theta> j) r"
+ by (auto simp:has_desc_fth_def)
+ with hfths show ?R
+ by auto
+next
+ assume "?R"
+ then obtain n \<theta>1 \<theta>2
+ where "(is_desc_fthread \<theta>1 p i j \<and> is_fthread \<theta>2 p j k)
+ \<or> (is_fthread \<theta>1 p i j \<and> is_desc_fthread \<theta>2 p j k)"
+ and [simp]: "\<theta>1 i = m" "\<theta>1 j = n" "\<theta>2 j = n" "\<theta>2 k = r"
+ by (auto simp:has_fth_def has_desc_fth_def)
+
+ hence ths2: "is_fthread \<theta>1 p i j" "is_fthread \<theta>2 p j k"
+ and dths: "is_desc_fthread \<theta>1 p i j \<or> is_desc_fthread \<theta>2 p j k"
+ by (auto simp:desc_is_fthread)
+
+ let ?\<theta> = "(\<lambda>i. if i < j then \<theta>1 i else \<theta>2 i)"
+ have "is_fthread ?\<theta> p i k"
+ unfolding is_fthread_def
+ proof
+ fix l assume range: "l \<in> {i..<k}"
+
+ show "eqlat p ?\<theta> l"
+ proof (cases rule:three_cases)
+ assume "Suc l < j"
+ with ths2 range show ?thesis
+ unfolding is_fthread_def Ball_def
+ by simp
+ next
+ assume "Suc l = j"
+ hence "l < j" "\<theta>2 (Suc l) = \<theta>1 (Suc l)" by auto
+ with ths2 range show ?thesis
+ unfolding is_fthread_def Ball_def
+ by simp
+ next
+ assume "j \<le> l"
+ with ths2 range show ?thesis
+ unfolding is_fthread_def Ball_def
+ by simp
+ qed arith
+ qed
+ moreover
+ from dths
+ have "\<exists>l. i \<le> l \<and> l < k \<and> descat p ?\<theta> l"
+ proof
+ assume "is_desc_fthread \<theta>1 p i j"
+
+ then obtain l where range: "i \<le> l" "l < j" and "descat p \<theta>1 l"
+ unfolding is_desc_fthread_def Bex_def by auto
+ hence "descat p ?\<theta> l"
+ by (cases "Suc l = j", auto)
+ with `j \<le> k` and range show ?thesis
+ by (rule_tac x="l" in exI, auto)
+ next
+ assume "is_desc_fthread \<theta>2 p j k"
+ then obtain l where range: "j \<le> l" "l < k" and "descat p \<theta>2 l"
+ unfolding is_desc_fthread_def Bex_def by auto
+ with `i < j` have "descat p ?\<theta> l" "i \<le> l"
+ by auto
+ with range show ?thesis
+ by (rule_tac x="l" in exI, auto)
+ qed
+ ultimately have "is_desc_fthread ?\<theta> p i k"
+ by (simp add: is_desc_fthread_def Bex_def)
+
+ moreover
+ have "?\<theta> i = m" "?\<theta> k = r" using range by auto
+
+ ultimately show "has_desc_fth p i k m r"
+ by (auto simp:has_desc_fth_def)
+qed
+
+
+
+lemma fth_single:
+ "has_fth p i (Suc i) m n = eql (snd (p i)) m n" (is "?L = ?R")
+proof
+ assume "?L" thus "?R"
+ unfolding is_fthread_def Ball_def has_fth_def
+ by auto
+next
+ let ?\<theta> = "\<lambda>k. if k = i then m else n"
+ assume edge: "?R"
+ hence "is_fthread ?\<theta> p i (Suc i) \<and> ?\<theta> i = m \<and> ?\<theta> (Suc i) = n"
+ unfolding is_fthread_def Ball_def
+ by auto
+
+ thus "?L"
+ unfolding has_fth_def
+ by auto
+qed
+
+lemma desc_fth_single:
+ "has_desc_fth p i (Suc i) m n =
+ dsc (snd (p i)) m n" (is "?L = ?R")
+proof
+ assume "?L" thus "?R"
+ unfolding is_desc_fthread_def has_desc_fth_def is_fthread_def
+ Bex_def
+ by (elim exE conjE) (case_tac "k = i", auto)
+next
+ let ?\<theta> = "\<lambda>k. if k = i then m else n"
+ assume edge: "?R"
+ hence "is_desc_fthread ?\<theta> p i (Suc i) \<and> ?\<theta> i = m \<and> ?\<theta> (Suc i) = n"
+ unfolding is_desc_fthread_def is_fthread_def Ball_def Bex_def
+ by auto
+ thus "?L"
+ unfolding has_desc_fth_def
+ by auto
+qed
+
+lemma mk_eql: "(G \<turnstile> m \<leadsto>\<^bsup>e\<^esup> n) \<Longrightarrow> eql G m n"
+ by (cases e, auto)
+
+lemma eql_scgcomp:
+ "eql (G * H) m r =
+ (\<exists>n. eql G m n \<and> eql H n r)" (is "?L = ?R")
+proof
+ show "?L \<Longrightarrow> ?R"
+ by (auto simp:in_grcomp intro!:mk_eql)
+
+ assume "?R"
+ then obtain n where l: "eql G m n" and r:"eql H n r" by auto
+ thus ?L
+ by (cases "dsc G m n") (auto simp:in_grcomp mult_sedge_def)
+qed
+
+lemma desc_scgcomp:
+ "dsc (G * H) m r =
+ (\<exists>n. (dsc G m n \<and> eql H n r) \<or> (eq G m n \<and> dsc H n r))" (is "?L = ?R")
+proof
+ show "?R \<Longrightarrow> ?L" by (auto simp:in_grcomp mult_sedge_def)
+
+ assume "?L"
+ thus ?R
+ by (auto simp:in_grcomp mult_sedge_def)
+ (case_tac "e", auto, case_tac "e'", auto)
+qed
+
+
+lemma has_fth_unfold:
+ assumes "i < j"
+ shows "has_fth p i j m n =
+ (\<exists>r. has_fth p i (Suc i) m r \<and> has_fth p (Suc i) j r n)"
+ by (rule combine_fthreads) (insert `i < j`, auto)
+
+lemma has_dfth_unfold:
+ assumes range: "i < j"
+ shows
+ "has_desc_fth p i j m r =
+ (\<exists>n. (has_desc_fth p i (Suc i) m n \<and> has_fth p (Suc i) j n r)
+ \<or> (has_fth p i (Suc i) m n \<and> has_desc_fth p (Suc i) j n r))"
+ by (rule combine_dfthreads) (insert `i < j`, auto)
+
+
+lemma Lemma7a:
+assumes "i \<le> j"
+shows
+ "has_fth p i j m n =
+ eql (prod (p\<langle>i,j\<rangle>)) m n"
+using prems
+proof (induct i arbitrary: m rule:inc_induct)
+ case 1 show ?case
+ unfolding has_fth_def is_fthread_def sub_path_def
+ by (auto simp:in_grunit one_sedge_def)
+next
+ case (2 i)
+ note IH = `\<And>m. has_fth p (Suc i) j m n =
+ eql (prod (p\<langle>Suc i,j\<rangle>)) m n`
+
+ have "has_fth p i j m n
+ = (\<exists>r. has_fth p i (Suc i) m r \<and> has_fth p (Suc i) j r n)"
+ by (rule has_fth_unfold[OF `i < j`])
+ also have "\<dots> = (\<exists>r. has_fth p i (Suc i) m r
+ \<and> eql (prod (p\<langle>Suc i,j\<rangle>)) r n)"
+ by (simp only:IH)
+ also have "\<dots> = (\<exists>r. eql (snd (p i)) m r
+ \<and> eql (prod (p\<langle>Suc i,j\<rangle>)) r n)"
+ by (simp only:fth_single)
+ also have "\<dots> = eql (snd (p i) * prod (p\<langle>Suc i,j\<rangle>)) m n"
+ by (simp only:eql_scgcomp)
+ also have "\<dots> = eql (prod (p\<langle>i,j\<rangle>)) m n"
+ by (simp only:prod_unfold[OF `i < j`])
+ finally show ?case .
+qed
+
+
+lemma Lemma7b:
+assumes "i \<le> j"
+shows
+ "has_desc_fth p i j m n =
+ dsc (prod (p\<langle>i,j\<rangle>)) m n"
+using prems
+proof (induct i arbitrary: m rule:inc_induct)
+ case 1 show ?case
+ unfolding has_desc_fth_def is_desc_fthread_def sub_path_def
+ by (auto simp:in_grunit one_sedge_def)
+next
+ case (2 i)
+ thus ?case
+ by (simp only:prod_unfold desc_scgcomp desc_fth_single
+ has_dfth_unfold fth_single Lemma7a) auto
+qed
+
+
+lemma descat_contract:
+ assumes [simp]: "increasing s"
+ shows
+ "descat (contract s p) \<theta> i =
+ has_desc_fth p (s i) (s (Suc i)) (\<theta> i) (\<theta> (Suc i))"
+ by (simp add:Lemma7b increasing_weak contract_def)
+
+lemma eqlat_contract:
+ assumes [simp]: "increasing s"
+ shows
+ "eqlat (contract s p) \<theta> i =
+ has_fth p (s i) (s (Suc i)) (\<theta> i) (\<theta> (Suc i))"
+ by (auto simp:Lemma7a increasing_weak contract_def)
+
+
+subsection {* Connecting threads *}
+
+definition
+ "connect s \<theta>s = (\<lambda>k. \<theta>s (section_of s k) k)"
+
+
+lemma next_in_range:
+ assumes [simp]: "increasing s"
+ assumes a: "k \<in> section s i"
+ shows "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))"
+proof -
+ from a have "k < s (Suc i)" by simp
+
+ hence "Suc k < s (Suc i) \<or> Suc k = s (Suc i)" by arith
+ thus ?thesis
+ proof
+ assume "Suc k < s (Suc i)"
+ with a have "Suc k \<in> section s i" by simp
+ thus ?thesis ..
+ next
+ assume eq: "Suc k = s (Suc i)"
+ with increasing_strict have "Suc k < s (Suc (Suc i))" by simp
+ with eq have "Suc k \<in> section s (Suc i)" by simp
+ thus ?thesis ..
+ qed
+qed
+
+
+
+lemma connect_threads:
+ assumes [simp]: "increasing s"
+ assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
+ assumes fth: "is_fthread (\<theta>s i) p (s i) (s (Suc i))"
+
+ shows
+ "is_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
+ unfolding is_fthread_def
+proof
+ fix k assume krng: "k \<in> section s i"
+
+ with fth have eqlat: "eqlat p (\<theta>s i) k"
+ unfolding is_fthread_def by simp
+
+ from krng and next_in_range
+ have "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))"
+ by simp
+ thus "eqlat p (connect s \<theta>s) k"
+ proof
+ assume "Suc k \<in> section s i"
+ with krng eqlat show ?thesis
+ unfolding connect_def
+ by (simp only:section_of_known `increasing s`)
+ next
+ assume skrng: "Suc k \<in> section s (Suc i)"
+ with krng have "Suc k = s (Suc i)" by auto
+
+ with krng skrng eqlat show ?thesis
+ unfolding connect_def
+ by (simp only:section_of_known connected[symmetric] `increasing s`)
+ qed
+qed
+
+
+lemma connect_dthreads:
+ assumes inc[simp]: "increasing s"
+ assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
+ assumes fth: "is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
+
+ shows
+ "is_desc_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
+ unfolding is_desc_fthread_def
+proof
+ show "is_fthread (connect s \<theta>s) p (s i) (s (Suc i))"
+ apply (rule connect_threads)
+ apply (insert fth)
+ by (auto simp:connected is_desc_fthread_def)
+
+ from fth
+ obtain k where dsc: "descat p (\<theta>s i) k" and krng: "k \<in> section s i"
+ unfolding is_desc_fthread_def by blast
+
+ from krng and next_in_range
+ have "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))"
+ by simp
+ hence "descat p (connect s \<theta>s) k"
+ proof
+ assume "Suc k \<in> section s i"
+ with krng dsc show ?thesis unfolding connect_def
+ by (simp only:section_of_known inc)
+ next
+ assume skrng: "Suc k \<in> section s (Suc i)"
+ with krng have "Suc k = s (Suc i)" by auto
+
+ with krng skrng dsc show ?thesis unfolding connect_def
+ by (simp only:section_of_known connected[symmetric] inc)
+ qed
+ with krng show "\<exists>k\<in>section s i. descat p (connect s \<theta>s) k" ..
+qed
+
+
+
+lemma mk_inf_thread:
+ assumes [simp]: "increasing s"
+ assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))"
+ shows "is_thread (s (Suc n)) \<theta> p"
+ unfolding is_thread_def
+proof (intro allI impI)
+ fix j assume st: "s (Suc n) \<le> j"
+
+ let ?k = "section_of s j"
+ from in_section_of st
+ have rs: "j \<in> section s ?k" by simp
+
+ with st have "s (Suc n) < s (Suc ?k)" by simp
+ with increasing_bij have "n < ?k" by simp
+ with rs and fths[of ?k]
+ show "eqlat p \<theta> j" by (simp add:is_fthread_def)
+qed
+
+
+lemma mk_inf_desc_thread:
+ assumes [simp]: "increasing s"
+ assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))"
+ assumes fdths: "\<exists>\<^sub>\<infinity>i. is_desc_fthread \<theta> p (s i) (s (Suc i))"
+ shows "is_desc_thread \<theta> p"
+ unfolding is_desc_thread_def
+proof (intro exI conjI)
+
+ from mk_inf_thread[of s n] is_thread_def fths
+ show "\<forall>i\<ge>s (Suc n). eqlat p \<theta> i" by simp
+
+ show "\<exists>\<^sub>\<infinity>l. descat p \<theta> l"
+ unfolding INF_nat
+ proof
+ fix i
+
+ let ?k = "section_of s i"
+ from fdths obtain j
+ where "?k < j" "is_desc_fthread \<theta> p (s j) (s (Suc j))"
+ unfolding INF_nat by auto
+ then obtain l where "s j \<le> l" and desc: "descat p \<theta> l"
+ unfolding is_desc_fthread_def
+ by auto
+
+ have "i < s (Suc ?k)" by (rule section_of2)
+ also have "\<dots> \<le> s j"
+ by (rule increasing_weak[of s], assumption)
+ (insert `?k < j`, arith)
+ also note `\<dots> \<le> l`
+ finally have "i < l" .
+ with desc
+ show "\<exists>l. i < l \<and> descat p \<theta> l" by blast
+ qed
+qed
+
+
+lemma desc_ex_choice:
+ assumes A: "((\<exists>n.\<forall>i\<ge>n. \<exists>x. P x i) \<and> (\<exists>\<^sub>\<infinity>i. \<exists>x. Q x i))"
+ and imp: "\<And>x i. Q x i \<Longrightarrow> P x i"
+ shows "\<exists>xs. ((\<exists>n.\<forall>i\<ge>n. P (xs i) i) \<and> (\<exists>\<^sub>\<infinity>i. Q (xs i) i))"
+ (is "\<exists>xs. ?Ps xs \<and> ?Qs xs")
+proof
+ let ?w = "\<lambda>i. (if (\<exists>x. Q x i) then (SOME x. Q x i)
+ else (SOME x. P x i))"
+
+ from A
+ obtain n where P: "\<And>i. n \<le> i \<Longrightarrow> \<exists>x. P x i"
+ by auto
+ {
+ fix i::'a assume "n \<le> i"
+
+ have "P (?w i) i"
+ proof (cases "\<exists>x. Q x i")
+ case True
+ hence "Q (?w i) i" by (auto intro:someI)
+ with imp show "P (?w i) i" .
+ next
+ case False
+ with P[OF `n \<le> i`] show "P (?w i) i"
+ by (auto intro:someI)
+ qed
+ }
+
+ hence "?Ps ?w" by (rule_tac x=n in exI) auto
+
+ moreover
+ from A have "\<exists>\<^sub>\<infinity>i. (\<exists>x. Q x i)" ..
+ hence "?Qs ?w" by (rule INF_mono) (auto intro:someI)
+ ultimately
+ show "?Ps ?w \<and> ?Qs ?w" ..
+qed
+
+
+
+lemma dthreads_join:
+ assumes [simp]: "increasing s"
+ assumes dthread: "is_desc_thread \<theta> (contract s p)"
+ shows "\<exists>\<theta>s. desc (\<lambda>i. is_fthread (\<theta>s i) p (s i) (s (Suc i))
+ \<and> \<theta>s i (s i) = \<theta> i
+ \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))
+ (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))
+ \<and> \<theta>s i (s i) = \<theta> i
+ \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))"
+ apply (rule desc_ex_choice)
+ apply (insert dthread)
+ apply (simp only:is_desc_thread_def)
+ apply (simp add:eqlat_contract)
+ apply (simp add:descat_contract)
+ apply (simp only:has_fth_def has_desc_fth_def)
+ by (auto simp:is_desc_fthread_def)
+
+
+
+lemma INF_drop_prefix:
+ "(\<exists>\<^sub>\<infinity>i::nat. i > n \<and> P i) = (\<exists>\<^sub>\<infinity>i. P i)"
+ apply (auto simp:INF_nat)
+ apply (drule_tac x = "max m n" in spec)
+ apply (elim exE conjE)
+ apply (rule_tac x = "na" in exI)
+ by auto
+
+
+
+lemma contract_keeps_threads:
+ assumes inc[simp]: "increasing s"
+ shows "(\<exists>\<theta>. is_desc_thread \<theta> p)
+ \<longleftrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> (contract s p))"
+ (is "?A \<longleftrightarrow> ?B")
+proof
+ assume "?A"
+ then obtain \<theta> n
+ where fr: "\<forall>i\<ge>n. eqlat p \<theta> i"
+ and ds: "\<exists>\<^sub>\<infinity>i. descat p \<theta> i"
+ unfolding is_desc_thread_def
+ by auto
+
+ let ?c\<theta> = "\<lambda>i. \<theta> (s i)"
+
+ have "is_desc_thread ?c\<theta> (contract s p)"
+ unfolding is_desc_thread_def
+ proof (intro exI conjI)
+
+ show "\<forall>i\<ge>n. eqlat (contract s p) ?c\<theta> i"
+ proof (intro allI impI)
+ fix i assume "n \<le> i"
+ also have "i \<le> s i"
+ using increasing_inc by auto
+ finally have "n \<le> s i" .
+
+ with fr have "is_fthread \<theta> p (s i) (s (Suc i))"
+ unfolding is_fthread_def by auto
+ hence "has_fth p (s i) (s (Suc i)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
+ unfolding has_fth_def by auto
+ with less_imp_le[OF increasing_strict]
+ have "eql (prod (p\<langle>s i,s (Suc i)\<rangle>)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
+ by (simp add:Lemma7a)
+ thus "eqlat (contract s p) ?c\<theta> i" unfolding contract_def
+ by auto
+ qed
+
+ show "\<exists>\<^sub>\<infinity>i. descat (contract s p) ?c\<theta> i"
+ unfolding INF_nat
+ proof
+ fix i
+
+ let ?K = "section_of s (max (s (Suc i)) n)"
+ from `\<exists>\<^sub>\<infinity>i. descat p \<theta> i` obtain j
+ where "s (Suc ?K) < j" "descat p \<theta> j"
+ unfolding INF_nat by blast
+
+ let ?L = "section_of s j"
+ {
+ fix x assume r: "x \<in> section s ?L"
+
+ have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2)
+ note `s (Suc ?K) < j`
+ also have "j < s (Suc ?L)"
+ by (rule section_of2)
+ finally have "Suc ?K \<le> ?L"
+ by (simp add:increasing_bij)
+ with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
+ with e1 r have "max (s (Suc i)) n < x" by simp
+
+ hence "(s (Suc i)) < x" "n < x" by auto
+ }
+ note range_est = this
+
+ have "is_desc_fthread \<theta> p (s ?L) (s (Suc ?L))"
+ unfolding is_desc_fthread_def is_fthread_def
+ proof
+ show "\<forall>m\<in>section s ?L. eqlat p \<theta> m"
+ proof
+ fix m assume "m\<in>section s ?L"
+ with range_est(2) have "n < m" .
+ with fr show "eqlat p \<theta> m" by simp
+ qed
+
+
+ from in_section_of inc less_imp_le[OF `s (Suc ?K) < j`]
+ have "j \<in> section s ?L" .
+
+ with `descat p \<theta> j`
+ show "\<exists>m\<in>section s ?L. descat p \<theta> m" ..
+ qed
+
+ with less_imp_le[OF increasing_strict]
+ have a: "descat (contract s p) ?c\<theta> ?L"
+ unfolding contract_def Lemma7b[symmetric]
+ by (auto simp:Lemma7b[symmetric] has_desc_fth_def)
+
+ have "i < ?L"
+ proof (rule classical)
+ assume "\<not> i < ?L"
+ hence "s ?L < s (Suc i)"
+ by (simp add:increasing_bij)
+ also have "\<dots> < s ?L"
+ by (rule range_est(1)) (simp add:increasing_strict)
+ finally show ?thesis .
+ qed
+ with a show "\<exists>l. i < l \<and> descat (contract s p) ?c\<theta> l"
+ by blast
+ qed
+ qed
+ with exI show "?B" .
+next
+ assume "?B"
+ then obtain \<theta>
+ where dthread: "is_desc_thread \<theta> (contract s p)" ..
+
+ with dthreads_join inc
+ obtain \<theta>s where ths_spec:
+ "desc (\<lambda>i. is_fthread (\<theta>s i) p (s i) (s (Suc i))
+ \<and> \<theta>s i (s i) = \<theta> i
+ \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))
+ (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))
+ \<and> \<theta>s i (s i) = \<theta> i
+ \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))"
+ (is "desc ?alw ?inf")
+ by blast
+
+ then obtain n where fr: "\<forall>i\<ge>n. ?alw i" by blast
+ hence connected: "\<And>i. n < i \<Longrightarrow> \<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
+ by auto
+
+ let ?j\<theta> = "connect s \<theta>s"
+
+ from fr ths_spec have ths_spec2:
+ "\<And>i. i > n \<Longrightarrow> is_fthread (\<theta>s i) p (s i) (s (Suc i))"
+ "\<exists>\<^sub>\<infinity>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
+ by (auto intro:INF_mono)
+
+ have p1: "\<And>i. i > n \<Longrightarrow> is_fthread ?j\<theta> p (s i) (s (Suc i))"
+ by (rule connect_threads) (auto simp:connected ths_spec2)
+
+ from ths_spec2(2)
+ have "\<exists>\<^sub>\<infinity>i. n < i \<and> is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
+ unfolding INF_drop_prefix .
+
+ hence p2: "\<exists>\<^sub>\<infinity>i. is_desc_fthread ?j\<theta> p (s i) (s (Suc i))"
+ apply (rule INF_mono)
+ apply (rule connect_dthreads)
+ by (auto simp:connected)
+
+ with `increasing s` p1
+ have "is_desc_thread ?j\<theta> p"
+ by (rule mk_inf_desc_thread)
+ with exI show "?A" .
+qed
+
+
+
+lemma repeated_edge:
+ assumes "\<And>i. i > n \<Longrightarrow> dsc (snd (p i)) k k"
+ shows "is_desc_thread (\<lambda>i. k) p"
+ using prems
+ unfolding is_desc_thread_def
+ apply (auto)
+ apply (rule_tac x="Suc n" in exI, auto)
+ apply (rule INF_mono[where P="\<lambda>i. n < i"])
+ apply (simp only:INF_nat)
+ by auto arith
+
+
+lemma fin_from_inf:
+ assumes "is_thread n \<theta> p"
+ assumes "n < i"
+ assumes "i < j"
+ shows "is_fthread \<theta> p i j"
+ using prems
+ unfolding is_thread_def is_fthread_def
+ by auto
+
+
+
+section {* Ramsey's Theorem *}
+
+
+definition
+ "set2pair S = (THE (x,y). x < y \<and> S = {x,y})"
+
+lemma set2pair_conv:
+ fixes x y :: nat
+ assumes "x < y"
+ shows "set2pair {x, y} = (x, y)"
+ unfolding set2pair_def
+proof (rule the_equality, simp_all only:split_conv split_paired_all)
+ from `x < y` show "x < y \<and> {x,y}={x,y}" by simp
+next
+ fix a b
+ assume a: "a < b \<and> {x, y} = {a, b}"
+ hence "{a, b} = {x, y}" by simp_all
+ hence "(a, b) = (x, y) \<or> (a, b) = (y, x)"
+ by (cases "x = y") auto
+ thus "(a, b) = (x, y)"
+ proof
+ assume "(a, b) = (y, x)"
+ with a and `x < y`
+ show ?thesis by auto (* contradiction *)
+ qed
+qed
+
+definition
+ "set2list = inv set"
+
+lemma finite_set2list:
+ assumes [intro]: "finite S"
+ shows "set (set2list S) = S"
+ unfolding set2list_def
+proof (rule f_inv_f)
+ from finite_list
+ have "\<exists>l. set l = S" .
+ thus "S \<in> range set"
+ unfolding image_def
+ by auto
+qed
+
+
+corollary RamseyNatpairs:
+ fixes S :: "'a set"
+ and f :: "nat \<times> nat \<Rightarrow> 'a"
+
+ assumes "finite S"
+ and inS: "\<And>x y. x < y \<Longrightarrow> f (x, y) \<in> S"
+
+ obtains T :: "nat set" and s :: "'a"
+ where "infinite T"
+ and "s \<in> S"
+ and "\<And>x y. \<lbrakk>x \<in> T; y \<in> T; x < y\<rbrakk> \<Longrightarrow> f (x, y) = s"
+proof -
+ from `finite S`
+ have "set (set2list S) = S" by (rule finite_set2list)
+ then
+ obtain l where S: "S = set l" by auto
+ also from set_conv_nth have "\<dots> = {l ! i |i. i < length l}" .
+ finally have "S = {l ! i |i. i < length l}" .
+
+ let ?s = "length l"
+
+ from inS
+ have index_less: "\<And>x y. x \<noteq> y \<Longrightarrow> index_of l (f (set2pair {x, y})) < ?s"
+ proof -
+ fix x y :: nat
+ assume neq: "x \<noteq> y"
+ have "f (set2pair {x, y}) \<in> S"
+ proof (cases "x < y")
+ case True hence "set2pair {x, y} = (x, y)"
+ by (rule set2pair_conv)
+ with True inS
+ show ?thesis by simp
+ next
+ case False
+ with neq have y_less: "y < x" by simp
+ have x:"{x,y} = {y,x}" by auto
+ with y_less have "set2pair {x, y} = (y, x)"
+ by (simp add:set2pair_conv)
+ with y_less inS
+ show ?thesis by simp
+ qed
+
+ thus "index_of l (f (set2pair {x, y})) < length l"
+ by (simp add: S index_of_length)
+ qed
+
+ have "\<exists>Y. infinite Y \<and>
+ (\<exists>t. t < ?s \<and>
+ (\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow>
+ index_of l (f (set2pair {x, y})) = t))"
+ by (rule Ramsey2[of "UNIV::nat set", simplified])
+ (auto simp:index_less)
+ then obtain T i
+ where inf: "infinite T"
+ and "i < length l"
+ and d: "\<And>x y. \<lbrakk>x \<in> T; y\<in>T; x \<noteq> y\<rbrakk>
+ \<Longrightarrow> index_of l (f (set2pair {x, y})) = i"
+ by auto
+
+ have "l ! i \<in> S" unfolding S
+ by (rule nth_mem)
+ moreover
+ have "\<And>x y. x \<in> T \<Longrightarrow> y\<in>T \<Longrightarrow> x < y
+ \<Longrightarrow> f (x, y) = l ! i"
+ proof -
+ fix x y assume "x \<in> T" "y \<in> T" "x < y"
+ with d have
+ "index_of l (f (set2pair {x, y})) = i" by auto
+ with `x < y`
+ have "i = index_of l (f (x, y))"
+ by (simp add:set2pair_conv)
+ with `i < length l`
+ show "f (x, y) = l ! i"
+ by (auto intro:index_of_member[symmetric] iff:index_of_length)
+ qed
+ moreover note inf
+ ultimately
+ show ?thesis using prems
+ by blast
+qed
+
+
+section {* Main Result *}
+
+
+theorem LJA_Theorem4:
+ assumes "bounded_acg P \<A>"
+ shows "SCT \<A> \<longleftrightarrow> SCT' \<A>"
+proof
+ assume "SCT \<A>"
+
+ show "SCT' \<A>"
+ proof (rule classical)
+ assume "\<not> SCT' \<A>"
+
+ then obtain n G
+ where in_closure: "(tcl \<A>) \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
+ and idemp: "G * G = G"
+ and no_strict_arc: "\<forall>p. \<not>(G \<turnstile> p \<leadsto>\<^bsup>\<down>\<^esup> p)"
+ unfolding SCT'_def no_bad_graphs_def by auto
+
+ from in_closure obtain k
+ where k_pow: "\<A> ^ k \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n"
+ and "0 < k"
+ unfolding in_tcl by auto
+
+ from power_induces_path k_pow
+ obtain loop where loop_props:
+ "has_fpath \<A> loop"
+ "n = fst loop" "n = end_node loop"
+ "G = prod loop" "k = length (snd loop)" .
+
+ with `0 < k` and path_loop_graph
+ have "has_ipath \<A> (omega loop)" by blast
+ with `SCT \<A>`
+ have thread: "\<exists>\<theta>. is_desc_thread \<theta> (omega loop)" by (auto simp:SCT_def)
+
+ let ?s = "\<lambda>i. k * i"
+ let ?cp = "\<lambda>i. (n, G)"
+
+ from loop_props have "fst loop = end_node loop" by auto
+ with `0 < k` `k = length (snd loop)`
+ have "\<And>i. (omega loop)\<langle>?s i,?s (Suc i)\<rangle> = loop"
+ by (rule sub_path_loop)
+
+ with `n = fst loop` `G = prod loop` `k = length (snd loop)`
+ have a: "contract ?s (omega loop) = ?cp"
+ unfolding contract_def
+ by (simp add:path_loop_def split_def fst_p0)
+
+ from `0 < k` have "increasing ?s"
+ by (auto simp:increasing_def)
+ with thread have "\<exists>\<theta>. is_desc_thread \<theta> ?cp"
+ unfolding a[symmetric]
+ by (unfold contract_keeps_threads[symmetric])
+
+ then obtain \<theta> where desc: "is_desc_thread \<theta> ?cp" by auto
+
+ then obtain n where thr: "is_thread n \<theta> ?cp"
+ unfolding is_desc_thread_def is_thread_def
+ by auto
+
+ have "bounded_th P n \<theta>"
+ proof -
+ from `bounded_acg P \<A>`
+ have "bounded_acg P (tcl \<A>)" by (rule bounded_plus)
+ with in_closure have "bounded_scg P G"
+ unfolding bounded_acg_def by simp
+ hence "bounded_mp P ?cp"
+ unfolding bounded_mp_def by simp
+ with thr bounded_th
+ show ?thesis by auto
+ qed
+ with bounded_th_infinite_visit
+ obtain p where inf_visit: "\<exists>\<^sub>\<infinity>i. \<theta> i = p" by blast
+
+ then obtain i where "n < i" "\<theta> i = p"
+ by (auto simp:INF_nat)
+
+ from desc
+ have "\<exists>\<^sub>\<infinity>i. descat ?cp \<theta> i"
+ unfolding is_desc_thread_def by auto
+ then obtain j
+ where "i < j" and "descat ?cp \<theta> j"
+ unfolding INF_nat by auto
+ from inf_visit obtain k where "j < k" "\<theta> k = p"
+ by (auto simp:INF_nat)
+
+ from `i < j` `j < k` `n < i` thr fin_from_inf `descat ?cp \<theta> j`
+ have "is_desc_fthread \<theta> ?cp i k"
+ unfolding is_desc_fthread_def
+ by auto
+
+ with `\<theta> k = p` `\<theta> i = p`
+ have dfth: "has_desc_fth ?cp i k p p"
+ unfolding has_desc_fth_def
+ by auto
+
+ from `i < j` `j < k` have "i < k" by auto
+ hence "prod (?cp\<langle>i, k\<rangle>) = G"
+ proof (induct i rule:strict_inc_induct)
+ case 1 thus ?case by (simp add:sub_path_def)
+ next
+ case (2 i) thus ?case
+ by (simp add:sub_path_def upt_rec[of i k] idemp)
+ qed
+
+ with `i < j` `j < k` dfth Lemma7b
+ have "dsc G p p" by auto
+ with no_strict_arc have False by auto
+ thus ?thesis ..
+ qed
+next
+ assume "SCT' \<A>"
+
+ show "SCT \<A>"
+ proof (rule classical)
+ assume "\<not> SCT \<A>"
+
+ with SCT_def
+ obtain p
+ where ipath: "has_ipath \<A> p"
+ and no_desc_th: "\<not> (\<exists>\<theta>. is_desc_thread \<theta> p)"
+ by auto
+
+ from `bounded_acg P \<A>`
+ have "finite (dest_graph (tcl \<A>))" (is "finite ?AG")
+ by (intro bounded_finite bounded_plus)
+
+ from pdesc_acgplus[OF ipath]
+ have a: "\<And>x y. x<y \<Longrightarrow> pdesc p\<langle>x,y\<rangle> \<in> dest_graph (tcl \<A>)"
+ unfolding has_edge_def .
+
+ obtain S G
+ where "infinite S" "G \<in> dest_graph (tcl \<A>)"
+ and all_G: "\<And>x y. \<lbrakk> x \<in> S; y \<in> S; x < y\<rbrakk> \<Longrightarrow>
+ pdesc (p\<langle>x,y\<rangle>) = G"
+ apply (rule RamseyNatpairs[of ?AG "\<lambda>(x,y). pdesc p\<langle>x, y\<rangle>"])
+ apply (rule `finite (dest_graph (tcl \<A>))`)
+ by (simp only:split_conv, rule a, auto)
+
+ obtain n H m where
+ G_struct: "G = (n, H, m)" by (cases G) simp
+
+ let ?s = "enumerate S"
+ let ?q = "contract ?s p"
+
+ note all_in_S[simp] = enumerate_in_set[OF `infinite S`]
+ from `infinite S`
+ have inc[simp]: "increasing ?s"
+ unfolding increasing_def by (simp add:enumerate_mono)
+ note increasing_bij[OF this, simp]
+
+ from ipath_contract inc ipath
+ have "has_ipath (tcl \<A>) ?q" .
+
+ from all_G G_struct
+ have all_H: "\<And>i. (snd (?q i)) = H"
+ unfolding contract_def
+ by simp
+
+ have loop: "(tcl \<A>) \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
+ and idemp: "H * H = H"
+ proof -
+ let ?i = "?s 0" and ?j = "?s (Suc 0)" and ?k = "?s (Suc (Suc 0))"
+
+ have "pdesc (p\<langle>?i,?j\<rangle>) = G"
+ and "pdesc (p\<langle>?j,?k\<rangle>) = G"
+ and "pdesc (p\<langle>?i,?k\<rangle>) = G"
+ using all_G
+ by auto
+
+ with G_struct
+ have "m = end_node (p\<langle>?i,?j\<rangle>)"
+ "n = fst (p\<langle>?j,?k\<rangle>)"
+ and Hs: "prod (p\<langle>?i,?j\<rangle>) = H"
+ "prod (p\<langle>?j,?k\<rangle>) = H"
+ "prod (p\<langle>?i,?k\<rangle>) = H"
+ by auto
+
+ hence "m = n" by simp
+ thus "tcl \<A> \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n"
+ using G_struct `G \<in> dest_graph (tcl \<A>)`
+ by (simp add:has_edge_def)
+
+ from sub_path_prod[of ?i ?j ?k p]
+ show "H * H = H"
+ unfolding Hs by simp
+ qed
+ moreover have "\<And>k. \<not>dsc H k k"
+ proof
+ fix k :: nat assume "dsc H k k"
+
+ with all_H repeated_edge
+ have "\<exists>\<theta>. is_desc_thread \<theta> ?q" by fast
+ with inc have "\<exists>\<theta>. is_desc_thread \<theta> p"
+ by (subst contract_keeps_threads)
+ with no_desc_th
+ show False ..
+ qed
+ ultimately
+ have False
+ using `SCT' \<A>`[unfolded SCT'_def no_bad_graphs_def]
+ by blast
+ thus ?thesis ..
+ qed
+qed
+
+
+
+lemma LJA_apply:
+ assumes fin: "finite_acg A"
+ assumes "SCT' A"
+ shows "SCT A"
+proof -
+ from fin obtain P where b: "bounded_acg P A"
+ unfolding finite_acg_def ..
+ show ?thesis using LJA_Theorem4[OF b]
+ by simp
+qed
+
+
+
+
+
+
+end
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Size_Change_Termination.thy Mon Feb 26 21:34:16 2007 +0100
@@ -0,0 +1,104 @@
+theory Size_Change_Termination
+imports SCT_Theorem SCT_Interpretation SCT_Implementation
+uses "size_change_termination.ML"
+begin
+
+use "size_change_termination.ML"
+
+
+
+section {* Simplifier setup *}
+
+text {* This is needed to run the SCT algorithm in the simplifier: *}
+
+lemma setbcomp_simps:
+ "{x\<in>{}. P x} = {}"
+ "{x\<in>insert y ys. P x} = (if P y then insert y {x\<in>ys. P x} else {x\<in>ys. P x})"
+ by auto
+
+lemma setbcomp_cong:
+ "A = B \<Longrightarrow> (\<And>x. P x = Q x) \<Longrightarrow> {x\<in>A. P x} = {x\<in>B. Q x}"
+ by auto
+
+lemma cartprod_simps:
+ "{} \<times> A = {}"
+ "insert a A \<times> B = Pair a ` B \<union> (A \<times> B)"
+ by (auto simp:image_def)
+
+lemma image_simps:
+ "fu ` {} = {}"
+ "fu ` insert a A = insert (fu a) (fu ` A)"
+ by (auto simp:image_def)
+
+lemmas union_simps =
+ Un_empty_left Un_empty_right Un_insert_left
+
+lemma subset_simps:
+ "{} \<subseteq> B"
+ "insert a A \<subseteq> B \<equiv> a \<in> B \<and> A \<subseteq> B"
+ by auto
+
+lemma element_simps:
+ "x \<in> {} \<equiv> False"
+ "x \<in> insert a A \<equiv> x = a \<or> x \<in> A"
+ by auto
+
+lemma set_eq_simp:
+ "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" by auto
+
+lemma ball_simps:
+ "\<forall>x\<in>{}. P x \<equiv> True"
+ "(\<forall>x\<in>insert a A. P x) \<equiv> P a \<and> (\<forall>x\<in>A. P x)"
+by auto
+
+lemma bex_simps:
+ "\<exists>x\<in>{}. P x \<equiv> False"
+ "(\<exists>x\<in>insert a A. P x) \<equiv> P a \<or> (\<exists>x\<in>A. P x)"
+by auto
+
+lemmas set_simps =
+ setbcomp_simps
+ cartprod_simps image_simps union_simps subset_simps
+ element_simps set_eq_simp
+ ball_simps bex_simps
+
+lemma sedge_simps:
+ "\<down> * x = \<down>"
+ "\<Down> * x = x"
+ by (auto simp:mult_sedge_def)
+
+lemmas sctTest_simps =
+ simp_thms
+ if_True
+ if_False
+ nat.inject
+ nat.distinct
+ Pair_eq
+
+ grcomp_code
+ edges_match.simps
+ connect_edges.simps
+
+ sedge_simps
+ sedge.distinct
+ set_simps
+
+ graph_mult_def
+ graph_leq_def
+ dest_graph.simps
+ graph_plus_def
+ graph.inject
+ graph_zero_def
+
+ test_SCT_def
+ mk_tcl_code
+
+ Let_def
+ split_conv
+
+lemmas sctTest_congs =
+ if_weak_cong let_weak_cong setbcomp_cong
+
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/size_change_termination.ML Mon Feb 26 21:34:16 2007 +0100
@@ -0,0 +1,881 @@
+
+structure SCT = struct
+
+fun matrix [] ys = []
+ | matrix (x::xs) ys = map (pair x) ys :: matrix xs ys
+
+fun map_matrix f xss = map (map f) xss
+
+val scgT = Sign.read_typ (the_context (), K NONE) "scg"
+val acgT = Sign.read_typ (the_context (), K NONE) "acg"
+
+fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT))
+fun graphT nT eT = Type ("Graphs.graph", [nT, eT])
+
+fun graph_const nT eT = Const ("Graphs.graph.Graph", HOLogic.mk_setT (edgeT nT eT) --> graphT nT eT)
+
+
+val no_step_const = "SCT_Interpretation.no_step"
+val no_step_def = thm "SCT_Interpretation.no_step_def"
+val no_stepI = thm "SCT_Interpretation.no_stepI"
+
+fun mk_no_step RD1 RD2 =
+ let val RDT = fastype_of RD1
+ in Const (no_step_const, RDT --> RDT --> HOLogic.boolT) $ RD1 $ RD2 end
+
+val decr_const = "SCT_Interpretation.decr"
+val decr_def = thm "SCT_Interpretation.decr_def"
+
+fun mk_decr RD1 RD2 M1 M2 =
+ let val RDT = fastype_of RD1
+ val MT = fastype_of M1
+ in Const (decr_const, RDT --> RDT --> MT --> MT --> HOLogic.boolT) $ RD1 $ RD2 $ M1 $ M2 end
+
+val decreq_const = "SCT_Interpretation.decreq"
+val decreq_def = thm "SCT_Interpretation.decreq_def"
+
+fun mk_decreq RD1 RD2 M1 M2 =
+ let val RDT = fastype_of RD1
+ val MT = fastype_of M1
+ in Const (decreq_const, RDT --> RDT --> MT --> MT --> HOLogic.boolT) $ RD1 $ RD2 $ M1 $ M2 end
+
+val stepP_const = "SCT_Interpretation.stepP"
+val stepP_def = thm "SCT_Interpretation.stepP.simps"
+
+fun mk_stepP RD1 RD2 M1 M2 Rel =
+ let val RDT = fastype_of RD1
+ val MT = fastype_of M1
+ in
+ Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT)
+ $ RD1 $ RD2 $ M1 $ M2 $ Rel
+ end
+
+val approx_const = "SCT_Interpretation.approx"
+val approx_empty = thm "SCT_Interpretation.approx_empty"
+val approx_less = thm "SCT_Interpretation.approx_less"
+val approx_leq = thm "SCT_Interpretation.approx_leq"
+
+fun mk_approx G RD1 RD2 Ms1 Ms2 =
+ let val RDT = fastype_of RD1
+ val MsT = fastype_of Ms1
+ in Const (approx_const, scgT --> RDT --> RDT --> MsT --> MsT --> HOLogic.boolT) $ G $ RD1 $ RD2 $ Ms1 $ Ms2 end
+
+val sound_int_const = "SCT_Interpretation.sound_int"
+val sound_int_def = thm "SCT_Interpretation.sound_int_def"
+fun mk_sound_int A RDs M =
+ let val RDsT = fastype_of RDs
+ val MT = fastype_of M
+ in Const (sound_int_const, acgT --> RDsT --> MT --> HOLogic.boolT) $ A $ RDs $ M end
+
+
+val nth_const = "List.nth"
+fun mk_nth xs =
+ let val lT as Type (_, [T]) = fastype_of xs
+ in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end
+
+
+val less_nat_const = Const ("Orderings.less", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val lesseq_nat_const = Const ("Orderings.less_eq", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+
+
+(*
+val has_edge_const = "Graphs.has_edge"
+fun mk_has_edge G n e n' =
+ let val nT = fastype_of n and eT = fastype_of e
+ in Const (has_edge_const, graphT nT eT --> nT --> eT --> nT --> HOLogic.boolT) $ n $ e $ n' end
+*)
+
+
+val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
+
+val all_less_zero = thm "SCT_Interpretation.all_less_zero"
+val all_less_Suc = thm "SCT_Interpretation.all_less_Suc"
+
+
+
+(* Lists as finite multisets *)
+
+(* --> Library *)
+fun del_index n [] = []
+ | del_index n (x :: xs) =
+ if n>0 then x :: del_index (n - 1) xs else xs
+
+
+fun remove1 eq x [] = []
+ | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys
+
+
+fun multi_union eq [] ys = ys
+ | multi_union eq (x::xs) ys = x :: multi_union eq xs (remove1 eq x ys)
+
+
+fun dest_ex (Const ("Ex", _) $ Abs (a as (_,T,_))) =
+ let
+ val (n, body) = Term.dest_abs a
+ in
+ (Free (n, T), body)
+ end
+ | dest_ex _ = raise Match
+
+fun dest_all_ex (t as (Const ("Ex",_) $ _)) =
+ let
+ val (v,b) = dest_ex t
+ val (vs, b') = dest_all_ex b
+ in
+ (v :: vs, b')
+ end
+ | dest_all_ex t = ([],t)
+
+
+fun dist_vars [] vs = (assert (null vs) "dist_vars"; [])
+ | dist_vars (T::Ts) vs =
+ case find_index (fn v => fastype_of v = T) vs of
+ ~1 => Free ("", T) :: dist_vars Ts vs
+ | i => (nth vs i) :: dist_vars Ts (del_index i vs)
+
+
+fun dest_case rebind t =
+ let
+ val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t
+ val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs
+ in
+ foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match]
+ end
+
+fun bind_many [] = I
+ | bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
+
+(* Builds relation descriptions from a relation definition *)
+fun mk_reldescs (Abs a) =
+ let
+ val (_, Abs a') = Term.dest_abs a
+ val (_, b) = Term.dest_abs a'
+ val cases = HOLogic.dest_disj b
+ val (vss, bs) = split_list (map dest_all_ex cases)
+ val unionTs = fold (multi_union (op =)) (map (map fastype_of) vss) []
+ val rebind = map (bind_many o dist_vars unionTs) vss
+
+ val RDs = map2 dest_case rebind bs
+ in
+ HOLogic.mk_list (fastype_of (hd RDs)) RDs
+ end
+
+fun abs_rel_tac (st : thm) =
+ let
+ val thy = theory_of_thm st
+ val (def, rd) = HOLogic.dest_eq (HOLogic.dest_Trueprop (hd (prems_of st)))
+ val RDs = cterm_of thy (mk_reldescs def)
+ val rdvar = Var (the_single (Term.add_vars rd [])) |> cterm_of thy
+ in
+ Seq.single (cterm_instantiate [(rdvar, RDs)] st)
+ end
+
+
+(* very primitive *)
+fun measures_of RD =
+ let
+ val domT = range_type (fastype_of (fst (HOLogic.dest_prod (snd (HOLogic.dest_prod RD)))))
+ val measures = LexicographicOrder.mk_base_funs domT
+ in
+ measures
+ end
+
+
+
+val mk_number = HOLogic.mk_nat
+val dest_number = HOLogic.dest_nat
+
+fun nums_to i = map mk_number (0 upto (i - 1))
+
+
+fun unfold_then_auto thm =
+ (SIMPSET (unfold_tac [thm]))
+ THEN (CLASIMPSET auto_tac)
+
+val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"]
+val nth_ss = (HOL_basic_ss addsimps nth_simps)
+val simp_nth_tac = simp_tac nth_ss
+
+
+
+fun tabulate_tlist thy l =
+ let
+ val n = length (HOLogic.dest_list l)
+ 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))
+ in
+ the o Inttab.lookup table
+ end
+
+val get_elem = snd o Logic.dest_equals o prop_of
+
+
+(* Attempt a proof of a given goal *)
+
+datatype proof_result =
+ Success of thm
+ | Stuck of thm
+ | Fail
+ | False
+ | Timeout (* not implemented *)
+
+fun try_to_prove tactic cgoal =
+ case SINGLE tactic (Goal.init cgoal) of
+ NONE => Fail
+ | SOME st => if Thm.no_prems st
+ then Success (Goal.finish st)
+ else if prems_of st = [HOLogic.Trueprop $ HOLogic.false_const] then False
+ else Stuck st
+
+fun simple_result (Success thm) = SOME thm
+ | simple_result _ = NONE
+
+
+fun inst_nums thy i j (t:thm) =
+ instantiate' [] [NONE, NONE, NONE, SOME (cterm_of thy (mk_number i)), NONE, SOME (cterm_of thy (mk_number j))] t
+
+datatype call_fact =
+ NoStep of thm
+ | Graph of (term * thm)
+
+fun rand (_ $ t) = t
+
+fun setup_probe_goal thy domT Dtab Mtab (i, j) =
+ let
+ val RD1 = get_elem (Dtab i)
+ val RD2 = get_elem (Dtab j)
+ val Ms1 = get_elem (Mtab i)
+ val Ms2 = get_elem (Mtab j)
+
+ val Mst1 = HOLogic.dest_list (rand Ms1)
+ val Mst2 = HOLogic.dest_list (rand Ms2)
+
+ val mvar1 = Free ("sctmfv1", domT --> HOLogic.natT)
+ val mvar2 = Free ("sctmfv2", domT --> HOLogic.natT)
+ val relvar = Free ("sctmfrel", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+ val N = length Mst1 and M = length Mst2
+ val saved_state = HOLogic.mk_Trueprop (mk_stepP RD1 RD2 mvar1 mvar2 relvar)
+ |> cterm_of thy
+ |> Goal.init
+ |> CLASIMPSET auto_tac |> Seq.hd
+
+ val no_step = saved_state
+ |> forall_intr (cterm_of thy relvar)
+ |> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const))))
+ |> CLASIMPSET auto_tac |> Seq.hd
+
+ in
+ if Thm.no_prems no_step
+ then NoStep (Goal.finish no_step RS no_stepI)
+ else
+ let
+ fun set_m1 i =
+ let
+ val M1 = nth Mst1 i
+ val with_m1 = saved_state
+ |> forall_intr (cterm_of thy mvar1)
+ |> forall_elim (cterm_of thy M1)
+ |> CLASIMPSET auto_tac |> Seq.hd
+
+ fun set_m2 j =
+ let
+ val M2 = nth Mst2 j
+ val with_m2 = with_m1
+ |> forall_intr (cterm_of thy mvar2)
+ |> forall_elim (cterm_of thy M2)
+ |> CLASIMPSET auto_tac |> Seq.hd
+
+ val decr = forall_intr (cterm_of thy relvar)
+ #> forall_elim (cterm_of thy less_nat_const)
+ #> CLASIMPSET auto_tac #> Seq.hd
+
+ val decreq = forall_intr (cterm_of thy relvar)
+ #> forall_elim (cterm_of thy lesseq_nat_const)
+ #> CLASIMPSET auto_tac #> Seq.hd
+
+ val thm1 = decr with_m2
+ in
+ if Thm.no_prems thm1
+ then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm1) 1))
+ else let val thm2 = decreq with_m2 in
+ if Thm.no_prems thm2
+ then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm2) 1))
+ else all_tac end
+ end
+ in set_m2 end
+
+ val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2)
+
+ val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1)))
+ THEN (rtac approx_empty 1)
+
+ val approx_thm = goal
+ |> cterm_of thy
+ |> Goal.init
+ |> tac |> Seq.hd
+ |> Goal.finish
+
+ val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm
+ in
+ Graph (G, approx_thm)
+ end
+ end
+
+
+
+
+
+fun probe_nostep thy Dtab i j =
+ HOLogic.mk_Trueprop (mk_no_step (get_elem (Dtab i)) (get_elem (Dtab j)))
+ |> cterm_of thy
+ |> try_to_prove (unfold_then_auto no_step_def)
+ |> simple_result
+
+fun probe_decr thy RD1 RD2 m1 m2 =
+ HOLogic.mk_Trueprop (mk_decr RD1 RD2 m1 m2)
+ |> cterm_of thy
+ |> try_to_prove (unfold_then_auto decr_def)
+ |> simple_result
+
+fun probe_decreq thy RD1 RD2 m1 m2 =
+ HOLogic.mk_Trueprop (mk_decreq RD1 RD2 m1 m2)
+ |> cterm_of thy
+ |> try_to_prove (unfold_then_auto decreq_def)
+ |> simple_result
+
+
+fun pr_tac (st : thm) = Seq.single (Output.warning (PolyML.makestring st); st)
+fun pr_thm (st : thm) = (Output.warning (PolyML.makestring st); st)
+
+
+fun build_approximating_graph thy Dtab Mtab Mss mlens mint nint =
+ let
+ val D1 = Dtab mint and D2 = Dtab nint
+ val Mst1 = Mtab mint and Mst2 = Mtab nint
+
+ val RD1 = get_elem D1 and RD2 = get_elem D2
+ val Ms1 = get_elem Mst1 and Ms2 = get_elem Mst2
+
+ val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2)
+
+ val Ms1 = nth (nth Mss mint) and Ms2 = nth (nth Mss mint)
+
+ fun add_edge (i,j) =
+ case timeap_msg ("decr(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")")
+ (probe_decr thy RD1 RD2 (Ms1 i)) (Ms2 j) of
+ SOME thm => (Output.warning "Success"; (rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac thm 1))
+ | NONE => case timeap_msg ("decr(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")")
+ (probe_decreq thy RD1 RD2 (Ms1 i)) (Ms2 j) of
+ SOME thm => (Output.warning "Success"; (rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac thm 1))
+ | NONE => all_tac
+
+ val approx_thm =
+ goal
+ |> cterm_of thy
+ |> Goal.init
+ |> SINGLE ((EVERY (map add_edge (product (0 upto (nth mlens mint) - 1) (0 upto (nth mlens nint) - 1))))
+ THEN (rtac approx_empty 1))
+ |> the
+ |> Goal.finish
+
+ val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm
+ in
+ (G, approx_thm)
+ end
+
+
+
+fun prove_call_fact thy Dtab Mtab Mss mlens (m, n) =
+ case probe_nostep thy Dtab m n of
+ SOME thm => (Output.warning "NoStep"; NoStep thm)
+ | NONE => Graph (build_approximating_graph thy Dtab Mtab Mss mlens m n)
+
+
+fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n))
+
+
+fun mk_set T [] = Const ("{}", HOLogic.mk_setT T)
+ | mk_set T (x :: xs) = Const ("insert",
+ T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $ mk_set T xs
+
+fun dest_set (Const ("{}", _)) = []
+ | dest_set (Const ("insert", _) $ x $ xs) = x :: dest_set xs
+
+val pr_graph = Sign.string_of_term
+
+
+fun pr_matrix thy = map_matrix (fn Graph (G, _) => pr_graph thy G | _ => "X")
+
+val in_graph_tac =
+ simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
+ THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *)
+
+fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
+ | approx_tac (Graph (G, thm)) =
+ rtac disjI2 1
+ THEN rtac exI 1
+ THEN rtac conjI 1
+ THEN rtac thm 2
+ THEN in_graph_tac
+
+fun all_less_tac [] = rtac all_less_zero 1
+ | all_less_tac (t :: ts) = rtac all_less_Suc 1
+ THEN simp_nth_tac 1
+ THEN t
+ THEN all_less_tac ts
+
+
+val length_const = "Nat.size"
+fun mk_length l = Const (length_const, fastype_of l --> HOLogic.natT) $ l
+val length_simps = thms "SCT_Interpretation.length_simps"
+
+
+
+fun mk_call_graph (st : thm) =
+ let
+ val thy = theory_of_thm st
+ val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
+
+ val RDs = HOLogic.dest_list RDlist
+ val n = length RDs
+
+ val Mss = map measures_of RDs
+
+ val domT = domain_type (fastype_of (hd (hd Mss)))
+
+ val mfuns = map (fn Ms => mk_nth (HOLogic.mk_list (fastype_of (hd Ms)) Ms)) Mss
+ |> (fn l => HOLogic.mk_list (fastype_of (hd l)) l)
+
+ val Dtab = tabulate_tlist thy RDlist
+ val Mtab = tabulate_tlist thy mfuns
+
+ val len_simp = Simplifier.rewrite (HOL_basic_ss addsimps length_simps) (cterm_of thy (mk_length RDlist))
+
+ val mlens = map length Mss
+
+ val indices = (n - 1 downto 0)
+ val pairs = matrix indices indices
+ val parts = map_matrix (fn (n,m) =>
+ (timeap_msg (string_of_int n ^ "," ^ string_of_int m)
+ (setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs
+
+
+ val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^
+ pr_graph thy G ^ ",\n")
+ | _ => I) cs) parts ""
+ val _ = Output.warning s
+
+
+ val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs)
+ |> mk_set (edgeT HOLogic.natT scgT)
+ |> curry op $ (graph_const HOLogic.natT scgT)
+
+
+ val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns)
+
+ val tac =
+ (SIMPSET (unfold_tac [sound_int_def, len_simp]))
+ THEN all_less_tac (map (all_less_tac o map approx_tac) parts)
+ in
+ tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
+ end
+
+
+
+
+
+
+
+
+
+
+
+
+(* Faster implementation of transitive closures *)
+
+(* sedge: Only relevant edges. Qtrees have separate value for 0 *)
+datatype sedge = LESS | LEQ | BOTH
+
+
+
+datatype key = KHere | K0 of key | K1 of key
+
+datatype 'a stree =
+ sLeaf of 'a
+ | sBranch of ('a * 'a stree * 'a stree)
+
+(*
+fun lookup (sLeaf x) KHere = x
+ | lookup (sBranch x s t) KHere = x
+ | lookup (sBranch x s t) (K0 k) = lookup s k
+ | lookup (sBranch x s t) (K1 k) = lookup t k
+ | lookup _ _ = raise Match
+*)
+
+datatype 'a qtree =
+ QEmpty
+ | QNode of 'a
+ | QQuad of ('a qtree * 'a qtree * 'a qtree * 'a qtree)
+
+fun qlookup z QEmpty k l = z
+ | qlookup z (QNode S) k l = S
+ | qlookup z (QQuad (a, b, c, d)) (K0 k) (K0 l) = qlookup z a k l
+ | qlookup z (QQuad (a, b, c, d)) (K0 k) (K1 l) = qlookup z b k l
+ | qlookup z (QQuad (a, b, c, d)) (K1 k) (K0 l) = qlookup z c k l
+ | qlookup z (QQuad (a, b, c, d)) (K1 k) (K1 l) = qlookup z d k l
+ | qlookup _ _ _ _ = raise Match
+
+
+
+(* Size-change graphs *)
+
+type
+ scg = sedge qtree
+
+
+(* addition of single edges *)
+fun add_sedge BOTH _ = BOTH
+ | add_sedge LESS LESS = LESS
+ | add_sedge LESS _ = BOTH
+ | add_sedge LEQ LEQ = LEQ
+ | add_sedge LEQ _ = BOTH
+
+fun mult_sedge LESS _ = LESS
+ | mult_sedge _ LESS = LESS
+ | mult_sedge LEQ x = x
+ | mult_sedge BOTH _ = BOTH
+
+fun subsumes_edge LESS LESS = true
+ | subsumes_edge LEQ _ = true
+ | subsumes_edge _ _ = false
+
+
+
+
+(* subsumes_SCG G H := G contains strictly less estimations than H *)
+fun subsumes_SCG (QEmpty : scg) (H : scg) = true
+ | subsumes_SCG (QQuad (a, b, c, d)) (QQuad (e,f,g,h)) =
+ (subsumes_SCG a e) andalso (subsumes_SCG b f)
+ andalso (subsumes_SCG c g) andalso (subsumes_SCG d h)
+ | subsumes_SCG (QNode e) (QNode e') = subsumes_edge e e'
+ | subsumes_SCG _ QEmpty = false
+ | subsumes_SCG _ _ = raise Match
+
+
+(* managing lists of SCGs. *)
+
+(*
+ Graphs are partially ordered. A list of graphs has the invariant that no G,H with G <= H.
+ To maintain this when adding a new graph G, check
+ (1) G <= H for some H in l => Do nothing
+ (2) has to be added. Then, all H <= G can be removed.
+
+ We can check (2) first, removing all smaller graphs.
+ If we could remove at least one, just add G in the end (Invariant!).
+ Otherwise, check again, if G needs to be added at all.
+
+ OTOH, doing (1) first is probably better, because it does not produce garbage unless needed.
+
+ The definition is tail-recursive. Order is not preserved (unneccessary).
+*)
+
+
+
+fun add_scg' G Hs = (* returns a flag indicating if the graph was really added *)
+ if exists (fn H => subsumes_SCG H G) Hs then (false, Hs) (* redundant addition *)
+ else (true, G :: remove (uncurry subsumes_SCG) G Hs) (* remove all new redundancy and add G *)
+ (* NB: This does the second checks twice :-( *)
+
+(* Simpler version *)
+fun add_scg' G Hs = (not (member (op =) Hs G), insert (op =) G Hs)
+
+
+val add_scg = snd oo add_scg' (* without flag *)
+
+
+
+
+
+(* quadtrees *)
+
+fun keylen 0 = 0
+ | keylen n = (keylen (n div 2)) + 1
+
+fun mk_key 0 _ = KHere
+ | mk_key l m = if m mod 2 = 0
+ then K0 (mk_key (l - 1) (m div 2))
+ else K1 (mk_key (l - 1) (m div 2))
+
+
+fun qupdate f KHere KHere n = f n
+ | qupdate f (K0 k) (K0 k') (QQuad (a, b, c, d)) = QQuad (qupdate f k k' a, b, c, d)
+ | qupdate f (K0 k) (K1 k') (QQuad (a, b, c, d)) = QQuad (a, qupdate f k k' b, c, d)
+ | qupdate f (K1 k) (K0 k') (QQuad (a, b, c, d)) = QQuad (a, b, qupdate f k k' c, d)
+ | qupdate f (K1 k) (K1 k') (QQuad (a, b, c, d)) = QQuad (a, b, c, qupdate f k k' d)
+
+
+
+
+
+
+
+
+(* quadtree composition *)
+
+fun qadd A QEmpty q = q
+ | qadd A q QEmpty = q
+ | qadd A (QNode s) (QNode t) = QNode (A s t)
+ | qadd A (QQuad (a, b, c, d)) (QQuad (e, f, g, h)) =
+ QQuad (qadd A a e, qadd A b f, qadd A c g, qadd A d h)
+ | qadd _ _ _ = raise Match
+
+
+fun qmult A m QEmpty H = QEmpty
+ | qmult A m G QEmpty = QEmpty
+ | qmult A m (QNode x) (QNode y) = QNode (m x y)
+ | qmult A m (QQuad (a, b, c, d)) (QQuad (e, f, g, h)) =
+ QQuad ((qadd A (qmult A m a e) (qmult A m b g)),
+ (qadd A (qmult A m a f) (qmult A m b h)),
+ (qadd A (qmult A m c e) (qmult A m d g)),
+ (qadd A (qmult A m c f) (qmult A m d h)))
+ | qmult _ _ _ _ = raise Match
+
+
+val (mult_scg : scg -> scg -> scg) = qmult add_sedge mult_sedge
+
+(* Misc notes:
+
+- When building the tcl: Check on addition and raise FAIL if the property is not true... (pract)
+
+- Can we reduce subsumption checking by some integer fingerprints?
+
+ Number of edges: LESS(G) LEQ(G)
+ G <= H ==> E(G) <= E(H)
+
+
+
+How to check:
+
+For each pair of adjacent edges: n -> m -> q
+ compute all product SCGS and check if they are subsumed by something in the tcl.
+
+ all midnode m: all fromnode n: all tonode q: alledges (n,m) e: alledges (m,q) e': subsumes (e*e') (edgs m,q)
+
+ This is still quite a lot of checking... But: no garbage, just inspection. Can probably be done in logic.
+
+*)
+
+
+
+(* Operations on lists: These preserve the invariants *)
+fun SCGs_mult Gs Hs = fold (fn (G,H) => add_scg (mult_scg G H)) (product Gs Hs) []
+val SCGs_plus = fold add_scg
+
+
+fun add_scgs Gs Hs = fold_rev (fn G => fn (Xs,As) =>
+ let val (b, Xs') = add_scg' G Xs
+ in (Xs', if b then G::As else As) end)
+ Gs (Hs,[])
+
+(* Transitive Closure for lists of SCGs *)
+fun SCGs_tcl Gs =
+ let
+ fun aux S [] = S
+ | aux S (H::HS) =
+ let val (S', Ns) = add_scgs (map (mult_scg H) Gs) S
+ in aux S' (SCGs_plus Ns HS) end
+ in
+ aux Gs Gs
+ end
+
+
+
+(* Kleene algorithm: DP version, with imperative array... *)
+
+
+
+
+(* Terrible imperative stuff: *)
+type matrix = scg list array array
+
+fun mupdate i j f M =
+ let
+ val row = Array.sub (M, i)
+ val x = Array.sub (row, j)
+ in
+ Array.update (row, j, f x)
+ end
+
+fun mget i j M = Array.sub(Array.sub(M,i),j)
+
+fun print_scg (x : scg) = Output.warning (PolyML.makestring x);
+
+
+fun kleene add mult tcl M =
+ let
+ val n = Array.length M
+
+ fun update Mkk i j k =
+ let
+ val Mik = mget i k M
+ val Mkj = mget k j M
+ in
+ mupdate i j (fn X => X |> add (mult Mik (mult Mkk Mkj))
+ |> add (mult Mik Mkj))
+ M
+ end
+
+ fun step k () =
+ let
+ val _ = mupdate k k tcl M
+ val Mkk = mget k k M
+
+ val no_k = filter_out (fn i => i = k) (0 upto (n - 1))
+ val _ = fold (fn i => fold (fn j => K (update Mkk i j k)) no_k) no_k ()
+
+ val _ = fold (fn i => K (update Mkk i k k)) no_k ()
+
+ val _ = fold (fn j => K (update Mkk k j k)) no_k ()
+ in
+ ()
+ end
+ in
+ fold step (0 upto (n - 1)) ()
+ end
+
+val (SCGs_kleene : matrix -> unit) = kleene SCGs_plus SCGs_mult SCGs_tcl
+
+
+fun andop x y = x andalso y
+fun orop x y = x orelse y
+
+fun array2 n x = Array.tabulate (n, (fn i => Array.array (n, x)))
+
+(*val bool_kleene = kleene orop andop I
+
+
+fun test_bool () =
+ let
+ val M = array2 2 false
+ val _ = mupdate 0 1 (K true) M
+ val _ = mupdate 1 0 (K true) M
+ val _ = bool_kleene M
+ in
+ M
+ end
+*)
+
+(* Standard 2-2-Size-change graphs *)
+
+val swap = QQuad(QEmpty, QNode LEQ,
+ QNode LEQ, QEmpty)
+
+val swapRTop = QQuad(QNode LESS, QNode LEQ,
+ QNode LEQ, QEmpty)
+
+val BTopRBot = QQuad(QNode LEQ, QEmpty,
+ QEmpty, QNode LESS)
+
+val RTopBBot = QQuad(QNode LESS, QEmpty,
+ QEmpty, QNode LEQ)
+
+val R2Straight = QQuad(QNode LESS, QEmpty,
+ QEmpty, QNode LESS)
+
+val R3StraightUp = QQuad(QNode LESS, QEmpty,
+ QNode LESS, QNode LESS)
+
+val R3StraightDn = QQuad(QNode LESS, QNode LESS,
+ QEmpty, QNode LESS)
+
+
+
+
+val diag = QQuad(QEmpty, QNode LEQ,
+ QEmpty, QEmpty)
+
+val straight = QQuad(QNode LEQ, QEmpty,
+ QEmpty, QEmpty)
+
+
+
+val R467913 = ([R2Straight, R3StraightDn, R3StraightDn] @ replicate 11 R2Straight @ [R3StraightUp, R3StraightUp])
+ |> map single
+
+val swapPos = [(0,8),(0,9),(0,10),(3,4),(3,5),(11,12)]
+
+val BRPos = (map (pair 5) (0 :: (3 upto 7)))
+ @ (map (pair 8) [8,9,11,12,13])
+ @ (map (pair 12) [8,9,11,12,13])
+
+val RBPos = map (pair 10) (3 upto 10)
+
+fun afold f arr x = Array.foldl (uncurry f) x arr
+
+fun msize M = afold (afold (curry op + o length)) M 0
+
+fun TestM () =
+ let
+ val M = array2 16 ([] : scg list)
+ val _ = Array.update (M, 4, Array.fromList R467913)
+ val _ = Array.update (M, 6, Array.fromList R467913)
+ val _ = Array.update (M, 7, Array.fromList R467913)
+ val _ = Array.update (M, 9, Array.fromList R467913)
+ val _ = Array.update (M, 13, Array.fromList R467913)
+
+ val _ = map (fn (i,j) => mupdate i j (K [swap]) M) swapPos
+ val _ = map (fn (i,j) => mupdate i j (K [BTopRBot]) M) BRPos
+ val _ = map (fn (i,j) => mupdate i j (K [RTopBBot]) M) RBPos
+
+ val _ = mupdate 1 14 (K [swapRTop]) M
+ val _ = mupdate 2 15 (K [swapRTop]) M
+
+ val G = [QQuad (QNode LEQ, QNode LESS, QEmpty, QNode LESS)]
+ val _ = mupdate 5 1 (K G) M
+ val _ = mupdate 8 2 (K G) M
+ val _ = mupdate 12 2 (K G) M
+
+ val G = [QQuad (QNode LESS, QEmpty, QNode LESS, QNode LEQ)]
+ val _ = mupdate 10 14 (K G) M
+
+ val G = [QQuad (QEmpty, QNode LEQ, QNode LESS, QNode LESS)]
+ val _ = mupdate 14 1 (K G) M
+ val _ = mupdate 14 2 (K G) M
+ val _ = mupdate 15 1 (K G) M
+ val _ = mupdate 15 2 (K G) M
+ in
+ M
+ end
+
+
+
+
+
+fun add_edge x QEmpty = QNode x
+ | add_edge x (QNode y) = QNode (add_sedge x y)
+
+
+fun sedge2ML (Const ("SCT_Definition.sedge.LESS", _)) = LESS
+ | sedge2ML (Const ("SCT_Definition.sedge.LEQ", _)) = LEQ
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+end
+
+
+
+
+
+