author blanchet Mon, 30 Jan 2012 17:15:59 +0100 changeset 46364 abab10d1f4a3 parent 46363 025db495b40e child 46365 547d1a1dcaf6
example tuning
```--- a/src/HOL/Metis_Examples/Abstraction.thy	Mon Jan 30 13:55:28 2012 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Mon Jan 30 17:15:59 2012 +0100
@@ -48,7 +48,7 @@

lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"

lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
proof -
@@ -110,25 +110,25 @@
"(cl, f) \<in> CLF \<Longrightarrow>
CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
f \<in> pset cl \<inter> cl"
-by (metis (lam_lifting) CollectD Sigma_triv subsetD)
+by (metis (lifting) CollectD Sigma_triv subsetD)

lemma
"(cl, f) \<in> CLF \<Longrightarrow>
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
f \<in> pset cl \<inter> cl"
-by (metis (lam_lifting) CollectD Sigma_triv)
+by (metis (lifting) CollectD Sigma_triv)

lemma
"(cl, f) \<in> CLF \<Longrightarrow>
CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) \<Longrightarrow>
f \<in> pset cl \<rightarrow> pset cl"
-by (metis (lam_lifting) CollectD Sigma_triv subsetD)
+by (metis (lifting) CollectD Sigma_triv subsetD)

lemma
"(cl, f) \<in> CLF \<Longrightarrow>
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
f \<in> pset cl \<rightarrow> pset cl"
-by (metis (lam_lifting) CollectD Sigma_triv)
+by (metis (lifting) CollectD Sigma_triv)

lemma
"(cl, f) \<in> CLF \<Longrightarrow>
@@ -157,7 +157,7 @@
by (metis mem_Collect_eq imageI set_rev_mp)

lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)"
-by (metis (lam_lifting) imageE)
+by (metis (lifting) imageE)

lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
by (metis map_pair_def map_pair_surj_on)```
```--- a/src/HOL/Metis_Examples/Big_O.thy	Mon Jan 30 13:55:28 2012 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Mon Jan 30 17:15:59 2012 +0100
@@ -20,10 +20,10 @@
"O(f\<Colon>('a => 'b)) == {h. \<exists>c. \<forall>x. abs (h x) <= c * abs (f x)}"

lemma bigo_pos_const:
-  "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
-    \<forall>x. (abs (h x)) <= (c * (abs (f x))))
-      = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
-by (metis (hide_lams, no_types) abs_ge_zero
+  "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
+    \<forall>x. abs (h x) \<le> c * abs (f x))
+    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
+by (metis (no_types) abs_ge_zero
comm_semiring_1_class.normalizing_semiring_rules(7) mult.comm_neutral
mult_nonpos_nonneg not_leE order_trans zero_less_one)

@@ -32,9 +32,9 @@
sledgehammer_params [isar_proof, isar_shrink_factor = 1]

lemma
-  "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
-    \<forall>x. (abs (h x)) <= (c * (abs (f x))))
-      = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
+  "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
+    \<forall>x. abs (h x) \<le> c * abs (f x))
+    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
@@ -63,9 +63,9 @@
sledgehammer_params [isar_proof, isar_shrink_factor = 2]

lemma
-  "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
-    \<forall>x. (abs (h x)) <= (c * (abs (f x))))
-      = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
+  "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
+    \<forall>x. abs (h x) \<le> c * abs (f x))
+    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
@@ -86,9 +86,9 @@
sledgehammer_params [isar_proof, isar_shrink_factor = 3]

lemma
-  "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
-    \<forall>x. (abs (h x)) <= (c * (abs (f x))))
-      = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
+  "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
+    \<forall>x. abs (h x) \<le> c * abs (f x))
+    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
@@ -106,9 +106,9 @@
sledgehammer_params [isar_proof, isar_shrink_factor = 4]

lemma
-  "(\<exists>(c\<Colon>'a\<Colon>linordered_idom).
-    \<forall>x. (abs (h x)) <= (c * (abs (f x))))
-      = (\<exists>c. 0 < c & (\<forall>x. (abs(h x)) <= (c * (abs (f x)))))"
+  "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
+    \<forall>x. abs (h x) \<le> c * abs (f x))
+    \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
apply auto
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
@@ -125,25 +125,17 @@

sledgehammer_params [isar_proof, isar_shrink_factor = 1]

-lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c & (\<forall>x. abs (h x) <= c * abs (f x)))}"
+lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
by (auto simp add: bigo_def bigo_pos_const)

-lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) <= O(g)"
+lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) \<le> O(g)"
apply (rule_tac x = "ca * c" in exI)
-apply (rule conjI)
- apply (rule mult_pos_pos)
-  apply (assumption)+
-(* sledgehammer *)
-apply (rule allI)
-apply (drule_tac x = "xa" in spec)+
-apply (subgoal_tac "ca * abs (f xa) <= ca * (c * abs (g xa))")
- apply (metis comm_semiring_1_class.normalizing_semiring_rules(19)
-          comm_semiring_1_class.normalizing_semiring_rules(7) order_trans)
-by (metis mult_le_cancel_left_pos)
+by (metis comm_semiring_1_class.normalizing_semiring_rules(7,19)
+          mult_le_cancel_left_pos order_trans mult_pos_pos)

lemma bigo_refl [intro]: "f : O(f)"