# HG changeset patch
# User wenzelm
# Date 1506190156 -7200
# Node ID ebb97a834338167d693488ca3e419debeccd0f75
# Parent  4b10fa05423baa1ae48a570aa6f5257a2cf5f541# Parent  cd8ad4eddb8addf81ca6d70ef91c778cd7e7e440
merged

diff -r cd8ad4eddb8a -r ebb97a834338 CONTRIBUTORS
--- a/CONTRIBUTORS	Sat Sep 23 13:46:48 2017 +0200
+++ b/CONTRIBUTORS	Sat Sep 23 20:09:16 2017 +0200
@@ -3,6 +3,10 @@
 listed as an author in one of the source files of this Isabelle distribution.
 
 
+Contributions to this Isabelle version
+--------------------------------------
+
+
 Contributions to Isabelle2017
 -----------------------------
 
diff -r cd8ad4eddb8a -r ebb97a834338 NEWS
--- a/NEWS	Sat Sep 23 13:46:48 2017 +0200
+++ b/NEWS	Sat Sep 23 20:09:16 2017 +0200
@@ -4,6 +4,16 @@
 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
 
 
+New in this Isabelle version
+----------------------------
+
+*** HOL ***
+
+* SMT module:
+  - The 'smt_oracle' option is now necessary when using the 'smt' method
+    with a solver other than Z3. INCOMPATIBILITY.
+
+
 New in Isabelle2017 (October 2017)
 ----------------------------------
 
diff -r cd8ad4eddb8a -r ebb97a834338 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Sat Sep 23 13:46:48 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Sat Sep 23 20:09:16 2017 +0200
@@ -739,7 +739,7 @@
 lemma holomorphic_factor_zero_nonconstant:
   assumes holf: "f holomorphic_on S" and S: "open S" "connected S"
       and "\<xi> \<in> S" "f \<xi> = 0"
-      and nonconst: "\<And>c. \<exists>z \<in> S. f z \<noteq> c"
+      and nonconst: "~ f constant_on S"
    obtains g r n
       where "0 < n"  "0 < r"  "ball \<xi> r \<subseteq> S"
             "g holomorphic_on ball \<xi> r"
@@ -747,7 +747,7 @@
             "\<And>w. w \<in> ball \<xi> r \<Longrightarrow> g w \<noteq> 0"
 proof (cases "\<forall>n>0. (deriv ^^ n) f \<xi> = 0")
   case True then show ?thesis
-    using holomorphic_fun_eq_const_on_connected [OF holf S _ \<open>\<xi> \<in> S\<close>] nonconst by auto
+    using holomorphic_fun_eq_const_on_connected [OF holf S _ \<open>\<xi> \<in> S\<close>] nonconst by (simp add: constant_on_def)
 next
   case False
   then obtain n0 where "n0 > 0" and n0: "(deriv ^^ n0) f \<xi> \<noteq> 0" by blast
@@ -3074,18 +3074,19 @@
 
 lemma holomorphic_factor_zero_Ex1:
   assumes "open s" "connected s" "z \<in> s" and
-        holo:"f holomorphic_on s"
-        and "f z = 0" and "\<exists>w\<in>s. f w \<noteq> 0"
+        holf: "f holomorphic_on s"
+        and f: "f z = 0" "\<exists>w\<in>s. f w \<noteq> 0"
   shows "\<exists>!n. \<exists>g r. 0 < n \<and> 0 < r \<and>
                 g holomorphic_on cball z r
                 \<and> (\<forall>w\<in>cball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0)"
 proof (rule ex_ex1I)
-  obtain g r n where "0 < n" "0 < r" "ball z r \<subseteq> s" and
+  have "\<not> f constant_on s"
+    by (metis \<open>z\<in>s\<close> constant_on_def f)
+  then obtain g r n where "0 < n" "0 < r" "ball z r \<subseteq> s" and
           g:"g holomorphic_on ball z r"
           "\<And>w. w \<in> ball z r \<Longrightarrow> f w = (w - z) ^ n * g w"
           "\<And>w. w \<in> ball z r \<Longrightarrow> g w \<noteq> 0"
-    using holomorphic_factor_zero_nonconstant[OF holo \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>]
-    by (metis assms(3) assms(5) assms(6))
+    by (blast intro: holomorphic_factor_zero_nonconstant[OF holf \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>])
   define r' where "r' \<equiv> r/2"
   have "cball z r' \<subseteq> ball z r" unfolding r'_def by (simp add: \<open>0 < r\<close> cball_subset_ball_iff)
   hence "cball z r' \<subseteq> s" "g holomorphic_on cball z r'"
