isabelle: src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy@22994525d0d4 (annotated)

48049 d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	1	(* Title: HOL/ex/Set_Comprehension_Pointfree_Tests.thy
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	2	Author: Lukas Bulwahn
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	3	Copyright 2012 TU Muenchen
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	4	*)
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	5
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	6	header {* Tests for the set comprehension to pointfree simproc *}
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	7
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	8	theory Set_Comprehension_Pointfree_Tests
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	9	imports Main
48055 9819d49d2f39 tuned header; wenzelm parents: 48049 diff changeset	10	uses "set_comprehension_pointfree.ML"
48049 d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	11	begin
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	12
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	13	simproc_setup finite_Collect ("finite (Collect P)") = {* Set_Comprehension_Pointfree.simproc *}
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	14
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	15	lemma
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	16	"finite {f a b\| a b. a : A \<and> b : B}"
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	17	apply simp (* works :) *)
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	18	oops
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	19
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	20	lemma
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	21	"finite {f a b\| a b. a : A \<and> a : A' \<and> b : B}"
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	22	(* apply simp -- does not terminate *)
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	23	oops
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	24
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	25	lemma
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	26	"finite {f a b\| a b. a : A \<and> b : B \<and> b : B'}"
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	27	(* apply simp -- does not terminate *)
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	28	oops
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	29
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	30	lemma
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	31	"finite {f a b c\| a b c. a : A \<and> b : B \<and> c : C}"
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	32	(* apply simp -- failed *)
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	33	oops
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	34
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	35	lemma
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	36	"finite {f a b c d\| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	37	(* apply simp -- failed *)
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	38	oops
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	39
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	40	lemma
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	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}"
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	42	(* apply simp -- failed *)
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	43	oops
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	44
d862b0d56c49 adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets bulwahn parents: diff changeset	45	end

author	haftmann
	Sun, 17 Jun 2012 20:38:12 +0200
changeset 48106	22994525d0d4
parent 48055	9819d49d2f39
child 48108	f93433b451b8
permissions	-rw-r--r--