src/HOL/Word/Word.thy
changeset 55817 0bc0217387a5
parent 55816 e8dd03241e86
child 55818 d8b2f50705d0
     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"