--- a/src/HOL/Library/SCT_Misc.thy Tue Nov 06 13:12:56 2007 +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 SCT_Misc (* FIXME proper name *)
-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