src/HOL/Metis_Examples/Big_O.thy

 begin
 
 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)
 
 (*** Now various verions with an increasing shrink factor ***)
 
 sledgehammer_params [isar_proofs, compress = 1]
 
 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>"
   have F1: "\<forall>x\<^sub>1::'a::linordered_idom. 0 \<le> \<bar>x\<^sub>1\<bar>" by (metis abs_ge_zero)
   have F2: "\<forall>x\<^sub>1::'a::linordered_idom. 1 * x\<^sub>1 = x\<^sub>1" by (metis mult_1)

 
 sledgehammer_params [isar_proofs, compress = 2]
 
 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>"
   have F1: "\<forall>x\<^sub>1::'a::linordered_idom. 1 * x\<^sub>1 = x\<^sub>1" by (metis mult_1)
   have F2: "\<forall>x\<^sub>2 x\<^sub>3::'a::linordered_idom. \<bar>x\<^sub>3\<bar> * \<bar>x\<^sub>2\<bar> = \<bar>x\<^sub>3 * x\<^sub>2\<bar>"

 
 sledgehammer_params [isar_proofs, compress = 3]
 
 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>"
   have F1: "\<forall>x\<^sub>1::'a::linordered_idom. 1 * x\<^sub>1 = x\<^sub>1" by (metis mult_1)
   have F2: "\<forall>x\<^sub>3 x\<^sub>1::'a::linordered_idom. 0 \<le> x\<^sub>1 \<longrightarrow> \<bar>x\<^sub>3 * x\<^sub>1\<bar> = \<bar>x\<^sub>3\<bar> * x\<^sub>1" by (metis abs_mult_pos)

 
 sledgehammer_params [isar_proofs, compress = 4]
 
 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>"
   have "\<forall>x\<^sub>1::'a::linordered_idom. 1 * x\<^sub>1 = x\<^sub>1" by (metis mult_1)
   hence "\<forall>x\<^sub>3. \<bar>c * \<bar>f x\<^sub>3\<bar>\<bar> = c * \<bar>f x\<^sub>3\<bar>"

   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
 qed
 
 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)"
 apply (auto simp add: bigo_alt_def)
 apply (rule_tac x = "ca * c" in exI)

 
 lemma bigo_plus_subset [intro]: "O(f + g) <= O(f) + O(g)"
 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)
 
 lemma bigo_plus_subset2 [intro]: "A <= O(f) \<Longrightarrow> B <= O(f) \<Longrightarrow> A + B <= O(f)"

  apply (metis less_max_iff_disj)
 apply clarify
 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)
  apply (metis add_nonneg_nonneg)
 apply (rule add_mono)

  apply (metis add_le_cancel_left diff_add_cancel diff_self minus_apply
               algebra_simps)
 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)
   have "\<forall>u. u \<in> O(\<lambda>R. \<bar>u R\<bar>)" by (metis bigo_abs2)
   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)
     by (metis abs_triangle_ineq3)
   also have "... <= O(f - g)"

     apply (subst fun_diff_def)
     apply (rule bigo_abs)
     done
   also have "... <= O(h)"
     using a by (rule bigo_elt_subset)
-  finally show "(\<lambda>x. abs (f x) - abs (g x)) : O(h)".
-qed
-
-lemma bigo_abs5: "f =o O(g) \<Longrightarrow> (\<lambda>x. abs(f x)) =o O(g)"
+  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. \<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)"
 proof -
   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])
 qed
 

             simp add: bigo_alt_def set_times_def func_times)
 (* sledgehammer *)
 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)
 
 lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
 by (metis bigo_mult bigo_refl set_times_mono3 subset_trans)

 lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
   apply (auto intro!: subsetI
     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)
   apply (erule spec)
   apply simp

 done
 
 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
 apply (subst setsum_right_distrib)
 apply (rule allI)

  apply (rule setsum_abs)
 apply (rule setsum_mono)
 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)
 apply (unfold bigo_def)
 apply (auto simp add: abs_mult)
 by (metis abs_ge_zero mult.left_commute mult_left_mono)
 
 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])
 apply (subst right_diff_distrib [symmetric])
 apply (rule bigo_setsum3)

 lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
     \<forall>x. 0 <= h x \<Longrightarrow>
       (\<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)
 apply (rule setsum.cong)
 apply (rule refl)

 subsection {* Less than or equal to *}
 
 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)
 done
 

   apply (subst abs_of_nonneg)
   apply (erule spec)+
 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)
   apply (subst abs_of_nonneg)
   apply (erule spec)+

 apply (erule bigo_lesseq2) back
 apply (rule allI)
 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)
 
 end