Adapted to Isabelle2018

.gitignore

@@ -175,11 +175,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

Makefile.in

@@ -1261,7 +1261,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))

configure.in

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

doc/isabelle.tex

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

drivers/isabelle-2017.gen

+theory number.Coprime
+  syntax predicate coprime "<app><const name=\"GCD.gcd_class.coprime\"/>%1%2</app>"
+end

drivers/isabelle-2018.gen

+theory number.Coprime
+  syntax predicate coprime "<app><const name=\"Rings.algebraic_semidom_class.coprime\"/>%1%2</app>"
+end

drivers/isabelle-common.gen

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

drivers/isabelle2017-realize.drv

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

drivers/isabelle2017.drv

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

drivers/isabelle2016-1-realize.drv → drivers/isabelle2018-realize.drv

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

drivers/isabelle2016-1.drv → drivers/isabelle2018.drv

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

examples/logic/genealogy/genealogy_Genealogy_Child_is_son_or_daughter_1.thy

 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"

examples/logic/genealogy/genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.thy

 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"

examples/logic/genealogy/genealogy_Genealogy_Sibling_is_brother_or_sister_1.thy

 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"

examples/logic/genealogy/genealogy_Genealogy_Sibling_sym_1.thy

 theory genealogy_Genealogy_Sibling_sym_1
-imports Why3
+imports Why3.Why3
 begin
 
 why3_open "genealogy_Genealogy_Sibling_sym_1.xml"

examples/logic/genealogy/why3session.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"/>

lib/isabelle/ROOT.2016-1

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

lib/isabelle/Tools/why3

@@ -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' \

lib/isabelle/Why3_Number.thy.2016-1 → lib/isabelle/Why3_Number.thy.2018

 theory Why3_Number
 imports
   Why3_Int
-  "~~/src/HOL/Number_Theory/Primes"
+  "HOL-Computational_Algebra.Primes"
 begin
 
 section {* Parity properties *}
@@ -108,7 +108,7 @@ why3_vc even_divides ..
 why3_vc odd_divides ..
 
 why3_vc divides_spec
-  by (metis divides_factorl dvd_div_mult_self)
+  by (metis divides_factorl dvd_div_mult_self) 
 
 why3_end
 
@@ -140,17 +140,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 +224,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 +261,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 +287,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 +297,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 +307,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 +317,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
 

lib/isabelle/Why3_Real.thy.2016-1 → lib/isabelle/Why3_Real.thy.2018

 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)
 

lib/isabelle/Why3_Set.thy.2016-1

