Adapted to Isabelle2017

.gitignore

@@ -164,11 +164,10 @@ pvsbin/
 /lib/isabelle/map/
 /lib/isabelle/real/
 /lib/isabelle/set/
-/lib/isabelle/Why3_Bool.thy
+/lib/isabelle/ROOT
 /lib/isabelle/Why3_BV.thy
-/lib/isabelle/Why3_Int.thy
-/lib/isabelle/Why3_List.thy
 /lib/isabelle/Why3_Number.thy
+/lib/isabelle/Why3_Real.thy
 /lib/isabelle/Why3_Set.thy
 /lib/isabelle/why3.ML
 /lib/isabelle/last_build

Makefile.in

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

configure.in

@@ -648,16 +648,16 @@ else
                 ISABELLEVERSION=2016-1
                 AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
                 ;;
-          2016*)
+          2017*)
 	        enable_isabelle_support=yes
-                ISABELLEVERSION=2016
+                ISABELLEVERSION=2017
                 AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
                 ;;
           *)
                 AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
                 enable_isabelle_support=no
-	        AC_MSG_WARN(You need Isabelle 2016 or later; Isabelle discarded)
-                reason_isabelle_support=" (need version >= 2016)"
+	        AC_MSG_WARN(You need Isabelle 2016-1 or later; Isabelle discarded)
+                reason_isabelle_support=" (need version >= 2016-1)"
                 ;;
         esac
     fi

doc/isabelle.tex

@@ -11,9 +11,9 @@ using ``Edit'' action in \texttt{why3 ide}.
 
 \subsection{Installation}
 
-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.
+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.
 
 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-1/etc/components
+.isabelle/Isabelle2017/etc/components
 \end{verbatim}
 or the system-wide file
 \begin{verbatim}

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

drivers/isabelle-common.gen

@@ -163,6 +163,10 @@ 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=\"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

drivers/isabelle2016-1-realize.drv

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

drivers/isabelle2016-1.drv

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

drivers/isabelle2016-realize.drv → drivers/isabelle2017-realize.drv

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

drivers/isabelle2016.drv → drivers/isabelle2017.drv

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

lib/isabelle/ROOT.2017

+chapter Why3
+
+session Why3 = "HOL-Word" +
+  options [document = false]
+  sessions
+    "HOL-Library"
+    "HOL-Decision_Procs"
+    "HOL-Computational_Algebra"
+  theories Why3

lib/isabelle/Tools/why3

@@ -83,7 +83,7 @@ else
 fi
 
 if [ "$BATCH" = true ]; then
-  echo "use_thy \"$NAME\";" | "$ISABELLE_TOOL" console "${SESSION_DIR[@]}" -l "$SESSION"
+  "$ISABELLE_TOOL" process "${SESSION_DIR[@]}" -l "$SESSION" -T "$NAME"
 elif [ "$INTERACTIVE" = true ]; then
   make_theory "$NAME"
   if [ -f "$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER" ]; then

lib/isabelle/Why3_BV.thy.2016 → lib/isabelle/Why3_BV.thy.2017

 theory Why3_BV
-imports Why3_Int "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison"
+imports
+  Why3_Int
+  "HOL-Word.Word"
+  "HOL-Word.Bit_Comparison"
 begin
 
 abbreviation (input) pow2 :: "int \<Rightarrow> int"
@@ -120,7 +123,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"
@@ -151,7 +154,7 @@ next
 qed
 
 lemma uint_pow: "uint ((b::'a::len word) ^ n) = uint b ^ n mod 2 ^ len_of TYPE('a)"
-  by (induct n) (simp_all add: mod_pos_pos_trivial uint_word_ariths pull_mods)
+  by (induct n) (simp_all add: mod_pos_pos_trivial uint_word_ariths mod_mult_right_eq)
 
 
 lemma eq_sub_equiv_aux:
@@ -172,10 +175,10 @@ lemma eq_sub_equiv_aux:
 lemma int_minus_mod: "((i::int) - j) mod n = (i + (n - j mod n)) mod n"
 proof -
   have "(i + (n - j mod n)) mod n = (i mod n + (n - j mod n) mod n) mod n"
-    by (simp only: pull_mods(1))
+    by (simp only: mod_add_eq)
   also have "(n - j mod n) mod n = (n mod n - j mod n) mod n"
