--- 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
-----------------------------
--- 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)
----------------------------------
--- 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'"
--- 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)"
--- 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"
--- 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 =
--- 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
--- 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>
--- 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}