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