more theorems for proof of concept for word type
authorhaftmann
Fri Jun 14 08:34:28 2019 +0000 (5 weeks ago ago)
changeset 70533bde161c740ca
parent 70532 e5cd5471c18a
child 70534 697450fd25c1
more theorems for proof of concept for word type
src/HOL/Library/Type_Length.thy
src/HOL/ex/Word_Type.thy
     1.1 --- a/src/HOL/Library/Type_Length.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Library/Type_Length.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -33,6 +33,13 @@
     1.4  
     1.5  class len = len0 +
     1.6    assumes len_gt_0 [iff]: "0 < LENGTH('a)"
     1.7 +begin
     1.8 +
     1.9 +lemma len_not_eq_0 [simp]:
    1.10 +  "LENGTH('a) \<noteq> 0"
    1.11 +  by simp
    1.12 +
    1.13 +end
    1.14  
    1.15  instantiation num0 and num1 :: len0
    1.16  begin
     2.1 --- a/src/HOL/ex/Word_Type.thy	Fri Jun 14 08:34:28 2019 +0000
     2.2 +++ b/src/HOL/ex/Word_Type.thy	Fri Jun 14 08:34:28 2019 +0000
     2.3 @@ -136,6 +136,13 @@
     2.4  subsubsection \<open>Conversions\<close>
     2.5  
     2.6  lemma [transfer_rule]:
     2.7 +  "rel_fun HOL.eq (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) numeral numeral"
     2.8 +proof -
     2.9 +  note transfer_rule_numeral [transfer_rule]
    2.10 +  show ?thesis by transfer_prover
    2.11 +qed
    2.12 +
    2.13 +lemma [transfer_rule]:
    2.14    "rel_fun HOL.eq pcr_word int of_nat"
    2.15  proof -
    2.16    note transfer_rule_of_nat [transfer_rule]
    2.17 @@ -236,6 +243,85 @@
    2.18  
    2.19  end
    2.20  
    2.21 +lemma [transfer_rule]:
    2.22 +  "rel_fun pcr_word (\<longleftrightarrow>) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)"
    2.23 +proof -
    2.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")
    2.25 +    for k :: int
    2.26 +  proof
    2.27 +    assume ?P
    2.28 +    then show ?Q
    2.29 +      by auto
    2.30 +  next
    2.31 +    assume ?Q
    2.32 +    then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
    2.33 +    then have "even (take_bit LENGTH('a) k)"
    2.34 +      by simp
    2.35 +    then show ?P
    2.36 +      by simp
    2.37 +  qed
    2.38 +  show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
    2.39 +    transfer_prover
    2.40 +qed
    2.41 +
    2.42 +instance word :: (len) semiring_modulo
    2.43 +proof
    2.44 +  show "a div b * b + a mod b = a" for a b :: "'a word"
    2.45 +  proof transfer
    2.46 +    fix k l :: int
    2.47 +    define r :: int where "r = 2 ^ LENGTH('a)"
    2.48 +    then have r: "take_bit LENGTH('a) k = k mod r" for k
    2.49 +      by (simp add: take_bit_eq_mod)
    2.50 +    have "k mod r = ((k mod r) div (l mod r) * (l mod r)
    2.51 +      + (k mod r) mod (l mod r)) mod r"
    2.52 +      by (simp add: div_mult_mod_eq)
    2.53 +    also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
    2.54 +      + (k mod r) mod (l mod r)) mod r"
    2.55 +      by (simp add: mod_add_left_eq)
    2.56 +    also have "... = (((k mod r) div (l mod r) * l) mod r
    2.57 +      + (k mod r) mod (l mod r)) mod r"
    2.58 +      by (simp add: mod_mult_right_eq)
    2.59 +    finally have "k mod r = ((k mod r) div (l mod r) * l
    2.60 +      + (k mod r) mod (l mod r)) mod r"
    2.61 +      by (simp add: mod_simps)
    2.62 +    with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l
    2.63 +      + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k"
    2.64 +      by simp
    2.65 +  qed
    2.66 +qed
    2.67 +
    2.68 +instance word :: (len) semiring_parity
    2.69 +proof
    2.70 +  show "\<not> 2 dvd (1::'a word)"
    2.71 +    by transfer simp
    2.72 +  consider (triv) "LENGTH('a) = 1" "take_bit LENGTH('a) 2 = (0 :: int)"
    2.73 +    | (take_bit_2) "take_bit LENGTH('a) 2 = (2 :: int)"
    2.74 +  proof (cases "LENGTH('a) \<ge> 2")
    2.75 +    case False
    2.76 +    then have "LENGTH('a) = 1"
    2.77 +      by (auto simp add: not_le dest: less_2_cases)
    2.78 +    then have "take_bit LENGTH('a) 2 = (0 :: int)"
    2.79 +      by simp
    2.80 +    with \<open>LENGTH('a) = 1\<close> triv show ?thesis
    2.81 +      by simp
    2.82 +  next
    2.83 +    case True
    2.84 +    then obtain n where "LENGTH('a) = Suc (Suc n)"
    2.85 +      by (auto dest: le_Suc_ex)
    2.86 +    then have "take_bit LENGTH('a) 2 = (2 :: int)"
    2.87 +      by simp
    2.88 +    with take_bit_2 show ?thesis
    2.89 +      by simp
    2.90 +  qed
    2.91 +  note * = this
    2.92 +  show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
    2.93 +    for a :: "'a word"
    2.94 +    by (transfer; cases rule: *) (simp_all add: mod_2_eq_odd)
    2.95 +  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
    2.96 +    for a :: "'a word"
    2.97 +    by (transfer; cases rule: *) (simp_all add: mod_2_eq_odd)
    2.98 +qed
    2.99 +
   2.100  
   2.101  subsubsection \<open>Orderings\<close>
   2.102