# HG changeset patch
# User paulson
# Date 1168530792 -3600
# Node ID f72cdc0a0af42bd2fa25d7305ab34a09244d6294
# Parent  49faa8c7a5d99a6ce5e7089a80205dc31a4c0cba
well-founded relations for the integers

diff -r 49faa8c7a5d9 -r f72cdc0a0af4 src/HOL/Integ/IntArith.thy
--- 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
diff -r 49faa8c7a5d9 -r f72cdc0a0af4 src/HOL/Library/Word.thy
--- 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: