Adapted Isabelle realization to changes in bit vector theory

lib/isabelle/Why3_BV.thy.2016

@@ -244,6 +244,9 @@ definition eq_sub_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a wor
   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))"
 
+definition size_bv :: "'a::len word" where
+  "size_bv = of_nat (len_of TYPE('a))"
+
 type_synonym word8 = "8 word"
 
 why3_open "bv/BV8.xml"
@@ -272,10 +275,12 @@ why3_open "bv/BV8.xml"
     rotate_right_bv=rotate_right_bv
     nth=bv_nth
     nth_bv=nth_bv
-    to_uint=uint
+    tqtint=uint
     to_int=sint
     of_int=of_int
     eq_sub_bv=eq_sub_bv
+    size_bv=size_bv
+    one=one_class.one
   types
     t=word8
 
@@ -360,9 +365,15 @@ why3_vc Nth_bv_is_nth2
   using assms
   by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
 
-why3_vc Of_int_zeros by simp
+why3_vc tqtaxiom using to_uint_bounds [of i] by auto
+
+why3_vc to_uint_size_bv by (simp add: size_bv_def)
+
+why3_vc to_uint_zeros by simp
 
-why3_vc Of_int_ones by (simp add: max_word_eq)
+why3_vc to_uint_one by simp
+
+why3_vc to_uint_ones by (simp add: max_word_eq)
 
 why3_vc to_uint_add
   by (simp add: uint_word_arith_bintrs bintrunc_mod2p emod_def)
@@ -462,10 +473,12 @@ why3_open "bv/BV16.xml"
     rotate_right_bv=rotate_right_bv
     nth=bv_nth
     nth_bv=nth_bv
-    to_uint=uint
+    tqtint=uint
     to_int=sint
     of_int=of_int
     eq_sub_bv=eq_sub_bv
+    size_bv=size_bv
+    one=one_class.one
   types
     t=word16
 
@@ -550,9 +563,15 @@ why3_vc Nth_bv_is_nth2
   using assms
   by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
 
-why3_vc Of_int_zeros by simp
+why3_vc tqtaxiom using to_uint_bounds [of i] by auto
+
+why3_vc to_uint_size_bv by (simp add: size_bv_def)
+
+why3_vc to_uint_zeros by simp
 
-why3_vc Of_int_ones by (simp add: max_word_eq)
+why3_vc to_uint_one by simp
+
+why3_vc to_uint_ones by (simp add: max_word_eq)
 
 why3_vc to_uint_add
   by (simp add: uint_word_arith_bintrs bintrunc_mod2p emod_def)
@@ -652,10 +671,12 @@ why3_open "bv/BV32.xml"
     rotate_right_bv=rotate_right_bv
     nth=bv_nth
     nth_bv=nth_bv
-    to_uint=uint
+    tqtint=uint
     to_int=sint
     of_int=of_int
     eq_sub_bv=eq_sub_bv
+    size_bv=size_bv
+    one=one_class.one
   types
     t=word32
 
@@ -740,9 +761,15 @@ why3_vc Nth_bv_is_nth2
   using assms
   by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
 
-why3_vc Of_int_zeros by simp
+why3_vc tqtaxiom using to_uint_bounds [of i] by auto
+
+why3_vc to_uint_size_bv by (simp add: size_bv_def)
+
+why3_vc to_uint_zeros by simp
 
-why3_vc Of_int_ones by (simp add: max_word_eq)
+why3_vc to_uint_one by simp
+
+why3_vc to_uint_ones by (simp add: max_word_eq)
 
 why3_vc to_uint_add
   by (simp add: uint_word_arith_bintrs bintrunc_mod2p emod_def)
@@ -842,10 +869,12 @@ why3_open "bv/BV64.xml"
     rotate_right_bv=rotate_right_bv
     nth=bv_nth
     nth_bv=nth_bv
-    to_uint=uint
+    tqtint=uint
     to_int=sint
     of_int=of_int
     eq_sub_bv=eq_sub_bv
+    size_bv=size_bv
+    one=one_class.one
   types
     t=word64
 
@@ -930,9 +959,15 @@ why3_vc Nth_bv_is_nth2
   using assms
   by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
 
-why3_vc Of_int_zeros by simp
+why3_vc tqtaxiom using to_uint_bounds [of i] by auto
+
+why3_vc to_uint_size_bv by (simp add: size_bv_def)
+
+why3_vc to_uint_zeros by simp
 
-why3_vc Of_int_ones by (simp add: max_word_eq)
+why3_vc to_uint_one by simp
+
+why3_vc to_uint_ones by (simp add: max_word_eq)
 
 why3_vc to_uint_add
   by (simp add: uint_word_arith_bintrs bintrunc_mod2p emod_def)
@@ -1004,14 +1039,27 @@ why3_vc eq_sub_bv_def
 why3_end
 
 
+definition rliteral_8 :: "'a::len0 word" where
+  "rliteral_8 = 2 ^ 8 - 1"
+
+definition rliteral_16 :: "'a::len0 word" where
+  "rliteral_16 = 2 ^ 16 - 1"
+
+definition rliteral_32 :: "'a::len0 word" where
+  "rliteral_32 = 2 ^ 32 - 1"
+
+
 why3_open "bv/BVConverter_32_64.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_32
+
+why3_vc rliteral_axiom by (simp add: rliteral_32_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_32_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)
@@ -1023,10 +1071,13 @@ why3_open "bv/BVConverter_16_64.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_16
+
+why3_vc rliteral_axiom by (simp add: rliteral_16_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_16_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)
@@ -1038,10 +1089,13 @@ why3_open "bv/BVConverter_8_64.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_8
+
+why3_vc rliteral_axiom by (simp add: rliteral_8_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)
@@ -1053,10 +1107,13 @@ why3_open "bv/BVConverter_16_32.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_16
+
+why3_vc rliteral_axiom by (simp add: rliteral_16_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_16_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)
@@ -1068,10 +1125,13 @@ why3_open "bv/BVConverter_8_32.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_8
+
+why3_vc rliteral_axiom by (simp add: rliteral_8_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)
@@ -1083,10 +1143,13 @@ why3_open "bv/BVConverter_8_16.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_8
+
+why3_vc rliteral_axiom by (simp add: rliteral_8_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV16.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV16.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)

lib/isabelle/Why3_BV.thy.2016-1

@@ -244,6 +244,9 @@ definition eq_sub_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a wor
   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))"
 
+definition size_bv :: "'a::len word" where
+  "size_bv = of_nat LENGTH('a)"
+
 type_synonym word8 = "8 word"
 
 why3_open "bv/BV8.xml"
@@ -272,10 +275,12 @@ why3_open "bv/BV8.xml"
     rotate_right_bv=rotate_right_bv
     nth=bv_nth
     nth_bv=nth_bv
-    to_uint=uint
+    tqtint=uint
     to_int=sint
     of_int=of_int
     eq_sub_bv=eq_sub_bv
+    size_bv=size_bv
+    one=one_class.one
   types
     t=word8
 
@@ -360,9 +365,15 @@ why3_vc Nth_bv_is_nth2
   using assms
   by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
 
-why3_vc Of_int_zeros by simp
+why3_vc tqtaxiom using to_uint_bounds [of i] by auto
+
+why3_vc to_uint_size_bv by (simp add: size_bv_def)
+
+why3_vc to_uint_zeros by simp
 
-why3_vc Of_int_ones by (simp add: max_word_eq)
+why3_vc to_uint_one by simp
+
+why3_vc to_uint_ones by (simp add: max_word_eq)
 
 why3_vc to_uint_add
   by (simp add: uint_word_arith_bintrs bintrunc_mod2p emod_def)
@@ -462,10 +473,12 @@ why3_open "bv/BV16.xml"
     rotate_right_bv=rotate_right_bv
     nth=bv_nth
     nth_bv=nth_bv
-    to_uint=uint
+    tqtint=uint
     to_int=sint
     of_int=of_int
     eq_sub_bv=eq_sub_bv
+    size_bv=size_bv
+    one=one_class.one
   types
     t=word16
 
@@ -550,9 +563,15 @@ why3_vc Nth_bv_is_nth2
   using assms
   by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
 
-why3_vc Of_int_zeros by simp
+why3_vc tqtaxiom using to_uint_bounds [of i] by auto
+
+why3_vc to_uint_size_bv by (simp add: size_bv_def)
+
+why3_vc to_uint_zeros by simp
 
-why3_vc Of_int_ones by (simp add: max_word_eq)
+why3_vc to_uint_one by simp
+
+why3_vc to_uint_ones by (simp add: max_word_eq)
 
 why3_vc to_uint_add
   by (simp add: uint_word_arith_bintrs bintrunc_mod2p emod_def)
