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