--- a/src/HOL/Integ/IntArith.thy Thu Jan 11 01:34:23 2007 +0100
+++ b/src/HOL/Integ/IntArith.thy Thu Jan 11 16:53:12 2007 +0100
@@ -6,7 +6,7 @@
header {* Integer arithmetic *}
theory IntArith
-imports Numeral
+imports Numeral "../Wellfounded_Relations"
uses ("int_arith1.ML")
begin
@@ -222,6 +222,37 @@
subsection "Induction principles for int"
+text{*Well-founded segments of the integers*}
+
+definition
+ int_ge_less_than :: "int => (int * int) set"
+where
+ "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
+
+theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
+proof -
+ have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
+ by (auto simp add: int_ge_less_than_def)
+ thus ?thesis
+ by (rule wf_subset [OF wf_measure])
+qed
+
+text{*This variant looks odd, but is typical of the relations suggested
+by RankFinder.*}
+
+definition
+ int_ge_less_than2 :: "int => (int * int) set"
+where
+ "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
+
+theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
+proof -
+ have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))"
+ by (auto simp add: int_ge_less_than2_def)
+ thus ?thesis
+ by (rule wf_subset [OF wf_measure])
+qed
+
(* `set:int': dummy construction *)
theorem int_ge_induct[case_names base step,induct set:int]:
assumes ge: "k \<le> (i::int)" and
--- a/src/HOL/Library/Word.thy Thu Jan 11 01:34:23 2007 +0100
+++ b/src/HOL/Library/Word.thy Thu Jan 11 16:53:12 2007 +0100
@@ -382,60 +382,13 @@
qed
lemma int_wf_ge_induct:
- assumes base: "P (k::int)"
- and ind : "!!i. (!!j. [| k \<le> j ; j < i |] ==> P j) ==> P i"
- and valid: "k \<le> i"
+ assumes ind : "!!i::int. (!!j. [| k \<le> j ; j < i |] ==> P j) ==> P i"
shows "P i"
-proof -
- have a: "\<forall> j. k \<le> j \<and> j < i --> P j"
- proof (rule int_ge_induct)
- show "k \<le> i"
- .
- next
- show "\<forall> j. k \<le> j \<and> j < k --> P j"
- by auto
- next
- fix i
- assume "k \<le> i"
- assume a: "\<forall> j. k \<le> j \<and> j < i --> P j"
- have pi: "P i"
- proof (rule ind)
- fix j
- assume "k \<le> j" and "j < i"
- with a
- show "P j"
- by auto
- qed
- show "\<forall> j. k \<le> j \<and> j < i + 1 --> P j"
- proof auto
- fix j
- assume kj: "k \<le> j"
- assume ji: "j \<le> i"
- show "P j"
- proof (cases "j = i")
- assume "j = i"
- with pi
- show "P j"
- by simp
- next
- assume "j ~= i"
- with ji
- have "j < i"
- by simp
- with kj and a
- show "P j"
- by blast
- qed
- qed
- qed
- show "P i"
- proof (rule ind)
- fix j
- assume "k \<le> j" and "j < i"
- with a
- show "P j"
- by auto
- qed
+proof (rule wf_induct_rule [OF wf_int_ge_less_than])
+ fix x
+ assume ih: "(\<And>y\<Colon>int. (y, x) \<in> int_ge_less_than k \<Longrightarrow> P y)"
+ thus "P x"
+ by (rule ind, simp add: int_ge_less_than_def)
qed
lemma unfold_nat_to_bv_helper: