structure TypeBase
The interface to TypeBase is intended to provide support for writers of high-level tools for reasoning about datatypes.
- Hol_datatype `tree = Leaf | Node of 'a => tree => tree`; <<HOL message: Defined type: "tree">> > val it = () : unit - TypeBase.read {Thy = current_theory(), Tyop = "tree"}; > val it = SOME----------------------- ----------------------- HOL datatype: "tree" Primitive recursion: |- !f0 f1. ?fn. (!a. fn (Leaf a) = f0 a) /\ !a0 a1. fn (Node a0 a1) = f1 a0 a1 (fn a0) (fn a1) Case analysis: |- (!f f1 a. case f f1 (Leaf a) = f a) /\ !f f1 a0 a1. case f f1 (Node a0 a1) = f1 a0 a1 Size: |- (!a. tree_size (Leaf a) = 1 + a) /\ !a0 a1. tree_size (Node a0 a1) = 1 + (tree_size a0 + tree_size a1) Induction: |- !P. (!n. P (Leaf n)) /\ (!t t0. P t /\ P t0 ==> P (Node t t0)) ==> !t. P t Case completeness: |- !t. (?n. t = Leaf n) \/ ?t' t0. t = Node t' t0 One-to-one: |- (!a a'. (Leaf a = Leaf a') = (a = a')) /\ !a0 a1 a0' a1'. (Node a0 a1 = Node a0' a1') = (a0 = a0') /\ (a1 = a1') Distinctness: |- !a1 a0 a. ~(Leaf a = Node a0 a1) : tyinfo option