Quelle  Binary_Trees.thy   Sprache: Isabelle

(*  Title:      ZF/Induct/Binary_Trees.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge
*)

section ‹Binary trees›

theory Binary_Trees imports ZF begin

subsection ‹Datatype definition›

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'"
  🍋 ‹Proving a freeness theorem.›
  by (fast elim!: bt.free_elims)

inductive_cases BrE: "Br(a, l, r) \ bt(A)"
  🍋 ‹An elimination rule, for type-checking.›

text ‹
  \medskip Lemmas to justify using 🍋‹bt› in other recursive type
  definitions.
›

lemma bt_mono: "A \ B \ bt(A) \ bt(B)"
    unfolding 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)"
    unfolding 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 ∈ C(Lf);
    ∧x y z r s. [x ∈ A;  y ∈ bt(A);  z ∈ bt(A);  r ∈ C(y);  s ∈ C(z)] ==>
    h(x, y, z, r, s) ∈ C(Br(x, y, z))
] ==> bt_rec(c, h, t) ∈ C(t)"
  🍋 ‹Type checking for recursor -- example only; not really needed.›
  apply (induct_tac t)
   apply simp_all
  done


subsection ‹Number of nodes, with an example of tail-recursion›

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)) =
      (λk ∈ 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 ‹Number of leaves›

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 ‹Reflecting trees›

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 ‹
  \medskip Theorems about 🍋‹n_leaves›.
›

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 ‹
  Theorems about 🍋‹bt_reflect›.
›

lemma bt_reflect_bt_reflect_ident: "t \ bt(A) \ bt_reflect(bt_reflect(t)) = t"
  by (induct set: bt) simp_all

end