Theory Tree_Rotations

(* Author: Tobias Nipkow *)

section ‹Tree Rotations›

theory Tree_Rotations
imports "HOL-Library.Tree"
begin

text ‹How to transform a tree into a list and into any other tree (with the same @{const inorder})
by rotations.›

fun is_list :: "'a tree ⇒ bool" where
"is_list (Node l _ r) = (l = Leaf ∧ is_list r)" |
"is_list Leaf = True"

text ‹Termination proof via measure function. NB @{term "size t - rlen t"} works for
the actual rotation equation but not for the second equation.›

fun rlen :: "'a tree ⇒ nat" where
"rlen Leaf = 0" |
"rlen (Node l x r) = rlen r + 1"

lemma rlen_le_size: "rlen t ≤ size t"
by(induction t) auto


subsection ‹Without positions›

function (sequential) list_of :: "'a tree ⇒ 'a tree" where
"list_of (Node (Node A a B) b C) = list_of (Node A a (Node B b C))" |
"list_of (Node Leaf a A) = Node Leaf a (list_of A)" |
"list_of Leaf = Leaf"
by pat_completeness auto

termination
proof
  let ?R = "measure(λt. 2*size t - rlen t)"
  show "wf ?R" by (auto simp add: mlex_prod_def)

  fix A a B b C
  show "(Node A a (Node B b C), Node (Node A a B) b C) ∈ ?R"
    using rlen_le_size[of C] by(simp)

  fix a A show "(A, Node Leaf a A) ∈ ?R" using rlen_le_size[of A] by(simp)
qed

lemma is_list_rot: "is_list(list_of t)"
by (induction t rule: list_of.induct) auto

lemma inorder_rot: "inorder(list_of t) = inorder t"
by (induction t rule: list_of.induct) auto


subsection ‹With positions›

datatype dir = L | R

type_synonym "pos" = "dir list"

function (sequential) rotR_poss :: "'a tree ⇒ pos list" where
"rotR_poss (Node (Node A a B) b C) = [] # rotR_poss (Node A a (Node B b C))" |
"rotR_poss (Node Leaf a A) = map (Cons R) (rotR_poss A)" |
"rotR_poss Leaf = []"
by pat_completeness auto

termination
proof
  let ?R = "measure(λt. 2*size t - rlen t)"
  show "wf ?R" by (auto simp add: mlex_prod_def)

  fix A a B b C
  show "(Node A a (Node B b C), Node (Node A a B) b C) ∈ ?R"
    using rlen_le_size[of C] by(simp)

  fix a A show "(A, Node Leaf a A) ∈ ?R" using rlen_le_size[of A] by(simp)
qed

fun rotR :: "'a tree ⇒ 'a tree" where
"rotR (Node (Node A a B) b C) = Node A a (Node B b C)"

fun rotL :: "'a tree ⇒ 'a tree" where
"rotL (Node A a (Node B b C)) = Node (Node A a B) b C"

fun apply_at :: "('a tree ⇒ 'a tree) ⇒ pos ⇒ 'a tree ⇒ 'a tree" where
  "apply_at f [] t = f t"
| "apply_at f (L # ds) (Node l a r) = Node (apply_at f ds l) a r"
| "apply_at f (R # ds) (Node l a r) = Node l a (apply_at f ds r)"

fun apply_ats :: "('a tree ⇒ 'a tree) ⇒ pos list ⇒ 'a tree ⇒ 'a tree" where
"apply_ats _ [] t = t" |
"apply_ats f (p#ps) t = apply_ats f ps (apply_at f p t)"

lemma apply_ats_append:
  "apply_ats f (ps⇩1 @ ps⇩2) t = apply_ats f ps⇩2 (apply_ats f ps⇩1 t)"
by (induction ps⇩1 arbitrary: t) auto

abbreviation "rotRs ≡ apply_ats rotR"
abbreviation "rotLs ≡ apply_ats rotL"

lemma apply_ats_map_R: "apply_ats f (map ((#) R) ps) ⟨l, a, r⟩ = Node l a (apply_ats f ps r)"
by(induction ps arbitrary: r) auto

lemma inorder_rotRs_poss: "inorder (rotRs (rotR_poss t) t) = inorder t"
apply(induction t rule: rotR_poss.induct)
apply(auto simp: apply_ats_map_R)
done

lemma is_list_rotRs: "is_list (rotRs (rotR_poss t) t)"
apply(induction t rule: rotR_poss.induct)
apply(auto simp: apply_ats_map_R)
done

lemma "is_list (rotRs ps t) ⟶ length ps ≤ length(rotR_poss t)"
quickcheck[expect=counterexample]
oops

lemma length_rotRs_poss: "length (rotR_poss t) = size t - rlen t"
proof(induction t rule: rotR_poss.induct)
  case (1 A a B b C)
  then show ?case using rlen_le_size[of C] by simp
qed auto

lemma is_list_inorder_same:
  "is_list t1 ⟹ is_list t2 ⟹ inorder t1 = inorder t2 ⟹ t1 = t2"
proof(induction t1 arbitrary: t2)
  case Leaf
  then show ?case by simp
next
  case Node
  then show ?case by (cases t2) simp_all
qed

lemma rot_id: "rotLs (rev (rotR_poss t)) (rotRs (rotR_poss t) t) = t"
apply(induction t rule: rotR_poss.induct)
apply(auto simp: apply_ats_map_R rev_map apply_ats_append)
done

corollary tree_to_tree_rotations: assumes "inorder t1 = inorder t2"
shows "rotLs (rev (rotR_poss t2)) (rotRs (rotR_poss t1) t1) = t2"
proof -
  have "rotRs (rotR_poss t1) t1 = rotRs (rotR_poss t2) t2" (is "?L = ?R")
    by (simp add: assms inorder_rotRs_poss is_list_inorder_same is_list_rotRs)
  hence "rotLs (rev (rotR_poss t2)) ?L = rotLs (rev (rotR_poss t2)) ?R"
    by simp
  also have "… = t2" by(rule rot_id)
  finally show ?thesis .
qed

lemma size_rlen_better_ub: "size t - rlen t ≤ size t - 1"
by (cases t) auto

end