author krauss Thu, 17 May 2007 23:00:06 +0200 changeset 23002 b469cf6dc531 parent 23001 3608f0362a91 child 23003 4b0bf04a4d68
moved lemmas to Nat.thy
```--- a/src/HOL/Library/SCT_Misc.thy	Thu May 17 22:58:53 2007 +0200
+++ b/src/HOL/Library/SCT_Misc.thy	Thu May 17 23:00:06 2007 +0200
@@ -24,43 +24,8 @@
"(x \<in> set l) = (index_of l x < length l)"
by (induct l) auto

-
subsection {* Some reasoning tools *}

-lemma inc_induct[consumes 1]:
-  assumes less: "i \<le> j"
-  assumes base: "P j"
-  assumes step: "\<And>i. \<lbrakk>i < j; P (Suc i)\<rbrakk> \<Longrightarrow> P i"
-  shows "P i"
-  using less
-proof (induct d\<equiv>"j - i" arbitrary: i)
-  case (0 i)
-  with `i \<le> j` have "i = j" by simp
-  with base show ?case by simp
-next
-  case (Suc d i)
-  hence "i < j" "P (Suc i)"
-    by simp_all
-  thus "P i" by (rule step)
-qed
-
-lemma strict_inc_induct[consumes 1]:
-  assumes less: "i < j"
-  assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i"
-  assumes step: "\<And>i. \<lbrakk>i < j; P (Suc i)\<rbrakk> \<Longrightarrow> P i"
-  shows "P i"
-  using less
-proof (induct d\<equiv>"j - i - 1" arbitrary: i)
-  case (0 i)
-  with `i < j` have "j = Suc i" by simp
-  with base show ?case by simp
-next
-  case (Suc d i)
-  hence "i < j" "P (Suc i)"
-    by simp_all
-  thus "P i" by (rule step)
-qed
-
lemma three_cases:
assumes "a1 \<Longrightarrow> thesis"
assumes "a2 \<Longrightarrow> thesis"```