18 |
18 |
19 definition bigo :: "('a => 'b\<Colon>{linordered_idom,number_ring}) => ('a => 'b) set" ("(1O'(_'))") where |
19 definition bigo :: "('a => 'b\<Colon>{linordered_idom,number_ring}) => ('a => 'b) set" ("(1O'(_'))") where |
20 "O(f\<Colon>('a => 'b)) == {h. \<exists>c. \<forall>x. abs (h x) <= c * abs (f x)}" |
20 "O(f\<Colon>('a => 'b)) == {h. \<exists>c. \<forall>x. abs (h x) <= c * abs (f x)}" |
21 |
21 |
22 lemma bigo_pos_const: |
22 lemma bigo_pos_const: |
23 "(\<exists>(c\<Colon>'a\<Colon>linordered_idom). |
23 "(\<exists>c\<Colon>'a\<Colon>linordered_idom. |
24 \<forall>x. (abs (h x)) <= (c * (abs (f x)))) |
24 \<forall>x. abs (h x) \<le> c * abs (f x)) |
25 = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))" |
25 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
26 by (metis (hide_lams, no_types) abs_ge_zero |
26 by (metis (no_types) abs_ge_zero |
27 comm_semiring_1_class.normalizing_semiring_rules(7) mult.comm_neutral |
27 comm_semiring_1_class.normalizing_semiring_rules(7) mult.comm_neutral |
28 mult_nonpos_nonneg not_leE order_trans zero_less_one) |
28 mult_nonpos_nonneg not_leE order_trans zero_less_one) |
29 |
29 |
30 (*** Now various verions with an increasing shrink factor ***) |
30 (*** Now various verions with an increasing shrink factor ***) |
31 |
31 |
32 sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
32 sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
33 |
33 |
34 lemma |
34 lemma |
35 "(\<exists>(c\<Colon>'a\<Colon>linordered_idom). |
35 "(\<exists>c\<Colon>'a\<Colon>linordered_idom. |
36 \<forall>x. (abs (h x)) <= (c * (abs (f x)))) |
36 \<forall>x. abs (h x) \<le> c * abs (f x)) |
37 = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))" |
37 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
38 apply auto |
38 apply auto |
39 apply (case_tac "c = 0", simp) |
39 apply (case_tac "c = 0", simp) |
40 apply (rule_tac x = "1" in exI, simp) |
40 apply (rule_tac x = "1" in exI, simp) |
41 apply (rule_tac x = "abs c" in exI, auto) |
41 apply (rule_tac x = "abs c" in exI, auto) |
42 proof - |
42 proof - |
61 qed |
61 qed |
62 |
62 |
63 sledgehammer_params [isar_proof, isar_shrink_factor = 2] |
63 sledgehammer_params [isar_proof, isar_shrink_factor = 2] |
64 |
64 |
65 lemma |
65 lemma |
66 "(\<exists>(c\<Colon>'a\<Colon>linordered_idom). |
66 "(\<exists>c\<Colon>'a\<Colon>linordered_idom. |
67 \<forall>x. (abs (h x)) <= (c * (abs (f x)))) |
67 \<forall>x. abs (h x) \<le> c * abs (f x)) |
68 = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))" |
68 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
69 apply auto |
69 apply auto |
70 apply (case_tac "c = 0", simp) |
70 apply (case_tac "c = 0", simp) |
71 apply (rule_tac x = "1" in exI, simp) |
71 apply (rule_tac x = "1" in exI, simp) |
72 apply (rule_tac x = "abs c" in exI, auto) |
72 apply (rule_tac x = "abs c" in exI, auto) |
73 proof - |
73 proof - |
84 qed |
84 qed |
85 |
85 |
86 sledgehammer_params [isar_proof, isar_shrink_factor = 3] |
86 sledgehammer_params [isar_proof, isar_shrink_factor = 3] |
87 |
87 |
88 lemma |
88 lemma |
89 "(\<exists>(c\<Colon>'a\<Colon>linordered_idom). |
89 "(\<exists>c\<Colon>'a\<Colon>linordered_idom. |
90 \<forall>x. (abs (h x)) <= (c * (abs (f x)))) |
90 \<forall>x. abs (h x) \<le> c * abs (f x)) |
91 = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))" |
91 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
92 apply auto |
92 apply auto |
93 apply (case_tac "c = 0", simp) |
93 apply (case_tac "c = 0", simp) |
94 apply (rule_tac x = "1" in exI, simp) |
94 apply (rule_tac x = "1" in exI, simp) |
95 apply (rule_tac x = "abs c" in exI, auto) |
95 apply (rule_tac x = "abs c" in exI, auto) |
96 proof - |
96 proof - |
104 qed |
104 qed |
105 |
105 |
106 sledgehammer_params [isar_proof, isar_shrink_factor = 4] |
106 sledgehammer_params [isar_proof, isar_shrink_factor = 4] |
107 |
107 |
108 lemma |
108 lemma |
109 "(\<exists>(c\<Colon>'a\<Colon>linordered_idom). |
109 "(\<exists>c\<Colon>'a\<Colon>linordered_idom. |
110 \<forall>x. (abs (h x)) <= (c * (abs (f x)))) |
110 \<forall>x. abs (h x) \<le> c * abs (f x)) |
111 = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))" |
111 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
112 apply auto |
112 apply auto |
113 apply (case_tac "c = 0", simp) |
113 apply (case_tac "c = 0", simp) |
114 apply (rule_tac x = "1" in exI, simp) |
114 apply (rule_tac x = "1" in exI, simp) |
115 apply (rule_tac x = "abs c" in exI, auto) |
115 apply (rule_tac x = "abs c" in exI, auto) |
116 proof - |
116 proof - |
123 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult) |
123 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult) |
124 qed |
124 qed |
125 |
125 |
126 sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
126 sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
127 |
127 |
128 lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c & (\<forall>x. abs (h x) <= c * abs (f x)))}" |
128 lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}" |
129 by (auto simp add: bigo_def bigo_pos_const) |
129 by (auto simp add: bigo_def bigo_pos_const) |
130 |
130 |
131 lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) <= O(g)" |
131 lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) \<le> O(g)" |
132 apply (auto simp add: bigo_alt_def) |
132 apply (auto simp add: bigo_alt_def) |
133 apply (rule_tac x = "ca * c" in exI) |
133 apply (rule_tac x = "ca * c" in exI) |
134 apply (rule conjI) |
134 by (metis comm_semiring_1_class.normalizing_semiring_rules(7,19) |
135 apply (rule mult_pos_pos) |
135 mult_le_cancel_left_pos order_trans mult_pos_pos) |
136 apply (assumption)+ |
|
137 (* sledgehammer *) |
|
138 apply (rule allI) |
|
139 apply (drule_tac x = "xa" in spec)+ |
|
140 apply (subgoal_tac "ca * abs (f xa) <= ca * (c * abs (g xa))") |
|
141 apply (metis comm_semiring_1_class.normalizing_semiring_rules(19) |
|
142 comm_semiring_1_class.normalizing_semiring_rules(7) order_trans) |
|
143 by (metis mult_le_cancel_left_pos) |
|
144 |
136 |
145 lemma bigo_refl [intro]: "f : O(f)" |
137 lemma bigo_refl [intro]: "f : O(f)" |
146 apply (auto simp add: bigo_def) |
138 unfolding bigo_def mem_Collect_eq |
147 by (metis mult_1 order_refl) |
139 by (metis mult_1 order_refl) |
148 |
140 |
149 lemma bigo_zero: "0 : O(g)" |
141 lemma bigo_zero: "0 : O(g)" |
150 apply (auto simp add: bigo_def func_zero) |
142 apply (auto simp add: bigo_def func_zero) |
151 by (metis mult_zero_left order_refl) |
143 by (metis mult_zero_left order_refl) |
762 |
754 |
763 lemma bigo_lesso1: "\<forall>x. f x <= g x \<Longrightarrow> f <o g =o O(h)" |
755 lemma bigo_lesso1: "\<forall>x. f x <= g x \<Longrightarrow> f <o g =o O(h)" |
764 apply (unfold lesso_def) |
756 apply (unfold lesso_def) |
765 apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0") |
757 apply (subgoal_tac "(\<lambda>x. max (f x - g x) 0) = 0") |
766 apply (metis bigo_zero) |
758 apply (metis bigo_zero) |
767 by (metis (lam_lifting, no_types) func_zero le_fun_def le_iff_diff_le_0 |
759 by (metis (lifting, no_types) func_zero le_fun_def le_iff_diff_le_0 |
768 min_max.sup_absorb2 order_eq_iff) |
760 min_max.sup_absorb2 order_eq_iff) |
769 |
761 |
770 lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow> |
762 lemma bigo_lesso2: "f =o g +o O(h) \<Longrightarrow> |
771 \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. k x <= f x \<Longrightarrow> |
763 \<forall>x. 0 <= k x \<Longrightarrow> \<forall>x. k x <= f x \<Longrightarrow> |
772 k <o g =o O(h)" |
764 k <o g =o O(h)" |