# Theory Abstraction

theory Abstraction
imports FuncSet
```(*  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 ‹Example Featuring Metis's Support for Lambda-Abstractions›

theory Abstraction
imports "HOL-Library.FuncSet"
begin

(* For Christoph Benzmüller *)
lemma "x < 1 ∧ ((=) = (=)) ⟹ ((=) = (=)) ∧ x < (2::nat)"

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"

lemma "(a, b) ∈ (SIGMA x:A. {y. x = f y}) ⟹ a ∈ A ∧ a = f b"

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"

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 ∈ pset cl → pset cl"
by (metis (no_types) Collect_mem_eq Sigma_triv)

lemma
"(cl, f) ∈ (SIGMA cl: CL. {f. f ∈ pset cl → pset cl}) ⟹
f ∈ pset cl → 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 ∈ pset cl ∩ 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 ∈ pset cl ∩ 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 ∈ pset cl → pset cl)  &  (monotone f (pset cl) (order cl))"
by auto

lemma
"(cl, f) ∈ CLF ⟹
CLF ⊆ (SIGMA cl: CL. {f. f ∈ pset cl ∩ cl}) ⟹
f ∈ pset cl ∩ cl"
by (metis (lifting) CollectD Sigma_triv subsetD)

lemma
"(cl, f) ∈ CLF ⟹
CLF = (SIGMA cl: CL. {f. f ∈ pset cl ∩ cl}) ⟹
f ∈ pset cl ∩ cl"
by (metis (lifting) CollectD Sigma_triv)

lemma
"(cl, f) ∈ CLF ⟹
CLF ⊆ (SIGMA cl': CL. {f. f ∈ pset cl' → pset cl'}) ⟹
f ∈ pset cl → pset cl"
by (metis (lifting) CollectD Sigma_triv subsetD)

lemma
"(cl, f) ∈ CLF ⟹
CLF = (SIGMA cl: CL. {f. f ∈ pset cl → pset cl}) ⟹
f ∈ pset cl → pset cl"
by (metis (lifting) CollectD Sigma_triv)

lemma
"(cl, f) ∈ CLF ⟹
CLF = (SIGMA cl: CL. {f. f ∈ pset cl → pset cl & monotone f (pset cl) (order cl)}) ⟹
(f ∈ pset cl → 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 (λw. w → w) xs) (map (λw. w × 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 ⟹
(∀x. even x --> f (f (Suc(f x))) ∈ A)"
by (metis mem_Collect_eq imageI set_rev_mp)

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) =
((λx. x → x) ` A) × ((λy. y × y) ` B)"
by (metis image_TimesA)

end
```