Commit 93445554 authored by MARCHE Claude's avatar MARCHE Claude

Merge remote-tracking branch 'sberghofer/master'

parents 513e98dd b98ab16c
......@@ -157,8 +157,7 @@ pvsbin/
/lib/isabelle/map/
/lib/isabelle/real/
/lib/isabelle/set/
/lib/isabelle/Tools/why3
/lib/isabelle/Why3_Number.thy
/lib/isabelle/Why3_BV.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
/lib/isabelle/bv
......
......@@ -1144,7 +1144,7 @@ clean::
ifeq (@enable_isabelle_libs@,yes)
ISABELLEVERSIONSPECIFIC=why3.ML Tools/why3 Why3_Number.thy
ISABELLEVERSIONSPECIFIC=why3.ML Why3_BV.thy
ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS))
......
......@@ -618,21 +618,21 @@ else
ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEDETECTEDVERSION in
2014*)
2015*)
enable_isabelle_support=yes
ISABELLEVERSION=2014
ISABELLEVERSION=2015
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
2015*)
2016*)
enable_isabelle_support=yes
ISABELLEVERSION=2015
ISABELLEVERSION=2016
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
*)
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle 2014 or 2015; Isabelle discarded)
reason_isabelle_support=" (need version >= 2014)"
AC_MSG_WARN(You need Isabelle 2015 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2015)"
;;
esac
fi
......
......@@ -11,9 +11,9 @@ using ``Edit'' action in \texttt{why3ide}.
\subsection{Installation}
You need version Isabelle2014 or Isabelle2015. Former versions are not
supported. We assume below that your version is 2015, please replace
2015 by 2014 otherwise.
You need version Isabelle2015 or Isabelle2016. Former versions are not
supported. We assume below that your version is 2016, please replace
2016 by 2015 otherwise.
Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path
......@@ -22,7 +22,7 @@ and installation of \why, you must manually add the path
\end{verbatim}
into either the user file
\begin{verbatim}
.isabelle/Isabelle2015/etc/components
.isabelle/Isabelle2016/etc/components
\end{verbatim}
or the system-wide file
\begin{verbatim}
......
theory number.Parity
syntax predicate even "<app><const name=\"Parity.even_odd_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.even_odd_class.odd\"/>%1</app>"
end
theory number.Parity
syntax predicate even "<app><const name=\"Parity.semiring_parity_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.semiring_parity_class.odd\"/>%1</app>"
theory algebra.Field
syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
syntax function (/) "<app><const name=\"Fields.inverse_class.divide\"/>%1%2</app>"
end
theory algebra.Field
syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
syntax function (/) "<app><const name=\"Rings.divide_class.divide\"/>%1%2</app>"
end
......@@ -150,6 +150,11 @@ theory set.Fset
syntax function cardinal "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"FSet.fcard\"/>%1</app></app>"
end
theory number.Parity
syntax predicate even "<app><const name=\"Parity.semiring_parity_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.semiring_parity_class.odd\"/>%1</app>"
end
theory number.Divisibility
syntax predicate divides "<app><const name=\"Rings.dvd_class.dvd\"/>%1%2</app>"
end
......@@ -166,11 +171,6 @@ theory number.Coprime
syntax predicate coprime "<app><const name=\"GCD.gcd_class.coprime\"/>%1%2</app>"
end
theory algebra.Field
syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
syntax function (/) "<app><const name=\"Fields.inverse_class.divide\"/>%1%2</app>"
end
theory real.Real
syntax function zero "<number val=\"0\"><type name=\"Real.real\"/></number>"
syntax function one "<number val=\"1\"><type name=\"Real.real\"/></number>"
......
......@@ -7,4 +7,4 @@ filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2014.gen"
import "isabelle-2016.gen"
......@@ -8,7 +8,7 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2014.gen"
import "isabelle-2016.gen"
transformation "simplify_trivial_quantification_in_goal"
#!/usr/bin/env bash
#
# DESCRIPTION: process files generated by Why3
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] WHY3_FILE"
echo
echo " Options are:"
echo " -b batch mode"
echo " -i NAME interactive mode using interface NAME"
echo
echo "Process files generated by Why3."
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## utilities
function make_theory()
{
BNAME=`basename "$1"`
if [ ! -e "$1.thy" ]; then
echo -e "theory $BNAME\nimports Why3\nbegin\n\nwhy3_open \"$BNAME.xml\"\n" > "$1.thy"
sed \
-e 's/<lemma name="\([^"]*\)"[^>]*>/why3_vc \1\n\n/g' \
-e 's/<[^l][^>]*>//g' \
"$1.xml" >> "$1.thy"
echo -e "why3_end\n\nend" >> "$1.thy"
fi
}
## process command line
while getopts "bi:" OPT
do
case "$OPT" in
b)
BATCH=true
;;
i)
INTERACTIVE=true
INTERFACE="$OPTARG"
;;
\?)
usage
;;
esac
done
## main
shift $(($OPTIND - 1))
[ "$#" != 1 ] && usage
NAME=`dirname "$1"`/`basename "$1" .xml`
if [ "$BATCH" = true ]; then
"$ISABELLE_PROCESS" -e "use_thy \"$NAME\";" -rq Why3
elif [ "$INTERACTIVE" = true ]; then
make_theory "$NAME"
case "$INTERFACE" in
emacs)
"$ISABELLE_TOOL" emacs -L Why3 "${NAME}.thy"
;;
jedit)
if [ -f "$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER" ]; then
"$ISABELLE_TOOL" java -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
"-settings=$(jvmpath "$JEDIT_SETTINGS")" "-server=$WHY3_JEDIT_SERVER" \
-reuseview -wait "$(jvmpath "${NAME}.thy")"
else
"$ISABELLE_TOOL" jedit -l Why3 "${NAME}.thy"
fi
;;
*)
fail "Unknown Isabelle interface: \"$INTERFACE\""
;;
esac
else
usage
fi
......@@ -240,11 +240,15 @@ 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"
constants
zero=zero_class.zero
zeros=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
......@@ -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
......@@ -280,7 +285,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zeros by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
......@@ -311,7 +316,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zeros by simp
why3_vc Asr_nth_low
using assms
......@@ -323,7 +328,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zeros by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
......@@ -333,7 +338,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
......@@ -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)
......@@ -354,7 +362,7 @@ 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_zero by simp
why3_vc Of_int_zeros by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
......@@ -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
......@@ -434,7 +444,7 @@ type_synonym word16 = "16 word"
why3_open "bv/BV16.xml"
constants
zero=zero_class.zero
zeros=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
......@@ -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
......@@ -470,7 +481,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zeros by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
......@@ -501,7 +512,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zeros by simp
why3_vc Asr_nth_low
using assms
......@@ -513,7 +524,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zeros by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
......@@ -523,7 +534,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
......@@ -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)
......@@ -544,7 +558,7 @@ 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_zero by simp
why3_vc Of_int_zeros by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
......@@ -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
......@@ -624,7 +640,7 @@ type_synonym word32 = "32 word"
why3_open "bv/BV32.xml"
constants
zero=zero_class.zero
zeros=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
......@@ -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
......@@ -660,7 +677,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zeros by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
......@@ -691,7 +708,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zeros by simp
why3_vc Asr_nth_low
using assms
......@@ -703,7 +720,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zeros by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
......@@ -713,7 +730,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
......@@ -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)
......@@ -734,7 +754,7 @@ 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_zero by simp
why3_vc Of_int_zeros by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
......@@ -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
......@@ -814,7 +836,7 @@ type_synonym word64 = "64 word"
why3_open "bv/BV64.xml"
constants
zero=zero_class.zero
zeros=zero_class.zero
ones=max_word
bw_and=bitAND
bw_or=bitOR
......@@ -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
......@@ -850,7 +873,7 @@ why3_vc nth_out_of_bound
using assms
by (auto simp add: bv_nth_def test_bit_bin)
why3_vc Nth_zero by (simp add: bv_nth_def)
why3_vc Nth_zeros by (simp add: bv_nth_def)
why3_vc Nth_ones
using assms
......@@ -881,7 +904,7 @@ why3_vc Lsr_nth_high
by (simp add: bv_nth_def nth_shiftr)
(simp add: test_bit_bin nat_add_distrib [symmetric] nat_less_iff)
why3_vc lsr_zero by simp
why3_vc lsr_zeros by simp
why3_vc Asr_nth_low
using assms
......@@ -893,7 +916,7 @@ why3_vc Asr_nth_high
by (simp add: bv_nth_def nth_sshiftr word_size)
(simp add: nat_add_distrib [symmetric] le_nat_iff nat_less_iff)
why3_vc asr_zero by (simp add: sshiftr_def)
why3_vc asr_zeros by (simp add: sshiftr_def)
why3_vc Lsl_nth_high
using assms
......@@ -903,7 +926,7 @@ why3_vc Lsl_nth_low
using assms
by (simp add: bv_nth_def nth_shiftl nat_le_eq_zle)
why3_vc lsl_zero by simp
why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
......@@ -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)
......@@ -924,7 +950,7 @@ 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_zero by simp
why3_vc Of_int_zeros by simp
why3_vc Of_int_ones by (simp add: max_word_eq)
......@@ -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
......
theory Why3_BV
imports Why3_Int "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison"
begin
abbreviation (input) pow2 :: "int \<Rightarrow> int"
where "pow2 i \<equiv> 2 ^ nat i"
why3_open "bv/Pow2int.xml"
constants
pow2=pow2
why3_vc Power_0 by simp
why3_vc Power_s using assms by (simp add: Power_s)
why3_vc Power_1 by simp
why3_vc Power_sum using assms by (simp add: Power_sum)
why3_vc pow2pos using assms by simp
why3_vc pow2_0 by simp
why3_vc pow2_1 by simp
why3_vc pow2_2 by simp
why3_vc pow2_3 by simp
why3_vc pow2_4 by simp
why3_vc pow2_5 by simp
why3_vc pow2_6 by simp
why3_vc pow2_7 by simp
why3_vc pow2_8 by simp
why3_vc pow2_9 by simp
why3_vc pow2_10 by simp
why3_vc pow2_11 by simp
why3_vc pow2_12 by simp
why3_vc pow2_13 by simp
why3_vc pow2_14 by simp
why3_vc pow2_15 by simp
why3_vc pow2_16 by simp
why3_vc pow2_17 by simp
why3_vc pow2_18 by simp
why3_vc pow2_19 by simp
why3_vc pow2_20 by simp
why3_vc pow2_21 by simp
why3_vc pow2_22 by simp
why3_vc pow2_23 by simp
why3_vc pow2_24 by simp
why3_vc pow2_25 by simp
why3_vc pow2_26 by simp
why3_vc pow2_27 by simp
why3_vc pow2_28 by simp
why3_vc pow2_29 by simp
why3_vc pow2_30 by simp
why3_vc pow2_31 by simp
why3_vc pow2_32 by simp
why3_vc pow2_33 by simp
why3_vc pow2_34 by simp
why3_vc pow2_35 by simp
why3_vc pow2_36 by simp
why3_vc pow2_37 by simp
why3_vc pow2_38 by simp
why3_vc pow2_39 by simp
why3_vc pow2_40 by simp
why3_vc pow2_41 by simp
why3_vc pow2_42 by simp
why3_vc pow2_43 by simp
why3_vc pow2_44 by simp
why3_vc pow2_45 by simp
why3_vc pow2_46 by simp
why3_vc pow2_47 by simp
why3_vc pow2_48 by simp
why3_vc pow2_49 by simp
why3_vc pow2_50 by simp
why3_vc pow2_51 by simp
why3_vc pow2_52 by simp
why3_vc pow2_53 by simp
why3_vc pow2_54 by simp
why3_vc pow2_55 by simp
why3_vc pow2_56 by simp
why3_vc pow2_57 by simp
why3_vc pow2_58 by simp
why3_vc pow2_59 by simp
why3_vc pow2_60 by simp
why3_vc pow2_61 by simp
why3_vc pow2_62 by simp
why3_vc pow2_63 by simp
why3_vc pow2_64 by simp
why3_end
lemma rotate1_nth:
assumes "0 < length xs"
shows "rotate1 xs ! (i mod length xs) = xs ! (Suc i mod length xs)"
proof (cases xs)
case Nil
with `0 < length xs` show ?thesis by simp
next
case (Cons y ys)
with mod_less_divisor [of "Suc (length ys)" i]
show ?thesis
by (auto simp add: nth_append mod_Suc simp del: mod_less_divisor)
qed
lemma rotl_nth:
"word_rotl j w !! ((i + j) mod len_of TYPE('a)) = (w::'a::len word) !! (i mod len_of TYPE('a))"
proof (induct j arbitrary: w i)
case 0
show ?case by simp
next
case (Suc n)
from Suc [of "of_bl (rotate1 (to_bl w))" "Suc i"]
rotate1_nth [of "to_bl w" "len_of TYPE('a) - Suc (Suc i mod len_of TYPE('a))"]
show ?case
by (simp add: word_rotl_def rotate1_rotate_swap word_bl.Abs_inverse
rev_nth test_bit_bl word_size Suc_diff_Suc)
(simp add: mod_Suc)
qed
lemma rotater1_rotater_swap: "rotater1 (rotater n xs) = rotater n (rotater1 xs)"
by (simp add: rotater_def funpow_swap1)
lemma length_rotater1 [simp]: "length (rotater1 xs) = length xs"
by (simp add: rotater1_def split add: list.split)
lemma rotater1_nth:
assumes "0 < length xs"
shows "rotater1 xs ! (Suc i mod length xs) = xs ! (i mod length xs)"
proof (cases xs rule: rev_cases)
case Nil
with `0 < length xs` show ?thesis by simp
next
case (snoc ys y)
with mod_less_divisor [of "Suc (length ys)" i]
show ?thesis
by (auto simp add: rotate1_rl' nth_append mod_Suc simp del: mod_less_divisor)
qed
lemma rotr_nth:
"word_rotr j w !! (i mod len_of TYPE('a)) = (w::'a::len word) !! ((i + j) mod len_of TYPE('a))"
proof (induct j arbitrary: w)
case 0
show ?case by simp
next
case (Suc n)
from Suc [of "of_bl (rotater1 (to_bl w))"]
rotater1_nth [of "to_bl w" "len_of TYPE('a) - Suc (Suc (i + n) mod len_of TYPE('a))", symmetric]
show ?case
by (simp add: word_rotr_def rotater1_rotater_swap word_bl.Abs_inverse
rev_nth test_bit_bl word_size Suc_diff_Suc)
(simp add: mod_Suc)
qed
lemma uint_pow: "uint ((b::'a::len word) ^ n) = uint b ^ n mod 2 ^ len_of TYPE('a)"
by (induct n) (simp_all add: mod_pos_pos_trivial uint_word_ariths pull_mods)
lemma eq_sub_equiv_aux:
"(\<forall>j. uint i \<le> j \<and> j < uint i + uint n \<longrightarrow>
(0 \<le> j \<and> a !! nat j) = (0 \<le> j \<and> b !! nat j)) =
(b AND (mask (unat n) << unat i) = a AND (mask (unat n) << unat i))"
apply (simp add: word_eq_iff word_ops_nth_size word_size nth_shiftl)
apply (rule iffI)
apply (rule allI)
apply (drule_tac x="int na" in spec)
apply (auto simp add: uint_nat)[1]
apply (rule allI)
apply (drule_tac x="nat j" in spec)
apply (auto simp add: uint_nat test_bit_bin)
done
lemma int_minus_mod: "((i::int) - j) mod n = (i + (n - j mod n)) mod n"
proof -
have "(i + (n - j mod n)) mod n = (i mod n + (n - j mod n) mod n) mod n"
by (simp only: pull_mods(1))
also have "(n - j mod n) mod n = (n mod n - j mod n) mod n"
by (simp add: pull_mods)
finally show ?thesis by (simp add: pull_mods)
qed
lemma nat_minus_mod:
assumes "0 < (n::nat)"
shows "((n - i mod n) + i) mod n = 0"
proof -
have "((n - i mod n) + i) mod n = (i + (n - i mod n)) mod n"
by (simp add: add_ac)
also have "\<dots> = (i mod n + (n - i mod n)) mod n"
by (simp add: pull_mods)
also from assms have "\<dots> = (n mod n + (i mod n - i mod n)) mod n"
by (simp add: add_ac)
finally show ?thesis by simp
qed
lemma nat_minus_mod':
assumes "0 < (n::nat)"
shows "(i + (n - j mod n) + j) mod n = i mod n"
proof -
have "(i + (n - j mod n) + j) mod n = (i + ((n - j mod n) + j)) mod n"
by (simp add: add_ac)
also have "\<dots> = (i mod n + ((n - j mod n) + j) mod n) mod n"
by (simp add: pull_mods)
also note nat_minus_mod [OF assms]
finally show ?thesis by simp
qed