Commit a7f61d63 authored by MARCHE Claude's avatar MARCHE Claude

Merge remote-tracking branch 'berghofer/master'

parents ee99af04 6bd0a067
......@@ -94,6 +94,9 @@ why3.conf
/bin/why3webserver.opt
/bin/why3webserver.byte
/bin/why3webserver
/bin/isabelle_client.opt
/bin/isabelle_client.byte
/bin/isabelle_client
# /doc/
/doc/version.tex
......@@ -175,11 +178,8 @@ pvsbin/
/lib/isabelle/map/
/lib/isabelle/real/
/lib/isabelle/set/
/lib/isabelle/ROOT
/lib/isabelle/Why3_BV.thy
/lib/isabelle/Why3_Number.thy
/lib/isabelle/Why3_Real.thy
/lib/isabelle/Why3_Set.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
/lib/isabelle/bv
......
......@@ -1260,7 +1260,7 @@ clean::
#######################
ISABELLEVERSIONSPECIFIC=ROOT why3.ML Why3_BV.thy Why3_Number.thy Why3_Real.thy Why3_Set.thy
ISABELLEVERSIONSPECIFIC=why3.ML Why3_Number.thy Why3_Real.thy
ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS))
......@@ -1424,6 +1424,41 @@ install-data::
clean::
rm -f drivers/isabelle-realizations.aux
#######################
# Isabelle client
#######################
ISABELLEC_FILES := isabelle_client_main
ISABELLECMODULES := $(addprefix src/isabelle-client/, $(ISABELLEC_FILES))
ISABELLECDEP = $(addsuffix .dep, $(ISABELLECMODULES))
ISABELLECCMO = $(addsuffix .cmo, $(ISABELLECMODULES))
ISABELLECCMX = $(addsuffix .cmx, $(ISABELLECMODULES))
$(ISABELLECCMO) $(ISABELLECCMX): INCLUDES += -I src/isabelle-client -I src/util
$(ISABELLECDEP): DEPFLAGS += -I src/isabelle-client
depend: $(ISABELLECDEP)
CLEANDIRS += src/isabelle-client
# build targets
byte: bin/isabelle_client.byte
opt: bin/isabelle_client.opt
bin/isabelle_client.opt: lib/why3/why3.cmxa $(ISABELLECCMX)
bin/isabelle_client.byte: lib/why3/why3.cma $(ISABELLECCMO)
install_no_local::
cp -f bin/isabelle_client.@OCAMLBEST@ $(BINDIR)/isabelle_client$(EXE)
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(ISABELLECDEP)
endif
clean::
rm -f bin/isabelle_client.byte bin/isabelle_client.opt bin/isabelle_client
#######################
# Ocaml realizations
#######################
......
......@@ -744,7 +744,7 @@ fi
# Default version used for generation of realization in the case Isabelle is not
# detected or Why3 is compiled with disable-isabelle.
ISABELLEVERSION=2017
ISABELLEVERSION=2018
if test "$enable_isabelle_libs" = no; then
enable_isabelle_support=no
......@@ -760,9 +760,9 @@ else
ISABELLEDETECTEDVERSION=[`$ISABELLE version | sed -n -e 's|Isabelle\([^:]*\).*$|\1|p'`]
case $ISABELLEDETECTEDVERSION in
2016-1*)
2018*)
enable_isabelle_support=yes
ISABELLEVERSION=2016-1
ISABELLEVERSION=2018
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
2017*)
......@@ -773,8 +773,8 @@ else
*)
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle 2016-1 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2016-1)"
AC_MSG_WARN(You need Isabelle 2017 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2017)"
;;
esac
fi
......
......@@ -11,9 +11,9 @@ using ``Edit'' action in \texttt{why3 ide}.
\subsection{Installation}
You need version Isabelle2016-1 or Isabelle2017. Former versions are not
supported. We assume below that your version is 2017, please replace
2017 by 2016-1 otherwise.
You need version Isabelle2017 or Isabelle2018. Former versions are not
supported. We assume below that your version is 2018, please replace
2018 by 2017 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/Isabelle2017/etc/components
.isabelle/Isabelle2018/etc/components
\end{verbatim}
or the system-wide file
\begin{verbatim}
......
theory number.Coprime
syntax predicate coprime "<app><const name=\"GCD.gcd_class.coprime\"/>%1%2</app>"
end
theory number.Coprime
syntax predicate coprime "<app><const name=\"Rings.algebraic_semidom_class.coprime\"/>%1%2</app>"
end
......@@ -160,10 +160,6 @@ theory number.Prime
syntax predicate prime "<app><const name=\"Factorial_Ring.normalization_semidom_class.prime\"/>%1</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>"
......
......@@ -7,3 +7,4 @@ filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2017.gen"
......@@ -8,6 +8,7 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2017.gen"
transformation "simplify_trivial_quantification_in_goal"
......@@ -7,3 +7,4 @@ filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2018.gen"
......@@ -8,6 +8,7 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2018.gen"
transformation "simplify_trivial_quantification_in_goal"
theory genealogy_Genealogy_Child_is_son_or_daughter_1
imports Why3
imports Why3.Why3
begin
why3_open "genealogy_Genealogy_Child_is_son_or_daughter_1.xml"
......
theory genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1
imports Why3
imports Why3.Why3
begin
why3_open "genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"
......
theory genealogy_Genealogy_Sibling_is_brother_or_sister_1
imports Why3
imports Why3.Why3
begin
why3_open "genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"
......
theory genealogy_Genealogy_Sibling_sym_1
imports Why3
imports Why3.Why3
begin
why3_open "genealogy_Genealogy_Sibling_sym_1.xml"
......
......@@ -32,7 +32,7 @@
<prover id="27" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="28" name="Z3" version="4.4.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="29" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="30" name="Isabelle" version="2016-1" timelimit="100" steplimit="1" memlimit="1000"/>
<prover id="30" name="Isabelle" version="2018" timelimit="100" steplimit="1" memlimit="4000"/>
<prover id="31" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="32" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="33" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
......
chapter Why3
session Why3 = "HOL-Word" +
options [document = false]
theories Why3
#!/usr/bin/env bash
#
# DESCRIPTION: Use Isabelle server when executing command
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] COMMAND"
echo
echo " Options are:"
echo " -d include session directory"
echo " -i include session"
echo " -s name of session (default Why3)"
echo
echo "Use Isabelle server when executing COMMAND."
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## main
SESSION_DIRS=()
INCLUDE_SESSIONS=()
SESSION=Why3
while getopts "d:i:s:" OPT
do
case "$OPT" in
s)
SESSION="$OPTARG"
;;
d)
SESSION_DIRS+=("-d" "$OPTARG")
;;
i)
INCLUDE_SESSIONS+=("-i" "$OPTARG")
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
SERVER=$("$ISABELLE_TOOL" server -s)
if [ $? -ne 0 ]
then
exit 2
fi
TMP1=${SERVER##[^=]*= }
ISABELLE_ADDRESS=${TMP1%%:[^:]*}
TMP2=${TMP1##[^:]*:}
ISABELLE_PORT=${TMP2%% [^ ]*}
TMP3=${TMP2##[^ ]* (password \"}
ISABELLE_PASSWORD=${TMP3%%\"[^\"]*}
export ISABELLE_ADDRESS
export ISABELLE_PORT
export ISABELLE_PASSWORD
ISABELLE_SESSION_ID=$(isabelle_client "${SESSION_DIRS[@]}" "${INCLUDE_SESSIONS[@]}" -s "${SESSION}")
if [ $? -ne 0 ]
then
fail "$ISABELLE_SESSION_ID"
fi
export ISABELLE_SESSION_ID
"$@"
RET1=$?
isabelle_client -x
RET2=$?
if [ $RET1 -ne 0 ]
then
exit $RET1
else
exit $RET2
fi
......@@ -34,7 +34,7 @@ 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"
echo -e "theory $BNAME\nimports Why3.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' \
......@@ -83,7 +83,11 @@ else
fi
if [ "$BATCH" = true ]; then
"$ISABELLE_TOOL" process "${SESSION_DIR[@]}" -l "$SESSION" -T "$NAME"
if [ "$ISABELLE_ADDRESS" ]; then
isabelle_client -t "$NAME"
else
"$ISABELLE_TOOL" process "${SESSION_DIR[@]}" -l "$SESSION" -T "$NAME"
fi
elif [ "$INTERACTIVE" = true ]; then
make_theory "$NAME"
if [ -f "$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER" ]; then
......
This diff is collapsed.
......@@ -32,7 +32,7 @@ lemma nth_eq: "0 \<le> i \<Longrightarrow> nat i < length xs \<Longrightarrow> n
by (induct xs arbitrary: i) (auto simp add: nat_diff_distrib)
why3_vc is_none_spec
by (simp add: is_none_def option.disc_eq_case(1))
by (simp add: is_none_def split: option.split)
why3_end
......@@ -77,7 +77,7 @@ next
qed
why3_vc is_none_spec
by (simp add: NthLength.is_none_def option.disc_eq_case(1))
by (simp add: is_none_def split: option.split)
why3_end
......@@ -87,7 +87,7 @@ section {* Head and tail *}
why3_open "list/HdTl.xml"
why3_vc is_none_spec
by (simp add: HdTl.is_none_def option.disc_eq_case(1))
by (simp add: is_none_def split: option.split)
why3_end
......@@ -113,7 +113,7 @@ why3_vc Nth0_head
by (simp add: hd_def split: list.split)
why3_vc is_none_spec
by (simp add: NthHdTl.is_none_def option.disc_eq_case(1))
by (simp add: is_none_def split: option.split)
why3_end
......@@ -163,7 +163,7 @@ next
qed
why3_vc is_none_spec
by (simp add: NthLengthAppend.is_none_def option.disc_eq_case(1))
by (simp add: is_none_def split: option.split)
why3_end
......
......@@ -91,30 +91,14 @@ proof -
then show ?thesis by (simp add: occ_def)
qed
(* We use occ_append to decompose into {l..<i} {i} {i+1..<j} {j} {j+1..<u} and this complete the
proof
*)
lemma occ_exchange2:
assumes "l \<le> i \<and> i < u \<and> l \<le> j \<and> j < u \<and> i < j"
shows "occ z (m(i := x, j := y)) l u = occ z (m(i := y, j := x)) l u"
proof -
from assms have h1:
"occ z (m (i := x, j := y)) l i + occ z (m (i := x, j := y)) i (i+1) + occ z (m (i := x, j := y)) (i+1) j +
occ z (m (i := x, j := y)) j (j+1) + occ z (m (i := x, j := y)) (j+1) u =
occ z (m (i := x, j := y)) l u"
by (smt occ_append)
from assms have h2:
"occ z (m (i := y, j := x)) l i + occ z (m (i := y, j := x)) i (i+1) + occ z (m (i := y, j := x)) (i+1) j +
occ z (m (i := y, j := x)) j (j+1) + occ z (m (i := y, j := x)) (j+1) u =
occ z (m (i := y, j := x)) l u"
by (smt occ_append)
show ?thesis
by (smt h1 h2 assms facts.set_def occ_bounds(1) occ_eq occ_exists occ_right_add)
qed
lemma vimage_update:
"m(i := x) -` {z} = (if x = z then m -` {z} \<union> {i} else m -` {z} - {i})"
by auto
why3_vc occ_exchange
using assms
by (smt fun_upd_twist occ_exchange2)
by (simp add: occ_def vimage_update insert_Diff_if card_insert)
(auto simp add: Diff_Int_distrib2 card_Diff_subset_Int)
why3_vc occ_left_add
proof -
......
......@@ -30,10 +30,9 @@ why3_vc even_2k by simp
why3_vc odd_2k1 by simp
why3_vc even_mod2
apply (simp add: even_def cmod_def)
by (metis abs_mult abs_mult_sgn abs_numeral mult.assoc mult_zero_right zmod_eq_0_iff)
why3_vc even_mod2
by (auto simp add: even_def cmod_def sgn_if minus_equation_iff [of n])
why3_end
......@@ -42,7 +41,7 @@ section {* Divisibility *}
why3_open "number/Divisibility.xml"
why3_vc divides_def
by (metis ComputerDivision.facts.Div_mod abs_mult add.right_neutral cmod_def dvd_0_left_iff dvd_def mult_zero_right zmod_eq_0_iff)
by (auto simp add: cmod_def sgn_if minus_equation_iff [of n])
why3_vc divides_refl by simp
......@@ -108,7 +107,7 @@ why3_vc even_divides ..
why3_vc odd_divides ..
why3_vc divides_spec
by (metis divides_factorl dvd_div_mult_self)
by (simp add: dvd_def mult.commute)
why3_end
......
theory Why3_Number
imports
Why3_Int
"~~/src/HOL/Number_Theory/Primes"
"HOL-Computational_Algebra.Primes"
begin
section {* Parity properties *}
......@@ -31,8 +31,7 @@ why3_vc even_2k by simp
why3_vc odd_2k1 by simp
why3_vc even_mod2
apply (simp add: even_def cmod_def)
by (metis abs_mult abs_mult_sgn abs_numeral mult.assoc mult_zero_right zmod_eq_0_iff)
by (auto simp add: even_def cmod_def sgn_if minus_equation_iff [of n])
why3_end
......@@ -42,7 +41,7 @@ section {* Divisibility *}
why3_open "number/Divisibility.xml"
why3_vc divides_def
by (metis ComputerDivision.facts.Div_mod abs_mult add.right_neutral cmod_def dvd_0_left_iff dvd_def mult_zero_right zmod_eq_0_iff)
by (auto simp add: cmod_def sgn_if minus_equation_iff [of n])
why3_vc divides_refl by simp
......@@ -108,7 +107,7 @@ why3_vc even_divides ..
why3_vc odd_divides ..
why3_vc divides_spec
by (metis divides_factorl dvd_div_mult_self)
by (simp add: dvd_def mult.commute)
why3_end
......@@ -140,17 +139,17 @@ why3_vc gcd_opp by simp
why3_vc gcd_euclid
using gcd_add_mult [of a "- q" b]
by (simp add: sign_simps)
by (simp add: algebra_simps)
why3_vc Gcd_computer_mod
using assms gcd_add_mult [of b "- 1" "a mod b"]
by (simp add: cmod_def zabs_def gcd_red_int [symmetric] sgn_if sign_simps del: gcd_mod2)
(simp add: zmod_zminus2_eq_if gcd_red_int [of a b] del: gcd_mod2)
by (simp add: cmod_def zabs_def gcd_red_int [symmetric] sgn_if algebra_simps del: gcd_mod_right)
(simp add: zmod_zminus2_eq_if gcd_red_int [of a b] del: gcd_mod_right)
why3_vc Gcd_euclidean_mod
using assms gcd_add_mult [of b "- 1" "a mod b"]
by (simp add: emod_def zabs_def gcd_red_int [symmetric] sign_simps del: gcd_mod2)
(simp add: zmod_zminus2_eq_if gcd_red_int [of a b] del: gcd_mod2)
by (simp add: emod_def zabs_def gcd_red_int [symmetric] algebra_simps del: gcd_mod_right)
(simp add: zmod_zminus2_eq_if gcd_red_int [of a b] del: gcd_mod_right)
why3_vc gcd_mult using assms
by (simp add: gcd_mult_distrib_int [symmetric])
......@@ -224,12 +223,12 @@ 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)
by (simp_all add: nat_dvd_iff)
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 (int d)" "int d * int d \<le> p" "int d dvd p"
by (auto simp add: int_dvd_iff le_nat_iff)
by (auto simp add: int_dvd_int_iff [symmetric] le_nat_iff)
from `prime (int d)` have "2 \<le> int d" by (simp add: prime_ge_2_int)
then have "2 \<le> int d" by simp
with `2 \<le> int d` have "2 * 2 \<le> int d * int d"
......@@ -261,7 +260,7 @@ section {* Coprime numbers *}
why3_open "number/Coprime.xml"
why3_vc coprime_def ..
why3_vc coprime_def by (rule coprime_iff_gcd_eq_1)
why3_vc prime_coprime
proof -
......@@ -287,7 +286,7 @@ proof -
qed
}
then show "coprime n p"
by (auto simp add: coprime_int)
by (auto simp add: coprime_iff_gcd_eq_1)
qed
next
assume H: "\<forall>n. 1 \<le> n \<and> n < p \<longrightarrow> coprime n p"
......@@ -297,7 +296,7 @@ proof -
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)
with H' show False by (simp add: coprime_iff_gcd_eq_1)
qed
qed
then show ?thesis by (simp add: prime_def)
......@@ -307,7 +306,7 @@ 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)
then show ?thesis by (simp add: coprime_dvd_mult_left_iff)
qed
why3_vc Euclid
......@@ -317,8 +316,8 @@ why3_vc Euclid
why3_vc gcd_coprime
proof -
have "gcd a (b * c) = gcd (b * c) a" by (simp add: gcd.commute)
also from assms have "coprime b a" by (simp add: gcd.commute)
then have "gcd (b * c) a = gcd c a" by (simp add: gcd_mult_cancel)
also from assms have "coprime a b" by (simp add: gcd.commute coprime_iff_gcd_eq_1)
then have "gcd (b * c) a = gcd c a" by (simp add: gcd_mult_left_left_cancel)
finally show ?thesis by (simp add: gcd.commute)
qed
......
theory Why3_Real
imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation" Why3_Setup
imports
Why3_Setup
Complex_Main
"HOL-Decision_Procs.Approximation"
begin
section {* Real numbers and the basic unary and binary operators *}
......@@ -22,7 +25,7 @@ why3_vc Comm by simp
why3_vc Assoc1 by simp
why3_vc Mul_distr_l by (simp add: Fields.linordered_field_class.sign_simps)
why3_vc Mul_distr_l by (simp add: algebra_simps)
why3_vc Mul_distr_r by (simp add: Rings.comm_semiring_class.distrib)
......
......@@ -7,9 +7,6 @@ begin
section {* Potentially infinite sets *}
definition choose_elt :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
"choose_elt S = (\<some>x. S x)"
definition complement :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
"complement S v = Not (S v)"
......@@ -22,7 +19,7 @@ why3_open "set/Set.xml"
inter = inf
diff = minus
complement = complement
choose = choose_elt
choose = Eps
all = top
why3_vc add_spec by (auto simp add: mem_def)
......@@ -49,7 +46,8 @@ why3_vc union_spec
by (simp add: mem_def)
why3_vc choose_spec
by (metis assms choose_elt_def mem_def set.Set.is_empty_def tfl_some)
using assms
by (auto simp add: mem_def is_empty_def intro: someI_ex)
why3_vc remove_spec
by (simp add: mem_def)
......@@ -61,7 +59,8 @@ why3_vc subset_refl
by (simp add: subset_def)
why3_vc subset_trans
by (meson H1 H2 subset_def)
using assms
by (simp add: subset_def)
why3_vc subset_remove
by (simp add: remove_spec subset_def)
......@@ -84,9 +83,6 @@ definition fremove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
definition fchoose :: "'a fset \<Rightarrow> 'a" where
"fchoose S = (\<some>x. x |\<in>| S)"
definition ext_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
"ext_eq S1 S2 = (S1 = S2)"
definition is_empty :: "'a fset \<Rightarrow> bool" where
"is_empty S = (S = fempty)"
......@@ -101,7 +97,7 @@ why3_open "set/Fset.xml"
diff = minus
choose = fchoose
all = top
infix_eqeq = ext_eq
infix_eqeq = HOL.eq
subset = fsubset_eq
is_empty = is_empty
types
......@@ -134,16 +130,16 @@ why3_vc subset_trans
why3_vc subset_remove by (auto simp add: fremove_def)
why3_vc subset_eq
using assms ext_eq_def fcard_seteq by fastforce
using assms fcard_seteq by fastforce
why3_vc subset_spec by auto
why3_vc infix_eqeq_spec
by (metis ext_eq_def fsubset_antisym subset_spec)
by (simp add: fset_eq_iff)
why3_vc extensionality
using assms
by (auto simp add: ext_eq_def)
by simp
why3_vc cardinal1
proof (cases s rule: fset_strong_cases)
......@@ -191,8 +187,7 @@ why3_vc diff_spec by simp
why3_vc choose_spec
using assms
using Why3_Set.is_empty_def
by (metis (full_types) ex_fin_conv fchoose_def someI_ex)
by (auto simp add: fchoose_def is_empty_def intro: someI_ex)
why3_vc is_empty_spec
by (simp add: Why3_Set.is_empty_def)
......
theory Why3_Set
imports Why3_Setup Why3_Map "~~/src/HOL/Library/FSet"
begin
section {* Potentially infinite sets *}
definition choose_elt :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
"choose_elt S = (\<some>x. S x)"
definition complement :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
"complement S v = Not (S v)"
why3_open "set/Set.xml"
constants
empty = bot
add = insert
remove = Set.remove
union = sup
inter = inf
diff = minus
complement = complement
choose = choose_elt
all = top
why3_vc add_spec by (auto simp add: mem_def)
why3_vc diff_def by simp
why3_vc diff_spec by (simp add: mem_def)
why3_vc inter_def by simp
why3_vc mem_empty by (simp add: const_def mem_def set.Set.is_empty_def)