1.1 --- a/src/HOL/Word/Word.thy Sat Mar 01 08:21:46 2014 +0100
1.2 +++ b/src/HOL/Word/Word.thy Sat Mar 01 09:34:08 2014 +0100
1.3 @@ -172,6 +172,76 @@
1.4 "case x of (XCONST of_int :: 'a) y => b" => "CONST word_int_case (%y. b) x"
1.5
1.6
1.7 +subsection {* Correspondence relation for theorem transfer *}
1.8 +
1.9 +definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
1.10 +where
1.11 + "cr_word = (\<lambda>x y. word_of_int x = y)"
1.12 +
1.13 +lemma Quotient_word:
1.14 + "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
1.15 + word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
1.16 + unfolding Quotient_alt_def cr_word_def
1.17 + by (simp add: no_bintr_alt1 word_of_int_uint) (simp add: word_of_int_def Abs_word_inject)
1.18 +
1.19 +lemma reflp_word:
1.20 + "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
1.21 + by (simp add: reflp_def)
1.22 +
1.23 +setup_lifting (no_code) Quotient_word reflp_word
1.24 +
1.25 +text {* TODO: The next lemma could be generated automatically. *}
1.26 +
1.27 +lemma uint_transfer [transfer_rule]:
1.28 + "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
1.29 + (uint :: 'a::len0 word \<Rightarrow> int)"
1.30 + unfolding fun_rel_def word.pcr_cr_eq cr_word_def
1.31 + by (simp add: no_bintr_alt1 uint_word_of_int)
1.32 +
1.33 +
1.34 +subsection {* Basic code generation setup *}
1.35 +
1.36 +definition Word :: "int \<Rightarrow> 'a::len0 word"
1.37 +where
1.38 + [code_post]: "Word = word_of_int"
1.39 +
1.40 +lemma [code abstype]:
1.41 + "Word (uint w) = w"
1.42 + by (simp add: Word_def word_of_int_uint)
1.43 +
1.44 +declare uint_word_of_int [code abstract]
1.45 +
1.46 +instantiation word :: (len0) equal
1.47 +begin
1.48 +
1.49 +definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
1.50 +where
1.51 + "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
1.52 +
1.53 +instance proof
1.54 +qed (simp add: equal equal_word_def word_uint_eq_iff)
1.55 +
1.56 +end
1.57 +
1.58 +notation fcomp (infixl "\<circ>>" 60)
1.59 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
1.60 +
1.61 +instantiation word :: ("{len0, typerep}") random
1.62 +begin
1.63 +
1.64 +definition
1.65 + "random_word i = Random.range i \<circ>\<rightarrow> (\<lambda>k. Pair (
1.66 + let j = word_of_int (int_of_integer (integer_of_natural k)) :: 'a word
1.67 + in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
1.68 +
1.69 +instance ..
1.70 +
1.71 +end
1.72 +
1.73 +no_notation fcomp (infixl "\<circ>>" 60)
1.74 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
1.75 +
1.76 +
1.77 subsection {* Type-definition locale instantiations *}
1.78
1.79 lemmas uint_0 = uint_nonnegative (* FIXME duplicate *)
1.80 @@ -210,75 +280,6 @@
1.81 by (fact td_ext_ubin)
1.82
1.83
1.84 -subsection {* Correspondence relation for theorem transfer *}
1.85 -
1.86 -definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
1.87 -where
1.88 - "cr_word = (\<lambda>x y. word_of_int x = y)"
1.89 -
1.90 -lemma Quotient_word:
1.91 - "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
1.92 - word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
1.93 - unfolding Quotient_alt_def cr_word_def
1.94 - by (simp add: word_ubin.norm_eq_iff)
1.95 -
1.96 -lemma reflp_word:
1.97 - "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
1.98 - by (simp add: reflp_def)
1.99 -
1.100 -setup_lifting (no_code) Quotient_word reflp_word
1.101 -
1.102 -text {* TODO: The next lemma could be generated automatically. *}
1.103 -
1.104 -lemma uint_transfer [transfer_rule]:
1.105 - "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
1.106 - (uint :: 'a::len0 word \<Rightarrow> int)"
1.107 - unfolding fun_rel_def word.pcr_cr_eq cr_word_def by (simp add: word_ubin.eq_norm)
1.108 -
1.109 -
1.110 -subsection {* Basic code generation setup *}
1.111 -
1.112 -definition Word :: "int \<Rightarrow> 'a::len0 word"
1.113 -where
1.114 - [code_post]: "Word = word_of_int"
1.115 -
1.116 -lemma [code abstype]:
1.117 - "Word (uint w) = w"
1.118 - by (simp add: Word_def)
1.119 -
1.120 -declare uint_word_of_int [code abstract]
1.121 -
1.122 -instantiation word :: (len0) equal
1.123 -begin
1.124 -
1.125 -definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
1.126 -where
1.127 - "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
1.128 -
1.129 -instance proof
1.130 -qed (simp add: equal equal_word_def)
1.131 -
1.132 -end
1.133 -
1.134 -notation fcomp (infixl "\<circ>>" 60)
1.135 -notation scomp (infixl "\<circ>\<rightarrow>" 60)
1.136 -
1.137 -instantiation word :: ("{len0, typerep}") random
1.138 -begin
1.139 -
1.140 -definition
1.141 - "random_word i = Random.range i \<circ>\<rightarrow> (\<lambda>k. Pair (
1.142 - let j = word_of_int (int_of_integer (integer_of_natural k)) :: 'a word
1.143 - in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
1.144 -
1.145 -instance ..
1.146 -
1.147 -end
1.148 -
1.149 -no_notation fcomp (infixl "\<circ>>" 60)
1.150 -no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
1.151 -
1.152 -
1.153 subsection {* Arithmetic operations *}
1.154
1.155 lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"