# HG changeset patch
# User Andreas Lochbihler
# Date 1338807354 -7200
# Node ID d7864276bca8938fba936cb155678da403567e66
# Parent  02d64fd408529fc0936be0961b8d97840ad0c6ec# Parent  e9b2782c4f99d20d5c68b4c967a29103de47c738
merged

diff -r 02d64fd40852 -r d7864276bca8 NEWS
--- a/NEWS	Mon Jun 04 09:50:57 2012 +0200
+++ b/NEWS	Mon Jun 04 12:55:54 2012 +0200
@@ -25,6 +25,12 @@
     It is switched on by default, and can be switched off by setting
     the configuration quickcheck_optimise_equality to false.    
 
+* The SMT solver Z3 has now by default a restricted set of directly
+supported features. For the full set of features (div/mod, nonlinear
+arithmetic, datatypes/records) with potential proof reconstruction
+failures, enable the configuration option "z3_with_extensions".
+Minor INCOMPATIBILITY.
+
 New in Isabelle2012 (May 2012)
 ------------------------------
 
diff -r 02d64fd40852 -r d7864276bca8 src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Mon Jun 04 09:50:57 2012 +0200
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Mon Jun 04 12:55:54 2012 +0200
@@ -50,6 +50,7 @@
 declare [[smt_certificates = "VCC_Max.certs"]]
 declare [[smt_read_only_certificates = true]]
 declare [[smt_oracle = false]]
+declare [[z3_with_extensions = true]]
 
 boogie_status
 
diff -r 02d64fd40852 -r d7864276bca8 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 04 09:50:57 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 04 12:55:54 2012 +0200
@@ -2319,7 +2319,7 @@
   note ab = conjunctD2[OF this[unfolded Un_subset_iff]]
   guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this]
   guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this]
-  have *:"\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False" by smt
+  have *:"\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False" using [[z3_with_extensions]] by smt
   note le_less_trans[OF component_le_norm[of _ k]] note this[OF w1(2)] this[OF w2(2)] moreover
   have "w1$$k \<le> w2$$k" apply(rule lem[OF w1(1) w2(1)]) using assms by auto ultimately
   show False unfolding euclidean_simps by(rule *) qed
@@ -3050,7 +3050,7 @@
       hence "d \<in> {a..b}" using s(2)[OF k(1)] unfolding k by auto note di = this[unfolded mem_interval,THEN spec[where x=i]]
       hence xyi:"y$$i \<noteq> x$$i" unfolding y_def unfolding i xi euclidean_lambda_beta'[OF i(2)] if_P[OF refl]
         apply(cases) apply(subst if_P,assumption) unfolding if_not_P not_le using as(2)
-        using assms(2)[unfolded content_eq_0] using i(2) by smt+ 
+        using assms(2)[unfolded content_eq_0] using i(2) using [[z3_with_extensions]] by smt+
       thus "y \<noteq> x" unfolding euclidean_eq[where 'a='a] using i by auto
       have *:"{..<DIM('a)} = insert i ({..<DIM('a)} - {i})" using i by auto
       have "norm (y - x) < e + setsum (\<lambda>i. 0) {..<DIM('a)}" apply(rule le_less_trans[OF norm_le_l1])
@@ -4236,7 +4236,7 @@
     proof- fix a b c d::"'n::ordered_euclidean_space" assume as:"ball 0 (max B1 B2) \<subseteq> {a..b}" "ball 0 (max B1 B2) \<subseteq> {c..d}"
       have **:"ball 0 B1 \<subseteq> ball (0::'n::ordered_euclidean_space) (max B1 B2)" "ball 0 B2 \<subseteq> ball (0::'n::ordered_euclidean_space) (max B1 B2)" by auto
       have *:"\<And>ga gc ha hc fa fc::real. abs(ga - i) < e / 3 \<and> abs(gc - i) < e / 3 \<and> abs(ha - j) < e / 3 \<and>
-        abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e" by smt
+        abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e" using [[z3_with_extensions]] by smt
       show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d} (\<lambda>x. if x \<in> s then f x else 0)) < e"
         unfolding real_norm_def apply(rule *, safe) unfolding real_norm_def[THEN sym]
         apply(rule B1(2),rule order_trans,rule **,rule as(1)) 
