# HG changeset patch
# User haftmann
# Date 1393662848 -3600
# Node ID 0bc0217387a5d5c71f98f7daa98e62c753362bcc
# Parent  e8dd03241e86caaa926882eab9afd0f6178ef1fe
earlier setup of transfer, without dependency on psychodelic interpretations

diff -r e8dd03241e86 -r 0bc0217387a5 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Mar 01 08:21:46 2014 +0100
+++ b/src/HOL/Word/Word.thy	Sat Mar 01 09:34:08 2014 +0100
@@ -172,6 +172,76 @@
   "case x of (XCONST of_int :: 'a) y => b" => "CONST word_int_case (%y. b) x"
 
 
+subsection {* Correspondence relation for theorem transfer *}
+
+definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
+where
+  "cr_word = (\<lambda>x y. word_of_int x = y)"
+
+lemma Quotient_word:
+  "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
+    word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
+  unfolding Quotient_alt_def cr_word_def
+  by (simp add: no_bintr_alt1 word_of_int_uint) (simp add: word_of_int_def Abs_word_inject)
+
+lemma reflp_word:
+  "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
+  by (simp add: reflp_def)
+
+setup_lifting (no_code) Quotient_word reflp_word
+
+text {* TODO: The next lemma could be generated automatically. *}
+
+lemma uint_transfer [transfer_rule]:
+  "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
+    (uint :: 'a::len0 word \<Rightarrow> int)"
+  unfolding fun_rel_def word.pcr_cr_eq cr_word_def
+  by (simp add: no_bintr_alt1 uint_word_of_int)
+
+
+subsection {* Basic code generation setup *}
+
+definition Word :: "int \<Rightarrow> 'a::len0 word"
+where
+  [code_post]: "Word = word_of_int"
+
+lemma [code abstype]:
+  "Word (uint w) = w"
+  by (simp add: Word_def word_of_int_uint)
+
+declare uint_word_of_int [code abstract]
+
+instantiation word :: (len0) equal
+begin
+
+definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
+where
+  "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
+
+instance proof
+qed (simp add: equal equal_word_def word_uint_eq_iff)
+
+end
+
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+instantiation word :: ("{len0, typerep}") random
+begin
+
+definition
+  "random_word i = Random.range i \<circ>\<rightarrow> (\<lambda>k. Pair (
+     let j = word_of_int (int_of_integer (integer_of_natural k)) :: 'a word
+     in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+
 subsection {* Type-definition locale instantiations *}
 
 lemmas uint_0 = uint_nonnegative (* FIXME duplicate *)
@@ -210,75 +280,6 @@
   by (fact td_ext_ubin)
 
 
-subsection {* Correspondence relation for theorem transfer *}
-
-definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
-where
-  "cr_word = (\<lambda>x y. word_of_int x = y)"
-
-lemma Quotient_word:
-  "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
-    word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
-  unfolding Quotient_alt_def cr_word_def
-  by (simp add: word_ubin.norm_eq_iff)
-
-lemma reflp_word:
-  "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
-  by (simp add: reflp_def)
-
-setup_lifting (no_code) Quotient_word reflp_word
-
-text {* TODO: The next lemma could be generated automatically. *}
-
-lemma uint_transfer [transfer_rule]:
-  "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
-    (uint :: 'a::len0 word \<Rightarrow> int)"
-  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by (simp add: word_ubin.eq_norm)
-
-
-subsection {* Basic code generation setup *}
-
-definition Word :: "int \<Rightarrow> 'a::len0 word"
-where
-  [code_post]: "Word = word_of_int"
-
-lemma [code abstype]:
-  "Word (uint w) = w"
-  by (simp add: Word_def)
-
-declare uint_word_of_int [code abstract]
-
-instantiation word :: (len0) equal
-begin
-
-definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
-where
-  "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
-
-instance proof
-qed (simp add: equal equal_word_def)
-
-end
-
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-instantiation word :: ("{len0, typerep}") random
-begin
-
-definition
-  "random_word i = Random.range i \<circ>\<rightarrow> (\<lambda>k. Pair (
-     let j = word_of_int (int_of_integer (integer_of_natural k)) :: 'a word
-     in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
-
-instance ..
-
-end
-
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-
 subsection {* Arithmetic operations *}
 
 lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"