wneuper/isa: src/HOL/ex/Set_Comprehension_Pointfree

     1 (*  Title:      HOL/ex/Set_Comprehension_Pointfree_Tests.thy

     2     Author:     Lukas Bulwahn, Rafal Kolanski

     3     Copyright   2012 TU Muenchen

     4 *)

     6 header {* Tests for the set comprehension to pointfree simproc *}

     8 theory Set_Comprehension_Pointfree_Tests

     9 imports Main

    10 begin

    12 lemma

    13   "finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}"

    14   by simp

    16 lemma

    17   "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B}"

    18   by simp

    20 lemma

    21   "finite B ==> finite A' ==> finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"

    22   by simp

    24 lemma

    25   "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"

    26   by simp

    28 lemma

    29   "finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"

    30   by simp

    32 lemma

    33   "finite A ==> finite B ==> finite C ==> finite D ==>

    34      finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"

    35   by simp

    37 lemma

    38   "finite A ==> finite B ==> finite C ==> finite D ==> finite E ==>

    39     finite {f a b c d e | a b c d e. a : A \<and> b : B \<and> c : C \<and> d : D \<and> e : E}"

    40   by simp

    42 lemma (* check arbitrary ordering *)

    43   "finite A ==> finite B ==> finite C ==> finite D ==> finite E \<Longrightarrow>

    44     finite {f a d c b e | e b c d a. b : B \<and> a : A \<and> e : E' \<and> c : C \<and> d : D \<and> e : E \<and> b : B'}"

    45   by simp

    47 lemma

    48   "\<lbrakk> finite A ; finite B ; finite C ; finite D \<rbrakk>

    49   \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"

    50   by simp

    52 lemma

    53   "finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D))

    54   \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"

    55   by simp

    57 lemma

    58   "finite S ==> finite {s'. EX s:S. s' = f a e s}"

    59   by simp

    61 lemma

    62   "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> a \<notin> Z}"

    63   by simp

    65 lemma

    66   "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> b : B \<and> (x,y) \<in> R}"

    67 by simp

    69 lemma

    70   "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> (x,y) \<in> R \<and> b : B}"

    71 by simp

    73 lemma

    74   "finite A ==> finite B ==> finite R ==> finite {f a (x, b) y| y b x a. a : A \<and> (x,y) \<in> R \<and> b : B}"

    75 by simp

    77 lemma

    78   "finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \<or> a : AA) \<and> b : B \<and> a \<notin> Z}"

    79 by simp

    81 lemma

    82   "finite A1 ==> finite A2 ==> finite A3 ==> finite A4 ==> finite A5 ==> finite B ==>

    83      finite {f a b c | a b c. ((a : A1 \<and> a : A2) \<or> (a : A3 \<and> (a : A4 \<or> a : A5))) \<and> b : B \<and> a \<notin> Z}"

    84 apply simp

    85 oops

    87 schematic_lemma (* check interaction with schematics *)

    88   "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}

    89    = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"

    90   by simp

    92 lemma

    93   assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"

    94 proof -

    95   have eq: "{(a,b,c,d). ([a, b], [c, d]) : S} = ((%(a, b, c, d). ([a, b], [c, d])) -` S)"

    96    unfolding vimage_def by (auto split: prod.split)  (* to be proved with the simproc *)

    97   from `finite S` show ?thesis

    98     unfolding eq by (auto intro!: finite_vimageI simp add: inj_on_def)

    99     (* to be automated with further rules and automation *)

   100 qed

   102 end

author	bulwahn
	Sun, 14 Oct 2012 19:16:33 +0200
changeset 50866	4d33963962fa
parent 50781	65318db3087b
child 50868	875ed58b3b65
permissions	-rw-r--r--