isabelle: src/HOL/Quotient_Examples/Lift_Set.thy@4a8743618257 (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
45694 4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	11	definition set where "set = (UNIV :: ('a => bool) => bool)"
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	12
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	13	typedef (open) 'a set = "set :: 'a set set"
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
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	17	text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
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	local_setup {* fn lthy =>
45694 4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	20	let
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	21	val quotients =
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	22	{qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	23	equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	24	val qty_full_name = @{type_name "set"}
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	25
45694 4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	26	fun qinfo phi = Quotient_Info.transform_quotients phi quotients
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	27	in
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	28	lthy
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	29	\|> Local_Theory.declaration {syntax = false, pervasive = true}
45694 4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	30	(fn phi =>
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	31	Quotient_Info.update_quotients qty_full_name (qinfo phi) #>
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	32	Quotient_Info.update_abs_rep qty_full_name
4a8743618257 prefer typedef without extra definition and alternative name; wenzelm parents: 45609 diff changeset	33	(Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	34	end
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	35	*}
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	36
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	37	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	38
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	39	quotient_definition empty where "empty :: 'a set"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	40	is "Set.empty"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	41
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	42	term "Lift_Set.empty"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	43	thm Lift_Set.empty_def
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	44
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	45	quotient_definition insert where "insert :: 'a => 'a set => 'a set"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	46	is "Set.insert"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	47
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	48	term "Lift_Set.insert"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	49	thm Lift_Set.insert_def
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	50
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	51	end

author	wenzelm
	Wed, 30 Nov 2011 16:27:10 +0100
changeset 45694	4a8743618257
parent 45609	2c0c8ce96f4a
child 45970	b6d0cff57d96
permissions	-rw-r--r--