# HG changeset patch
# User nipkow
# Date 1035887572 -3600
# Node ID 0b8fbcf65d736990c351a15e6451f284e9242414
# Parent  48bfc2cc0938455823f55bfa2960ce4c3b27dce5
added induction thms

diff -r 48bfc2cc0938 -r 0b8fbcf65d73 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Mon Oct 28 17:56:00 2002 +0100
+++ b/src/HOL/Integ/IntArith.thy	Tue Oct 29 11:32:52 2002 +0100
@@ -25,4 +25,80 @@
   with False show ?thesis by simp
 qed
 
+subsubsection "Induction principles for int"
+
+                     (* `set:int': dummy construction *)
+theorem int_ge_induct[case_names base step,induct set:int]:
+  assumes ge: "k \<le> (i::int)" and
+        base: "P(k)" and
+        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
+  shows "P i"
+proof -
+  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i"
+    proof (induct n)
+      case 0
+      hence "i = k" by arith
+      thus "P i" using base by simp
+    next
+      case (Suc n)
+      hence "n = nat((i - 1) - k)" by arith
+      moreover
+      have ki1: "k \<le> i - 1" using Suc.prems by arith
+      ultimately
+      have "P(i - 1)" by(rule Suc.hyps)
+      from step[OF ki1 this] show ?case by simp
+    qed
+  }
+  from this ge show ?thesis by fast
+qed
+
+                     (* `set:int': dummy construction *)
+theorem int_gr_induct[case_names base step,induct set:int]:
+  assumes gr: "k < (i::int)" and
+        base: "P(k+1)" and
+        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
+  shows "P i"
+apply(rule int_ge_induct[of "k + 1"])
+  using gr apply arith
+ apply(rule base)
+apply(rule step)
+ apply simp+
+done
+
+theorem int_le_induct[consumes 1,case_names base step]:
+  assumes le: "i \<le> (k::int)" and
+        base: "P(k)" and
+        step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
+  shows "P i"
+proof -
+  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i <= k \<Longrightarrow> P i"
+    proof (induct n)
+      case 0
+      hence "i = k" by arith
+      thus "P i" using base by simp
+    next
+      case (Suc n)
+      hence "n = nat(k - (i+1))" by arith
+      moreover
+      have ki1: "i + 1 \<le> k" using Suc.prems by arith
+      ultimately
+      have "P(i+1)" by(rule Suc.hyps)
+      from step[OF ki1 this] show ?case by simp
+    qed
+  }
+  from this le show ?thesis by fast
+qed
+
+theorem int_less_induct[consumes 1,case_names base step]:
+  assumes less: "(i::int) < k" and
+        base: "P(k - 1)" and
+        step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
+  shows "P i"
+apply(rule int_le_induct[of _ "k - 1"])
+  using less apply arith
+ apply(rule base)
+apply(rule step)
+ apply simp+
+done
+
 end