diff -r 02d64fd40852 -r d7864276bca8 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Jun 04 09:50:57 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Jun 04 12:55:54 2012 +0200
@@ -327,9 +327,13 @@
 
 lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by smt
 
-lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)" by smt
+lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)"
+  using [[z3_with_extensions]]
+  by smt
 
-lemma "x + (let y = x mod 2 in y + y) < x + (3::int)" by smt
+lemma "x + (let y = x mod 2 in y + y) < x + (3::int)"
+  using [[z3_with_extensions]]
+  by smt
 
 lemma
   assumes "x \<noteq> (0::real)"
@@ -339,7 +343,7 @@
 lemma
   assumes "(n + m) mod 2 = 0" and "n mod 4 = 3"
   shows "n mod 2 = 1 & m mod 2 = (1::int)"
-  using assms by smt
+  using assms [[z3_with_extensions]] by smt
 
 
 
@@ -393,18 +397,21 @@
 subsection {* Non-linear arithmetic over integers and reals *}
 
 lemma "a > (0::int) \<Longrightarrow> a*b > 0 \<Longrightarrow> b > 0"
-  using [[smt_oracle=true]]
+  using [[smt_oracle, z3_with_extensions]]
   by smt
 
 lemma  "(a::int) * (x + 1 + y) = a * x + a * (y + 1)"
+  using [[z3_with_extensions]]
   by smt
 
 lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)"
+  using [[z3_with_extensions]]
   by smt
 
 lemma
   "(U::int) + (1 + p) * (b + e) + p * d =
    U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
+  using [[z3_with_extensions]]
   by smt
 
 lemma [z3_rule]:
@@ -413,7 +420,9 @@
   shows False
   using assms by (metis mult_le_0_iff)
 
-lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0" by smt
+lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0"
+  using [[z3_with_extensions]]
+  by smt
 
 
 
