Theory Pairing_Heap_List1_Analysis2

(* Author: Tobias Nipkow *)

subsection ‹Okasaki's Pairing Heaps via Transfer from Tree Analysis›

theory Pairing_Heap_List1_Analysis2
imports
  Pairing_Heap_List1_Analysis
  Pairing_Heap_Tree_Analysis
begin

text‹This theory transfers the amortized analysis of the tree-based
pairing heaps to Okasaki's pairing heaps.›

abbreviation "is_root' == Pairing_Heap_List1_Analysis.is_root"
abbreviation "del_min' == Pairing_Heap_List1.del_min"
abbreviation "insert' == Pairing_Heap_List1.insert"
abbreviation "merge' == Pairing_Heap_List1.merge"
abbreviation "pass⇩1' == Pairing_Heap_List1.pass⇩1"
abbreviation "pass⇩2' == Pairing_Heap_List1.pass⇩2"
abbreviation "T⇩p⇩a⇩s⇩s⇩1' == Pairing_Heap_List1_Analysis.T_pass⇩1"
abbreviation "T⇩p⇩a⇩s⇩s⇩2' == Pairing_Heap_List1_Analysis.T_pass⇩2"

fun homs :: "'a heap list ⇒ 'a tree" where
"homs [] = Leaf" |
"homs (Hp x lhs # rhs) = Node (homs lhs) x (homs rhs)"

fun hom :: "'a heap ⇒ 'a tree" where
"hom heap.Empty = Leaf" |
"hom (Hp x hs) = (Node (homs hs) x Leaf)"

lemma homs_pass1': "no_Emptys hs ⟹ homs(pass⇩1' hs) = pass⇩1 (homs hs)"
apply(induction hs rule: Pairing_Heap_List1.pass⇩1.induct)
  subgoal for h1 h2
  apply(case_tac h1)
   apply simp
  apply(case_tac h2)
   apply (auto)
  done
 apply simp
subgoal for h
apply(case_tac h)
 apply (auto)
done
done

lemma hom_merge': "⟦ no_Emptys lhs; Pairing_Heap_List1_Analysis.is_root h⟧
       ⟹ hom (merge' (Hp x lhs) h) = link ⟨homs lhs, x, hom h⟩"
by(cases h) auto

lemma hom_pass2': "no_Emptys hs ⟹ hom(pass⇩2' hs) = pass⇩2 (homs hs)"
by(induction hs rule: homs.induct) (auto simp: hom_merge' is_root_pass2)

lemma del_min': "is_root' h ⟹ hom(del_min' h) = del_min (hom h)"
by(cases h)
  (auto simp: homs_pass1' hom_pass2' no_Emptys_pass1 is_root_pass2)

lemma insert': "is_root' h ⟹ hom(insert' x h) = insert x (hom h)"
by(cases h)(auto)

lemma merge':
  "⟦ is_root' h1; is_root' h2 ⟧ ⟹ hom(merge' h1 h2) = merge (hom h1) (hom h2)"
apply(cases h1)
 apply(simp)
apply(cases h2)
 apply(auto)
done

lemma T_pass1': "no_Emptys hs ⟹ T⇩p⇩a⇩s⇩s⇩1' hs = T_pass⇩1(homs hs)"
apply(induction hs rule: Pairing_Heap_List1.pass⇩1.induct)
  subgoal for h1 h2
  apply(case_tac h1)
   apply simp
  apply(case_tac h2)
   apply (auto)
  done
 apply simp
subgoal for h
apply(case_tac h)
 apply (auto)
done
done

lemma T_pass2': "no_Emptys hs ⟹ T⇩p⇩a⇩s⇩s⇩2' hs = T_pass⇩2(homs hs)"
by(induction hs rule: homs.induct) (auto simp: hom_merge' is_root_pass2)

lemma size_hp: "is_root' h ⟹ size_hp h = size (hom h)"
proof(induction h)
  case (Hp _ hs) thus ?case
    apply(induction hs rule: homs.induct)
      apply simp
     apply force
    apply simp
    done
qed simp

interpretation Amortized2
where arity = arity and exec = exec and inv = is_root
and cost = cost and Φ = Φ and U = U
and hom = hom
and exec' = Pairing_Heap_List1_Analysis.exec
and cost' = Pairing_Heap_List1_Analysis.cost and inv' = "is_root'"
and U' = Pairing_Heap_List1_Analysis.U
proof (standard, goal_cases)
  case (1 _ f) thus ?case
    by (cases f)(auto simp: merge' del_min' numeral_eq_Suc)
next
  case (2 ts f)
  show ?case
  proof(cases f)
    case [simp]: Del_min
    then obtain h where [simp]: "ts = [h]" using 2 by auto
    show ?thesis using 2
      by(cases h) (auto simp: is_root_pass2 no_Emptys_pass1)
  qed (insert 2,
      auto simp: Pairing_Heap_List1_Analysis.is_root_merge numeral_eq_Suc)
next
  case (3 t) thus ?case by (cases t) (auto)
next
  case (4 ts f) show ?case
  proof (cases f)
    case [simp]: Del_min
    then obtain h where "ts = [h]" using 4 by auto
    thus ?thesis using 4
      by (cases h)(auto simp: T_pass1' T_pass2' no_Emptys_pass1 homs_pass1')
  next
    case [simp]: Merge
    then obtain h1 h2 where "ts = [h1, h2]" using 4 by (auto simp: numeral_2_eq_2)
    thus ?thesis by (simp)
  qed (insert 4, auto)
next
  case (5 _ f) thus ?case by(cases f) (auto simp: size_hp numeral_eq_Suc)
qed

end