Adapted Isabelle realization to changes in bv.why

lib/isabelle/Why3_BV.thy.2015

@@ -240,6 +240,10 @@ where "rotate_left_bv v n \<equiv> word_rotl (unat n) v"
 abbreviation (input) rotate_right_bv :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
 where "rotate_right_bv v n \<equiv> word_rotr (unat n) v"
 
+definition eq_sub_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
+  eq_sub_bv_defn: "eq_sub_bv a b i n =
+    (b AND (mask (unat n) << unat i) = a AND (mask (unat n) << unat i))"
+
 type_synonym word8 = "8 word"
 
 why3_open "bv/BV8.xml"
@@ -271,6 +275,7 @@ why3_open "bv/BV8.xml"
     to_uint=uint
     to_int=sint
     of_int=of_int
+    eq_sub_bv=eq_sub_bv
   types
     t=word8
 
@@ -347,6 +352,9 @@ why3_vc to_uint_of_int
   using assms
   by (simp add: uint_in_range_def word_of_int uint_word_of_int mod_pos_pos_trivial)
 
+why3_vc nth_bv_def
+  by (simp add: word_eq_iff word_ops_nth_size word_size nth_shiftr)
+
 why3_vc Nth_bv_is_nth
   by (simp add: bv_nth_def unat_def)
 
@@ -424,8 +432,10 @@ why3_vc Extensionality
   by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
 
 why3_vc eq_sub_equiv
-  by (simp add: eq_sub_equiv_aux eq_sub_def
-    eq_sub_bv_def [simplified of_int_1, folded mask_def] bv_nth_def)
+  by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
+
+why3_vc eq_sub_bv_def
+  by (simp add: eq_sub_bv_defn mask_def)
 
 why3_end
 
@@ -461,6 +471,7 @@ why3_open "bv/BV16.xml"
     to_uint=uint
     to_int=sint
     of_int=of_int
+    eq_sub_bv=eq_sub_bv
   types
     t=word16
 
@@ -537,6 +548,9 @@ why3_vc to_uint_of_int
   using assms
   by (simp add: uint_in_range_def word_of_int uint_word_of_int mod_pos_pos_trivial)
 
+why3_vc nth_bv_def
+  by (simp add: word_eq_iff word_ops_nth_size word_size nth_shiftr)
+
 why3_vc Nth_bv_is_nth
   by (simp add: bv_nth_def unat_def)
 
@@ -614,8 +628,10 @@ why3_vc Extensionality
   by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
 
 why3_vc eq_sub_equiv
-  by (simp add: eq_sub_equiv_aux eq_sub_def
-    eq_sub_bv_def [simplified of_int_1, folded mask_def] bv_nth_def)
+  by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
+
+why3_vc eq_sub_bv_def
+  by (simp add: eq_sub_bv_defn mask_def)
 
 why3_end
 
@@ -651,6 +667,7 @@ why3_open "bv/BV32.xml"
     to_uint=uint
     to_int=sint
     of_int=of_int
+    eq_sub_bv=eq_sub_bv
   types
     t=word32
 
@@ -727,6 +744,9 @@ why3_vc to_uint_of_int
   using assms
   by (simp add: uint_in_range_def word_of_int uint_word_of_int mod_pos_pos_trivial)
 
+why3_vc nth_bv_def
+  by (simp add: word_eq_iff word_ops_nth_size word_size nth_shiftr)
+
 why3_vc Nth_bv_is_nth
   by (simp add: bv_nth_def unat_def)
 
@@ -804,8 +824,10 @@ why3_vc Extensionality
   by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
 
 why3_vc eq_sub_equiv
-  by (simp add: eq_sub_equiv_aux eq_sub_def
-    eq_sub_bv_def [simplified of_int_1, folded mask_def] bv_nth_def)
+  by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
+
+why3_vc eq_sub_bv_def
+  by (simp add: eq_sub_bv_defn mask_def)
 
 why3_end
 
@@ -841,6 +863,7 @@ why3_open "bv/BV64.xml"
     to_uint=uint
     to_int=sint
     of_int=of_int
+    eq_sub_bv=eq_sub_bv
   types
     t=word64
 
@@ -917,6 +940,9 @@ why3_vc to_uint_of_int
   using assms
   by (simp add: uint_in_range_def word_of_int uint_word_of_int mod_pos_pos_trivial)
 
+why3_vc nth_bv_def
+  by (simp add: word_eq_iff word_ops_nth_size word_size nth_shiftr)
+
 why3_vc Nth_bv_is_nth
   by (simp add: bv_nth_def unat_def)
 
@@ -994,8 +1020,10 @@ why3_vc Extensionality
   by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
 
 why3_vc eq_sub_equiv
-  by (simp add: eq_sub_equiv_aux eq_sub_def
-    eq_sub_bv_def [simplified of_int_1, folded mask_def] bv_nth_def)
+  by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
+
+why3_vc eq_sub_bv_def
+  by (simp add: eq_sub_bv_defn mask_def)
 
 why3_end
 

lib/isabelle/Why3_BV.thy.2016

