# HG changeset patch
# User krauss
# Date 1179435606 -7200
# Node ID b469cf6dc5313fd651fd6d7fb64961448f35a3d6
# Parent  3608f0362a913824acc42da083a86903d9c297c6
moved lemmas to Nat.thy

diff -r 3608f0362a91 -r b469cf6dc531 src/HOL/Library/SCT_Misc.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"