isabelle-datatype

name	isabelle-datatype
description	How to read constants and theorems generated by Isabelle datatype and codatatype definitions

Reading Datatype and Codatatype Definitions

A datatype defines finite values (e.g., lists, trees); a codatatype defines potentially infinite values (e.g., streams, lazy lists).

Constants

Datatype example: datatype 'a list = Nil | Cons (hd: 'a) (tl: "'a list")

A finite list with two constructors Nil (empty) and Cons (prepend), and selectors hd (head) and tl (tail).

• Constructors — Nil builds an empty list; Cons x xs prepends x to xs
• Selectors — hd (Cons x xs) = x, tl (Cons x xs) = xs. Partial for multi-constructor types: hd Nil is undefined
• case_list — pattern matching. case xs of Nil ⇒ e₁ | Cons a as ⇒ e₂ a as
• map_list — apply a function to every element. map_list f (Cons x xs) = Cons (f x) (map_list f xs)
• set_list — the set of all elements. set_list (Cons x xs) = {x} ∪ set_list xs
• pred_list — a predicate holds for every element. pred_list P xs means P holds for all elements
• rel_list — two lists related element-wise. rel_list R xs ys means same shape, corresponding elements related by R
• rec_list — the recursor, analogous to a fold. rec_list z s Nil = z and rec_list z s (Cons x xs) = s x xs (rec_list z s xs). It walks the list from tail to head: for Nil it returns z; for Cons x xs it calls s with three arguments — the element x, the tail xs, and the result of recursing on xs.

Codatatype example: codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream")

An infinite stream with a single constructor SCons and two selectors shd (head) and stl (tail).

It also has map_stream, set_stream, pred_stream, rel_stream, case_stream with a similar reading as list.

• corec_stream — the corecursor, which builds a stream from a seed. corec_stream g q h k a = SCons (g a) (if q a then h a else corec_stream g q h k (k a)). At each step, g extracts the head from the seed; then if the stop condition q holds, h supplies the remaining tail directly, otherwise the seed is advanced by k and the process repeats.

Another examlpe: codatatype 'a llist = LNil | LCons (lhd: 'a) (ltl: "'a llist")

Theorems

• list.split: P (case xs of Nil ⇒ e₁ | Cons a as ⇒ e₂ a as) = ((xs = Nil ⟶ P e₁) ∧ (∀a as. xs = Cons a as ⟶ P (e₂ a as))) → A property holds of a case expression over a list iff it holds when the list is Nil and it holds for every possible Cons a as.

• list.induct: P Nil ⟹ (⋀x xs. P xs ⟹ P (Cons x xs)) ⟹ P xs → To prove a property for all lists: prove it for Nil, then prove it for Cons x xs assuming it holds for xs (structural induction).

Codatatype: Coinduction

• stream.coinduct:

  R x y ⟹
  (⋀a b. R a b ⟹ shd a = shd b ∧ R (stl a) (stl b)) ⟹
  x = y
  

  → To prove two streams are equal, find a relation R holding between them and show that R implies equal heads and R-related tails (bisimulation principle).

• llist.rel_coinduct:

  P x y ⟹
  (⋀a b. P a b ⟹
    (a = LNil) = (b = LNil) ∧
    (a ≠ LNil ⟶ b ≠ LNil ⟶ R (lhd a) (lhd b) ∧ P (ltl a) (ltl b))) ⟹
  rel_llist R x y
  

  → To prove two lazy lists are related by rel_llist R, find a relation P and show that P implies matching constructors, R-related heads, and P-related tails.

Codatatype: Corecursor

• llist.corec: ¬p a ⟹ corec_llist p g q h k a = LCons (g a) (if q a then h a else corec_llist p g q h k (k a)) → When the stop predicate p does not hold, the corecursor produces LCons with head g a and a tail determined by q: if q a then h a directly, otherwise recurse with advanced seed k a.

• llist.corec_sel: ¬p a ⟹ lhd (corec_llist p g q h k a) = g a → The head of a corecursor result equals g applied to the seed.

• llist.corec_disc: p a ⟹ corec_llist p g q h k a = LNil → When the stop predicate holds, the corecursor produces LNil.

• llist.corec_disc_iff: (corec_llist p g q h k a = LNil) = p a → The corecursor produces LNil if and only if the stop predicate holds.