Adapted to Isabelle2016-1. Contributed by Stefan Berghofer <stefan.berghofer@secunet.com>

.gitignore

@@ -162,7 +162,12 @@ pvsbin/
 /lib/isabelle/map/
 /lib/isabelle/real/
 /lib/isabelle/set/
+/lib/isabelle/Why3_Bool.thy
 /lib/isabelle/Why3_BV.thy
+/lib/isabelle/Why3_Int.thy
+/lib/isabelle/Why3_List.thy
+/lib/isabelle/Why3_Number.thy
+/lib/isabelle/Why3_Set.thy
 /lib/isabelle/why3.ML
 /lib/isabelle/last_build
 /lib/isabelle/bv

Makefile.in

@@ -1117,7 +1117,7 @@ clean::
 
 ifeq (@enable_isabelle_libs@,yes)
 
-ISABELLEVERSIONSPECIFIC=why3.ML Why3_BV.thy
+ISABELLEVERSIONSPECIFIC=why3.ML Why3_Bool.thy Why3_BV.thy Why3_Int.thy Why3_List.thy Why3_Number.thy Why3_Set.thy
 
 ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
 ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS))

configure.in

@@ -646,9 +646,9 @@ else
         ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
 
         case $ISABELLEDETECTEDVERSION in
-          2015*)
+          2016-1*)
 	        enable_isabelle_support=yes
-                ISABELLEVERSION=2015
+                ISABELLEVERSION=2016-1
                 AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
                 ;;
           2016*)
@@ -659,8 +659,8 @@ else
           *)
                 AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
                 enable_isabelle_support=no
-	        AC_MSG_WARN(You need Isabelle 2015 or later; Isabelle discarded)
-                reason_isabelle_support=" (need version >= 2015)"
+	        AC_MSG_WARN(You need Isabelle 2016 or later; Isabelle discarded)
+                reason_isabelle_support=" (need version >= 2016)"
                 ;;
         esac
     fi

doc/isabelle.tex

@@ -11,9 +11,9 @@ using ``Edit'' action in \texttt{why3 ide}.
 
 \subsection{Installation}
 
-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.
+You need version Isabelle2016 or Isabelle2016-1. Former versions are not
+supported. We assume below that your version is 2016-1, please replace
+2016-1 by 2016 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/Isabelle2016/etc/components
+.isabelle/Isabelle2016-1/etc/components
 \end{verbatim}
 or the system-wide file
 \begin{verbatim}

drivers/isabelle-2015.gen

-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

drivers/isabelle-2016-1.gen

+theory number.Prime
+  syntax predicate prime "<app><const name=\"Factorial_Ring.normalization_semidom_class.prime\"/>%1</app>"
+end

drivers/isabelle-2016.gen

-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>"
+theory number.Prime
+  syntax predicate prime "<app><const name=\"Primes.prime\"/><app><const name=\"Int.nat\"/>%1</app></app>"
 end

drivers/isabelle-common.gen

@@ -163,14 +163,15 @@ theory number.Gcd
   syntax function gcd "<app><const name=\"GCD.gcd_class.gcd\"/>%1%2</app>"
 end
 
-theory number.Prime
-  syntax predicate prime "<app><const name=\"Primes.prime\"/><app><const name=\"Int.nat\"/>%1</app></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>"
+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>"

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

@@ -7,4 +7,4 @@ filename "%t.xml"
 transformation "inline_trivial"
 
 import "isabelle-common.gen"
-import "isabelle-2015.gen"
+import "isabelle-2016-1.gen"

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

@@ -8,7 +8,7 @@ transformation "inline_trivial"
 transformation "eliminate_builtin"
 
 import "isabelle-common.gen"
-import "isabelle-2015.gen"
+import "isabelle-2016-1.gen"
 
 
 transformation "simplify_trivial_quantification_in_goal"

lib/isabelle/Tools/why3

@@ -70,16 +70,28 @@ shift $(($OPTIND - 1))
 
 NAME=`dirname "$1"`/`basename "$1" .xml`
 
+if [ "$ISABELLE_WHY3_SESSION" ]; then
+  SESSION="$ISABELLE_WHY3_SESSION"
+else
+  SESSION=Why3
+fi
+
+if [ "$ISABELLE_WHY3_SESSION_DIR" ]; then
+  SESSION_DIR=("-d" "$ISABELLE_WHY3_SESSION_DIR")
+else
+  SESSION_DIR=()
+fi
+
 if [ "$BATCH" = true ]; then
