removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)
--- a/src/HOL/IsaMakefile Fri Nov 06 13:36:46 2009 +0100
+++ b/src/HOL/IsaMakefile Fri Nov 06 13:42:29 2009 +0100
@@ -57,7 +57,6 @@
HOL-Prolog \
HOL-SET_Protocol \
HOL-SMT-Examples \
- HOL-SizeChange \
HOL-Statespace \
HOL-Subst \
TLA-Buffer \
@@ -766,19 +765,6 @@
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
-## HOL-SizeChange
-
-HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz
-
-$(LOG)/HOL-SizeChange.gz: $(OUT)/HOL Library/Kleene_Algebra.thy \
- SizeChange/Graphs.thy SizeChange/Misc_Tools.thy \
- SizeChange/Criterion.thy SizeChange/Correctness.thy \
- SizeChange/Interpretation.thy SizeChange/Implementation.thy \
- SizeChange/Size_Change_Termination.thy SizeChange/Examples.thy \
- SizeChange/sct.ML SizeChange/ROOT.ML
- @$(ISABELLE_TOOL) usedir $(OUT)/HOL SizeChange
-
-
## HOL-Decision_Procs
HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz
@@ -1443,7 +1429,7 @@
$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz \
$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz \
$(LOG)/HOL-SET_Protocol.gz $(LOG)/HOL-SMT-Examples.gz \
- $(LOG)/HOL-SMT.gz $(LOG)/HOL-SizeChange.gz \
+ $(LOG)/HOL-SMT.gz \
$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \
$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \
$(LOG)/HOL-W0.gz $(LOG)/HOL-Word-Examples.gz \
--- a/src/HOL/SizeChange/Correctness.thy Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1450 +0,0 @@
-(* Title: HOL/Library/SCT_Theorem.thy
- Author: Alexander Krauss, TU Muenchen
-*)
-
-header "Proof of the Size-Change Principle"
-
-theory Correctness
-imports Main Ramsey Misc_Tools Criterion
-begin
-
-subsection {* Auxiliary definitions *}
-
-definition is_thread :: "nat \<Rightarrow> 'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> bool"
-where
- "is_thread n \<theta> p = (\<forall>i\<ge>n. eqlat p \<theta> i)"
-
-definition is_fthread ::
- "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
-where
- "is_fthread \<theta> mp i j = (\<forall>k\<in>{i..<j}. eqlat mp \<theta> k)"
-
-definition is_desc_fthread ::
- "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
-where
- "is_desc_fthread \<theta> mp i j =
- (is_fthread \<theta> mp i j \<and>
- (\<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)"
-
-
-subsection {* Everything is finite *}
-
-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 INFM_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 range_composition)
- 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 finite_range_ignore_prefix:
- fixes f :: "nat \<Rightarrow> 'a"
- assumes fA: "finite A"
- assumes inA: "\<forall>x\<ge>n. f x \<in> A"
- shows "finite (range f)"
-proof -
- have a: "UNIV = {0 ..< (n::nat)} \<union> { x. n \<le> x }" by auto
- have b: "range f = f ` {0 ..< n} \<union> f ` { x. n \<le> x }"
- (is "\<dots> = ?A \<union> ?B")
- by (unfold a) (simp add:image_Un)
-
- have "finite ?A" by (rule finite_imageI) simp
- moreover
- from inA have "?B \<subseteq> A" by auto
- from this fA have "finite ?B" by (rule finite_subset)
- ultimately show ?thesis using b by simp
-qed
-
-
-
-
-definition
- "finite_graph G = finite (dest_graph G)"
-definition
- "all_finite G = (\<forall>n H m. has_edge G n H m \<longrightarrow> finite_graph H)"
-definition
- "finite_acg A = (finite_graph A \<and> all_finite A)"
-definition
- "nodes G = fst ` dest_graph G \<union> snd ` snd ` dest_graph G"
-definition
- "edges G = fst ` snd ` dest_graph G"
-definition
- "smallnodes G = \<Union>(nodes ` edges G)"
-
-lemma thread_image_nodes:
- assumes th: "is_thread n \<theta> p"
- shows "\<forall>i\<ge>n. \<theta> i \<in> nodes (snd (p i))"
-using prems
-unfolding is_thread_def has_edge_def nodes_def
-by force
-
-lemma finite_nodes: "finite_graph G \<Longrightarrow> finite (nodes G)"
- unfolding finite_graph_def nodes_def
- by auto
-
-lemma nodes_subgraph: "A \<le> B \<Longrightarrow> nodes A \<subseteq> nodes B"
- unfolding graph_leq_def nodes_def
- by auto
-
-lemma finite_edges: "finite_graph G \<Longrightarrow> finite (edges G)"
- unfolding finite_graph_def edges_def
- by auto
-
-lemma edges_sum[simp]: "edges (A + B) = edges A \<union> edges B"
- unfolding edges_def graph_plus_def
- by auto
-
-lemma nodes_sum[simp]: "nodes (A + B) = nodes A \<union> nodes B"
- unfolding nodes_def graph_plus_def
- by auto
-
-lemma finite_acg_subset:
- "A \<le> B \<Longrightarrow> finite_acg B \<Longrightarrow> finite_acg A"
- unfolding finite_acg_def finite_graph_def all_finite_def
- has_edge_def graph_leq_def
- by (auto elim:finite_subset)
-
-lemma scg_finite:
- fixes G :: "'a scg"
- assumes fin: "finite (nodes G)"
- shows "finite_graph G"
- unfolding finite_graph_def
-proof (rule finite_subset)
- show "dest_graph G \<subseteq> nodes G \<times> UNIV \<times> nodes G" (is "_ \<subseteq> ?P")
- unfolding nodes_def
- by force
- show "finite ?P"
- by (intro finite_cartesian_product fin finite)
-qed
-
-lemma smallnodes_sum[simp]:
- "smallnodes (A + B) = smallnodes A \<union> smallnodes B"
- unfolding smallnodes_def
- by auto
-
-lemma in_smallnodes:
- fixes A :: "'a acg"
- assumes e: "has_edge A x G y"
- shows "nodes G \<subseteq> smallnodes A"
-proof -
- have "fst (snd (x, G, y)) \<in> fst ` snd ` dest_graph A"
- unfolding has_edge_def
- by (rule imageI)+ (rule e[unfolded has_edge_def])
- then have "G \<in> edges A"
- unfolding edges_def by simp
- thus ?thesis
- unfolding smallnodes_def
- by blast
-qed
-
-lemma finite_smallnodes:
- assumes fA: "finite_acg A"
- shows "finite (smallnodes A)"
- unfolding smallnodes_def edges_def
-proof
- from fA
- show "finite (nodes ` fst ` snd ` dest_graph A)"
- unfolding finite_acg_def finite_graph_def
- by simp
-
- fix M assume "M \<in> nodes ` fst ` snd ` dest_graph A"
- then obtain n G m
- where M: "M = nodes G" and nGm: "(n,G,m) \<in> dest_graph A"
- by auto
-
- from fA
- have "all_finite A" unfolding finite_acg_def by simp
- with nGm have "finite_graph G"
- unfolding all_finite_def has_edge_def by auto
- with finite_nodes
- show "finite M"
- unfolding finite_graph_def M .
-qed
-
-lemma nodes_tcl:
- "nodes (tcl A) = nodes A"
-proof
- show "nodes A \<subseteq> nodes (tcl A)"
- apply (rule nodes_subgraph)
- by (subst tcl_unfold_right) simp
-
- show "nodes (tcl A) \<subseteq> nodes A"
- proof
- fix x assume "x \<in> nodes (tcl A)"
- then obtain z G y
- where z: "z \<in> dest_graph (tcl A)"
- and dis: "z = (x, G, y) \<or> z = (y, G, x)"
- unfolding nodes_def
- by auto force+
-
- from dis
- show "x \<in> nodes A"
- proof
- assume "z = (x, G, y)"
- with z have "has_edge (tcl A) x G y" unfolding has_edge_def by simp
- then obtain n where "n > 0 " and An: "has_edge (A ^ n) x G y"
- unfolding in_tcl by auto
- then obtain n' where "n = Suc n'" by (cases n, auto)
- hence "A ^ n = A * A ^ n'" by (simp add:power_Suc)
- with An obtain e k
- where "has_edge A x e k" by (auto simp:in_grcomp)
- thus "x \<in> nodes A" unfolding has_edge_def nodes_def
- by force
- next
- assume "z = (y, G, x)"
- with z have "has_edge (tcl A) y G x" unfolding has_edge_def by simp
- then obtain n where "n > 0 " and An: "has_edge (A ^ n) y G x"
- unfolding in_tcl by auto
- then obtain n' where "n = Suc n'" by (cases n, auto)
- hence "A ^ n = A ^ n' * A" by (simp add:power_Suc power_commutes)
- with An obtain e k
- where "has_edge A k e x" by (auto simp:in_grcomp)
- thus "x \<in> nodes A" unfolding has_edge_def nodes_def
- by force
- qed
- qed
-qed
-
-lemma smallnodes_tcl:
- fixes A :: "'a acg"
- shows "smallnodes (tcl A) = smallnodes A"
-proof (intro equalityI subsetI)
- fix n assume "n \<in> smallnodes (tcl A)"
- then obtain x G y where edge: "has_edge (tcl A) x G y"
- and "n \<in> nodes G"
- unfolding smallnodes_def edges_def has_edge_def
- by auto
-
- from `n \<in> nodes G`
- have "n \<in> fst ` dest_graph G \<or> n \<in> snd ` snd ` dest_graph G"
- (is "?A \<or> ?B")
- unfolding nodes_def by blast
- thus "n \<in> smallnodes A"
- proof
- assume ?A
- then obtain m e where A: "has_edge G n e m"
- unfolding has_edge_def by auto
-
- have "tcl A = A * star A"
- unfolding tcl_def
- by (simp add: star_simulation[of A A A, simplified])
-
- with edge
- have "has_edge (A * star A) x G y" by simp
- then obtain H H' z
- where AH: "has_edge A x H z" and G: "G = H * H'"
- by (auto simp:in_grcomp)
- from A
- obtain m' e' where "has_edge H n e' m'"
- by (auto simp:G in_grcomp)
- hence "n \<in> nodes H" unfolding nodes_def has_edge_def
- by force
- with in_smallnodes[OF AH] show "n \<in> smallnodes A" ..
- next
- assume ?B
- then obtain m e where B: "has_edge G m e n"
- unfolding has_edge_def by auto
-
- with edge
- have "has_edge (star A * A) x G y" by (simp add:tcl_def)
- then obtain H H' z
- where AH': "has_edge A z H' y" and G: "G = H * H'"
- by (auto simp:in_grcomp simp del: star_slide2)
- from B
- obtain m' e' where "has_edge H' m' e' n"
- by (auto simp:G in_grcomp)
- hence "n \<in> nodes H'" unfolding nodes_def has_edge_def
- by force
- with in_smallnodes[OF AH'] show "n \<in> smallnodes A" ..
- qed
-next
- fix x assume "x \<in> smallnodes A"
- then show "x \<in> smallnodes (tcl A)"
- by (subst tcl_unfold_right) simp
-qed
-
-lemma finite_nodegraphs:
- assumes F: "finite F"
- shows "finite { G::'a scg. nodes G \<subseteq> F }" (is "finite ?P")
-proof (rule finite_subset)
- show "?P \<subseteq> Graph ` (Pow (F \<times> UNIV \<times> F))" (is "?P \<subseteq> ?Q")
- proof
- fix x assume xP: "x \<in> ?P"
- obtain S where x[simp]: "x = Graph S"
- by (cases x) auto
- from xP
- show "x \<in> ?Q"
- apply (simp add:nodes_def)
- apply (rule imageI)
- apply (rule PowI)
- apply force
- done
- qed
- show "finite ?Q"
- by (auto intro:finite_imageI finite_cartesian_product F finite)
-qed
-
-lemma finite_graphI:
- fixes A :: "'a acg"
- assumes fin: "finite (nodes A)" "finite (smallnodes A)"
- shows "finite_graph A"
-proof -
- obtain S where A[simp]: "A = Graph S"
- by (cases A) auto
-
- have "finite S"
- proof (rule finite_subset)
- show "S \<subseteq> nodes A \<times> { G::'a scg. nodes G \<subseteq> smallnodes A } \<times> nodes A"
- (is "S \<subseteq> ?T")
- proof
- fix x assume xS: "x \<in> S"
- obtain a b c where x[simp]: "x = (a, b, c)"
- by (cases x) auto
-
- then have edg: "has_edge A a b c"
- unfolding has_edge_def using xS
- by simp
-
- hence "a \<in> nodes A" "c \<in> nodes A"
- unfolding nodes_def has_edge_def by force+
- moreover
- from edg have "nodes b \<subseteq> smallnodes A" by (rule in_smallnodes)
- hence "b \<in> { G :: 'a scg. nodes G \<subseteq> smallnodes A }" by simp
- ultimately show "x \<in> ?T" by simp
- qed
-
- show "finite ?T"
- by (intro finite_cartesian_product fin finite_nodegraphs)
- qed
- thus ?thesis
- unfolding finite_graph_def by simp
-qed
-
-
-lemma smallnodes_allfinite:
- fixes A :: "'a acg"
- assumes fin: "finite (smallnodes A)"
- shows "all_finite A"
- unfolding all_finite_def
-proof (intro allI impI)
- fix n H m assume "has_edge A n H m"
- then have "nodes H \<subseteq> smallnodes A"
- by (rule in_smallnodes)
- then have "finite (nodes H)"
- by (rule finite_subset) (rule fin)
- thus "finite_graph H" by (rule scg_finite)
-qed
-
-lemma finite_tcl:
- fixes A :: "'a acg"
- shows "finite_acg (tcl A) \<longleftrightarrow> finite_acg A"
-proof
- assume f: "finite_acg A"
- from f have g: "finite_graph A" and "all_finite A"
- unfolding finite_acg_def by auto
-
- from g have "finite (nodes A)" by (rule finite_nodes)
- then have "finite (nodes (tcl A))" unfolding nodes_tcl .
- moreover
- from f have "finite (smallnodes A)" by (rule finite_smallnodes)
- then have fs: "finite (smallnodes (tcl A))" unfolding smallnodes_tcl .
- ultimately
- have "finite_graph (tcl A)" by (rule finite_graphI)
-
- moreover from fs have "all_finite (tcl A)"
- by (rule smallnodes_allfinite)
- ultimately show "finite_acg (tcl A)" unfolding finite_acg_def ..
-next
- assume a: "finite_acg (tcl A)"
- have "A \<le> tcl A" by (rule less_tcl)
- thus "finite_acg A" using a
- by (rule finite_acg_subset)
-qed
-
-lemma finite_acg_empty: "finite_acg (Graph {})"
- unfolding finite_acg_def finite_graph_def all_finite_def
- has_edge_def
- by simp
-
-lemma finite_acg_ins:
- assumes fA: "finite_acg (Graph A)"
- assumes fG: "finite G"
- shows "finite_acg (Graph (insert (a, Graph G, b) A))"
- using fA fG
- unfolding finite_acg_def finite_graph_def all_finite_def
- has_edge_def
- by auto
-
-lemmas finite_acg_simps = finite_acg_empty finite_acg_ins finite_graph_def
-
-subsection {* 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> (eqp 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:
- "i \<le> j \<Longrightarrow> has_fth p i j m n = eql (prod (p\<langle>i,j\<rangle>)) m n"
-proof (induct i arbitrary: m rule:inc_induct)
- case base show ?case
- unfolding has_fth_def is_fthread_def sub_path_def
- by (auto simp:in_grunit one_sedge_def)
-next
- case (step 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 base show ?case
- unfolding has_desc_fth_def is_desc_fthread_def sub_path_def
- by (auto simp:in_grunit one_sedge_def)
-next
- case (step 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)
-
-
-subsubsection {* 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 \<theta> p] fths
- show "\<forall>i\<ge>s (Suc n). eqlat p \<theta> i"
- by (fold is_thread_def) simp
-
- show "\<exists>\<^sub>\<infinity>l. descat p \<theta> l"
- unfolding INFM_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 INFM_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) simp
- also have "\<dots> \<le> s j"
- by (rule increasing_weak [OF `increasing s`]) (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 INFM_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 INFM_drop_prefix:
- "(\<exists>\<^sub>\<infinity>i::nat. i > n \<and> P i) = (\<exists>\<^sub>\<infinity>i. P i)"
- apply (auto simp:INFM_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 INFM_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 INFM_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) simp
- note `s (Suc ?K) < j`
- also have "j < s (Suc ?L)"
- by (rule section_of2) simp
- 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:INFM_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 INFM_drop_prefix .
-
- hence p2: "\<exists>\<^sub>\<infinity>i. is_desc_fthread ?j\<theta> p (s i) (s (Suc i))"
- apply (rule INFM_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"
-proof-
- have th: "\<forall> m. \<exists>na>m. n < na" by arith
- show ?thesis using prems
- unfolding is_desc_thread_def
- apply (auto)
- apply (rule_tac x="Suc n" in exI, auto)
- apply (rule INFM_mono[where P="\<lambda>i. n < i"])
- apply (simp only:INFM_nat)
- by (auto simp add: th)
-qed
-
-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
-
-
-subsection {* 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 "finite S"
- shows "set (set2list S) = S"
- unfolding set2list_def
-proof (rule f_inv_into_f)
- from `finite S` have "\<exists>l. set l = S"
- by (rule finite_list)
- 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: "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 using i
- 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
-
-
-subsection {* Main Result *}
-
-
-theorem LJA_Theorem4:
- assumes "finite_acg 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::nat. (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 "finite (range \<theta>)"
- proof (rule finite_range_ignore_prefix)
-
- from `finite_acg A`
- have "finite_acg (tcl A)" by (simp add:finite_tcl)
- with in_closure have "finite_graph G"
- unfolding finite_acg_def all_finite_def by blast
- thus "finite (nodes G)" by (rule finite_nodes)
-
- from thread_image_nodes[OF thr]
- show "\<forall>i\<ge>n. \<theta> i \<in> nodes G" by simp
- qed
- with finite_range
- obtain p where inf_visit: "\<exists>\<^sub>\<infinity>i. \<theta> i = p" by auto
-
- then obtain i where "n < i" "\<theta> i = p"
- by (auto simp:INFM_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 INFM_nat by auto
- from inf_visit obtain k where "j < k" "\<theta> k = p"
- by (auto simp:INFM_nat)
-
- from `i < j` `j < k` `n < i` thr
- fin_from_inf[of n \<theta> ?cp]
- `descat ?cp \<theta> j`
- have "is_desc_fthread \<theta> ?cp i k"
- unfolding is_desc_fthread_def
- by auto
-
- 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 base thus ?case by (simp add:sub_path_def)
- next
- case (step i) thus ?case
- by (simp add:sub_path_def upt_rec[of i k] idemp)
- qed
-
- with `i < j` `j < k` dfth Lemma7b[of i k ?cp p p]
- have "dsc G p p" by auto
- with no_strict_arc have False by auto
- thus ?thesis ..
- qed
-next
- assume "SCT' A"
-
- 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 blast
-
- from `finite_acg A`
- have "finite_acg (tcl A)" by (simp add: finite_tcl)
- hence "finite (dest_graph (tcl A))" (is "finite ?AG")
- by (simp add: finite_acg_def finite_graph_def)
-
- from pdesc_acgplus[OF ipath]
- have a: "\<And>x y. x<y \<Longrightarrow> pdesc p\<langle>x,y\<rangle> \<in> dest_graph (tcl A)"
- 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 ?AG`)
- by (simp only:split_conv, rule a, auto)
-
- obtain n H m where
- G_struct: "G = (n, H, m)" by (cases G)
-
- 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 :: 'a 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
-
-end
--- a/src/HOL/SizeChange/Criterion.thy Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(* Title: HOL/Library/SCT_Definition.thy
- ID: $Id$
- Author: Alexander Krauss, TU Muenchen
-*)
-
-header {* The Size-Change Principle (Definition) *}
-
-theory Criterion
-imports Graphs Infinite_Set
-begin
-
-subsection {* Size-Change Graphs *}
-
-datatype sedge =
- LESS ("\<down>")
- | LEQ ("\<Down>")
-
-instantiation sedge :: comm_monoid_mult
-begin
-
-definition
- one_sedge_def: "1 = \<Down>"
-
-definition
- mult_sedge_def:" a * b = (if a = \<down> then \<down> else b)"
-
-instance 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
-
-end
-
-lemma sedge_UNIV:
- "UNIV = { LESS, LEQ }"
-proof (intro equalityI subsetI)
- fix x show "x \<in> { LESS, LEQ }"
- by (cases x) auto
-qed auto
-
-instance sedge :: finite
-proof
- show "finite (UNIV::sedge set)"
- by (simp add: sedge_UNIV)
-qed
-
-
-
-types 'a scg = "('a, sedge) graph"
-types 'a acg = "('a, 'a scg) graph"
-
-
-subsection {* 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)
- "eqp G i j \<equiv> has_edge G i LEQ j"
-
-abbreviation
- eql :: "'a scg \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-("_ \<turnstile> _ \<leadsto> _")
-where
- "eql G i j \<equiv> has_edge G i LESS j \<or> has_edge G i LEQ j"
-
-
-abbreviation (input) descat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
-where
- "descat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))"
-
-abbreviation (input) eqat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
-where
- "eqat p \<theta> i \<equiv> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i))"
-
-
-abbreviation (input) eqlat :: "('a, 'a scg) ipath \<Rightarrow> 'a sequence \<Rightarrow> nat \<Rightarrow> bool"
-where
- "eqlat p \<theta> i \<equiv> (has_edge (snd (p i)) (\<theta> i) LESS (\<theta> (Suc i))
- \<or> has_edge (snd (p i)) (\<theta> i) LEQ (\<theta> (Suc i)))"
-
-
-definition is_desc_thread :: "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> bool"
-where
- "is_desc_thread \<theta> p = ((\<exists>n.\<forall>i\<ge>n. eqlat p \<theta> i) \<and> (\<exists>\<^sub>\<infinity>i. descat p \<theta> i))"
-
-definition SCT :: "'a acg \<Rightarrow> bool"
-where
- "SCT \<A> =
- (\<forall>p. has_ipath \<A> p \<longrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> p))"
-
-
-
-definition no_bad_graphs :: "'a acg \<Rightarrow> bool"
-where
- "no_bad_graphs A =
- (\<forall>n G. has_edge A n G n \<and> G * G = G
- \<longrightarrow> (\<exists>p. has_edge G p LESS p))"
-
-
-definition SCT' :: "'a acg \<Rightarrow> bool"
-where
- "SCT' A = no_bad_graphs (tcl A)"
-
-end
--- a/src/HOL/SizeChange/Examples.thy Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-(* Title: HOL/Library/SCT_Examples.thy
- ID: $Id$
- Author: Alexander Krauss, TU Muenchen
-*)
-
-header {* Examples for Size-Change Termination *}
-
-theory 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 @{context}") (* Build control graph *)
- apply (rule SCT_Main) (* Apply main theorem *)
- apply (simp add:finite_acg_simps) (* show finiteness *)
- oops (*FIXME 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 @{context}")
- apply (rule SCT_Main)
- apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
- oops (* FIXME 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 @{context}")
- apply (rule SCT_Main)
- apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
- oops (* FIXME 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 @{context}")
- apply (rule SCT_Main)
- apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
- by (simp only:sctTest_simps cong: sctTest_congs)
-
-end
--- a/src/HOL/SizeChange/Graphs.thy Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,768 +0,0 @@
-(* Title: HOL/Library/Graphs.thy
- Author: Alexander Krauss, TU Muenchen
-*)
-
-header {* General Graphs as Sets *}
-
-theory Graphs
-imports Main Misc_Tools Kleene_Algebra
-begin
-
-subsection {* Basic types, Size Change Graphs *}
-
-datatype ('a, 'b) graph =
- Graph "('a \<times> 'b \<times> 'a) set"
-
-primrec 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
-
-lemma split_graph_all:
- "(\<And>gr. PROP P gr) \<equiv> (\<And>set. PROP P (Graph set))"
-proof
- fix set
- assume "\<And>gr. PROP P gr"
- then show "PROP P (Graph set)" .
-next
- fix gr
- assume "\<And>set. PROP P (Graph set)"
- then have "PROP P (Graph (dest_graph gr))" .
- then show "PROP P gr" by simp
-qed
-
-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)"
-
-
-subsection {* 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 assms
- by (cases G, cases H) (auto simp:split_paired_all has_edge_def)
-
-
-instantiation graph :: (type, type) comm_monoid_add
-begin
-
-definition
- graph_zero_def: "0 = Graph {}"
-
-definition
- graph_plus_def [code del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
-
-instance proof
- fix x y z :: "('a,'b) graph"
- show "x + y + z = x + (y + z)"
- and "x + y = y + x"
- and "0 + x = x"
- unfolding graph_plus_def graph_zero_def by auto
-qed
-
-end
-
-instantiation graph :: (type, type) "{distrib_lattice, complete_lattice}"
-begin
-
-definition
- graph_leq_def [code del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
-
-definition
- graph_less_def [code del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
-
-definition
- [code del]: "bot = Graph {}"
-
-definition
- [code del]: "top = Graph UNIV"
-
-definition
- [code del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
-
-definition
- [code del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
-
-definition
- Inf_graph_def [code del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
-
-definition
- Sup_graph_def [code del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
-
-instance proof
- fix x y z :: "('a,'b) graph"
- fix A :: "('a, 'b) graph set"
-
- show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
- unfolding graph_leq_def graph_less_def
- by (cases x, cases y) auto
-
- show "x \<le> x" unfolding graph_leq_def ..
-
- { assume "x \<le> y" "y \<le> z"
- with order_trans show "x \<le> z"
- unfolding graph_leq_def . }
-
- { assume "x \<le> y" "y \<le> x" thus "x = y"
- unfolding graph_leq_def
- by (cases x, cases y) simp }
-
- show "inf x y \<le> x" "inf x y \<le> y"
- unfolding inf_graph_def graph_leq_def
- by auto
-
- { assume "x \<le> y" "x \<le> z" thus "x \<le> inf y z"
- unfolding inf_graph_def graph_leq_def
- by auto }
-
- show "x \<le> sup x y" "y \<le> sup x y"
- unfolding sup_graph_def graph_leq_def graph_plus_def by auto
-
- { assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x"
- unfolding sup_graph_def graph_leq_def graph_plus_def by auto }
-
- show "bot \<le> x" unfolding graph_leq_def bot_graph_def by simp
-
- show "x \<le> top" unfolding graph_leq_def top_graph_def by simp
-
- show "sup x (inf y z) = inf (sup x y) (sup x z)"
- unfolding inf_graph_def sup_graph_def graph_leq_def graph_plus_def by auto
-
- { assume "x \<in> A" thus "Inf A \<le> x"
- unfolding Inf_graph_def graph_leq_def by auto }
-
- { assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" thus "z \<le> Inf A"
- unfolding Inf_graph_def graph_leq_def by auto }
-
- { assume "x \<in> A" thus "x \<le> Sup A"
- unfolding Sup_graph_def graph_leq_def by auto }
-
- { assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" thus "Sup A \<le> z"
- unfolding Sup_graph_def graph_leq_def by auto }
-qed
-
-end
-
-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)
-
-
-subsubsection {* Multiplicative Structure *}
-
-instantiation graph :: (type, times) mult_zero
-begin
-
-definition
- graph_mult_def [code del]: "G * H = grcomp G H"
-
-instance proof
- fix a :: "('a, 'b) graph"
-
- show "0 * a = 0"
- unfolding graph_mult_def graph_zero_def
- by (cases a) (simp add:grcomp.simps)
- show "a * 0 = 0"
- unfolding graph_mult_def graph_zero_def
- by (cases a) (simp add:grcomp.simps)
-qed
-
-end
-
-instantiation graph :: (type, one) one
-begin
-
-definition
- graph_one_def: "1 = Graph { (x, 1, x) |x. True}"
-
-instance ..
-
-end
-
-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)
-
-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) "{semiring_1, idem_add}"
-proof
- fix a b c :: "('a, 'b) graph"
-
- show "1 * a = a"
- by (rule graph_ext) (auto simp:in_grcomp in_grunit)
- show "a * 1 = a"
- by (rule graph_ext) (auto simp:in_grcomp in_grunit)
-
- 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
-
- show "a + a = a" unfolding graph_plus_def by simp
-
-qed
-
-instantiation graph :: (type, monoid_mult) star
-begin
-
-definition
- graph_star_def: "star (G \<Colon> ('a, 'b) graph) = (SUP n. G ^ n)"
-
-instance ..
-
-end
-
-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 assms
- 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 assms
- by (auto simp: in_grplus)
-
-lemma in_graph_compE:
- assumes GH: "has_edge (G * H) n e n'"
- obtains e1 k e2
- where "has_edge G n e1 k" "has_edge H k e2 n'" "e = e1 * e2"
- using GH
- by (auto simp: in_grcomp)
-
-lemma
- assumes "x \<in> S k"
- shows "x \<in> (\<Union>k. S k)"
- using assms by blast
-
-lemma graph_union_least:
- assumes "\<And>n. Graph (G n) \<le> C"
- shows "Graph (\<Union>n. G n) \<le> C"
- using assms unfolding graph_leq_def
- by auto
-
-lemma Sup_graph_eq:
- "(SUP n. Graph (G n)) = Graph (\<Union>n. G n)"
-proof (rule order_antisym)
- show "(SUP n. Graph (G n)) \<le> Graph (\<Union>n. G n)"
- by (rule SUP_leI) (auto simp add: graph_leq_def)
-
- show "Graph (\<Union>n. G n) \<le> (SUP n. Graph (G n))"
- by (rule graph_union_least, rule le_SUPI', rule)
-qed
-
-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_complete_lattice
-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 less_le_not_le show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" .
-
- 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 simp del: power.simps power_Suc)
- apply (rule_tac x = "n - 1" in exI, auto)
- done
-
-
-subsection {* 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))))"
-
-
-subsection {* Finite Paths *}
-
-types ('n, 'e) fpath = "('n \<times> ('e \<times> 'n) list)"
-
-inductive 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 assms 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 assms
-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 assms
- 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" by fact
- 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 -
- {
- fix i
- from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
- by simp
- from this and `has_fpath G p`
- have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)"
- by (rule path_nth_graph)
-
- from path_loop_connect[OF loop nonempty] pk_G
- have "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
- }
- then show ?thesis by (auto simp:has_ipath_def)
-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
-
-
-subsection {* 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 base show ?case by (auto simp:sub_path_def intro:has_fpath.intros)
-next
- case (step 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 assms 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 assms
- 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 assms
-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])
- using `0 < k` and k
- apply auto
- done
-
- 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])
- apply (simp add:path_nth_def)
- done
- qed
-qed
-
-end
--- a/src/HOL/SizeChange/Implementation.thy Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,185 +0,0 @@
-(* Title: HOL/Library/SCT_Implementation.thy
- ID: $Id$
- Author: Alexander Krauss, TU Muenchen
-*)
-
-header {* Implemtation of the SCT criterion *}
-
-theory Implementation
-imports Correctness
-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)
-
-
-lemma mk_tcl_finite_terminates:
- fixes A :: "'a acg"
- assumes fA: "finite_acg A"
- shows "mk_tcl_dom (A, A)"
-proof -
- from fA have fin_tcl: "finite_acg (tcl A)"
- by (simp add:finite_tcl)
-
- hence "finite (dest_graph (tcl A))"
- unfolding finite_acg_def finite_graph_def ..
-
- let ?count = "\<lambda>G. card (dest_graph G)"
- let ?N = "?count (tcl A)"
- let ?m = "\<lambda>X. ?N - (?count X)"
-
- let ?P = "\<lambda>X. mk_tcl_dom (A, X)"
-
- {
- fix X
- assume "X \<le> tcl A"
- then
- have "mk_tcl_dom (A, X)"
- proof (induct X rule:measure_induct_rule[of ?m])
- case (less X)
- show ?case
- proof (cases "X * A \<le> X")
- case True
- with mk_tcl.domintros show ?thesis by auto
- next
- case False
- then have l: "X < X + X * A"
- unfolding graph_less_def graph_leq_def graph_plus_def
- by auto
-
- from `X \<le> tcl A`
- have "X * A \<le> tcl A * A" by (simp add:mult_mono)
- also have "\<dots> \<le> A + tcl A * A" by simp
- also have "\<dots> = tcl A" by (simp add:tcl_unfold_right[symmetric])
- finally have "X * A \<le> tcl A" .
- with `X \<le> tcl A`
- have "X + X * A \<le> tcl A + tcl A"
- by (rule add_mono)
- hence less_tcl: "X + X * A \<le> tcl A" by simp
- hence "X < tcl A"
- using l `X \<le> tcl A` by auto
-
- from less_tcl fin_tcl
- have "finite_acg (X + X * A)" by (rule finite_acg_subset)
- hence "finite (dest_graph (X + X * A))"
- unfolding finite_acg_def finite_graph_def ..
-
- hence X: "?count X < ?count (X + X * A)"
- using l[simplified graph_less_def graph_leq_def]
- by (rule psubset_card_mono)
-
- have "?count X < ?N"
- apply (rule psubset_card_mono)
- by fact (rule `X < tcl A`[simplified graph_less_def])
-
- with X have "?m (X + X * A) < ?m X" by arith
-
- from less.hyps this less_tcl
- have "mk_tcl_dom (A, X + X * A)" .
- with mk_tcl.domintros show ?thesis .
- qed
- qed
- }
- from this less_tcl show ?thesis .
-qed
-
-
-lemma mk_tcl_finite_tcl:
- fixes A :: "'a acg"
- assumes fA: "finite_acg A"
- shows "mk_tcl A A = tcl A"
- using mk_tcl_finite_terminates[OF fA]
- by (simp only: tcl_def mk_tcl_correctness star_simulation)
-
-definition test_SCT :: "nat acg \<Rightarrow> bool"
-where
- "test_SCT \<A> =
- (let \<T> = mk_tcl \<A> \<A>
- in (\<forall>(n,G,m)\<in>dest_graph \<T>.
- n \<noteq> m \<or> G * G \<noteq> G \<or>
- (\<exists>(p::nat,e,q)\<in>dest_graph G. p = q \<and> e = LESS)))"
-
-
-lemma SCT'_exec:
- assumes fin: "finite_acg A"
- shows "SCT' A = test_SCT A"
- using mk_tcl_finite_tcl[OF fin]
- unfolding test_SCT_def Let_def
- unfolding SCT'_def no_bad_graphs_def has_edge_def
- by force
-
-code_modulename SML
- Implementation Graphs
-
-lemma [code]:
- "(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]:
- "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)"
- unfolding graph_plus_def ..
-
-lemma [code]:
- "(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 :: "nat acg \<Rightarrow> nat 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 assms
- 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
-
-(* ML {* @{code test_SCT} *} *)
-
-end
--- a/src/HOL/SizeChange/Interpretation.thy Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,415 +0,0 @@
-(* Title: HOL/Library/SCT_Interpretation.thy
- ID: $Id$
- Author: Alexander Krauss, TU Muenchen
-*)
-
-header {* Applying SCT to function definitions *}
-
-theory Interpretation
-imports Main Misc_Tools Criterion
-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> accp R x"
- shows "\<exists>y. R y x \<and> \<not> accp R y"
-proof (rule classical)
- assume "\<not> ?thesis"
- hence "\<And>y. R y x \<Longrightarrow> accp R y" by blast
- with accp.accI have "accp R x" .
- with notacc show ?thesis by contradiction
-qed
-
-lemma non_acc_has_idseq:
- assumes "\<not> accp R x"
- shows "\<exists>s. idseq R s x"
-proof -
-
- have "\<exists>f. \<forall>x. \<not>accp R x \<longrightarrow> R (f x) x \<and> \<not>accp R (f x)"
- by (rule choice, auto simp:not_acc_smaller)
-
- then obtain f where
- in_R: "\<And>x. \<not>accp R x \<Longrightarrow> R (f x) x"
- and nia: "\<And>x. \<not>accp R x \<Longrightarrow> \<not>accp R (f x)"
- by blast
-
- let ?s = "\<lambda>i. (f ^^ i) x"
-
- {
- fix i
- have "\<not>accp R (?s i)"
- by (induct i) (auto simp:nia `\<not>accp 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)"
-
-primrec 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 assms
- 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 '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 assms
- 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 assms
- 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 INFM_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 :: "nat scg \<Rightarrow> ('a, 'q) cdesc \<Rightarrow> ('a, 'q) cdesc
- \<Rightarrow> 'a measures \<Rightarrow> 'a measures \<Rightarrow> bool"
- where
- "approx G C C' M M'
- = (\<forall>i j. (dsc G i j \<longrightarrow> decr C C' (M i) (M' j))
- \<and>(eqp 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 assms
- 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 assms
- 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 :: "nat 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 assms
- 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. accp R x"
-proof (rule, rule classical)
- fix x
- assume "\<not> accp 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> eqp (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 "eqp (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 INFM_nat
- proof
- fix i
- from inf obtain j where "i < j" and d: "descat ?p th j"
- unfolding INFM_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 "accp R x" ..
-qed
-
-end
--- a/src/HOL/SizeChange/Misc_Tools.thy Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,173 +0,0 @@
-(* Title: HOL/Library/SCT_Misc.thy
- ID: $Id$
- Author: Alexander Krauss, TU Muenchen
-*)
-
-header {* Miscellaneous Tools for Size-Change Termination *}
-
-theory Misc_Tools
-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 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 assms
- by auto
-
-
-subsection {* Sequences *}
-
-types
- 'a sequence = "nat \<Rightarrow> 'a"
-
-
-subsubsection {* 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 assms
- unfolding increasing_def by simp
-
-lemma increasing_weak:
- assumes "increasing s"
- assumes "i \<le> j"
- shows "s i \<le> s j"
- using assms increasing_strict[of s i j]
- by (cases "i < j") auto
-
-lemma increasing_inc:
- assumes "increasing s"
- shows "n \<le> s n"
-proof (induct n)
- case 0 then show ?case by simp
-next
- case (Suc n)
- with increasing_strict [OF `increasing s`, of n "Suc n"]
- show ?case by auto
-qed
-
-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)
-
-
-subsubsection {* 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 "increasing s"
- shows "\<exists>i. n < s (Suc i)"
-proof -
- have "n \<le> s n"
- using `increasing s` by (rule increasing_inc)
- also have "\<dots> < s (Suc n)"
- using `increasing s` increasing_strict 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 [OF `increasing s`])
-
-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 "increasing s"
- assumes "s i \<le> k"
- shows "k \<in> section s (section_of s k)"
- using assms
- by (auto intro:section_of1 section_of2)
-
-end
--- a/src/HOL/SizeChange/ROOT.ML Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(* Title: HOL/SizeChange/ROOT.ML
- ID: $Id$
-*)
-
-no_document use_thy "Infinite_Set";
-no_document use_thy "Ramsey";
-use_thy "Examples";
--- a/src/HOL/SizeChange/Size_Change_Termination.thy Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-(* Title: HOL/Library/Size_Change_Termination.thy
- Author: Alexander Krauss, TU Muenchen
-*)
-
-header "Size-Change Termination"
-
-theory Size_Change_Termination
-imports Correctness Interpretation Implementation
-uses "sct.ML"
-begin
-
-subsection {* 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
-
-
-lemma SCT_Main:
- "finite_acg A \<Longrightarrow> test_SCT A \<Longrightarrow> SCT A"
- using LJA_Theorem4 SCT'_exec
- by auto
-
-end
--- a/src/HOL/SizeChange/document/root.tex Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-
-% $Id$
-
-\documentclass[11pt,a4paper]{article}
-\usepackage{latexsym}
-\usepackage{isabelle,isabellesym}
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-
-\begin{document}
-
-\title{Size-Change Termination}
-\author{Alexander Krauss}
-\maketitle
-
-%\tableofcontents
-
-\parindent 0pt\parskip 0.5ex
-
-\input{session}
-
-\end{document}
--- a/src/HOL/SizeChange/sct.ML Fri Nov 06 13:36:46 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,351 +0,0 @@
-(* Title: HOL/SizeChange/sct.ML
- Author: Alexander Krauss, TU Muenchen
-
-Tactics for size change termination.
-*)
-signature SCT =
-sig
- val abs_rel_tac : tactic
- val mk_call_graph : Proof.context -> tactic
-end
-
-structure Sct : 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 = @{typ "nat scg"}
-val acgT = @{typ "nat acg"}
-
-fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT))
-fun graphT nT eT = Type ("Graphs.graph", [nT, eT])
-
-fun graph_const nT eT = Const ("Graphs.graph.Graph", HOLogic.mk_setT (edgeT nT eT) --> graphT nT eT)
-
-val stepP_const = "Interpretation.stepP"
-val stepP_def = thm "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 no_stepI = thm "Interpretation.no_stepI"
-
-val approx_const = "Interpretation.approx"
-val approx_empty = thm "Interpretation.approx_empty"
-val approx_less = thm "Interpretation.approx_less"
-val approx_leq = thm "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 = "Interpretation.sound_int"
-val sound_int_def = thm "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 has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
-
-val all_less_zero = thm "Interpretation.all_less_zero"
-val all_less_Suc = thm "Interpretation.all_less_Suc"
-
-(* --> Library? *)
-fun del_index n [] = []
- | del_index n (x :: xs) =
- if n>0 then x :: del_index (n - 1) xs else xs
-
-(* Lists as finite multisets *)
-
-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 = (null vs orelse error "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 = Function_Lib.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 ctxt RD =
- let
- val domT = range_type (fastype_of (fst (HOLogic.dest_prod (snd (HOLogic.dest_prod RD)))))
- val measures = MeasureFunctions.get_measure_functions ctxt domT
- in
- measures
- end
-
-val mk_number = HOLogic.mk_nat
-val dest_number = HOLogic.dest_nat
-
-fun nums_to i = map_range mk_number i
-
-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_range (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) n)
- in
- the o Inttab.lookup table
- end
-
-val get_elem = snd o Logic.dest_equals o prop_of
-
-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 ctxt domT Dtab Mtab (i, j) =
- let
- val css = clasimpset_of ctxt
- val thy = ProofContext.theory_of ctxt
- 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
- |> auto_tac css |> 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))))
- |> auto_tac css |> Seq.hd
-
- in
- if Thm.no_prems no_step
- then NoStep (Goal.finish ctxt 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)
- |> auto_tac css |> 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)
- |> auto_tac css |> Seq.hd
-
- val decr = forall_intr (cterm_of thy relvar)
- #> forall_elim (cterm_of thy @{const HOL.less(nat)})
- #> auto_tac css #> Seq.hd
-
- val decreq = forall_intr (cterm_of thy relvar)
- #> forall_elim (cterm_of thy @{const HOL.less_eq(nat)})
- #> auto_tac css #> 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 ctxt 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 ctxt 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_range (fn n => EVERY (map_range (set_m1 n) M)) N))
- THEN (rtac approx_empty 1)
-
- val approx_thm = goal
- |> cterm_of thy
- |> Goal.init
- |> tac |> Seq.hd
- |> Goal.finish ctxt
-
- val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm
- in
- Graph (G, approx_thm)
- end
- end
-
-fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n))
-
-fun in_graph_tac ctxt =
- simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
- THEN (simp_tac (simpset_of ctxt) 1) (* FIXME reduce simpset *)
-
-fun approx_tac _ (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
- | approx_tac ctxt (Graph (G, thm)) =
- rtac disjI2 1
- THEN rtac exI 1
- THEN rtac conjI 1
- THEN rtac thm 2
- THEN (in_graph_tac ctxt)
-
-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
-
-
-fun mk_length l = HOLogic.size_const (fastype_of l) $ l;
-val length_simps = thms "Interpretation.length_simps"
-
-
-
-fun mk_call_graph ctxt (st : thm) =
- let
- val thy = ProofContext.theory_of ctxt
- val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
-
- val RDs = HOLogic.dest_list RDlist
- val n = length RDs
-
- val Mss = map (measures_of ctxt) 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 ctxt 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 ^ "): " ^
- Syntax.string_of_term ctxt G ^ ",\n")
- | _ => I) cs) parts ""
- val _ = 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)
- |> HOLogic.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 =
- unfold_tac [sound_int_def, len_simp] (simpset_of ctxt)
- THEN all_less_tac (map (all_less_tac o map (approx_tac ctxt)) parts)
- in
- tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
- end
-
-
-end
-
-
-
-
-
-
-