Theory Datatypes
section ‹Sample datatype definitions›
theory Datatypes imports ZF begin
subsection ‹A type with four constructors›
text ‹
It has four contructors, of arities 0--3, and two parameters ‹A› and ‹B›.
›
consts
data :: "[i, i] ⇒ i"
datatype "data(A, B)" =
Con0
| Con1 ("a ∈ A")
| Con2 ("a ∈ A", "b ∈ B")
| Con3 ("a ∈ A", "b ∈ B", "d ∈ data(A, B)")
lemma data_unfold: "data(A, B) = ({0} + A) + (A × B + A × B × data(A, B))"
by (fast intro!: data.intros [unfolded data.con_defs]
elim: data.cases [unfolded data.con_defs])
text ‹
\medskip Lemmas to justify using \<^term>‹data› in other recursive
type definitions.
›
lemma data_mono: "⟦A ⊆ C; B ⊆ D⟧ ⟹ data(A, B) ⊆ data(C, D)"
unfolding data.defs
apply (rule lfp_mono)
apply (rule data.bnd_mono)+
apply (rule univ_mono Un_mono basic_monos | assumption)+
done
lemma data_univ: "data(univ(A), univ(A)) ⊆ univ(A)"
unfolding data.defs data.con_defs
apply (rule lfp_lowerbound)
apply (rule_tac [2] subset_trans [OF A_subset_univ Un_upper1, THEN univ_mono])
apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
done
lemma data_subset_univ:
"⟦A ⊆ univ(C); B ⊆ univ(C)⟧ ⟹ data(A, B) ⊆ univ(C)"
by (rule subset_trans [OF data_mono data_univ])
subsection ‹Example of a big enumeration type›
text ‹
Can go up to at least 100 constructors, but it takes nearly 7
minutes \dots\ (back in 1994 that is).
›
consts
enum :: i