--- a/src/HOL/Metis_Examples/Big_O.thy Mon Dec 28 01:26:34 2015 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Mon Dec 28 01:28:28 2015 +0100
@@ -17,12 +17,12 @@
subsection {* Definitions *}
definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where
- "O(f::('a => 'b)) == {h. \<exists>c. \<forall>x. abs (h x) <= c * abs (f x)}"
+ "O(f::('a => 'b)) == {h. \<exists>c. \<forall>x. \<bar>h x\<bar> <= c * \<bar>f x\<bar>}"
lemma bigo_pos_const:
"(\<exists>c::'a::linordered_idom.
- \<forall>x. abs (h x) \<le> c * abs (f x))
- \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+ \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+ \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
by (metis (no_types) abs_ge_zero
algebra_simps mult.comm_neutral
mult_nonpos_nonneg not_le_imp_less order_trans zero_less_one)
@@ -33,12 +33,12 @@
lemma
"(\<exists>c::'a::linordered_idom.
- \<forall>x. abs (h x) \<le> c * abs (f x))
- \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+ \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+ \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -64,12 +64,12 @@
lemma
"(\<exists>c::'a::linordered_idom.
- \<forall>x. abs (h x) \<le> c * abs (f x))
- \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+ \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+ \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -87,12 +87,12 @@
lemma
"(\<exists>c::'a::linordered_idom.
- \<forall>x. abs (h x) \<le> c * abs (f x))
- \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+ \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+ \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -107,12 +107,12 @@
lemma
"(\<exists>c::'a::linordered_idom.
- \<forall>x. abs (h x) \<le> c * abs (f x))
- \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+ \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)
+ \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
- apply (rule_tac x = "abs c" in exI, auto)
+ apply (rule_tac x = "\<bar>c\<bar>" in exI, auto)
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
@@ -125,7 +125,7 @@
sledgehammer_params [isar_proofs, compress = 1]
-lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
+lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. \<bar>h x\<bar> <= c * \<bar>f x\<bar>))}"
by (auto simp add: bigo_def bigo_pos_const)
lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) \<le> O(g)"
@@ -160,25 +160,25 @@
apply (rule subsetI)
apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
apply (subst bigo_pos_const [symmetric])+
-apply (rule_tac x = "\<lambda>n. if abs (g n) <= (abs (f n)) then x n else 0" in exI)
+apply (rule_tac x = "\<lambda>n. if \<bar>g n\<bar> <= \<bar>f n\<bar> then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply clarsimp
- apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
+ apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= (c + c) * \<bar>f xa\<bar>")
apply (metis mult_2 order_trans)
- apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+ apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
apply (erule order_trans)
apply (simp add: ring_distribs)
apply (rule mult_left_mono)
apply (simp add: abs_triangle_ineq)
apply (simp add: order_less_le)
-apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
+apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply auto
-apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
+apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= (c + c) * \<bar>g xa\<bar>")
apply (metis order_trans mult_2)
-apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> <= c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
apply (erule order_trans)
apply (simp add: ring_distribs)
by (metis abs_triangle_ineq mult_le_cancel_left_pos)
@@ -200,9 +200,8 @@
apply (drule_tac x = "xa" in spec)+
apply (subgoal_tac "0 <= f xa + g xa")
apply (simp add: ring_distribs)
- apply (subgoal_tac "abs (a xa + b xa) <= abs (a xa) + abs (b xa)")
- apply (subgoal_tac "abs (a xa) + abs (b xa) <=
- max c ca * f xa + max c ca * g xa")
+ apply (subgoal_tac "\<bar>a xa + b xa\<bar> <= \<bar>a xa\<bar> + \<bar>b xa\<bar>")
+ apply (subgoal_tac "\<bar>a xa\<bar> + \<bar>b xa\<bar> <= max c ca * f xa + max c ca * g xa")
apply (metis order_trans)
defer 1
apply (metis abs_triangle_ineq)
@@ -236,17 +235,17 @@
by (metis add_le_cancel_left diff_add_cancel func_plus le_fun_def
algebra_simps)
-lemma bigo_abs: "(\<lambda>x. abs(f x)) =o O(f)"
+lemma bigo_abs: "(\<lambda>x. \<bar>f x\<bar>) =o O(f)"
apply (unfold bigo_def)
apply auto
by (metis mult_1 order_refl)
-lemma bigo_abs2: "f =o O(\<lambda>x. abs(f x))"
+lemma bigo_abs2: "f =o O(\<lambda>x. \<bar>f x\<bar>)"
apply (unfold bigo_def)
apply auto
by (metis mult_1 order_refl)
-lemma bigo_abs3: "O(f) = O(\<lambda>x. abs(f x))"
+lemma bigo_abs3: "O(f) = O(\<lambda>x. \<bar>f x\<bar>)"
proof -
have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset)
have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs)
@@ -254,15 +253,15 @@
thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto
qed
-lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. abs (f x)) =o (\<lambda>x. abs (g x)) +o O(h)"
+lemma bigo_abs4: "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o (\<lambda>x. \<bar>g x\<bar>) +o O(h)"
apply (drule set_plus_imp_minus)
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
proof -
assume a: "f - g : O(h)"
- have "(\<lambda>x. abs (f x) - abs (g x)) =o O(\<lambda>x. abs(abs (f x) - abs (g x)))"
+ have "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) =o O(\<lambda>x. \<bar>\<bar>f x\<bar> - \<bar>g x\<bar>\<bar>)"
by (rule bigo_abs2)
- also have "... <= O(\<lambda>x. abs (f x - g x))"
+ also have "... <= O(\<lambda>x. \<bar>f x - g x\<bar>)"
apply (rule bigo_elt_subset)
apply (rule bigo_bounded)
apply (metis abs_ge_zero)
@@ -274,10 +273,10 @@
done
also have "... <= O(h)"
using a by (rule bigo_elt_subset)
- finally show "(\<lambda>x. abs (f x) - abs (g x)) : O(h)".
+ finally show "(\<lambda>x. \<bar>f x\<bar> - \<bar>g x\<bar>) : O(h)" .
qed
-lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs(f x)) =o O(g)"
+lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) =o O(g)"
by (unfold bigo_def, auto)
lemma bigo_elt_subset2 [intro]: "f : g +o O(h) \<Longrightarrow> O(f) <= O(g) + O(h)"
@@ -285,14 +284,14 @@
assume "f : g +o O(h)"
also have "... <= O(g) + O(h)"
by (auto del: subsetI)
- also have "... = O(\<lambda>x. abs(g x)) + O(\<lambda>x. abs(h x))"
+ also have "... = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
by (metis bigo_abs3)
- also have "... = O((\<lambda>x. abs(g x)) + (\<lambda>x. abs(h x)))"
+ also have "... = O((\<lambda>x. \<bar>g x\<bar>) + (\<lambda>x. \<bar>h x\<bar>))"
by (rule bigo_plus_eq [symmetric], auto)
finally have "f : ...".
then have "O(f) <= ..."
by (elim bigo_elt_subset)
- also have "... = O(\<lambda>x. abs(g x)) + O(\<lambda>x. abs(h x))"
+ also have "... = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
by (rule bigo_plus_eq, auto)
finally show ?thesis
by (simp add: bigo_abs3 [symmetric])
@@ -307,7 +306,7 @@
apply (rule_tac x = "c * ca" in exI)
apply (rule allI)
apply (erule_tac x = x in allE)+
-apply (subgoal_tac "c * ca * abs (f x * g x) = (c * abs(f x)) * (ca * abs (g x))")
+apply (subgoal_tac "c * ca * \<bar>f x * g x\<bar> = (c * \<bar>f x\<bar>) * (ca * \<bar>g x\<bar>)")
apply (metis (no_types) abs_ge_zero abs_mult mult_mono')
by (metis mult.assoc mult.left_commute abs_of_pos mult.left_commute abs_mult)
@@ -466,9 +465,9 @@
simp add: bigo_def elt_set_times_def func_times
simp del: abs_mult ac_simps)
(* sledgehammer *)
- apply (rule_tac x = "ca * (abs c)" in exI)
+ apply (rule_tac x = "ca * \<bar>c\<bar>" in exI)
apply (rule allI)
- apply (subgoal_tac "ca * abs(c) * abs(f x) = abs(c) * (ca * abs(f x))")
+ apply (subgoal_tac "ca * \<bar>c\<bar> * \<bar>f x\<bar> = \<bar>c\<bar> * (ca * \<bar>f x\<bar>)")
apply (erule ssubst)
apply (subst abs_mult)
apply (rule mult_left_mono)
@@ -493,10 +492,10 @@
subsection {* Setsum *}
lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 <= h x y \<Longrightarrow>
- \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) <= c * (h x y) \<Longrightarrow>
+ \<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
(\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
apply (auto simp add: bigo_def)
-apply (rule_tac x = "abs c" in exI)
+apply (rule_tac x = "\<bar>c\<bar>" in exI)
apply (subst abs_of_nonneg) back back
apply (rule setsum_nonneg)
apply force
@@ -508,19 +507,19 @@
by (metis abs_ge_self abs_mult_pos order_trans)
lemma bigo_setsum1: "\<forall>x y. 0 <= h x y \<Longrightarrow>
- \<exists>c. \<forall>x y. abs (f x y) <= c * (h x y) \<Longrightarrow>
+ \<exists>c. \<forall>x y. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
(\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
by (metis (no_types) bigo_setsum_main)
lemma bigo_setsum2: "\<forall>y. 0 <= h y \<Longrightarrow>
- \<exists>c. \<forall>y. abs (f y) <= c * (h y) \<Longrightarrow>
+ \<exists>c. \<forall>y. \<bar>f y\<bar> <= c * (h y) \<Longrightarrow>
(\<lambda>x. SUM y : A x. f y) =o O(\<lambda>x. SUM y : A x. h y)"
apply (rule bigo_setsum1)
by metis+
lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
(\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
- O(\<lambda>x. SUM y : A x. abs(l x y * h(k x y)))"
+ O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
apply (rule bigo_setsum1)
apply (rule allI)+
apply (rule abs_ge_zero)
@@ -531,7 +530,7 @@
lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
(\<lambda>x. SUM y : A x. l x y * f(k x y)) =o
(\<lambda>x. SUM y : A x. l x y * g(k x y)) +o
- O(\<lambda>x. SUM y : A x. abs(l x y * h(k x y)))"
+ O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
apply (subst setsum_subtractf [symmetric])
@@ -544,7 +543,7 @@
(\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
- (\<lambda>x. SUM y : A x. abs((l x y) * h(k x y)))")
+ (\<lambda>x. SUM y : A x. \<bar>(l x y) * h(k x y)\<bar>)")
apply (erule ssubst)
apply (erule bigo_setsum3)
apply (rule ext)
@@ -616,14 +615,14 @@
definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where
"f <o g == (\<lambda>x. max (f x - g x) 0)"
-lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) <= abs (f x) \<Longrightarrow>
+lemma bigo_lesseq1: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> <= \<bar>f x\<bar> \<Longrightarrow>
g =o O(h)"
apply (unfold bigo_def)
apply clarsimp
apply (blast intro: order_trans)
done
-lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. abs (g x) <= f x \<Longrightarrow>
+lemma bigo_lesseq2: "f =o O(h) \<Longrightarrow> \<forall>x. \<bar>g x\<bar> <= f x \<Longrightarrow>
g =o O(h)"
apply (erule bigo_lesseq1)
apply (blast intro: abs_ge_self order_trans)
@@ -638,7 +637,7 @@
done
lemma bigo_lesseq4: "f =o O(h) \<Longrightarrow>
- \<forall>x. 0 <= g x \<Longrightarrow> \<forall>x. g x <= abs (f x) \<Longrightarrow>
+ \<forall>x. 0 <= g x \<Longrightarrow> \<forall>x. g x <= \<bar>f x\<bar> \<Longrightarrow>
g =o O(h)"
apply (erule bigo_lesseq1)
apply (rule allI)
@@ -703,7 +702,7 @@
by (auto simp add: func_plus fun_diff_def algebra_simps
split: split_max abs_split)
-lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x <= g x + C * abs (h x)"
+lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x <= g x + C * \<bar>h x\<bar>"
apply (simp only: lesso_def bigo_alt_def)
apply clarsimp
by (metis add.commute diff_le_eq)