|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Abstraction.thy
Sprache: Unknown
(* Title: HOL/Metis_Examples/Abstraction.thy
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
Example featuring Metis's support for lambda-abstractions.
*)
section \<open>Example Featuring Metis's Support for Lambda-Abstractions\<close>
theory Abstraction
imports "HOL-Library.FuncSet"
begin
(* For Christoph Benzmüller *)
lemma "x < 1 \ ((=) = (=)) \ ((=) = (=)) \ x < (2::nat)"
by (metis nat_1_add_1 trans_less_add2)
lemma "((=) ) = (\x y. y = x)"
by metis
consts
monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
pset :: "'a set => 'a set"
order :: "'a set => ('a * 'a) set"
lemma "a \ {x. P x} \ P a"
proof -
assume "a \ {x. P x}"
thus "P a" by (metis mem_Collect_eq)
qed
lemma Collect_triv: "a \ {x. P x} \ P a"
by (metis mem_Collect_eq)
lemma "a \ {x. P x --> Q x} \ a \ {x. P x} \ a \ {x. Q x}"
by (metis Collect_imp_eq ComplD UnE)
lemma "(a, b) \ Sigma A B \ a \ A \ b \ B a"
proof -
assume A1: "(a, b) \ Sigma A B"
hence F1: "b \ B a" by (metis mem_Sigma_iff)
have F2: "a \ A" by (metis A1 mem_Sigma_iff)
have "b \ B a" by (metis F1)
thus "a \ A \ b \ B a" by (metis F2)
qed
lemma Sigma_triv: "(a, b) \ Sigma A B \ a \ A & b \ B a"
by (metis SigmaD1 SigmaD2)
lemma "(a, b) \ (SIGMA x:A. {y. x = f y}) \ a \ A \ a = f b"
by (metis (full_types, lifting) CollectD SigmaD1 SigmaD2)
lemma "(a, b) \ (SIGMA x:A. {y. x = f y}) \ a \ A \ a = f b"
proof -
assume A1: "(a, b) \ (SIGMA x:A. {y. x = f y})"
hence F1: "a \ A" by (metis mem_Sigma_iff)
have "b \ {R. a = f R}" by (metis A1 mem_Sigma_iff)
hence "a = f b" by (metis (full_types) mem_Collect_eq)
thus "a \ A \ a = f b" by (metis F1)
qed
lemma "(cl, f) \ CLF \ CLF = (SIGMA cl: CL.{f. f \ pset cl}) \ f \ pset cl"
by (metis Collect_mem_eq SigmaD2)
lemma "(cl, f) \ CLF \ CLF = (SIGMA cl: CL.{f. f \ pset cl}) \ f \ pset cl"
proof -
assume A1: "(cl, f) \ CLF"
assume A2: "CLF = (SIGMA cl:CL. {f. f \ pset cl})"
have "\v u. (u, v) \ CLF \ v \ {R. R \ pset u}" by (metis A2 mem_Sigma_iff)
hence "\v u. (u, v) \ CLF \ v \ pset u" by (metis mem_Collect_eq)
thus "f \ pset cl" by (metis A1)
qed
lemma
"(cl, f) \ (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) \
f \<in> pset cl \<rightarrow> pset cl"
by (metis (no_types) Collect_mem_eq Sigma_triv)
lemma
"(cl, f) \ (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) \
f \<in> pset cl \<rightarrow> pset cl"
proof -
assume A1: "(cl, f) \ (SIGMA cl:CL. {f. f \ pset cl \ pset cl})"
have "f \ {R. R \ pset cl \ pset cl}" using A1 by simp
thus "f \ pset cl \ pset cl" by (metis mem_Collect_eq)
qed
lemma
"(cl, f) \ (SIGMA cl: CL. {f. f \ pset cl \ cl}) \
f \<in> pset cl \<inter> cl"
by (metis (no_types) Collect_conj_eq Int_def Sigma_triv inf_idem)
lemma
"(cl, f) \ (SIGMA cl: CL. {f. f \ pset cl \ cl}) \
f \<in> pset cl \<inter> cl"
proof -
assume A1: "(cl, f) \ (SIGMA cl:CL. {f. f \ pset cl \ cl})"
have "f \ {R. R \ pset cl \ cl}" using A1 by simp
hence "f \ Id_on cl `` pset cl" by (metis Int_commute Image_Id_on mem_Collect_eq)
hence "f \ cl \ pset cl" by (metis Image_Id_on)
thus "f \ pset cl \ cl" by (metis Int_commute)
qed
lemma
"(cl, f) \ (SIGMA cl: CL. {f. f \ pset cl \ pset cl & monotone f (pset cl) (order cl)}) \
(f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
by auto
lemma
"(cl, f) \ CLF \
CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
f \<in> pset cl \<inter> cl"
by (metis (lifting) CollectD Sigma_triv subsetD)
lemma
"(cl, f) \ CLF \
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
f \<in> pset cl \<inter> cl"
by (metis (lifting) CollectD Sigma_triv)
lemma
"(cl, f) \ CLF \
CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) \<Longrightarrow>
f \<in> pset cl \<rightarrow> pset cl"
by (metis (lifting) CollectD Sigma_triv subsetD)
lemma
"(cl, f) \ CLF \
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
f \<in> pset cl \<rightarrow> pset cl"
by (metis (lifting) CollectD Sigma_triv)
lemma
"(cl, f) \ CLF \
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
(f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
by auto
lemma "map (\x. (f x, g x)) xs = zip (map f xs) (map g xs)"
apply (induct xs)
apply (metis list.map(1) zip_Nil)
by auto
lemma
"map (\w. (w \ w, w \ w)) xs =
zip (map (\<lambda>w. w \<rightarrow> w) xs) (map (\<lambda>w. w \<times> w) xs)"
apply (induct xs)
apply (metis list.map(1) zip_Nil)
by auto
lemma "(\x. Suc (f x)) ` {x. even x} \ A \ \x. even x --> Suc (f x) \ A"
by (metis mem_Collect_eq image_eqI subsetD)
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 mem_Collect_eq imageI rev_subsetD)
lemma "f \ (\u v. b \ u \ v) ` A \ \u v. P (b \ u \ v) \ P(f y)"
by (metis (lifting) imageE)
lemma image_TimesA: "(\(x, y). (f x, g y)) ` (A \ B) = (f ` A) \ (g ` B)"
by (metis map_prod_def map_prod_surj_on)
lemma image_TimesB:
"(\(x, y, z). (f x, g y, h z)) ` (A \ B \ C) = (f ` A) \ (g ` B) \ (h ` C)"
by force
lemma image_TimesC:
"(\(x, y). (x \ x, y \ y)) ` (A \ B) =
((\<lambda>x. x \<rightarrow> x) ` A) \<times> ((\<lambda>y. y \<times> y) ` B)"
by (metis image_TimesA)
end
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
|
|
|
|
|
