From 1e02629b88a3d7eea859bef074f3c8e23acb96d1 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Fri, 20 Nov 2015 10:40:04 +0100
Subject: [PATCH] update Isabelle realization of BV (in progress)

---
 lib/isabelle/Why3_BV.thy | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/lib/isabelle/Why3_BV.thy b/lib/isabelle/Why3_BV.thy
index e90369d7d..50e272b1e 100644
--- a/lib/isabelle/Why3_BV.thy
+++ b/lib/isabelle/Why3_BV.thy
@@ -192,12 +192,17 @@ where "lsl v i \<equiv> v << nat i"
 abbreviation (input) lsl_bv :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
 where "lsl_bv v n \<equiv> v << unat n"
 
-abbreviation (input) rotate_left :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-where "rotate_left v n \<equiv> word_rotl (unat n) v"
+abbreviation (input) rotate_left :: "'a::len0 word \<Rightarrow> int \<Rightarrow> 'a word"
+where "rotate_left v n \<equiv> word_rotl (nat n) v"
 
-abbreviation (input) rotate_right :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-where "rotate_right v n \<equiv> word_rotr (unat n) v"
+abbreviation (input) rotate_right :: "'a::len0 word \<Rightarrow> int \<Rightarrow> 'a word"
+where "rotate_right v n \<equiv> word_rotr (nat n) v"
 
+abbreviation (input) rotate_left_bv :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+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"
 
 type_synonym word8 = "8 word"
 
@@ -223,6 +228,8 @@ why3_open "bv/BV8.xml"
     lsl_bv=lsl_bv
     rotate_left=rotate_left
     rotate_right=rotate_right
+    rotate_left_bv=rotate_left_bv
+    rotate_right_bv=rotate_right_bv
     nth=bv_nth
     nth_bv=nth_bv
     to_uint=uint
-- 
GitLab