# HG changeset patch
# User haftmann
# Date 1593624730 0
# Node ID 10a8d943a8d8d611c33572467b0be61c410a669f
# Parent  694009ed4ee1ce5ee198c6a9d0d2db9d03b788b3
more explicit proofs

diff -r 694009ed4ee1 -r 10a8d943a8d8 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Wed Jul 01 22:11:30 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Wed Jul 01 17:32:10 2020 +0000
@@ -545,15 +545,22 @@
 lemmas sbintrunc_minus_simps =
   sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]]
 
-lemmas thobini1 = arg_cong [where f = "\<lambda>w. w BIT b"] for b
-
-lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]
-
-lemmas sbintrunc_Suc_Is =
-  sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans]]
-
-lemmas sbintrunc_Suc_minus_Is =
-  sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans]]
+lemma sbintrunc_BIT_I:
+  \<open>0 < n \<Longrightarrow>
+  sbintrunc (n - 1) 0 = y \<Longrightarrow>
+  sbintrunc n 0 = 2 * y\<close>
+  by simp
+
+lemma sbintrunc_Suc_Is:
+  \<open>sbintrunc n (- 1) = y \<Longrightarrow>
+  sbintrunc (Suc n) (- 1) = 1 + 2 * y\<close>
+  by (auto simp add: Bit_def)
+
+lemma sbintrunc_Suc_minus_Is:
+  \<open>0 < n \<Longrightarrow>
+  sbintrunc (n - 1) w = y \<Longrightarrow>
+  sbintrunc n (w BIT b) = y BIT b\<close>
+  by (cases n) simp_all
 
 lemma sbintrunc_Suc_lem: "sbintrunc (Suc n) x = y \<Longrightarrow> m = Suc n \<Longrightarrow> sbintrunc m x = y"
   by auto