-    by (simp add: pull_mods)
-  finally show ?thesis by (simp add: pull_mods)
+    by simp
+  finally show ?thesis by (simp add: pull_mods [symmetric])
 qed
 
 lemma nat_minus_mod:
@@ -185,7 +188,7 @@ proof -
   have "((n - i mod n) + i) mod n = (i + (n - i mod n)) mod n"
     by (simp add: add_ac)
   also have "\<dots> = (i mod n + (n - i mod n)) mod n"
-    by (simp add: pull_mods)
+    by (simp add: pull_mods [symmetric])
   also from assms have "\<dots> = (n mod n + (i mod n - i mod n)) mod n"
     by (simp add: add_ac)
   finally show ?thesis by simp
@@ -198,7 +201,7 @@ proof -
   have "(i + (n - j mod n) + j) mod n = (i + ((n - j mod n) + j)) mod n"
     by (simp add: add_ac)
   also have "\<dots> = (i mod n + ((n - j mod n) + j) mod n) mod n"
-    by (simp add: pull_mods)
+    by (simp add: pull_mods [symmetric])
   also note nat_minus_mod [OF assms]
   finally show ?thesis by simp
 qed
@@ -245,7 +248,7 @@ definition eq_sub_bv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a wor
     (b AND (mask (unat n) << unat i) = a AND (mask (unat n) << unat i))"
 
 definition size_bv :: "'a::len word" where
-  "size_bv = of_nat (len_of TYPE('a))"
+  "size_bv = of_nat LENGTH('a)"
 
 type_synonym word8 = "8 word"
 
@@ -262,7 +265,7 @@ why3_open "bv/BV8.xml"
     neg=uminus
     mul=times
     udiv=divide
-    urem=mod
+    urem=modulo
     lsr=lsr
     asr=asr
     lsl=lsl
@@ -428,7 +431,7 @@ why3_vc lsl_bv_is_lsl by (simp add: unat_def)
 
 why3_vc to_uint_lsl
   by (simp add: emod_def shiftl_t2n unat_def
-    uint_word_ariths mult_ac uint_pow pull_mods)
+    uint_word_ariths mult_ac uint_pow pull_mods [symmetric])
 
 why3_vc Extensionality
   using assms
@@ -458,7 +461,7 @@ why3_open "bv/BV16.xml"
     neg=uminus
     mul=times
     udiv=divide
-    urem=mod
+    urem=modulo
     lsr=lsr
     asr=asr
     lsl=lsl
@@ -624,7 +627,7 @@ why3_vc lsl_bv_is_lsl by (simp add: unat_def)
 
 why3_vc to_uint_lsl
   by (simp add: emod_def shiftl_t2n unat_def
-    uint_word_ariths mult_ac uint_pow pull_mods)
+    uint_word_ariths mult_ac uint_pow pull_mods [symmetric])
 
 why3_vc Extensionality
   using assms
@@ -654,7 +657,7 @@ why3_open "bv/BV32.xml"
     neg=uminus
     mul=times
     udiv=divide
-    urem=mod
+    urem=modulo
     lsr=lsr
     asr=asr
     lsl=lsl
@@ -820,7 +823,7 @@ why3_vc lsl_bv_is_lsl by (simp add: unat_def)
 
 why3_vc to_uint_lsl
   by (simp add: emod_def shiftl_t2n unat_def
-    uint_word_ariths mult_ac uint_pow pull_mods)
+    uint_word_ariths mult_ac uint_pow pull_mods [symmetric])
 
 why3_vc Extensionality
   using assms
@@ -850,7 +853,7 @@ why3_open "bv/BV64.xml"
     neg=uminus
     mul=times
     udiv=divide
-    urem=mod
+    urem=modulo
     lsr=lsr
     asr=asr
     lsl=lsl
@@ -1016,7 +1019,7 @@ why3_vc lsl_bv_is_lsl by (simp add: unat_def)
 
 why3_vc to_uint_lsl
   by (simp add: emod_def shiftl_t2n unat_def
-    uint_word_ariths mult_ac uint_pow pull_mods)
+    uint_word_ariths mult_ac uint_pow pull_mods [symmetric])
 
 why3_vc Extensionality
   using assms

lib/isabelle/Why3_Bool.thy.2016

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

lib/isabelle/Why3_Int.thy.2016

-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_times [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
-