src/HOL/Int.thy

   using less apply arith
  apply(rule base)
 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:
      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"