section ‹Sets with at Most 2 Elements› (*<*) theory Bool_Bounded_Set imports "HOL-Cardinals.Cardinals" begin (*>*) typedef 'a bset = "{A :: 'a set. |A| ≤o ctwo}" morphisms set_bset Abs_bset by (rule exI[of _ "{}"]) (auto simp: card_of_empty4 ctwo_def) setup_lifting type_definition_bset lift_definition map_bset :: "('a ⇒ 'b) ⇒ 'a bset ⇒ 'b bset" is image using card_of_image ordLeq_transitive by blast inductive rel_bset :: "('a ⇒ 'b ⇒ bool) ⇒ 'a bset ⇒ 'b bset ⇒ bool" for R where "set_bset x ⊆ {(x, y). R x y} ⟹ rel_bset R (map_bset fst x) (map_bset snd x)" lift_definition bempty :: "'a bset" is "{}" by (auto simp: card_of_empty4 ctwo_def) lift_definition bsingleton :: "'a ⇒ 'a bset" is "λx. {x}" by (auto simp: ctwo_def) lift_definition bdoubleton :: "'a ⇒ 'a ⇒ 'a bset" is "λx y. {x, y}" by (auto simp: ctwo_def finite_card_of_iff_card2 card.insert_remove card_Diff_singleton_if) lemma map_bset_bempty[simp]: "map_bset f bempty = bempty" by transfer simp lemma map_bset_eq_bempty[simp]: "map_bset f x = bempty ⟷ x = bempty" "bempty = map_bset f x ⟷ x = bempty" by (transfer, simp)+ lemma map_bset_bsingleton[simp]: "map_bset f (bsingleton x) = bsingleton (f x)" by transfer simp lemma map_bset_bdoubleton[simp]: "map_bset f (bdoubleton x y) = bdoubleton (f x) (f y)" by transfer simp lemma bdoubleton_same[simp]: "bdoubleton x x = bsingleton x" by transfer simp lemma bempty_neq_bsingleton[simp]: "bempty ≠ bsingleton x" "bsingleton x ≠ bempty" by (transfer, simp)+ lemma bempty_neq_bdoubleton[simp]: "bempty ≠ bdoubleton x y" "bdoubleton x y ≠ bempty" by (transfer, simp)+ lemma bsinleton_eq_bdoubleton[simp]: "bsingleton x = bdoubleton y z ⟷ (x = y ∧ y = z)" "bdoubleton y z = bsingleton x ⟷ (x = y ∧ y = z)" by (transfer, auto)+ lemma bsinleton_inj[simp]: "bsingleton x = bsingleton y ⟷ (x = y)" by (transfer, simp) lemma bdoubleton_eq_iff[simp]: "bdoubleton x y = bdoubleton z w ⟷ (x = z ∧ y = w ∨ x = w ∧ y = z)" by transfer (simp add: doubleton_eq_iff) lemmas [simp] = bempty.rep_eq bsingleton.rep_eq bdoubleton.rep_eq lemma bset_cases: "⟦X = bempty ⟹ P; ⋀x. X = bsingleton x ⟹ P; ⋀x y. ⟦x ≠ y; X = bdoubleton x y⟧ ⟹ P⟧ ⟹ P" proof (transfer fixing: P) fix Z :: "'a set" assume "|Z| ≤o ctwo" moreover then have "finite Z" by (metis card_of_ordLeq_infinite ctwo_def finite_code) ultimately have "card Z ≤ 2" unfolding ctwo_def by (subst (asm) finite_card_of_iff_card2) auto moreover assume "Z = {} ⟹ P" "⋀x. Z = {x} ⟹ P" "⋀x y. ⟦x ≠ y; Z = {x, y}⟧ ⟹ P" ultimately show P using ‹finite Z› proof (induct "card Z") case (Suc m) from Suc(2)[symmetric] Suc(2-7) show P by (cases m) (auto simp: card_Suc_eq) qed simp qed bnf "'k bset" map: map_bset sets: set_bset bd: natLeq rel: rel_bset proof (standard, goal_cases) case 1 then show ?case by transfer simp next case 2 then show ?case apply (rule ext) apply transfer apply auto done next case 3 then show ?case apply transfer apply (auto simp: image_iff) done next case 4 then show ?case apply (rule ext) apply transfer apply simp done next case 5 then show ?case by (simp add: card_order_csum natLeq_card_order) next case 6 then show ?case by (simp add: cinfinite_csum natLeq_cinfinite) next case 7 then show ?case by (simp add: regularCard_natLeq) next case 8 then show ?case apply transfer apply (erule ordLeq_ordLess_trans[OF _ ctwo_ordLess_natLeq]) done next case (9 R S) then show ?case proof (safe elim!: rel_bset.cases, unfold rel_bset.simps) fix z1 z2 assume "set_bset z1 ⊆ {(x, y). R x y}" "set_bset z2 ⊆ {(x, y). S x y}" "map_bset snd z1 = map_bset fst z2" then show "∃x. map_bset fst z1 = map_bset fst x ∧ map_bset snd z2 = map_bset snd x ∧ set_bset x ⊆ {(x, y). (R OO S) x y}" by (cases z1 z2 rule: bset_cases[case_product bset_cases]) (fastforce intro: exI[of _ "bsingleton (a, b)" for a b] dest: spec[of _ "bdoubleton (a, b) (c, d)" for a b c d])+ qed next case (10 R) then show ?case by (auto simp: fun_eq_iff intro: rel_bset.intros elim: rel_bset.cases) qed (*<*) end (*>*)