Theory HOL-Library.Code_Cardinality
section ‹Code setup for sets with cardinality type information›
theory Code_Cardinality imports Cardinality begin
text ‹
Implement \<^term>‹CARD('a)› via \<^term>‹card_UNIV› and provide
implementations for \<^term>‹finite›, \<^term>‹card›, \<^term>‹(⊆)›,
and \<^term>‹(=)›if the calling context already provides \<^class>‹finite_UNIV›
and \<^class>‹card_UNIV› instances. If we implemented the latter
always via \<^term>‹card_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 "⟦ ∀y∈set xs. y ∉ set ys; ∀x∈set 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
\<^class>‹card_UNIV› and is therefore not implemented via \<^term>‹card_UNIV›.
Constrain the element type with sort \<^class>‹card_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
have "List.coset [True] = set [False] ∧
List.coset [] ⊆ List.set [True, False] ∧
finite (List.coset [True])"
by eval
end
end