--- a/CONTRIBUTORS Mon May 21 22:52:16 2018 +0100
+++ b/CONTRIBUTORS Tue May 22 19:58:17 2018 +0100
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* May 2018: Manuel Eberl
+ Landau symbols and asymptotic equivalence (moved from the AFP)
+
* May 2018: Jose Divasón (Universidad de la Rioja),
Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
Fabian Immler (TUM)
--- a/NEWS Mon May 21 22:52:16 2018 +0100
+++ b/NEWS Tue May 22 19:58:17 2018 +0100
@@ -201,6 +201,8 @@
*** HOL ***
+* Landau_Symbols from the AFP was moved to HOL-Library
+
* Clarified relationship of characters, strings and code generation:
* Type "char" is now a proper datatype of 8-bit values.
@@ -313,6 +315,9 @@
* Theory List: functions "sorted_wrt" and "sorted" now compare every
element in a list to all following elements, not just the next one.
+* Theory List: the non-standard filter-syntax "[x <- xs. P]" is
+ deprecated and is currently only available as input syntax anymore.
+
* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
* Predicate coprime is now a real definition, not a mere
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Tue May 22 19:58:17 2018 +0100
@@ -1217,8 +1217,8 @@
\<^item> Change of binding status of variables: anything beyond the built-in
@{keyword "binder"} mixfix annotation requires explicit syntax translations.
- For example, consider list filter comprehension @{term "[x \<leftarrow> xs . P]"} as
- defined in theory @{theory List} in Isabelle/HOL.
+ For example, consider the set comprehension syntax @{term "{x. P}"} as
+ defined in theory @{theory Set} in Isabelle/HOL.
\<close>
--- a/src/Doc/Main/Main_Doc.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/Doc/Main/Main_Doc.thy Tue May 22 19:58:17 2018 +0100
@@ -572,7 +572,6 @@
@{term"[m..<n]"} & @{term[source]"upt m n"}\\
@{term"[i..j]"} & @{term[source]"upto i j"}\\
\<open>[e. x \<leftarrow> xs]\<close> & @{term"map (%x. e) xs"}\\
-@{term"[x \<leftarrow> xs. b]"} & @{term[source]"filter (\<lambda>x. b) xs"} \\
@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\
@{term"\<Sum>x\<leftarrow>xs. e"} & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
\end{supertabular}
--- a/src/Doc/Sledgehammer/document/root.tex Mon May 21 22:52:16 2018 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Tue May 22 19:58:17 2018 +0100
@@ -768,6 +768,10 @@
Be aware that E-Par is experimental software. It has been known to generate
zombie processes. Use at your own risks.
+\item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of
+E that supports a $\lambda$-free fragment of higher-order logic. Use at your
+own risks.
+
\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the
--- a/src/Doc/Tutorial/Inductive/AB.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/Doc/Tutorial/Inductive/AB.thy Tue May 22 19:58:17 2018 +0100
@@ -64,15 +64,13 @@
\<close>
lemma correctness:
- "(w \<in> S \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b]) \<and>
- (w \<in> A \<longrightarrow> size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1) \<and>
- (w \<in> B \<longrightarrow> size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1)"
+ "(w \<in> S \<longrightarrow> size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w)) \<and>
+ (w \<in> A \<longrightarrow> size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w) + 1) \<and>
+ (w \<in> B \<longrightarrow> size(filter (\<lambda>x. x=b) w) = size(filter (\<lambda>x. x=a) w) + 1)"
txt\<open>\noindent
These propositions are expressed with the help of the predefined @{term
-filter} function on lists, which has the convenient syntax @{text"[x\<leftarrow>xs. P
-x]"}, the list of all elements @{term x} in @{term xs} such that @{prop"P x"}
-holds. Remember that on lists @{text size} and @{text length} are synonymous.
+filter} function on lists. Remember that on lists @{text size} and @{text length} are synonymous.
The proof itself is by rule induction and afterwards automatic:
\<close>
@@ -112,8 +110,8 @@
\<close>
lemma step1: "\<forall>i < size w.
- \<bar>(int(size[x\<leftarrow>take (i+1) w. P x])-int(size[x\<leftarrow>take (i+1) w. \<not>P x]))
- - (int(size[x\<leftarrow>take i w. P x])-int(size[x\<leftarrow>take i w. \<not>P x]))\<bar> \<le> 1"
+ \<bar>(int(size(filter P (take (i+1) w)))-int(size(filter (\<lambda>x. \<not>P x) (take (i+1) w))))
+ - (int(size(filter P (take i w)))-int(size(filter (\<lambda>x. \<not>P x) (take i w))))\<bar> \<le> 1"
txt\<open>\noindent
The lemma is a bit hard to read because of the coercion function
@@ -137,8 +135,8 @@
\<close>
lemma part1:
- "size[x\<leftarrow>w. P x] = size[x\<leftarrow>w. \<not>P x]+2 \<Longrightarrow>
- \<exists>i\<le>size w. size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1"
+ "size(filter P w) = size(filter (\<lambda>x. \<not>P x) w)+2 \<Longrightarrow>
+ \<exists>i\<le>size w. size(filter P (take i w)) = size(filter (\<lambda>x. \<not>P x) (take i w))+1"
txt\<open>\noindent
This is proved by @{text force} with the help of the intermediate value theorem,
@@ -157,10 +155,10 @@
lemma part2:
- "\<lbrakk>size[x\<leftarrow>take i w @ drop i w. P x] =
- size[x\<leftarrow>take i w @ drop i w. \<not>P x]+2;
- size[x\<leftarrow>take i w. P x] = size[x\<leftarrow>take i w. \<not>P x]+1\<rbrakk>
- \<Longrightarrow> size[x\<leftarrow>drop i w. P x] = size[x\<leftarrow>drop i w. \<not>P x]+1"
+ "\<lbrakk>size(filter P (take i w @ drop i w)) =
+ size(filter (\<lambda>x. \<not>P x) (take i w @ drop i w))+2;
+ size(filter P (take i w)) = size(filter (\<lambda>x. \<not>P x) (take i w))+1\<rbrakk>
+ \<Longrightarrow> size(filter P (drop i w)) = size(filter (\<lambda>x. \<not>P x) (drop i w))+1"
by(simp del: append_take_drop_id)
text\<open>\noindent
@@ -187,9 +185,9 @@
\<close>
theorem completeness:
- "(size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] \<longrightarrow> w \<in> S) \<and>
- (size[x\<leftarrow>w. x=a] = size[x\<leftarrow>w. x=b] + 1 \<longrightarrow> w \<in> A) \<and>
- (size[x\<leftarrow>w. x=b] = size[x\<leftarrow>w. x=a] + 1 \<longrightarrow> w \<in> B)"
+ "(size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w) \<longrightarrow> w \<in> S) \<and>
+ (size(filter (\<lambda>x. x=a) w) = size(filter (\<lambda>x. x=b) w) + 1 \<longrightarrow> w \<in> A) \<and>
+ (size(filter (\<lambda>x. x=b) w) = size(filter (\<lambda>x. x=a) w) + 1 \<longrightarrow> w \<in> B)"
txt\<open>\noindent
The proof is by induction on @{term w}. Structural induction would fail here
@@ -234,9 +232,9 @@
apply(clarify)
txt\<open>\noindent
This yields an index @{prop"i \<le> length v"} such that
-@{prop[display]"length [x\<leftarrow>take i v . x = a] = length [x\<leftarrow>take i v . x = b] + 1"}
+@{prop[display]"length (filter (\<lambda>x. x=a) (take i v)) = length (filter (\<lambda>x. x=b) (take i v)) + 1"}
With the help of @{thm[source]part2} it follows that
-@{prop[display]"length [x\<leftarrow>drop i v . x = a] = length [x\<leftarrow>drop i v . x = b] + 1"}
+@{prop[display]"length (filter (\<lambda>x. x=a) (drop i v)) = length (filter (\<lambda>x. x=b) (drop i v)) + 1"}
\<close>
apply(drule part2[of "\<lambda>x. x=a", simplified])
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue May 22 19:58:17 2018 +0100
@@ -287,7 +287,7 @@
continuously differentiable, which ensures that the path integral exists at least for any continuous
f, since all piecewise continuous functions are integrable. However, our notion of validity is
weaker, just piecewise differentiability... [namely] continuity plus differentiability except on a
-finite set ... [Our] underlying theory of integration is the Kurzweil-Henstock theory. In contrast to
+finite set ... [Our] underlying theory of integration is the Kurzweil-Henstock theory. In contrast to
the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this
can integrate all derivatives.''
--- a/src/HOL/Library/AList.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Library/AList.thy Tue May 22 19:58:17 2018 +0100
@@ -45,7 +45,7 @@
using assms by (simp add: update_keys)
lemma update_filter:
- "a \<noteq> k \<Longrightarrow> update k v [q\<leftarrow>ps. fst q \<noteq> a] = [q\<leftarrow>update k v ps. fst q \<noteq> a]"
+ "a \<noteq> k \<Longrightarrow> update k v (filter (\<lambda>q. fst q \<noteq> a) ps) = filter (\<lambda>q. fst q \<noteq> a) (update k v ps)"
by (induct ps) auto
lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
@@ -361,12 +361,12 @@
proof -
have "y \<noteq> x \<longleftrightarrow> x \<noteq> y" for y
by auto
- then show "[p \<leftarrow> al. fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al. fst p \<in> D \<and> fst p \<noteq> x]"
+ then show "filter (\<lambda>p. fst p \<in> D \<and> x \<noteq> fst p) al = filter (\<lambda>p. fst p \<in> D \<and> fst p \<noteq> x) al"
by simp
assume "x \<notin> D"
then have "y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" for y
by auto
- then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
+ then show "filter (\<lambda>p. fst p \<in> D \<and> x \<noteq> fst p) al = filter (\<lambda>p. fst p \<in> D) al"
by simp
qed
@@ -492,7 +492,7 @@
lemma distinct_map_ran: "distinct (map fst al) \<Longrightarrow> distinct (map fst (map_ran f al))"
by (simp add: map_ran_def split_def comp_def)
-lemma map_ran_filter: "map_ran f [p\<leftarrow>ps. fst p \<noteq> a] = [p\<leftarrow>map_ran f ps. fst p \<noteq> a]"
+lemma map_ran_filter: "map_ran f (filter (\<lambda>p. fst p \<noteq> a) ps) = filter (\<lambda>p. fst p \<noteq> a) (map_ran f ps)"
by (simp add: map_ran_def filter_map split_def comp_def)
lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
--- a/src/HOL/Library/Finite_Map.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Library/Finite_Map.thy Tue May 22 19:58:17 2018 +0100
@@ -84,10 +84,10 @@
definition map_filter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
"map_filter P m = (\<lambda>x. if P x then m x else None)"
-lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
+lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of (filter (\<lambda>(k, _). P k) m)"
proof
fix x
- show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
+ show "map_filter P (map_of m) x = map_of (filter (\<lambda>(k, _). P k) m) x"
by (induct m) (auto simp: map_filter_def)
qed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Landau_Symbols.thy Tue May 22 19:58:17 2018 +0100
@@ -0,0 +1,2208 @@
+(*
+ File: Landau_Symbols_Definition.thy
+ Author: Manuel Eberl <eberlm@in.tum.de>
+
+ Landau symbols for reasoning about the asymptotic growth of functions.
+*)
+section {* Definition of Landau symbols *}
+
+theory Landau_Symbols
+imports
+ Complex_Main
+begin
+
+lemma eventually_subst':
+ "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> eventually (\<lambda>x. P x (f x)) F = eventually (\<lambda>x. P x (g x)) F"
+ by (rule eventually_subst, erule eventually_rev_mp) simp
+
+
+subsection {* Definition of Landau symbols *}
+
+text {*
+ Our Landau symbols are sign-oblivious, i.e. any function always has the same growth
+ as its absolute. This has the advantage of making some cancelling rules for sums nicer, but
+ introduces some problems in other places. Nevertheless, we found this definition more convenient
+ to work with.
+*}
+
+definition bigo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ ("(1O[_]'(_'))")
+ where "bigo F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
+
+definition smallo :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ ("(1o[_]'(_'))")
+ where "smallo F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F)}"
+
+definition bigomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ ("(1\<Omega>[_]'(_'))")
+ where "bigomega F g = {f. (\<exists>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
+
+definition smallomega :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ ("(1\<omega>[_]'(_'))")
+ where "smallomega F g = {f. (\<forall>c>0. eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F)}"
+
+definition bigtheta :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ ("(1\<Theta>[_]'(_'))")
+ where "bigtheta F g = bigo F g \<inter> bigomega F g"
+
+abbreviation bigo_at_top ("(2O'(_'))") where
+ "O(g) \<equiv> bigo at_top g"
+
+abbreviation smallo_at_top ("(2o'(_'))") where
+ "o(g) \<equiv> smallo at_top g"
+
+abbreviation bigomega_at_top ("(2\<Omega>'(_'))") where
+ "\<Omega>(g) \<equiv> bigomega at_top g"
+
+abbreviation smallomega_at_top ("(2\<omega>'(_'))") where
+ "\<omega>(g) \<equiv> smallomega at_top g"
+
+abbreviation bigtheta_at_top ("(2\<Theta>'(_'))") where
+ "\<Theta>(g) \<equiv> bigtheta at_top g"
+
+
+text {* The following is a set of properties that all Landau symbols satisfy. *}
+
+named_theorems landau_divide_simps
+
+locale landau_symbol =
+ fixes L :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ and L' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"
+ and Lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"
+ assumes bot': "L bot f = UNIV"
+ assumes filter_mono': "F1 \<le> F2 \<Longrightarrow> L F2 f \<subseteq> L F1 f"
+ assumes in_filtermap_iff:
+ "f' \<in> L (filtermap h' F') g' \<longleftrightarrow> (\<lambda>x. f' (h' x)) \<in> L' F' (\<lambda>x. g' (h' x))"
+ assumes filtercomap:
+ "f' \<in> L F'' g' \<Longrightarrow> (\<lambda>x. f' (h' x)) \<in> L' (filtercomap h' F'') (\<lambda>x. g' (h' x))"
+ assumes sup: "f \<in> L F1 g \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L (sup F1 F2) g"
+ assumes in_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"
+ assumes cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> L F (f) = L F (g)"
+ assumes cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> L F (f) = L F (g)"
+ assumes in_cong_bigtheta: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)"
+ assumes cmult [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. c * f x) = L F (f)"
+ assumes cmult_in_iff [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. c * f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
+ assumes mult_left [simp]: "f \<in> L F (g) \<Longrightarrow> (\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)"
+ assumes inverse: "eventually (\<lambda>x. f x \<noteq> 0) F \<Longrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F \<Longrightarrow>
+ f \<in> L F (g) \<Longrightarrow> (\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))"
+ assumes subsetI: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"
+ assumes plus_subset1: "f \<in> o[F](g) \<Longrightarrow> L F (g) \<subseteq> L F (\<lambda>x. f x + g x)"
+ assumes trans: "f \<in> L F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
+ assumes compose: "f \<in> L F (g) \<Longrightarrow> filterlim h' F G \<Longrightarrow> (\<lambda>x. f (h' x)) \<in> L' G (\<lambda>x. g (h' x))"
+ assumes norm_iff [simp]: "(\<lambda>x. norm (f x)) \<in> Lr F (\<lambda>x. norm (g x)) \<longleftrightarrow> f \<in> L F (g)"
+ assumes abs [simp]: "Lr Fr (\<lambda>x. \<bar>fr x\<bar>) = Lr Fr fr"
+ assumes abs_in_iff [simp]: "(\<lambda>x. \<bar>fr x\<bar>) \<in> Lr Fr gr \<longleftrightarrow> fr \<in> Lr Fr gr"
+begin
+
+lemma bot [simp]: "f \<in> L bot g" by (simp add: bot')
+
+lemma filter_mono: "F1 \<le> F2 \<Longrightarrow> f \<in> L F2 g \<Longrightarrow> f \<in> L F1 g"
+ using filter_mono'[of F1 F2] by blast
+
+lemma cong_ex:
+ "eventually (\<lambda>x. f1 x = f2 x) F \<Longrightarrow> eventually (\<lambda>x. g1 x = g2 x) F \<Longrightarrow>
+ f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)"
+ by (subst cong, assumption, subst in_cong, assumption, rule refl)
+
+lemma cong_ex_bigtheta:
+ "f1 \<in> \<Theta>[F](f2) \<Longrightarrow> g1 \<in> \<Theta>[F](g2) \<Longrightarrow> f1 \<in> L F (g1) \<longleftrightarrow> f2 \<in> L F (g2)"
+ by (subst cong_bigtheta, assumption, subst in_cong_bigtheta, assumption, rule refl)
+
+lemma bigtheta_trans1:
+ "f \<in> L F (g) \<Longrightarrow> g \<in> \<Theta>[F](h) \<Longrightarrow> f \<in> L F (h)"
+ by (subst cong_bigtheta[symmetric])
+
+lemma bigtheta_trans2:
+ "f \<in> \<Theta>[F](g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
+ by (subst in_cong_bigtheta)
+
+lemma cmult' [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x * c) = L F (f)"
+ by (subst mult.commute) (rule cmult)
+
+lemma cmult_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x * c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
+ by (subst mult.commute) (rule cmult_in_iff)
+
+lemma cdiv [simp]: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>x. f x / c) = L F (f)"
+ using cmult'[of "inverse c" F f] by (simp add: field_simps)
+
+lemma cdiv_in_iff' [simp]: "c \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / c) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
+ using cmult_in_iff'[of "inverse c" f] by (simp add: field_simps)
+
+lemma uminus [simp]: "L F (\<lambda>x. -g x) = L F (g)" using cmult[of "-1"] by simp
+
+lemma uminus_in_iff [simp]: "(\<lambda>x. -f x) \<in> L F (g) \<longleftrightarrow> f \<in> L F (g)"
+ using cmult_in_iff[of "-1"] by simp
+
+lemma const: "c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"
+ by (subst (2) cmult[symmetric]) simp_all
+
+(* Simplifier loops without the NO_MATCH *)
+lemma const' [simp]: "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> L F (\<lambda>_. c) = L F (\<lambda>_. 1)"
+ by (rule const)
+
+lemma const_in_iff: "c \<noteq> 0 \<Longrightarrow> (\<lambda>_. c) \<in> L F (f) \<longleftrightarrow> (\<lambda>_. 1) \<in> L F (f)"
+ using cmult_in_iff'[of c "\<lambda>_. 1"] by simp
+
+lemma const_in_iff' [simp]: "NO_MATCH 1 c \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> (\<lambda>_. c) \<in> L F (f) \<longleftrightarrow> (\<lambda>_. 1) \<in> L F (f)"
+ by (rule const_in_iff)
+
+lemma plus_subset2: "g \<in> o[F](f) \<Longrightarrow> L F (f) \<subseteq> L F (\<lambda>x. f x + g x)"
+ by (subst add.commute) (rule plus_subset1)
+
+lemma mult_right [simp]: "f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (\<lambda>x. g x * h x)"
+ using mult_left by (simp add: mult.commute)
+
+lemma mult: "f1 \<in> L F (g1) \<Longrightarrow> f2 \<in> L F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
+ by (rule trans, erule mult_left, erule mult_right)
+
+lemma inverse_cancel:
+ assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
+ assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+ shows "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> g \<in> L F (f)"
+proof
+ assume "(\<lambda>x. inverse (f x)) \<in> L F (\<lambda>x. inverse (g x))"
+ from inverse[OF _ _ this] assms show "g \<in> L F (f)" by simp
+qed (intro inverse assms)
+
+lemma divide_right:
+ assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+ assumes "f \<in> L F (g)"
+ shows "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"
+ by (subst (1 2) divide_inverse) (intro mult_right inverse assms)
+
+lemma divide_right_iff:
+ assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+ shows "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> f \<in> L F (g)"
+proof
+ assume "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x / h x)"
+ from mult_right[OF this, of h] assms show "f \<in> L F (g)"
+ by (subst (asm) cong_ex[of _ f F _ g]) (auto elim!: eventually_mono)
+qed (simp add: divide_right assms)
+
+lemma divide_left:
+ assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
+ assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+ assumes "g \<in> L F(f)"
+ shows "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"
+ by (subst (1 2) divide_inverse) (intro mult_left inverse assms)
+
+lemma divide_left_iff:
+ assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
+ assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+ assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+ shows "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x) \<longleftrightarrow> g \<in> L F (f)"
+proof
+ assume A: "(\<lambda>x. h x / f x) \<in> L F (\<lambda>x. h x / g x)"
+ from assms have B: "eventually (\<lambda>x. h x / f x / h x = inverse (f x)) F"
+ by eventually_elim (simp add: divide_inverse)
+ from assms have C: "eventually (\<lambda>x. h x / g x / h x = inverse (g x)) F"
+ by eventually_elim (simp add: divide_inverse)
+ from divide_right[OF assms(3) A] assms show "g \<in> L F (f)"
+ by (subst (asm) cong_ex[OF B C]) (simp add: inverse_cancel)
+qed (simp add: divide_left assms)
+
+lemma divide:
+ assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
+ assumes "eventually (\<lambda>x. g2 x \<noteq> 0) F"
+ assumes "f1 \<in> L F (f2)" "g2 \<in> L F (g1)"
+ shows "(\<lambda>x. f1 x / g1 x) \<in> L F (\<lambda>x. f2 x / g2 x)"
+ by (subst (1 2) divide_inverse) (intro mult inverse assms)
+
+lemma divide_eq1:
+ assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+ shows "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
+proof-
+ have "f \<in> L F (\<lambda>x. g x / h x) \<longleftrightarrow> (\<lambda>x. f x * h x / h x) \<in> L F (\<lambda>x. g x / h x)"
+ using assms by (intro in_cong) (auto elim: eventually_mono)
+ thus ?thesis by (simp only: divide_right_iff assms)
+qed
+
+lemma divide_eq2:
+ assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+ shows "(\<lambda>x. f x / h x) \<in> L F (\<lambda>x. g x) \<longleftrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
+proof-
+ have "L F (\<lambda>x. g x) = L F (\<lambda>x. g x * h x / h x)"
+ using assms by (intro cong) (auto elim: eventually_mono)
+ thus ?thesis by (simp only: divide_right_iff assms)
+qed
+
+lemma inverse_eq1:
+ assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+ shows "f \<in> L F (\<lambda>x. inverse (g x)) \<longleftrightarrow> (\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"
+ using divide_eq1[of g F f "\<lambda>_. 1"] by (simp add: divide_inverse assms)
+
+lemma inverse_eq2:
+ assumes "eventually (\<lambda>x. f x \<noteq> 0) F"
+ shows "(\<lambda>x. inverse (f x)) \<in> L F (g) \<longleftrightarrow> (\<lambda>x. 1) \<in> L F (\<lambda>x. f x * g x)"
+ using divide_eq2[of f F "\<lambda>_. 1" g] by (simp add: divide_inverse assms mult_ac)
+
+lemma inverse_flip:
+ assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+ assumes "eventually (\<lambda>x. h x \<noteq> 0) F"
+ assumes "(\<lambda>x. inverse (g x)) \<in> L F (h)"
+ shows "(\<lambda>x. inverse (h x)) \<in> L F (g)"
+using assms by (simp add: divide_eq1 divide_eq2 inverse_eq_divide mult.commute)
+
+lemma lift_trans:
+ assumes "f \<in> L F (g)"
+ assumes "(\<lambda>x. t x (g x)) \<in> L F (h)"
+ assumes "\<And>f g. f \<in> L F (g) \<Longrightarrow> (\<lambda>x. t x (f x)) \<in> L F (\<lambda>x. t x (g x))"
+ shows "(\<lambda>x. t x (f x)) \<in> L F (h)"
+ by (rule trans[OF assms(3)[OF assms(1)] assms(2)])
+
+lemma lift_trans':
+ assumes "f \<in> L F (\<lambda>x. t x (g x))"
+ assumes "g \<in> L F (h)"
+ assumes "\<And>g h. g \<in> L F (h) \<Longrightarrow> (\<lambda>x. t x (g x)) \<in> L F (\<lambda>x. t x (h x))"
+ shows "f \<in> L F (\<lambda>x. t x (h x))"
+ by (rule trans[OF assms(1) assms(3)[OF assms(2)]])
+
+lemma lift_trans_bigtheta:
+ assumes "f \<in> L F (g)"
+ assumes "(\<lambda>x. t x (g x)) \<in> \<Theta>[F](h)"
+ assumes "\<And>f g. f \<in> L F (g) \<Longrightarrow> (\<lambda>x. t x (f x)) \<in> L F (\<lambda>x. t x (g x))"
+ shows "(\<lambda>x. t x (f x)) \<in> L F (h)"
+ using cong_bigtheta[OF assms(2)] assms(3)[OF assms(1)] by simp
+
+lemma lift_trans_bigtheta':
+ assumes "f \<in> L F (\<lambda>x. t x (g x))"
+ assumes "g \<in> \<Theta>[F](h)"
+ assumes "\<And>g h. g \<in> \<Theta>[F](h) \<Longrightarrow> (\<lambda>x. t x (g x)) \<in> \<Theta>[F](\<lambda>x. t x (h x))"
+ shows "f \<in> L F (\<lambda>x. t x (h x))"
+ using cong_bigtheta[OF assms(3)[OF assms(2)]] assms(1) by simp
+
+lemma (in landau_symbol) mult_in_1:
+ assumes "f \<in> L F (\<lambda>_. 1)" "g \<in> L F (\<lambda>_. 1)"
+ shows "(\<lambda>x. f x * g x) \<in> L F (\<lambda>_. 1)"
+ using mult[OF assms] by simp
+
+lemma (in landau_symbol) of_real_cancel:
+ "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<Longrightarrow> f \<in> Lr F g"
+ by (subst (asm) norm_iff [symmetric], subst (asm) (1 2) norm_of_real) simp_all
+
+lemma (in landau_symbol) of_real_iff:
+ "(\<lambda>x. of_real (f x)) \<in> L F (\<lambda>x. of_real (g x)) \<longleftrightarrow> f \<in> Lr F g"
+ by (subst norm_iff [symmetric], subst (1 2) norm_of_real) simp_all
+
+lemmas [landau_divide_simps] =
+ inverse_cancel divide_left_iff divide_eq1 divide_eq2 inverse_eq1 inverse_eq2
+
+end
+
+
+text {*
+ The symbols $O$ and $o$ and $\Omega$ and $\omega$ are dual, so for many rules, replacing $O$ with
+ $\Omega$, $o$ with $\omega$, and $\leq$ with $\geq$ in a theorem yields another valid theorem.
+ The following locale captures this fact.
+*}
+
+locale landau_pair =
+ fixes L l :: "'a filter \<Rightarrow> ('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('a \<Rightarrow> 'b) set"
+ fixes L' l' :: "'c filter \<Rightarrow> ('c \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> ('c \<Rightarrow> 'b) set"
+ fixes Lr lr :: "'a filter \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) set"
+ and R :: "real \<Rightarrow> real \<Rightarrow> bool"
+ assumes L_def: "L F g = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"
+ and l_def: "l F g = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F}"
+ and L'_def: "L' F' g' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"
+ and l'_def: "l' F' g' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g' x))) F'}"
+ and Lr_def: "Lr F'' g'' = {f. \<exists>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"
+ and lr_def: "lr F'' g'' = {f. \<forall>c>0. eventually (\<lambda>x. R (norm (f x)) (c * norm (g'' x))) F''}"
+ and R: "R = (\<le>) \<or> R = (\<ge>)"
+
+interpretation landau_o:
+ landau_pair bigo smallo bigo smallo bigo smallo "(\<le>)"
+ by unfold_locales (auto simp: bigo_def smallo_def intro!: ext)
+
+interpretation landau_omega:
+ landau_pair bigomega smallomega bigomega smallomega bigomega smallomega "(\<ge>)"
+ by unfold_locales (auto simp: bigomega_def smallomega_def intro!: ext)
+
+
+context landau_pair
+begin
+
+lemmas R_E = disjE [OF R, case_names le ge]
+
+lemma bigI:
+ "c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F \<Longrightarrow> f \<in> L F (g)"
+ unfolding L_def by blast
+
+lemma bigE:
+ assumes "f \<in> L F (g)"
+ obtains c where "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"
+ using assms unfolding L_def by blast
+
+lemma smallI:
+ "(\<And>c. c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F) \<Longrightarrow> f \<in> l F (g)"
+ unfolding l_def by blast
+
+lemma smallD:
+ "f \<in> l F (g) \<Longrightarrow> c > 0 \<Longrightarrow> eventually (\<lambda>x. R (norm (f x)) (c * (norm (g x)))) F"
+ unfolding l_def by blast
+
+lemma bigE_nonneg_real:
+ assumes "f \<in> Lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F"
+ obtains c where "c > 0" "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
+proof-
+ from assms(1) obtain c where c: "c > 0" "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
+ by (auto simp: Lr_def)
+ from c(2) assms(2) have "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
+ by eventually_elim simp
+ from c(1) and this show ?thesis by (rule that)
+qed
+
+lemma smallD_nonneg_real:
+ assumes "f \<in> lr F (g)" "eventually (\<lambda>x. f x \<ge> 0) F" "c > 0"
+ shows "eventually (\<lambda>x. R (f x) (c * \<bar>g x\<bar>)) F"
+ using assms by (auto simp: lr_def dest!: spec[of _ c] elim: eventually_elim2)
+
+lemma small_imp_big: "f \<in> l F (g) \<Longrightarrow> f \<in> L F (g)"
+ by (rule bigI[OF _ smallD, of 1]) simp_all
+
+lemma small_subset_big: "l F (g) \<subseteq> L F (g)"
+ using small_imp_big by blast
+
+lemma R_refl [simp]: "R x x" using R by auto
+
+lemma R_linear: "\<not>R x y \<Longrightarrow> R y x"
+ using R by auto
+
+lemma R_trans [trans]: "R a b \<Longrightarrow> R b c \<Longrightarrow> R a c"
+ using R by auto
+
+lemma R_mult_left_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (c*a) (c*b)"
+ using R by (auto simp: mult_left_mono)
+
+lemma R_mult_right_mono: "R a b \<Longrightarrow> c \<ge> 0 \<Longrightarrow> R (a*c) (b*c)"
+ using R by (auto simp: mult_right_mono)
+
+lemma big_trans:
+ assumes "f \<in> L F (g)" "g \<in> L F (h)"
+ shows "f \<in> L F (h)"
+proof-
+ from assms(1) guess c by (elim bigE) note c = this
+ from assms(2) guess d by (elim bigE) note d = this
+ from c(2) d(2) have "eventually (\<lambda>x. R (norm (f x)) (c * d * (norm (h x)))) F"
+ proof eventually_elim
+ fix x assume "R (norm (f x)) (c * (norm (g x)))"
+ also assume "R (norm (g x)) (d * (norm (h x)))"
+ with c(1) have "R (c * (norm (g x))) (c * (d * (norm (h x))))"
+ by (intro R_mult_left_mono) simp_all
+ finally show "R (norm (f x)) (c * d * (norm (h x)))" by (simp add: algebra_simps)
+ qed
+ with c(1) d(1) show ?thesis by (intro bigI[of "c*d"]) simp_all
+qed
+
+lemma big_small_trans:
+ assumes "f \<in> L F (g)" "g \<in> l F (h)"
+ shows "f \<in> l F (h)"
+proof (rule smallI)
+ fix c :: real assume c: "c > 0"
+ from assms(1) guess d by (elim bigE) note d = this
+ note d(2)
+ moreover from c d assms(2)
+ have "eventually (\<lambda>x. R (norm (g x)) (c * inverse d * norm (h x))) F"
+ by (intro smallD) simp_all
+ ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * (norm (h x)))) F"
+ by eventually_elim (erule R_trans, insert R d(1), auto simp: field_simps)
+qed
+
+lemma small_big_trans:
+ assumes "f \<in> l F (g)" "g \<in> L F (h)"
+ shows "f \<in> l F (h)"
+proof (rule smallI)
+ fix c :: real assume c: "c > 0"
+ from assms(2) guess d by (elim bigE) note d = this
+ note d(2)
+ moreover from c d assms(1)
+ have "eventually (\<lambda>x. R (norm (f x)) (c * inverse d * norm (g x))) F"
+ by (intro smallD) simp_all
+ ultimately show "eventually (\<lambda>x. R (norm (f x)) (c * norm (h x))) F"
+ by eventually_elim (rotate_tac 2, erule R_trans, insert R c d(1), auto simp: field_simps)
+qed
+
+lemma small_trans:
+ "f \<in> l F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> l F (h)"
+ by (rule big_small_trans[OF small_imp_big])
+
+lemma small_big_trans':
+ "f \<in> l F (g) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
+ by (rule small_imp_big[OF small_big_trans])
+
+lemma big_small_trans':
+ "f \<in> L F (g) \<Longrightarrow> g \<in> l F (h) \<Longrightarrow> f \<in> L F (h)"
+ by (rule small_imp_big[OF big_small_trans])
+
+lemma big_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> L F (f) \<subseteq> L F (g)"
+ by (intro subsetI) (drule (1) big_trans)
+
+lemma small_subsetI [intro]: "f \<in> L F (g) \<Longrightarrow> l F (f) \<subseteq> l F (g)"
+ by (intro subsetI) (drule (1) small_big_trans)
+
+lemma big_refl [simp]: "f \<in> L F (f)"
+ by (rule bigI[of 1]) simp_all
+
+lemma small_refl_iff: "f \<in> l F (f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+proof (rule iffI[OF _ smallI])
+ assume f: "f \<in> l F f"
+ have "(1/2::real) > 0" "(2::real) > 0" by simp_all
+ from smallD[OF f this(1)] smallD[OF f this(2)]
+ show "eventually (\<lambda>x. f x = 0) F" by eventually_elim (insert R, auto)
+next
+ fix c :: real assume "c > 0" "eventually (\<lambda>x. f x = 0) F"
+ from this(2) show "eventually (\<lambda>x. R (norm (f x)) (c * norm (f x))) F"
+ by eventually_elim simp_all
+qed
+
+lemma big_small_asymmetric: "f \<in> L F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
+ by (drule (1) big_small_trans) (simp add: small_refl_iff)
+
+lemma small_big_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> L F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
+ by (drule (1) small_big_trans) (simp add: small_refl_iff)
+
+lemma small_asymmetric: "f \<in> l F (g) \<Longrightarrow> g \<in> l F (f) \<Longrightarrow> eventually (\<lambda>x. f x = 0) F"
+ by (drule (1) small_trans) (simp add: small_refl_iff)
+
+
+lemma plus_aux:
+ assumes "f \<in> o[F](g)"
+ shows "g \<in> L F (\<lambda>x. f x + g x)"
+proof (rule R_E)
+ assume [simp]: "R = (\<le>)"
+ have A: "1/2 > (0::real)" by simp
+ {
+ fix x assume "norm (f x) \<le> 1/2 * norm (g x)"
+ hence "1/2 * (norm (g x)) \<le> (norm (g x)) - (norm (f x))" by simp
+ also have "norm (g x) - norm (f x) \<le> norm (f x + g x)"
+ by (subst add.commute) (rule norm_diff_ineq)
+ finally have "1/2 * (norm (g x)) \<le> norm (f x + g x)" by simp
+ } note B = this
+
+ show "g \<in> L F (\<lambda>x. f x + g x)"
+ apply (rule bigI[of "2"], simp)
+ using landau_o.smallD[OF assms A] apply eventually_elim
+ using B apply (simp add: algebra_simps)
+ done
+next
+ assume [simp]: "R = (\<lambda>x y. x \<ge> y)"
+ show "g \<in> L F (\<lambda>x. f x + g x)"
+ proof (rule bigI[of "1/2"])
+ show "eventually (\<lambda>x. R (norm (g x)) (1/2 * norm (f x + g x))) F"
+ using landau_o.smallD[OF assms zero_less_one]
+ proof eventually_elim
+ case (elim x)
+ have "norm (f x + g x) \<le> norm (f x) + norm (g x)" by (rule norm_triangle_ineq)
+ also note elim
+ finally show ?case by simp
+ qed
+ qed simp_all
+qed
+
+end
+
+
+
+lemma bigomega_iff_bigo: "g \<in> \<Omega>[F](f) \<longleftrightarrow> f \<in> O[F](g)"
+proof
+ assume "f \<in> O[F](g)"
+ then guess c by (elim landau_o.bigE)
+ thus "g \<in> \<Omega>[F](f)" by (intro landau_omega.bigI[of "inverse c"]) (simp_all add: field_simps)
+next
+ assume "g \<in> \<Omega>[F](f)"
+ then guess c by (elim landau_omega.bigE)
+ thus "f \<in> O[F](g)" by (intro landau_o.bigI[of "inverse c"]) (simp_all add: field_simps)
+qed
+
+lemma smallomega_iff_smallo: "g \<in> \<omega>[F](f) \<longleftrightarrow> f \<in> o[F](g)"
+proof
+ assume "f \<in> o[F](g)"
+ from landau_o.smallD[OF this, of "inverse c" for c]
+ show "g \<in> \<omega>[F](f)" by (intro landau_omega.smallI) (simp_all add: field_simps)
+next
+ assume "g \<in> \<omega>[F](f)"
+ from landau_omega.smallD[OF this, of "inverse c" for c]
+ show "f \<in> o[F](g)" by (intro landau_o.smallI) (simp_all add: field_simps)
+qed
+
+
+context landau_pair
+begin
+
+lemma big_mono:
+ "eventually (\<lambda>x. R (norm (f x)) (norm (g x))) F \<Longrightarrow> f \<in> L F (g)"
+ by (rule bigI[OF zero_less_one]) simp
+
+lemma big_mult:
+ assumes "f1 \<in> L F (g1)" "f2 \<in> L F (g2)"
+ shows "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
+proof-
+ from assms(1) guess c1 by (elim bigE) note c1 = this
+ from assms(2) guess c2 by (elim bigE) note c2 = this
+
+ from c1(1) and c2(1) have "c1 * c2 > 0" by simp
+ moreover have "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * c2 * norm (g1 x * g2 x))) F"
+ using c1(2) c2(2)
+ proof eventually_elim
+ case (elim x)
+ show ?case
+ proof (cases rule: R_E)
+ case le
+ have "norm (f1 x) * norm (f2 x) \<le> (c1 * norm (g1 x)) * (c2 * norm (g2 x))"
+ using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
+ with le show ?thesis by (simp add: le norm_mult mult_ac)
+ next
+ case ge
+ have "(c1 * norm (g1 x)) * (c2 * norm (g2 x)) \<le> norm (f1 x) * norm (f2 x)"
+ using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
+ with ge show ?thesis by (simp_all add: norm_mult mult_ac)
+ qed
+ qed
+ ultimately show ?thesis by (rule bigI)
+qed
+
+lemma small_big_mult:
+ assumes "f1 \<in> l F (g1)" "f2 \<in> L F (g2)"
+ shows "(\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"
+proof (rule smallI)
+ fix c1 :: real assume c1: "c1 > 0"
+ from assms(2) guess c2 by (elim bigE) note c2 = this
+ with c1 assms(1) have "eventually (\<lambda>x. R (norm (f1 x)) (c1 * inverse c2 * norm (g1 x))) F"
+ by (auto intro!: smallD)
+ thus "eventually (\<lambda>x. R (norm (f1 x * f2 x)) (c1 * norm (g1 x * g2 x))) F" using c2(2)
+ proof eventually_elim
+ case (elim x)
+ show ?case
+ proof (cases rule: R_E)
+ case le
+ have "norm (f1 x) * norm (f2 x) \<le> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
+ using elim le c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
+ with le c2(1) show ?thesis by (simp add: le norm_mult field_simps)
+ next
+ case ge
+ have "norm (f1 x) * norm (f2 x) \<ge> (c1 * inverse c2 * norm (g1 x)) * (c2 * norm (g2 x))"
+ using elim ge c1(1) c2(1) by (intro mult_mono mult_nonneg_nonneg) auto
+ with ge c2(1) show ?thesis by (simp add: ge norm_mult field_simps)
+ qed
+ qed
+qed
+
+lemma big_small_mult:
+ "f1 \<in> L F (g1) \<Longrightarrow> f2 \<in> l F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"
+ by (subst (1 2) mult.commute) (rule small_big_mult)
+
+lemma small_mult: "f1 \<in> l F (g1) \<Longrightarrow> f2 \<in> l F (g2) \<Longrightarrow> (\<lambda>x. f1 x * f2 x) \<in> l F (\<lambda>x. g1 x * g2 x)"
+ by (rule small_big_mult, assumption, rule small_imp_big)
+
+lemmas mult = big_mult small_big_mult big_small_mult small_mult
+
+
+sublocale big: landau_symbol L L' Lr
+proof
+ have L: "L = bigo \<or> L = bigomega"
+ by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
+ {
+ fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
+ hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
+ } note A = this
+ {
+ fix c :: 'b and F and f :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
+ from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
+ show "L F (\<lambda>x. c * f x) = L F f" by (intro equalityI big_subsetI) (simp_all add: field_simps)
+ }
+ {
+ fix c :: 'b and F and f g :: "'a \<Rightarrow> 'b" assume "c \<noteq> 0"
+ from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
+ have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
+ thus "((\<lambda>x. c * f x) \<in> L F g) = (f \<in> L F g)" by (intro iffI) (erule (1) big_trans)+
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> L F (g)"
+ assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
+ from A guess c by (elim bigE) note c = this
+ from c(2) B have "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
+ by eventually_elim (rule R_E, insert c(1), simp_all add: field_simps norm_inverse norm_divide)
+ with c(1) show "(\<lambda>x. inverse (g x)) \<in> L F (\<lambda>x. inverse (f x))" by (rule bigI)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
+ with plus_aux show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" by (blast intro!: big_subsetI)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
+ show "L F (f) = L F (g)" unfolding L_def
+
+ thm eventually_subst A
+ by (subst eventually_subst'[OF A]) (rule refl)
+ }
+ {
+ fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
+ show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" unfolding L_def mem_Collect_eq
+ by (subst (1) eventually_subst'[OF A]) (rule refl)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" thus "L F f \<subseteq> L F g" by (rule big_subsetI)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
+ with A L show "L F (f) = L F (g)" unfolding bigtheta_def
+ by (intro equalityI big_subsetI) (auto simp: bigomega_iff_bigo)
+ fix h:: "'a \<Rightarrow> 'b"
+ show "f \<in> L F (h) \<longleftrightarrow> g \<in> L F (h)" by (rule disjE[OF L])
+ (insert A, auto simp: bigtheta_def bigomega_iff_bigo intro: landau_o.big_trans)
+ }
+ {
+ fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g"
+ thus "(\<lambda>x. h x * f x) \<in> L F (\<lambda>x. h x * g x)" by (intro big_mult) simp
+ }
+ {
+ fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> L F g" "g \<in> L F h"
+ thus "f \<in> L F (h)" by (rule big_trans)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
+ assume "f \<in> L F g" and "filterlim h F G"
+ thus "(\<lambda>x. f (h x)) \<in> L' G (\<lambda>x. g (h x))" by (auto simp: L_def L'_def filterlim_iff)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F G :: "'a filter"
+ assume "f \<in> L F g" "f \<in> L G g"
+ from this [THEN bigE] guess c1 c2 . note c12 = this
+ define c where "c = (if R c1 c2 then c2 else c1)"
+ from c12 have c: "R c1 c" "R c2 c" "c > 0" by (auto simp: c_def dest: R_linear)
+ with c12(2,4) have "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) F"
+ "eventually (\<lambda>x. R (norm (f x)) (c * norm (g x))) G"
+ by (force elim: eventually_mono intro: R_trans[OF _ R_mult_right_mono])+
+ with c show "f \<in> L (sup F G) g" by (auto simp: L_def eventually_sup)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
+ assume "(f \<in> L F g)"
+ thus "((\<lambda>x. f (h x)) \<in> L' (filtercomap h F) (\<lambda>x. g (h x)))"
+ unfolding L_def L'_def by auto
+ }
+qed (auto simp: L_def Lr_def eventually_filtermap L'_def
+ intro: filter_leD exI[of _ "1::real"])
+
+sublocale small: landau_symbol l l' lr
+proof
+ {
+ fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
+ hence "(\<lambda>x. c * f x) \<in> L F f" by (intro bigI[of "norm c"]) (simp_all add: norm_mult)
+ } note A = this
+ {
+ fix c :: 'b and f :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
+ from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
+ show "l F (\<lambda>x. c * f x) = l F f"
+ by (intro equalityI small_subsetI) (simp_all add: field_simps)
+ }
+ {
+ fix c :: 'b and f g :: "'a \<Rightarrow> 'b" and F assume "c \<noteq> 0"
+ from `c \<noteq> 0` and A[of c f] and A[of "inverse c" "\<lambda>x. c * f x"]
+ have "(\<lambda>x. c * f x) \<in> L F f" "f \<in> L F (\<lambda>x. c * f x)" by (simp_all add: field_simps)
+ thus "((\<lambda>x. c * f x) \<in> l F g) = (f \<in> l F g)" by (intro iffI) (erule (1) big_small_trans)+
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> o[F](g)"
+ with plus_aux show "l F g \<subseteq> l F (\<lambda>x. f x + g x)" by (blast intro!: small_subsetI)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> l F (g)"
+ assume B: "eventually (\<lambda>x. f x \<noteq> 0) F" "eventually (\<lambda>x. g x \<noteq> 0) F"
+ show "(\<lambda>x. inverse (g x)) \<in> l F (\<lambda>x. inverse (f x))"
+ proof (rule smallI)
+ fix c :: real assume c: "c > 0"
+ from B smallD[OF A c]
+ show "eventually (\<lambda>x. R (norm (inverse (g x))) (c * norm (inverse (f x)))) F"
+ by eventually_elim (rule R_E, simp_all add: field_simps norm_inverse norm_divide)
+ qed
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
+ show "l F (f) = l F (g)" unfolding l_def by (subst eventually_subst'[OF A]) (rule refl)
+ }
+ {
+ fix f g h :: "'a \<Rightarrow> 'b" and F assume A: "eventually (\<lambda>x. f x = g x) F"
+ show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" unfolding l_def mem_Collect_eq
+ by (subst (1) eventually_subst'[OF A]) (rule refl)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g"
+ thus "l F f \<subseteq> l F g" by (intro small_subsetI small_imp_big)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
+ have L: "L = bigo \<or> L = bigomega"
+ by (rule R_E) (auto simp: bigo_def L_def bigomega_def fun_eq_iff)
+ with A show "l F (f) = l F (g)" unfolding bigtheta_def
+ by (intro equalityI small_subsetI) (auto simp: bigomega_iff_bigo)
+ have l: "l = smallo \<or> l = smallomega"
+ by (rule R_E) (auto simp: smallo_def l_def smallomega_def fun_eq_iff)
+ fix h:: "'a \<Rightarrow> 'b"
+ show "f \<in> l F (h) \<longleftrightarrow> g \<in> l F (h)" by (rule disjE[OF l])
+ (insert A, auto simp: bigtheta_def bigomega_iff_bigo smallomega_iff_smallo
+ intro: landau_o.big_small_trans landau_o.small_big_trans)
+ }
+ {
+ fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g"
+ thus "(\<lambda>x. h x * f x) \<in> l F (\<lambda>x. h x * g x)" by (intro big_small_mult) simp
+ }
+ {
+ fix f g h :: "'a \<Rightarrow> 'b" and F assume "f \<in> l F g" "g \<in> l F h"
+ thus "f \<in> l F (h)" by (rule small_trans)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G
+ assume "f \<in> l F g" and "filterlim h F G"
+ thus "(\<lambda>x. f (h x)) \<in> l' G (\<lambda>x. g (h x))"
+ by (auto simp: l_def l'_def filterlim_iff)
+ }
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and h :: "'c \<Rightarrow> 'a" and F G :: "'a filter"
+ assume "(f \<in> l F g)"
+ thus "((\<lambda>x. f (h x)) \<in> l' (filtercomap h F) (\<lambda>x. g (h x)))"
+ unfolding l_def l'_def by auto
+ }
+qed (auto simp: l_def lr_def eventually_filtermap l'_def eventually_sup intro: filter_leD)
+
+
+text {* These rules allow chaining of Landau symbol propositions in Isar with "also".*}
+
+lemma big_mult_1: "f \<in> L F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
+ and big_mult_1': "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> L F (\<lambda>x. g x * h x)"
+ and small_mult_1: "f \<in> l F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> L F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
+ and small_mult_1': "(\<lambda>_. 1) \<in> L F (g) \<Longrightarrow> f \<in> l F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
+ and small_mult_1'': "f \<in> L F (g) \<Longrightarrow> (\<lambda>_. 1) \<in> l F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
+ and small_mult_1''': "(\<lambda>_. 1) \<in> l F (g) \<Longrightarrow> f \<in> L F (h) \<Longrightarrow> f \<in> l F (\<lambda>x. g x * h x)"
+ by (drule (1) big.mult big_small_mult small_big_mult, simp)+
+
+lemma big_1_mult: "f \<in> L F (g) \<Longrightarrow> h \<in> L F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
+ and big_1_mult': "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> L F (g)"
+ and small_1_mult: "f \<in> l F (g) \<Longrightarrow> h \<in> L F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"
+ and small_1_mult': "h \<in> L F (\<lambda>_. 1) \<Longrightarrow> f \<in> l F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"
+ and small_1_mult'': "f \<in> L F (g) \<Longrightarrow> h \<in> l F (\<lambda>_. 1) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"
+ and small_1_mult''': "h \<in> l F (\<lambda>_. 1) \<Longrightarrow> f \<in> L F (g) \<Longrightarrow> (\<lambda>x. f x * h x) \<in> l F (g)"
+ by (drule (1) big.mult big_small_mult small_big_mult, simp)+
+
+lemmas mult_1_trans =
+ big_mult_1 big_mult_1' small_mult_1 small_mult_1' small_mult_1'' small_mult_1'''
+ big_1_mult big_1_mult' small_1_mult small_1_mult' small_1_mult'' small_1_mult'''
+
+lemma big_equal_iff_bigtheta: "L F (f) = L F (g) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
+proof
+ have L: "L = bigo \<or> L = bigomega"
+ by (rule R_E) (auto simp: fun_eq_iff L_def bigo_def bigomega_def)
+ fix f g :: "'a \<Rightarrow> 'b" assume "L F (f) = L F (g)"
+ with big_refl[of f F] big_refl[of g F] have "f \<in> L F (g)" "g \<in> L F (f)" by simp_all
+ thus "f \<in> \<Theta>[F](g)" using L unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
+qed (rule big.cong_bigtheta)
+
+lemma big_prod:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (g x)"
+ shows "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>y. \<Prod>x\<in>A. g x y)"
+ using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult)
+
+lemma big_prod_in_1:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> L F (\<lambda>_. 1)"
+ shows "(\<lambda>y. \<Prod>x\<in>A. f x y) \<in> L F (\<lambda>_. 1)"
+ using assms by (induction A rule: infinite_finite_induct) (auto intro!: big.mult_in_1)
+
+end
+
+
+context landau_symbol
+begin
+
+lemma plus_absorb1:
+ assumes "f \<in> o[F](g)"
+ shows "L F (\<lambda>x. f x + g x) = L F (g)"
+proof (intro equalityI)
+ from plus_subset1 and assms show "L F g \<subseteq> L F (\<lambda>x. f x + g x)" .
+ from landau_o.small.plus_subset1[OF assms] and assms have "(\<lambda>x. -f x) \<in> o[F](\<lambda>x. f x + g x)"
+ by (auto simp: landau_o.small.uminus_in_iff)
+ from plus_subset1[OF this] show "L F (\<lambda>x. f x + g x) \<subseteq> L F (g)" by simp
+qed
+
+lemma plus_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x + g x) = L F (f)"
+ using plus_absorb1[of g F f] by (simp add: add.commute)
+
+lemma diff_absorb1: "f \<in> o[F](g) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (g)"
+ by (simp only: diff_conv_add_uminus plus_absorb1 landau_o.small.uminus uminus)
+
+lemma diff_absorb2: "g \<in> o[F](f) \<Longrightarrow> L F (\<lambda>x. f x - g x) = L F (f)"
+ by (simp only: diff_conv_add_uminus plus_absorb2 landau_o.small.uminus_in_iff)
+
+lemmas absorb = plus_absorb1 plus_absorb2 diff_absorb1 diff_absorb2
+
+end
+
+
+lemma bigthetaI [intro]: "f \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> \<Theta>[F](g)"
+ unfolding bigtheta_def bigomega_def by blast
+
+lemma bigthetaD1 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> O[F](g)"
+ and bigthetaD2 [dest]: "f \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> \<Omega>[F](g)"
+ unfolding bigtheta_def bigo_def bigomega_def by blast+
+
+lemma bigtheta_refl [simp]: "f \<in> \<Theta>[F](f)"
+ unfolding bigtheta_def by simp
+
+lemma bigtheta_sym: "f \<in> \<Theta>[F](g) \<longleftrightarrow> g \<in> \<Theta>[F](f)"
+ unfolding bigtheta_def by (auto simp: bigomega_iff_bigo)
+
+lemmas landau_flip =
+ bigomega_iff_bigo[symmetric] smallomega_iff_smallo[symmetric]
+ bigomega_iff_bigo smallomega_iff_smallo bigtheta_sym
+
+
+interpretation landau_theta: landau_symbol bigtheta bigtheta bigtheta
+proof
+ fix f g :: "'a \<Rightarrow> 'b" and F
+ assume "f \<in> o[F](g)"
+ hence "O[F](g) \<subseteq> O[F](\<lambda>x. f x + g x)" "\<Omega>[F](g) \<subseteq> \<Omega>[F](\<lambda>x. f x + g x)"
+ by (rule landau_o.big.plus_subset1 landau_omega.big.plus_subset1)+
+ thus "\<Theta>[F](g) \<subseteq> \<Theta>[F](\<lambda>x. f x + g x)" unfolding bigtheta_def by blast
+next
+ fix f g :: "'a \<Rightarrow> 'b" and F
+ assume "f \<in> \<Theta>[F](g)"
+ thus A: "\<Theta>[F](f) = \<Theta>[F](g)"
+ apply (subst (1 2) bigtheta_def)
+ apply (subst landau_o.big.cong_bigtheta landau_omega.big.cong_bigtheta, assumption)+
+ apply (rule refl)
+ done
+ thus "\<Theta>[F](f) \<subseteq> \<Theta>[F](g)" by simp
+ fix h :: "'a \<Rightarrow> 'b"
+ show "f \<in> \<Theta>[F](h) \<longleftrightarrow> g \<in> \<Theta>[F](h)" by (subst (1 2) bigtheta_sym) (simp add: A)
+next
+ fix f g h :: "'a \<Rightarrow> 'b" and F
+ assume "f \<in> \<Theta>[F](g)" "g \<in> \<Theta>[F](h)"
+ thus "f \<in> \<Theta>[F](h)" unfolding bigtheta_def
+ by (blast intro: landau_o.big.trans landau_omega.big.trans)
+next
+ fix f :: "'a \<Rightarrow> 'b" and F1 F2 :: "'a filter"
+ assume "F1 \<le> F2"
+ thus "\<Theta>[F2](f) \<subseteq> \<Theta>[F1](f)"
+ by (auto simp: bigtheta_def intro: landau_o.big.filter_mono landau_omega.big.filter_mono)
+qed (auto simp: bigtheta_def landau_o.big.norm_iff
+ landau_o.big.cmult landau_omega.big.cmult
+ landau_o.big.cmult_in_iff landau_omega.big.cmult_in_iff
+ landau_o.big.in_cong landau_omega.big.in_cong
+ landau_o.big.mult landau_omega.big.mult
+ landau_o.big.inverse landau_omega.big.inverse
+ landau_o.big.compose landau_omega.big.compose
+ landau_o.big.bot' landau_omega.big.bot'
+ landau_o.big.in_filtermap_iff landau_omega.big.in_filtermap_iff
+ landau_o.big.sup landau_omega.big.sup
+ landau_o.big.filtercomap landau_omega.big.filtercomap
+ dest: landau_o.big.cong landau_omega.big.cong)
+
+lemmas landau_symbols =
+ landau_o.big.landau_symbol_axioms landau_o.small.landau_symbol_axioms
+ landau_omega.big.landau_symbol_axioms landau_omega.small.landau_symbol_axioms
+ landau_theta.landau_symbol_axioms
+
+lemma bigoI [intro]:
+ assumes "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
+ shows "f \<in> O[F](g)"
+proof (rule landau_o.bigI)
+ show "max 1 c > 0" by simp
+ note assms
+ moreover have "\<And>x. c * (norm (g x)) \<le> max 1 c * (norm (g x))" by (simp add: mult_right_mono)
+ ultimately show "eventually (\<lambda>x. (norm (f x)) \<le> max 1 c * (norm (g x))) F"
+ by (auto elim!: eventually_mono dest: order.trans)
+qed
+
+lemma smallomegaD [dest]:
+ assumes "f \<in> \<omega>[F](g)"
+ shows "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
+proof (cases "c > 0")
+ case False
+ show ?thesis
+ by (intro always_eventually allI, rule order.trans[of _ 0])
+ (insert False, auto intro!: mult_nonpos_nonneg)
+qed (blast dest: landau_omega.smallD[OF assms, of c])
+
+
+lemma bigthetaI':
+ assumes "c1 > 0" "c2 > 0"
+ assumes "eventually (\<lambda>x. c1 * (norm (g x)) \<le> (norm (f x)) \<and> (norm (f x)) \<le> c2 * (norm (g x))) F"
+ shows "f \<in> \<Theta>[F](g)"
+apply (rule bigthetaI)
+apply (rule landau_o.bigI[OF assms(2)]) using assms(3) apply (eventually_elim, simp)
+apply (rule landau_omega.bigI[OF assms(1)]) using assms(3) apply (eventually_elim, simp)
+done
+
+lemma bigthetaI_cong: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> f \<in> \<Theta>[F](g)"
+ by (intro bigthetaI'[of 1 1]) (auto elim!: eventually_mono)
+
+lemma (in landau_symbol) ev_eq_trans1:
+ "f \<in> L F (\<lambda>x. g x (h x)) \<Longrightarrow> eventually (\<lambda>x. h x = h' x) F \<Longrightarrow> f \<in> L F (\<lambda>x. g x (h' x))"
+ by (rule bigtheta_trans1[OF _ bigthetaI_cong]) (auto elim!: eventually_mono)
+
+lemma (in landau_symbol) ev_eq_trans2:
+ "eventually (\<lambda>x. f x = f' x) F \<Longrightarrow> (\<lambda>x. g x (f' x)) \<in> L F (h) \<Longrightarrow> (\<lambda>x. g x (f x)) \<in> L F (h)"
+ by (rule bigtheta_trans2[OF bigthetaI_cong]) (auto elim!: eventually_mono)
+
+declare landau_o.smallI landau_omega.bigI landau_omega.smallI [intro]
+declare landau_o.bigE landau_omega.bigE [elim]
+declare landau_o.smallD
+
+lemma (in landau_symbol) bigtheta_trans1':
+ "f \<in> L F (g) \<Longrightarrow> h \<in> \<Theta>[F](g) \<Longrightarrow> f \<in> L F (h)"
+ by (subst cong_bigtheta[symmetric]) (simp add: bigtheta_sym)
+
+lemma (in landau_symbol) bigtheta_trans2':
+ "g \<in> \<Theta>[F](f) \<Longrightarrow> g \<in> L F (h) \<Longrightarrow> f \<in> L F (h)"
+ by (rule bigtheta_trans2, subst bigtheta_sym)
+
+lemma bigo_bigomega_trans: "f \<in> O[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> O[F](h)"
+ and bigo_smallomega_trans: "f \<in> O[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
+ and smallo_bigomega_trans: "f \<in> o[F](g) \<Longrightarrow> h \<in> \<Omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
+ and smallo_smallomega_trans: "f \<in> o[F](g) \<Longrightarrow> h \<in> \<omega>[F](g) \<Longrightarrow> f \<in> o[F](h)"
+ and bigomega_bigo_trans: "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<Omega>[F](h)"
+ and bigomega_smallo_trans: "f \<in> \<Omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
+ and smallomega_bigo_trans: "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> O[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
+ and smallomega_smallo_trans: "f \<in> \<omega>[F](g) \<Longrightarrow> h \<in> o[F](g) \<Longrightarrow> f \<in> \<omega>[F](h)"
+ by (unfold bigomega_iff_bigo smallomega_iff_smallo)
+ (erule (1) landau_o.big_trans landau_o.big_small_trans landau_o.small_big_trans
+ landau_o.big_trans landau_o.small_trans)+
+
+lemmas landau_trans_lift [trans] =
+ landau_symbols[THEN landau_symbol.lift_trans]
+ landau_symbols[THEN landau_symbol.lift_trans']
+ landau_symbols[THEN landau_symbol.lift_trans_bigtheta]
+ landau_symbols[THEN landau_symbol.lift_trans_bigtheta']
+
+lemmas landau_mult_1_trans [trans] =
+ landau_o.mult_1_trans landau_omega.mult_1_trans
+
+lemmas landau_trans [trans] =
+ landau_symbols[THEN landau_symbol.bigtheta_trans1]
+ landau_symbols[THEN landau_symbol.bigtheta_trans2]
+ landau_symbols[THEN landau_symbol.bigtheta_trans1']
+ landau_symbols[THEN landau_symbol.bigtheta_trans2']
+ landau_symbols[THEN landau_symbol.ev_eq_trans1]
+ landau_symbols[THEN landau_symbol.ev_eq_trans2]
+
+ landau_o.big_trans landau_o.small_trans landau_o.small_big_trans landau_o.big_small_trans
+ landau_omega.big_trans landau_omega.small_trans
+ landau_omega.small_big_trans landau_omega.big_small_trans
+
+ bigo_bigomega_trans bigo_smallomega_trans smallo_bigomega_trans smallo_smallomega_trans
+ bigomega_bigo_trans bigomega_smallo_trans smallomega_bigo_trans smallomega_smallo_trans
+
+lemma bigtheta_inverse [simp]:
+ shows "(\<lambda>x. inverse (f x)) \<in> \<Theta>[F](\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<in> \<Theta>[F](g)"
+proof-
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)"
+ then guess c1 c2 :: real unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
+ note c = this
+ from c(3) have "inverse c2 > 0" by simp
+ moreover from c(2,4)
+ have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))) F"
+ proof eventually_elim
+ fix x assume A: "(norm (f x)) \<le> c1 * (norm (g x))" "c2 * (norm (g x)) \<le> (norm (f x))"
+ from A c(1,3) have "f x = 0 \<longleftrightarrow> g x = 0" by (auto simp: field_simps mult_le_0_iff)
+ with A c(1,3) show "norm (inverse (f x)) \<le> inverse c2 * norm (inverse (g x))"
+ by (force simp: field_simps norm_inverse norm_divide)
+ qed
+ ultimately have "(\<lambda>x. inverse (f x)) \<in> O[F](\<lambda>x. inverse (g x))" by (rule landau_o.bigI)
+ }
+ thus ?thesis unfolding bigtheta_def
+ by (force simp: bigomega_iff_bigo bigtheta_sym)
+qed
+
+lemma bigtheta_divide:
+ assumes "f1 \<in> \<Theta>(f2)" "g1 \<in> \<Theta>(g2)"
+ shows "(\<lambda>x. f1 x / g1 x) \<in> \<Theta>(\<lambda>x. f2 x / g2 x)"
+ by (subst (1 2) divide_inverse, intro landau_theta.mult) (simp_all add: bigtheta_inverse assms)
+
+lemma eventually_nonzero_bigtheta:
+ assumes "f \<in> \<Theta>[F](g)"
+ shows "eventually (\<lambda>x. f x \<noteq> 0) F \<longleftrightarrow> eventually (\<lambda>x. g x \<noteq> 0) F"
+proof-
+ {
+ fix f g :: "'a \<Rightarrow> 'b" and F assume A: "f \<in> \<Theta>[F](g)" and B: "eventually (\<lambda>x. f x \<noteq> 0) F"
+ from A guess c1 c2 unfolding bigtheta_def by (elim landau_o.bigE landau_omega.bigE IntE)
+ from B this(2,4) have "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim auto
+ }
+ with assms show ?thesis by (force simp: bigtheta_sym)
+qed
+
+
+subsection {* Landau symbols and limits *}
+
+lemma bigoI_tendsto_norm:
+ fixes f g
+ assumes "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
+ assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+ shows "f \<in> O[F](g)"
+proof (rule bigoI)
+ from assms have "eventually (\<lambda>x. dist (norm (f x / g x)) c < 1) F"
+ using tendstoD by force
+ thus "eventually (\<lambda>x. (norm (f x)) \<le> (norm c + 1) * (norm (g x))) F"
+ unfolding dist_real_def using assms(2)
+ proof eventually_elim
+ case (elim x)
+ have "(norm (f x)) - norm c * (norm (g x)) \<le> norm ((norm (f x)) - c * (norm (g x)))"
+ unfolding norm_mult [symmetric] using norm_triangle_ineq2[of "norm (f x)" "c * norm (g x)"]
+ by (simp add: norm_mult abs_mult)
+ also from elim have "\<dots> = norm (norm (g x)) * norm (norm (f x / g x) - c)"
+ unfolding norm_mult [symmetric] by (simp add: algebra_simps norm_divide)
+ also from elim have "norm (norm (f x / g x) - c) \<le> 1" by simp
+ hence "norm (norm (g x)) * norm (norm (f x / g x) - c) \<le> norm (norm (g x)) * 1"
+ by (rule mult_left_mono) simp_all
+ finally show ?case by (simp add: algebra_simps)
+ qed
+qed
+
+lemma bigoI_tendsto:
+ assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
+ assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+ shows "f \<in> O[F](g)"
+ using assms by (rule bigoI_tendsto_norm[OF tendsto_norm])
+
+lemma bigomegaI_tendsto_norm:
+ assumes c_not_0: "(c::real) \<noteq> 0"
+ assumes lim: "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
+ shows "f \<in> \<Omega>[F](g)"
+proof (cases "F = bot")
+ case False
+ show ?thesis
+ proof (rule landau_omega.bigI)
+ from lim have "c \<ge> 0" by (rule tendsto_lowerbound) (insert False, simp_all)
+ with c_not_0 have "c > 0" by simp
+ with c_not_0 show "c/2 > 0" by simp
+ from lim have ev: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<epsilon>) F"
+ by (subst (asm) tendsto_iff) (simp add: dist_real_def)
+ from ev[OF `c/2 > 0`] show "eventually (\<lambda>x. (norm (f x)) \<ge> c/2 * (norm (g x))) F"
+ proof (eventually_elim)
+ fix x assume B: "norm (norm (f x / g x) - c) < c / 2"
+ from B have g: "g x \<noteq> 0" by auto
+ from B have "-c/2 < -norm (norm (f x / g x) - c)" by simp
+ also have "... \<le> norm (f x / g x) - c" by simp
+ finally show "(norm (f x)) \<ge> c/2 * (norm (g x))" using g
+ by (simp add: field_simps norm_mult norm_divide)
+ qed
+ qed
+qed simp
+
+lemma bigomegaI_tendsto:
+ assumes c_not_0: "(c::real) \<noteq> 0"
+ assumes lim: "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
+ shows "f \<in> \<Omega>[F](g)"
+ by (rule bigomegaI_tendsto_norm[OF _ tendsto_norm, of c]) (insert assms, simp_all)
+
+lemma smallomegaI_filterlim_at_top_norm:
+ assumes lim: "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
+ shows "f \<in> \<omega>[F](g)"
+proof (rule landau_omega.smallI)
+ fix c :: real assume c_pos: "c > 0"
+ from lim have ev: "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F"
+ by (subst (asm) filterlim_at_top) simp
+ thus "eventually (\<lambda>x. (norm (f x)) \<ge> c * (norm (g x))) F"
+ proof eventually_elim
+ fix x assume A: "norm (f x / g x) \<ge> c"
+ from A c_pos have "g x \<noteq> 0" by auto
+ with A show "(norm (f x)) \<ge> c * (norm (g x))" by (simp add: field_simps norm_divide)
+ qed
+qed
+
+lemma smallomegaI_filterlim_at_infinity:
+ assumes lim: "filterlim (\<lambda>x. f x / g x) at_infinity F"
+ shows "f \<in> \<omega>[F](g)"
+proof (rule smallomegaI_filterlim_at_top_norm)
+ from lim show "filterlim (\<lambda>x. norm (f x / g x)) at_top F"
+ by (rule filterlim_at_infinity_imp_norm_at_top)
+qed
+
+lemma smallomegaD_filterlim_at_top_norm:
+ assumes "f \<in> \<omega>[F](g)"
+ assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+ shows "LIM x F. norm (f x / g x) :> at_top"
+proof (subst filterlim_at_top_gt, clarify)
+ fix c :: real assume c: "c > 0"
+ from landau_omega.smallD[OF assms(1) this] assms(2)
+ show "eventually (\<lambda>x. norm (f x / g x) \<ge> c) F"
+ by eventually_elim (simp add: field_simps norm_divide)
+qed
+
+lemma smallomegaD_filterlim_at_infinity:
+ assumes "f \<in> \<omega>[F](g)"
+ assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+ shows "LIM x F. f x / g x :> at_infinity"
+ using assms by (intro filterlim_norm_at_top_imp_at_infinity smallomegaD_filterlim_at_top_norm)
+
+lemma smallomega_1_conv_filterlim: "f \<in> \<omega>[F](\<lambda>_. 1) \<longleftrightarrow> filterlim f at_infinity F"
+ by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)
+
+lemma smalloI_tendsto:
+ assumes lim: "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
+ assumes "eventually (\<lambda>x. g x \<noteq> 0) F"
+ shows "f \<in> o[F](g)"
+proof (rule landau_o.smallI)
+ fix c :: real assume c_pos: "c > 0"
+ from c_pos and lim have ev: "eventually (\<lambda>x. norm (f x / g x) < c) F"
+ by (subst (asm) tendsto_iff) (simp add: dist_real_def)
+ with assms(2) show "eventually (\<lambda>x. (norm (f x)) \<le> c * (norm (g x))) F"
+ by eventually_elim (simp add: field_simps norm_divide)
+qed
+
+lemma smalloD_tendsto:
+ assumes "f \<in> o[F](g)"
+ shows "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
+unfolding tendsto_iff
+proof clarify
+ fix e :: real assume e: "e > 0"
+ hence "e/2 > 0" by simp
+ from landau_o.smallD[OF assms this] show "eventually (\<lambda>x. dist (f x / g x) 0 < e) F"
+ proof eventually_elim
+ fix x assume "(norm (f x)) \<le> e/2 * (norm (g x))"
+ with e have "dist (f x / g x) 0 \<le> e/2"
+ by (cases "g x = 0") (simp_all add: dist_real_def norm_divide field_simps)
+ also from e have "... < e" by simp
+ finally show "dist (f x / g x) 0 < e" by simp
+ qed
+qed
+
+lemma bigthetaI_tendsto_norm:
+ assumes c_not_0: "(c::real) \<noteq> 0"
+ assumes lim: "((\<lambda>x. norm (f x / g x)) \<longlongrightarrow> c) F"
+ shows "f \<in> \<Theta>[F](g)"
+proof (rule bigthetaI)
+ from c_not_0 have "\<bar>c\<bar> > 0" by simp
+ with lim have "eventually (\<lambda>x. norm (norm (f x / g x) - c) < \<bar>c\<bar>) F"
+ by (subst (asm) tendsto_iff) (simp add: dist_real_def)
+ hence g: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim (auto simp add: field_simps)
+
+ from lim g show "f \<in> O[F](g)" by (rule bigoI_tendsto_norm)
+ from c_not_0 and lim show "f \<in> \<Omega>[F](g)" by (rule bigomegaI_tendsto_norm)
+qed
+
+lemma bigthetaI_tendsto:
+ assumes c_not_0: "(c::real) \<noteq> 0"
+ assumes lim: "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F"
+ shows "f \<in> \<Theta>[F](g)"
+ using assms by (intro bigthetaI_tendsto_norm[OF _ tendsto_norm, of "c"]) simp_all
+
+lemma tendsto_add_smallo:
+ assumes "(f1 \<longlongrightarrow> a) F"
+ assumes "f2 \<in> o[F](f1)"
+ shows "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
+proof (subst filterlim_cong[OF refl refl])
+ from landau_o.smallD[OF assms(2) zero_less_one]
+ have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)) F" by simp
+ thus "eventually (\<lambda>x. f1 x + f2 x = f1 x * (1 + f2 x / f1 x)) F"
+ by eventually_elim (auto simp: field_simps)
+next
+ from assms(1) show "((\<lambda>x. f1 x * (1 + f2 x / f1 x)) \<longlongrightarrow> a) F"
+ by (force intro: tendsto_eq_intros smalloD_tendsto[OF assms(2)])
+qed
+
+lemma tendsto_diff_smallo:
+ shows "(f1 \<longlongrightarrow> a) F \<Longrightarrow> f2 \<in> o[F](f1) \<Longrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
+ using tendsto_add_smallo[of f1 a F "\<lambda>x. -f2 x"] by simp
+
+lemma tendsto_add_smallo_iff:
+ assumes "f2 \<in> o[F](f1)"
+ shows "(f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
+proof
+ assume "((\<lambda>x. f1 x + f2 x) \<longlongrightarrow> a) F"
+ hence "((\<lambda>x. f1 x + f2 x - f2 x) \<longlongrightarrow> a) F"
+ by (rule tendsto_diff_smallo) (simp add: landau_o.small.plus_absorb2 assms)
+ thus "(f1 \<longlongrightarrow> a) F" by simp
+qed (rule tendsto_add_smallo[OF _ assms])
+
+lemma tendsto_diff_smallo_iff:
+ shows "f2 \<in> o[F](f1) \<Longrightarrow> (f1 \<longlongrightarrow> a) F \<longleftrightarrow> ((\<lambda>x. f1 x - f2 x) \<longlongrightarrow> a) F"
+ using tendsto_add_smallo_iff[of "\<lambda>x. -f2 x" F f1 a] by simp
+
+lemma tendsto_divide_smallo:
+ assumes "((\<lambda>x. f1 x / g1 x) \<longlongrightarrow> a) F"
+ assumes "f2 \<in> o[F](f1)" "g2 \<in> o[F](g1)"
+ assumes "eventually (\<lambda>x. g1 x \<noteq> 0) F"
+ shows "((\<lambda>x. (f1 x + f2 x) / (g1 x + g2 x)) \<longlongrightarrow> a) F" (is "(?f \<longlongrightarrow> _) _")
+proof (subst tendsto_cong)
+ let ?f' = "\<lambda>x. (f1 x / g1 x) * (1 + f2 x / f1 x) / (1 + g2 x / g1 x)"
+
+ have "(?f' \<longlongrightarrow> a * (1 + 0) / (1 + 0)) F"
+ by (rule tendsto_mult tendsto_divide tendsto_add assms tendsto_const
+ smalloD_tendsto[OF assms(2)] smalloD_tendsto[OF assms(3)])+ simp_all
+ thus "(?f' \<longlongrightarrow> a) F" by simp
+
+ have "(1/2::real) > 0" by simp
+ from landau_o.smallD[OF assms(2) this] landau_o.smallD[OF assms(3) this]
+ have "eventually (\<lambda>x. norm (f2 x) \<le> norm (f1 x)/2) F"
+ "eventually (\<lambda>x. norm (g2 x) \<le> norm (g1 x)/2) F" by simp_all
+ with assms(4) show "eventually (\<lambda>x. ?f x = ?f' x) F"
+ proof eventually_elim
+ fix x assume A: "norm (f2 x) \<le> norm (f1 x)/2" and
+ B: "norm (g2 x) \<le> norm (g1 x)/2" and C: "g1 x \<noteq> 0"
+ show "?f x = ?f' x"
+ proof (cases "f1 x = 0")
+ assume D: "f1 x \<noteq> 0"
+ from D have "f1 x + f2 x = f1 x * (1 + f2 x/f1 x)" by (simp add: field_simps)
+ moreover from C have "g1 x + g2 x = g1 x * (1 + g2 x/g1 x)" by (simp add: field_simps)
+ ultimately have "?f x = (f1 x * (1 + f2 x/f1 x)) / (g1 x * (1 + g2 x/g1 x))" by (simp only:)
+ also have "... = ?f' x" by simp
+ finally show ?thesis .
+ qed (insert A, simp)
+ qed
+qed
+
+
+lemma bigo_powr:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes "f \<in> O[F](g)" "p \<ge> 0"
+ shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)"
+proof-
+ from assms(1) guess c by (elim landau_o.bigE landau_omega.bigE IntE)
+ note c = this
+ from c(2) assms(2) have "eventually (\<lambda>x. (norm (f x)) powr p \<le> (c * (norm (g x))) powr p) F"
+ by (auto elim!: eventually_mono intro!: powr_mono2)
+ thus "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" using c(1)
+ by (intro bigoI[of _ "c powr p"]) (simp_all add: powr_mult)
+qed
+
+lemma smallo_powr:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes "f \<in> o[F](g)" "p > 0"
+ shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)"
+proof (rule landau_o.smallI)
+ fix c :: real assume c: "c > 0"
+ hence "c powr (1/p) > 0" by simp
+ from landau_o.smallD[OF assms(1) this]
+ show "eventually (\<lambda>x. norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)) F"
+ proof eventually_elim
+ fix x assume "(norm (f x)) \<le> c powr (1 / p) * (norm (g x))"
+ with assms(2) have "(norm (f x)) powr p \<le> (c powr (1 / p) * (norm (g x))) powr p"
+ by (intro powr_mono2) simp_all
+ also from assms(2) c have "... = c * (norm (g x)) powr p"
+ by (simp add: field_simps powr_mult powr_powr)
+ finally show "norm (\<bar>f x\<bar> powr p) \<le> c * norm (\<bar>g x\<bar> powr p)" by simp
+ qed
+qed
+
+lemma smallo_powr_nonneg:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes "f \<in> o[F](g)" "p > 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
+ shows "(\<lambda>x. f x powr p) \<in> o[F](\<lambda>x. g x powr p)"
+proof -
+ from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)"
+ by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+ also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> o[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro smallo_powr) fact+
+ also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
+ by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+ finally show ?thesis .
+qed
+
+lemma bigtheta_powr:
+ fixes f :: "'a \<Rightarrow> real"
+ shows "f \<in> \<Theta>[F](g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>g x\<bar> powr p)"
+apply (cases "p < 0")
+apply (subst bigtheta_inverse[symmetric], subst (1 2) powr_minus[symmetric])
+unfolding bigtheta_def apply (auto simp: bigomega_iff_bigo intro!: bigo_powr)
+done
+
+lemma bigo_powr_nonneg:
+ fixes f :: "'a \<Rightarrow> real"
+ assumes "f \<in> O[F](g)" "p \<ge> 0" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
+ shows "(\<lambda>x. f x powr p) \<in> O[F](\<lambda>x. g x powr p)"
+proof -
+ from assms(3) have "(\<lambda>x. f x powr p) \<in> \<Theta>[F](\<lambda>x. \<bar>f x\<bar> powr p)"
+ by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+ also have "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> O[F](\<lambda>x. \<bar>g x\<bar> powr p)" by (intro bigo_powr) fact+
+ also from assms(4) have "(\<lambda>x. \<bar>g x\<bar> powr p) \<in> \<Theta>[F](\<lambda>x. g x powr p)"
+ by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+ finally show ?thesis .
+qed
+
+lemma zero_in_smallo [simp]: "(\<lambda>_. 0) \<in> o[F](f)"
+ by (intro landau_o.smallI) simp_all
+
+lemma zero_in_bigo [simp]: "(\<lambda>_. 0) \<in> O[F](f)"
+ by (intro landau_o.bigI[of 1]) simp_all
+
+lemma in_bigomega_zero [simp]: "f \<in> \<Omega>[F](\<lambda>x. 0)"
+ by (rule landau_omega.bigI[of 1]) simp_all
+
+lemma in_smallomega_zero [simp]: "f \<in> \<omega>[F](\<lambda>x. 0)"
+ by (simp add: smallomega_iff_smallo)
+
+
+lemma in_smallo_zero_iff [simp]: "f \<in> o[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+proof
+ assume "f \<in> o[F](\<lambda>_. 0)"
+ from landau_o.smallD[OF this, of 1] show "eventually (\<lambda>x. f x = 0) F" by simp
+next
+ assume "eventually (\<lambda>x. f x = 0) F"
+ hence "\<forall>c>0. eventually (\<lambda>x. (norm (f x)) \<le> c * \<bar>0\<bar>) F" by simp
+ thus "f \<in> o[F](\<lambda>_. 0)" unfolding smallo_def by simp
+qed
+
+lemma in_bigo_zero_iff [simp]: "f \<in> O[F](\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+proof
+ assume "f \<in> O[F](\<lambda>_. 0)"
+ thus "eventually (\<lambda>x. f x = 0) F" by (elim landau_o.bigE) simp
+next
+ assume "eventually (\<lambda>x. f x = 0) F"
+ hence "eventually (\<lambda>x. (norm (f x)) \<le> 1 * \<bar>0\<bar>) F" by simp
+ thus "f \<in> O[F](\<lambda>_. 0)" by (intro landau_o.bigI[of 1]) simp_all
+qed
+
+lemma zero_in_smallomega_iff [simp]: "(\<lambda>_. 0) \<in> \<omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+ by (simp add: smallomega_iff_smallo)
+
+lemma zero_in_bigomega_iff [simp]: "(\<lambda>_. 0) \<in> \<Omega>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+ by (simp add: bigomega_iff_bigo)
+
+lemma zero_in_bigtheta_iff [simp]: "(\<lambda>_. 0) \<in> \<Theta>[F](f) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+ unfolding bigtheta_def by simp
+
+lemma in_bigtheta_zero_iff [simp]: "f \<in> \<Theta>[F](\<lambda>x. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+ unfolding bigtheta_def by simp
+
+
+lemma cmult_in_bigo_iff [simp]: "(\<lambda>x. c * f x) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
+ and cmult_in_bigo_iff' [simp]: "(\<lambda>x. f x * c) \<in> O[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> O[F](g)"
+ and cmult_in_smallo_iff [simp]: "(\<lambda>x. c * f x) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
+ and cmult_in_smallo_iff' [simp]: "(\<lambda>x. f x * c) \<in> o[F](g) \<longleftrightarrow> c = 0 \<or> f \<in> o[F](g)"
+ by (cases "c = 0", simp, simp)+
+
+lemma bigo_const [simp]: "(\<lambda>_. c) \<in> O[F](\<lambda>_. 1)" by (rule bigoI[of _ "norm c"]) simp
+
+lemma bigo_const_iff [simp]: "(\<lambda>_. c1) \<in> O[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 = 0 \<or> c2 \<noteq> 0"
+ by (cases "c1 = 0"; cases "c2 = 0")
+ (auto simp: bigo_def eventually_False intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
+
+lemma bigomega_const_iff [simp]: "(\<lambda>_. c1) \<in> \<Omega>[F](\<lambda>_. c2) \<longleftrightarrow> F = bot \<or> c1 \<noteq> 0 \<or> c2 = 0"
+ by (cases "c1 = 0"; cases "c2 = 0")
+ (auto simp: bigomega_def eventually_False mult_le_0_iff
+ intro: exI[of _ 1] exI[of _ "norm c1 / norm c2"])
+
+lemma smallo_real_nat_transfer:
+ "(f :: real \<Rightarrow> real) \<in> o(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> o(\<lambda>x. g (real x))"
+ by (rule landau_o.small.compose[OF _ filterlim_real_sequentially])
+
+lemma bigo_real_nat_transfer:
+ "(f :: real \<Rightarrow> real) \<in> O(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> O(\<lambda>x. g (real x))"
+ by (rule landau_o.big.compose[OF _ filterlim_real_sequentially])
+
+lemma smallomega_real_nat_transfer:
+ "(f :: real \<Rightarrow> real) \<in> \<omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<omega>(\<lambda>x. g (real x))"
+ by (rule landau_omega.small.compose[OF _ filterlim_real_sequentially])
+
+lemma bigomega_real_nat_transfer:
+ "(f :: real \<Rightarrow> real) \<in> \<Omega>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Omega>(\<lambda>x. g (real x))"
+ by (rule landau_omega.big.compose[OF _ filterlim_real_sequentially])
+
+lemma bigtheta_real_nat_transfer:
+ "(f :: real \<Rightarrow> real) \<in> \<Theta>(g) \<Longrightarrow> (\<lambda>x::nat. f (real x)) \<in> \<Theta>(\<lambda>x. g (real x))"
+ unfolding bigtheta_def using bigo_real_nat_transfer bigomega_real_nat_transfer by blast
+
+lemmas landau_real_nat_transfer [intro] =
+ bigo_real_nat_transfer smallo_real_nat_transfer bigomega_real_nat_transfer
+ smallomega_real_nat_transfer bigtheta_real_nat_transfer
+
+
+lemma landau_symbol_if_at_top_eq [simp]:
+ assumes "landau_symbol L L' Lr"
+ shows "L at_top (\<lambda>x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)"
+apply (rule landau_symbol.cong[OF assms])
+using less_add_one[of a] apply (auto intro: eventually_mono eventually_ge_at_top[of "a + 1"])
+done
+
+lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq]
+
+
+
+lemma sum_in_smallo:
+ assumes "f \<in> o[F](h)" "g \<in> o[F](h)"
+ shows "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)"
+proof-
+ {
+ fix f g assume fg: "f \<in> o[F](h)" "g \<in> o[F](h)"
+ have "(\<lambda>x. f x + g x) \<in> o[F](h)"
+ proof (rule landau_o.smallI)
+ fix c :: real assume "c > 0"
+ hence "c/2 > 0" by simp
+ from fg[THEN landau_o.smallD[OF _ this]]
+ show "eventually (\<lambda>x. norm (f x + g x) \<le> c * (norm (h x))) F"
+ by eventually_elim (auto intro: order.trans[OF norm_triangle_ineq])
+ qed
+ }
+ from this[of f g] this[of f "\<lambda>x. -g x"] assms
+ show "(\<lambda>x. f x + g x) \<in> o[F](h)" "(\<lambda>x. f x - g x) \<in> o[F](h)" by simp_all
+qed
+
+lemma big_sum_in_smallo:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> o[F](g)"
+ shows "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> o[F](g)"
+ using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_smallo)
+
+lemma sum_in_bigo:
+ assumes "f \<in> O[F](h)" "g \<in> O[F](h)"
+ shows "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)"
+proof-
+ {
+ fix f g assume fg: "f \<in> O[F](h)" "g \<in> O[F](h)"
+ from fg(1) guess c1 by (elim landau_o.bigE) note c1 = this
+ from fg(2) guess c2 by (elim landau_o.bigE) note c2 = this
+ from c1(2) c2(2) have "eventually (\<lambda>x. norm (f x + g x) \<le> (c1 + c2) * (norm (h x))) F"
+ by eventually_elim (auto simp: algebra_simps intro: order.trans[OF norm_triangle_ineq])
+ hence "(\<lambda>x. f x + g x) \<in> O[F](h)" by (rule bigoI)
+ }
+ from this[of f g] this[of f "\<lambda>x. -g x"] assms
+ show "(\<lambda>x. f x + g x) \<in> O[F](h)" "(\<lambda>x. f x - g x) \<in> O[F](h)" by simp_all
+qed
+
+lemma big_sum_in_bigo:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> O[F](g)"
+ shows "(\<lambda>x. sum (\<lambda>y. f y x) A) \<in> O[F](g)"
+ using assms by (induction A rule: infinite_finite_induct) (auto intro: sum_in_bigo)
+
+context landau_symbol
+begin
+
+lemma mult_cancel_left:
+ assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
+ notes [trans] = bigtheta_trans1 bigtheta_trans2
+ shows "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f2 \<in> L F (g2)"
+proof
+ assume A: "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)"
+ from assms have nz: "eventually (\<lambda>x. f1 x \<noteq> 0) F" by (simp add: eventually_nonzero_bigtheta)
+ hence "f2 \<in> \<Theta>[F](\<lambda>x. f1 x * f2 x / f1 x)"
+ by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+ also from A assms nz have "(\<lambda>x. f1 x * f2 x / f1 x) \<in> L F (\<lambda>x. g1 x * g2 x / f1 x)"
+ by (intro divide_right) simp_all
+ also from assms nz have "(\<lambda>x. g1 x * g2 x / f1 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x / g1 x)"
+ by (intro landau_theta.mult landau_theta.divide) (simp_all add: bigtheta_sym)
+ also from assms have "(\<lambda>x. g1 x * g2 x / g1 x) \<in> \<Theta>[F](g2)"
+ by (intro bigthetaI_cong) (auto elim!: eventually_mono)
+ finally show "f2 \<in> L F (g2)" .
+next
+ assume "f2 \<in> L F (g2)"
+ hence "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. f1 x * g2 x)" by (rule mult_left)
+ also have "(\<lambda>x. f1 x * g2 x) \<in> \<Theta>[F](\<lambda>x. g1 x * g2 x)"
+ by (intro landau_theta.mult_right assms)
+ finally show "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x)" .
+qed
+
+lemma mult_cancel_right:
+ assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
+ shows "(\<lambda>x. f1 x * f2 x) \<in> L F (\<lambda>x. g1 x * g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
+ by (subst (1 2) mult.commute) (rule mult_cancel_left[OF assms])
+
+lemma divide_cancel_right:
+ assumes "f2 \<in> \<Theta>[F](g2)" and "eventually (\<lambda>x. g2 x \<noteq> 0) F"
+ shows "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow> f1 \<in> L F (g1)"
+ by (subst (1 2) divide_inverse, intro mult_cancel_right bigtheta_inverse) (simp_all add: assms)
+
+lemma divide_cancel_left:
+ assumes "f1 \<in> \<Theta>[F](g1)" and "eventually (\<lambda>x. g1 x \<noteq> 0) F"
+ shows "(\<lambda>x. f1 x / f2 x) \<in> L F (\<lambda>x. g1 x / g2 x) \<longleftrightarrow>
+ (\<lambda>x. inverse (f2 x)) \<in> L F (\<lambda>x. inverse (g2 x))"
+ by (simp only: divide_inverse mult_cancel_left[OF assms])
+
+end
+
+
+lemma powr_smallo_iff:
+ assumes "filterlim g at_top F" "F \<noteq> bot"
+ shows "(\<lambda>x. g x powr p :: real) \<in> o[F](\<lambda>x. g x powr q) \<longleftrightarrow> p < q"
+proof-
+ from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
+ hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
+ have B: "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p) \<Longrightarrow> (\<lambda>x. g x powr p) \<notin> o[F](\<lambda>x. g x powr q)"
+ proof
+ assume "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)"
+ from landau_o.big_small_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
+ with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
+ thus False by (simp add: eventually_False assms)
+ qed
+ show ?thesis
+ proof (cases p q rule: linorder_cases)
+ assume "p < q"
+ hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
+ by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+ with `p < q` show ?thesis by auto
+ next
+ assume "p = q"
+ hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
+ with B `p = q` show ?thesis by auto
+ next
+ assume "p > q"
+ hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
+ by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp: powr_diff [symmetric] )
+ with B `p > q` show ?thesis by auto
+ qed
+qed
+
+lemma powr_bigo_iff:
+ assumes "filterlim g at_top F" "F \<noteq> bot"
+ shows "(\<lambda>x. g x powr p :: real) \<in> O[F](\<lambda>x. g x powr q) \<longleftrightarrow> p \<le> q"
+proof-
+ from assms have "eventually (\<lambda>x. g x \<ge> 1) F" by (force simp: filterlim_at_top)
+ hence A: "eventually (\<lambda>x. g x \<noteq> 0) F" by eventually_elim simp
+ have B: "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p) \<Longrightarrow> (\<lambda>x. g x powr p) \<notin> O[F](\<lambda>x. g x powr q)"
+ proof
+ assume "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" "(\<lambda>x. g x powr p) \<in> O[F](\<lambda>x. g x powr q)"
+ from landau_o.small_big_asymmetric[OF this] have "eventually (\<lambda>x. g x = 0) F" by simp
+ with A have "eventually (\<lambda>_::'a. False) F" by eventually_elim simp
+ thus False by (simp add: eventually_False assms)
+ qed
+ show ?thesis
+ proof (cases p q rule: linorder_cases)
+ assume "p < q"
+ hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
+ by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+ with `p < q` show ?thesis by (auto intro: landau_o.small_imp_big)
+ next
+ assume "p = q"
+ hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" by (auto intro!: bigthetaD1)
+ with B `p = q` show ?thesis by auto
+ next
+ assume "p > q"
+ hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
+ by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+ with B `p > q` show ?thesis by (auto intro: landau_o.small_imp_big)
+ qed
+qed
+
+lemma powr_bigtheta_iff:
+ assumes "filterlim g at_top F" "F \<noteq> bot"
+ shows "(\<lambda>x. g x powr p :: real) \<in> \<Theta>[F](\<lambda>x. g x powr q) \<longleftrightarrow> p = q"
+ using assms unfolding bigtheta_def by (auto simp: bigomega_iff_bigo powr_bigo_iff)
+
+
+subsection \<open>Flatness of real functions\<close>
+
+text \<open>
+ Given two real-valued functions $f$ and $g$, we say that $f$ is flatter than $g$ if
+ any power of $f(x)$ is asymptotically dominated by any positive power of $g(x)$. This is
+ a useful notion since, given two products of powers of functions sorted by flatness, we can
+ compare them asymptotically by simply comparing the exponent lists lexicographically.
+
+ A simple sufficient criterion for flatness it that $\ln f(x) \in o(\ln g(x))$, which we show
+ now.
+\<close>
+lemma ln_smallo_imp_flat:
+ fixes f g :: "real \<Rightarrow> real"
+ assumes lim_f: "filterlim f at_top at_top"
+ assumes lim_g: "filterlim g at_top at_top"
+ assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
+ assumes q: "q > 0"
+ shows "(\<lambda>x. f x powr p) \<in> o(\<lambda>x. g x powr q)"
+proof (rule smalloI_tendsto)
+ from lim_f have "eventually (\<lambda>x. f x > 0) at_top"
+ by (simp add: filterlim_at_top_dense)
+ hence f_nz: "eventually (\<lambda>x. f x \<noteq> 0) at_top" by eventually_elim simp
+
+ from lim_g have g_gt_1: "eventually (\<lambda>x. g x > 1) at_top"
+ by (simp add: filterlim_at_top_dense)
+ hence g_nz: "eventually (\<lambda>x. g x \<noteq> 0) at_top" by eventually_elim simp
+ thus "eventually (\<lambda>x. g x powr q \<noteq> 0) at_top"
+ by eventually_elim simp
+
+ have eq: "eventually (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x) =
+ p * ln (f x) - q * ln (g x)) at_top"
+ using g_gt_1 by eventually_elim (insert q, simp_all add: field_simps)
+ have "filterlim (\<lambda>x. q * (p/q * (ln (f x) / ln (g x)) - 1) * ln (g x)) at_bot at_top"
+ by (insert q)
+ (rule filterlim_tendsto_neg_mult_at_bot tendsto_mult
+ tendsto_const tendsto_diff smalloD_tendsto[OF ln_o_ln] lim_g
+ filterlim_compose[OF ln_at_top] | simp)+
+ hence "filterlim (\<lambda>x. p * ln (f x) - q * ln (g x)) at_bot at_top"
+ by (subst (asm) filterlim_cong[OF refl refl eq])
+ hence *: "((\<lambda>x. exp (p * ln (f x) - q * ln (g x))) \<longlongrightarrow> 0) at_top"
+ by (rule filterlim_compose[OF exp_at_bot])
+ have eq: "eventually (\<lambda>x. exp (p * ln (f x) - q * ln (g x)) = f x powr p / g x powr q) at_top"
+ using f_nz g_nz by eventually_elim (simp add: powr_def exp_diff)
+ show "((\<lambda>x. f x powr p / g x powr q) \<longlongrightarrow> 0) at_top"
+ using * by (subst (asm) filterlim_cong[OF refl refl eq])
+qed
+
+lemma ln_smallo_imp_flat':
+ fixes f g :: "real \<Rightarrow> real"
+ assumes lim_f: "filterlim f at_top at_top"
+ assumes lim_g: "filterlim g at_top at_top"
+ assumes ln_o_ln: "(\<lambda>x. ln (f x)) \<in> o(\<lambda>x. ln (g x))"
+ assumes q: "q < 0"
+ shows "(\<lambda>x. g x powr q) \<in> o(\<lambda>x. f x powr p)"
+proof -
+ from lim_f lim_g have "eventually (\<lambda>x. f x > 0) at_top" "eventually (\<lambda>x. g x > 0) at_top"
+ by (simp_all add: filterlim_at_top_dense)
+ hence "eventually (\<lambda>x. f x \<noteq> 0) at_top" "eventually (\<lambda>x. g x \<noteq> 0) at_top"
+ by (auto elim: eventually_mono)
+ moreover from assms have "(\<lambda>x. f x powr -p) \<in> o(\<lambda>x. g x powr -q)"
+ by (intro ln_smallo_imp_flat assms) simp_all
+ ultimately show ?thesis unfolding powr_minus
+ by (simp add: landau_o.small.inverse_cancel)
+qed
+
+
+subsection \<open>Asymptotic Equivalence\<close>
+
+(* TODO Move *)
+lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
+ by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
+
+named_theorems asymp_equiv_intros
+named_theorems asymp_equiv_simps
+
+definition asymp_equiv :: "('a \<Rightarrow> ('b :: real_normed_field)) \<Rightarrow> 'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+ ("_ \<sim>[_] _" [51, 10, 51] 50)
+ where "f \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
+
+abbreviation (input) asymp_equiv_at_top where
+ "asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"
+
+bundle asymp_equiv_notation
+begin
+notation asymp_equiv_at_top (infix "\<sim>" 50)
+end
+
+lemma asymp_equivI: "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F \<Longrightarrow> f \<sim>[F] g"
+ by (simp add: asymp_equiv_def)
+
+lemma asymp_equivD: "f \<sim>[F] g \<Longrightarrow> ((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) \<longlongrightarrow> 1) F"
+ by (simp add: asymp_equiv_def)
+
+lemma asymp_equiv_filtermap_iff:
+ "f \<sim>[filtermap h F] g \<longleftrightarrow> (\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
+ by (simp add: asymp_equiv_def filterlim_filtermap)
+
+lemma asymp_equiv_refl [simp, asymp_equiv_intros]: "f \<sim>[F] f"
+proof (intro asymp_equivI)
+ have "eventually (\<lambda>x. 1 = (if f x = 0 \<and> f x = 0 then 1 else f x / f x)) F"
+ by (intro always_eventually) simp
+ moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
+ ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
+ by (rule Lim_transform_eventually)
+qed
+
+lemma asymp_equiv_symI:
+ assumes "f \<sim>[F] g"
+ shows "g \<sim>[F] f"
+ using tendsto_inverse[OF asymp_equivD[OF assms]]
+ by (auto intro!: asymp_equivI simp: if_distrib conj_commute cong: if_cong)
+
+lemma asymp_equiv_sym: "f \<sim>[F] g \<longleftrightarrow> g \<sim>[F] f"
+ by (blast intro: asymp_equiv_symI)
+
+lemma asymp_equivI':
+ assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> 1) F"
+ shows "f \<sim>[F] g"
+proof (cases "F = bot")
+ case False
+ have "eventually (\<lambda>x. f x \<noteq> 0) F"
+ proof (rule ccontr)
+ assume "\<not>eventually (\<lambda>x. f x \<noteq> 0) F"
+ hence "frequently (\<lambda>x. f x = 0) F" by (simp add: frequently_def)
+ hence "frequently (\<lambda>x. f x / g x = 0) F" by (auto elim!: frequently_elim1)
+ from limit_frequently_eq[OF False this assms] show False by simp_all
+ qed
+ hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"
+ by eventually_elim simp
+ from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def
+ by (rule Lim_transform_eventually)
+qed (simp_all add: asymp_equiv_def)
+
+
+lemma asymp_equiv_cong:
+ assumes "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
+ shows "f1 \<sim>[F] g1 \<longleftrightarrow> f2 \<sim>[F] g2"
+ unfolding asymp_equiv_def
+proof (rule tendsto_cong, goal_cases)
+ case 1
+ from assms show ?case by eventually_elim simp
+qed
+
+lemma asymp_equiv_eventually_zeros:
+ fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
+ assumes "f \<sim>[F] g"
+ shows "eventually (\<lambda>x. f x = 0 \<longleftrightarrow> g x = 0) F"
+proof -
+ let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+ have "eventually (\<lambda>x. x \<noteq> 0) (nhds (1::'b))"
+ by (rule t1_space_nhds) auto
+ hence "eventually (\<lambda>x. x \<noteq> 0) (filtermap ?h F)"
+ using assms unfolding asymp_equiv_def filterlim_def
+ by (rule filter_leD [rotated])
+ hence "eventually (\<lambda>x. ?h x \<noteq> 0) F" by (simp add: eventually_filtermap)
+ thus ?thesis by eventually_elim (auto split: if_splits)
+qed
+
+lemma asymp_equiv_transfer:
+ assumes "f1 \<sim>[F] g1" "eventually (\<lambda>x. f1 x = f2 x) F" "eventually (\<lambda>x. g1 x = g2 x) F"
+ shows "f2 \<sim>[F] g2"
+ using assms(1) asymp_equiv_cong[OF assms(2,3)] by simp
+
+lemma asymp_equiv_transfer_trans [trans]:
+ assumes "(\<lambda>x. f x (h1 x)) \<sim>[F] (\<lambda>x. g x (h1 x))"
+ assumes "eventually (\<lambda>x. h1 x = h2 x) F"
+ shows "(\<lambda>x. f x (h2 x)) \<sim>[F] (\<lambda>x. g x (h2 x))"
+ by (rule asymp_equiv_transfer[OF assms(1)]) (insert assms(2), auto elim!: eventually_mono)
+
+lemma asymp_equiv_trans [trans]:
+ fixes f g h
+ assumes "f \<sim>[F] g" "g \<sim>[F] h"
+ shows "f \<sim>[F] h"
+proof -
+ let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+ from assms[THEN asymp_equiv_eventually_zeros]
+ have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
+ moreover from tendsto_mult[OF assms[THEN asymp_equivD]]
+ have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
+ ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
+qed
+
+lemma asymp_equiv_trans_lift1 [trans]:
+ assumes "a \<sim>[F] f b" "b \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
+ shows "a \<sim>[F] f c"
+ using assms by (blast intro: asymp_equiv_trans)
+
+lemma asymp_equiv_trans_lift2 [trans]:
+ assumes "f a \<sim>[F] b" "a \<sim>[F] c" "\<And>c d. c \<sim>[F] d \<Longrightarrow> f c \<sim>[F] f d"
+ shows "f c \<sim>[F] b"
+ using asymp_equiv_symI[OF assms(3)[OF assms(2)]] assms(1)
+ by (blast intro: asymp_equiv_trans)
+
+lemma asymp_equivD_const:
+ assumes "f \<sim>[F] (\<lambda>_. c)"
+ shows "(f \<longlongrightarrow> c) F"
+proof (cases "c = 0")
+ case False
+ with tendsto_mult_right[OF asymp_equivD[OF assms], of c] show ?thesis by simp
+next
+ case True
+ with asymp_equiv_eventually_zeros[OF assms] show ?thesis
+ by (simp add: Lim_eventually)
+qed
+
+lemma asymp_equiv_refl_ev:
+ assumes "eventually (\<lambda>x. f x = g x) F"
+ shows "f \<sim>[F] g"
+ by (intro asymp_equivI Lim_eventually)
+ (insert assms, auto elim!: eventually_mono)
+
+lemma asymp_equiv_sandwich:
+ fixes f g h :: "'a \<Rightarrow> 'b :: {real_normed_field, order_topology, linordered_field}"
+ assumes "eventually (\<lambda>x. f x \<ge> 0) F"
+ assumes "eventually (\<lambda>x. f x \<le> g x) F"
+ assumes "eventually (\<lambda>x. g x \<le> h x) F"
+ assumes "f \<sim>[F] h"
+ shows "g \<sim>[F] f" "g \<sim>[F] h"
+proof -
+ show "g \<sim>[F] f"
+ proof (rule asymp_equivI, rule tendsto_sandwich)
+ from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
+ show "eventually (\<lambda>n. (if h n = 0 \<and> f n = 0 then 1 else h n / f n) \<ge>
+ (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
+ by eventually_elim (auto intro!: divide_right_mono)
+ from assms(1-3) asymp_equiv_eventually_zeros[OF assms(4)]
+ show "eventually (\<lambda>n. 1 \<le>
+ (if g n = 0 \<and> f n = 0 then 1 else g n / f n)) F"
+ by eventually_elim (auto intro!: divide_right_mono)
+ qed (insert asymp_equiv_symI[OF assms(4)], simp_all add: asymp_equiv_def)
+ also note \<open>f \<sim>[F] h\<close>
+ finally show "g \<sim>[F] h" .
+qed
+
+lemma asymp_equiv_imp_eventually_same_sign:
+ fixes f g :: "real \<Rightarrow> real"
+ assumes "f \<sim>[F] g"
+ shows "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
+proof -
+ from assms have "((\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> sgn 1) F"
+ unfolding asymp_equiv_def by (rule tendsto_sgn) simp_all
+ from order_tendstoD(1)[OF this, of "1/2"]
+ have "eventually (\<lambda>x. sgn (if f x = 0 \<and> g x = 0 then 1 else f x / g x) > 1/2) F"
+ by simp
+ thus "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F"
+ proof eventually_elim
+ case (elim x)
+ thus ?case
+ by (cases "f x" "0 :: real" rule: linorder_cases;
+ cases "g x" "0 :: real" rule: linorder_cases) simp_all
+ qed
+qed
+
+lemma
+ fixes f g :: "_ \<Rightarrow> real"
+ assumes "f \<sim>[F] g"
+ shows asymp_equiv_eventually_same_sign: "eventually (\<lambda>x. sgn (f x) = sgn (g x)) F" (is ?th1)
+ and asymp_equiv_eventually_neg_iff: "eventually (\<lambda>x. f x < 0 \<longleftrightarrow> g x < 0) F" (is ?th2)
+ and asymp_equiv_eventually_pos_iff: "eventually (\<lambda>x. f x > 0 \<longleftrightarrow> g x > 0) F" (is ?th3)
+proof -
+ from assms have "filterlim (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x) (nhds 1) F"
+ by (rule asymp_equivD)
+ from order_tendstoD(1)[OF this zero_less_one]
+ show ?th1 ?th2 ?th3
+ by (eventually_elim; force simp: sgn_if divide_simps split: if_splits)+
+qed
+
+lemma asymp_equiv_tendsto_transfer:
+ assumes "f \<sim>[F] g" and "(f \<longlongrightarrow> c) F"
+ shows "(g \<longlongrightarrow> c) F"
+proof -
+ let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"
+ have "eventually (\<lambda>x. ?h x = g x) F"
+ using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
+ moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
+ hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"
+ by (rule asymp_equivD)
+ from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp
+ ultimately show ?thesis by (rule Lim_transform_eventually)
+qed
+
+lemma tendsto_asymp_equiv_cong:
+ assumes "f \<sim>[F] g"
+ shows "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"
+proof -
+ {
+ fix f g :: "'a \<Rightarrow> 'b"
+ assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"
+ have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"
+ using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp
+ moreover have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F"
+ by (intro tendsto_intros asymp_equivD *)
+ ultimately have "(f \<longlongrightarrow> c * 1) F"
+ by (rule Lim_transform_eventually)
+ }
+ from this[of f g] this[of g f] assms show ?thesis by (auto simp: asymp_equiv_sym)
+qed
+
+
+lemma smallo_imp_eventually_sgn:
+ fixes f g :: "real \<Rightarrow> real"
+ assumes "g \<in> o(f)"
+ shows "eventually (\<lambda>x. sgn (f x + g x) = sgn (f x)) at_top"
+proof -
+ have "0 < (1/2 :: real)" by simp
+ from landau_o.smallD[OF assms, OF this]
+ have "eventually (\<lambda>x. \<bar>g x\<bar> \<le> 1/2 * \<bar>f x\<bar>) at_top" by simp
+ thus ?thesis
+ proof eventually_elim
+ case (elim x)
+ thus ?case
+ by (cases "f x" "0::real" rule: linorder_cases;
+ cases "f x + g x" "0::real" rule: linorder_cases) simp_all
+ qed
+qed
+
+context
+begin
+
+private lemma asymp_equiv_add_rightI:
+ assumes "f \<sim>[F] g" "h \<in> o[F](g)"
+ shows "(\<lambda>x. f x + h x) \<sim>[F] g"
+proof -
+ let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+ from landau_o.smallD[OF assms(2) zero_less_one]
+ have ev: "eventually (\<lambda>x. g x = 0 \<longrightarrow> h x = 0) F" by eventually_elim auto
+ have "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1) F"
+ unfolding asymp_equiv_def using ev
+ by (intro tendsto_cong) (auto elim!: eventually_mono simp: divide_simps)
+ also have "\<dots> \<longleftrightarrow> ((\<lambda>x. ?T f g x + h x / g x) \<longlongrightarrow> 1 + 0) F" by simp
+ also have \<dots> by (intro tendsto_intros asymp_equivD assms smalloD_tendsto)
+ finally show "(\<lambda>x. f x + h x) \<sim>[F] g" .
+qed
+
+lemma asymp_equiv_add_right [asymp_equiv_simps]:
+ assumes "h \<in> o[F](g)"
+ shows "(\<lambda>x. f x + h x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
+proof
+ assume "(\<lambda>x. f x + h x) \<sim>[F] g"
+ from asymp_equiv_add_rightI[OF this, of "\<lambda>x. -h x"] assms show "f \<sim>[F] g"
+ by simp
+qed (simp_all add: asymp_equiv_add_rightI assms)
+
+end
+
+lemma asymp_equiv_add_left [asymp_equiv_simps]:
+ assumes "h \<in> o[F](g)"
+ shows "(\<lambda>x. h x + f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] g"
+ using asymp_equiv_add_right[OF assms] by (simp add: add.commute)
+
+lemma asymp_equiv_add_right' [asymp_equiv_simps]:
+ assumes "h \<in> o[F](g)"
+ shows "g \<sim>[F] (\<lambda>x. f x + h x) \<longleftrightarrow> g \<sim>[F] f"
+ using asymp_equiv_add_right[OF assms] by (simp add: asymp_equiv_sym)
+
+lemma asymp_equiv_add_left' [asymp_equiv_simps]:
+ assumes "h \<in> o[F](g)"
+ shows "g \<sim>[F] (\<lambda>x. h x + f x) \<longleftrightarrow> g \<sim>[F] f"
+ using asymp_equiv_add_left[OF assms] by (simp add: asymp_equiv_sym)
+
+lemma smallo_imp_asymp_equiv:
+ assumes "(\<lambda>x. f x - g x) \<in> o[F](g)"
+ shows "f \<sim>[F] g"
+proof -
+ from assms have "(\<lambda>x. f x - g x + g x) \<sim>[F] g"
+ by (subst asymp_equiv_add_left) simp_all
+ thus ?thesis by simp
+qed
+
+lemma asymp_equiv_uminus [asymp_equiv_intros]:
+ "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. -f x) \<sim>[F] (\<lambda>x. -g x)"
+ by (simp add: asymp_equiv_def cong: if_cong)
+
+lemma asymp_equiv_uminus_iff [asymp_equiv_simps]:
+ "(\<lambda>x. -f x) \<sim>[F] g \<longleftrightarrow> f \<sim>[F] (\<lambda>x. -g x)"
+ by (simp add: asymp_equiv_def cong: if_cong)
+
+lemma asymp_equiv_mult [asymp_equiv_intros]:
+ fixes f1 f2 g1 g2 :: "'a \<Rightarrow> 'b :: real_normed_field"
+ assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
+ shows "(\<lambda>x. f1 x * f2 x) \<sim>[F] (\<lambda>x. g1 x * g2 x)"
+proof -
+ let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+ let ?S = "\<lambda>x. (if f1 x = 0 \<and> g1 x = 0 then 1 - ?T f2 g2 x
+ else if f2 x = 0 \<and> g2 x = 0 then 1 - ?T f1 g1 x else 0)"
+ let ?S' = "\<lambda>x. ?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) x - ?T f1 g1 x * ?T f2 g2 x"
+ {
+ fix f g :: "'a \<Rightarrow> 'b" assume "f \<sim>[F] g"
+ have "((\<lambda>x. 1 - ?T f g x) \<longlongrightarrow> 0) F"
+ by (rule tendsto_eq_intros refl asymp_equivD[OF \<open>f \<sim>[F] g\<close>])+ simp_all
+ } note A = this
+
+ from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"
+ by (intro tendsto_mult asymp_equivD)
+ moreover {
+ have "eventually (\<lambda>x. ?S x = ?S' x) F"
+ using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
+ moreover have "(?S \<longlongrightarrow> 0) F"
+ by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])
+ (auto intro: le_infI1 le_infI2)
+ ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)
+ }
+ ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"
+ by (rule Lim_transform)
+ thus ?thesis by (simp add: asymp_equiv_def)
+qed
+
+lemma asymp_equiv_power [asymp_equiv_intros]:
+ "f \<sim>[F] g \<Longrightarrow> (\<lambda>x. f x ^ n) \<sim>[F] (\<lambda>x. g x ^ n)"
+ by (induction n) (simp_all add: asymp_equiv_mult)
+
+lemma asymp_equiv_inverse [asymp_equiv_intros]:
+ assumes "f \<sim>[F] g"
+ shows "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
+proof -
+ from tendsto_inverse[OF asymp_equivD[OF assms]]
+ have "((\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) \<longlongrightarrow> 1) F"
+ by (simp add: if_distrib cong: if_cong)
+ also have "(\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else g x / f x) =
+ (\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else inverse (f x) / inverse (g x))"
+ by (intro ext) (simp add: field_simps)
+ finally show ?thesis by (simp add: asymp_equiv_def)
+qed
+
+lemma asymp_equiv_inverse_iff [asymp_equiv_simps]:
+ "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x)) \<longleftrightarrow> f \<sim>[F] g"
+proof
+ assume "(\<lambda>x. inverse (f x)) \<sim>[F] (\<lambda>x. inverse (g x))"
+ hence "(\<lambda>x. inverse (inverse (f x))) \<sim>[F] (\<lambda>x. inverse (inverse (g x)))" (is ?P)
+ by (rule asymp_equiv_inverse)
+ also have "?P \<longleftrightarrow> f \<sim>[F] g" by (intro asymp_equiv_cong) simp_all
+ finally show "f \<sim>[F] g" .
+qed (simp_all add: asymp_equiv_inverse)
+
+lemma asymp_equiv_divide [asymp_equiv_intros]:
+ assumes "f1 \<sim>[F] g1" "f2 \<sim>[F] g2"
+ shows "(\<lambda>x. f1 x / f2 x) \<sim>[F] (\<lambda>x. g1 x / g2 x)"
+ using asymp_equiv_mult[OF assms(1) asymp_equiv_inverse[OF assms(2)]] by (simp add: field_simps)
+
+lemma asymp_equiv_compose [asymp_equiv_intros]:
+ assumes "f \<sim>[G] g" "filterlim h G F"
+ shows "f \<circ> h \<sim>[F] g \<circ> h"
+proof -
+ let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+ have "f \<circ> h \<sim>[F] g \<circ> h \<longleftrightarrow> ((?T f g \<circ> h) \<longlongrightarrow> 1) F"
+ by (simp add: asymp_equiv_def o_def)
+ also have "\<dots> \<longleftrightarrow> (?T f g \<longlongrightarrow> 1) (filtermap h F)"
+ by (rule tendsto_compose_filtermap)
+ also have "\<dots>"
+ by (rule tendsto_mono[of _ G]) (insert assms, simp_all add: asymp_equiv_def filterlim_def)
+ finally show ?thesis .
+qed
+
+lemma asymp_equiv_compose':
+ assumes "f \<sim>[G] g" "filterlim h G F"
+ shows "(\<lambda>x. f (h x)) \<sim>[F] (\<lambda>x. g (h x))"
+ using asymp_equiv_compose[OF assms] by (simp add: o_def)
+
+lemma asymp_equiv_powr_real [asymp_equiv_intros]:
+ fixes f g :: "'a \<Rightarrow> real"
+ assumes "f \<sim>[F] g" "eventually (\<lambda>x. f x \<ge> 0) F" "eventually (\<lambda>x. g x \<ge> 0) F"
+ shows "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"
+proof -
+ let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+ have "eventually (\<lambda>x. ?T f g x powr y = ?T (\<lambda>x. f x powr y) (\<lambda>x. g x powr y) x) F"
+ using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)
+ by eventually_elim (auto simp: powr_divide)
+ moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
+ by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
+ hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
+ ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
+qed
+
+lemma asymp_equiv_norm [asymp_equiv_intros]:
+ fixes f g :: "'a \<Rightarrow> 'b :: real_normed_field"
+ assumes "f \<sim>[F] g"
+ shows "(\<lambda>x. norm (f x)) \<sim>[F] (\<lambda>x. norm (g x))"
+ using tendsto_norm[OF asymp_equivD[OF assms]]
+ by (simp add: if_distrib asymp_equiv_def norm_divide cong: if_cong)
+
+lemma asymp_equiv_abs_real [asymp_equiv_intros]:
+ fixes f g :: "'a \<Rightarrow> real"
+ assumes "f \<sim>[F] g"
+ shows "(\<lambda>x. \<bar>f x\<bar>) \<sim>[F] (\<lambda>x. \<bar>g x\<bar>)"
+ using tendsto_rabs[OF asymp_equivD[OF assms]]
+ by (simp add: if_distrib asymp_equiv_def cong: if_cong)
+
+lemma asymp_equiv_imp_eventually_le:
+ assumes "f \<sim>[F] g" "c > 1"
+ shows "eventually (\<lambda>x. norm (f x) \<le> c * norm (g x)) F"
+proof -
+ from order_tendstoD(2)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
+ asymp_equiv_eventually_zeros[OF assms(1)]
+ show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
+qed
+
+lemma asymp_equiv_imp_eventually_ge:
+ assumes "f \<sim>[F] g" "c < 1"
+ shows "eventually (\<lambda>x. norm (f x) \<ge> c * norm (g x)) F"
+proof -
+ from order_tendstoD(1)[OF asymp_equivD[OF asymp_equiv_norm[OF assms(1)]] assms(2)]
+ asymp_equiv_eventually_zeros[OF assms(1)]
+ show ?thesis by eventually_elim (auto split: if_splits simp: field_simps)
+qed
+
+lemma asymp_equiv_imp_bigo:
+ assumes "f \<sim>[F] g"
+ shows "f \<in> O[F](g)"
+proof (rule bigoI)
+ have "(3/2::real) > 1" by simp
+ from asymp_equiv_imp_eventually_le[OF assms this]
+ show "eventually (\<lambda>x. norm (f x) \<le> 3/2 * norm (g x)) F"
+ by eventually_elim simp
+qed
+
+lemma asymp_equiv_imp_bigomega:
+ "f \<sim>[F] g \<Longrightarrow> f \<in> \<Omega>[F](g)"
+ using asymp_equiv_imp_bigo[of g F f] by (simp add: asymp_equiv_sym bigomega_iff_bigo)
+
+lemma asymp_equiv_imp_bigtheta:
+ "f \<sim>[F] g \<Longrightarrow> f \<in> \<Theta>[F](g)"
+ by (intro bigthetaI asymp_equiv_imp_bigo asymp_equiv_imp_bigomega)
+
+lemma asymp_equiv_at_infinity_transfer:
+ assumes "f \<sim>[F] g" "filterlim f at_infinity F"
+ shows "filterlim g at_infinity F"
+proof -
+ from assms(1) have "g \<in> \<Theta>[F](f)" by (rule asymp_equiv_imp_bigtheta[OF asymp_equiv_symI])
+ also from assms have "f \<in> \<omega>[F](\<lambda>_. 1)" by (simp add: smallomega_1_conv_filterlim)
+ finally show ?thesis by (simp add: smallomega_1_conv_filterlim)
+qed
+
+lemma asymp_equiv_at_top_transfer:
+ fixes f g :: "_ \<Rightarrow> real"
+ assumes "f \<sim>[F] g" "filterlim f at_top F"
+ shows "filterlim g at_top F"
+proof (rule filterlim_at_infinity_imp_filterlim_at_top)
+ show "filterlim g at_infinity F"
+ by (rule asymp_equiv_at_infinity_transfer[OF assms(1) filterlim_mono[OF assms(2)]])
+ (auto simp: at_top_le_at_infinity)
+ from assms(2) have "eventually (\<lambda>x. f x > 0) F"
+ using filterlim_at_top_dense by blast
+ with asymp_equiv_eventually_pos_iff[OF assms(1)] show "eventually (\<lambda>x. g x > 0) F"
+ by eventually_elim blast
+qed
+
+lemma asymp_equiv_at_bot_transfer:
+ fixes f g :: "_ \<Rightarrow> real"
+ assumes "f \<sim>[F] g" "filterlim f at_bot F"
+ shows "filterlim g at_bot F"
+ unfolding filterlim_uminus_at_bot
+ by (rule asymp_equiv_at_top_transfer[of "\<lambda>x. -f x" F "\<lambda>x. -g x"])
+ (insert assms, auto simp: filterlim_uminus_at_bot asymp_equiv_uminus)
+
+lemma asymp_equivI'_const:
+ assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> c) F" "c \<noteq> 0"
+ shows "f \<sim>[F] (\<lambda>x. c * g x)"
+ using tendsto_mult[OF assms(1) tendsto_const[of "inverse c"]] assms(2)
+ by (intro asymp_equivI') (simp add: field_simps)
+
+lemma asymp_equivI'_inverse_const:
+ assumes "((\<lambda>x. f x / g x) \<longlongrightarrow> inverse c) F" "c \<noteq> 0"
+ shows "(\<lambda>x. c * f x) \<sim>[F] g"
+ using tendsto_mult[OF assms(1) tendsto_const[of "c"]] assms(2)
+ by (intro asymp_equivI') (simp add: field_simps)
+
+lemma filterlim_at_bot_imp_at_infinity: "filterlim f at_bot F \<Longrightarrow> filterlim f at_infinity F"
+ for f :: "_ \<Rightarrow> real" using at_bot_le_at_infinity filterlim_mono by blast
+
+lemma asymp_equiv_imp_diff_smallo:
+ assumes "f \<sim>[F] g"
+ shows "(\<lambda>x. f x - g x) \<in> o[F](g)"
+proof (rule landau_o.smallI)
+ fix c :: real assume "c > 0"
+ hence c: "min c 1 > 0" by simp
+ let ?h = "\<lambda>x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
+ from assms have "((\<lambda>x. ?h x - 1) \<longlongrightarrow> 1 - 1) F"
+ by (intro tendsto_diff asymp_equivD tendsto_const)
+ from tendstoD[OF this c] show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
+ proof eventually_elim
+ case (elim x)
+ from elim have "norm (f x - g x) \<le> norm (f x / g x - 1) * norm (g x)"
+ by (subst norm_mult [symmetric]) (auto split: if_splits simp: divide_simps)
+ also have "norm (f x / g x - 1) * norm (g x) \<le> c * norm (g x)" using elim
+ by (auto split: if_splits simp: mult_right_mono)
+ finally show ?case .
+ qed
+qed
+
+lemma asymp_equiv_altdef:
+ "f \<sim>[F] g \<longleftrightarrow> (\<lambda>x. f x - g x) \<in> o[F](g)"
+ by (rule iffI[OF asymp_equiv_imp_diff_smallo smallo_imp_asymp_equiv])
+
+lemma asymp_equiv_0_left_iff [simp]: "(\<lambda>_. 0) \<sim>[F] f \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+ and asymp_equiv_0_right_iff [simp]: "f \<sim>[F] (\<lambda>_. 0) \<longleftrightarrow> eventually (\<lambda>x. f x = 0) F"
+ by (simp_all add: asymp_equiv_altdef landau_o.small_refl_iff)
+
+lemma asymp_equiv_sandwich_real:
+ fixes f g l u :: "'a \<Rightarrow> real"
+ assumes "l \<sim>[F] g" "u \<sim>[F] g" "eventually (\<lambda>x. f x \<in> {l x..u x}) F"
+ shows "f \<sim>[F] g"
+ unfolding asymp_equiv_altdef
+proof (rule landau_o.smallI)
+ fix c :: real assume c: "c > 0"
+ have "eventually (\<lambda>x. norm (f x - g x) \<le> max (norm (l x - g x)) (norm (u x - g x))) F"
+ using assms(3) by eventually_elim auto
+ moreover have "eventually (\<lambda>x. norm (l x - g x) \<le> c * norm (g x)) F"
+ "eventually (\<lambda>x. norm (u x - g x) \<le> c * norm (g x)) F"
+ using assms(1,2) by (auto simp: asymp_equiv_altdef dest: landau_o.smallD[OF _ c])
+ hence "eventually (\<lambda>x. max (norm (l x - g x)) (norm (u x - g x)) \<le> c * norm (g x)) F"
+ by eventually_elim simp
+ ultimately show "eventually (\<lambda>x. norm (f x - g x) \<le> c * norm (g x)) F"
+ by eventually_elim (rule order.trans)
+qed
+
+lemma asymp_equiv_sandwich_real':
+ fixes f g l u :: "'a \<Rightarrow> real"
+ assumes "f \<sim>[F] l" "f \<sim>[F] u" "eventually (\<lambda>x. g x \<in> {l x..u x}) F"
+ shows "f \<sim>[F] g"
+ using asymp_equiv_sandwich_real[of l F f u g] assms by (simp add: asymp_equiv_sym)
+
+lemma asymp_equiv_sandwich_real'':
+ fixes f g l u :: "'a \<Rightarrow> real"
+ assumes "l1 \<sim>[F] u1" "u1 \<sim>[F] l2" "l2 \<sim>[F] u2"
+ "eventually (\<lambda>x. f x \<in> {l1 x..u1 x}) F" "eventually (\<lambda>x. g x \<in> {l2 x..u2 x}) F"
+ shows "f \<sim>[F] g"
+ by (rule asymp_equiv_sandwich_real[OF asymp_equiv_sandwich_real'[OF _ _ assms(5)]
+ asymp_equiv_sandwich_real'[OF _ _ assms(5)] assms(4)];
+ blast intro: asymp_equiv_trans assms(1,2,3))+
+
+end
--- a/src/HOL/Library/Library.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Library/Library.thy Tue May 22 19:58:17 2018 +0100
@@ -38,6 +38,7 @@
Indicator_Function
Infinite_Set
IArray
+ Landau_Symbols
Lattice_Algebras
Lattice_Syntax
Lattice_Constructions
--- a/src/HOL/Library/Multiset.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Library/Multiset.thy Tue May 22 19:58:17 2018 +0100
@@ -1888,7 +1888,7 @@
apply simp
done
-lemma mset_compl_union [simp]: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
+lemma mset_compl_union [simp]: "mset (filter P xs) + mset (filter (\<lambda>x. \<not>P x) xs) = mset xs"
by (induct xs) auto
lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
@@ -2582,14 +2582,14 @@
show "mset ys = mset xs" by simp
from \<open>sorted (map f ys)\<close>
show "sorted (map f ys)" .
- show "[x\<leftarrow>ys . f k = f x] = [x\<leftarrow>xs . f k = f x]" if "k \<in> set ys" for k
+ show "filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs" if "k \<in> set ys" for k
proof -
from mset_equal
have set_equal: "set xs = set ys" by (rule mset_eq_setD)
with that have "insert k (set ys) = set ys" by auto
with \<open>inj_on f (set xs)\<close> have inj: "inj_on f (insert k (set ys))"
by (simp add: set_equal)
- from inj have "[x\<leftarrow>ys . f k = f x] = filter (HOL.eq k) ys"
+ from inj have "filter (\<lambda>x. f k = f x) ys = filter (HOL.eq k) ys"
by (auto intro!: inj_on_filter_key_eq)
also have "\<dots> = replicate (count (mset ys) k) k"
by (simp add: replicate_count_mset_eq_filter_eq)
@@ -2597,7 +2597,7 @@
using mset_equal by simp
also have "\<dots> = filter (HOL.eq k) xs"
by (simp add: replicate_count_mset_eq_filter_eq)
- also have "\<dots> = [x\<leftarrow>xs . f k = f x]"
+ also have "\<dots> = filter (\<lambda>x. f k = f x) xs"
using inj by (auto intro!: inj_on_filter_key_eq [symmetric] simp add: set_equal)
finally show ?thesis .
qed
@@ -2610,9 +2610,9 @@
by (rule sort_key_inj_key_eq) (simp_all add: assms)
lemma sort_key_by_quicksort:
- "sort_key f xs = sort_key f [x\<leftarrow>xs. f x < f (xs ! (length xs div 2))]
- @ [x\<leftarrow>xs. f x = f (xs ! (length xs div 2))]
- @ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs")
+ "sort_key f xs = sort_key f (filter (\<lambda>x. f x < f (xs ! (length xs div 2))) xs)
+ @ filter (\<lambda>x. f x = f (xs ! (length xs div 2))) xs
+ @ sort_key f (filter (\<lambda>x. f x > f (xs ! (length xs div 2))) xs)" (is "sort_key f ?lhs = ?rhs")
proof (rule properties_for_sort_key)
show "mset ?rhs = mset ?lhs"
by (rule multiset_eqI) (auto simp add: mset_filter)
@@ -2623,14 +2623,14 @@
assume "l \<in> set ?rhs"
let ?pivot = "f (xs ! (length xs div 2))"
have *: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto
- have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]"
+ have "filter (\<lambda>x. f x = f l) (sort_key f xs) = filter (\<lambda>x. f x = f l) xs"
unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
- with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp
+ with * have **: "filter (\<lambda>x. f l = f x) (sort_key f xs) = filter (\<lambda>x. f l = f x) xs" by simp
have "\<And>x P. P (f x) ?pivot \<and> f l = f x \<longleftrightarrow> P (f l) ?pivot \<and> f l = f x" by auto
- then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] =
- [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp
+ then have "\<And>P. filter (\<lambda>x. P (f x) ?pivot \<and> f l = f x) (sort_key f xs) =
+ filter (\<lambda>x. P (f l) ?pivot \<and> f l = f x) (sort_key f xs)" by simp
note *** = this [of "(<)"] this [of "(>)"] this [of "(=)"]
- show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
+ show "filter (\<lambda>x. f l = f x) ?rhs = filter (\<lambda>x. f l = f x) ?lhs"
proof (cases "f l" ?pivot rule: linorder_cases)
case less
then have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto
@@ -2648,15 +2648,15 @@
qed
lemma sort_by_quicksort:
- "sort xs = sort [x\<leftarrow>xs. x < xs ! (length xs div 2)]
- @ [x\<leftarrow>xs. x = xs ! (length xs div 2)]
- @ sort [x\<leftarrow>xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
+ "sort xs = sort (filter (\<lambda>x. x < xs ! (length xs div 2)) xs)
+ @ filter (\<lambda>x. x = xs ! (length xs div 2)) xs
+ @ sort (filter (\<lambda>x. x > xs ! (length xs div 2)) xs)" (is "sort ?lhs = ?rhs")
using sort_key_by_quicksort [of "\<lambda>x. x", symmetric] by simp
text \<open>A stable parametrized quicksort\<close>
definition part :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b list \<Rightarrow> 'b list \<times> 'b list \<times> 'b list" where
- "part f pivot xs = ([x \<leftarrow> xs. f x < pivot], [x \<leftarrow> xs. f x = pivot], [x \<leftarrow> xs. pivot < f x])"
+ "part f pivot xs = (filter (\<lambda>x. f x < pivot) xs, filter (\<lambda>x. f x = pivot) xs, filter (\<lambda>x. f x > pivot) xs)"
lemma part_code [code]:
"part f pivot [] = ([], [], [])"
--- a/src/HOL/List.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/List.thy Tue May 22 19:58:17 2018 +0100
@@ -78,13 +78,13 @@
"filter P [] = []" |
"filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
-text \<open>Special syntax for filter:\<close>
+text \<open>Special input syntax for filter:\<close>
syntax (ASCII)
"_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
syntax
"_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_\<leftarrow>_ ./ _])")
translations
- "[x<-xs . P]" \<rightleftharpoons> "CONST filter (\<lambda>x. P) xs"
+ "[x<-xs . P]" \<rightharpoonup> "CONST filter (\<lambda>x. P) xs"
primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
fold_Nil: "fold f [] = id" |
@@ -1598,7 +1598,7 @@
lemma inj_on_filter_key_eq:
assumes "inj_on f (insert y (set xs))"
- shows "[x\<leftarrow>xs . f y = f x] = filter (HOL.eq y) xs"
+ shows "filter (\<lambda>x. f y = f x) xs = filter (HOL.eq y) xs"
using assms by (induct xs) auto
lemma filter_cong[fundef_cong]:
@@ -4430,8 +4430,8 @@
done
lemma nths_shift_lemma:
- "map fst [p<-zip xs [i..<i + length xs] . snd p \<in> A] =
- map fst [p<-zip xs [0..<length xs] . snd p + i \<in> A]"
+ "map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [i..<i + length xs])) =
+ map fst (filter (\<lambda>p. snd p + i \<in> A) (zip xs [0..<length xs]))"
by (induct xs rule: rev_induct) (simp_all add: add.commute)
lemma nths_append:
@@ -4720,19 +4720,19 @@
lemma transpose_aux_filter_head:
"concat (map (case_list [] (\<lambda>h t. [h])) xss) =
- map (\<lambda>xs. hd xs) [ys\<leftarrow>xss . ys \<noteq> []]"
+ map (\<lambda>xs. hd xs) (filter (\<lambda>ys. ys \<noteq> []) xss)"
by (induct xss) (auto split: list.split)
lemma transpose_aux_filter_tail:
"concat (map (case_list [] (\<lambda>h t. [t])) xss) =
- map (\<lambda>xs. tl xs) [ys\<leftarrow>xss . ys \<noteq> []]"
+ map (\<lambda>xs. tl xs) (filter (\<lambda>ys. ys \<noteq> []) xss)"
by (induct xss) (auto split: list.split)
lemma transpose_aux_max:
"max (Suc (length xs)) (foldr (\<lambda>xs. max (length xs)) xss 0) =
- Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) [ys\<leftarrow>xss . ys\<noteq>[]] 0))"
+ Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) (filter (\<lambda>ys. ys \<noteq> []) xss) 0))"
(is "max _ ?foldB = Suc (max _ ?foldA)")
-proof (cases "[ys\<leftarrow>xss . ys\<noteq>[]] = []")
+proof (cases "(filter (\<lambda>ys. ys \<noteq> []) xss) = []")
case True
hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
proof (induct xss)
@@ -4744,16 +4744,16 @@
next
case False
- have foldA: "?foldA = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0 - 1"
+ have foldA: "?foldA = foldr (\<lambda>x. max (length x)) (filter (\<lambda>ys. ys \<noteq> []) xss) 0 - 1"
by (induct xss) auto
- have foldB: "?foldB = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0"
+ have foldB: "?foldB = foldr (\<lambda>x. max (length x)) (filter (\<lambda>ys. ys \<noteq> []) xss) 0"
by (induct xss) auto
have "0 < ?foldB"
proof -
from False
- obtain z zs where zs: "[ys\<leftarrow>xss . ys \<noteq> []] = z#zs" by (auto simp: neq_Nil_conv)
- hence "z \<in> set ([ys\<leftarrow>xss . ys \<noteq> []])" by auto
+ obtain z zs where zs: "(filter (\<lambda>ys. ys \<noteq> []) xss) = z#zs" by (auto simp: neq_Nil_conv)
+ hence "z \<in> set (filter (\<lambda>ys. ys \<noteq> []) xss)" by auto
hence "z \<noteq> []" by auto
thus ?thesis
unfolding foldB zs
@@ -4781,7 +4781,7 @@
lemma nth_transpose:
fixes xs :: "'a list list"
assumes "i < length (transpose xs)"
- shows "transpose xs ! i = map (\<lambda>xs. xs ! i) [ys \<leftarrow> xs. i < length ys]"
+ shows "transpose xs ! i = map (\<lambda>xs. xs ! i) (filter (\<lambda>ys. i < length ys) xs)"
using assms proof (induct arbitrary: i rule: transpose.induct)
case (3 x xs xss)
define XS where "XS = (x # xs) # xss"
@@ -5154,7 +5154,7 @@
lemma filter_equals_takeWhile_sorted_rev:
assumes sorted: "sorted (rev (map f xs))"
- shows "[x \<leftarrow> xs. t < f x] = takeWhile (\<lambda> x. t < f x) xs"
+ shows "filter (\<lambda>x. t < f x) xs = takeWhile (\<lambda> x. t < f x) xs"
(is "filter ?P xs = ?tW")
proof (rule takeWhile_eq_filter[symmetric])
let "?dW" = "dropWhile ?P xs"
@@ -5178,18 +5178,18 @@
qed
lemma sorted_map_same:
- "sorted (map f [x\<leftarrow>xs. f x = g xs])"
+ "sorted (map f (filter (\<lambda>x. f x = g xs) xs))"
proof (induct xs arbitrary: g)
case Nil then show ?case by simp
next
case (Cons x xs)
- then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
- moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
+ then have "sorted (map f (filter (\<lambda>y. f y = (\<lambda>xs. f x) xs) xs))" .
+ moreover from Cons have "sorted (map f (filter (\<lambda>y. f y = (g \<circ> Cons x) xs) xs))" .
ultimately show ?case by simp_all
qed
lemma sorted_same:
- "sorted [x\<leftarrow>xs. x = g xs]"
+ "sorted (filter (\<lambda>x. x = g xs) xs)"
using sorted_map_same [of "\<lambda>x. x"] by simp
end
@@ -5411,7 +5411,7 @@
text \<open>Stability of @{const sort_key}:\<close>
-lemma sort_key_stable: "[y <- sort_key f xs. f y = k] = [y <- xs. f y = k]"
+lemma sort_key_stable: "filter (\<lambda>y. f y = k) (sort_key f xs) = filter (\<lambda>y. f y = k) xs"
proof (induction xs)
case Nil thus ?case by simp
next
@@ -5422,12 +5422,12 @@
using Cons.IH by (metis (mono_tags) filter.simps(2) filter_sort)
next
case True
- hence ler: "[y <- (a # xs). f y = k] = 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])"
+ hence ler: "filter (\<lambda>y. f y = k) (a # xs) = a # filter (\<lambda>y. f y = f a) xs" by simp
+ have "\<forall>y \<in> set (sort_key f (filter (\<lambda>y. f y = f a) xs)). f y = f a" by simp
+ hence "insort_key f a (sort_key f (filter (\<lambda>y. f y = f a) xs))
+ = a # (sort_key f (filter (\<lambda>y. f y = f a) xs))"
by (simp add: insort_is_Cons)
- hence lel: "[y <- sort_key f (a # xs). f y = k] = a # [y <- sort_key f xs. f y = f a]"
+ hence lel: "filter (\<lambda>y. f y = k) (sort_key f (a # xs)) = a # filter (\<lambda>y. f y = f a) (sort_key f xs)"
by (metis True filter_sort ler sort_key_simps(2))
from lel ler show ?thesis using Cons.IH True by (auto)
qed
@@ -5447,7 +5447,7 @@
length_filter_conv_card intro: card_mono)
lemma transpose_max_length:
- "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length [x \<leftarrow> xs. x \<noteq> []]"
+ "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length (filter (\<lambda>x. x \<noteq> []) xs)"
(is "?L = ?R")
proof (cases "transpose xs = []")
case False
@@ -5459,7 +5459,7 @@
using False by (simp add: nth_transpose)
next
case True
- hence "[x \<leftarrow> xs. x \<noteq> []] = []"
+ hence "filter (\<lambda>x. x \<noteq> []) xs = []"
by (auto intro!: filter_False simp: transpose_empty)
thus ?thesis by (simp add: transpose_empty True)
qed
@@ -5480,7 +5480,7 @@
fixes xs :: "'a list list"
assumes sorted: "sorted (rev (map length xs))"
and i: "i < length (transpose xs)"
- and j: "j < length [ys \<leftarrow> xs. i < length ys]"
+ and j: "j < length (filter (\<lambda>ys. i < length ys) xs)"
shows "transpose xs ! i ! j = xs ! j ! i"
using j filter_equals_takeWhile_sorted_rev[OF sorted, of i]
nth_transpose[OF i] nth_map[OF j]
@@ -5542,7 +5542,7 @@
have "length (xs ! i) \<le> length (xs ! k)" by simp
thus "Suc j \<le> length (xs ! k)" using j_less by simp
qed
- have i_less_filter: "i < length [ys\<leftarrow>xs . j < length ys]"
+ have i_less_filter: "i < length (filter (\<lambda>ys. j < length ys) xs) "
unfolding filter_equals_takeWhile_sorted_rev[OF sorted, of j]
using i_less_tW by (simp_all add: Suc_le_eq)
from j show "?R ! j = xs ! i ! j"
@@ -5581,7 +5581,7 @@
show len: "length ?trans = length ?map"
by (simp_all add: length_transpose foldr_map comp_def)
moreover
- { fix i assume "i < n" hence "[ys\<leftarrow>xs . i < length ys] = xs"
+ { fix i assume "i < n" hence "filter (\<lambda>ys. i < length ys) xs = xs"
using rect by (auto simp: in_set_conv_nth intro!: filter_True) }
ultimately show "\<forall>i < length ?trans. ?trans ! i = ?map ! i"
by (auto simp: nth_transpose intro: nth_equalityI)
--- a/src/HOL/MicroJava/DFA/Kildall.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Tue May 22 19:58:17 2018 +0100
@@ -38,7 +38,7 @@
lemma (in Semilat) nth_merges:
"\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
- (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
+ (merges f ps ss)!p = map snd (filter (\<lambda>(p',t'). p'=p) ps) ++_f ss!p"
(is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
proof (induct ps)
show "\<And>ss. ?P ss []" by simp
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Tue May 22 19:58:17 2018 +0100
@@ -80,13 +80,13 @@
assume merge: "?s1 \<noteq> T"
from x ss1 have "?s1 =
(if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
- then (map snd [(p', t') \<leftarrow> ss1 . p'=pc+1]) ++_f x
+ then (map snd (filter (\<lambda>(p', t'). p'=pc+1) ss1)) ++_f x
else \<top>)"
by (rule merge_def)
with merge obtain
app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'"
(is "?app ss1") and
- sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1"
+ sum: "(map snd (filter (\<lambda>(p',t'). p' = pc+1) ss1) ++_f x) = ?s1"
(is "?map ss1 ++_f x = _" is "?sum ss1 = _")
by (simp split: if_split_asm)
from app less
@@ -115,7 +115,7 @@
from x ss2 have
"?s2 =
(if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
- then map snd [(p', t') \<leftarrow> ss2 . p' = pc + 1] ++_f x
+ then map snd (filter (\<lambda>(p', t'). p' = pc + 1) ss2) ++_f x
else \<top>)"
by (rule merge_def)
ultimately have ?thesis by simp
@@ -194,7 +194,7 @@
ultimately
have "merge c pc ?step (c!Suc pc) =
(if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
- then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
+ then map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc
else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
moreover {
fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
@@ -207,7 +207,7 @@
} hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
moreover
from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto
- hence "map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>"
+ hence "map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc \<noteq> \<top>"
(is "?map ++_f _ \<noteq> _")
proof (rule disjE)
assume pc': "Suc pc = length \<phi>"
@@ -215,7 +215,7 @@
moreover
from pc' bounded pc
have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
- hence "[(p',t') \<leftarrow> ?step.p'=pc+1] = []" by (blast intro: filter_False)
+ hence "filter (\<lambda>(p',t').p'=pc+1) ?step = []" by (blast intro: filter_False)
hence "?map = []" by simp
ultimately show ?thesis by (simp add: B_neq_T)
next
@@ -262,7 +262,7 @@
hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti)
ultimately
have "merge c pc ?step (c!Suc pc) =
- map snd [(p',t')\<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s)
+ map snd (filter (\<lambda>(p',t').p'=pc+1) ?step) ++_f c!Suc pc" by (rule merge_not_top_s)
hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)
also {
from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp
--- a/src/HOL/MicroJava/DFA/LBVCorrect.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy Tue May 22 19:58:17 2018 +0100
@@ -88,7 +88,7 @@
also
from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
with cert_in_A step_in_A
- have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))"
+ have "?merge = (map snd (filter (\<lambda>(p',t').p'=pc+1) (?step pc)) ++_f (c!(pc+1)))"
by (rule merge_not_top_s)
finally
have "s' <=_r ?s2" using step_in_A cert_in_A True step
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Tue May 22 19:58:17 2018 +0100
@@ -113,7 +113,7 @@
lemma (in Semilat) pp_ub1':
assumes S: "snd`set S \<subseteq> A"
assumes y: "y \<in> A" and ab: "(a, b) \<in> set S"
- shows "b <=_r map snd [(p', t') \<leftarrow> S . p' = a] ++_f y"
+ shows "b <=_r map snd (filter (\<lambda>(p', t'). p' = a) S) ++_f y"
proof -
from S have "\<forall>(x,y) \<in> set S. y \<in> A" by auto
with semilat y ab show ?thesis by - (rule ub1')
@@ -172,7 +172,7 @@
"\<And>x. x \<in> A \<Longrightarrow> snd`set ss \<subseteq> A \<Longrightarrow>
merge c pc ss x =
(if \<forall>(pc',s') \<in> set ss. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' then
- map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x
+ map snd (filter (\<lambda>(p',t'). p'=pc+1) ss) ++_f x
else \<top>)"
(is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x")
proof (induct ss)
@@ -202,15 +202,15 @@
hence "\<forall>(pc', s')\<in>set ls. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
moreover
from True have
- "map snd [(p',t')\<leftarrow>ls . p'=pc+1] ++_f ?if' =
- (map snd [(p',t')\<leftarrow>l#ls . p'=pc+1] ++_f x)"
+ "map snd (filter (\<lambda>(p',t'). p'=pc+1) ls) ++_f ?if' =
+ (map snd (filter (\<lambda>(p',t'). p'=pc+1) (l#ls)) ++_f x)"
by simp
ultimately
show ?thesis using True by simp
next
case False
moreover
- from ls have "set (map snd [(p', t')\<leftarrow>ls . p' = Suc pc]) \<subseteq> A" by auto
+ from ls have "set (map snd (filter (\<lambda>(p', t'). p' = Suc pc) ls)) \<subseteq> A" by auto
ultimately show ?thesis by auto
qed
finally show "?P (l#ls) x" .
@@ -219,7 +219,7 @@
lemma (in lbv) merge_not_top_s:
assumes x: "x \<in> A" and ss: "snd`set ss \<subseteq> A"
assumes m: "merge c pc ss x \<noteq> \<top>"
- shows "merge c pc ss x = (map snd [(p',t') \<leftarrow> ss. p'=pc+1] ++_f x)"
+ shows "merge c pc ss x = (map snd (filter (\<lambda>(p',t'). p'=pc+1) ss) ++_f x)"
proof -
from ss m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc')"
by (rule merge_not_top)
@@ -307,8 +307,8 @@
assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
shows "merge c pc ss x \<in> A"
proof -
- from s0 have "set (map snd [(p', t')\<leftarrow>ss . p'=pc+1]) \<subseteq> A" by auto
- with x have "(map snd [(p', t')\<leftarrow>ss . p'=pc+1] ++_f x) \<in> A"
+ from s0 have "set (map snd (filter (\<lambda>(p', t'). p'=pc+1) ss)) \<subseteq> A" by auto
+ with x have "(map snd (filter (\<lambda>(p', t'). p'=pc+1) ss) ++_f x) \<in> A"
by (auto intro!: plusplus_closed semilat)
with s0 x show ?thesis by (simp add: merge_def T_A)
qed
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy Tue May 22 19:58:17 2018 +0100
@@ -155,7 +155,7 @@
lemma ub1':
assumes "semilat (A, r, f)"
shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
- \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y"
+ \<Longrightarrow> b <=_r map snd (filter (\<lambda>(p', t'). p' = a) S) ++_f y"
proof -
interpret Semilat A r f using assms by (rule Semilat.intro)
@@ -175,7 +175,7 @@
lemma plusplus_empty:
"\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
- (map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q"
+ (map snd (filter (\<lambda>(p', t'). p' = q) S) ++_f ss ! q) = ss ! q"
by (induct S) auto
end
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue May 22 19:58:17 2018 +0100
@@ -317,7 +317,7 @@
| "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1"
theorem S\<^sub>1_sound:
-"w \<in> S\<^sub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"w \<in> S\<^sub>1 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
nitpick [expect = genuine]
oops
@@ -330,7 +330,7 @@
| "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2"
theorem S\<^sub>2_sound:
-"w \<in> S\<^sub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"w \<in> S\<^sub>2 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
nitpick [expect = genuine]
oops
@@ -343,12 +343,12 @@
| "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3"
theorem S\<^sub>3_sound:
-"w \<in> S\<^sub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"w \<in> S\<^sub>3 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
nitpick [card = 1-5, expect = none]
sorry
theorem S\<^sub>3_complete:
-"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>3"
+"length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) \<longrightarrow> w \<in> S\<^sub>3"
nitpick [expect = genuine]
oops
@@ -362,19 +362,19 @@
| "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
theorem S\<^sub>4_sound:
-"w \<in> S\<^sub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"w \<in> S\<^sub>4 \<longrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
nitpick [card = 1-5, expect = none]
sorry
theorem S\<^sub>4_complete:
-"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>4"
+"length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) \<longrightarrow> w \<in> S\<^sub>4"
nitpick [card = 1-5, expect = none]
sorry
theorem S\<^sub>4_A\<^sub>4_B\<^sub>4_sound_and_complete:
-"w \<in> S\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-"w \<in> A\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
-"w \<in> B\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
+"w \<in> S\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w)"
+"w \<in> A\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = a) w) = length (filter (\<lambda>x. x = b) w) + 1"
+"w \<in> B\<^sub>4 \<longleftrightarrow> length (filter (\<lambda>x. x = b) w) = length (filter (\<lambda>x. x = a) w) + 1"
nitpick [card = 1-5, expect = none]
sorry
--- a/src/HOL/Nominal/Examples/W.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Nominal/Examples/W.thy Tue May 22 19:58:17 2018 +0100
@@ -9,7 +9,7 @@
abbreviation
"difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60)
where
- "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
+ "xs - ys \<equiv> filter (\<lambda>x. x\<notin>set ys) xs"
lemma difference_eqvt_tvar[eqvt]:
fixes pi::"tvar prm"
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue May 22 19:58:17 2018 +0100
@@ -71,7 +71,7 @@
oops
theorem S\<^sub>1_sound:
-"S\<^sub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"S\<^sub>1p w \<Longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
quickcheck[tester=smart_exhaustive, size=15]
oops
@@ -113,7 +113,7 @@
oops
*)
theorem S\<^sub>2_sound:
-"S\<^sub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"S\<^sub>2p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
quickcheck[tester=smart_exhaustive, size=5, iterations=10]
oops
@@ -133,16 +133,16 @@
lemma S\<^sub>3_sound:
-"S\<^sub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"S\<^sub>3p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
quickcheck[tester=smart_exhaustive, size=10, iterations=10]
oops
-lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
+lemma "\<not> (length w > 2) \<or> \<not> (length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w))"
quickcheck[size=10, tester = smart_exhaustive]
oops
theorem S\<^sub>3_complete:
-"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> S\<^sub>3p w"
+"length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w) \<longrightarrow> S\<^sub>3p w"
(*quickcheck[generator=SML]*)
quickcheck[tester=smart_exhaustive, size=10, iterations=100]
oops
@@ -158,12 +158,12 @@
| "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
theorem S\<^sub>4_sound:
-"S\<^sub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+"S\<^sub>4p w \<longrightarrow> length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w)"
quickcheck[tester = smart_exhaustive, size=5, iterations=1]
oops
theorem S\<^sub>4_complete:
-"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> S\<^sub>4p w"
+"length (filter (\<lambda>x. x=a) w) = length (filter (\<lambda>x. x=b) w) \<longrightarrow> S\<^sub>4p w"
quickcheck[tester = smart_exhaustive, size=5, iterations=1]
oops
@@ -301,7 +301,7 @@
subsection "Compressed matrix"
-definition "sparsify xs = [i \<leftarrow> zip [0..<length xs] xs. snd i \<noteq> 0]"
+definition "sparsify xs = filter (\<lambda>i. snd i \<noteq> 0) (zip [0..<length xs] xs)"
(*
lemma sparsify_length: "(i, x) \<in> set (sparsify xs) \<Longrightarrow> i < length xs"
by (auto simp: sparsify_def set_zip)
--- a/src/HOL/Probability/Probability_Mass_Function.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue May 22 19:58:17 2018 +0100
@@ -2028,7 +2028,7 @@
private lemma pmf_of_list_aux:
assumes "\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0"
assumes "sum_list (map snd xs) = 1"
- shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])) \<partial>count_space UNIV) = 1"
+ shows "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) = 1"
proof -
have "(\<integral>\<^sup>+ x. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))) \<partial>count_space UNIV) =
(\<integral>\<^sup>+ x. ennreal (sum_list (map (\<lambda>(x',p). indicator {x'} x * p) xs)) \<partial>count_space UNIV)"
@@ -2083,7 +2083,7 @@
show "x \<in> set (map fst xs)"
proof (rule ccontr)
assume "x \<notin> set (map fst xs)"
- hence "[z\<leftarrow>xs . fst z = x] = []" by (auto simp: filter_empty_conv)
+ hence "filter (\<lambda>z. fst z = x) xs = []" by (auto simp: filter_empty_conv)
with A assms show False by (simp add: pmf_pmf_of_list set_pmf_eq)
qed
qed
@@ -2122,10 +2122,10 @@
have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
by simp
also from assms
- have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
+ have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd (filter (\<lambda>z. fst z = x) xs))))"
by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list Int_def)
also from assms
- have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
+ have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
by (subst sum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
@@ -2184,7 +2184,7 @@
{
fix x assume A: "x \<in> fst ` set xs" and B: "x \<notin> set_pmf (pmf_of_list xs)"
then obtain y where y: "(x, y) \<in> set xs" by auto
- from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
+ from B have "sum_list (map snd (filter (\<lambda>z. fst z = x) xs)) = 0"
by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
ultimately have "y = 0" using assms(1)
@@ -2199,11 +2199,11 @@
defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
shows "pmf_of_list_wf xs'" "pmf_of_list xs' = pmf_of_list xs"
proof -
- have "map snd [z\<leftarrow>xs . snd z \<noteq> 0] = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
+ have "map snd (filter (\<lambda>z. snd z \<noteq> 0) xs) = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
by (induction xs) simp_all
with assms(1) show wf: "pmf_of_list_wf xs'"
by (auto simp: pmf_of_list_wf_def xs'_def sum_list_filter_nonzero)
- have "sum_list (map snd [z\<leftarrow>xs' . fst z = i]) = sum_list (map snd [z\<leftarrow>xs . fst z = i])" for i
+ have "sum_list (map snd (filter (\<lambda>z. fst z = i) xs')) = sum_list (map snd (filter (\<lambda>z. fst z = i) xs))" for i
unfolding xs'_def by (induction xs) simp_all
with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs"
by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list)
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Tue May 22 19:58:17 2018 +0100
@@ -186,7 +186,7 @@
oops
lemma
- "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
+ "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) (filter (\<lambda>ys. i < length ys) xs)"
quickcheck[random, iterations = 10000]
quickcheck[exhaustive, expect = counterexample]
oops
@@ -228,13 +228,13 @@
oops
lemma
- "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
+ "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. i < length ys) (remdups xs))"
quickcheck[random]
quickcheck[exhaustive, expect = counterexample]
oops
lemma
- "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
+ "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. length ys \<in> {..<i}) (List.transpose xs))"
quickcheck[random]
quickcheck[exhaustive, expect = counterexample]
oops
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Tue May 22 19:58:17 2018 +0100
@@ -69,12 +69,12 @@
definition
inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
- [simp]: "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"
+ [simp]: "inter_list xs ys = filter (\<lambda>x. x \<in> set xs \<and> x \<in> set ys) xs"
definition
diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
- [simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"
+ [simp]: "diff_list xs ys = filter (\<lambda>x. x \<notin> set ys) xs"
definition
rsp_fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
--- a/src/HOL/Random.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Random.thy Tue May 22 19:58:17 2018 +0100
@@ -116,7 +116,7 @@
lemma select_weight_drop_zero:
"select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
proof -
- have "sum_list (map fst [(k, _)\<leftarrow>xs . 0 < k]) = sum_list (map fst xs)"
+ have "sum_list (map fst (filter (\<lambda>(k, _). 0 < k) xs)) = sum_list (map fst xs)"
by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
then show ?thesis by (simp only: select_weight_def pick_drop_zero)
qed
--- a/src/HOL/Tools/ATP/atp_problem.ML Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 22 19:58:17 2018 +0100
@@ -32,7 +32,7 @@
gen_simp : bool}
datatype polymorphism = Monomorphic | Polymorphic
- datatype thf_choice = THF_Without_Choice | THF_With_Choice
+ datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
@@ -188,7 +188,7 @@
gen_simp : bool}
datatype polymorphism = Monomorphic | Polymorphic
-datatype thf_choice = THF_Without_Choice | THF_With_Choice
+datatype thf_choice = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue May 22 19:58:17 2018 +0100
@@ -162,6 +162,9 @@
fun is_type_enc_native (Native _) = true
| is_type_enc_native _ = false
+fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _)) = false
+ | is_type_enc_full_higher_order (Native (Higher_Order _, _, _)) = true
+ | is_type_enc_full_higher_order _ = false
fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true
| is_type_enc_higher_order _ = false
@@ -668,17 +671,22 @@
| _ => raise Same.SAME))
handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
-fun adjust_order THF_Without_Choice (Higher_Order _) =
- Higher_Order THF_Without_Choice
- | adjust_order _ type_enc = type_enc
+fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free
+ | min_hologic _ THF_Lambda_Free = THF_Lambda_Free
+ | min_hologic THF_Without_Choice _ = THF_Without_Choice
+ | min_hologic _ THF_Without_Choice = THF_Without_Choice
+ | min_hologic _ _ = THF_With_Choice
+
+fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic')
+ | adjust_hologic _ type_enc = type_enc
fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars
| no_type_classes poly = poly
-fun adjust_type_enc (THF (Polymorphic, choice)) (Native (order, poly, level)) =
- Native (adjust_order choice order, no_type_classes poly, level)
- | adjust_type_enc (THF (Monomorphic, choice)) (Native (order, _, level)) =
- Native (adjust_order choice order, Mangled_Monomorphic, level)
+fun adjust_type_enc (THF (Polymorphic, hologic)) (Native (order, poly, level)) =
+ Native (adjust_hologic hologic order, no_type_classes poly, level)
+ | adjust_type_enc (THF (Monomorphic, hologic)) (Native (order, _, level)) =
+ Native (adjust_hologic hologic order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) =
Native (First_Order, Mangled_Monomorphic, level)
| adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =
@@ -881,14 +889,15 @@
fun raw_atp_type_of_typ type_enc =
let
fun term (Type (s, Ts)) =
- AType ((case (is_type_enc_higher_order type_enc, s) of
- (true, @{type_name bool}) => `I tptp_bool_type
- | (true, @{type_name fun}) => `I tptp_fun_type
- | _ =>
- if s = fused_infinite_type_name andalso is_type_enc_native type_enc then
- `I tptp_individual_type
- else
- `make_fixed_type_const s, []), map term Ts)
+ AType
+ ((if s = @{type_name fun} andalso is_type_enc_higher_order type_enc then
+ `I tptp_fun_type
+ else if s = @{type_name bool} andalso is_type_enc_full_higher_order type_enc then
+ `I tptp_bool_type
+ else if s = fused_infinite_type_name andalso is_type_enc_native type_enc then
+ `I tptp_individual_type
+ else
+ `make_fixed_type_const s, []), map term Ts)
| term (TFree (s, _)) = AType ((`make_tfree s, []), [])
| term (TVar z) = AType ((tvar_name z, []), [])
in term end
@@ -927,13 +936,22 @@
if is_type_enc_polymorphic type_enc then to_poly_atype
else to_mangled_atype
fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
+ fun to_ho (ty as AType (((s, _), _), tys)) =
+ if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
+ | to_ho _ = raise Fail "unexpected type"
+ fun to_lfho (ty as AType (((s, _), _), tys)) =
+ if s = tptp_fun_type then to_afun to_ho to_lfho tys
+ else if pred_sym then bool_atype
+ else to_atype ty
+ | to_lfho _ = raise Fail "unexpected type"
fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
| to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
| to_fo _ _ = raise Fail "unexpected type"
- fun to_ho (ty as AType (((s, _), _), tys)) =
- if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
- | to_ho _ = raise Fail "unexpected type"
- in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
+ in
+ if is_type_enc_full_higher_order type_enc then to_ho
+ else if is_type_enc_higher_order type_enc then to_lfho
+ else to_fo ary
+ end
fun native_atp_type_of_typ type_enc pred_sym ary =
native_atp_type_of_raw_atp_type type_enc pred_sym ary o raw_atp_type_of_typ type_enc
@@ -1082,7 +1100,7 @@
| intro top_level args (IConst (name as (s, _), T, T_args)) =
(case proxify_const s of
SOME proxy_base =>
- if top_level orelse is_type_enc_higher_order type_enc then
+ if top_level orelse is_type_enc_full_higher_order type_enc then
(case (top_level, s) of
(_, "c_False") => IConst (`I tptp_false, T, [])
| (_, "c_True") => IConst (`I tptp_true, T, [])
@@ -1238,7 +1256,7 @@
|> transform_elim_prop
|> Object_Logic.atomize_term ctxt
val need_trueprop = (fastype_of t = @{typ bool})
- val is_ho = is_type_enc_higher_order type_enc
+ val is_ho = is_type_enc_full_higher_order type_enc
in
t |> need_trueprop ? HOLogic.mk_Trueprop
|> (if is_ho then unextensionalize_def
@@ -1251,7 +1269,7 @@
(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical
reasons. *)
fun should_use_iff_for_eq CNF _ = false
- | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
+ | should_use_iff_for_eq (THF _) format = not (is_type_enc_full_higher_order format)
| should_use_iff_for_eq _ _ = true
fun make_formula ctxt format type_enc iff_for_eq name stature role t =
@@ -1393,7 +1411,7 @@
|> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @
([tptp_equal, tptp_old_equal]
|> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false}))
- |> not (is_type_enc_higher_order type_enc)
+ |> not (is_type_enc_full_higher_order type_enc)
? cons (prefixed_predicator_name,
{pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false})
@@ -1592,7 +1610,8 @@
if is_pred_sym sym_tab s then tm else predicatify completish tm
| _ => predicatify completish tm)
val do_iterm =
- not (is_type_enc_higher_order type_enc) ? (introduce_app_ops #> introduce_predicators)
+ (not (is_type_enc_higher_order type_enc) ? introduce_app_ops)
+ #> (not (is_type_enc_full_higher_order type_enc) ? introduce_predicators)
#> filter_type_args_in_iterm thy ctrss type_enc
in update_iformula (formula_map do_iterm) end
@@ -2595,7 +2614,7 @@
else
Sufficient_App_Op_And_Predicator
val lam_trans =
- if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
+ if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN
else lam_trans
val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts
--- a/src/HOL/Tools/ATP/atp_proof.ML Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue May 22 19:58:17 2018 +0100
@@ -54,6 +54,7 @@
val e_parN : string
val e_sineN : string
val e_tofofN : string
+ val ehohN : string
val iproverN : string
val iprover_eqN : string
val leo2N : string
@@ -124,6 +125,7 @@
val e_parN = "e_par"
val e_sineN = "e_sine"
val e_tofofN = "e_tofof"
+val ehohN = "ehoh"
val iproverN = "iprover"
val iprover_eqN = "iprover_eq"
val leo2N = "leo2"
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue May 22 19:58:17 2018 +0100
@@ -353,6 +353,32 @@
val e_par = (e_parN, fn () => e_par_config)
+(* Ehoh *)
+
+val ehoh_thf0 = THF (Monomorphic, THF_Lambda_Free)
+
+val ehoh_config : atp_config =
+ {exec = fn _ => (["E_HOME"], ["eprover"]),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+ "--auto-schedule --tstp-in --tstp-out --silent --cpu-limit=" ^
+ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ file_name,
+ proof_delims =
+ [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
+ tstp_proof_delims,
+ known_failures =
+ [(TimedOut, "Failure: Resource limit exceeded (time)"),
+ (TimedOut, "time limit exceeded")] @
+ known_szs_status_failures,
+ prem_role = Conjecture,
+ best_slices =
+ (* FUDGE *)
+ K [(1.0, (((500, ""), ehoh_thf0, "mono_native_higher", liftingN, false), ""))],
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = default_max_new_mono_instances}
+
+val ehoh = (ehohN, fn () => ehoh_config)
+
+
(* iProver *)
val iprover_config : atp_config =
@@ -792,10 +818,11 @@
end
val atps =
- [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, leo3, satallax, spass, vampire,
- z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
- remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, remote_satallax,
- remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
+ [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, satallax, spass,
+ vampire, z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e,
+ remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3,
+ remote_satallax, remote_vampire, remote_snark, remote_pirate, remote_waldmeister,
+ remote_waldmeister_new]
val _ = Theory.setup (fold add_atp atps)
--- a/src/HOL/ex/Quicksort.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/ex/Quicksort.thy Tue May 22 19:58:17 2018 +0100
@@ -13,11 +13,11 @@
fun quicksort :: "'a list \<Rightarrow> 'a list" where
"quicksort [] = []"
-| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+| "quicksort (x#xs) = quicksort (filter (\<lambda>y. \<not> x\<le>y) xs) @ [x] @ quicksort (filter (\<lambda>y. x\<le>y) xs)"
lemma [code]:
"quicksort [] = []"
- "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+ "quicksort (x#xs) = quicksort (filter (\<lambda>y. \<not> x\<le>y) xs) @ [x] @ quicksort (filter (\<lambda>y. x\<le>y) xs)"
by (simp_all add: not_le)
lemma quicksort_permutes [simp]:
--- a/src/HOL/ex/Radix_Sort.thy Mon May 21 22:52:16 2018 +0100
+++ b/src/HOL/ex/Radix_Sort.thy Tue May 22 19:58:17 2018 +0100
@@ -44,7 +44,7 @@
lemma sorted_from_Suc2:
"\<lbrakk> cols xss n; i < n;
sorted_col i xss;
- \<And>x. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = x] \<rbrakk>
+ \<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss) \<rbrakk>
\<Longrightarrow> sorted_from i xss"
proof(induction xss rule: induct_list012)
case 1 show ?case by simp
@@ -68,7 +68,7 @@
proof(rule "3.IH"[OF _ "3.prems"(2)])
show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def)
show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp
- show "\<And>x. sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = x]"
+ show "\<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (xs2 # xss))"
using "3.prems"(4)
sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]]
by fastforce
@@ -81,7 +81,7 @@
shows "sorted_from i (sort_col i xss)"
proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)])
show "sorted_col i (sort_col i xss)" by(simp add: sorted)
- fix x show "sorted_from (i+1) [ys \<leftarrow> sort_col i xss . ys ! i = x]"
+ fix x show "sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (sort_col i xss))"
proof -
from assms(3)
have "sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss)"
--- a/src/Pure/global_theory.ML Mon May 21 22:52:16 2018 +0100
+++ b/src/Pure/global_theory.ML Tue May 22 19:58:17 2018 +0100
@@ -128,8 +128,19 @@
fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
-fun add_facts arg thy =
- thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2);
+fun add_facts (b, fact) thy =
+ let
+ val full_name = Sign.full_name thy b;
+ val pos = Binding.pos_of b;
+ fun err msg =
+ error ("Malformed global fact " ^ quote full_name ^ Position.here pos ^ "\n" ^ msg);
+ fun check thm =
+ ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes (Thm.full_prop_of thm)))
+ handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
+ val arg = (b, Lazy.map_finished (tap (List.app check)) fact);
+ in
+ thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
+ end;
fun add_thms_lazy kind (b, thms) thy =
if Binding.is_empty b then Thm.register_proofs thms thy