wneuper/isa: src/HOL/ex/Set_Comprehension_Pointfree

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

     2     Author:     Lukas Bulwahn

     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 uses "set_comprehension_pointfree.ML"

    11 begin

    13 simproc_setup finite_Collect ("finite (Collect P)") = {* Set_Comprehension_Pointfree.simproc *}

    15 lemma

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

    17 apply simp (* works :) *)

    18 oops

    20 lemma

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

    22 (* apply simp -- does not terminate *)

    23 oops

    25 lemma

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

    27 (* apply simp -- does not terminate *)

    28 oops

    30 lemma

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

    32 (* apply simp -- failed *)

    33 oops

    35 lemma

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

    37 (* apply simp -- failed *)

    38 oops

    40 lemma

    41   "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}"

    42 (* apply simp -- failed *)

    43 oops

    45 end

author	wenzelm
	Fri, 01 Jun 2012 12:45:22 +0200
changeset 49070	9819d49d2f39
parent 49064	d862b0d56c49
child 49123	f93433b451b8
permissions	-rw-r--r--