src/HOL/Metis_Examples/Big_O.thy
changeset 46364 abab10d1f4a3
parent 45705 a25ff4283352
child 46369 9ac0c64ad8e7
     1.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Mon Jan 30 13:55:28 2012 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Mon Jan 30 17:15:59 2012 +0100
     1.3 @@ -20,10 +20,10 @@
     1.4    "O(f\<Colon>('a => 'b)) == {h. \<exists>c. \<forall>x. abs (h x) <= c * abs (f x)}"
     1.5  
     1.6  lemma bigo_pos_const:
     1.7 -  "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
     1.8 -    \<forall>x. (abs (h x)) <= (c * (abs (f x))))
     1.9 -      = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
    1.10 -by (metis (hide_lams, no_types) abs_ge_zero
    1.11 +  "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    1.12 +    \<forall>x. abs (h x) \<le> c * abs (f x))
    1.13 +    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
    1.14 +by (metis (no_types) abs_ge_zero
    1.15        comm_semiring_1_class.normalizing_semiring_rules(7) mult.comm_neutral
    1.16        mult_nonpos_nonneg not_leE order_trans zero_less_one)
    1.17  
    1.18 @@ -32,9 +32,9 @@
    1.19  sledgehammer_params [isar_proof, isar_shrink_factor = 1]
    1.20  
    1.21  lemma
    1.22 -  "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
    1.23 -    \<forall>x. (abs (h x)) <= (c * (abs (f x))))
    1.24 -      = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
    1.25 +  "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    1.26 +    \<forall>x. abs (h x) \<le> c * abs (f x))
    1.27 +    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
    1.28    apply auto
    1.29    apply (case_tac "c = 0", simp)
    1.30    apply (rule_tac x = "1" in exI, simp)
    1.31 @@ -63,9 +63,9 @@
    1.32  sledgehammer_params [isar_proof, isar_shrink_factor = 2]
    1.33  
    1.34  lemma
    1.35 -  "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
    1.36 -    \<forall>x. (abs (h x)) <= (c * (abs (f x))))
    1.37 -      = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
    1.38 +  "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    1.39 +    \<forall>x. abs (h x) \<le> c * abs (f x))
    1.40 +    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
    1.41    apply auto
    1.42    apply (case_tac "c = 0", simp)
    1.43    apply (rule_tac x = "1" in exI, simp)
    1.44 @@ -86,9 +86,9 @@
    1.45  sledgehammer_params [isar_proof, isar_shrink_factor = 3]
    1.46  
    1.47  lemma
    1.48 -  "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
    1.49 -    \<forall>x. (abs (h x)) <= (c * (abs (f x))))
    1.50 -      = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
    1.51 +  "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    1.52 +    \<forall>x. abs (h x) \<le> c * abs (f x))
    1.53 +    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
    1.54    apply auto
    1.55    apply (case_tac "c = 0", simp)
    1.56    apply (rule_tac x = "1" in exI, simp)
    1.57 @@ -106,9 +106,9 @@
    1.58  sledgehammer_params [isar_proof, isar_shrink_factor = 4]
    1.59  
    1.60  lemma
    1.61 -  "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
    1.62 -    \<forall>x. (abs (h x)) <= (c * (abs (f x))))
    1.63 -      = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
    1.64 +  "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    1.65 +    \<forall>x. abs (h x) \<le> c * abs (f x))
    1.66 +    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
    1.67    apply auto
    1.68    apply (case_tac "c = 0", simp)
    1.69    apply (rule_tac x = "1" in exI, simp)
    1.70 @@ -125,25 +125,17 @@
    1.71  
    1.72  sledgehammer_params [isar_proof, isar_shrink_factor = 1]
    1.73  
    1.74 -lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c & (\<forall>x. abs (h x) <= c * abs (f x)))}"
    1.75 +lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
    1.76  by (auto simp add: bigo_def bigo_pos_const)
    1.77  
    1.78 -lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) <= O(g)"
    1.79 +lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) \<le> O(g)"
    1.80  apply (auto simp add: bigo_alt_def)
    1.81  apply (rule_tac x = "ca * c" in exI)
    1.82 -apply (rule conjI)
    1.83 - apply (rule mult_pos_pos)
    1.84 -  apply (assumption)+
    1.85 -(* sledgehammer *)
    1.86 -apply (rule allI)
    1.87 -apply (drule_tac x = "xa" in spec)+
    1.88 -apply (subgoal_tac "ca * abs (f xa) <= ca * (c * abs (g xa))")
    1.89 - apply (metis comm_semiring_1_class.normalizing_semiring_rules(19)
    1.90 -          comm_semiring_1_class.normalizing_semiring_rules(7) order_trans)
    1.91 -by (metis mult_le_cancel_left_pos)
    1.92 +by (metis comm_semiring_1_class.normalizing_semiring_rules(7,19)
    1.93 +          mult_le_cancel_left_pos order_trans mult_pos_pos)
    1.94  
    1.95  lemma bigo_refl [intro]: "f : O(f)"
    1.96 -apply (auto simp add: bigo_def)
    1.97 +unfolding bigo_def mem_Collect_eq
    1.98  by (metis mult_1 order_refl)
    1.99  
   1.100  lemma bigo_zero: "0 : O(g)"
   1.101 @@ -764,7 +756,7 @@
   1.102  apply (unfold lesso_def)
   1.103  apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0")
   1.104   apply (metis bigo_zero)
   1.105 -by (metis (lam_lifting, no_types) func_zero le_fun_def le_iff_diff_le_0
   1.106 +by (metis (lifting, no_types) func_zero le_fun_def le_iff_diff_le_0
   1.107        min_max.sup_absorb2 order_eq_iff)
   1.108  
   1.109  lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow>