1 (* Title: ZF/Induct/Binary_Trees.thy
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3 Copyright 1992 University of Cambridge
6 header {* Binary trees *}
8 theory Binary_Trees imports Main begin
10 subsection {* Datatype definition *}
16 Lf | Br ("a \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)")
18 declare bt.intros [simp]
20 lemma Br_neq_left: "l \<in> bt(A) ==> Br(x, l, r) \<noteq> l"
21 by (induct arbitrary: x r set: bt) auto
23 lemma Br_iff: "Br(a, l, r) = Br(a', l', r') \<longleftrightarrow> a = a' & l = l' & r = r'"
24 -- "Proving a freeness theorem."
25 by (fast elim!: bt.free_elims)
27 inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
28 -- "An elimination rule, for type-checking."
31 \medskip Lemmas to justify using @{term bt} in other recursive type
35 lemma bt_mono: "A \<subseteq> B ==> bt(A) \<subseteq> bt(B)"
36 apply (unfold bt.defs)
38 apply (rule bt.bnd_mono)+
39 apply (rule univ_mono basic_monos | assumption)+
42 lemma bt_univ: "bt(univ(A)) \<subseteq> univ(A)"
43 apply (unfold bt.defs bt.con_defs)
44 apply (rule lfp_lowerbound)
45 apply (rule_tac [2] A_subset_univ [THEN univ_mono])
46 apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
49 lemma bt_subset_univ: "A \<subseteq> univ(B) ==> bt(A) \<subseteq> univ(B)"
50 apply (rule subset_trans)
58 !!x y z r s. [| x \<in> A; y \<in> bt(A); z \<in> bt(A); r \<in> C(y); s \<in> C(z) |] ==>
59 h(x, y, z, r, s) \<in> C(Br(x, y, z))
60 |] ==> bt_rec(c, h, t) \<in> C(t)"
61 -- {* Type checking for recursor -- example only; not really needed. *}
67 subsection {* Number of nodes, with an example of tail-recursion *}
69 consts n_nodes :: "i => i"
72 "n_nodes(Br(a, l, r)) = succ(n_nodes(l) #+ n_nodes(r))"
74 lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
75 by (induct set: bt) auto
77 consts n_nodes_aux :: "i => i"
79 "n_nodes_aux(Lf) = (\<lambda>k \<in> nat. k)"
80 "n_nodes_aux(Br(a, l, r)) =
81 (\<lambda>k \<in> nat. n_nodes_aux(r) ` (n_nodes_aux(l) ` succ(k)))"
84 "t \<in> bt(A) ==> k \<in> nat ==> n_nodes_aux(t)`k = n_nodes(t) #+ k"
85 apply (induct arbitrary: k set: bt)
91 n_nodes_tail :: "i => i" where
92 "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
94 lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
95 by (simp add: n_nodes_tail_def n_nodes_aux_eq)
98 subsection {* Number of leaves *}
104 "n_leaves(Br(a, l, r)) = n_leaves(l) #+ n_leaves(r)"
106 lemma n_leaves_type [simp]: "t \<in> bt(A) ==> n_leaves(t) \<in> nat"
107 by (induct set: bt) auto
110 subsection {* Reflecting trees *}
113 bt_reflect :: "i => i"
115 "bt_reflect(Lf) = Lf"
116 "bt_reflect(Br(a, l, r)) = Br(a, bt_reflect(r), bt_reflect(l))"
118 lemma bt_reflect_type [simp]: "t \<in> bt(A) ==> bt_reflect(t) \<in> bt(A)"
119 by (induct set: bt) auto
122 \medskip Theorems about @{term n_leaves}.
125 lemma n_leaves_reflect: "t \<in> bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"
126 by (induct set: bt) (simp_all add: add_commute)
128 lemma n_leaves_nodes: "t \<in> bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
129 by (induct set: bt) simp_all
132 Theorems about @{term bt_reflect}.
135 lemma bt_reflect_bt_reflect_ident: "t \<in> bt(A) ==> bt_reflect(bt_reflect(t)) = t"
136 by (induct set: bt) simp_all