# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260405587 -3600
# Node ID 0668d218bfa5d53f7217c933b35ff222d79e2920
# Parent  94d6d29459c9c99bff094a2fc910976d7ae908ac
Lifted some kind of induction.

diff -r 94d6d29459c9 -r 0668d218bfa5 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Wed Dec 09 23:32:16 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Dec 10 01:39:47 2009 +0100
@@ -294,6 +294,26 @@
 apply(simp_all add: left_distrib add_strict_mono)
 done
 
+lemma int_induct_raw:
+  assumes a: "P (0::nat, 0)"
+  and     b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1,0))"
+  and     c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (minus_raw (1,0)))"
+  shows      "P x"
+apply(case_tac x) apply(simp)
+apply(rule_tac x="b" in spec)
+apply(rule_tac Nat.induct)
+apply(rule allI)
+apply(rule_tac Nat.induct)
+using a b c apply(auto)
+done
+
+lemma int_induct:
+  assumes a: "P (0::int)"
+  and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
+  and     c: "\<And>i. P i \<Longrightarrow> P (i + (- 1))"
+  shows      "P x"
+using a b c by (lifting int_induct_raw)
+
 lemma zero_le_imp_eq_int: 
   fixes k::int
   shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"