|
(* Title: ZF/Induct/Binary_Trees.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
section \<open>Binary trees\<close>
theory Binary_Trees imports ZF begin
subsection \<open>Datatype definition\<close>
consts
bt :: "i => i"
datatype "bt(A)" =
Lf | Br ("a \ A", "t1 \ bt(A)", "t2 \ bt(A)")
declare bt.intros [simp]
lemma Br_neq_left: "l \ bt(A) ==> Br(x, l, r) \ l"
by (induct arbitrary: x r set: bt) auto
lemma Br_iff: "Br(a, l, r) = Br(a', l', r') \ a = a' & l = l' & r = r'"
\<comment> \<open>Proving a freeness theorem.\<close>
by (fast elim!: bt.free_elims)
inductive_cases BrE: "Br(a, l, r) \ bt(A)"
\<comment> \<open>An elimination rule, for type-checking.\<close>
text \<open>
\medskip Lemmas to justify using \<^term>\<open>bt\<close> in other recursive type
definitions.
\<close>
lemma bt_mono: "A \ B ==> bt(A) \ bt(B)"
apply (unfold bt.defs)
apply (rule lfp_mono)
apply (rule bt.bnd_mono)+
apply (rule univ_mono basic_monos | assumption)+
done
lemma bt_univ: "bt(univ(A)) \ univ(A)"
apply (unfold bt.defs bt.con_defs)
apply (rule lfp_lowerbound)
apply (rule_tac [2] A_subset_univ [THEN univ_mono])
apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
done
lemma bt_subset_univ: "A \ univ(B) ==> bt(A) \ univ(B)"
apply (rule subset_trans)
apply (erule bt_mono)
apply (rule bt_univ)
done
lemma bt_rec_type:
"[| t \ bt(A);
c \<in> C(Lf);
!!x y z r s. [| x \<in> A; y \<in> bt(A); z \<in> bt(A); r \<in> C(y); s \<in> C(z) |] ==>
h(x, y, z, r, s) \<in> C(Br(x, y, z))
|] ==> bt_rec(c, h, t) \<in> C(t)"
\<comment> \<open>Type checking for recursor -- example only; not really needed.\<close>
apply (induct_tac t)
apply simp_all
done
subsection \<open>Number of nodes, with an example of tail-recursion\<close>
consts n_nodes :: "i => i"
primrec
"n_nodes(Lf) = 0"
"n_nodes(Br(a, l, r)) = succ(n_nodes(l) #+ n_nodes(r))"
lemma n_nodes_type [simp]: "t \ bt(A) ==> n_nodes(t) \ nat"
by (induct set: bt) auto
consts n_nodes_aux :: "i => i"
primrec
"n_nodes_aux(Lf) = (\k \ nat. k)"
"n_nodes_aux(Br(a, l, r)) =
(\<lambda>k \<in> nat. n_nodes_aux(r) ` (n_nodes_aux(l) ` succ(k)))"
lemma n_nodes_aux_eq:
"t \ bt(A) ==> k \ nat ==> n_nodes_aux(t)`k = n_nodes(t) #+ k"
apply (induct arbitrary: k set: bt)
apply simp
apply (atomize, simp)
done
definition
n_nodes_tail :: "i => i" where
"n_nodes_tail(t) == n_nodes_aux(t) ` 0"
lemma "t \ bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
by (simp add: n_nodes_tail_def n_nodes_aux_eq)
subsection \<open>Number of leaves\<close>
consts
n_leaves :: "i => i"
primrec
"n_leaves(Lf) = 1"
"n_leaves(Br(a, l, r)) = n_leaves(l) #+ n_leaves(r)"
lemma n_leaves_type [simp]: "t \ bt(A) ==> n_leaves(t) \ nat"
by (induct set: bt) auto
subsection \<open>Reflecting trees\<close>
consts
bt_reflect :: "i => i"
primrec
"bt_reflect(Lf) = Lf"
"bt_reflect(Br(a, l, r)) = Br(a, bt_reflect(r), bt_reflect(l))"
lemma bt_reflect_type [simp]: "t \ bt(A) ==> bt_reflect(t) \ bt(A)"
by (induct set: bt) auto
text \<open>
\medskip Theorems about \<^term>\<open>n_leaves\<close>.
\<close>
lemma n_leaves_reflect: "t \ bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"
by (induct set: bt) (simp_all add: add_commute)
lemma n_leaves_nodes: "t \ bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
by (induct set: bt) simp_all
text \<open>
Theorems about \<^term>\<open>bt_reflect\<close>.
\<close>
lemma bt_reflect_bt_reflect_ident: "t \ bt(A) ==> bt_reflect(bt_reflect(t)) = t"
by (induct set: bt) simp_all
end
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
