--- 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