@@ -652,10 +671,12 @@ why3_open "bv/BV32.xml"
     rotate_right_bv=rotate_right_bv
     nth=bv_nth
     nth_bv=nth_bv
-    to_uint=uint
+    tqtint=uint
     to_int=sint
     of_int=of_int
     eq_sub_bv=eq_sub_bv
+    size_bv=size_bv
+    one=one_class.one
   types
     t=word32
 
@@ -740,9 +761,15 @@ why3_vc Nth_bv_is_nth2
   using assms
   by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
 
-why3_vc Of_int_zeros by simp
+why3_vc tqtaxiom using to_uint_bounds [of i] by auto
+
+why3_vc to_uint_size_bv by (simp add: size_bv_def)
+
+why3_vc to_uint_zeros by simp
 
-why3_vc Of_int_ones by (simp add: max_word_eq)
+why3_vc to_uint_one by simp
+
+why3_vc to_uint_ones by (simp add: max_word_eq)
 
 why3_vc to_uint_add
   by (simp add: uint_word_arith_bintrs bintrunc_mod2p emod_def)
@@ -842,10 +869,12 @@ why3_open "bv/BV64.xml"
     rotate_right_bv=rotate_right_bv
     nth=bv_nth
     nth_bv=nth_bv
-    to_uint=uint
+    tqtint=uint
     to_int=sint
     of_int=of_int
     eq_sub_bv=eq_sub_bv
+    size_bv=size_bv
+    one=one_class.one
   types
     t=word64
 
@@ -930,9 +959,15 @@ why3_vc Nth_bv_is_nth2
   using assms
   by (simp add: bv_nth_def unat_def to_uint_of_int uint_in_range_def)
 
-why3_vc Of_int_zeros by simp
+why3_vc tqtaxiom using to_uint_bounds [of i] by auto
+
+why3_vc to_uint_size_bv by (simp add: size_bv_def)
+
+why3_vc to_uint_zeros by simp
 
-why3_vc Of_int_ones by (simp add: max_word_eq)
+why3_vc to_uint_one by simp
+
+why3_vc to_uint_ones by (simp add: max_word_eq)
 
 why3_vc to_uint_add
   by (simp add: uint_word_arith_bintrs bintrunc_mod2p emod_def)
@@ -1004,14 +1039,27 @@ why3_vc eq_sub_bv_def
 why3_end
 
 
+definition rliteral_8 :: "'a::len0 word" where
+  "rliteral_8 = 2 ^ 8 - 1"
+
+definition rliteral_16 :: "'a::len0 word" where
+  "rliteral_16 = 2 ^ 16 - 1"
+
+definition rliteral_32 :: "'a::len0 word" where
+  "rliteral_32 = 2 ^ 32 - 1"
+
+
 why3_open "bv/BVConverter_32_64.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_32
+
+why3_vc rliteral_axiom by (simp add: rliteral_32_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_32_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)
@@ -1023,10 +1071,13 @@ why3_open "bv/BVConverter_16_64.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_16
+
+why3_vc rliteral_axiom by (simp add: rliteral_16_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_16_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)
@@ -1038,10 +1089,13 @@ why3_open "bv/BVConverter_8_64.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_8
+
+why3_vc rliteral_axiom by (simp add: rliteral_8_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV64.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)
@@ -1053,10 +1107,13 @@ why3_open "bv/BVConverter_16_32.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_16
+
+why3_vc rliteral_axiom by (simp add: rliteral_16_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_16_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)
@@ -1068,10 +1125,13 @@ why3_open "bv/BVConverter_8_32.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_8
+
+why3_vc rliteral_axiom by (simp add: rliteral_8_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV32.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)
@@ -1083,10 +1143,13 @@ why3_open "bv/BVConverter_8_16.xml"
   constants
     toBig = ucast
     toSmall = ucast
+    rliteral = rliteral_8
+
+why3_vc rliteral_axiom by (simp add: rliteral_8_def)
 
 why3_vc toSmall_to_uint
   using assms
-  by (simp add: BV16.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial)
+  by (simp add: BV16.ule_def ucast_def uint_word_of_int mod_pos_pos_trivial rliteral_8_def)
 
 why3_vc toBig_to_uint
   by (simp add: uint_up_ucast is_up)