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>
```