src/HOL/ex/Word_Type.thy
changeset 70348 bde161c740ca
parent 70171 3173d7878274
     1.1 --- a/src/HOL/ex/Word_Type.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/ex/Word_Type.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -136,6 +136,13 @@
     1.4  subsubsection \<open>Conversions\<close>
     1.5  
     1.6  lemma [transfer_rule]:
     1.7 +  "rel_fun HOL.eq (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) numeral numeral"
     1.8 +proof -
     1.9 +  note transfer_rule_numeral [transfer_rule]
    1.10 +  show ?thesis by transfer_prover
    1.11 +qed
    1.12 +
    1.13 +lemma [transfer_rule]:
    1.14    "rel_fun HOL.eq pcr_word int of_nat"
    1.15  proof -
    1.16    note transfer_rule_of_nat [transfer_rule]
    1.17 @@ -236,6 +243,85 @@
    1.18  
    1.19  end
    1.20  
    1.21 +lemma [transfer_rule]:
    1.22 +  "rel_fun pcr_word (\<longleftrightarrow>) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)"
    1.23 +proof -
    1.24 +  have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
    1.25 +    for k :: int
    1.26 +  proof
    1.27 +    assume ?P
    1.28 +    then show ?Q
    1.29 +      by auto
    1.30 +  next
    1.31 +    assume ?Q
    1.32 +    then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
    1.33 +    then have "even (take_bit LENGTH('a) k)"
    1.34 +      by simp
    1.35 +    then show ?P
    1.36 +      by simp
    1.37 +  qed
    1.38 +  show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
    1.39 +    transfer_prover
    1.40 +qed
    1.41 +
    1.42 +instance word :: (len) semiring_modulo
    1.43 +proof
    1.44 +  show "a div b * b + a mod b = a" for a b :: "'a word"
    1.45 +  proof transfer
    1.46 +    fix k l :: int
    1.47 +    define r :: int where "r = 2 ^ LENGTH('a)"
    1.48 +    then have r: "take_bit LENGTH('a) k = k mod r" for k
    1.49 +      by (simp add: take_bit_eq_mod)
    1.50 +    have "k mod r = ((k mod r) div (l mod r) * (l mod r)
    1.51 +      + (k mod r) mod (l mod r)) mod r"
    1.52 +      by (simp add: div_mult_mod_eq)
    1.53 +    also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
    1.54 +      + (k mod r) mod (l mod r)) mod r"
    1.55 +      by (simp add: mod_add_left_eq)
    1.56 +    also have "... = (((k mod r) div (l mod r) * l) mod r
    1.57 +      + (k mod r) mod (l mod r)) mod r"
    1.58 +      by (simp add: mod_mult_right_eq)
    1.59 +    finally have "k mod r = ((k mod r) div (l mod r) * l
    1.60 +      + (k mod r) mod (l mod r)) mod r"
    1.61 +      by (simp add: mod_simps)
    1.62 +    with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l
    1.63 +      + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k"
    1.64 +      by simp
    1.65 +  qed
    1.66 +qed
    1.67 +
    1.68 +instance word :: (len) semiring_parity
    1.69 +proof
    1.70 +  show "\<not> 2 dvd (1::'a word)"
    1.71 +    by transfer simp
    1.72 +  consider (triv) "LENGTH('a) = 1" "take_bit LENGTH('a) 2 = (0 :: int)"
    1.73 +    | (take_bit_2) "take_bit LENGTH('a) 2 = (2 :: int)"
    1.74 +  proof (cases "LENGTH('a) \<ge> 2")
    1.75 +    case False
    1.76 +    then have "LENGTH('a) = 1"
    1.77 +      by (auto simp add: not_le dest: less_2_cases)
    1.78 +    then have "take_bit LENGTH('a) 2 = (0 :: int)"
    1.79 +      by simp
    1.80 +    with \<open>LENGTH('a) = 1\<close> triv show ?thesis
    1.81 +      by simp
    1.82 +  next
    1.83 +    case True
    1.84 +    then obtain n where "LENGTH('a) = Suc (Suc n)"
    1.85 +      by (auto dest: le_Suc_ex)
    1.86 +    then have "take_bit LENGTH('a) 2 = (2 :: int)"
    1.87 +      by simp
    1.88 +    with take_bit_2 show ?thesis
    1.89 +      by simp
    1.90 +  qed
    1.91 +  note * = this
    1.92 +  show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
    1.93 +    for a :: "'a word"
    1.94 +    by (transfer; cases rule: *) (simp_all add: mod_2_eq_odd)
    1.95 +  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
    1.96 +    for a :: "'a word"
    1.97 +    by (transfer; cases rule: *) (simp_all add: mod_2_eq_odd)
    1.98 +qed
    1.99 +
   1.100  
   1.101  subsubsection \<open>Orderings\<close>
   1.102