diff -r cd8ad4eddb8a -r ebb97a834338 src/HOL/Analysis/Great_Picard.thy
--- a/src/HOL/Analysis/Great_Picard.thy	Sat Sep 23 13:46:48 2017 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy	Sat Sep 23 20:09:16 2017 +0200
@@ -1000,7 +1000,7 @@
       and holf: "\<And>n::nat. \<F> n holomorphic_on S"
       and holg: "g holomorphic_on S"
       and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially"
-      and nonconst: "\<And>c. \<exists>z \<in> S. g z \<noteq> c"
+      and nonconst: "~ g constant_on S"
       and nz: "\<And>n z. z \<in> S \<Longrightarrow> \<F> n z \<noteq> 0"
       and "z0 \<in> S"
       shows "g z0 \<noteq> 0"
@@ -1164,14 +1164,14 @@
       and holf: "\<And>n::nat. \<F> n holomorphic_on S"
       and holg: "g holomorphic_on S"
       and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially"
-      and nonconst: "\<And>c. \<exists>z \<in> S. g z \<noteq> c"
+      and nonconst: "~ g constant_on S"
       and inj: "\<And>n. inj_on (\<F> n) S"
     shows "inj_on g S"
 proof -
   have False if z12: "z1 \<in> S" "z2 \<in> S" "z1 \<noteq> z2" "g z2 = g z1" for z1 z2
   proof -
     obtain z0 where "z0 \<in> S" and z0: "g z0 \<noteq> g z2"
-      using nonconst by blast
+      using constant_on_def nonconst by blast
     have "(\<lambda>z. g z - g z1) holomorphic_on S"
       by (intro holomorphic_intros holg)
     then obtain r where "0 < r" "ball z2 r \<subseteq> S" "\<And>z. dist z2 z < r \<and> z \<noteq> z2 \<Longrightarrow> g z \<noteq> g z1"
@@ -1214,7 +1214,8 @@
         show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e"
           by simp
       qed
-      show "\<And>c. \<exists>z\<in>S - {z1}. g z - g z1 \<noteq> c"
+      show "\<not> (\<lambda>z. g z - g z1) constant_on S - {z1}"
+        unfolding constant_on_def
         by (metis Diff_iff \<open>z0 \<in> S\<close> empty_iff insert_iff right_minus_eq z0 z12)
       show "\<And>n z. z \<in> S - {z1} \<Longrightarrow> \<F> n z - \<F> n z1 \<noteq> 0"
         by (metis DiffD1 DiffD2 eq_iff_diff_eq_0 inj inj_onD insertI1 \<open>z1 \<in> S\<close>)
@@ -1360,8 +1361,9 @@
           using \<open>Z \<subseteq> S\<close> e hol\<G> by force
         show "\<And>n z. z \<in> ball v e \<Longrightarrow> (\<G> \<circ> j) n z \<noteq> 0"
           using \<G>not0 \<open>Z \<subseteq> S\<close> e by fastforce
-        show "\<exists>z\<in>ball v e. h z \<noteq> c" for c
-        proof -
+        show "\<not> h constant_on ball v e"
+        proof (clarsimp simp: constant_on_def)
+          fix c
           have False if "\<And>z. dist v z < e \<Longrightarrow> h z = c"  
           proof -
             have "h v = c"
@@ -1389,7 +1391,7 @@
             show False
               using \<open>C < cmod (\<F> (j n) y)\<close> le_C not_less by blast
           qed
-          then show ?thesis by force
+          then show "\<exists>x\<in>ball v e. h x \<noteq> c" by force
         qed
         show "h holomorphic_on ball v e"
           by (simp add: holh)
@@ -1828,7 +1830,6 @@
     by meson
 qed
 
-
 corollary Casorati_Weierstrass:
   assumes "open M" "z \<in> M" "f holomorphic_on (M - {z})"
       and "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
diff -r cd8ad4eddb8a -r ebb97a834338 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Sat Sep 23 13:46:48 2017 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Sat Sep 23 20:09:16 2017 +0200
@@ -806,6 +806,75 @@
   qed
 qed
 
