avoid smt proofs in distribution
authorhaftmann
Thu Dec 07 18:44:04 2017 +0000 (17 months ago)
changeset 67160f37bf261bdf6
parent 67159 deccbba7cfe3
child 67161 b762ed417ed9
avoid smt proofs in distribution
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Misc_Numeric.thy
     1.1 --- a/src/HOL/Word/Bit_Representation.thy	Thu Dec 07 20:55:03 2017 +0100
     1.2 +++ b/src/HOL/Word/Bit_Representation.thy	Thu Dec 07 18:44:04 2017 +0000
     1.3 @@ -142,11 +142,15 @@
     1.4  lemma bin_exhaust: "(\<And>x b. bin = x BIT b \<Longrightarrow> Q) \<Longrightarrow> Q"
     1.5  by (metis bin_ex_rl)
     1.6  
     1.7 -primrec bin_nth
     1.8 +primrec bin_nth :: "int \<Rightarrow> nat \<Rightarrow> bool"
     1.9    where
    1.10      Z: "bin_nth w 0 \<longleftrightarrow> bin_last w"
    1.11    | Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n"
    1.12  
    1.13 +lemma bin_nth_eq_mod:
    1.14 +  "bin_nth w n \<longleftrightarrow> odd (w div 2 ^ n)"
    1.15 +  by (induction n arbitrary: w) (simp_all add: bin_last_def bin_rest_def odd_iff_mod_2_eq_one zdiv_zmult2_eq)
    1.16 +
    1.17  lemma bin_abs_lem: "bin = (w BIT b) \<Longrightarrow> bin \<noteq> -1 \<longrightarrow> bin \<noteq> 0 \<longrightarrow> nat \<bar>w\<bar> < nat \<bar>bin\<bar>"
    1.18    apply clarsimp
    1.19    apply (unfold Bit_def)
    1.20 @@ -266,27 +270,46 @@
    1.21      Z : "sbintrunc 0 bin = (if bin_last bin then -1 else 0)"
    1.22    | Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
    1.23  
    1.24 -lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
    1.25 -  by (induct n arbitrary: w) auto
    1.26 -
    1.27  lemma bintrunc_mod2p: "bintrunc n w = w mod 2 ^ n"
    1.28    by (induct n arbitrary: w) (auto simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
    1.29  
    1.30 -lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
    1.31 -  apply (induct n arbitrary: w)
    1.32 -   apply (auto simp add: bin_last_odd bin_rest_def Bit_def elim!: evenE oddE)
    1.33 -   apply (smt pos_zmod_mult_2 zle2p)
    1.34 -  apply (simp add: mult_mod_right)
    1.35 -  done
    1.36 +lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n"
    1.37 +proof (induction n arbitrary: w)
    1.38 +  case 0
    1.39 +  then show ?case
    1.40 +    by (auto simp add: bin_last_odd odd_iff_mod_2_eq_one)
    1.41 +next
    1.42 +  case (Suc n)
    1.43 +  moreover have "((bin_rest w + 2 ^ n) mod (2 * 2 ^ n) - 2 ^ n) BIT bin_last w =
    1.44 +    (w + 2 * 2 ^ n) mod (4 * 2 ^ n) - 2 * 2 ^ n"
    1.45 +  proof (cases w rule: parity_cases)
    1.46 +    case even
    1.47 +    then show ?thesis
    1.48 +      by (simp add: bin_last_odd bin_rest_def Bit_B0_2t mult_mod_right)
    1.49 +  next
    1.50 +    case odd
    1.51 +    then have "2 * (w div 2) = w - 1"
    1.52 +      using minus_mod_eq_mult_div [of w 2] by simp
    1.53 +    moreover have "(2 * 2 ^ n + w - 1) mod (2 * 2 * 2 ^ n) + 1 = (2 * 2 ^ n + w) mod (2 * 2 * 2 ^ n)"
    1.54 +      using odd emep1 [of "2 * 2 ^ n + w - 1" "2 * 2 * 2 ^ n"] by simp
    1.55 +    ultimately show ?thesis 
    1.56 +      using odd by (simp add: bin_last_odd bin_rest_def Bit_B1_2t mult_mod_right) (simp add: algebra_simps)
    1.57 +  qed
    1.58 +  ultimately show ?case
    1.59 +    by simp
    1.60 +qed
    1.61  
    1.62  
    1.63  subsection "Simplifications for (s)bintrunc"
    1.64  
    1.65 +lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
    1.66 +  by (simp add: bintrunc_mod2p bin_sign_def)
    1.67 +
    1.68  lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
    1.69 -  by (induct n) auto
    1.70 +  by (simp add: bintrunc_mod2p)
    1.71  
    1.72  lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
    1.73 -  by (induct n) auto
    1.74 +  by (simp add: sbintrunc_mod2p)
    1.75  
    1.76  lemma sbintrunc_n_minus1 [simp]: "sbintrunc n (- 1) = -1"
    1.77    by (induct n) auto
     2.1 --- a/src/HOL/Word/Misc_Numeric.thy	Thu Dec 07 20:55:03 2017 +0100
     2.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Thu Dec 07 18:44:04 2017 +0000
     2.3 @@ -8,9 +8,10 @@
     2.4    imports Main
     2.5  begin
     2.6  
     2.7 -lemma one_mod_exp_eq_one [simp]: "1 mod (2 * 2 ^ n) = (1::int)"
     2.8 -  by (smt mod_pos_pos_trivial zero_less_power)
     2.9 -
    2.10 +lemma one_mod_exp_eq_one [simp]:
    2.11 +  "1 mod (2 * 2 ^ n) = (1::int)"
    2.12 +  using power_gt1 [of 2 n] by (auto intro: mod_pos_pos_trivial)
    2.13 +  
    2.14  lemma mod_2_neq_1_eq_eq_0: "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
    2.15    for k :: int
    2.16    by (fact not_mod_2_eq_1_eq_0)