1(*  Title:      ZF/Induct/Binary_Trees.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1992  University of Cambridge
4*)
5
6section \<open>Binary trees\<close>
7
8theory Binary_Trees imports ZF begin
9
10subsection \<open>Datatype definition\<close>
11
12consts
13  bt :: "i => i"
14
15datatype "bt(A)" =
16  Lf | Br ("a \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)")
17
18declare bt.intros [simp]
19
20lemma Br_neq_left: "l \<in> bt(A) ==> Br(x, l, r) \<noteq> l"
21  by (induct arbitrary: x r set: bt) auto
22
23lemma Br_iff: "Br(a, l, r) = Br(a', l', r') \<longleftrightarrow> a = a' & l = l' & r = r'"
24  \<comment> \<open>Proving a freeness theorem.\<close>
25  by (fast elim!: bt.free_elims)
26
27inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
28  \<comment> \<open>An elimination rule, for type-checking.\<close>
29
30text \<open>
31  \medskip Lemmas to justify using \<^term>\<open>bt\<close> in other recursive type
32  definitions.
33\<close>
34
35lemma bt_mono: "A \<subseteq> B ==> bt(A) \<subseteq> bt(B)"
36  apply (unfold bt.defs)
37  apply (rule lfp_mono)
38    apply (rule bt.bnd_mono)+
39  apply (rule univ_mono basic_monos | assumption)+
40  done
41
42lemma 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)
47  done
48
49lemma bt_subset_univ: "A \<subseteq> univ(B) ==> bt(A) \<subseteq> univ(B)"
50  apply (rule subset_trans)
51   apply (erule bt_mono)
52  apply (rule bt_univ)
53  done
54
55lemma bt_rec_type:
56  "[| t \<in> bt(A);
57    c \<in> C(Lf);
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  \<comment> \<open>Type checking for recursor -- example only; not really needed.\<close>
62  apply (induct_tac t)
63   apply simp_all
64  done
65
66
67subsection \<open>Number of nodes, with an example of tail-recursion\<close>
68
69consts  n_nodes :: "i => i"
70primrec
71  "n_nodes(Lf) = 0"
72  "n_nodes(Br(a, l, r)) = succ(n_nodes(l) #+ n_nodes(r))"
73
74lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
75  by (induct set: bt) auto
76
77consts  n_nodes_aux :: "i => i"
78primrec
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)))"
82
83lemma n_nodes_aux_eq:
84    "t \<in> bt(A) ==> k \<in> nat ==> n_nodes_aux(t)`k = n_nodes(t) #+ k"
85  apply (induct arbitrary: k set: bt)
86   apply simp
87  apply (atomize, simp)
88  done
89
90definition
91  n_nodes_tail :: "i => i"  where
92  "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
93
94lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
95  by (simp add: n_nodes_tail_def n_nodes_aux_eq)
96
97
98subsection \<open>Number of leaves\<close>
99
100consts
101  n_leaves :: "i => i"
102primrec
103  "n_leaves(Lf) = 1"
104  "n_leaves(Br(a, l, r)) = n_leaves(l) #+ n_leaves(r)"
105
106lemma n_leaves_type [simp]: "t \<in> bt(A) ==> n_leaves(t) \<in> nat"
107  by (induct set: bt) auto
108
109
110subsection \<open>Reflecting trees\<close>
111
112consts
113  bt_reflect :: "i => i"
114primrec
115  "bt_reflect(Lf) = Lf"
116  "bt_reflect(Br(a, l, r)) = Br(a, bt_reflect(r), bt_reflect(l))"
117
118lemma bt_reflect_type [simp]: "t \<in> bt(A) ==> bt_reflect(t) \<in> bt(A)"
119  by (induct set: bt) auto
120
121text \<open>
122  \medskip Theorems about \<^term>\<open>n_leaves\<close>.
123\<close>
124
125lemma 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)
127
128lemma n_leaves_nodes: "t \<in> bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
129  by (induct set: bt) simp_all
130
131text \<open>
132  Theorems about \<^term>\<open>bt_reflect\<close>.
133\<close>
134
135lemma bt_reflect_bt_reflect_ident: "t \<in> bt(A) ==> bt_reflect(bt_reflect(t)) = t"
136  by (induct set: bt) simp_all
137
138end
139