isabelle: src/HOL/Quotient_Examples/Lift_Set.thy@6f08aef43dc5 (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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	5	section \<open>Example of lifting definitions with the lifting infrastructure\<close>
45536 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
49834 b27bbb021df1 discontinued obsolete typedef (open) syntax; wenzelm parents: 47308 diff changeset	13	typedef '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
55584 a879f14b6f95 merged 'List.set' with BNF-generated 'set' blanchet parents: 49834 diff changeset	15	unfolding set_def by (rule UNIV_witness)
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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	19	text \<open>Now, we can employ lift_definition to lift definitions.\<close>
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	20
55584 a879f14b6f95 merged 'List.set' with BNF-generated 'set' blanchet parents: 49834 diff changeset	21	lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" .
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	22
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	23	term "Lift_Set.empty"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	24	thm Lift_Set.empty_def
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	25
55584 a879f14b6f95 merged 'List.set' with BNF-generated 'set' blanchet parents: 49834 diff changeset	26	lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" .
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	27
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	28	term "Lift_Set.insert"
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	29	thm Lift_Set.insert_def
5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	30
70009 435fb018e8ee "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports; wenzelm parents: 63167 diff changeset	31	export_code empty insert in SML file_prefix set
47097 987cb55cac44 fix example files kuncar parents: 47092 diff changeset	32
45536 5b0b1dc2e40f adding a preliminary example to show how the quotient_definition package can be generalized bulwahn parents: diff changeset	33	end

author	wenzelm
	Tue, 05 Mar 2024 20:58:41 +0100
changeset 79793	6f08aef43dc5
parent 70009	435fb018e8ee
permissions	-rw-r--r--