--- a/NEWS Wed Aug 23 19:54:11 2017 +0100
+++ b/NEWS Wed Aug 23 19:54:30 2017 +0100
@@ -215,6 +215,9 @@
* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
+* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"
+filter for describing points x such that f(x) is in the filter F.
+
* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
space. INCOMPATIBILITY.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Base_FDS.thy Wed Aug 23 19:54:30 2017 +0100
@@ -0,0 +1,22 @@
+theory Base_FDS
+imports "../Library/Pattern_Aliases"
+begin
+
+declare Let_def [simp]
+
+text \<open>Lemma \<open>size_prod_measure\<close>, when declared with the \<open>measure_function\<close> attribute,
+enables \<open>fun\<close> to prove termination of a larger class of functions automatically.
+By default, \<open>fun\<close> only tries lexicographic combinations of the sizes of the parameters.
+With \<open>size_prod_measure\<close> enabled it also tries measures based on the sum of the sizes
+of different parameters.
+
+To alert the reader whenever such a more subtle termination proof is taking place
+the lemma is not enabled all the time but only locally in a \<open>context\<close> block
+around such function definitions.
+\<close>
+
+lemma size_prod_measure:
+ "is_measure f \<Longrightarrow> is_measure g \<Longrightarrow> is_measure (size_prod f g)"
+by (rule is_measure_trivial)
+
+end
\ No newline at end of file
--- a/src/HOL/Data_Structures/Binomial_Heap.thy Wed Aug 23 19:54:11 2017 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Wed Aug 23 19:54:30 2017 +0100
@@ -4,13 +4,11 @@
theory Binomial_Heap
imports
+ Base_FDS
Complex_Main
Priority_Queue
begin
-lemma sum_power2: "(\<Sum>i\<in>{0..<k}. (2::nat)^i) = 2^k-1"
-by (induction k) auto
-
text \<open>
We formalize the binomial heap presentation from Okasaki's book.
We show the functional correctness and complexity of all operations.
@@ -96,7 +94,7 @@
"link t\<^sub>1 t\<^sub>2 = (case (t\<^sub>1,t\<^sub>2) of (Node r x\<^sub>1 c\<^sub>1, Node _ x\<^sub>2 c\<^sub>2) \<Rightarrow>
if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#c\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#c\<^sub>2)
)"
-
+
lemma link_invar_btree:
assumes "invar_btree t\<^sub>1"
assumes "invar_btree t\<^sub>2"
@@ -104,7 +102,7 @@
shows "invar_btree (link t\<^sub>1 t\<^sub>2)"
using assms
unfolding link_def
- by (force split: tree.split )
+ by (force split: tree.split)
lemma link_otree_invar:
assumes "otree_invar t\<^sub>1"
@@ -179,17 +177,17 @@
lemma ins_mset[simp]: "mset_heap (ins x t) = {#x#} + mset_heap t"
unfolding ins_def
- by auto
-
+ by auto
+
fun merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
"merge ts\<^sub>1 [] = ts\<^sub>1"
| "merge [] ts\<^sub>2 = ts\<^sub>2"
| "merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = (
- if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2)
- else if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2#merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2
+ if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1 # merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2) else
+ if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2 # merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2
else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)
- )"
-
+ )"
+
lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2" by (cases ts\<^sub>2) auto
lemma merge_rank_bound:
@@ -281,7 +279,7 @@
using assms
apply (induction ts arbitrary: x rule: find_min.induct)
apply (auto
- simp: Let_def otree_invar_root_min intro: order_trans;
+ simp: otree_invar_root_min intro: order_trans;
meson linear order_trans otree_invar_root_min
)+
done
@@ -300,7 +298,7 @@
shows "find_min ts \<in># mset_heap ts"
using assms
apply (induction ts rule: find_min.induct)
- apply (auto simp: Let_def)
+ apply (auto)
done
lemma find_min:
@@ -323,8 +321,8 @@
shows "root t' = find_min ts"
using assms
apply (induction ts arbitrary: t' ts' rule: find_min.induct)
- apply (auto simp: Let_def split: prod.splits)
- done
+ apply (auto split: prod.splits)
+ done
lemma get_min_mset:
assumes "get_min ts = (t',ts')"
--- a/src/HOL/Data_Structures/Leftist_Heap.thy Wed Aug 23 19:54:11 2017 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy Wed Aug 23 19:54:30 2017 +0100
@@ -4,15 +4,13 @@
theory Leftist_Heap
imports
+ Base_FDS
Tree2
Priority_Queue
Complex_Main
begin
-(* FIXME mv Base *)
-lemma size_prod_measure[measure_function]:
- "is_measure f \<Longrightarrow> is_measure g \<Longrightarrow> is_measure (size_prod f g)"
-by (rule is_measure_trivial)
+unbundle pattern_aliases
fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
"mset_tree Leaf = {#}" |
@@ -48,12 +46,16 @@
fun get_min :: "'a lheap \<Rightarrow> 'a" where
"get_min(Node n l a r) = a"
-fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
+text\<open>Explicit termination argument: sum of sizes\<close>
+
+function merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
"merge Leaf t2 = t2" |
"merge t1 Leaf = t1" |
-"merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
- (if a1 \<le> a2 then node l1 a1 (merge r1 (Node n2 l2 a2 r2))
- else node l2 a2 (merge r2 (Node n1 l1 a1 r1)))"
+"merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
+ (if a1 \<le> a2 then node l1 a1 (merge r1 t2)
+ else node l2 a2 (merge r2 t1))"
+by pat_completeness auto
+termination by (relation "measure (\<lambda>(t1,t2). size t1 + size t2)") auto
lemma merge_code: "merge t1 t2 = (case (t1,t2) of
(Leaf, _) \<Rightarrow> t2 |
@@ -72,9 +74,6 @@
subsection "Lemmas"
-(* FIXME mv DS_Base *)
-declare Let_def [simp]
-
lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
by(cases t) auto
@@ -179,12 +178,16 @@
finally show ?case .
qed
-fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
+text\<open>Explicit termination argument: sum of sizes\<close>
+
+function t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
"t_merge Leaf t2 = 1" |
"t_merge t2 Leaf = 1" |
-"t_merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
- (if a1 \<le> a2 then 1 + t_merge r1 (Node n2 l2 a2 r2)
- else 1 + t_merge r2 (Node n1 l1 a1 r1))"
+"t_merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
+ (if a1 \<le> a2 then 1 + t_merge r1 t2
+ else 1 + t_merge r2 t1)"
+by pat_completeness auto
+termination by (relation "measure (\<lambda>(t1,t2). size t1 + size t2)") auto
definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
"t_insert x t = t_merge (Node 1 Leaf x Leaf) t"
@@ -209,7 +212,7 @@
using t_merge_log[of "Node 1 Leaf x Leaf" t]
by(simp add: t_insert_def split: tree.split)
-(* FIXME mv Lemmas_log *)
+(* FIXME mv ? *)
lemma ld_ld_1_less:
assumes "x > 0" "y > 0" shows "log 2 x + log 2 y + 1 < 2 * log 2 (x+y)"
proof -
@@ -218,7 +221,7 @@
also have "\<dots> < (x+y)^2" using assms
by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)
also have "\<dots> = 2 powr (2 * log 2 (x+y))"
- using assms by(simp add: powr_add log_powr[symmetric] powr_numeral)
+ using assms by(simp add: powr_add log_powr[symmetric])
finally show ?thesis by simp
qed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Going_To_Filter.thy Wed Aug 23 19:54:30 2017 +0100
@@ -0,0 +1,124 @@
+(*
+ File: Going_To_Filter.thy
+ Author: Manuel Eberl, TU München
+
+ A filter describing the points x such that f(x) tends to some other filter.
+*)
+section \<open>The `going\_to' filter\<close>
+theory Going_To_Filter
+ imports Complex_Main
+begin
+
+definition going_to_within :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a set \<Rightarrow> 'a filter"
+ ("(_)/ going'_to (_)/ within (_)" [1000,60,60] 60) where
+ "f going_to F within A = inf (filtercomap f F) (principal A)"
+
+abbreviation going_to :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter"
+ (infix "going'_to" 60)
+ where "f going_to F \<equiv> f going_to F within UNIV"
+
+text \<open>
+ The `going\_to' filter is, in a sense, the opposite of @{term filtermap}.
+ It corresponds to the intuition of, given a function $f: A \to B$ and a filter $F$ on the
+ range of $B$, looking at such values of $x$ that $f(x)$ approaches $F$. This can be
+ written as @{term "f going_to F"}.
+
+ A classic example is the @{term "at_infinity"} filter, which describes the neigbourhood
+ of infinity (i.\,e.\ all values sufficiently far away from the zero). This can also be written
+ as @{term "norm going_to at_top"}.
+
+ Additionally, the `going\_to' filter can be restricted with an optional `within' parameter.
+ For instance, if one would would want to consider the filter of complex numbers near infinity
+ that do not lie on the negative real line, one could write
+ @{term "norm going_to at_top within - complex_of_real ` {..0}"}.
+
+ A third, less mathematical example lies in the complexity analysis of algorithms.
+ Suppose we wanted to say that an algorithm on lists takes $O(n^2)$ time where $n$ is
+ the length of the input list. We can write this using the Landau symbols from the AFP,
+ where the underlying filter is @{term "length going_to at_top"}. If, on the other hand,
+ we want to look the complexity of the algorithm on sorted lists, we could use the filter
+ @{term "length going_to at_top within {xs. sorted xs}"}.
+\<close>
+
+lemma going_to_def: "f going_to F = filtercomap f F"
+ by (simp add: going_to_within_def)
+
+lemma eventually_going_toI [intro]:
+ assumes "eventually P F"
+ shows "eventually (\<lambda>x. P (f x)) (f going_to F)"
+ using assms by (auto simp: going_to_def)
+
+lemma filterlim_going_toI_weak [intro]: "filterlim f F (f going_to F within A)"
+ unfolding going_to_within_def
+ by (meson filterlim_filtercomap filterlim_iff inf_le1 le_filter_def)
+
+lemma going_to_mono: "F \<le> G \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f going_to F within A \<le> f going_to G within B"
+ unfolding going_to_within_def by (intro inf_mono filtercomap_mono) simp_all
+
+lemma going_to_inf:
+ "f going_to (inf F G) within A = inf (f going_to F within A) (f going_to G within A)"
+ by (simp add: going_to_within_def filtercomap_inf inf_assoc inf_commute inf_left_commute)
+
+lemma going_to_sup:
+ "f going_to (sup F G) within A \<ge> sup (f going_to F within A) (f going_to G within A)"
+ by (auto simp: going_to_within_def intro!: inf.coboundedI1 filtercomap_sup filtercomap_mono)
+
+lemma going_to_top [simp]: "f going_to top within A = principal A"
+ by (simp add: going_to_within_def)
+
+lemma going_to_bot [simp]: "f going_to bot within A = bot"
+ by (simp add: going_to_within_def)
+
+lemma going_to_principal:
+ "f going_to principal A within B = principal (f -` A \<inter> B)"
+ by (simp add: going_to_within_def)
+
+lemma going_to_within_empty [simp]: "f going_to F within {} = bot"
+ by (simp add: going_to_within_def)
+
+lemma going_to_within_union [simp]:
+ "f going_to F within (A \<union> B) = sup (f going_to F within A) (f going_to F within B)"
+ by (simp add: going_to_within_def inf_sup_distrib1 [symmetric])
+
+lemma eventually_going_to_at_top_linorder:
+ fixes f :: "'a \<Rightarrow> 'b :: linorder"
+ shows "eventually P (f going_to at_top within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x \<ge> C \<longrightarrow> P x)"
+ unfolding going_to_within_def eventually_filtercomap
+ eventually_inf_principal eventually_at_top_linorder by fast
+
+lemma eventually_going_to_at_bot_linorder:
+ fixes f :: "'a \<Rightarrow> 'b :: linorder"
+ shows "eventually P (f going_to at_bot within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x \<le> C \<longrightarrow> P x)"
+ unfolding going_to_within_def eventually_filtercomap
+ eventually_inf_principal eventually_at_bot_linorder by fast
+
+lemma eventually_going_to_at_top_dense:
+ fixes f :: "'a \<Rightarrow> 'b :: {linorder,no_top}"
+ shows "eventually P (f going_to at_top within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x > C \<longrightarrow> P x)"
+ unfolding going_to_within_def eventually_filtercomap
+ eventually_inf_principal eventually_at_top_dense by fast
+
+lemma eventually_going_to_at_bot_dense:
+ fixes f :: "'a \<Rightarrow> 'b :: {linorder,no_bot}"
+ shows "eventually P (f going_to at_bot within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x < C \<longrightarrow> P x)"
+ unfolding going_to_within_def eventually_filtercomap
+ eventually_inf_principal eventually_at_bot_dense by fast
+
+lemma eventually_going_to_nhds:
+ "eventually P (f going_to nhds a within A) \<longleftrightarrow>
+ (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>A. f x \<in> S \<longrightarrow> P x))"
+ unfolding going_to_within_def eventually_filtercomap eventually_inf_principal
+ eventually_nhds by fast
+
+lemma eventually_going_to_at:
+ "eventually P (f going_to (at a within B) within A) \<longleftrightarrow>
+ (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>A. f x \<in> B \<inter> S - {a} \<longrightarrow> P x))"
+ unfolding at_within_def going_to_inf eventually_inf_principal
+ eventually_going_to_nhds going_to_principal by fast
+
+lemma norm_going_to_at_top_eq: "norm going_to at_top = at_infinity"
+ by (simp add: eventually_at_infinity eventually_going_to_at_top_linorder filter_eq_iff)
+
+lemmas at_infinity_altdef = norm_going_to_at_top_eq [symmetric]
+
+end
--- a/src/HOL/Library/Library.thy Wed Aug 23 19:54:11 2017 +0100
+++ b/src/HOL/Library/Library.thy Wed Aug 23 19:54:30 2017 +0100
@@ -30,6 +30,7 @@
Function_Division
Function_Growth
Fun_Lexorder
+ Going_To_Filter
Groups_Big_Fun
Indicator_Function
Infinite_Set
--- a/src/HOL/Set_Interval.thy Wed Aug 23 19:54:11 2017 +0100
+++ b/src/HOL/Set_Interval.thy Wed Aug 23 19:54:30 2017 +0100
@@ -1894,6 +1894,9 @@
subsection \<open>The formula for geometric sums\<close>
+lemma sum_power2: "(\<Sum>i=0..<k. (2::nat)^i) = 2^k-1"
+by (induction k) (auto simp: mult_2)
+
lemma geometric_sum:
assumes "x \<noteq> 1"
shows "(\<Sum>i<n. x ^ i) = (x ^ n - 1) / (x - 1::'a::field)"