+lemma exposed_face_of_parallel:
+   "T exposed_face_of S \<longleftrightarrow>
+         T face_of S \<and>
+         (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b} \<and>
+                (T \<noteq> {} \<longrightarrow> T \<noteq> S \<longrightarrow> a \<noteq> 0) \<and>
+                (T \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. (w + a) \<in> affine hull S)))"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+  proof (clarsimp simp: exposed_face_of_def)
+    fix a b
+    assume faceS: "S \<inter> {x. a \<bullet> x = b} face_of S" and Ssub: "S \<subseteq> {x. a \<bullet> x \<le> b}" 
+    show "\<exists>c d. S \<subseteq> {x. c \<bullet> x \<le> d} \<and>
+                S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. c \<bullet> x = d} \<and>
+                (S \<inter> {x. a \<bullet> x = b} \<noteq> {} \<longrightarrow> S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> c \<noteq> 0) \<and>
+                (S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. w + c \<in> affine hull S))"
+    proof (cases "affine hull S \<inter> {x. -a \<bullet> x \<le> -b} = {} \<or> affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}")
+      case True
+      then show ?thesis
+      proof
+        assume "affine hull S \<inter> {x. - a \<bullet> x \<le> - b} = {}"
+       then show ?thesis
+         apply (rule_tac x="0" in exI)
+         apply (rule_tac x="1" in exI)
+         using hull_subset by fastforce
+    next
+      assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
+      then show ?thesis
+         apply (rule_tac x="0" in exI)
+         apply (rule_tac x="0" in exI)
+        using Ssub hull_subset by fastforce
+    qed
+  next
+    case False
+    then obtain a' b' where "a' \<noteq> 0" 
+      and le: "affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> {x. - a \<bullet> x \<le> - b}" 
+      and eq: "affine hull S \<inter> {x. a' \<bullet> x = b'} = affine hull S \<inter> {x. - a \<bullet> x = - b}" 
+      and mem: "\<And>w. w \<in> affine hull S \<Longrightarrow> w + a' \<in> affine hull S"
+      using affine_parallel_slice affine_affine_hull by metis 
+    show ?thesis
+    proof (intro conjI impI allI ballI exI)
+      have *: "S \<subseteq> - (affine hull S \<inter> {x. P x}) \<union> affine hull S \<inter> {x. Q x} \<Longrightarrow> S \<subseteq> {x. ~P x \<or> Q x}" 
+        for P Q 
+        using hull_subset by fastforce  
+      have "S \<subseteq> {x. ~ (a' \<bullet> x \<le> b') \<or> a' \<bullet> x = b'}"
+        apply (rule *)
+        apply (simp only: le eq)
+        using Ssub by auto
+      then show "S \<subseteq> {x. - a' \<bullet> x \<le> - b'}"
+        by auto 
+      show "S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. - a' \<bullet> x = - b'}"
+        using eq hull_subset [of S affine] by force
+      show "\<lbrakk>S \<inter> {x. a \<bullet> x = b} \<noteq> {}; S \<inter> {x. a \<bullet> x = b} \<noteq> S\<rbrakk> \<Longrightarrow> - a' \<noteq> 0"
+        using \<open>a' \<noteq> 0\<close> by auto
+      show "w + - a' \<in> affine hull S"
+        if "S \<inter> {x. a \<bullet> x = b} \<noteq> S" "w \<in> affine hull S" for w
+      proof -
+        have "w + 1 *\<^sub>R (w - (w + a')) \<in> affine hull S"
+          using affine_affine_hull mem mem_affine_3_minus that(2) by blast
+        then show ?thesis  by simp
+      qed
+    qed
+  qed
+qed
+next
+  assume ?rhs then show ?lhs
+    unfolding exposed_face_of_def by blast
+qed
+
 subsection\<open>Extreme points of a set: its singleton faces\<close>
 
 definition extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
diff -r cd8ad4eddb8a -r ebb97a834338 src/HOL/Library/Stirling.thy
--- a/src/HOL/Library/Stirling.thy	Sat Sep 23 13:46:48 2017 +0200
+++ b/src/HOL/Library/Stirling.thy	Sat Sep 23 20:09:16 2017 +0200
@@ -246,7 +246,7 @@
 \<close>
 
 definition zip_with_prev :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'b list"
-  where "zip_with_prev f x xs = map (\<lambda>(x,y). f x y) (zip (x # xs) xs)"
+  where "zip_with_prev f x xs = map2 f (x # xs) xs"
 
 lemma zip_with_prev_altdef:
   "zip_with_prev f x xs =