@@ -498,6 +507,7 @@
     eval_dioph ks (map (\<lambda>x. x div 2) xs) =
       (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
   using [[smt_oracle=true]] (*FIXME*)
+  using [[z3_with_extensions]]
   by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
 
 
diff -r 02d64fd40852 -r d7864276bca8 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Jun 04 09:50:57 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Mon Jun 04 12:55:54 2012 +0200
@@ -315,6 +315,7 @@
   "(3::nat) div 3 = 1"
   "(x::nat) div 3 \<le> x"
   "(x div 3 = x) = (x = 0)"
+  using [[z3_with_extensions]]
   by smt+
 
 lemma
@@ -329,11 +330,13 @@
   "(3::nat) mod 3 = 0"
   "x mod 3 < 3"
   "(x mod 3 = x) = (x < 3)"
+  using [[z3_with_extensions]]
   by smt+
 
 lemma
   "(x::nat) = x div 1 * 1 + x mod 1"
   "x = x div 3 * 3 + x mod 3"
+  using [[z3_with_extensions]]
   by smt+
 
 lemma
@@ -447,6 +450,7 @@
   "(-1::int) div -3 = 0"
   "(-3::int) div -3 = 1"
   "(-5::int) div -3 = 1"
+  using [[z3_with_extensions]]
   by smt+
 
 lemma
@@ -476,11 +480,13 @@
   "(-5::int) mod -3 = -2"
   "x mod 3 < 3"
   "(x mod 3 = x) \<longrightarrow> (x < 3)"
+  using [[z3_with_extensions]]
   by smt+
 
 lemma
   "(x::int) = x div 1 * 1 + x mod 1"
   "x = x div 3 * 3 + x mod 3"
+  using [[z3_with_extensions]]
   by smt+
 
 lemma
@@ -585,6 +591,7 @@
   "(x::real) / 1 = x"
   "x > 0 \<longrightarrow> x / 3 < x"
   "x < 0 \<longrightarrow> x / 3 > x"
+  using [[z3_with_extensions]]
   by smt+
 
 lemma
@@ -592,6 +599,7 @@
   "(x * 3) / 3 = x"
   "x > 0 \<longrightarrow> 2 * x / 3 < x"
   "x < 0 \<longrightarrow> 2 * x / 3 > x"
+  using [[z3_with_extensions]]
   by smt+
 
 lemma
@@ -793,7 +801,7 @@
   "(fst (x, y) = snd (x, y)) = (x = y)"
   "(fst p = snd p) = (p = (snd p, fst p))"
   using fst_conv snd_conv pair_collapse
-  using [[smt_datatypes, smt_oracle]]
+  using [[smt_datatypes, smt_oracle, z3_with_extensions]]
   by smt+
 
 lemma
@@ -807,14 +815,14 @@
   "hd (tl [x, y, z]) = y"
   "tl (tl [x, y, z]) = [z]"
   using hd.simps tl.simps(2)
-  using [[smt_datatypes, smt_oracle]]
+  using [[smt_datatypes, smt_oracle, z3_with_extensions]]
   by smt+
 
 lemma
   "fst (hd [(a, b)]) = a"
   "snd (hd [(a, b)]) = b"
   using fst_conv snd_conv pair_collapse hd.simps tl.simps(2)
-  using [[smt_datatypes, smt_oracle]]
+  using [[smt_datatypes, smt_oracle, z3_with_extensions]]
   by smt+
 
 
@@ -826,7 +834,7 @@
   "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2"
   "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2"
   using point.simps
-  using [[smt_datatypes, smt_oracle]]
+  using [[smt_datatypes, smt_oracle, z3_with_extensions]]
   using [[z3_options="AUTO_CONFIG=false"]]
   by smt+
 
@@ -839,7 +847,7 @@
   "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p"
   using point.simps
-  using [[smt_datatypes, smt_oracle]]
+  using [[smt_datatypes, smt_oracle, z3_with_extensions]]
   using [[z3_options="AUTO_CONFIG=false"]]
   by smt+
 
@@ -848,7 +856,7 @@
   "cx (p \<lparr> cy := a \<rparr>) = cx p"
   "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
   using point.simps
-  using [[smt_datatypes, smt_oracle]]
+  using [[smt_datatypes, smt_oracle, z3_with_extensions]]
   using [[z3_options="AUTO_CONFIG=false"]]
   by smt+
 
@@ -860,7 +868,7 @@
   "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2"
   "black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2"
   using point.simps bw_point.simps
-  using [[smt_datatypes, smt_oracle]]
+  using [[smt_datatypes, smt_oracle, z3_with_extensions]]
   by smt+
 
 lemma
@@ -877,7 +885,7 @@
   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
      p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   using point.simps bw_point.simps
-  using [[smt_datatypes, smt_oracle]]
+  using [[smt_datatypes, smt_oracle, z3_with_extensions]]
   using [[z3_options="AUTO_CONFIG=false"]]
   by smt+
 
@@ -891,7 +899,7 @@
   "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> =
      p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
   using point.simps bw_point.simps
-  using [[smt_datatypes, smt_oracle]]
+  using [[smt_datatypes, smt_oracle, z3_with_extensions]]
   using [[z3_options="AUTO_CONFIG=false"]]
   by smt
 
@@ -905,7 +913,7 @@
   "nplus n1 n1 = n2"
   "nplus n1 n2 = n3"
   using n1_def n2_def n3_def nplus_def
-  using [[smt_datatypes, smt_oracle]]
+  using [[smt_datatypes, smt_oracle, z3_with_extensions]]
   using [[z3_options="AUTO_CONFIG=false"]]
   by smt+
 
diff -r 02d64fd40852 -r d7864276bca8 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Jun 04 09:50:57 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon Jun 04 12:55:54 2012 +0200
@@ -11,6 +11,7 @@
     Z3_Non_Commercial_Accepted |
     Z3_Non_Commercial_Declined
   val z3_non_commercial: unit -> z3_non_commercial
+  val z3_with_extensions: bool Config.T
   val setup: theory -> theory
 end
 
@@ -133,6 +134,9 @@
 end
 
 
+val z3_with_extensions =
+  Attrib.setup_config_bool @{binding z3_with_extensions} (K false)
+
 local
   fun z3_make_command is_remote name () =
     if_z3_non_commercial (make_command is_remote name)
@@ -163,11 +167,8 @@
       handle SMT_Failure.SMT _ => outcome (swap o split_last)
     end
 
-  val with_extensions =
-    Attrib.setup_config_bool @{binding z3_with_extensions} (K true)
-
   fun select_class ctxt =
-    if Config.get ctxt with_extensions then Z3_Interface.smtlib_z3C
+    if Config.get ctxt z3_with_extensions then Z3_Interface.smtlib_z3C
     else SMTLIB_Interface.smtlibC
 
   fun mk is_remote = {