# HG changeset patch
# User haftmann
# Date 1571424091 0
# Node ID 954e7f79c25a1ea2003c1389e8f5e814dbaa6148
# Parent  5f6dea6a7a4cb3a7ae55dad9418d6a3e02263a67
moved generic instance to distribution

diff -r 5f6dea6a7a4c -r 954e7f79c25a src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Oct 18 16:25:54 2019 +0200
+++ b/src/HOL/Word/Word.thy	Fri Oct 18 18:41:31 2019 +0000
@@ -1279,6 +1279,21 @@
   unfolding unat_def word_less_alt
   by (rule nat_less_eq_zless [symmetric]) simp
 
+lemmas unat_mono = word_less_nat_alt [THEN iffD1]
+
+instance word :: (len) wellorder
+proof
+  fix P :: "'a word \<Rightarrow> bool" and a
+  assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)"
+  have "wf (measure unat)" ..
+  moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat"
+    by (auto simp add: word_less_nat_alt)
+  ultimately have "wf {(a, b :: ('a::len) word). a < b}"
+    by (rule wf_subset)
+  then show "P a" using *
+    by induction blast
+qed
+
 lemma wi_less:
   "(word_of_int n < (word_of_int m :: 'a::len0 word)) =
     (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))"
@@ -1305,8 +1320,6 @@
 lemma udvd_iff_dvd: "x udvd y \<longleftrightarrow> unat x dvd unat y"
   unfolding dvd_def udvd_nat_alt by force
 
-lemmas unat_mono = word_less_nat_alt [THEN iffD1]
-
 lemma unat_minus_one:
   assumes "w \<noteq> 0"
   shows "unat (w - 1) = unat w - 1"