--- a/NEWS Wed Mar 27 17:39:28 2024 +0100
+++ b/NEWS Wed Mar 27 17:39:46 2024 +0100
@@ -61,6 +61,9 @@
"preplay_timeout". INCOMPATIBILITY.
- Added the action "order" testing the proof method of the same name.
+* HOL-ex.Sketch_and_Explore: improvements to generate more natural and
+readable proof sketches from proof states.
+
* Explicit type class for discrete_linear_ordered_semidom for integral
semidomains with a discrete linear order.
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Mar 27 17:39:28 2024 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Mar 27 17:39:46 2024 +0100
@@ -2439,6 +2439,51 @@
\<Longrightarrow> setdist {x} S > 0"
using less_eq_real_def setdist_eq_0_closedin by fastforce
+text \<open>A consequence of the results above\<close>
+lemma compact_minkowski_sum_cball:
+ fixes A :: "'a :: heine_borel set"
+ assumes "compact A"
+ shows "compact (\<Union>x\<in>A. cball x r)"
+proof (cases "A = {}")
+ case False
+ show ?thesis
+ unfolding compact_eq_bounded_closed
+ proof safe
+ have "open (-(\<Union>x\<in>A. cball x r))"
+ unfolding open_dist
+ proof safe
+ fix x assume x: "x \<notin> (\<Union>x\<in>A. cball x r)"
+ have "\<exists>x'\<in>{x}. \<exists>y\<in>A. dist x' y = setdist {x} A"
+ using \<open>A \<noteq> {}\<close> assms
+ by (intro setdist_compact_closed) (auto simp: compact_imp_closed)
+ then obtain y where y: "y \<in> A" "dist x y = setdist {x} A"
+ by blast
+ with x have "setdist {x} A > r"
+ by (auto simp: dist_commute)
+ moreover have "False" if "dist z x < setdist {x} A - r" "u \<in> A" "z \<in> cball u r" for z u
+ by (smt (verit, del_insts) mem_cball setdist_Lipschitz setdist_sing_in_set that)
+ ultimately
+ show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> - (\<Union>x\<in>A. cball x r)"
+ by (force intro!: exI[of _ "setdist {x} A - r"])
+ qed
+ thus "closed (\<Union>x\<in>A. cball x r)"
+ using closed_open by blast
+ next
+ from assms have "bounded A"
+ by (simp add: compact_imp_bounded)
+ then obtain x c where c: "\<And>y. y \<in> A \<Longrightarrow> dist x y \<le> c"
+ unfolding bounded_def by blast
+ have "\<forall>y\<in>(\<Union>x\<in>A. cball x r). dist x y \<le> c + r"
+ proof safe
+ fix y z assume *: "y \<in> A" "z \<in> cball y r"
+ thus "dist x z \<le> c + r"
+ using * c[of y] cball_trans mem_cball by blast
+ qed
+ thus "bounded (\<Union>x\<in>A. cball x r)"
+ unfolding bounded_def by blast
+ qed
+qed auto
+
no_notation
eucl_less (infix "<e" 50)
--- a/src/HOL/Data_Structures/Array_Braun.thy Wed Mar 27 17:39:28 2024 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy Wed Mar 27 17:39:46 2024 +0100
@@ -3,9 +3,10 @@
section "Arrays via Braun Trees"
theory Array_Braun
- imports
- Array_Specs
- Braun_Tree
+imports
+ Time_Funs
+ Array_Specs
+ Braun_Tree
begin
subsection "Array"
@@ -443,13 +444,6 @@
definition brauns1 :: "'a list \<Rightarrow> 'a tree" where
"brauns1 xs = (if xs = [] then Leaf else brauns 0 xs ! 0)"
-fun T_brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
- "T_brauns k xs = (if xs = [] then 0 else
- let ys = take (2^k) xs;
- zs = drop (2^k) xs;
- ts = brauns (k+1) zs
- in 4 * min (2^k) (length xs) + T_brauns (k+1) zs)"
-
paragraph "Functional correctness"
@@ -497,8 +491,28 @@
paragraph "Running Time Analysis"
-theorem T_brauns:
- "T_brauns k xs = 4 * length xs"
+time_fun_0 "(^)"
+
+time_fun nodes
+
+lemma T_nodes: "T_nodes ls xs rs = length xs + 1"
+by(induction ls xs rs rule: T_nodes.induct) auto
+
+time_fun brauns
+
+lemma T_brauns_pretty: "T_brauns k xs = (if xs = [] then 0 else
+ let ys = take (2^k) xs;
+ zs = drop (2^k) xs;
+ ts = brauns (k+1) zs
+ in T_take (2 ^ k) xs + T_drop (2 ^ k) xs + T_brauns (k + 1) zs + T_drop (2 ^ k) ts + T_nodes ts ys (drop (2 ^ k) ts)) + 1"
+by(simp)
+
+lemma T_brauns_simple: "T_brauns k xs = (if xs = [] then 0 else
+ 3 * (min (2^k) (length xs) + 1) + (min (2^k) (length xs - 2^k) + 1) + T_brauns (k+1) (drop (2^k) xs)) + 1"
+by(simp add: T_nodes T_take_eq T_drop_eq length_brauns min_def)
+
+theorem T_brauns_ub:
+ "T_brauns k xs \<le> 9 * (length xs + 1)"
proof (induction xs arbitrary: k rule: measure_induct_rule[where f = length])
case (less xs)
show ?case
@@ -507,15 +521,28 @@
thus ?thesis by(simp)
next
assume "xs \<noteq> []"
- let ?zs = "drop (2^k) xs"
- have "T_brauns k xs = T_brauns (k+1) ?zs + 4 * min (2^k) (length xs)"
- using \<open>xs \<noteq> []\<close> by(simp)
- also have "\<dots> = 4 * length ?zs + 4 * min (2^k) (length xs)"
+ let ?n = "length xs" let ?zs = "drop (2^k) xs"
+ have *: "?n - 2^k + 1 \<le> ?n"
+ using \<open>xs \<noteq> []\<close> less_eq_Suc_le by fastforce
+ have "T_brauns k xs =
+ 3 * (min (2^k) ?n + 1) + (min (2^k) (?n - 2^k) + 1) + T_brauns (k+1) ?zs + 1"
+ unfolding T_brauns_simple[of k xs] using \<open>xs \<noteq> []\<close> by(simp del: T_brauns.simps)
+ also have "\<dots> \<le> 4 * min (2^k) ?n + T_brauns (k+1) ?zs + 5"
+ by(simp add: min_def)
+ also have "\<dots> \<le> 4 * min (2^k) ?n + 9 * (length ?zs + 1) + 5"
using less[of ?zs "k+1"] \<open>xs \<noteq> []\<close>
- by (simp)
- also have "\<dots> = 4 * length xs"
+ by (simp del: T_brauns.simps)
+ also have "\<dots> = 4 * min (2^k) ?n + 9 * (?n - 2^k + 1) + 5"
+ by(simp)
+ also have "\<dots> = 4 * min (2^k) ?n + 4 * (?n - 2^k) + 5 * (?n - 2^k + 1) + 9"
by(simp)
- finally show ?case .
+ also have "\<dots> = 4 * ?n + 5 * (?n - 2^k + 1) + 9"
+ by(simp)
+ also have "\<dots> \<le> 4 * ?n + 5 * ?n + 9"
+ using * by(simp)
+ also have "\<dots> = 9 * (?n + 1)"
+ by (simp add: Suc_leI)
+ finally show ?thesis .
qed
qed
@@ -551,17 +578,53 @@
definition list_fast :: "'a tree \<Rightarrow> 'a list" where
"list_fast t = list_fast_rec [t]"
-function T_list_fast_rec :: "'a tree list \<Rightarrow> nat" where
+(* TODO: map and filter are a problem!
+- The automatically generated T_map is slightly more complicated than needed.
+- We cannot use the manually defined T_map directly because the automatic translation
+ assumes that T_map has a more complicated type and generates a "wrong" call.
+Therefore we hide map/filter at the moment.
+*)
+
+definition "filter_not_Leaf = filter (\<lambda>t. t \<noteq> Leaf)"
+
+definition "map_left = map left"
+definition "map_right = map right"
+definition "map_value = map value"
+
+definition "T_filter_not_Leaf ts = length ts + 1"
+definition "T_map_left ts = length ts + 1"
+definition "T_map_right ts = length ts + 1"
+definition "T_map_value ts = length ts + 1"
+(*
+time_fun "tree.value"
+time_fun "left"
+time_fun "right"
+*)
+
+lemmas defs = filter_not_Leaf_def map_left_def map_right_def map_value_def
+ T_filter_not_Leaf_def T_map_value_def T_map_left_def T_map_right_def
+
+(* A variant w/o explicit map/filter; T_list_fast_rec is generated from it *)
+lemma list_fast_rec_simp:
+"list_fast_rec ts = (let us = filter_not_Leaf ts in
+ if us = [] then [] else
+ map_value us @ list_fast_rec (map_left us @ map_right us))"
+unfolding defs list_fast_rec.simps[of ts] by(rule refl)
+
+time_function list_fast_rec equations list_fast_rec_simp
+termination
+ by (relation "measure (sum_list o map size)"; simp add: list_fast_rec_term defs)
+
+lemma T_list_fast_rec_pretty:
"T_list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts
- in length ts + (if us = [] then 0 else
- 5 * length us + T_list_fast_rec (map left us @ map right us)))"
- by (pat_completeness, auto)
-
-termination
- by (relation "measure (sum_list o map size)"; simp add: list_fast_rec_term)
+ in length ts + 1 + (if us = [] then 0 else
+ 5 * (length us + 1) + T_list_fast_rec (map left us @ map right us))) + 1"
+unfolding defs T_list_fast_rec.simps[of ts]
+by(simp add: T_append)
declare T_list_fast_rec.simps[simp del]
+
paragraph "Functional Correctness"
lemma list_fast_rec_all_Leaf:
@@ -624,6 +687,7 @@
"braun t \<Longrightarrow> list_fast t = list t"
by (simp add: list_fast_def take_nths_00 braun_list_eq list_fast_rec_correct[where k=0])
+
paragraph "Running Time Analysis"
lemma sum_tree_list_children: "\<forall>t \<in> set ts. t \<noteq> Leaf \<Longrightarrow>
@@ -631,7 +695,7 @@
by(induction ts)(auto simp add: neq_Leaf_iff algebra_simps)
theorem T_list_fast_rec_ub:
- "T_list_fast_rec ts \<le> sum_list (map (\<lambda>t. 7*size t + 1) ts)"
+ "T_list_fast_rec ts \<le> sum_list (map (\<lambda>t. 14*size t + 1) ts) + 2"
proof (induction ts rule: measure_induct_rule[where f="sum_list o map size"])
case (less ts)
let ?us = "filter (\<lambda>t. t \<noteq> Leaf) ts"
@@ -639,22 +703,26 @@
proof cases
assume "?us = []"
thus ?thesis using T_list_fast_rec.simps[of ts]
- by(simp add: sum_list_Suc)
+ by(simp add: defs sum_list_Suc)
next
assume "?us \<noteq> []"
let ?children = "map left ?us @ map right ?us"
- have "T_list_fast_rec ts = T_list_fast_rec ?children + 5 * length ?us + length ts"
- using \<open>?us \<noteq> []\<close> T_list_fast_rec.simps[of ts] by(simp)
- also have "\<dots> \<le> (\<Sum>t\<leftarrow>?children. 7 * size t + 1) + 5 * length ?us + length ts"
+ have 1: "1 \<le> length ?us"
+ using \<open>?us \<noteq> []\<close> linorder_not_less by auto
+ have "T_list_fast_rec ts = T_list_fast_rec ?children + 5 * length ?us + length ts + 7"
+ using \<open>?us \<noteq> []\<close> T_list_fast_rec.simps[of ts] by(simp add: defs T_append)
+ also have "\<dots> \<le> (\<Sum>t\<leftarrow>?children. 14 * size t + 1) + 5 * length ?us + length ts + 9"
using less[of "?children"] list_fast_rec_term[of "?us"] \<open>?us \<noteq> []\<close>
by (simp)
- also have "\<dots> = (\<Sum>t\<leftarrow>?children. 7*size t) + 7 * length ?us + length ts"
+ also have "\<dots> = (\<Sum>t\<leftarrow>?children. 14 * size t) + 7 * length ?us + length ts + 9"
by(simp add: sum_list_Suc o_def)
- also have "\<dots> = (\<Sum>t\<leftarrow>?us. 7*size t) + length ts"
+ also have "\<dots> \<le> (\<Sum>t\<leftarrow>?children. 14 * size t) + 14 * length ?us + length ts + 2"
+ using 1 by(simp add: sum_list_Suc o_def)
+ also have "\<dots> = (\<Sum>t\<leftarrow>?us. 14 * size t) + length ts + 2"
by(simp add: sum_tree_list_children)
- also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 7*size t) + length ts"
+ also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 14 * size t) + length ts + 2"
by(simp add: sum_list_filter_le_nat)
- also have "\<dots> = (\<Sum>t\<leftarrow>ts. 7 * size t + 1)"
+ also have "\<dots> = (\<Sum>t\<leftarrow>ts. 14 * size t + 1) + 2"
by(simp add: sum_list_Suc)
finally show ?case .
qed
--- a/src/HOL/Data_Structures/Define_Time_Function.ML Wed Mar 27 17:39:28 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML Wed Mar 27 17:39:46 2024 +0100
@@ -353,7 +353,9 @@
(* The converter for timing functions given to the walker *)
val converter : term option converter = {
- constc = fn _ => fn _ => fn _ => fn _ => NONE,
+ constc = fn _ => fn _ => fn _ => fn t =>
+ (case t of Const ("HOL.undefined", _) => SOME (Const ("HOL.undefined", @{typ "nat"}))
+ | _ => NONE),
funcc = funcc,
ifc = ifc,
casec = casec,
--- a/src/HOL/Data_Structures/Time_Funs.thy Wed Mar 27 17:39:28 2024 +0100
+++ b/src/HOL/Data_Structures/Time_Funs.thy Wed Mar 27 17:39:46 2024 +0100
@@ -7,6 +7,11 @@
imports Define_Time_Function
begin
+time_fun "(@)"
+
+lemma T_append: "T_append xs ys = length xs + 1"
+by(induction xs) auto
+
text \<open>Automatic definition of \<open>T_length\<close> is cumbersome because of the type class for \<open>size\<close>.\<close>
fun T_length :: "'a list \<Rightarrow> nat" where
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Mar 27 17:39:28 2024 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Mar 27 17:39:46 2024 +0100
@@ -390,26 +390,6 @@
"DERIV_floatarith x (Num f) = Num 0" |
"DERIV_floatarith x (Var n) = (if x = n then Num 1 else Num 0)"
-lemma has_real_derivative_powr':
- fixes f g :: "real \<Rightarrow> real"
- assumes "(f has_real_derivative f') (at x)"
- assumes "(g has_real_derivative g') (at x)"
- assumes "f x > 0"
- defines "h \<equiv> \<lambda>x. f x powr g x * (g' * ln (f x) + f' * g x / f x)"
- shows "((\<lambda>x. f x powr g x) has_real_derivative h x) (at x)"
-proof (subst DERIV_cong_ev[OF refl _ refl])
- from assms have "isCont f x"
- by (simp add: DERIV_continuous)
- hence "f \<midarrow>x\<rightarrow> f x" by (simp add: continuous_at)
- with \<open>f x > 0\<close> have "eventually (\<lambda>x. f x > 0) (nhds x)"
- by (auto simp: tendsto_at_iff_tendsto_nhds dest: order_tendstoD)
- thus "eventually (\<lambda>x. f x powr g x = exp (g x * ln (f x))) (nhds x)"
- by eventually_elim (simp add: powr_def)
-next
- from assms show "((\<lambda>x. exp (g x * ln (f x))) has_real_derivative h x) (at x)"
- by (auto intro!: derivative_eq_intros simp: h_def powr_def)
-qed
-
lemma DERIV_floatarith:
assumes "n < length vs"
assumes isDERIV: "isDERIV n f (vs[n := x])"
--- a/src/HOL/Probability/Information.thy Wed Mar 27 17:39:28 2024 +0100
+++ b/src/HOL/Probability/Information.thy Wed Mar 27 17:39:46 2024 +0100
@@ -857,7 +857,7 @@
using int X by (intro entropy_le) auto
also have "\<dots> \<le> log b (measure MX (space MX))"
using Px distributed_imp_emeasure_nonzero[OF X]
- by (intro log_le)
+ by (intro Transcendental.log_mono)
(auto intro!: finite_measure_mono b_gt_1 less_le[THEN iffD2]
simp: emeasure_eq_measure cong: conj_cong)
finally show ?thesis .
@@ -1087,7 +1087,7 @@
done
have "- log b 1 \<le> - log b (integral\<^sup>L ?P ?f)"
- proof (intro le_imp_neg_le log_le[OF b_gt_1])
+ proof (intro le_imp_neg_le Transcendental.log_mono[OF b_gt_1])
have If: "integrable ?P ?f"
unfolding real_integrable_def
proof (intro conjI)
@@ -1332,7 +1332,7 @@
by (auto simp: split_beta')
have "- log b 1 \<le> - log b (integral\<^sup>L ?P ?f)"
- proof (intro le_imp_neg_le log_le[OF b_gt_1])
+ proof (intro le_imp_neg_le Transcendental.log_mono[OF b_gt_1])
have If: "integrable ?P ?f"
using neg fin by (force simp add: real_integrable_def)
then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Mar 27 17:39:28 2024 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Mar 27 17:39:46 2024 +0100
@@ -473,7 +473,7 @@
using entropy_le_card[of "t\<circ>OB", OF simple_distributedI[OF simple_function_finite _ refl]] by simp
also have "\<dots> \<le> log b (real (n + 1)^card observations)"
using card_T_bound not_empty
- by (auto intro!: log_le simp: card_gt_0_iff of_nat_power [symmetric] simp del: of_nat_power of_nat_Suc)
+ by (auto intro!: log_mono simp: card_gt_0_iff of_nat_power [symmetric] simp del: of_nat_power of_nat_Suc)
also have "\<dots> = real (card observations) * log b (real n + 1)"
by (simp add: log_nat_power add.commute)
finally show ?thesis .
--- a/src/HOL/Transcendental.thy Wed Mar 27 17:39:28 2024 +0100
+++ b/src/HOL/Transcendental.thy Wed Mar 27 17:39:46 2024 +0100
@@ -2665,7 +2665,7 @@
lemma log_le_cancel_iff [simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a x \<le> log a y \<longleftrightarrow> x \<le> y"
by (simp flip: linorder_not_less)
-lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
+lemma log_mono: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
by simp
lemma log_less: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x < y \<Longrightarrow> log a x < log a y"
@@ -3201,6 +3201,27 @@
declare has_real_derivative_powr[THEN DERIV_chain2, derivative_intros]
+text \<open>A more general version, by Johannes Hölzl\<close>
+lemma has_real_derivative_powr':
+ fixes f g :: "real \<Rightarrow> real"
+ assumes "(f has_real_derivative f') (at x)"
+ assumes "(g has_real_derivative g') (at x)"
+ assumes "f x > 0"
+ defines "h \<equiv> \<lambda>x. f x powr g x * (g' * ln (f x) + f' * g x / f x)"
+ shows "((\<lambda>x. f x powr g x) has_real_derivative h x) (at x)"
+proof (subst DERIV_cong_ev[OF refl _ refl])
+ from assms have "isCont f x"
+ by (simp add: DERIV_continuous)
+ hence "f \<midarrow>x\<rightarrow> f x" by (simp add: continuous_at)
+ with \<open>f x > 0\<close> have "eventually (\<lambda>x. f x > 0) (nhds x)"
+ by (auto simp: tendsto_at_iff_tendsto_nhds dest: order_tendstoD)
+ thus "eventually (\<lambda>x. f x powr g x = exp (g x * ln (f x))) (nhds x)"
+ by eventually_elim (simp add: powr_def)
+next
+ from assms show "((\<lambda>x. exp (g x * ln (f x))) has_real_derivative h x) (at x)"
+ by (auto intro!: derivative_eq_intros simp: h_def powr_def)
+qed
+
lemma tendsto_zero_powrI:
assumes "(f \<longlongrightarrow> (0::real)) F" "(g \<longlongrightarrow> b) F" "\<forall>\<^sub>F x in F. 0 \<le> f x" "0 < b"
shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> 0) F"