header {* Assessed Exercise II: Hereditarily Finite Sets*} (*<*)theory HF_ex imports "~~/src/HOL/Library/Nat_Bijection" begin text{*Thanks for Brian Huffman for this development, up to the cases and induct rules.*} typedef (open) hf = "UNIV :: nat set" .. definition hfset :: "hf \ hf set" where "hfset a = Abs_hf ` set_decode (Rep_hf a)" definition HF :: "hf set \ hf" where "HF A = Abs_hf (set_encode (Rep_hf ` A))" (*>*) text{*The \emph{hereditarily finite sets} are built up recursively, starting with the \emph{empty set}, using an operator which \emph{inserts} an element into a set. Note that sets and elements have the same type!*} definition hempty :: "hf" (*<*) where "hempty = HF {}"(*>*) definition hinsert :: "hf \ hf \ hf" (*<*) where "hinsert a b = HF (insert a (hfset b))" (*>*) text{*There is also a \emph{membership relation} on these strange sets.*} definition hmem :: "hf \ hf \ bool" (*<*) where "hmem a b \ a \ hfset b" text {* HF Set enumerations *} syntax "_HFinset" :: "args => hf" ("{|(_)|}") syntax (xsymbols) "_HFinset" :: "args => hf" ("\_\") translations "{|x, y|}" == "CONST hinsert x \y\" "{|x|}" == "CONST hinsert x (CONST hempty)" notation (xsymbols) hempty ("\\") notation (HTML) hempty ("\\") section {* Basic lemmas *} lemma finite_hfset [simp]: "finite (hfset a)" unfolding hfset_def by simp lemma HF_hfset [simp]: "HF (hfset a) = a" unfolding HF_def hfset_def by (simp add: image_image Abs_hf_inverse Rep_hf_inverse) lemma hfset_HF [simp]: "finite A \ hfset (HF A) = A" unfolding HF_def hfset_def by (simp add: image_image Abs_hf_inverse Rep_hf_inverse) (*>*) text{*The membership relation satisfies the following natural properties.*} lemma hmem_hempty(*<*) [simp](*>*): "\ hmem a hempty" (*<*) unfolding hmem_def hempty_def by simp(*>*) lemma hmem_hinsert(*<*) [simp](*>*): "hmem a (hinsert b c) \ a = b \ hmem a c" (*<*) unfolding hmem_def hinsert_def by simp (*>*) text{*Two sets are \emph{equal} if and only if they have the same elements.*} lemma hf_ext: "a = b \ (\x. hmem x a \ hmem x b)" (*<*) unfolding hmem_def set_eq_iff [symmetric] by (metis HF_hfset) lemma finite_cases [consumes 1, case_names empty insert]: "\finite F; F = {} \ P; \A x. \F = insert x A; x \ A; finite A\ \ P\ \ P" by (induct F rule: finite_induct, simp_all) lemma hf_cases [cases type: hf, case_names hempty hinsert]: obtains "y = hempty" | a b where "y = hinsert a b" and "\ hmem a b" proof - have "finite (hfset y)" by (rule finite_hfset) thus thesis proof (cases rule: finite_cases) case empty hence "y = hempty" by (simp add: hf_ext hmem_def hempty_def) thus thesis .. next case (insert A a) hence "y = hinsert a (HF A)" and "\ hmem a (HF A)" by (simp_all add: hf_ext hmem_def hinsert_def) thus thesis .. qed qed lemma Rep_hf_hinsert: "\ hmem a b \ Rep_hf (hinsert a b) = 2 ^ (Rep_hf a) + Rep_hf b" unfolding hinsert_def HF_def hfset_def apply (simp add: image_image Abs_hf_inverse Rep_hf_inverse) apply (subst set_encode_insert) apply simp apply (clarsimp simp add: hmem_def hfset_def image_def Rep_hf_inject [symmetric] Abs_hf_inverse) apply simp done lemma less_two_power: "n < 2 ^ n" by (induct n, auto) section{*Verifying the Axioms of HF*} (*>*) text{*Using that crucial property (which is called extensionality), one can easily prove that the primitive set operators can be characterised by their elements.*} lemma hempty_iff: "z = hempty \ (\x. \ hmem x z)" by (simp add: hf_ext) lemma hinsert_iff: "z = hinsert x y \ (\u. hmem u z \ hmem u y | u=x)" by (auto simp add: hf_ext) text{*Many properties of the hereditarily finite sets can be proved using the following \emph{induction rule}. (This rule also tells us that every such set is a finite construction.)*} lemma hf_induct [induct type: hf, case_names hempty hinsert]: assumes [simp]: "P hempty" "\x y. \P x; P y; \ hmem x y\ \ P (hinsert x y)" shows "P z" (*<*)proof (induct z rule: wf_induct [where r="measure Rep_hf", OF wf_measure]) case (1 x) show ?case proof (cases x rule: hf_cases) case hempty thus ?thesis by simp next case (hinsert a b) thus ?thesis using 1 by (simp add: Rep_hf_hinsert less_le_trans [OF less_two_power le_add1]) qed qed lemma hf_equalityI [intro]: "(\x. hmem x a \ hmem x b) \ a = b" by (simp add: hf_ext) (*>*) text {*You are likely to need this induction rule to prove the existence results below. \begin{task}Prove that insertion operations can be exchanged, as shown below.\end{task} *} lemma hinsert_commute: "hinsert x (hinsert y z) = hinsert y (hinsert x z)" (*<*)oops(*>*) text{*Ordered pairs can be defined as shown, where @{term"\a,b\"} abbreviates @{text"hinsert a (hinsert b hempty)"}.*} definition hpair :: "hf \ hf \ hf" where "hpair a b = \\a,a\,\a,b\\" text {*\begin{task}Prove that ordered pairing is injective. \end{task} *} lemma "hpair a b = hpair a' b' \ a=a' & b=b'" (*<*)oops (*>*) text {*\begin{task}Prove that it is always possible to delete a given element @{term"x"} from a given set @{term"z"}. (That is, there exists a set @{term"u"} standing for the result of this deletion.) \end{task} *} lemma delete1: "hmem x z ==> \u. hinsert x u = z & \ hmem x u" (*<*)oops(*>*) text {*\begin{task}Prove the existence of the union of two given sets @{term"x"} and @{term"y"}. \end{task} *} lemma binary_union: "\z. \u. hmem u z \ hmem u x | hmem u y" (*<*)oops(*>*) text {*\begin{task}Prove the existence of the union of given a set @{term"X"} of sets. \end{task} *} lemma union_of_set: "\z. \u. hmem u z \ (\y. hmem y X & hmem u y)" (*<*)oops(*>*) text {*\begin{task}Define the subset relation as shown, and prove the following theorem. (It is useful for proving the existence of power sets.) \end{task} *} definition hsubset :: "hf \ hf \ bool" where "hsubset a b \ (\x. hmem x a \ hmem x b)" lemma hsubset_insert2_iff: "hsubset z (hinsert x y) \ hsubset z y \ (\u. hinsert x u = z \ \ hmem x u \ hsubset u y)" (*<*)oops(*>*) (*<*)end (*>*)