-  "$ISABELLE_PROCESS" -e "use_thy \"$NAME\";" -rq Why3
+  echo "use_thy \"$NAME\";" | "$ISABELLE_TOOL" console "${SESSION_DIR[@]}" -l "$SESSION"
 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")"
+    "$ISABELLE_TOOL" java -jar "$(platform_path "$JEDIT_HOME/dist/jedit.jar")" \
+      "-settings=$(platform_path "$JEDIT_SETTINGS")" "-server=$WHY3_JEDIT_SERVER" \
+      -reuseview -wait "$(platform_path "${NAME}.thy")"
   else
-    "$ISABELLE_TOOL" jedit -l Why3 "${NAME}.thy"
+    "$ISABELLE_TOOL" jedit "${SESSION_DIR[@]}" -l "$SESSION" "${NAME}.thy"
   fi
 else
   usage

lib/isabelle/Tools/why3_jedit

@@ -26,12 +26,30 @@ function fail()
 
 ## main
 
-[ "$1" = "-?" ] && usage
+SESSION=Why3
+SESSION_DIR=()
+
+while getopts "l:d:" OPT
+do
+  case "$OPT" in
+    l)
+      SESSION="$OPTARG"
+      ;;
+    d)
+      SESSION_DIR=("-d" "$OPTARG")
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
 
 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 "$@"
+  exec "$ISABELLE_TOOL" jedit "-j-server=$WHY3_JEDIT_SERVER" "${SESSION_DIR[@]}" -l "$SESSION" "$@"
 fi

lib/isabelle/Why3_BV.thy.2015 → lib/isabelle/Why3_BV.thy.2016-1

@@ -120,7 +120,7 @@ lemma rotater1_rotater_swap: "rotater1 (rotater n xs) = rotater n (rotater1 xs)"
   by (simp add: rotater_def funpow_swap1)
 
 lemma length_rotater1 [simp]: "length (rotater1 xs) = length xs"
-  by (simp add: rotater1_def split add: list.split)
+  by (simp add: rotater1_def split: list.split)
 
 lemma rotater1_nth:
   assumes "0 < length xs"
@@ -258,8 +258,8 @@ why3_open "bv/BV8.xml"
     sub=minus
     neg=uminus
     mul=times
-    udiv=div
-    urem=mod
+    udiv=divide
+    urem=modulo
     lsr=lsr
     asr=asr
     lsl=lsl
@@ -448,8 +448,8 @@ why3_open "bv/BV16.xml"
     sub=minus
     neg=uminus
     mul=times
-    udiv=div
-    urem=mod
+    udiv=divide
+    urem=modulo
     lsr=lsr
     asr=asr
     lsl=lsl
@@ -638,8 +638,8 @@ why3_open "bv/BV32.xml"
     sub=minus
     neg=uminus
     mul=times
-    udiv=div
-    urem=mod
+    udiv=divide
+    urem=modulo
     lsr=lsr
     asr=asr
     lsl=lsl
@@ -828,8 +828,8 @@ why3_open "bv/BV64.xml"
     sub=minus
     neg=uminus
     mul=times
-    udiv=div
-    urem=mod
+    udiv=divide
+    urem=modulo
     lsr=lsr
     asr=asr
     lsl=lsl

lib/isabelle/Why3_Bool.thy.2016-1

+theory Why3_Bool
+imports Why3_Setup
+begin
+
+section {* Basic theory of Booleans *}
+
+why3_open "bool/Bool.xml"
+
+why3_vc andb_def by (simp split: bool.split)
+
+why3_vc orb_def by (simp split: bool.split)
+
+why3_vc xorb_def by (simp split: bool.split)
+
+why3_vc notb_def by (simp split: bool.split)
+
+why3_vc implb_def by (simp split: bool.split)
+
+why3_end
+
+end

lib/isabelle/Why3_Int.thy.2016-1