diff -r cd8ad4eddb8a -r ebb97a834338 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Sat Sep 23 13:46:48 2017 +0200
+++ b/src/HOL/Library/Tree.thy	Sat Sep 23 20:09:16 2017 +0200
@@ -475,6 +475,12 @@
 lemma height_mirror[simp]: "height(mirror t) = height t"
 by (induction t) simp_all
 
+lemma min_height_mirror [simp]: "min_height (mirror t) = min_height t"
+by (induction t) simp_all  
+
+lemma ipl_mirror [simp]: "ipl (mirror t) = ipl t"
+by (induction t) simp_all
+
 lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)"
 by (induction t) simp_all
 
diff -r cd8ad4eddb8a -r ebb97a834338 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Sep 23 13:46:48 2017 +0200
+++ b/src/HOL/List.thy	Sat Sep 23 20:09:16 2017 +0200
@@ -151,6 +151,9 @@
   \<comment> \<open>Warning: simpset does not contain this definition, but separate
        theorems for \<open>xs = []\<close> and \<open>xs = z # zs\<close>\<close>
 
+abbreviation map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
+"map2 f xs ys \<equiv> map (\<lambda>(x,y). f x y) (zip xs ys)"
+
 primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
 "product [] _ = []" |
 "product (x#xs) ys = map (Pair x) ys @ product xs ys"
@@ -2011,11 +2014,17 @@
 
 subsubsection \<open>@{const take} and @{const drop}\<close>
 
-lemma take_0 [simp]: "take 0 xs = []"
+lemma take_0: "take 0 xs = []"
+by (induct xs) auto
+
+lemma drop_0: "drop 0 xs = xs"
 by (induct xs) auto
 
-lemma drop_0 [simp]: "drop 0 xs = xs"
-by (induct xs) auto
+lemma take0[simp]: "take 0 = (\<lambda>xs. [])"
+by(rule ext) (rule take_0)
+
+lemma drop0[simp]: "drop 0 = (\<lambda>x. x)"
+by(rule ext) (rule drop_0)
 
 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
 by simp
@@ -2031,6 +2040,9 @@
 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
 by(cases xs, simp_all)
 
+lemma hd_take: "j > 0 \<Longrightarrow> hd (take j xs) = hd xs"
+by (metis gr0_conv_Suc list.sel(1) take.simps(1) take_Suc)
+
 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
 by (induct xs arbitrary: n) simp_all
 
@@ -4393,12 +4405,12 @@
 done
 
 lemma nths_shift_lemma:
-     "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
-      map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
+  "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
+   map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
 by (induct xs rule: rev_induct) (simp_all add: add.commute)
 
 lemma nths_append:
-     "nths (l @ l') A = nths l A @ nths l' {j. j + length l : A}"
+  "nths (l @ l') A = nths l A @ nths l' {j. j + length l : A}"
 apply (unfold nths_def)
 apply (induct l' rule: rev_induct, simp)
 apply (simp add: upt_add_eq_append[of 0] nths_shift_lemma)
@@ -4406,7 +4418,7 @@
 done
 
 lemma nths_Cons:
-"nths (x # l) A = (if 0:A then [x] else []) @ nths l {j. Suc j : A}"
+  "nths (x # l) A = (if 0:A then [x] else []) @ nths l {j. Suc j : A}"
 apply (induct l rule: rev_induct)
  apply (simp add: nths_def)
 apply (simp del: append_Cons add: append_Cons[symmetric] nths_append)
@@ -4429,17 +4441,18 @@
 lemma nths_singleton [simp]: "nths [x] A = (if 0 : A then [x] else [])"
 by (simp add: nths_Cons)
 
-
 lemma distinct_nthsI[simp]: "distinct xs \<Longrightarrow> distinct (nths xs I)"
-  by (induct xs arbitrary: I) (auto simp: nths_Cons)
-
+by (induct xs arbitrary: I) (auto simp: nths_Cons)
 
 lemma nths_upt_eq_take [simp]: "nths l {..<n} = take n l"
-  by (induct l rule: rev_induct)
-     (simp_all split: nat_diff_split add: nths_append)
+by (induct l rule: rev_induct)
+   (simp_all split: nat_diff_split add: nths_append)
+
+lemma filter_eq_nths: "filter P xs = nths xs {i. i<length xs \<and> P(xs!i)}"
+by(induction xs) (auto simp: nths_Cons)
 
 lemma filter_in_nths:
- "distinct xs \<Longrightarrow> filter (%x. x \<in> set (nths xs s)) xs = nths xs s"
+  "distinct xs \<Longrightarrow> filter (%x. x \<in> set (nths xs s)) xs = nths xs s"
 proof (induct xs arbitrary: s)
   case Nil thus ?case by simp
 next
@@ -5123,7 +5136,7 @@
 
 text\<open>Currently it is not shown that @{const sort} returns a
 permutation of its input because the nicest proof is via multisets,
-which are not yet available. Alternatively one could define a function
+which are not part of Main. Alternatively one could define a function
 that counts the number of occurrences of an element in a list and use
 that instead of multisets to state the correctness property.\<close>
 
@@ -5336,6 +5349,59 @@
   "sorted (map fst (enumerate n xs))"
   by (simp add: enumerate_eq_zip)
 
+text \<open>Stability of function @{const sort_key}:\<close>
+
+lemma sort_key_stable:
+  "x \<in> set xs \<Longrightarrow> [y <- sort_key f xs. f y = f x] = [y <- xs. f y = f x]"
+proof (induction xs arbitrary: x)
+  case Nil thus ?case by simp
+next  
+  case (Cons a xs)
+  thus ?case 
+  proof (cases "x \<in> set xs")
+    case True 
+    thus ?thesis
+    proof (cases "f a = f x")
+      case False thus ?thesis 
+        using Cons.IH by (metis (mono_tags) True filter.simps(2) filter_sort)
+    next
+      case True
+      hence ler: "[y <- (a # xs). f y = f x] = a # [y <- xs. f y = f a]" by simp
+      have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
+      hence "insort_key f a (sort_key f [y <- xs. f y = f a]) 
+              = a # (sort_key f [y <- xs. f y = f a])"
+        by (simp add: insort_is_Cons)
+      hence lel: "[y <- sort_key f (a # xs). f y = f x] = a # [y <- sort_key f xs. f y = f a]"
+        by (metis True filter_sort ler sort_key_simps(2))
+      from lel ler show ?thesis using Cons.IH \<open>x \<in> set xs\<close> by (metis True filter_sort)
+    qed
+  next
+    case False
+    from Cons.prems have "x = a" by (metis False set_ConsD)
+    have ler: "[y <- (a # xs). f y = f a] = a # [y <- xs. f y = f a]" by simp
+    have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
+    hence "insort_key f a (sort_key f [y <- xs. f y = f a]) 
+           = a # (sort_key f [y <- xs. f y = f a])"
+      by (simp add: insort_is_Cons)
+    hence lel: "[y <- sort_key f (a # xs). f y = f a] = a # [y <- sort_key f xs. f y = f a]"
+      by (metis (mono_tags) filter.simps(2) filter_sort sort_key_simps(2))
+    show ?thesis (is "?l = ?r")
+    proof (cases "f a \<in> set (map f xs)")
+      case False
+      hence "\<forall>y \<in> set xs. f y \<noteq> f a" by (metis image_eqI set_map)
+      hence R: "?r = [a]" using ler \<open>x=a\<close> by simp
+      have L: "?l = [a]" using lel \<open>x=a\<close> by (metis R filter_sort insort_key.simps(1) sort_key_simps)
+      from L R show ?thesis ..
+    next
+      case True
+      then obtain z where Z: "z \<in> set xs \<and> f z = f a" by auto
+      hence L: "[y <- sort_key f xs. f y = f z] = [y <- sort_key f xs. f y = f a]" by simp
+      from Z have R: "[y <- xs. f y = f z] = [y <- xs. f y = f a]" by simp 
+      from L R Z show ?thesis using Cons.IH ler lel \<open>x=a\<close> by metis
+    qed
+  qed
+qed
+
 
 subsubsection \<open>@{const transpose} on sorted lists\<close>
 
diff -r cd8ad4eddb8a -r ebb97a834338 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Sat Sep 23 13:46:48 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Sat Sep 23 20:09:16 2017 +0200
@@ -202,9 +202,13 @@
       (replay_data as {context = ctxt, ...} : SMT_Translate.replay_data) output =
     (case outcome output of
       (Unsat, lines) =>
-        if not (Config.get ctxt SMT_Config.oracle) andalso is_some replay0
-        then the replay0 outer_ctxt replay_data lines
-        else oracle ()
+        if Config.get ctxt SMT_Config.oracle then
+          oracle ()
+        else
+          (case replay0 of
+            SOME replay => replay outer_ctxt replay_data lines
+          | NONE => error "No proof reconstruction for solver -- \
+            \declare [[smt_oracle]] to allow oracle")
     | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat)))
 
   val cfalse = Thm.cterm_of @{context} @{prop False}