Quelle Set_Comprehension_Pointfree_Examples.thy Sprache: Isabelle

(*  Title:      HOL/ex/Set_Comprehension_Pointfree_Examples.thy
    Author:     Lukas Bulwahn, Rafal Kolanski
    Copyright   2012 TU Muenchen
*)

section \<open>Examples for the set comprehension to pointfree simproc\<close>

theory Set_Comprehension_Pointfree_Examples
imports Main
begin

declare [[simproc add: finite_Collect]]

lemma
  "finite (UNIV::'a set) \ finite {p. \x::'a. p = (x, x)}"
  by simp

lemma
  "finite A \ finite B \ finite {f a b| a b. a \ A \ b \ B}"
  by simp

lemma
  "finite B \ finite A' \ finite {f a b| a b. a \ A \ a \ A' \ b \ B}"
  by simp

lemma
  "finite A \ finite B \ finite {f a b| a b. a \ A \ b \ B \ b \ B'}"
  by simp

lemma
  "finite A \ finite B \ finite C \ finite {f a b c| a b c. a \ A \ b \ B \ c \ C}"
  by simp

lemma
  "finite A \ finite B \ finite C \ finite D \
     finite {f a b c d| a b c d. a \<in> A \<and> b \<in> B \<and> c \<in> C \<and> d \<in> D}"
  by simp

lemma
  "finite A \ finite B \ finite C \ finite D \ finite E \
    finite {f a b c d e | a b c d e. a \<in> A \<and> b \<in> B \<and> c \<in> C \<and> d \<in> D \<and> e \<in> E}"
  by simp

lemma
  "finite A \ finite B \ finite C \ finite D \ finite E \
    finite {f a d c b e | e b c d a. b \<in> B \<and> a \<in> A \<and> e \<in> E' \<and> c \<in> C \<and> d \<in> D \<and> e \<in> E \<and> b \<in> B'}"
  by simp

lemma
  "\ finite A ; finite B ; finite C ; finite D \
  \<Longrightarrow> finite ({f a b c d| a b c d. a \<in> A \<and> b \<in> B \<and> c \<in> C \<and> d \<in> D})"
  by simp

lemma
  "finite ((\(a,b,c,d). f a b c d) ` (A \ B \ C \ D))
  \<Longrightarrow> finite ({f a b c d| a b c d. a \<in> A \<and> b \<in> B \<and> c \<in> C \<and> d \<in> D})"
  by simp

lemma
  "finite S \ finite {s'. \s\S. s' = f a e s}"
  by simp

lemma
  "finite A \ finite B \ finite {f a b| a b. a \ A \ b \ B \ a \ Z}"
  by simp

lemma
  "finite A \ finite B \ finite R \ finite {f a b x y| a b x y. a \ A \ b \ B \ (x,y) \ R}"
by simp

lemma
  "finite A \ finite B \ finite R \ finite {f a b x y| a b x y. a \ A \ (x,y) \ R \ b \ B}"
by simp

lemma
  "finite A \ finite B \ finite R \ finite {f a (x, b) y| y b x a. a \ A \ (x,y) \ R \ b \ B}"
by simp

lemma
  "finite A \ finite AA \ finite B \ finite {f a b| a b. (a \ A \ a \ AA) \ b \ B \ a \ Z}"
by simp

lemma
  "finite A1 \ finite A2 \ finite A3 \ finite A4 \ finite A5 \ finite B \
     finite {f a b c | a b c. ((a \<in> A1 \<and> a \<in> A2) \<or> (a \<in> A3 \<and> (a \<in> A4 \<or> a \<in> A5))) \<and> b \<in> B \<and> a \<notin> Z}"
apply simp
oops

lemma "finite B \ finite {c. \x. x \ B \ c = a * x}"
by simp

lemma
  "finite A \ finite B \ finite {f a * g b |a b. a \ A \ b \ B}"
by simp

lemma
  "finite S \ inj (\(x, y). g x y) \ finite {f x y| x y. g x y \ S}"
  by (auto intro: finite_vimageI)

lemma
  "finite A \ finite S \ inj (\(x, y). g x y) \ finite {f x y z | x y z. g x y \ S & z \ A}"
  by (auto intro: finite_vimageI)

lemma
  "finite S \ finite A \ inj (\(x, y). g x y) \ inj (\(x, y). h x y)
    \<Longrightarrow> finite {f a b c d | a b c d. g a c \<in> S \<and> h b d \<in> A}"
  by (auto intro: finite_vimageI)

lemma
  assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) \ S}"
using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
  (* injectivity to be automated with further rules and automation *)

schematic_goal (* check interaction with schematics *)
  "finite {x :: ?'A \ ?'B \ bool. \a b. x = Pair_Rep a b}
   = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
  by simp

declare [[simproc del: finite_Collect]]

section \<open>Testing simproc in code generation\<close>

definition union :: "nat set => nat set => nat set"
where
  "union A B = {x. x \ A \ x \ B}"

definition common_subsets :: "nat set \ nat set \ nat set set"
where
  "common_subsets S1 S2 = {S. S \ S1 \ S \ S2}"

definition products :: "nat set => nat set => nat set"
where
  "products A B = {c. \a b. a \ A \ b \ B \ c = a * b}"

export_code union common_subsets products checking SML

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

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.