+theory Why3_Int
+imports Why3_Setup
+begin
+
+section {* Integers and the basic operators *}
+
+why3_open "int/Int.xml"
+
+why3_vc Comm by simp
+
+why3_vc Comm1 by simp
+
+why3_vc Assoc by simp
+
+why3_vc Assoc1 by simp
+
+why3_vc Unitary by simp
+
+why3_vc Inv_def_l by simp
+
+why3_vc Inv_def_r by simp
+
+why3_vc Unit_def_l by simp
+
+why3_vc Unit_def_r by simp
+
+why3_vc Mul_distr_l by (simp add: ring_distribs)
+
+why3_vc Mul_distr_r by (simp add: ring_distribs)
+
+why3_vc infix_mn_def by simp
+
+why3_vc NonTrivialRing by simp
+
+why3_vc infix_lseq_def by auto
+
+why3_vc Refl by simp
+
+why3_vc Trans using assms by simp
+
+why3_vc Total by auto
+
+why3_vc Antisymm using assms by simp
+
+why3_vc ZeroLessOne by simp
+
+why3_vc CompatOrderAdd using assms by simp
+
+why3_vc CompatOrderMult using assms by (rule mult_right_mono)
+
+why3_end
+
+
+section {* Absolute Value *}
+
+why3_open "int/Abs.xml"
+
+why3_vc abs_def by simp
+
+why3_vc Abs_le by auto
+
+why3_vc Abs_pos by simp
+
+why3_end
+
+
+section {* Minimum and Maximum *}
+
+why3_open "int/MinMax.xml"
+
+why3_vc Max_l using assms by simp
+
+why3_vc Max_comm by simp
+
+why3_vc Max_assoc by simp
+
+why3_vc Min_r using assms by simp
+
+why3_vc Min_comm by simp
+
+why3_vc Min_assoc by simp
+
+why3_vc max_def by auto
+
+why3_vc min_def by auto
+
+why3_end
+
+
+section {* Euclidean Division *}
+
+definition ediv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "ediv" 70) where
+  "a ediv b = sgn b * (a div \<bar>b\<bar>)"
+
+definition emod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "emod" 70) where
+  "a emod b = a mod \<bar>b\<bar>"
+
+why3_open "int/EuclideanDivision.xml"
+  constants
+    div = ediv
+    mod = emod
+
+why3_vc Div_1 by (simp add: ediv_def)
+
+why3_vc Div_1_left using assms by (simp add: ediv_def div_pos_pos_trivial)
+
+why3_vc Div_inf using assms by (simp add: ediv_def div_pos_pos_trivial)
+
+why3_vc Div_inf_neg
+  using assms
+  by (cases "x = y") (simp_all add: ediv_def
+    zdiv_zminus1_eq_if div_pos_pos_trivial mod_pos_pos_trivial)
+
+why3_vc Div_mod
+  by (simp add: ediv_def emod_def mult.assoc [symmetric] abs_sgn)
+
+why3_vc Div_mult using assms by (simp add: ediv_def add.commute)
+
+why3_vc Div_bound
+proof -
+  from assms show ?C1
+    by (simp add: ediv_def pos_imp_zdiv_nonneg_iff)
+
+  show ?C2
+  proof (cases "x = 0")
+    case False
+    show ?thesis
+    proof (cases "y = 1")
+      case False
+      with assms `x \<noteq> 0` have "x div y < x"
+        by (simp add: int_div_less_self)
+      with assms show ?thesis by (simp add: ediv_def)
+    qed (simp add: ediv_def)
+  qed (simp add: ediv_def)
+qed
+
+why3_vc Div_minus1_left
+  using assms
+  by (simp only: zdiv_zminus1_eq_if ediv_def)
+    (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
+
+why3_vc Mod_0 by (simp add: emod_def)
+
+why3_vc Mod_1 by (simp add: emod_def)
+
+why3_vc Mod_1_left using assms by (simp add: emod_def mod_pos_pos_trivial)
+
+why3_vc Mod_minus1_left
+  using assms
+  by (simp only: emod_def zmod_zminus1_eq_if) (simp add: mod_pos_pos_trivial)
+
+why3_vc Mod_mult using assms by (simp add: emod_def add.commute)
+
+why3_vc Mod_bound using assms by (simp_all add: emod_def)
+
+why3_vc Div_unique using assms
+ proof - 
+  have h0: "y \<noteq> 0" using assms by auto
+  have h1: "x = y * (x ediv y) + (x emod y)" using h0 Div_mod by blast
+  have h2: "0 \<le> x emod y \<and> x emod y < y" using assms H1 h0 Mod_bound zabs_def
+    by (metis abs_sgn monoid_mult_class.mult.right_neutral sgn_pos)
+  have h3: "x - y < y * (x ediv y)" using h1 h2 by linarith
+  have h4: "y * (x ediv y) \<le> x" using h1 h2 by linarith
+  show ?thesis
+  proof (cases "x ediv y > q")
+   assume a:"q < x ediv y"
+   have h5: "x ediv y \<ge> q + 1" using a by linarith
+   have h6: "y * (x ediv y) >= y * (q + 1)" by (metis H1 h5 le_less mult_left_mono)
+   have h7: "y * (x ediv y) >= q * y + y" by (metis Comm1 Mul_distr_l h6 monoid_mult_class.mult.right_neutral) 
+   thus "x ediv y = q" using H3 h1 h2 h7 by linarith
+   next
+   assume a:"\<not> q < x ediv y"
+   show "x ediv y = q"    
+   proof (cases "x ediv y < q")
+    assume b:"x ediv y < q"
+    have h5: "x ediv y \<le> q - 1" using b by linarith
+    have h6: "y * (x ediv y) <= y * (q - 1)" by (metis H1 h5 le_less mult_left_mono)
+    have h7: "y * (x ediv y) <= q * y - y" by (metis Comm1 h6 int_distrib(4) monoid_mult_class.mult.right_neutral) 
+    thus "x ediv y = q" using H2 h3 h7 by linarith
+    next
+    assume b:"\<not> x ediv y < q"
+    show ?thesis using a b by linarith
+   qed
+  qed
+qed
+
+why3_end
+
+section {* Computer Division *}
+
+definition cdiv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "cdiv" 70) where
+  "a cdiv b = sgn a * sgn b * (\<bar>a\<bar> div \<bar>b\<bar>)"
+
+definition cmod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "cmod" 70) where
+  "a cmod b = sgn a * (\<bar>a\<bar> mod \<bar>b\<bar>)"
+
+why3_open "int/ComputerDivision.xml"
+  constants
+    div = cdiv
+    mod = cmod
+
+why3_vc Div_1 by (simp add: cdiv_def mult_sgn_abs)
+
+why3_vc Div_inf using assms by (simp add: cdiv_def div_pos_pos_trivial)
+
+why3_vc Div_sign_neg
+  using assms
+  by (cases "x = 0") (simp_all add: cdiv_def
+    zdiv_zminus1_eq_if div_nonpos_pos_le0 pos_imp_zdiv_neg_iff)
+
+why3_vc Div_sign_pos
+  using assms
+  by (cases "x = 0")
+    (simp_all add: cdiv_def pos_imp_zdiv_nonneg_iff)
+
+why3_vc Div_mod
+proof -
+  have "y * (sgn x * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>)) + sgn x * (\<bar>x\<bar> mod \<bar>y\<bar>) =
+    sgn x * (y * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>) + \<bar>x\<bar> mod \<bar>y\<bar>)"
+    by (simp add: ring_distribs)
+  then show ?thesis
+    by (cases "x = 0") (simp_all add: cdiv_def cmod_def abs_sgn
+      sgn_mult [symmetric] order.strict_iff_order)
+qed
+
+why3_vc Div_mult
+proof (cases "y = 0")
+  case False
+  with assms show ?thesis
+    by (cases "z = 0")
+      (simp_all add: cdiv_def add.commute add_pos_pos)
+qed simp
+
+why3_vc Div_bound
+proof -
+  from assms show ?C1
+    by (simp add: cdiv_def pos_imp_zdiv_nonneg_iff sgn_if)
+
+  show ?C2
+  proof (cases "x = 0")
+    case False
+    show ?thesis
+    proof (cases "y = 1")
+      case False
+      with assms `x \<noteq> 0` have "x div y < x"
+        by (simp add: int_div_less_self)
+      with assms show ?thesis by (simp add: cdiv_def sgn_if)
+    qed (simp add: cdiv_def sgn_if)
+  qed (simp add: cdiv_def)
+qed
+
+why3_vc Mod_1 by (simp add: cmod_def)
+
+why3_vc Mod_inf using assms by (simp add: cmod_def mod_pos_pos_trivial sgn_if)
+
+why3_vc Mod_mult
+proof (cases "y = 0")
+  case False
+  with assms show ?thesis
+    by (cases "z = 0") (simp_all add: cmod_def add.commute add_pos_pos)
+qed simp
+
+why3_vc Mod_bound
+proof -
+  from assms show ?C1
+    by (auto simp add: cmod_def sgn_if intro: less_le_trans [of _ 0])
+
+  from assms show ?C2
+    by (auto simp add: cmod_def sgn_if intro: le_less_trans [of _ 0])
+qed
+
+why3_vc Mod_sign_neg using assms by (simp add: cmod_def sgn_if)
+
+why3_vc Mod_sign_pos using assms by (simp add: cmod_def sgn_if)
+
+why3_vc Rounds_toward_zero
+proof (cases "x = 0")
+  case False
+  then have "\<bar>sgn x\<bar> = 1" by (simp add: sgn_if)
+  have "sgn x * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>) * y =
+    sgn x * (y * sgn y * (\<bar>x\<bar> div \<bar>y\<bar>))" (is "?l = ?r")
+    by simp
+  then have "\<bar>?l\<bar> = \<bar>?r\<bar>" by (simp (no_asm_simp))
+  also note abs_sgn [symmetric]
+  also note abs_mult
+  also have "\<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>) \<le> \<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>) + \<bar>x\<bar> mod \<bar>y\<bar>"
+    by (rule add_increasing2) (simp_all add: assms)
+  with assms have "\<bar>\<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>)\<bar> \<le> \<bar>\<bar>y\<bar> * (\<bar>x\<bar> div \<bar>y\<bar>) + \<bar>x\<bar> mod \<bar>y\<bar>\<bar>"
+    by (simp add: pos_imp_zdiv_nonneg_iff)
+  finally show ?thesis using `\<bar>sgn x\<bar> = 1`
+    by (simp add: cdiv_def)
+qed (simp add: cdiv_def)
+
+why3_end
+
+
+section {* Division by 2 *}
+
+why3_open "int/Div2.xml"
+
+why3_vc div2
+  by (rule exI [of _ "x div 2"]) auto
+
+why3_end
+
+
+section {* Power of an integer to an integer *}
+
+why3_open "int/Power.xml"
+
+why3_vc Power_0 by simp
+
+why3_vc Power_1 by simp
+
+why3_vc Power_s using assms by (simp add: nat_add_distrib)
+
+why3_vc Power_s_alt using assms by (simp add: nat_diff_distrib power_Suc [symmetric])
+
+why3_vc Power_sum using assms by (simp add: nat_add_distrib power_add)
+
+why3_vc Power_mult using assms by (simp add: nat_mult_distrib power_mult)
+
+why3_vc Power_mult2 by (simp add: power_mult_distrib)
+
+why3_vc Power_non_neg using assms by simp
+
+why3_vc Power_monotonic using assms by (simp add: power_increasing)
+
+why3_end
+
+end
+

