author haftmann Thu Dec 07 18:44:04 2017 +0000 (17 months ago) changeset 67160 f37bf261bdf6 parent 67159 deccbba7cfe3 child 67161 b762ed417ed9
avoid smt proofs in distribution
```     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)
```