PFDS.thy

theory PFDS
imports Main
begin

datatype 'a Tree = E | T "'a Tree" 'a "'a Tree"

primrec trmax :: "'a ⇒ 'a Tree ⇒ 'a" where
"trmax a E = a" |
"trmax _ (T _ here right) = trmax here right" 

primrec trmin :: "'a ⇒ 'a Tree ⇒ 'a" where
"trmin a E = a" |
"trmin _ (T left here _) = trmin here left"

primrec bst :: "'a::{ord, bot, top} Tree ⇒ bool" where
"bst E = True" |
"bst (T left here right) = (bst left ∧ (trmax bot left ≤ here) ∧ bst right ∧ (here ≤ trmin top right))"

primrec flatten :: "'a Tree ⇒ 'a list" where
"flatten E = []" |
"flatten (T left here right) = flatten left @ here # flatten right"

lemma "hd (flatten E @ x # y) = x"
apply(auto)
done

lemma headlemma : "hd (a @ b # c) = hd (a @ b # d)"
apply(case_tac a)
apply(auto)
done

lemma "trmin (hd []) tree = hd (flatten tree)"
apply(induct_tac tree)
apply(auto)
apply(case_tac x1)
apply(auto)
apply(simp add: headlemma)
done

lemma "trmax (hd []) tree = hd (rev (flatten tree))"
apply(induct_tac tree)
apply(auto)
apply(case_tac x3)
apply(auto)
apply(simp add: headlemma)
done