Adapt to both isabelle 2014 and 2015

Signed-off-by: Claude Marche <Claude.Marche@inria.fr>

.gitignore

@@ -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/

Makefile.in

@@ -1098,6 +1098,18 @@ 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
+
 ISABELLELIBS_INT_FILES = Exponentiation Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
 ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELIBS_INT_FILES)))
 
@@ -1147,7 +1159,7 @@ 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
@@ -1171,44 +1183,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

configure.in

@@ -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
+                ISABELLEVERSION=2014
+                AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
+                ;;
           2015*)
 	        enable_isabelle_support=yes
-                AC_MSG_RESULT($ISABELLEVERSION)
+                ISABELLEVERSION=2015
+                AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
                 ;;
           *)
-                AC_MSG_RESULT($ISABELLEVERSION)
+                AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
                 enable_isabelle_support=no
-	        AC_MSG_WARN(You need Isabelle2015; Isabelle discarded)
-                reason_isabelle_support=" (need version 2015)"
+	        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

drivers/isabelle-2014.gen

+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

drivers/isabelle-2015.gen

+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

drivers/isabelle-common.gen

@@ -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.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

drivers/isabelle-realize.drv → drivers/isabelle2014-realize.drv

@@ -7,3 +7,4 @@ filename "%t.xml"
 transformation "inline_trivial"
 
 import "isabelle-common.gen"
+import "isabelle-2014.gen"

drivers/isabelle.drv → drivers/isabelle2014.drv

@@ -8,5 +8,7 @@ transformation "inline_trivial"
 transformation "eliminate_builtin"
 
 import "isabelle-common.gen"
+import "isabelle-2014.gen"
+
 
 transformation "simplify_trivial_quantification_in_goal"

drivers/isabelle2015-realize.drv

+(* 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"

drivers/isabelle2015.drv

+(* 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"

lib/isabelle/Why3_Number.thy.2014

+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

lib/isabelle2014/ROOT

-chapter Why3
-
-session Why3 = HOL +
-  options [document = false]
-  theories Why3

lib/isabelle2014/Tools/why3_jedit

-#!/usr/bin/env bash
-#
-# DESCRIPTION: Isabelle/jEdit with Why3 session and server port
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [ARGS...]"
-  echo
-  echo "Start Isabelle/jEdit with Why3 session and server port, for quick invocation"
-  echo "via why3ide."
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## main
-
-[ "$1" = "-?" ] && usage
-
-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 "$@"
-fi

lib/isabelle2014/etc/settings

-# -*- shell-script -*- :mode=shellscript:
-
-WHY3_ISABELLE_HOME="$COMPONENT"
-WHY3_JEDIT_SERVER="server-Why3"
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$WHY3_ISABELLE_HOME/Tools"

share/provers-detection-data.conf

@@ -506,7 +506,20 @@ version_ok = "2015"
 version_bad = "2014"
 # not why3-cpulimit 0 %m because isabelle needs more memory at start-up
 command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
-driver = "drivers/isabelle.drv"