Quelle  Abstraction.thy   Sprache: Isabelle

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

end