equal
deleted
inserted
replaced
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_proofs, isar_shrinkage = 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) \<le> c * abs (f x)) |
36 \<forall>x. abs (h x) \<le> c * abs (f x)) |
37 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
37 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
58 hence "\<forall>x\<^isub>3. c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F1) |
58 hence "\<forall>x\<^isub>3. c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F1) |
59 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1) |
59 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1) |
60 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4) |
60 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4) |
61 qed |
61 qed |
62 |
62 |
63 sledgehammer_params [isar_proof, isar_shrink_factor = 2] |
63 sledgehammer_params [isar_proofs, isar_shrinkage = 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) \<le> c * abs (f x)) |
67 \<forall>x. abs (h x) \<le> c * abs (f x)) |
68 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
68 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
81 hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F2 abs_mult_pos) |
81 hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F2 abs_mult_pos) |
82 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero) |
82 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero) |
83 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2) |
83 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2) |
84 qed |
84 qed |
85 |
85 |
86 sledgehammer_params [isar_proof, isar_shrink_factor = 3] |
86 sledgehammer_params [isar_proofs, isar_shrinkage = 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) \<le> c * abs (f x)) |
90 \<forall>x. abs (h x) \<le> c * abs (f x)) |
91 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
91 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
101 hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one) |
101 hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one) |
102 hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans) |
102 hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans) |
103 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero) |
103 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero) |
104 qed |
104 qed |
105 |
105 |
106 sledgehammer_params [isar_proof, isar_shrink_factor = 4] |
106 sledgehammer_params [isar_proofs, isar_shrinkage = 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) \<le> c * abs (f x)) |
110 \<forall>x. abs (h x) \<le> c * abs (f x)) |
111 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
111 \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))" |
121 by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) |
121 by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) |
122 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) |
122 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) |
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_proofs, isar_shrinkage = 1] |
127 |
127 |
128 lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<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) \<le> O(g)" |
131 lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) \<le> O(g)" |