src/HOL/Metis_Examples/Big_O.thy
 changeset 50020 6b9611abcd4c parent 49918 cf441f4a358b child 51130 76d68444cd59
```     1.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Tue Nov 06 15:12:31 2012 +0100
1.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Tue Nov 06 15:15:33 2012 +0100
1.3 @@ -29,7 +29,7 @@
1.4
1.5  (*** Now various verions with an increasing shrink factor ***)
1.6
1.7 -sledgehammer_params [isar_proofs, isar_shrinkage = 1]
1.8 +sledgehammer_params [isar_proofs, isar_shrink = 1]
1.9
1.10  lemma
1.11    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
1.12 @@ -60,7 +60,7 @@
1.13    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
1.14  qed
1.15
1.16 -sledgehammer_params [isar_proofs, isar_shrinkage = 2]
1.17 +sledgehammer_params [isar_proofs, isar_shrink = 2]
1.18
1.19  lemma
1.20    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
1.21 @@ -83,7 +83,7 @@
1.22    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
1.23  qed
1.24
1.25 -sledgehammer_params [isar_proofs, isar_shrinkage = 3]
1.26 +sledgehammer_params [isar_proofs, isar_shrink = 3]
1.27
1.28  lemma
1.29    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
1.30 @@ -103,7 +103,7 @@
1.31    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
1.32  qed
1.33
1.34 -sledgehammer_params [isar_proofs, isar_shrinkage = 4]
1.35 +sledgehammer_params [isar_proofs, isar_shrink = 4]
1.36
1.37  lemma
1.38    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
1.39 @@ -123,7 +123,7 @@
1.40    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
1.41  qed
1.42
1.43 -sledgehammer_params [isar_proofs, isar_shrinkage = 1]
1.44 +sledgehammer_params [isar_proofs, isar_shrink = 1]
1.45
1.46  lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
1.47  by (auto simp add: bigo_def bigo_pos_const)
```