Commit f546ae8a authored by Stefan Berghofer's avatar Stefan Berghofer

Adapted to Isabelle2016

Isabelle2015 is still supported, but support for Isabelle2014 has been
discontinued.
parent 295c2913
......@@ -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
This diff is collapsed.
......@@ -232,7 +232,7 @@ proof (induct n rule: less_induct)
next
case False
with `1 < n` obtain k where "k dvd n" "k \<noteq> 1" "k \<noteq> n"
by (auto simp add: prime_nat_def)
by (auto simp add: Primes.prime_def)
with `1 < n` have "k \<le> n" by (simp add: dvd_imp_le)
with `k \<noteq> n` have "k < n" by simp
moreover from `k dvd n` `1 < n` have "k \<noteq> 0" by (rule_tac notI) simp
......@@ -263,7 +263,7 @@ proof
with `2 \<le> p` obtain d
where d: "prime d" "d * d \<le> p" "d dvd p"
by (auto simp add: int_dvd_iff le_nat_iff int_mult)
from `prime d` have "2 \<le> d" by auto
from `prime d` have "2 \<le> d" by (simp add: prime_ge_2_nat)
then have "2 \<le> int d" by simp
with `2 \<le> int d` have "2 * 2 \<le> int d * int d"
by (rule mult_mono) simp_all
......@@ -275,14 +275,14 @@ qed
why3_vc even_prime
proof -
from `prime (nat p)` have "0 \<le> p" by (simp add: prime_def)
from `prime (nat p)` have "2 \<le> nat p" by auto
from `prime (nat p)` have "2 \<le> nat p" by (simp add: prime_ge_2_nat)
with `prime (nat p)` `even p` `0 \<le> p` show ?thesis
by (auto simp add: order_le_less prime_odd_nat even_nat_iff [symmetric])
qed
why3_vc odd_prime
proof -
from `prime (nat p)` have "2 \<le> nat p" by auto
from `prime (nat p)` have "2 \<le> nat p" by (simp add: prime_ge_2_nat)
with `prime (nat p)` `3 \<le> p` show ?thesis
by (auto simp add: order_le_less prime_odd_nat even_nat_iff [symmetric])
qed
......
theory Why3_Number
imports
Why3_Int
"~~/src/HOL/Number_Theory/Primes"
begin
section {* Parity properties *}
why3_open "number/Parity.xml"
why3_vc even_def by (simp add: even_equiv_def)
why3_vc odd_def by (simp add: odd_equiv_def)
why3_vc even_or_odd by auto
why3_vc even_not_odd using assms by simp
why3_vc odd_not_even using assms by simp
why3_vc even_odd using assms by simp
why3_vc odd_even using assms by simp
why3_vc even_even using assms by simp
why3_vc odd_odd using assms by simp
why3_vc even_2k by simp
why3_vc odd_2k1 by simp
why3_end
section {* Divisibility *}
why3_open "number/Divisibility.xml"
why3_vc divides_def by (simp add: dvd_def mult.commute)
why3_vc divides_refl by simp
why3_vc divides_1_n by simp
why3_vc divides_0 by simp
why3_vc divides_left using assms by simp
why3_vc divides_right using assms by simp
why3_vc divides_oppr using assms by simp
why3_vc divides_oppl using assms by simp
why3_vc divides_oppr_rev using assms by simp
why3_vc divides_oppl_rev using assms by simp
why3_vc divides_plusr using assms by simp
why3_vc divides_minusr using assms by simp
why3_vc divides_multl using assms by simp
why3_vc divides_multr using assms by simp
why3_vc divides_factorl by simp
why3_vc divides_factorr by simp
why3_vc divides_n_1 using assms by auto
why3_vc divides_antisym
using assms
by (auto dest: zdvd_antisym_abs)
why3_vc divides_trans using assms by (rule dvd_trans)
why3_vc divides_bounds using assms by (simp add: dvd_imp_le_int)
why3_vc mod_divides_euclidean
using assms
by (auto simp add: emod_def split add: split_if_asm)
why3_vc divides_mod_euclidean
using assms
by (simp add: emod_def dvd_eq_mod_eq_0 zabs_def zmod_zminus2_eq_if)
why3_vc mod_divides_computer
using assms
by (auto simp add: cmod_def zabs_def sgn_0_0 zmod_zminus1_eq_if
not_sym [OF less_imp_neq [OF pos_mod_bound]]
split add: split_if_asm)
why3_vc divides_mod_computer
using assms
by (simp add: cmod_def dvd_eq_mod_eq_0 zabs_def
zmod_zminus1_eq_if zmod_zminus2_eq_if)
why3_vc even_divides by (rule even_iff_2_dvd)
why3_vc odd_divides by (simp add: even_iff_2_dvd)
why3_end
section {* Greatest Common Divisor *}
why3_open "number/Gcd.xml"
why3_vc gcd_nonneg by simp
why3_vc gcd_def1 by simp
why3_vc gcd_def2 by simp
why3_vc gcd_def3 using assms by (rule gcd_greatest_int)
why3_vc gcd_unique using assms
by (simp add: gcd_unique_int [symmetric])
why3_vc Comm by (rule gcd_commute_int)
why3_vc Assoc by (rule gcd_assoc_int)
why3_vc gcd_0_pos using assms by simp
why3_vc gcd_0_neg using assms by simp
why3_vc gcd_opp by simp
why3_vc gcd_euclid
using gcd_add_mult_int [of a "- q" b]
by (simp add: sign_simps)
why3_vc Gcd_computer_mod
using assms gcd_add_mult_int [of b "- 1" "a mod b"]
by (simp add: cmod_def zabs_def gcd_red_int [symmetric] sgn_if sign_simps)
(simp add: zmod_zminus2_eq_if gcd_red_int [of a b])
why3_vc Gcd_euclidean_mod
using assms gcd_add_mult_int [of b "- 1" "a mod b"]
by (simp add: emod_def zabs_def gcd_red_int [symmetric] sign_simps)
(simp add: zmod_zminus2_eq_if gcd_red_int [of a b])
why3_vc gcd_mult using assms
by (simp add: gcd_mult_distrib_int [symmetric])
why3_end
section {* Prime numbers *}
why3_open "number/Prime.xml"
why3_vc prime_def
unfolding prime_def
proof
assume "1 < nat p \<and> (\<forall>m. m dvd nat p \<longrightarrow> m = 1 \<or> m = nat p)"
then have "1 < p" and H: "\<And>m. m \<ge> 0 \<Longrightarrow> m dvd p \<Longrightarrow> m = 1 \<or> m = p"
by (auto simp add: dvd_int_iff)
show "2 \<le> p \<and> (\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p)"
proof
from `1 < p` show "2 \<le> p" by simp
show "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
proof (intro strip)
fix n
assume "1 < n \<and> n < p"
with H [of n] show "\<not> n dvd p" by auto
qed
qed
next
assume "2 \<le> p \<and> (\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p)"
then have "2 \<le> p" and H: "\<And>n. 1 < n \<Longrightarrow> n < nat p \<Longrightarrow> \<not> n dvd p"
by auto
show "1 < nat p \<and> (\<forall>m. m dvd nat p \<longrightarrow> m = 1 \<or> m = nat p)"
proof
from `2 \<le> p` show "1 < nat p" by simp
show "\<forall>m. m dvd nat p \<longrightarrow> m = 1 \<or> m = nat p"
proof (intro strip)
fix m
assume "m dvd nat p"
with `2 \<le> p` have "1 \<le> m" by (cases "m = 0") auto
show "m = 1 \<or> m = nat p"
proof (cases "m = 1")
case False
show ?thesis
proof (cases "m = nat p")
case False
from `2 \<le> p` `m dvd nat p` have "m \<le> nat p" by (simp add: dvd_imp_le)
with False `m \<noteq> 1` `1 \<le> m` `m dvd nat p` H show ?thesis by (simp add: int_dvd_iff)
qed simp
qed simp
qed
qed
qed
why3_vc not_prime_1 by simp
why3_vc prime_2 by simp
why3_vc prime_3 by simp
why3_vc prime_divisors
using assms
by (auto simp add: prime_int_altdef dest: spec [of _ "\<bar>d\<bar>"])
lemma small_divisors_aux:
"1 < (n::nat) \<Longrightarrow> n < p \<Longrightarrow> n dvd p \<Longrightarrow> \<exists>d. prime d \<and> d * d \<le> p \<and> d dvd p"
proof (induct n rule: less_induct)
case (less n)
then obtain m where "p = n * m" by (auto simp add: dvd_def)
show ?case
proof (cases "prime n")
case True
show ?thesis
proof (cases "n \<le> m")
case True
with `p = n * m` `prime n`
show ?thesis by auto
next
case False
then have "m < n" by simp
moreover from `n < p` `p = n * m` have "1 < m" by simp
moreover from `1 < n` `n < p` `p = n * m` have "m < p" by simp
moreover from `p = n * m` have "m dvd p" by simp
ultimately show ?thesis by (rule less)
qed
next
case False
with `1 < n` obtain k where "k dvd n" "k \<noteq> 1" "k \<noteq> n"
by (auto simp add: prime_nat_def)
with `1 < n` have "k \<le> n" by (simp add: dvd_imp_le)
with `k \<noteq> n` have "k < n" by simp
moreover from `k dvd n` `1 < n` have "k \<noteq> 0" by (rule_tac notI) simp
with `k \<noteq> 1` have "1 < k" by simp
moreover from `k < n` `n < p` have "k < p" by simp
moreover from `k dvd n` `n dvd p` have "k dvd p" by (rule dvd.order_trans)
ultimately show ?thesis by (rule less)
qed
qed
why3_vc small_divisors
unfolding prime_def
proof
show "2 \<le> p" by fact
show "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
proof (intro strip)
fix n
assume "1 < n \<and> n < p"
show "\<not> n dvd p"
proof
assume "n dvd p"
with `1 < n \<and> n < p`
have "1 < nat n" "nat n < nat p" "nat n dvd nat p"
by (simp_all add: transfer_nat_int_relations)
then have "\<exists>d. prime d \<and> d * d \<le> nat p \<and> d dvd (nat p)"
by (rule small_divisors_aux)
with `2 \<le> p` obtain d
where d: "prime d" "d * d \<le> p" "d dvd p"
by (auto simp add: int_dvd_iff le_nat_iff int_mult)
from `prime d` have "2 \<le> d" by auto
then have "2 \<le> int d" by simp
with `2 \<le> int d` have "2 * 2 \<le> int d * int d"
by (rule mult_mono) simp_all
with d assms `2 \<le> d` show False by auto
qed
qed
qed
why3_vc even_prime
proof -
from `prime (nat p)` have "0 \<le> p" by (simp add: prime_def)
from `prime (nat p)` have "2 \<le> nat p" by auto
with `prime (nat p)` `even p` `0 \<le> p` show ?thesis
by (auto simp add: order_le_less prime_odd_nat pos_int_even_equiv_nat_even)
qed
why3_vc odd_prime
proof -
from `prime (nat p)` have "2 \<le> nat p" by auto
with `prime (nat p)` `3 \<le> p` show ?thesis
by (auto simp add: order_le_less prime_odd_nat pos_int_even_equiv_nat_even)
qed
why3_end
section {* Coprime numbers *}
why3_open "number/Coprime.xml"
why3_vc coprime_def ..
why3_vc prime_coprime
proof -
have "(\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p) =
(\<forall>n. 1 \<le> n \<and> n < p \<longrightarrow> coprime n p)"
proof
assume H: "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
show "\<forall>n. 1 \<le> n \<and> n < p \<longrightarrow> coprime n p"
proof (intro strip)
fix n
assume H': "1 \<le> n \<and> n < p"
{
fix d
assume "0 \<le> d" "d dvd n" "d dvd p"
with H' have "d \<noteq> 0" by auto
have "d = 1"
proof (rule ccontr)
assume "d \<noteq> 1"
with `0 \<le> d` `d \<noteq> 0` have "1 < d" by simp
moreover from `d dvd p` H' have "d \<le> p" by (auto dest: zdvd_imp_le)
moreover from `d dvd n` H' have "d \<noteq> p" by (auto dest: zdvd_imp_le)
ultimately show False using `d dvd p` H by auto
qed
}
then show "coprime n p"
by (auto simp add: coprime_int)
qed
next
assume H: "\<forall>n. 1 \<le> n \<and> n < p \<longrightarrow> coprime n p"
show "\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p"
proof (intro strip notI)
fix n
assume H': "1 < n \<and> n < p" "n dvd p"
then have "1 \<le> n \<and> n < p" by simp
with H have "coprime n p" by simp
with H' show False by (simp add: coprime_int)
qed
qed
then show ?thesis by (simp add: prime_def)
qed
why3_vc Gauss
proof -
from assms
have "coprime a b" "a dvd c * b" by (simp_all add: mult.commute)
then show ?thesis by (rule coprime_dvd_mult_int)
qed
why3_vc Euclid
proof -
from `p dvd a * b` have "nat \<bar>p\<bar> dvd nat \<bar>a\<bar> * nat \<bar>b\<bar>"
by (simp add: dvd_int_iff abs_mult nat_mult_distrib)
moreover from `prime (nat p)` have "prime (nat \<bar>p\<bar>)"
by (simp add: prime_def)
ultimately show ?thesis by (simp add: dvd_int_iff)
qed
why3_vc gcd_coprime
proof -
have "gcd a (b * c) = gcd (b * c) a" by (simp add: gcd_commute_int)
also from assms have "coprime b a" by (simp add: gcd_commute_int)
then have "gcd (b * c) a = gcd c a" by (simp add: gcd_mult_cancel_int)
finally show ?thesis by (simp add: gcd_commute_int)
qed
why3_end
end
......@@ -181,9 +181,9 @@ subsection {* Rounding towards zero *}
why3_vc Real_of_truncate
using floor_correct [of x] ceiling_correct [of x]
by (simp_all add: truncate_def)
by (simp_all add: truncate_def del: of_int_floor_le le_of_int_ceiling)
why3_vc Truncate_int by (simp add:truncate_def)
why3_vc Truncate_int by (simp add: truncate_def)
why3_vc Truncate_up_neg
using assms ceiling_correct [of x]
......@@ -299,6 +299,9 @@ section {* Power of a real to a real exponent *}
section {* Trigonometric Functions *}
abbreviation (input)
"why3_divide \<equiv> divide"
why3_open "real/Trigonometry.xml"
constants
cos = cos
......
......@@ -527,26 +527,26 @@ name = "Isabelle"
exec = "isabelle"
version_switch = "version"