theory DemoAVL
imports Main
begin

datatype tree = Tip | Br tree tree

text{* The height of a tree:*}

fun ht :: "tree \<Rightarrow> nat" where
"ht Tip = 0" |
"ht (Br t u) = max (ht t) (ht u) + 1"

text{* What is an AVL tree: *}

fun avl :: "tree \<Rightarrow> bool" where
"avl Tip \<longleftrightarrow> True" |
"avl (Br t u) \<longleftrightarrow> avl t \<and> avl u \<and> (ht t=ht u | ht t=ht u + 1 | ht u=ht t + 1)"

text{* A lower bound for the number of internal nodes in an
AVL tree of a given height. *}

fun fib1 :: "nat => nat" where
"fib1 0 = 0" |
"fib1 (Suc 0) = 1" |
"fib1 (Suc (Suc n)) = fib1 n + fib1 (Suc n) + 1"

lemma fib1_Suc: "fib1(Suc n) \<le> 2*fib1(n) + 1"
apply(induct n rule: fib1.induct)
apply auto
done

text{* A structured but still opaque proof: *}

lemma "avl t \<Longrightarrow> fib1(ht t) \<le> size t"
proof(induct t rule:avl.induct)
  case 1 thus ?case by simp
next
  case (2 t u)
  thus ?case using fib1_Suc[where n="ht t"]
      by (auto simp add: max_def)
qed

text{* A more detailed version: *}

lemma "avl t \<Longrightarrow> fib1(ht t) \<le> size t"
proof(induct t rule:avl.induct)
  case 1 thus ?case by simp
next
  case (2 t u)
  hence IH: "fib1(ht t) \<le> size t" "fib1(ht u) \<le> size u" by auto
  -- "The 3 cases:"
  have "ht t = ht u \<Longrightarrow> ?case" using IH fib1_Suc[where n="ht t"] by simp
  moreover
  have "ht t = ht u + 1 \<Longrightarrow> ?case" using IH by(simp add:max_def)
  moreover
  have "ht u = ht t + 1 \<Longrightarrow> ?case" using IH by(simp add:max_def)
  ultimately 
  show ?case using 2(3) by auto
qed

text{* Exercise: refine the above proof, show some step in more detail. *}

end