isabelle: src/HOL/Quotient_Examples/Lift_Set.thy@987cb55cac44 (annotated)

45576 6ea2bba2694a improving header bulwahn parents: 45536 diff changeset	1	(* Title: HOL/Quotient_Examples/Lift_Set.thy
45609 2c0c8ce96f4a misspelled name kuncar parents: 45576 diff changeset	2	Author: Lukas Bulwahn and Ondrej Kuncar
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	3	*)
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	4
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	5	header {* Example of lifting definitions with the quotient infrastructure *}
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	6
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	7	theory Lift_Set
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	8	imports Main
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	9	begin
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	10
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45694 diff changeset	11	definition set where "set = (UNIV :: ('a \<Rightarrow> bool) set)"
45694 4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	12
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45694 diff changeset	13	typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set"
45694 4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	14	morphisms member Set
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	15	unfolding set_def by auto
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	16
47097 987cb55cac44 fix example files kuncar parents: 47092 diff changeset	17	setup_lifting type_definition_set[unfolded set_def]
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	18
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	19	text {* Now, we can employ quotient_definition to lift definitions. *}
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	20
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	21	quotient_definition empty where "empty :: 'a set"
47092 fa3538d6004b fix Quotient_Examples kuncar parents: 45970 diff changeset	22	is "bot :: 'a \<Rightarrow> bool" done
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	23
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	24	term "Lift_Set.empty"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	25	thm Lift_Set.empty_def
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	26
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45694 diff changeset	27	definition insertp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45694 diff changeset	28	"insertp x P y \<longleftrightarrow> y = x \<or> P y"
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45694 diff changeset	29
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	30	quotient_definition insert where "insert :: 'a => 'a set => 'a set"
47092 fa3538d6004b fix Quotient_Examples kuncar parents: 45970 diff changeset	31	is insertp done
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	32
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	33	term "Lift_Set.insert"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	34	thm Lift_Set.insert_def
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	35
47097 987cb55cac44 fix example files kuncar parents: 47092 diff changeset	36	export_code empty insert in SML
987cb55cac44 fix example files kuncar parents: 47092 diff changeset	37
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	38	end
45970 b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set` haftmann parents: 45694 diff changeset	39

author	kuncar
	Fri, 23 Mar 2012 14:26:09 +0100
changeset 47097	987cb55cac44
parent 47092	fa3538d6004b
child 47308	9caab698dbe4
permissions	-rw-r--r--