lib/isabelle/Why3_List.thy.2016-1

+theory Why3_List
+imports Why3_Setup
+begin
+
+section {* Length of a list *}
+
+why3_open "list/Length.xml"
+
+why3_vc length_def by (cases l) simp_all
+
+why3_vc Length_nil by simp
+
+why3_vc Length_nonnegative by simp
+
+why3_end
+
+
+section {* Membership in a list *}
+
+why3_open "list/Mem.xml"
+
+why3_vc mem_def by (simp split: list.split)
+
+why3_end
+
+
+section {* Nth element of a list *}
+
+why3_open "list/Nth.xml"
+
+lemma nth_eq: "0 \<le> i \<Longrightarrow> nat i < length xs \<Longrightarrow> nth i xs = Some (xs ! nat i)"
+  by (induct xs arbitrary: i) (auto simp add: nat_diff_distrib)
+
+why3_end
+
+
+why3_open "list/NthNoOpt.xml"
+
+why3_vc nth_cons_0 by simp
+
+why3_vc nth_cons_n
+  using assms
+  by (simp add: nat_diff_distrib)
+
+why3_end
+
+
+why3_open "list/NthLength.xml"
+
+why3_vc nth_none_1
+  using assms
+  by (induct l arbitrary: i) simp_all
+
+why3_vc nth_none_2
+  using assms
+  by (induct l arbitrary: i) simp_all
+
+why3_vc nth_none_3
+  using assms
+proof (induct l arbitrary: i)
+  case Nil
+  then show ?case by simp arith
+next
+  case (Cons x xs)
+  show ?case
+  proof (cases "i < 0")