@@ -240,6 +240,10 @@ where "rotate_left_bv v n \<equiv> word_rotl (unat n) v"
 abbreviation (input) rotate_right_bv :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
 where "rotate_right_bv v n \<equiv> word_rotr (unat n) v"
 
+definition eq_sub_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
+  eq_sub_bv_defn: "eq_sub_bv a b i n =
+    (b AND (mask (unat n) << unat i) = a AND (mask (unat n) << unat i))"
+
 type_synonym word8 = "8 word"
 
 why3_open "bv/BV8.xml"
@@ -271,6 +275,7 @@ why3_open "bv/BV8.xml"
     to_uint=uint
     to_int=sint
     of_int=of_int
+    eq_sub_bv=eq_sub_bv
   types
     t=word8
 
@@ -347,6 +352,9 @@ why3_vc to_uint_of_int
   using assms
   by (simp add: uint_in_range_def word_of_int uint_word_of_int mod_pos_pos_trivial)
 
+why3_vc nth_bv_def
+  by (simp add: word_eq_iff word_ops_nth_size word_size nth_shiftr)
+
 why3_vc Nth_bv_is_nth
   by (simp add: bv_nth_def unat_def)
 
@@ -424,8 +432,10 @@ why3_vc Extensionality
   by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
 
 why3_vc eq_sub_equiv
-  by (simp add: eq_sub_equiv_aux eq_sub_def
-    eq_sub_bv_def [simplified of_int_1, folded mask_def] bv_nth_def)
+  by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
+
+why3_vc eq_sub_bv_def
+  by (simp add: eq_sub_bv_defn mask_def)
 
 why3_end
 
@@ -461,6 +471,7 @@ why3_open "bv/BV16.xml"
     to_uint=uint
     to_int=sint
     of_int=of_int
+    eq_sub_bv=eq_sub_bv
   types
     t=word16
 
@@ -537,6 +548,9 @@ why3_vc to_uint_of_int
   using assms
   by (simp add: uint_in_range_def word_of_int uint_word_of_int mod_pos_pos_trivial)
 
+why3_vc nth_bv_def
+  by (simp add: word_eq_iff word_ops_nth_size word_size nth_shiftr)
+
 why3_vc Nth_bv_is_nth
   by (simp add: bv_nth_def unat_def)
 
@@ -614,8 +628,10 @@ why3_vc Extensionality
   by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
 
 why3_vc eq_sub_equiv
-  by (simp add: eq_sub_equiv_aux eq_sub_def
-    eq_sub_bv_def [simplified of_int_1, folded mask_def] bv_nth_def)
+  by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
+
+why3_vc eq_sub_bv_def
+  by (simp add: eq_sub_bv_defn mask_def)
 
 why3_end
 
@@ -651,6 +667,7 @@ why3_open "bv/BV32.xml"
     to_uint=uint
     to_int=sint
     of_int=of_int
+    eq_sub_bv=eq_sub_bv
   types
     t=word32
 
@@ -727,6 +744,9 @@ why3_vc to_uint_of_int
   using assms
   by (simp add: uint_in_range_def word_of_int uint_word_of_int mod_pos_pos_trivial)
 
+why3_vc nth_bv_def
+  by (simp add: word_eq_iff word_ops_nth_size word_size nth_shiftr)
+
 why3_vc Nth_bv_is_nth
   by (simp add: bv_nth_def unat_def)
 
@@ -804,8 +824,10 @@ why3_vc Extensionality
   by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
 
 why3_vc eq_sub_equiv
-  by (simp add: eq_sub_equiv_aux eq_sub_def
-    eq_sub_bv_def [simplified of_int_1, folded mask_def] bv_nth_def)
+  by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
+
+why3_vc eq_sub_bv_def
+  by (simp add: eq_sub_bv_defn mask_def)
 
 why3_end
 
@@ -841,6 +863,7 @@ why3_open "bv/BV64.xml"
     to_uint=uint
     to_int=sint
     of_int=of_int
+    eq_sub_bv=eq_sub_bv
   types
     t=word64
 
@@ -917,6 +940,9 @@ why3_vc to_uint_of_int
   using assms
   by (simp add: uint_in_range_def word_of_int uint_word_of_int mod_pos_pos_trivial)
 
+why3_vc nth_bv_def
+  by (simp add: word_eq_iff word_ops_nth_size word_size nth_shiftr)
+
 why3_vc Nth_bv_is_nth
   by (simp add: bv_nth_def unat_def)
 
@@ -994,8 +1020,10 @@ why3_vc Extensionality
   by (simp add: eq_sub_def bv_nth_def word_eq_iff all_nat)
 
 why3_vc eq_sub_equiv
-  by (simp add: eq_sub_equiv_aux eq_sub_def
-    eq_sub_bv_def [simplified of_int_1, folded mask_def] bv_nth_def)
+  by (simp add: eq_sub_equiv_aux eq_sub_def eq_sub_bv_defn bv_nth_def)
+
+why3_vc eq_sub_bv_def
+  by (simp add: eq_sub_bv_defn mask_def)
 
 why3_end