Commit 57ca6f0e authored by MARCHE Claude's avatar MARCHE Claude

Adapted to Isabelle2016-1. Contributed by Stefan Berghofer <berghofe@in.tum.de>

parent 609d9c20
......@@ -164,7 +164,12 @@ pvsbin/
/lib/isabelle/map/
/lib/isabelle/real/
/lib/isabelle/set/
/lib/isabelle/Why3_Bool.thy
/lib/isabelle/Why3_BV.thy
/lib/isabelle/Why3_Int.thy
/lib/isabelle/Why3_List.thy
/lib/isabelle/Why3_Number.thy
/lib/isabelle/Why3_Set.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
/lib/isabelle/bv
......
......@@ -1153,7 +1153,7 @@ clean::
ifeq (@enable_isabelle_libs@,yes)
ISABELLEVERSIONSPECIFIC=why3.ML Why3_BV.thy
ISABELLEVERSIONSPECIFIC=why3.ML Why3_Bool.thy Why3_BV.thy Why3_Int.thy Why3_List.thy Why3_Number.thy Why3_Set.thy
ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS))
......
......@@ -638,9 +638,9 @@ else
ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEDETECTEDVERSION in
2015*)
2016-1*)
enable_isabelle_support=yes
ISABELLEVERSION=2015
ISABELLEVERSION=2016-1
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
2016*)
......@@ -651,8 +651,8 @@ else
*)
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle 2015 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2015)"
AC_MSG_WARN(You need Isabelle 2016 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2016)"
;;
esac
fi
......
......@@ -11,9 +11,9 @@ using ``Edit'' action in \texttt{why3 ide}.
\subsection{Installation}
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.
You need version Isabelle2016 or Isabelle2016-1. Former versions are not
supported. We assume below that your version is 2016-1, please replace
2016-1 by 2016 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/Isabelle2016/etc/components
.isabelle/Isabelle2016-1/etc/components
\end{verbatim}
or the system-wide file
\begin{verbatim}
......
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 number.Prime
syntax predicate prime "<app><const name=\"Factorial_Ring.normalization_semidom_class.prime\"/>%1</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>"
theory number.Prime
syntax predicate prime "<app><const name=\"Primes.prime\"/><app><const name=\"Int.nat\"/>%1</app></app>"
end
......@@ -163,14 +163,15 @@ theory number.Gcd
syntax function gcd "<app><const name=\"GCD.gcd_class.gcd\"/>%1%2</app>"
end
theory number.Prime
syntax predicate prime "<app><const name=\"Primes.prime\"/><app><const name=\"Int.nat\"/>%1</app></app>"
end
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=\"Rings.divide_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-2015.gen"
import "isabelle-2016-1.gen"
......@@ -8,7 +8,7 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2015.gen"
import "isabelle-2016-1.gen"
transformation "simplify_trivial_quantification_in_goal"
......@@ -70,16 +70,28 @@ shift $(($OPTIND - 1))
NAME=`dirname "$1"`/`basename "$1" .xml`
if [ "$ISABELLE_WHY3_SESSION" ]; then
SESSION="$ISABELLE_WHY3_SESSION"
else
SESSION=Why3
fi
if [ "$ISABELLE_WHY3_SESSION_DIR" ]; then
SESSION_DIR=("-d" "$ISABELLE_WHY3_SESSION_DIR")
else
SESSION_DIR=()
fi
if [ "$BATCH" = true ]; then
"$ISABELLE_PROCESS" -e "use_thy \"$NAME\";" -rq Why3
echo "use_thy \"$NAME\";" | "$ISABELLE_TOOL" console "${SESSION_DIR[@]}" -l "$SESSION"
elif [ "$INTERACTIVE" = true ]; then
make_theory "$NAME"
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")"
"$ISABELLE_TOOL" java -jar "$(platform_path "$JEDIT_HOME/dist/jedit.jar")" \
"-settings=$(platform_path "$JEDIT_SETTINGS")" "-server=$WHY3_JEDIT_SERVER" \
-reuseview -wait "$(platform_path "${NAME}.thy")"
else
"$ISABELLE_TOOL" jedit -l Why3 "${NAME}.thy"
"$ISABELLE_TOOL" jedit "${SESSION_DIR[@]}" -l "$SESSION" "${NAME}.thy"
fi
else
usage
......
......@@ -26,12 +26,30 @@ function fail()
## main
[ "$1" = "-?" ] && usage
SESSION=Why3
SESSION_DIR=()
while getopts "l:d:" OPT
do
case "$OPT" in
l)
SESSION="$OPTARG"
;;
d)
SESSION_DIR=("-d" "$OPTARG")
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
SERVER_FILE="$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER"
if [ -f "$SERVER_FILE" ]; then
fail "Server already running: \"$SERVER_FILE\""
else
exec "$ISABELLE_TOOL" jedit "-j-server=$WHY3_JEDIT_SERVER" -l Why3 "$@"
exec "$ISABELLE_TOOL" jedit "-j-server=$WHY3_JEDIT_SERVER" "${SESSION_DIR[@]}" -l "$SESSION" "$@"
fi
......@@ -120,7 +120,7 @@ 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)
by (simp add: rotater1_def split: list.split)
lemma rotater1_nth:
assumes "0 < length xs"
......@@ -258,8 +258,8 @@ why3_open "bv/BV8.xml"
sub=minus
neg=uminus
mul=times
udiv=div
urem=mod
udiv=divide
urem=modulo
lsr=lsr
asr=asr
lsl=lsl
......@@ -448,8 +448,8 @@ why3_open "bv/BV16.xml"
sub=minus
neg=uminus
mul=times
udiv=div
urem=mod
udiv=divide
urem=modulo
lsr=lsr
asr=asr
lsl=lsl
......@@ -638,8 +638,8 @@ why3_open "bv/BV32.xml"
sub=minus
neg=uminus
mul=times
udiv=div
urem=mod
udiv=divide
urem=modulo
lsr=lsr
asr=asr
lsl=lsl
......@@ -828,8 +828,8 @@ why3_open "bv/BV64.xml"
sub=minus
neg=uminus
mul=times
udiv=div
urem=mod
udiv=divide
urem=modulo
lsr=lsr
asr=asr
lsl=lsl
......
theory Why3_Bool
imports Why3_Setup
begin
section {* Basic theory of Booleans *}
why3_open "bool/Bool.xml"
why3_vc andb_def by (simp split: bool.split)
why3_vc orb_def by (simp split: bool.split)
why3_vc xorb_def by (simp split: bool.split)
why3_vc notb_def by (simp split: bool.split)
why3_vc implb_def by (simp split: bool.split)
why3_end
end
theory Why3_Int
imports Why3_Setup
begin
section {* Integers and the basic operators *}
why3_open "int/Int.xml"
why3_vc Comm by simp
why3_vc Comm1 by simp
why3_vc Assoc by simp
why3_vc Assoc1 by simp
why3_vc Unitary by simp
why3_vc Inv_def_l by simp
why3_vc Inv_def_r by simp
why3_vc Unit_def_l by simp
why3_vc Unit_def_r by simp
why3_vc Mul_distr_l by (simp add: ring_distribs)
why3_vc Mul_distr_r by (simp add: ring_distribs)
why3_vc infix_mn_def by simp
why3_vc NonTrivialRing by simp
why3_vc infix_lseq_def by auto
why3_vc Refl by simp
why3_vc Trans using assms by simp
why3_vc Total by auto
why3_vc Antisymm using assms by simp
why3_vc ZeroLessOne by simp
why3_vc CompatOrderAdd using assms by simp
why3_vc CompatOrderMult using assms by (rule mult_right_mono)
why3_end
section {* Absolute Value *}
why3_open "int/Abs.xml"
why3_vc abs_def by simp
why3_vc Abs_le by auto
why3_vc Abs_pos by simp
why3_end
section {* Minimum and Maximum *}
why3_open "int/MinMax.xml"
why3_vc Max_l using assms by simp
why3_vc Max_comm by simp
why3_vc Max_assoc by simp
why3_vc Min_r using assms by simp
why3_vc Min_comm by simp
why3_vc Min_assoc by simp
why3_vc max_def by auto
why3_vc min_def by auto
why3_end
section {* Euclidean Division *}
definition ediv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "ediv" 70) where
"a ediv b = sgn b * (a div \<bar>b\<bar>)"
definition emod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "emod" 70) where
"a emod b = a mod \<bar>b\<bar>"
why3_open "int/EuclideanDivision.xml"
constants
div = ediv
mod = emod
why3_vc Div_1 by (simp add: ediv_def)
why3_vc Div_1_left using assms by (simp add: ediv_def div_pos_pos_trivial)
why3_vc Div_inf using assms by (simp add: ediv_def div_pos_pos_trivial)
why3_vc Div_inf_neg
using assms
by (cases "x = y") (simp_all add: ediv_def
zdiv_zminus1_eq_if div_pos_pos_trivial mod_pos_pos_trivial)
why3_vc Div_mod
by (simp add: ediv_def emod_def mult.assoc [symmetric] abs_sgn)
why3_vc Div_mult using assms by (simp add: ediv_def add.commute)
why3_vc Div_bound
proof -
from assms show ?C1
by (simp add: ediv_def pos_imp_zdiv_nonneg_iff)
show ?C2
proof (cases "x = 0")
case False
show ?thesis
proof (cases "y = 1")
case False
with assms `x \<noteq> 0` have "x div y < x"
by (simp add: int_div_less_self)
with assms show ?thesis by (simp add: ediv_def)
qed (simp add: ediv_def)
qed (simp add: ediv_def)
qed
why3_vc Div_minus1_left
using assms
by (simp only: zdiv_zminus1_eq_if ediv_def)
(simp add: div_pos_pos_trivial mod_pos_pos_trivial)
why3_vc Mod_0 by (simp add: emod_def)
why3_vc Mod_1 by (simp add: emod_def)
why3_vc Mod_1_left using assms by (simp add: emod_def mod_pos_pos_trivial)
why3_vc Mod_minus1_left
using assms
by (simp only: emod_def zmod_zminus1_eq_if) (simp add: mod_pos_pos_trivial)
why3_vc Mod_mult using assms by (simp add: emod_def add.commute)
why3_vc Mod_bound using assms by (simp_all add: emod_def)
why3_vc Div_unique using assms
proof -
have h0: "y \<noteq> 0" using assms by auto
have h1: "x = y * (x ediv y) + (x emod y)" using h0 Div_mod by blast
have h2: "0 \<le> x emod y \<and> x emod y < y" using assms H1 h0 Mod_bound zabs_def
by (metis abs_sgn monoid_mult_class.mult.right_neutral sgn_pos)
have h3: "x - y < y * (x ediv y)" using h1 h2 by linarith
have h4: "y * (x ediv y) \<le> x" using h1 h2 by linarith
show ?thesis
proof (cases "x ediv y > q")
assume a:"q < x ediv y"
have h5: "x ediv y \<ge> q + 1" using a by linarith
have h6: "y * (x ediv y) >= y * (q + 1)" by (metis H1 h5 le_less mult_left_mono)
have h7: "y * (x ediv y) >= q * y + y" by (metis Comm1 Mul_distr_l h6 monoid_mult_class.mult.right_neutral)
thus "x ediv y = q" using H3 h1 h2 h7 by linarith
next
assume a:"\<not> q < x ediv y"
show "x ediv y = q"
proof (cases "x ediv y < q")
assume b:"x ediv y < q"
have h5: "x ediv y \<le> q - 1" using b by linarith
have h6: "y * (x ediv y) <= y * (q - 1)" by (metis H1 h5 le_less mult_left_mono)
have h7: "y * (x ediv y) <= q * y - y" by (metis Comm1 h6 int_distrib(4) monoid_mult_class.mult.right_neutral)
thus "x ediv y = q" using H2 h3 h7 by linarith
next
assume b:"\<not> x ediv y < q"
show ?thesis using a b by linarith
qed
qed
qed
why3_end
section {* Computer Division *}
definition cdiv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "cdiv" 70) where
"a cdiv b = sgn a * sgn b * (\<bar>a\<bar> div \<bar>b\<bar>)"
definition cmod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "cmod" 70) where
"a cmod b = sgn a * (\<bar>a\<bar> mod \<bar>b\<bar>)"
why3_open "int/ComputerDivision.xml"
constants
div = cdiv
mod = cmod
why3_vc Div_1 by (simp add: cdiv_def mult_sgn_abs)
why3_vc Div_inf using assms by (simp add: cdiv_def div_pos_pos_trivial)
why3_vc Div_sign_neg
using assms
by (cases "x = 0") (simp_all add: cdiv_def
zdiv_zminus1_eq_if div_nonpos_pos_le0 pos_imp_zdiv_neg_iff)
why3_vc Div_sign_pos
using assms
by (cases "x = 0")
(simp_all add: cdiv_def pos_imp_zdiv_nonneg_iff)
why3_vc Div_mod
proof -
have "y * (sgn x * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>)) + sgn x * (\<bar>x\<bar> mod \<bar>y\<bar>) =
sgn x * (y * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>) + \<bar>x\<bar> mod \<bar>y\<bar>)"
by (simp add: ring_distribs)
then show ?thesis
by (cases "x = 0") (simp_all add: cdiv_def cmod_def abs_sgn
sgn_mult [symmetric] order.strict_iff_order)
qed
why3_vc Div_mult
proof (cases "y = 0")
case False
with assms show ?thesis
by (cases "z = 0")
(simp_all add: cdiv_def add.commute add_pos_pos)
qed simp
why3_vc Div_bound
proof -
from assms show ?C1
by (simp add: cdiv_def pos_imp_zdiv_nonneg_iff sgn_if)
show ?C2
proof (cases "x = 0")
case False
show ?thesis
proof (cases "y = 1")
case False
with assms `x \<noteq> 0` have "x div y < x"
by (simp add: int_div_less_self)
with assms show ?thesis by (simp add: cdiv_def sgn_if)
qed (simp add: cdiv_def sgn_if)
qed (simp add: cdiv_def)
qed
why3_vc Mod_1 by (simp add: cmod_def)
why3_vc Mod_inf using assms by (simp add: cmod_def mod_pos_pos_trivial sgn_if)
why3_vc Mod_mult
proof (cases "y = 0")
case False
with assms show ?thesis
by (cases "z = 0") (simp_all add: cmod_def add.commute add_pos_pos)
qed simp
why3_vc Mod_bound
proof -
from assms show ?C1
by (auto simp add: cmod_def sgn_if intro: less_le_trans [of _ 0])
from assms show ?C2
by (auto simp add: cmod_def sgn_if intro: le_less_trans [of _ 0])
qed
why3_vc Mod_sign_neg using assms by (simp add: cmod_def sgn_if)
why3_vc Mod_sign_pos using assms by (simp add: cmod_def sgn_if)
why3_vc Rounds_toward_zero
proof (cases "x = 0")
case False
then have "\<bar>sgn x\<bar> = 1" by (simp add: sgn_if)
have "sgn x * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>) * y =
sgn x * (y * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>))" (is "?l = ?r")
by simp
then have "\<bar>?l\<bar> = \<bar>?r\<bar>" by (simp (no_asm_simp))
also note abs_sgn [symmetric]
also note abs_mult
also have "\<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>) \<le> \<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>) + \<bar>x\<bar> mod \<bar>y\<bar>"
by (rule add_increasing2) (simp_all add: assms)
with assms have "\<bar>\<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>)\<bar> \<le> \<bar>\<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>) + \<bar>x\<bar> mod \<bar>y\<bar>\<bar>"
by (simp add: pos_imp_zdiv_nonneg_iff)
finally show ?thesis using `\<bar>sgn x\<bar> = 1`
by (simp add: cdiv_def)
qed (simp add: cdiv_def)
why3_end
section {* Division by 2 *}
why3_open "int/Div2.xml"
why3_vc div2
by (rule exI [of _ "x div 2"]) auto
why3_end
section {* Power of an integer to an integer *}
why3_open "int/Power.xml"
why3_vc Power_0 by simp
why3_vc Power_1 by simp
why3_vc Power_s using assms by (simp add: nat_add_distrib)
why3_vc Power_s_alt using assms by (simp add: nat_diff_distrib power_Suc [symmetric])
why3_vc Power_sum using assms by (simp add: nat_add_distrib power_add)
why3_vc Power_mult using assms by (simp add: nat_mult_distrib power_mult)
why3_vc Power_mult2 by (simp add: power_mult_distrib)
why3_vc Power_non_neg using assms by simp
why3_vc Power_monotonic using assms by (simp add: power_increasing)
why3_end
end
theory Why3_List
imports Why3_Setup
begin
section {* Length of a list *}
why3_open "list/Length.xml"
why3_vc length_def by (cases l) simp_all
why3_vc Length_nil by simp
why3_vc Length_nonnegative by simp
why3_end
section {* Membership in a list *}
why3_open "list/Mem.xml"
why3_vc mem_def by (simp split: list.split)
why3_end
section {* Nth element of a list *}
why3_open "list/Nth.xml"
lemma nth_eq: "0 \<le> i \<Longrightarrow> nat i < length xs \<Longrightarrow> nth i xs = Some (xs ! nat i)"
by (induct xs arbitrary: i) (auto simp add: nat_diff_distrib)
why3_end
why3_open "list/NthNoOpt.xml"
why3_vc nth_cons_0 by simp
why3_vc nth_cons_n
using assms
by (simp add: nat_diff_distrib)
why3_end
why3_open "list/NthLength.xml"
why3_vc nth_none_1
using assms
by (induct l arbitrary: i) simp_all
why3_vc nth_none_2
using assms
by (induct l arbitrary: i) simp_all
why3_vc nth_none_3
using assms
proof (induct l arbitrary: i)
case Nil
then show ?case by simp arith
next
case (Cons x xs)
show ?case
proof (cases "i < 0")
case False
with Cons have "0 < i" by (simp split: if_split_asm)
with Cons have "Nth.nth (i - 1) xs = None" by simp
then have "i - 1 < 0 \<or> int (length xs) \<le> i - 1"
by (rule Cons)
with `0 < i` show ?thesis by auto
qed simp
qed
why3_end
section {* Head and tail *}
why3_open "list/HdTl.xml"
why3_end
why3_open "list/HdTlNoOpt.xml"
why3_vc hd_cons by simp
why3_vc tl_cons by simp
why3_end
section {* Relation between head, tail, and nth *}
why3_open "list/NthHdTl.xml"
why3_vc Nth_tl
using assms
by (simp add: tl_def split: list.split_asm)
why3_vc Nth0_head
by (simp add: hd_def split: list.split)
why3_end
section {* Appending two lists *}
why3_open "list/Append.xml"
why3_vc infix_plpl_def by (simp split: list.split)
why3_vc Append_assoc by simp
why3_vc Append_l_nil by simp
why3_vc Append_length by simp
why3_vc mem_append by simp
why3_vc mem_decomp
using assms
by (simp add: in_set_conv_decomp)
why3_end
why3_open "list/NthLengthAppend.xml"
why3_vc nth_append_1
proof (cases "0 \<le> i")
case True
with assms have "nat i < length l1" by simp
with True show ?thesis
by (simp add: nth_eq nth_append)
next
case False
then show ?thesis by (simp add: nth_none_1)
qed
why3_vc nth_append_2
proof (cases "nat i < length (l1 @ l2)")
case True
with assms show ?thesis
by (auto simp add: nth_eq nth_append nat_diff_distrib)
next
case False
with assms show ?thesis by (simp add: nth_none_2)
qed
why3_end
section {* Reversing a list *}
why3_open "list/Reverse.xml"
why3_vc reverse_def by (simp split: list.split)
why3_vc Reverse_length by simp