lemma "ord t ⟹ ord (ins i t)"
  apply(induction t)
   apply(auto)

proof (prove)
goal (2 subgoals):
 1. ⋀t1 x2 t2.
       ⟦ord t1 ⟹ ord (ins i t1); ord t2 ⟹ ord (ins i t2);
        ord_list (flatten t1 @ x2 # flatten t2); i < x2⟧
       ⟹ ord_list (flatten (ins i t1) @ x2 # flatten t2)
 2. ⋀t1 x2 t2.
       ⟦ord t1 ⟹ ord (ins i t1); ord t2 ⟹ ord (ins i t2);
        ord_list (flatten t1 @ x2 # flatten t2); ¬ i < x2; i ≠ x2⟧
       ⟹ ord_list (flatten t1 @ x2 # flatten (ins i t2))

datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"


(* Flatten a binary tree into a list in infix order *)
fun flatten :: "'a tree ⇒ 'a list" where
  "flatten Tip = []" |
  "flatten (Node l x r) = flatten l @ [x] @ flatten r"

(* Check if an integer list is ordered *)
fun ord_list :: "int list ⇒ bool" where
  "ord_list [] = True" |
  "ord_list [x] = True" |
  "ord_list (x#xs) = ((x < hd xs) ∧ (ord_list xs))"

(* Check if a binary tree of integers is ordered *)
fun ord :: "int tree ⇒ bool" where
  "ord Tip = True" |
  "ord (Node l x r) = ord_list(flatten (Node l x r))"

(* Insert an integer into an ordered binary tree *)
fun ins :: "int ⇒ int tree ⇒ int tree" where
  "ins x Tip = Node Tip x Tip" |
  "ins x (Node l a r) =
    (if x = a then
       Node l a r
     else if x < a then
       Node (ins x l) a r
     else
       Node l a (ins x r))"


(* Lemma needed for lemma below *)
lemma ord_list_dist: "ord_list (xs @ ys) ⟹ (ord_list xs ∧ ord_list ys)"
  apply(induction xs rule: ord_list.induct)
    apply(auto)
  apply(induction ys)
   apply(auto)
  done

(* Lemma proving ordered property holds after insertion *)
lemma "ord t ⟹ ord (ins i t)"
  apply(induction t)
   apply(auto)
  done