-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)
-
-why3_vc union_def by simp
-
-why3_vc add_remove
-  using assms
-  by (simp add: fun_upd_idem_iff mem_def)
-
-why3_vc inter_spec by (simp add: mem_def)
-
-why3_vc remove_add by auto
-
-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)
-
-why3_vc remove_spec
-  by (simp add: mem_def)
-
-why3_vc subset_diff
-  by (simp add: diff_spec subset_def)
-
-why3_vc subset_refl
-  by (simp add: subset_def)
-
-why3_vc subset_trans
-  by (meson H1 H2 subset_def)
-
-why3_vc subset_remove
-  by (simp add: remove_spec subset_def)
-
-why3_vc complement_def
-  by (simp add: complement_def)
-
-why3_vc extensionality
-  using assms
-  by (auto simp add: infix_eqeq_def mem_def)
-
-why3_end
-
-
-section {* Finite sets *}
-
-definition fremove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
-  "fremove x A = A - {|x|}"
-
-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)"
-
-why3_open "set/Fset.xml"
-  constants
-    mem = fmember
-    empty = bot
-    add = finsert
-    remove = fremove
-    union = sup
-    inter = inf
-    diff = minus
-    choose = fchoose
-    all = top
-    infix_eqeq = ext_eq
-    subset = fsubset_eq
-    is_empty = is_empty
-  types
-    set = fset
-
-why3_vc add_spec by simp
-
-why3_vc add_remove
-  using assms
-  by (auto simp add: fremove_def)
-
-why3_vc remove_add by (simp add: fremove_def)
-
-why3_vc empty_def by (simp add: is_empty_def)
-
-why3_vc inter_spec by simp
-
-why3_vc union_spec by simp
-
-why3_vc remove_spec by (auto simp add: fremove_def)
-
-why3_vc subset_diff by auto
-
-why3_vc subset_refl by simp
-
-why3_vc subset_trans
-  using assms
-  by simp
-
-why3_vc subset_remove by (auto simp add: fremove_def)
-
-why3_vc subset_eq
-  using assms ext_eq_def fcard_seteq by fastforce
-
-why3_vc subset_spec by auto
-
-why3_vc infix_eqeq_spec
-  by (metis ext_eq_def fsubset_antisym subset_spec)
-
-why3_vc extensionality
-  using assms
-  by (auto simp add: ext_eq_def)
-
-why3_vc cardinal1
-proof (cases s rule: fset_strong_cases)
-  case 1
-  with assms
-  show ?thesis by (simp add: fcard_fempty)
-next
-  case (2 s' x)
-  show ?thesis
-  proof (cases s' rule: fset_strong_cases)
-    case 1
-    with `s = finsert x s'` assms
-    show ?thesis by (simp add: fchoose_def)
-  next
-    case (2 s'' y)
-    with `s = finsert x s'` assms
-    show ?thesis by (auto simp add: fcard_finsert_if fchoose_def
-      split: if_split_asm)
-  qed
-qed
-
-why3_vc cardinal_add
-  using assms
-  by (simp add: fcard_finsert_disjoint)
-
-why3_vc cardinal_empty by (simp add: is_empty_def)
-
-why3_vc cardinal_nonneg by simp
-
-why3_vc cardinal_remove
-proof -
-  from assms
-  have "1 \<le> fcard s"
-    by (cases s rule: fset_strong_cases)
-      (auto simp add: fcard_finsert_disjoint)
-  with assms show ?thesis
-    by (simp add: fremove_def)
-qed
-
-why3_vc cardinal_subset
-  using assms
-  by (simp add: fcard_mono)
-
-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)
-
-why3_vc is_empty_spec
-  by (simp add: Why3_Set.is_empty_def)
-
-why3_end
-
-end

lib/isabelle/realizations.2016-1 → lib/isabelle/realizations.2018

@@ -20,7 +20,7 @@ da4b981eb0a086bafef4994a856470521dc76f3a  real/PowerInt.xml
 7543f13d887b95912e75f4286bb897ce6fa1c2a1  number/Gcd.xml
 d009220356ef6e55d1b92a43cec115ec1400b8e1  number/Parity.xml
 cf7bb9cfeed1b1dbb9ce5ed909508e24684ea7cb  number/Prime.xml
-c65c034efcb501c5828bc93ccd8ea479c0b096f1  number/Coprime.xml
+d6303a372876fe72982dcfbff168c8e8566bb439  number/Coprime.xml
 017b0bfd1148c566644b949d9d0eecd6dbae7b2b  set/Set.xml
 01b883e67d69549f63707ce4ebfc3a2d3e474876  set/Fset.xml
 6cf45ce21a7f543a525d4ad16344d5646fc5cb59  map/Map.xml

lib/isabelle/why3.ML.2016-1 → lib/isabelle/why3.ML.2018

@@ -713,8 +713,8 @@ fun add_axioms s [t] =
       fold_map Specification.axiom
         (map_index (fn (i, t) =>
            ((fact_binding (s ^ "_" ^ string_of_int (i + 1)), []), t)) ts) #>
-      apfst (pair (fact_binding s)) #>
-      uncurry Global_Theory.store_thms #> snd;
+      apfst (pair (fact_binding s) #> rpair [] #> single) #>
+      uncurry Global_Theory.add_thmss #> snd;
 
 fun dest_record thy [((s, _), args, [((cname, _), cargs)])] =
       let val tyname = Sign.full_name thy (Binding.name s)
@@ -977,7 +977,7 @@ fun close incomplete thy =
       {theories, env = SOME {thyname, vcs, ...}} =>
         let
           val (proved, unproved) = partition_vcs vcs;
-          val _ = Thm.join_proofs (maps (#1 o snd) proved)
+          val _ = Thm.consolidate (maps (#1 o snd) proved)
         in
           (if null unproved
            then writeln ("Finished Why3 theory " ^ thyname)

share/provers-detection-data.conf

@@ -624,11 +624,11 @@ name = "Isabelle"
 exec = "isabelle"
 version_switch = "version"
 version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
-version_ok = "2016-1"
+version_ok = "2018"
 version_bad = "2017"
-version_bad = "2016"
+version_bad = "2016-1"
 command = "%e why3 -b %f"
-driver = "isabelle2016-1"
+driver = "isabelle2018"
 in_place = true
 editor = "isabelle-jedit"
 
@@ -638,8 +638,8 @@ exec = "isabelle"
 version_switch = "version"
 version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
 version_ok = "2017"
+version_bad = "2018"
 version_bad = "2016-1"
-version_bad = "2016"
 command = "%e why3 -b %f"
 driver = "isabelle2017"
 in_place = true