# HG changeset patch
# User haftmann
# Date 1575187260 0
# Node ID eda1ef0090ef95b16c30c870313ef816fe90ad88
# Parent  410935efbf5c04ffc2e5df2a6ab6d6f302873499
transfer rule for bit operation

diff -r 410935efbf5c -r eda1ef0090ef src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Sun Dec 01 08:00:59 2019 +0000
+++ b/src/HOL/ex/Word.thy	Sun Dec 01 08:01:00 2019 +0000
@@ -646,6 +646,23 @@
     done
 qed
 
+context
+  includes lifting_syntax
+begin
+
+lemma transfer_rule_bit_word:
+  \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) bit\<close>
+proof -
+  let ?t = \<open>\<lambda>a n. odd (take_bit LENGTH('a) a div take_bit LENGTH('a) ((2::int) ^ n))\<close>
+  have \<open>((pcr_word :: int \<Rightarrow> 'a word \<Rightarrow> bool) ===> (=)) ?t bit\<close>
+    by (unfold bit_def) transfer_prover
+  also have \<open>?t = (\<lambda>k n. n < LENGTH('a) \<and> bit k n)\<close>
+    by (simp add: fun_eq_iff bit_take_bit_iff flip: bit_def)
+  finally show ?thesis .
+qed
+
+end
+
 instantiation word :: (len) semiring_bit_shifts
 begin