Commit b3a0ad7b authored by Clément Fumex's avatar Clément Fumex
Browse files

Merge branch 'master' into bv_rea_clem

parents 9999d201 bdf7e149
......@@ -156,6 +156,9 @@ pvsbin/
/lib/isabelle/list/
/lib/isabelle/map/
/lib/isabelle/set/
/lib/isabelle/Tools/why3
/lib/isabelle/Why3_Number.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
# /src/driver/
......
* marks an incompatible change
provers
o support for Isabelle 2015 (released May 25, 2015)
Version 0.86.1, May 22, 2015
============================
......
......@@ -148,7 +148,7 @@ LIB_CORE = ident ty term pattern decl theory \
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection parse_cvc4_z3_model
LIB_MLW = ity expr dexpr
LIB_MLW = ity expr dexpr mdecl
LIB_PARSER = ptree glob parser typing lexer
......@@ -1108,6 +1108,21 @@ clean::
ifeq (@enable_isabelle_libs@,yes)
ISABELLEVERSIONSPECIFIC=why3.ML Tools/why3 Why3_Number.thy
ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS))
ISABELLEREALIZEDRV=drivers/isabelle@ISABELLEVERSION@-realize.drv
$(ISABELLEVERSIONSPECIFICTARGETS): $(ISABELLEVERSIONSPECIFICSOURCES)
for i in $(ISABELLEVERSIONSPECIFIC); do \
cp lib/isabelle/$$i.@ISABELLEVERSION@ lib/isabelle/$$i ; \
done
clean::
rm -f $(ISABELLEVERSIONSPECIFICTARGETS)
ISABELLELIBS_INT_FILES = Exponentiation Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELIBS_INT_FILES)))
......@@ -1157,7 +1172,10 @@ else
ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
endif
lib/isabelle/last_build: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
ifneq (@enable_local@,yes)
cp -r lib/isabelle "$(LIBDIR)/why3"
endif
@(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \
echo "Building the Why3 heap for Isabelle/HOL:"; \
isabelle build -bc Why3; \
......@@ -1169,7 +1187,6 @@ lib/isabelle/last_build: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS
fi)
install_no_local::
cp -r lib/isabelle "$(LIBDIR)/why3"
cp drivers/isabelle-realizations.aux "$(DATADIR)/why3/drivers/"
install_no_local:: lib/isabelle/last_build
......@@ -1179,44 +1196,44 @@ install_local:: lib/isabelle/last_build
update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/int.why
mkdir -p lib/isabelle/int
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
$(ISABELLELIBS_BOOL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/bool.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bool.why
mkdir -p lib/isabelle/bool
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
$(ISABELLELIBS_REAL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/real.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/real.why
mkdir -p lib/isabelle/real
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
$(ISABELLELIBS_NUMBER): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/number.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/number.why
mkdir -p lib/isabelle/number
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
$(ISABELLELIBS_SET): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/set.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/set.why
mkdir -p lib/isabelle/set
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
$(ISABELLELIBS_MAP): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/map.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/map.why
mkdir -p lib/isabelle/map
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
$(ISABELLELIBS_LIST): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/list.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/list.why
mkdir -p lib/isabelle/list
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
$(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/option.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/option.why
mkdir -p lib/isabelle/option
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
# do not update isabelle realizations systematically
# opt byte: update-isabelle
......
......@@ -615,18 +615,24 @@ else
reason_isabelle_support=" (isabelle not found)"
else
AC_MSG_CHECKING(Isabelle version)
ISABELLEVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEVERSION in
case $ISABELLEDETECTEDVERSION in
2014*)
enable_isabelle_support=yes
AC_MSG_RESULT($ISABELLEVERSION)
ISABELLEVERSION=2014
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
2015*)
enable_isabelle_support=yes
ISABELLEVERSION=2015
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
*)
AC_MSG_RESULT($ISABELLEVERSION)
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle2013-2; Isabelle discarded)
reason_isabelle_support=" (need version 2013-2)"
AC_MSG_WARN(You need Isabelle 2014 or 2015; Isabelle discarded)
reason_isabelle_support=" (need version >= 2014)"
;;
esac
fi
......@@ -864,7 +870,7 @@ if test "$enable_pvs_support" = yes ; then
fi
echo " Isabelle : $enable_isabelle_support$reason_isabelle_support"
if test "$enable_isabelle_support" = yes ; then
echo " Version : $ISABELLEVERSION"
echo " Version : $ISABELLEVERSION ($ISABELLEDETECTEDVERSION)"
echo " Realization support : $enable_isabelle_libs$reason_isabelle_libs"
fi
if test "$enable_local" = yes ; then
......
......@@ -11,7 +11,9 @@ using ``Edit'' action in \texttt{why3ide}.
\subsection{Installation}
You need version Isabelle2014. Former versions are not supported.
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.
Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path
......@@ -20,7 +22,7 @@ and installation of \why, you must manually add the path
\end{verbatim}
into either the user file
\begin{verbatim}
.isabelle/Isabelle2014/etc/components
.isabelle/Isabelle2015/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>"
end
......@@ -146,11 +146,6 @@ 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.even_odd_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.even_odd_class.odd\"/>%1</app>"
end
theory number.Divisibility
syntax predicate divides "<app><const name=\"Rings.dvd_class.dvd\"/>%1%2</app>"
end
......
......@@ -7,3 +7,4 @@ filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2014.gen"
......@@ -8,5 +8,7 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2014.gen"
transformation "simplify_trivial_quantification_in_goal"
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
printer "isabelle-realize"
filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2015.gen"
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
printer "isabelle"
filename "%f_%t_%g.xml"
transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2015.gen"
transformation "simplify_trivial_quantification_in_goal"
......@@ -45,7 +45,7 @@
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="unknown" time="0.01"/></proof>
<proof prover="13"><result status="valid" time="0.04"/></proof>
<proof prover="14" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="4.96"/></proof>
<proof prover="14" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="6.23"/></proof>
<proof prover="15"><result status="valid" time="0.02"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.01" steps="12"/></proof>
......@@ -72,7 +72,7 @@
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.00"/></proof>
<proof prover="13"><result status="timeout" time="5.23"/></proof>
<proof prover="14" edited="genealogy_Genealogy_Sibling_sym_1.xml"><result status="valid" time="4.85"/></proof>
<proof prover="14" edited="genealogy_Genealogy_Sibling_sym_1.xml"><result status="valid" time="6.09"/></proof>
<proof prover="15"><result status="valid" time="0.12"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.02" steps="5"/></proof>
......@@ -98,7 +98,7 @@
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="unknown" time="0.02"/></proof>
<proof prover="13"><result status="valid" time="0.03"/></proof>
<proof prover="14" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="5.03"/></proof>
<proof prover="14" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="6.19"/></proof>
<proof prover="15"><result status="valid" time="0.04"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.02" steps="9"/></proof>
......@@ -123,7 +123,7 @@
<proof prover="11"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.04"/></proof>
<proof prover="13"><result status="timeout" time="5.26"/></proof>
<proof prover="14" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="5.12"/></proof>
<proof prover="14" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="6.50"/></proof>
<proof prover="15"><result status="valid" time="0.07"/></proof>
<proof prover="16"><result status="valid" time="0.01"/></proof>
<proof prover="17"><result status="valid" time="0.02" steps="32"/></proof>
......
#!/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 interactive mode"
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
;;
\?)
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"
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
else
usage
fi
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 arith
why3_vc odd_def by arith
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 ..
why3_vc odd_divides ..
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