# HG changeset patch
# User haftmann
# Date 1273496104 -7200
# Node ID 3560de0fe851e05bc674c43cfd41e3e7a379f9f3
# Parent  59b50c691b75665c02c5049a3bd62945e6a93d2f
moved int induction lemma to theory Int as int_bidirectional_induct

diff -r 59b50c691b75 -r 3560de0fe851 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon May 10 14:18:41 2010 +0200
+++ b/src/HOL/Int.thy	Mon May 10 14:55:04 2010 +0200
@@ -1784,6 +1784,23 @@
 apply (rule step, simp+)
 done
 
+theorem int_bidirectional_induct [case_names base step1 step2]:
+  fixes k :: int
+  assumes base: "P k"
+    and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
+    and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
+  shows "P i"
+proof -
+  have "i \<le> k \<or> i \<ge> k" by arith
+  then show ?thesis proof
+    assume "i \<ge> k" then show ?thesis using base
+      by (rule int_ge_induct) (fact step1)
+  next
+    assume "i \<le> k" then show ?thesis using base
+      by (rule int_le_induct) (fact step2)
+  qed
+qed
+
 subsection{*Intermediate value theorems*}
 
 lemma int_val_lemma: