Quellcode-Bibliothek 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 \<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

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.12Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.