# Theory Card_Datatype_Ex

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

theory Card_Datatype_Ex imports
"../Card_Datatype"
begin

subsection ‹Examples›

subsubsection ‹Finite types›

datatype ('a, 'b) foo = Foo 'a | Bar 'a 'b | FooBar 'a 'b "'a + 'b" | Stop

lemma inj_foo [simp]:
"inj Foo"
"inj Bar" "inj (Bar x)"
"inj FooBar" "inj (FooBar x)" "inj (FooBar x y)"

context includes card_datatype begin

lemma UNIV_foo:
"(UNIV :: ('a, 'b) foo set) =
rangeC {Foo} ∪
rangeC (rangeC {Bar}) ∪
rangeC (rangeC (rangeC {FooBar})) ∪
rangeC {λ_::unit. Stop}"
apply(rule UNIV_eq_I)
apply(case_tac x)
apply(simp_all)
done

lemma finite_UNIV_foo:
"finite (UNIV :: ('a, 'b) foo set) ⟷ finite (UNIV :: 'a set) ∧ finite (UNIV :: 'b set)"

definition card_foo :: "nat ⇒ nat ⇒ nat"
where "card_foo a b = (if a = 0 ∨ b = 0 then 0 else a + a * b + a * b * card_sum a b + 1)"

lemma CARD_foo [card_simps]:
"CARD(('a, 'b) foo) = card_foo CARD('a) CARD('b)"
by(simp add: card_foo_def UNIV_foo Let_def card_simps)

end

datatype ('a, 'b) bar
= Bar1
| Bar2 "'a ⇒ 'b"
| Bar3 "('a, 'b) foo" "'a ⇒ char ⇒ 'b ⇒ 'a" "('a × 'b) option"
| Bar4 char 'a bool

lemma inj_bar [simp]:
"inj Bar2"
"inj Bar3"
"inj (Bar3 x)"
"inj (Bar3 x y)"
"inj Bar4"
"inj (Bar4 z)"
"inj (Bar4 z u)"

context includes card_datatype begin

lemma UNIV_bar:
"(UNIV :: ('a, 'b) bar set) =
rangeC {λ_::unit. Bar1} ∪
rangeC {Bar2} ∪
rangeC (rangeC (rangeC {Bar3})) ∪
rangeC (rangeC (rangeC {Bar4}))"
apply(rule UNIV_eq_I)
apply(case_tac x)
apply(simp_all)
done

lemma finite_UNIV_bar:
"finite (UNIV :: ('a, 'b) bar set) ⟷ finite (UNIV :: 'a set) ∧ finite (UNIV :: 'b set)"
by(auto simp add: UNIV_bar finite_UNIV_fun finite_prod finite_UNIV_foo)

definition card_bar :: "nat ⇒ nat ⇒ nat"
where
"card_bar a b =
(if a = 0 ∨ b = 0 then 0
else 1 + card_fun a b + card_foo a b * card_fun a (card_fun CARD(char) (card_fun b a)) * card_option (card_prod a b) + CARD(char) * a * CARD(bool))"

lemma CARD_bar [card_simps]:
"CARD(('a, 'b) bar) = card_bar CARD('a) CARD('b)"
by(simp add: UNIV_bar card_bar_def finite_UNIV_bar finite_UNIV_foo finite_prod finite_UNIV_fun card_simps del: card_prod)

end

subsection ‹Infinite types›

datatype 'a tree = Leaf | Node 'a "'a tree" "'a tree"

lemma inj_expr [simp]:
"inj Node"
"inj (Node a)"
"inj (Node a l)"

context includes card_datatype begin

lemma finite_UNIV_tree: "finite (UNIV :: 'a tree set) ⟷ False"
proof -
have "rangeIt Leaf (Node (undefined :: 'a) Leaf) ⊆ UNIV" by simp
from finite_subset[OF this] show ?thesis by auto
qed

definition card_tree :: "nat ⇒ nat"
where "card_tree _ = 0"

lemma CARD_tree [card_simps]:
"CARD('a tree) = card_tree CARD('a)"

end

end
```