Theory HOL-Library.Code_Cardinality

section ‹Code setup for sets with cardinality type information›

theory Code_Cardinality imports Cardinality begin

text ‹
  Implement termCARD('a) via termcard_UNIV and provide
  implementations for termfinite, termcard, term(⊆), 
  and term(=)if the calling context already provides classfinite_UNIV
  and classcard_UNIV instances. If we implemented the latter
  always via termcard_UNIV, we would require instances of essentially all 
  element types, i.e., a lot of instantiation proofs and -- at run time --
  possibly slow dictionary constructions.
›

context
begin

qualified definition card_UNIV' :: "'a card_UNIV"
where [code del]: "card_UNIV' = Phantom('a) CARD('a)"

lemma CARD_code [code_unfold]:
  "CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)"
by(simp add: card_UNIV'_def)

lemma card_UNIV'_code [code]:
  "card_UNIV' = card_UNIV"
by(simp add: card_UNIV card_UNIV'_def)

end

lemma card_Compl:
  "finite A  card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)

context fixes xs :: "'a :: finite_UNIV list"
begin

qualified definition finite' :: "'a set  bool"
where [simp, code del, code_abbrev]: "finite' = finite"

lemma finite'_code [code]:
  "finite' (set xs)  True"
  "finite' (List.coset xs)  of_phantom (finite_UNIV :: 'a finite_UNIV)"
by(simp_all add: card_gt_0_iff finite_UNIV)

end

context fixes xs :: "'a :: card_UNIV list"
begin

qualified definition card' :: "'a set  nat" 
where [simp, code del, code_abbrev]: "card' = card"
 
lemma card'_code [code]:
  "card' (set xs) = length (remdups xs)"
  "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
by(simp_all add: List.card_set card_Compl card_UNIV)


qualified definition subset' :: "'a set  'a set  bool"
where [simp, code del, code_abbrev]: "subset' = (⊆)"

lemma subset'_code [code]:
  "subset' A (List.coset ys)  (y  set ys. y  A)"
  "subset' (set ys) B  (y  set ys. y  B)"
  "subset' (List.coset xs) (set ys)  (let n = CARD('a) in n > 0  card(set (xs @ ys)) = n)"
by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
  (metis finite_compl finite_set rev_finite_subset)

qualified definition eq_set :: "'a set  'a set  bool"
where [simp, code del, code_abbrev]: "eq_set = (=)"

lemma eq_set_code [code]:
  fixes ys
  defines "rhs  
  let n = CARD('a)
  in if n = 0 then False else 
        let xs' = remdups xs; ys' = remdups ys 
        in length xs' + length ys' = n  (x  set xs'. x  set ys')  (y  set ys'. y  set xs')"
  shows "eq_set (List.coset xs) (set ys)  rhs"
  and "eq_set (set ys) (List.coset xs)  rhs"
  and "eq_set (set xs) (set ys)  (x  set xs. x  set ys)  (y  set ys. y  set xs)"
  and "eq_set (List.coset xs) (List.coset ys)  (x  set xs. x  set ys)  (y  set ys. y  set xs)"
proof goal_cases
  {
    case 1
    show ?case (is "?lhs  ?rhs")
    proof
      show ?rhs if ?lhs
        using that
        by (auto simp add: rhs_def Let_def List.card_set[symmetric]
          card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV
          Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
      show ?lhs if ?rhs
      proof - 
        have " yset xs. y  set ys; xset ys. x  set xs   set xs  set ys = {}" by blast
        with that show ?thesis
          by (auto simp add: rhs_def Let_def List.card_set[symmetric]
            card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"]
            dest: card_eq_UNIV_imp_eq_UNIV split: if_split_asm)
      qed
    qed
  }
  moreover
  case 2
  ultimately show ?case unfolding eq_set_def by blast
next
  case 3
  show ?case unfolding eq_set_def List.coset_def by blast
next
  case 4
  show ?case unfolding eq_set_def List.coset_def by blast
qed

end

text ‹
  Provide more informative exceptions than Match for non-rewritten cases.
  If generated code raises one these exceptions, then a code equation calls
  the mentioned operator for an element type that is not an instance of
  classcard_UNIV and is therefore not implemented via termcard_UNIV.
  Constrain the element type with sort classcard_UNIV to change this.
›

lemma card_coset_error [code]:
  "card (List.coset xs) = 
   Code.abort (STR ''card (List.coset _) requires type class instance card_UNIV'')
     (λ_. card (List.coset xs))"
by(simp)

lemma coset_subseteq_set_code [code]:
  "List.coset xs  set ys  
  (if xs = []  ys = [] then False 
   else Code.abort
     (STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'')
     (λ_. List.coset xs  set ys))"
by simp

notepad begin ― ‹test code setup›
have "List.coset [True] = set [False]  
      List.coset []  List.set [True, False]  
      finite (List.coset [True])"
  by eval

end

end