1.1 --- a/src/HOL/Metis_Examples/Abstraction.thy Fri Nov 18 11:47:12 2011 +0100
1.2 +++ b/src/HOL/Metis_Examples/Abstraction.thy Fri Nov 18 11:47:12 2011 +0100
1.3 @@ -8,16 +8,14 @@
1.4 header {* Example Featuring Metis's Support for Lambda-Abstractions *}
1.5
1.6 theory Abstraction
1.7 -imports Main "~~/src/HOL/Library/FuncSet"
1.8 +imports "~~/src/HOL/Library/FuncSet"
1.9 begin
1.10
1.11 -declare [[metis_new_skolemizer]]
1.12 -
1.13 (* For Christoph Benzmüller *)
1.14 lemma "x < 1 \<and> ((op =) = (op =)) \<Longrightarrow> ((op =) = (op =)) \<and> x < (2::nat)"
1.15 by (metis nat_1_add_1 trans_less_add2)
1.16
1.17 -lemma "(op = ) = (%x y. y = x)"
1.18 +lemma "(op = ) = (\<lambda>x y. y = x)"
1.19 by metis
1.20
1.21 consts
1.22 @@ -25,20 +23,20 @@
1.23 pset :: "'a set => 'a set"
1.24 order :: "'a set => ('a * 'a) set"
1.25
1.26 -lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
1.27 +lemma "a \<in> {x. P x} \<Longrightarrow> P a"
1.28 proof -
1.29 assume "a \<in> {x. P x}"
1.30 hence "a \<in> P" by (metis Collect_def)
1.31 thus "P a" by (metis mem_def)
1.32 qed
1.33
1.34 -lemma Collect_triv: "a \<in> {x. P x} ==> P a"
1.35 +lemma Collect_triv: "a \<in> {x. P x} \<Longrightarrow> P a"
1.36 by (metis mem_Collect_eq)
1.37
1.38 -lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
1.39 +lemma "a \<in> {x. P x --> Q x} \<Longrightarrow> a \<in> {x. P x} \<Longrightarrow> a \<in> {x. Q x}"
1.40 by (metis Collect_imp_eq ComplD UnE)
1.41
1.42 -lemma "(a, b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
1.43 +lemma "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
1.44 proof -
1.45 assume A1: "(a, b) \<in> Sigma A B"
1.46 hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
1.47 @@ -47,17 +45,11 @@
1.48 thus "a \<in> A \<and> b \<in> B a" by (metis F2)
1.49 qed
1.50
1.51 -lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
1.52 +lemma Sigma_triv: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
1.53 by (metis SigmaD1 SigmaD2)
1.54
1.55 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
1.56 -(* Metis says this is satisfiable!
1.57 -by (metis CollectD SigmaD1 SigmaD2)
1.58 -*)
1.59 -by (meson CollectD SigmaD1 SigmaD2)
1.60 -
1.61 -lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
1.62 -by (metis mem_Sigma_iff singleton_conv2 vimage_Collect_eq vimage_singleton_eq)
1.63 +by (metis (full_types, lam_lifting) CollectD SigmaD1 SigmaD2)
1.64
1.65 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
1.66 proof -
1.67 @@ -69,44 +61,42 @@
1.68 thus "a \<in> A \<and> a = f b" by (metis F1)
1.69 qed
1.70
1.71 -lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
1.72 +lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
1.73 by (metis Collect_mem_eq SigmaD2)
1.74
1.75 -lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
1.76 +lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
1.77 proof -
1.78 assume A1: "(cl, f) \<in> CLF"
1.79 assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
1.80 have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
1.81 have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
1.82 hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis F1 Collect_def)
1.83 - hence "f \<in> pset cl" by (metis A1)
1.84 - thus "f \<in> pset cl" by metis
1.85 + thus "f \<in> pset cl" by (metis A1)
1.86 qed
1.87
1.88 lemma
1.89 - "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
1.90 - f \<in> pset cl \<rightarrow> pset cl"
1.91 + "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
1.92 + f \<in> pset cl \<rightarrow> pset cl"
1.93 by (metis (no_types) Collect_def Sigma_triv mem_def)
1.94
1.95 lemma
1.96 - "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
1.97 - f \<in> pset cl \<rightarrow> pset cl"
1.98 + "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
1.99 + f \<in> pset cl \<rightarrow> pset cl"
1.100 proof -
1.101 assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
1.102 have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
1.103 have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
1.104 - hence "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
1.105 - thus "f \<in> pset cl \<rightarrow> pset cl" by metis
1.106 + thus "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
1.107 qed
1.108
1.109 lemma
1.110 - "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
1.111 - f \<in> pset cl \<inter> cl"
1.112 + "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
1.113 + f \<in> pset cl \<inter> cl"
1.114 by (metis (no_types) Collect_conj_eq Int_def Sigma_triv inf_idem)
1.115
1.116 lemma
1.117 - "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
1.118 - f \<in> pset cl \<inter> cl"
1.119 + "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
1.120 + f \<in> pset cl \<inter> cl"
1.121 proof -
1.122 assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
1.123 have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
1.124 @@ -118,71 +108,73 @@
1.125 qed
1.126
1.127 lemma
1.128 - "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
1.129 + "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
1.130 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
1.131 by auto
1.132
1.133 -lemma "(cl,f) \<in> CLF ==>
1.134 - CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
1.135 +lemma
1.136 + "(cl, f) \<in> CLF \<Longrightarrow>
1.137 + CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
1.138 f \<in> pset cl \<inter> cl"
1.139 +by (metis (lam_lifting) Collect_def Sigma_triv mem_def subsetD)
1.140 +
1.141 +lemma
1.142 + "(cl, f) \<in> CLF \<Longrightarrow>
1.143 + CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
1.144 + f \<in> pset cl \<inter> cl"
1.145 +by (metis (lam_lifting) Int_Collect SigmaD2 inf1I mem_def)
1.146 +
1.147 +lemma
1.148 + "(cl, f) \<in> CLF \<Longrightarrow>
1.149 + CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) \<Longrightarrow>
1.150 + f \<in> pset cl \<rightarrow> pset cl"
1.151 +by (metis (lam_lifting) Collect_def Sigma_triv mem_def subsetD)
1.152 +
1.153 +lemma
1.154 + "(cl, f) \<in> CLF \<Longrightarrow>
1.155 + CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
1.156 + f \<in> pset cl \<rightarrow> pset cl"
1.157 +by (metis (lam_lifting) Collect_def Sigma_triv mem_def)
1.158 +
1.159 +lemma
1.160 + "(cl, f) \<in> CLF \<Longrightarrow>
1.161 + CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
1.162 + (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
1.163 by auto
1.164
1.165 -lemma "(cl,f) \<in> CLF ==>
1.166 - CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
1.167 - f \<in> pset cl \<inter> cl"
1.168 -by auto
1.169 -
1.170 -lemma
1.171 - "(cl,f) \<in> CLF ==>
1.172 - CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==>
1.173 - f \<in> pset cl \<rightarrow> pset cl"
1.174 -by fast
1.175 -
1.176 -lemma
1.177 - "(cl,f) \<in> CLF ==>
1.178 - CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
1.179 - f \<in> pset cl \<rightarrow> pset cl"
1.180 -by auto
1.181 -
1.182 -lemma
1.183 - "(cl,f) \<in> CLF ==>
1.184 - CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
1.185 - (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
1.186 -by auto
1.187 -
1.188 -lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
1.189 -apply (induct xs)
1.190 - apply (metis map.simps(1) zip_Nil)
1.191 -by (metis (lam_lifting, no_types) map.simps(2) zip_Cons_Cons)
1.192 -
1.193 -lemma "map (%w. (w -> w, w \<times> w)) xs =
1.194 - zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
1.195 +lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)"
1.196 apply (induct xs)
1.197 apply (metis map.simps(1) zip_Nil)
1.198 by auto
1.199
1.200 -lemma "(%x. Suc (f x)) ` {x. even x} <= A ==> \<forall>x. even x --> Suc (f x) \<in> A"
1.201 +lemma
1.202 + "map (\<lambda>w. (w -> w, w \<times> w)) xs =
1.203 + zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)"
1.204 +apply (induct xs)
1.205 + apply (metis map.simps(1) zip_Nil)
1.206 +by auto
1.207 +
1.208 +lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A"
1.209 by (metis Collect_def image_eqI mem_def subsetD)
1.210
1.211 -lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A
1.212 - ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
1.213 +lemma
1.214 + "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow>
1.215 + (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
1.216 by (metis Collect_def imageI mem_def set_rev_mp)
1.217
1.218 -lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)"
1.219 -(* sledgehammer *)
1.220 -by auto
1.221 +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)"
1.222 +by (metis (lam_lifting) imageE)
1.223
1.224 -lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
1.225 +lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
1.226 by (metis map_pair_def map_pair_surj_on)
1.227
1.228 lemma image_TimesB:
1.229 - "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"
1.230 -(* sledgehammer *)
1.231 + "(\<lambda>(x, y, z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f ` A) \<times> (g ` B) \<times> (h ` C)"
1.232 by force
1.233
1.234 lemma image_TimesC:
1.235 - "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
1.236 - ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)"
1.237 + "(\<lambda>(x, y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
1.238 + ((\<lambda>x. x \<rightarrow> x) ` A) \<times> ((\<lambda>y. y \<times> y) ` B)"
1.239 by (metis image_TimesA)
1.240
1.241 end