# Theory Card_Datatype

(*  Title:      Containers/Card_Datatype.thy
Author:     Andreas Lochbihler, ETH Zurich *)

theory Card_Datatype
imports
begin

section ‹Definitions to prove equations about the cardinality of data types›

subsection ‹Specialised @{term range} constants›

definition rangeIt :: "'a  ('a  'a)  'a set"
where "rangeIt x f = range (λn. (f ^^ n) x)"

definition rangeC :: "('a  'b) set  'b set"
where "rangeC F = (f  F. range f)"

lemma infinite_rangeIt:
assumes inj: "inj f"
and x: "y. x  f y"
shows "¬ finite (rangeIt x f)"
proof -
have "inj (λn. (f ^^ n) x)"
proof(rule injI)
fix n m
assume "(f ^^ n) x = (f ^^ m) x"
thus "n = m"
proof(induct n arbitrary: m)
case 0
thus ?case using x by(cases m)(auto intro: sym)
next
case (Suc n)
thus ?case using x by(cases m)(auto intro: sym dest: injD[OF inj])
qed
qed
thus ?thesis
by(auto simp add: rangeIt_def dest: finite_imageD)
qed

lemma in_rangeC: "f  A  f x  rangeC A"
by(auto simp add: rangeC_def)

lemma in_rangeCE: assumes "y  rangeC A"
obtains f x where "f  A" "y = f x"
using assms by(auto simp add: rangeC_def)

lemma in_rangeC_singleton: "f x  rangeC {f}"
by(auto simp add: rangeC_def)

lemma in_rangeC_singleton_const: "x  rangeC {λ_. x}"
by(rule in_rangeC_singleton)

lemma rangeC_rangeC: "f  rangeC A  f x  rangeC (rangeC A)"
by(auto simp add: rangeC_def)

lemma rangeC_eq_empty: "rangeC A = {}  A = {}"
by(auto simp add: rangeC_def)

lemma Ball_rangeC_iff:
"(x  rangeC A. P x)  (f  A. x. P (f x))"
by(auto intro: in_rangeC elim: in_rangeCE)

lemma Ball_rangeC_singleton:
"(x  rangeC {f}. P x)  (x. P (f x))"
by(simp add: Ball_rangeC_iff)

lemma Ball_rangeC_rangeC:
"(x  rangeC (rangeC A). P x)  (f  rangeC A. x. P (f x))"
by(simp add: Ball_rangeC_iff)

lemma finite_rangeC:
assumes inj: "f  A. inj f"
and disjoint: "f  A. g  A. f  g  (x y. f x  g y)"
shows "finite (rangeC (A :: ('a  'b) set))  finite A  (A  {}  finite (UNIV :: 'a set))"
(is "?lhs  ?rhs")
proof
assume ?lhs
thus ?rhs using inj disjoint
proof(induct "rangeC A" arbitrary: A rule: finite_psubset_induct)
case (psubset A)
show ?case
proof(cases "A = {}")
case True thus ?thesis by simp
next
case False
then obtain f A' where A: "A = insert f A'" and f: "f  A" "f  A'"
by(fastforce dest: mk_disjoint_insert)
from A have rA: "rangeC A = rangeC A'  range f"
by(auto simp add: rangeC_def)

have "¬ range f  rangeC A'"
proof
assume "range f  rangeC A'"
moreover obtain x where x: "x  range f" by auto
ultimately have "x  rangeC A'" by auto
then obtain g where "g  A'" "x  range g" by(auto simp add: rangeC_def)
with f  A' A have "g  A" "f  g" by auto
with f  A have "x y. f x  g y" by(rule psubset.prems[rule_format])
thus False using x x  range g by auto
qed
hence "rangeC A'  rangeC A" unfolding rA by auto
hence "finite A'  (A'  {}  finite (UNIV :: 'a set))"
using psubset.prems
by -(erule psubset.hyps, auto simp add: A)
with A have "finite A" by simp
moreover with finite (rangeC A) A f  A. inj f
have "finite (UNIV :: 'a set)"
by(auto simp add: rangeC_def dest: finite_imageD)
ultimately show ?thesis by blast
qed
qed
qed(auto simp add: rangeC_def)

lemma finite_rangeC_singleton_const:
"finite (rangeC {λ_. x})"
by(auto simp add: rangeC_def image_def)

lemma card_Un:
" finite A; finite B   card (A  B) = card (A) + card (B) - card(A  B)"
by(subst card_Un_Int) simp_all

lemma card_rangeC_singleton_const:
"card (rangeC {λ_. f}) = 1"
by(simp add: rangeC_def image_def)

lemma card_rangeC:
assumes inj: "f  A. inj f"
and disjoint: "f  A. g  A. f  g  (x y. f x  g y)"
shows "card (rangeC (A :: ('a  'b) set)) = CARD('a) * card A"
(is "?lhs = ?rhs")
proof(cases "finite (UNIV :: 'a set)  finite A")
case False
thus ?thesis using False finite_rangeC[OF assms]
by(auto simp add: card_eq_0_iff rangeC_eq_empty)
next
case True
{ fix f
assume "f  A"
hence "card (range f) = CARD('a)" using inj by(simp add: card_image) }
thus ?thesis using disjoint True unfolding rangeC_def
by(subst card_UN_disjoint) auto
qed

lemma rangeC_Int_rangeC:
" f  A. g  B. x y. f x  g y   rangeC A  rangeC B = {}"
by(auto simp add: rangeC_def)

lemmas rangeC_simps =
in_rangeC_singleton
in_rangeC_singleton_const
rangeC_rangeC
rangeC_eq_empty
Ball_rangeC_singleton
Ball_rangeC_rangeC
finite_rangeC
finite_rangeC_singleton_const
card_rangeC_singleton_const
card_rangeC
rangeC_Int_rangeC

bundle card_datatype =
rangeC_simps [simp]
card_Un [simp]
fun_eq_iff [simp]
Int_Un_distrib [simp]
Int_Un_distrib2 [simp]
card_eq_0_iff [simp]
imageI [simp] image_eqI [simp del]
conj_cong [cong]
infinite_rangeIt [simp]

subsection ‹Cardinality primitives for polymorphic HOL types›

ML structure Card_Simp_Rules = Named_Thms
(
val name = @{binding card_simps}
val description = "Simplification rules for cardinality of types"
)
setup Card_Simp_Rules.setup

definition card_fun :: "nat  nat  nat"
where "card_fun a b = (if a  0  b  0  b = 1 then b ^ a else 0)"

lemma CARD_fun [card_simps]:
"CARD('a  'b) = card_fun CARD('a) CARD('b)"
by(simp add: card_fun card_fun_def)

definition card_sum :: "nat  nat  nat"
where "card_sum a b = (if a = 0  b = 0 then 0 else a + b)"

lemma CARD_sum [card_simps]:
"CARD('a + 'b) = card_sum CARD('a) CARD('b)"
by(simp add: card_UNIV_sum card_sum_def)

definition card_option :: "nat  nat"
where "card_option n = (if n = 0 then 0 else Suc n)"

lemma CARD_option [card_simps]:
"CARD('a option) = card_option CARD('a)"
by(simp add: card_option_def card_UNIV_option)

definition card_prod :: "nat  nat  nat"
where "card_prod a b = a * b"

lemma CARD_prod [card_simps]:
"CARD('a * 'b) = card_prod CARD('a) CARD('b)"
by(simp add: card_prod_def)

definition card_list :: "nat  nat"
where "card_list _ = 0"

lemma CARD_list [card_simps]: "CARD('a list) = card_list CARD('a)"
by(simp add: card_list_def infinite_UNIV_listI)

end