# HG changeset patch
# User haftmann
# Date 1512672244 0
# Node ID f37bf261bdf6897b8586a87e1f2667801f5e09d3
# Parent  deccbba7cfe31677b06a51707e2c16091a70c19b
avoid smt proofs in distribution

diff -r deccbba7cfe3 -r f37bf261bdf6 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Thu Dec 07 20:55:03 2017 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Dec 07 18:44:04 2017 +0000
@@ -142,11 +142,15 @@
 lemma bin_exhaust: "(\<And>x b. bin = x BIT b \<Longrightarrow> Q) \<Longrightarrow> Q"
 by (metis bin_ex_rl)
 
-primrec bin_nth
+primrec bin_nth :: "int \<Rightarrow> nat \<Rightarrow> bool"
   where
     Z: "bin_nth w 0 \<longleftrightarrow> bin_last w"
   | Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n"
 
+lemma bin_nth_eq_mod:
+  "bin_nth w n \<longleftrightarrow> odd (w div 2 ^ n)"
+  by (induction n arbitrary: w) (simp_all add: bin_last_def bin_rest_def odd_iff_mod_2_eq_one zdiv_zmult2_eq)
+
 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>"
   apply clarsimp
   apply (unfold Bit_def)
@@ -266,27 +270,46 @@
     Z : "sbintrunc 0 bin = (if bin_last bin then -1 else 0)"
   | Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
 
-lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
-  by (induct n arbitrary: w) auto
-
 lemma bintrunc_mod2p: "bintrunc n w = w mod 2 ^ n"
   by (induct n arbitrary: w) (auto simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
 
-lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
-  apply (induct n arbitrary: w)
-   apply (auto simp add: bin_last_odd bin_rest_def Bit_def elim!: evenE oddE)
-   apply (smt pos_zmod_mult_2 zle2p)
-  apply (simp add: mult_mod_right)
-  done
+lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n"
+proof (induction n arbitrary: w)
+  case 0
+  then show ?case
+    by (auto simp add: bin_last_odd odd_iff_mod_2_eq_one)
+next
+  case (Suc n)
+  moreover have "((bin_rest w + 2 ^ n) mod (2 * 2 ^ n) - 2 ^ n) BIT bin_last w =
+    (w + 2 * 2 ^ n) mod (4 * 2 ^ n) - 2 * 2 ^ n"
+  proof (cases w rule: parity_cases)
+    case even
+    then show ?thesis
+      by (simp add: bin_last_odd bin_rest_def Bit_B0_2t mult_mod_right)
+  next
+    case odd
+    then have "2 * (w div 2) = w - 1"
+      using minus_mod_eq_mult_div [of w 2] by simp
+    moreover have "(2 * 2 ^ n + w - 1) mod (2 * 2 * 2 ^ n) + 1 = (2 * 2 ^ n + w) mod (2 * 2 * 2 ^ n)"
+      using odd emep1 [of "2 * 2 ^ n + w - 1" "2 * 2 * 2 ^ n"] by simp
+    ultimately show ?thesis 
+      using odd by (simp add: bin_last_odd bin_rest_def Bit_B1_2t mult_mod_right) (simp add: algebra_simps)
+  qed
+  ultimately show ?case
+    by simp
+qed
 
 
 subsection "Simplifications for (s)bintrunc"
 
+lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
+  by (simp add: bintrunc_mod2p bin_sign_def)
+
 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
-  by (induct n) auto
+  by (simp add: bintrunc_mod2p)
 
 lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
-  by (induct n) auto
+  by (simp add: sbintrunc_mod2p)
 
 lemma sbintrunc_n_minus1 [simp]: "sbintrunc n (- 1) = -1"
   by (induct n) auto
diff -r deccbba7cfe3 -r f37bf261bdf6 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Thu Dec 07 20:55:03 2017 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy	Thu Dec 07 18:44:04 2017 +0000
@@ -8,9 +8,10 @@
   imports Main
 begin
 
-lemma one_mod_exp_eq_one [simp]: "1 mod (2 * 2 ^ n) = (1::int)"
-  by (smt mod_pos_pos_trivial zero_less_power)
-
+lemma one_mod_exp_eq_one [simp]:
+  "1 mod (2 * 2 ^ n) = (1::int)"
+  using power_gt1 [of 2 n] by (auto intro: mod_pos_pos_trivial)
+  
 lemma mod_2_neq_1_eq_eq_0: "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
   for k :: int
   by (fact not_mod_2_eq_1_eq_0)