isabelle: src/CCL/Set.thy@22ef720a92b0 (annotated)

60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 58977 diff changeset	1	section \<open>Extending FOL by a modified version of HOL set theory\<close>
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3935 diff changeset	2
bcf7544875b2 converted to Isar theory format; wenzelm parents: 3935 diff changeset	3	theory Set
48475 02dd825f5a4e more session ROOT files; wenzelm parents: 42156 diff changeset	4	imports "~~/src/FOL/FOL"
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3935 diff changeset	5	begin
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	6
39128 93a7365fb4ee turned eta_contract into proper configuration option; wenzelm parents: 38499 diff changeset	7	declare [[eta_contract]]
93a7365fb4ee turned eta_contract into proper configuration option; wenzelm parents: 38499 diff changeset	8
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 3935 diff changeset	9	typedecl 'a set
55380 4de48353034e prefer vacuous definitional type classes over axiomatic ones; wenzelm parents: 48475 diff changeset	10	instance set :: ("term") "term" ..
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	11
62143 3c9a0985e6be eliminated old defs; wenzelm parents: 62020 diff changeset	12
3c9a0985e6be eliminated old defs; wenzelm parents: 62020 diff changeset	13	subsection \<open>Set comprehension and membership\<close>
3c9a0985e6be eliminated old defs; wenzelm parents: 62020 diff changeset	14
3c9a0985e6be eliminated old defs; wenzelm parents: 62020 diff changeset	15	axiomatization Collect :: "['a \<Rightarrow> o] \<Rightarrow> 'a set"
3c9a0985e6be eliminated old defs; wenzelm parents: 62020 diff changeset	16	and mem :: "['a, 'a set] \<Rightarrow> o" (infixl ":" 50)
3c9a0985e6be eliminated old defs; wenzelm parents: 62020 diff changeset	17	where mem_Collect_iff: "(a : Collect(P)) \<longleftrightarrow> P(a)"
3c9a0985e6be eliminated old defs; wenzelm parents: 62020 diff changeset	18	and set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	19
3935 52c14fe8f16b adapted to qualified names; wenzelm parents: 3837 diff changeset	20	syntax
62143 3c9a0985e6be eliminated old defs; wenzelm parents: 62020 diff changeset	21	"_Coll" :: "[idt, o] \<Rightarrow> 'a set" ("(1{_./ _})")
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	22	translations
62143 3c9a0985e6be eliminated old defs; wenzelm parents: 62020 diff changeset	23	"{x. P}" == "CONST Collect(\<lambda>x. P)"
20140 98acc6d0fab6 removed obsolete ML files; wenzelm parents: 17456 diff changeset	24
58977 9576b510f6a2 more symbols; wenzelm parents: 58889 diff changeset	25	lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}"
20140 98acc6d0fab6 removed obsolete ML files; wenzelm parents: 17456 diff changeset	26	apply (rule mem_Collect_iff [THEN iffD2])
98acc6d0fab6 removed obsolete ML files; wenzelm parents: 17456 diff changeset	27	apply assumption
98acc6d0fab6 removed obsolete ML files; wenzelm parents: 17456 diff changeset	28	done
98acc6d0fab6 removed obsolete ML files; wenzelm parents: 17456 diff changeset	29
58977 9576b510f6a2 more symbols; wenzelm parents: 58889 diff changeset	30	lemma CollectD: "a : {x. P(x)} \<Longrightarrow> P(a)"
20140 98acc6d0fab6 removed obsolete ML files; wenzelm parents: 17456 diff changeset	31	apply (erule mem_Collect_iff [THEN iffD1])
98acc6d0fab6 removed obsolete ML files; wenzelm parents: 17456 diff changeset	32	done
98acc6d0fab6 removed obsolete ML files; wenzelm parents: 17456 diff changeset	33
98acc6d0fab6 removed obsolete ML files; wenzelm parents: 17456 diff changeset	34	lemmas CollectE = CollectD [elim_format]
98acc6d0fab6 removed obsolete ML files; wenzelm parents: 17456 diff changeset	35
58977 9576b510f6a2 more symbols; wenzelm parents: 58889 diff changeset	36	lemma set_ext: "(\<And>x. x:A \<longleftrightarrow> x:B) \<Longrightarrow> A = B"
20140

author	haftmann
	Mon, 05 Jun 2017 21:24:40 +0200
changeset 66023	22ef720a92b0
parent 62143	3c9a0985e6be
child 66453	cc19f7ca2ed6
permissions	-rw-r--r--