Theory Bool_Bounded_Set

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
(*>*)