--- a/src/HOL/Metis_Examples/Abstraction.thy Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy Fri Nov 18 11:47:12 2011 +0100
@@ -13,13 +13,12 @@
declare [[metis_new_skolemizer]]
-(*For Christoph Benzmueller*)
-lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))"
- by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)
+(* For Christoph Benzmüller *)
+lemma "x < 1 \<and> ((op =) = (op =)) \<Longrightarrow> ((op =) = (op =)) \<and> x < (2::nat)"
+by (metis nat_1_add_1 trans_less_add2)
-(*this is a theorem, but we can't prove it unless ext is applied explicitly
-lemma "(op=) = (%x y. y=x)"
-*)
+lemma "(op = ) = (%x y. y = x)"
+by metis
consts
monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
@@ -31,20 +30,18 @@
proof -
assume "a \<in> {x. P x}"
hence "a \<in> P" by (metis Collect_def)
- hence "P a" by (metis mem_def)
- thus "P a" by metis
+ thus "P a" by (metis mem_def)
qed
lemma Collect_triv: "a \<in> {x. P x} ==> P a"
by (metis mem_Collect_eq)
-
declare [[ sledgehammer_problem_prefix = "Abstraction__Collect_mp" ]]
lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
- by (metis Collect_imp_eq ComplD UnE)
+by (metis Collect_imp_eq ComplD UnE)
declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_triv" ]]
-lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
+lemma "(a, b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
proof -
assume A1: "(a, b) \<in> Sigma A B"
hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
@@ -63,7 +60,6 @@
*)
by (meson CollectD SigmaD1 SigmaD2)
-
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
by (metis mem_Sigma_iff singleton_conv2 vimage_Collect_eq vimage_singleton_eq)
@@ -77,7 +73,6 @@
thus "a \<in> A \<and> a = f b" by (metis F1)
qed
-
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_in_pp" ]]
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
by (metis Collect_mem_eq SigmaD2)
@@ -97,6 +92,11 @@
lemma
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
f \<in> pset cl \<rightarrow> pset cl"
+by (metis (no_types) Collect_def Sigma_triv mem_def)
+
+lemma
+ "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
+ f \<in> pset cl \<rightarrow> pset cl"
proof -
assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
@@ -108,7 +108,12 @@
declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Int" ]]
lemma
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
- f \<in> pset cl \<inter> cl"
+ f \<in> pset cl \<inter> cl"
+by (metis (no_types) Collect_conj_eq Int_def Sigma_triv inf_idem)
+
+lemma
+ "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
+ f \<in> pset cl \<inter> cl"
proof -
assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
@@ -119,7 +124,6 @@
thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
qed
-
declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Pi_mono" ]]
lemma
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
@@ -132,14 +136,12 @@
f \<in> pset cl \<inter> cl"
by auto
-
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]]
lemma "(cl,f) \<in> CLF ==>
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
f \<in> pset cl \<inter> cl"
by auto
-
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]]
lemma
"(cl,f) \<in> CLF ==>
@@ -147,7 +149,6 @@
f \<in> pset cl \<rightarrow> pset cl"
by fast
-
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]]
lemma
"(cl,f) \<in> CLF ==>
@@ -155,7 +156,6 @@
f \<in> pset cl \<rightarrow> pset cl"
by auto
-
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]]
lemma
"(cl,f) \<in> CLF ==>
@@ -166,69 +166,44 @@
declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipA" ]]
lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
apply (induct xs)
- apply (metis map_is_Nil_conv zip.simps(1))
-by auto
+ apply (metis map.simps(1) zip_Nil)
+by (metis (lam_lifting, no_types) map.simps(2) zip_Cons_Cons)
declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipB" ]]
lemma "map (%w. (w -> w, w \<times> w)) xs =
zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
apply (induct xs)
- apply (metis Nil_is_map_conv zip_Nil)
+ apply (metis map.simps(1) zip_Nil)
by auto
declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenA" ]]
-lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)"
-by (metis Collect_def image_subset_iff mem_def)
+lemma "(%x. Suc (f x)) ` {x. even x} <= A ==> \<forall>x. even x --> Suc (f x) \<in> A"
+by (metis Collect_def image_eqI mem_def subsetD)
declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenB" ]]
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A
==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
-by (metis Collect_def imageI image_image image_subset_iff mem_def)
+by (metis Collect_def imageI mem_def set_rev_mp)
declare [[ sledgehammer_problem_prefix = "Abstraction__image_curry" ]]
lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)"
-(*sledgehammer*)
+(* sledgehammer *)
by auto
declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesA" ]]
lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
-(*sledgehammer*)
-apply (rule equalityI)
-(***Even the two inclusions are far too difficult
-using [[ sledgehammer_problem_prefix = "Abstraction__image_TimesA_simpler"]]
-***)
-apply (rule subsetI)
-apply (erule imageE)
-(*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*)
-apply (erule ssubst)
-apply (erule SigmaE)
-(*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*)
-apply (erule ssubst)
-apply (subst split_conv)
-apply (rule SigmaI)
-apply (erule imageI) +
-txt{*subgoal 2*}
-apply (clarify )
-apply (simp add: )
-apply (rule rev_image_eqI)
-apply (blast intro: elim:)
-apply (simp add: )
-done
-
-(*Given the difficulty of the previous problem, these two are probably
-impossible*)
+by (metis map_pair_def map_pair_surj_on)
declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesB" ]]
lemma image_TimesB:
"(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"
-(*sledgehammer*)
+(* sledgehammer *)
by force
declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesC" ]]
lemma image_TimesC:
"(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)"
-(*sledgehammer*)
-by auto
+by (metis image_TimesA)
end