# HG changeset patch
# User haftmann
# Date 1593895521 0
# Node ID c7ac6d4f3914c75a2ac82337c7e2dbc3808d67e9
# Parent  cb7ddc321f521cad24642d0263dfab7b9739bb96
prefer explicit proof

diff -r cb7ddc321f52 -r c7ac6d4f3914 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Jul 03 17:11:57 2020 +0200
+++ b/src/HOL/Word/Word.thy	Sat Jul 04 20:45:21 2020 +0000
@@ -4551,11 +4551,23 @@
 
 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
 
-lemmas test_bit_rsplit_alt =
-  trans [OF nth_rev_alt [THEN test_bit_cong]
-  test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
-
-\<comment> \<open>lazy way of expressing that u and v, and su and sv, have same types\<close>
+lemma test_bit_rsplit_alt:
+  \<open>(word_rsplit w  :: 'b::len word list) ! i !! m \<longleftrightarrow>
+    w !! ((length (word_rsplit w :: 'b::len word list) - Suc i) * size (hd (word_rsplit w :: 'b::len word list)) + m)\<close>
+  if \<open>i < length (word_rsplit w :: 'b::len word list)\<close> \<open>m < size (hd (word_rsplit w :: 'b::len word list))\<close> \<open>0 < length (word_rsplit w :: 'b::len word list)\<close>
+  for w :: \<open>'a::len word\<close>
+  apply (rule trans)
+   apply (rule test_bit_cong)
+   apply (rule nth_rev_alt)
+   apply (rule that(1))
+  apply (rule test_bit_rsplit)
+    apply (rule refl)
+  apply (rule asm_rl)
+   apply (rule that(2))
+  apply (rule diff_Suc_less)
+  apply (rule that(3))
+  done
+
 lemma word_rsplit_len_indep [OF refl refl refl refl]:
   "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
     word_rsplit v = sv \<Longrightarrow> length su = length sv"