text:
(*
  Title:     HOL/ex/Triangular_Numbers.thy
  Author:    Manuel Eberl, TU München
*)
section \<open>Triangular Numbers\<close>
theory Triangular_Numbers
  imports Complex_Main
begin

definition triangle_num :: "nat \<Rightarrow> nat" where
  "triangle_num n = (n * (n + 1)) div 2"

lemma real_triangle_num:
  "real (triangle_num n) = real n * (real n + 1) / 2"
  by (simp add: triangle_num_def field_char_0_class.of_nat_div algebra_simps)

lemma triangle_num_altdef: "triangle_num n = (\<Sum>k\<le>n. k)"
  by (induction n) (auto simp: triangle_num_def)

lemma triangle_num_ge: "triangle_num n \<ge> n"
  unfolding triangle_num_altdef by (rule member_le_sum) auto

lemma triangle_num_Suc: "triangle_num (Suc n) = triangle_num n + Suc n"
  by (simp add: triangle_num_altdef)

lemma triangle_num_0 [simp]: "triangle_num 0 = 0"
  and triangle_num_1 [simp]: "triangle_num 1 = 1"
  by (simp_all add: triangle_num_def)

lemma triangle_num_numeral [simp]:
  "triangle_num (numeral n) = fst (divmod (n * Num.inc n) (Num.Bit0 Num.One))"
  unfolding fst_divmod numeral_mult numeral_inc triangle_num_def ..

lemma triangle_num_eq_0_iff [simp]: "triangle_num n = 0 \<longleftrightarrow> n = 0"
  using triangle_num_ge[of n] by auto

lemma triangle_num_gt_0_iff [simp]: "triangle_num n > 0 \<longleftrightarrow> n > 0"
  using triangle_num_eq_0_iff[of n] by linarith

lemma strict_mono_triangle_num: "strict_mono triangle_num"
  unfolding strict_mono_Suc_iff by (auto simp: triangle_num_altdef)

lemma triangle_num_le: "m \<le> n \<Longrightarrow> triangle_num m \<le> triangle_num n"
  using strict_mono_leD[OF strict_mono_triangle_num] .

lemma triangle_num_less: "m < n \<Longrightarrow> triangle_num m < triangle_num n"
  using strict_monoD[OF strict_mono_triangle_num] .

lemma triangle_num_less_iff: "triangle_num m < triangle_num n \<longleftrightarrow> m < n"
  using strict_mono_less[OF strict_mono_triangle_num] .

lemma triangle_num_le_iff: "triangle_num m \<le> triangle_num n \<longleftrightarrow> m \<le> n"
  using strict_mono_less_eq[OF strict_mono_triangle_num] .

lemma triangle_num_eq_iff: "triangle_num m = triangle_num n \<longleftrightarrow> m = n"
  using strict_mono_eq[OF strict_mono_triangle_num] .

theorem inverse_triangle_num_sums: "(\<lambda>n. 1 / triangle_num (Suc n)) sums 2"
proof -
  have "(\<lambda>n. inverse (real (Suc n)) - inverse (real (Suc (Suc n)))) sums
          (inverse (real (Suc 0)) - 0)"
    by (intro telescope_sums' LIMSEQ_inverse_real_of_nat)
  also have "(\<lambda>n. inverse (real (Suc n)) - inverse (real (Suc (Suc n)))) =
               (\<lambda>n. 1 / real (2 * triangle_num (Suc n)))"
    by (auto simp: field_simps triangle_num_def)
  also have "inverse (real (Suc 0)) - 0 = 1"
    by simp
  finally have "(\<lambda>n. 2 * (1 / real (2 * triangle_num (Suc n)))) sums (2 * 1)"
    by (intro sums_mult)
  thus ?thesis by simp
qed

end


text:
theory IHT_Splay_Tree
  imports
    IHT_Tree
    Amortized_Complexity.Splay_Tree_Analysis
    "../Asymptotics/Asymptotics_1D"
begin

definition rotate_rr :: "'a::heap ptree \<Rightarrow> 'a ptree Heap" where
  "rotate_rr p = do {
    p' \<leftarrow> rotate_r p;
    rotate_r p'
   }"

lemma rotate_rr_rule [hoare_triple]:
  "<btree \<langle>\<langle>\<langle>A1, a', A2\<rangle>, a, B\<rangle>, b, CD\<rangle> p * $10>
    rotate_rr p
   <btree \<langle>A1, a', \<langle>A2, a, \<langle>B, b, CD\<rangle>\<rangle>\<rangle>>" by auto2

definition rotate_lr :: "'a::heap ptree \<Rightarrow> 'a ptree Heap" where
  "rotate_lr p = (case p of
     None \<Rightarrow> raise ''Empty ptree''
   | Some pp \<Rightarrow> do {
       t \<leftarrow> !pp;
       lp' \<leftarrow> rotate_l (lsub t);
       pp := Node lp' (val t) (rsub t);
       rotate_r p
     })"

lemma rotate_lr_rule [hoare_triple]:
  "<btree \<langle>\<langle>A, a, \<langle>B1, b', B2\<rangle>\<rangle>, b, CD\<rangle> p * $12>
    rotate_lr p
   <btree \<langle>\<langle>A, a, B1\<rangle>, b', \<langle>B2, b, CD\<rangle>\<rangle>>" by auto2

definition rotate_rl :: "'a::heap ptree \<Rightarrow> 'a ptree Heap" where
  "rotate_rl p = (case p of
     None \<Rightarrow> raise ''Empty ptree''
   | Some pp \<Rightarrow> do {
       t \<leftarrow> !pp;
       rp' \<leftarrow> rotate_r (rsub t);
       pp := Node (lsub t) (val t) rp';
       rotate_l p
     })"

lemma rotate_rl_rule [hoare_triple]:
  "<btree \<langle>AB, b, \<langle>\<langle>C1, c', C2\<rangle>, c, D\<rangle>\<rangle> p * $12>
    rotate_rl p
   <btree \<langle>\<langle>AB, b, C1\<rangle>, c', \<langle>C2, c, D\<rangle>\<rangle>>" by auto2

definition rotate_ll :: "'a::heap ptree \<Rightarrow> 'a ptree Heap" where
  "rotate_ll p = do {
    p' \<leftarrow> rotate_l p;
    rotate_l p'
  }"

lemma rotate_ll_rule [hoare_triple]:
  "<btree \<langle>A1, a', \<langle>A2, a, \<langle>B, b, CD\<rangle>\<rangle>\<rangle> p * $10>
    rotate_ll p
   <btree \<langle>\<langle>\<langle>A1, a', A2\<rangle>, a, B\<rangle>, b, CD\<rangle>>" by auto2

partial_function (heap_time) splay_impl :: "'a::{heap,linorder} \<Rightarrow> 'a ptree \<Rightarrow> 'a ptree Heap" where
  "splay_impl x p = (case p of
     None \<Rightarrow> return None
   | Some pp \<Rightarrow> do {
      t \<leftarrow> !pp;
      if x = val t then return p
      else if x < val t then (case lsub t of
         None \<Rightarrow> return p
       | Some lp \<Rightarrow> do {
           lt \<leftarrow> !lp;
           if x = val lt then rotate_r p
           else if x < val lt then (case lsub lt of
              None \<Rightarrow> rotate_r p
            | Some llp \<Rightarrow> do {
               llp' \<leftarrow> splay_impl x (lsub lt);
               lp := Node llp' (val lt) (rsub lt);
               rotate_rr p })
           else (case rsub lt of
              None \<Rightarrow> rotate_r p
            | Some rlp \<Rightarrow> do {
               rlp' \<leftarrow> splay_impl x (rsub lt);
               lp := Node (lsub lt) (val lt) rlp';
               rotate_lr p })})
      else (case rsub t of
         None \<Rightarrow> return p
       | Some rp \<Rightarrow> do {
           rt \<leftarrow> !rp;
           if x = val rt then rotate_l p
           else if x < val rt then (case lsub rt of
              None \<Rightarrow> rotate_l p
            | Some lrp \<Rightarrow> do {
               lrp' \<leftarrow> splay_impl x (lsub rt);
               rp := Node lrp' (val rt) (rsub rt);
               rotate_rl p })
           else (case rsub rt of
              None \<Rightarrow> rotate_l p
            | Some rrp \<Rightarrow> do {
               rrp' \<leftarrow> splay_impl x (rsub rt);
               rp := Node (lsub rt) (val rt) rrp';
               rotate_ll p })}) })"

declare splay.simps(1) [rewrite]

lemma splay_code': "splay x (Tree.Node AB b CD) =
  (if x=b
   then Tree.Node AB b CD
   else if x < b
        then case AB of
          Leaf \<Rightarrow> Tree.Node AB b CD |
          Tree.Node A a B \<Rightarrow>
            (if x=a then Tree.Node A a (Tree.Node B b CD)
             else if x < a
                  then if A = Leaf then Tree.Node A a (Tree.Node B b CD)
                       else case splay x A of
                         Tree.Node A\<^sub>1 a' A\<^sub>2 \<Rightarrow> Tree.Node A\<^sub>1 a' (Tree.Node A\<^sub>2 a (Tree.Node B b CD))
                  else if B = Leaf then Tree.Node A a (Tree.Node B b CD)
                       else case splay x B of
                         Tree.Node B\<^sub>1 b' B\<^sub>2 \<Rightarrow> Tree.Node (Tree.Node A a B\<^sub>1) b' (Tree.Node B\<^sub>2 b CD))
        else case CD of
          Leaf \<Rightarrow> Tree.Node AB b CD |
          Tree.Node C c D \<Rightarrow>
            (if x=c then Tree.Node (Tree.Node AB b C) c D
             else if x < c
                  then if C = Leaf then Tree.Node (Tree.Node AB b C) c D
                       else case splay x C of
                         Tree.Node C\<^sub>1 c' C\<^sub>2 \<Rightarrow> Tree.Node (Tree.Node AB b C\<^sub>1) c' (Tree.Node C\<^sub>2 c D)
                  else if D=Leaf then Tree.Node (Tree.Node AB b C) c D
                       else case splay x D of
                         Tree.Node D\<^sub>1 d D\<^sub>2 \<Rightarrow> Tree.Node (Tree.Node (Tree.Node AB b C) c D\<^sub>1) d D\<^sub>2))"
  by(auto split!: tree.split)

declare splay_code' [rewrite]

definition splay_time :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> nat" where
  "splay_time a t = 15 * T_splay a t"

lemma splay_time_simp:
  "splay_time a Leaf = 15"
  "splay_time a \<langle>l, b, r\<rangle> =
    (if a = b then 15
     else if a < b then case l of
        Leaf \<Rightarrow> 15
      | \<langle>ll, c, lr\<rangle> \<Rightarrow>
        (if a = c then 15
         else if a < c then if ll = Leaf then 15 else splay_time a ll + 15
              else if lr = Leaf then 15 else splay_time a lr + 15)
     else case r of
        Leaf \<Rightarrow> 15
      | \<langle>rl, c, rr\<rangle> \<Rightarrow>
         (if a = c then 15
          else if a < c then if rl = Leaf then 15 else splay_time a rl + 15
               else if rr = Leaf then 15 else splay_time a rr + 15))"
  by (auto split!: tree.split simp: splay_time_def)
declare splay_time_simp [rewrite]
setup \<open>add_fun_induct_rule (@{term_pat splay}, @{thm T_splay.induct[simplified LT EQ GT]})\<close>

lemma splay_not_Leaf: "splay x \<langle>l, a, r\<rangle> \<noteq> Leaf" by auto
setup \<open>add_forward_prfstep_cond @{thm splay_not_Leaf} [with_term "splay ?x \<langle>?l, ?a, ?r\<rangle>"]\<close>

lemma splay_correct [hoare_triple]:
  "<btree t a * $(splay_time x t)>
    splay_impl x a
   <btree (splay x t)>\<^sub>t"
@proof @fun_induct "splay x t" arbitrary a @with
  @subgoal "(x = x, t = \<langle>lt, b, rt\<rangle>)"
    @case "x = b"
    @case "x < b" @with
      @case "lt = Leaf"
    @end
    @case "x > b" @with
      @case "rt = Leaf"
    @end
  @endgoal @end
@qed

definition tree_constr_gen :: "'a::heap ptree \<Rightarrow> 'a \<Rightarrow> 'a ptree \<Rightarrow> 'a ptree Heap" where
  "tree_constr_gen lp v rp = do {
     p \<leftarrow> ref (Node lp v rp);
     return (Some p)
   }"

lemma tree_constr_gen_rule [hoare_triple]:
  "<btree lt lp * btree rt rp * $2>
    tree_constr_gen lp v rp
   <btree \<langle>lt, v, rt\<rangle>>" by auto2

definition insert_impl :: "'a::{heap,linorder} \<Rightarrow> 'a ptree \<Rightarrow> 'a ptree Heap" where
  "insert_impl x p = (case p of
     None \<Rightarrow> tree_constr x
   | _ \<Rightarrow> do {
      p' \<leftarrow> splay_impl x p;
      (case p' of
        None \<Rightarrow> raise ''splay_insert''
      | Some pp' \<Rightarrow> do {
          t' \<leftarrow> !pp';
          case cmp x (val t') of
            EQ \<Rightarrow> return p'
          | LT \<Rightarrow> do {
              pp' := Node None (val t') (rsub t');
              tree_constr_gen (lsub t') x p'
            }
          | GT \<Rightarrow> do {
              pp' := Node (lsub t') (val t') None;
              tree_constr_gen p' x (rsub t')
            }})})"

definition insert_time :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> nat" where [rewrite]:
  "insert_time x t = 15 * T_insert x t + 4"

lemma insert_time_simps:
  "insert_time a t = 15 + (if t = Leaf then 4 else splay_time a t + 4)"
  by (auto split!: tree.split simp add: splay_time_def insert_time_def  T_insert_def)

lemma aa2 [backward]:
  assumes "True" (* TODO: fix this *)
  shows
 "insert_time a t \<ge> (if t = Leaf then 4 else splay_time a t + 4)"
  unfolding insert_time_simps by simp

setup \<open>add_rewrite_rule @{thm Splay_Tree.insert.simps}\<close>
setup \<open>fold add_rewrite_rule @{thms cmp_val.case}\<close>
setup \<open>add_cases_rule @{thm cmp_val.induct}\<close>

lemma insert_correct [hoare_triple]:
  "<btree t a * $(insert_time x t)>
    insert_impl x a
   <btree (insert x t)>\<^sub>t"
@proof
  @have "insert_time x t \<ge>\<^sub>t (if t = Leaf then 4 else splay_time x t + 4)"
  @case "t = Leaf"
  @let "V = cmp x (value (splay x t))"
  @cases V
@qed

partial_function (heap_time) splay_max_impl :: "'a::{heap,linorder} ptree \<Rightarrow> 'a ptree Heap" where
  "splay_max_impl p = (case p of
     None \<Rightarrow> return None
   | Some pp \<Rightarrow> do {
      t \<leftarrow> !pp;
      case rsub t of
        None \<Rightarrow> return p
      | Some rp \<Rightarrow> do {
          rt \<leftarrow> !rp;
          if rsub rt = None then rotate_l p
          else do {
            rrp' \<leftarrow> splay_max_impl (rsub rt);
            case rrp' of
              None \<Rightarrow> raise ''splay_max_impl''
            | Some rrt \<Rightarrow> do {
                rp := Node (lsub rt) (val rt) rrp';
                rotate_ll p }}}})"

definition splay_max_time :: "'a::linorder tree \<Rightarrow> nat" where
  "splay_max_time t = 15 * T_splay_max t"

lemma splay_max_time_simps [rewrite]:
  "splay_max_time Leaf = 15"
  "splay_max_time \<langle>l, b, Leaf\<rangle> = 15"
  "splay_max_time \<langle>l, b, \<langle>rl, c, rr\<rangle>\<rangle> = (if rr=Leaf then 15 else splay_max_time rr + 15)"
  by (simp add: splay_max_time_def)+

setup \<open>fold add_rewrite_rule @{thms splay_max.simps}\<close>

lemma splay_max_not_Leaf: "splay_max \<langle>l, a, r\<rangle> \<noteq> Leaf" by auto
setup \<open>add_forward_prfstep_cond @{thm splay_max_not_Leaf} [with_term "splay_max \<langle>?l, ?a, ?r\<rangle>"]\<close>

lemma splay_max_correct [hoare_triple]:
  "<btree t a * $(splay_max_time t)>
    splay_max_impl a
   <btree (splay_max t)>\<^sub>t"
@proof @fun_induct "splay_max t" arbitrary a @qed

definition delete_impl :: "'a::{heap,linorder} \<Rightarrow> 'a ptree \<Rightarrow> 'a ptree Heap" where
  "delete_impl x p = (case p of
     None \<Rightarrow> return None
   | Some _ \<Rightarrow> do {
       p' \<leftarrow> splay_impl x p;
       case p' of
         None \<Rightarrow> raise ''delete_impl''
       | Some pp' \<Rightarrow> do {
           t' \<leftarrow> !pp';
           if x = val t' then
              if lsub t' = None then return (rsub t')
              else do {
                lp' \<leftarrow> splay_max_impl (lsub t');
                (case lp' of
                    None \<Rightarrow> raise ''delete_impl''
                  | Some lpp' \<Rightarrow> do {
                      lt' \<leftarrow> !lpp';
                      pp' := Node (lsub lt') (val lt') (rsub t');
                      return p' })}
           else return p' }})"

definition delete_time :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> nat" where
  "delete_time a t = 15 * T_delete a t + 5"

lemma delete_time_simps:
  "delete_time a t = 15 + (if t = Leaf then 5 else splay_time a t + (case splay a t of
    \<langle>l, x, r\<rangle> \<Rightarrow>
      if x=a then case l of Leaf \<Rightarrow> 5 | _ \<Rightarrow> splay_max_time l + 5
      else 5))"
  by (auto split!: tree.split simp: splay_time_def splay_max_time_def delete_time_def T_delete_def)

lemma aa [backward]:
  assumes "True" (* TODO: fix this *)
  shows
 "delete_time a t \<ge> (if t = Leaf then 5 else splay_time a t + (case splay a t of
    \<langle>l, x, r\<rangle> \<Rightarrow>
      if x=a then case l of Leaf \<Rightarrow> 5 | _ \<Rightarrow> splay_max_time l + 5
      else 5))"
  unfolding delete_time_simps by simp

setup \<open>add_rewrite_rule @{thm Splay_Tree.delete_def}\<close>

lemma splay_delete_correct [hoare_triple]:
  "<btree t a * $(delete_time x t)>
    delete_impl x a
   <btree (delete x t)>\<^sub>t"
@proof
  @have "delete_time x t \<ge>\<^sub>t (if t = Leaf then 5 else splay_time x t + (case splay x t of
    \<langle>l, xx, r\<rangle> \<Rightarrow>
      if xx=x then case l of Leaf \<Rightarrow> 5 | _ \<Rightarrow> splay_max_time l + 5
      else 5))"
  @case "t = Leaf"
  @case "x = value (splay x t)"
@qed

section \<open>Amortized analysis\<close>

definition splay_tree_P :: "'a tree \<Rightarrow> nat" where
  "splay_tree_P t = 15 * nat \<lceil>\<Phi> t\<rceil>"

definition splay_tree :: "'a::heap tree \<Rightarrow> 'a ptree \<Rightarrow> assn" where [rewrite_ent]:
  "splay_tree t a = btree t a * $(splay_tree_P t)"

lemma \<Phi>_nneg: "\<Phi> t \<ge> 0" by (induct t) auto

definition splay_atime :: "nat \<Rightarrow> nat" where
  "splay_atime n = 15 * nat (\<lceil>3 * log 2 n + 1\<rceil> + 1)"

lemma amor_transfer:
  assumes "real t + P a - P b \<le> c" and "c \<ge> 0" and "\<forall>x. P x \<ge> 0"
  shows "t + nat \<lceil>P a\<rceil> \<le> nat \<lceil>P b\<rceil> + nat (\<lceil>c\<rceil> + 1)" (is "?lhs \<le> ?rhs")
proof -
  have transfer': "real ?lhs \<le> real ?rhs"
  proof -
    have ineq1: "real t + \<lceil>P a\<rceil> - \<lceil>P b\<rceil> \<le> \<lceil>c\<rceil> + 1" using assms by linarith
    have ineq2: "\<forall>x. \<lceil>P x\<rceil> \<ge> 0" using assms by (smt zero_le_ceiling)
    show ?thesis using ineq1 ineq2 by (simp only: of_nat_add of_nat_nat assms)
  qed
  then show ?thesis
    using of_nat_le_iff by blast
qed

lemma a_splay [resolve]:
  assumes "bst t"
  shows "splay_time a t + splay_tree_P (splay a t) \<le> splay_tree_P t + splay_atime (size1 t)"
proof -
  have ineq1: "T_splay a t + nat (\<lceil>\<Phi> (splay a t)\<rceil>) \<le> nat (\<lceil>\<Phi> t\<rceil>) + nat (\<lceil>3 * log 2 (size1 t) + 1\<rceil> + 1)"
    apply (rule amor_transfer [of "T_splay a t" "\<Phi>"])
    apply (subst A_splay_def[symmetric])
    using assms by (rule A_splay_ub3) (simp add: \<Phi>_nneg)+
  then show ?thesis
    by (simp only: splay_tree_P_def splay_atime_def splay_time_def)
qed

lemma splay_tree_splay_amor [hoare_triple]:
  "bst t \<Longrightarrow>
   <splay_tree t a * $(splay_atime (size1 t))>
    splay_impl x a
   <splay_tree (splay x t)>\<^sub>t"
@proof
  @have "splay_tree_P t + splay_atime (size1 t) \<ge>\<^sub>t splay_time x t + splay_tree_P (splay x t)"
@qed

lemma splay_atime_alt: "\<forall>\<^sub>F x in sequentially. real (splay_atime x) = 30 + 15 * real (nat (\<lceil>3 * log 2 (real x)\<rceil>))"
  unfolding eventually_sequentially apply(rule exI[where x=1])
  apply (auto simp: splay_atime_def) apply(subst nat_add_distrib)
  apply auto apply(rule less_le_trans[of _ 0]) using log2_gt_zero by auto

lemma splay_atime_asym [asym_bound]:
  "(\<lambda>n. splay_atime n) \<in> \<Theta>(\<lambda>x. ln (real x))"
  apply(rule landau_theta.ev_eq_trans2[OF splay_atime_alt])
  using abcd_lnx[of 30 15 3 0] by auto

definition insert_atime :: "nat \<Rightarrow> nat" where
  "insert_atime n = 15 * nat (\<lceil>4 * log 2 n + 3\<rceil> + 1) + 4"

lemma a_insert [backward]:
  assumes "bst t"
  shows "insert_time x t + splay_tree_P (insert x t) \<le> splay_tree_P t + insert_atime (size1 t)"
proof -
  have ineq1: "T_insert x t + nat \<lceil>\<Phi> (insert x t)\<rceil> \<le> nat \<lceil>\<Phi> t\<rceil> + nat (\<lceil>4 * \<phi> t + 3\<rceil> + 1)"
    apply (rule amor_transfer [of "T_insert x t" "\<Phi>"])
    using assms by (rule amor_insert) (simp add: \<Phi>_nneg)+
  then show ?thesis
    by (simp only: insert_time_def splay_tree_P_def insert_atime_def splay_time_def)
qed

lemma insert_atime_alt: "\<forall>\<^sub>F x in sequentially. real (insert_atime x) = 64 + 15 * real (nat (\<lceil>4 * log 2 (real x)\<rceil>))"
  unfolding eventually_sequentially apply(rule exI[where x=1])
  apply (auto simp: insert_atime_def) apply(subst nat_add_distrib)
  apply auto apply(rule less_le_trans[of _ 0] ) using log2_gt_zero by auto

lemma insert_atime_asym [asym_bound]:
  "(\<lambda>n. insert_atime n) \<in> \<Theta>(\<lambda>x. ln (real x))"
  apply(rule landau_theta.ev_eq_trans2[OF insert_atime_alt])
  using abcd_lnx[of 64 15 4 0] by auto

lemma splay_tree_insert_amor [hoare_triple]:
  "bst t \<Longrightarrow>
   <splay_tree t a * $(insert_atime (size1 t))>
    insert_impl x a
   <splay_tree (insert x t)>\<^sub>t"
@proof
  @have "splay_tree_P t + insert_atime (size1 t) \<ge>\<^sub>t insert_time x t + splay_tree_P (insert x t)"
@qed

definition delete_atime :: "nat \<Rightarrow> nat" where
  "delete_atime n = 15 * nat (\<lceil>6 * log 2 n + 3\<rceil> + 1) + 5"

lemma a_delete [backward]:
  assumes "bst t"
  shows "delete_time x t + splay_tree_P (delete x t) \<le> splay_tree_P t + delete_atime (size1 t)"
proof -
  have ineq1: "T_delete x t + nat \<lceil>\<Phi> (delete x t)\<rceil> \<le> nat \<lceil>\<Phi> t\<rceil> + nat (\<lceil>6 * \<phi> t + 3\<rceil> + 1)"
    apply (rule amor_transfer [of "T_delete x t" "\<Phi>"])
    using assms by (rule amor_delete) (simp add: \<Phi>_nneg)+
  then show ?thesis
    by (simp only: delete_time_def splay_tree_P_def delete_atime_def)
qed

lemma delete_atime_alt: "\<forall>\<^sub>F x in sequentially. real (delete_atime x) = 65 + 15 * real (nat (\<lceil>6 * log 2 (real x)\<rceil>))"
  unfolding eventually_sequentially apply(rule exI[where x=1])
  apply (auto simp: delete_atime_def) apply(subst nat_add_distrib)
  apply auto apply(rule less_le_trans[of _ 0] ) using log2_gt_zero by auto

lemma delete_atime_asym [asym_bound]:
  "(\<lambda>n. delete_atime n) \<in> \<Theta>(\<lambda>x. ln (real x))"
  apply(rule landau_theta.ev_eq_trans2[OF delete_atime_alt])
  using abcd_lnx[of 65 15 6 0] by auto

lemma splay_tree_delete_amor [hoare_triple]:
  "bst t \<Longrightarrow>
   <splay_tree t a * $(delete_atime (size1 t))>
    delete_impl x a
   <splay_tree (delete x t)>\<^sub>t"
@proof
  @have "splay_tree_P t + delete_atime (size1 t) \<ge>\<^sub>t delete_time x t + splay_tree_P (delete x t)"
@qed

setup \<open>del_prfstep_thm @{thm splay_tree_def}\<close>

section \<open>Abstract assertion\<close>

definition splay_tree_set :: "'a::{heap,linorder} set \<Rightarrow> 'a ptree \<Rightarrow> assn" where [rewrite_ent]:
  "splay_tree_set S a = (\<exists>\<^sub>At. splay_tree t a * \<up>(bst t) * \<up>(set_tree t = S))"

lemma size_set_tree:
  "bst t \<Longrightarrow> card (set_tree t) = size t"
proof (induct t)
  case Leaf show ?case by simp
next
  case (Node t1 x2 t2)
  have "set_tree t1 \<inter> set_tree t2 = {}" using Node by fastforce
  then have size1: "card (set_tree t1 \<union> set_tree t2) = size t1 + size t2"
    using Node by (simp add: card_Un_disjoint)
  have "x2 \<notin> set_tree t1 \<union> set_tree t2" using Node by fastforce
  then show ?case using size1 by auto
qed

lemma size1_set_tree [rewrite]:
  "bst t \<Longrightarrow> card (set_tree t) + 1 = size1 t"
  using size_set_tree by auto

(* some now commented-out proofs in Splay_Tree.Splay_Tree by Nipkow *)

lemma ST_set_splay: "set_tree(Splay_Tree.splay a t) = set_tree t"
proof(induction a t rule: splay.induct)
  case (6 a)
  with Splay_Tree.splay_not_Leaf[OF 6(3), of a] show ?case by(fastforce)
next
  case (8 _ a)
  with Splay_Tree.splay_not_Leaf[OF 8(3), of a] show ?case by(fastforce)
next
  case (11 _ a)
  with Splay_Tree.splay_not_Leaf[OF 11(3), of a] show ?case by(fastforce)
next
  case (14 _ a)
  with Splay_Tree.splay_not_Leaf[OF 14(3), of a] show ?case by(fastforce)
qed auto

lemma ST_set_insert: "set_tree(insert a t) = Set.insert a (set_tree t)"
  apply(cases t)
 apply simp
using ST_set_splay[of a t]
  by(simp split: tree.split) fastforce

lemma splay_max_Leaf: "splay_max t = Tree.Node l a r \<Longrightarrow> r = Leaf"
by(induction t arbitrary: l rule: splay_max.induct)
  (auto split: tree.splits if_splits)

lemma set_splay_max: "set_tree(splay_max t) = set_tree t"
apply(induction t rule: splay_max.induct)
   apply(simp)
  apply(simp)
apply(force split: tree.split)
done

lemma ST_set_delete: assumes "bst t"
shows "set_tree (Splay_Tree.delete a t) = set_tree t - {a}"
proof(cases t)
  case Leaf thus ?thesis by(simp add: delete_def)
next
  case (Node l x r)
  obtain l' x' r' where sp[simp]: "splay a (Tree.Node l x r) = Tree.Node l' x' r'"
    by (metis neq_Leaf_iff splay_Leaf_iff)
  show ?thesis
  proof cases
    assume [simp]: "x' = a"
    show ?thesis
    proof cases
      assume "l' = Leaf"
      thus ?thesis
        using Node assms ST_set_splay[of a "Tree.Node l x r"] bst_splay[of "Tree.Node l x r" a]
        by(simp add: delete_def split: tree.split prod.split)(fastforce)
    next
      assume "l' \<noteq> Leaf"
      moreover then obtain l'' m r'' where "splay_max l' = Tree.Node l'' m r''"
        using splay_max_Leaf_iff tree.exhaust by blast
      moreover have "a \<notin> set_tree l'"
        by (metis (no_types) Node assms less_irrefl sp splay_bstL)
      ultimately show ?thesis
        using Node assms ST_set_splay[of a "Tree.Node l x r"] bst_splay[of "Tree.Node l x r" a]
          splay_max_Leaf[of l' l'' m r''] set_splay_max[of l']
        by(clarsimp simp: delete_def split: tree.split) auto
    qed
  next
    assume "x' \<noteq> a"
    thus ?thesis using Node assms ST_set_splay[of a "Tree.Node l x r"] splay_to_root[OF _ sp]
      by (simp add: delete_def)
  qed
qed

lemma bst_splay_max: "bst t \<Longrightarrow> bst (splay_max t)"
proof(induction t rule: splay_max.induct)
  case (3 l b rl c rr)
  { fix rrl' d' rrr'
    have "splay_max rr = Tree.Node rrl' d' rrr'
       \<Longrightarrow> \<forall>x \<in> set_tree(Tree.Node rrl' d' rrr'). c < x"
      using "3.prems" set_splay_max[of rr]
      by (clarsimp split: tree.split simp: ball_Un)
  }
  with 3 show ?case by (fastforce split: tree.split simp: ball_Un)
qed auto

lemma bst_delete: assumes "bst t" shows "bst (delete a t)"
  proof(cases t)
  case Leaf thus ?thesis by(simp add: delete_def)
next
  case (Node l x r)
  obtain l' x' r' where sp[simp]: "splay a (Tree.Node l x r) = Tree.Node l' x' r'"
    by (metis neq_Leaf_iff splay_Leaf_iff)
  show ?thesis
  proof cases
    assume [simp]: "x' = a"
    show ?thesis
    proof cases
      assume "l' = Leaf"
      thus ?thesis using Node assms bst_splay[of "Tree.Node l x r" a]
        by(simp add: delete_def split: tree.split prod.split)
    next
      assume "l' \<noteq> Leaf"
      thus ?thesis
        using Node assms ST_set_splay[of a "Tree.Node l x r"] bst_splay[of "Tree.Node l x r" a]
          bst_splay_max[of l'] set_splay_max[of l']
        by(clarsimp simp: delete_def split: tree.split)
          (metis (no_types) insertI1 less_trans)
    qed
  next
    assume "x' \<noteq> a"
    thus ?thesis using Node assms bst_splay[of "Tree.Node l x r" a]
      by(auto simp: delete_def split: tree.split prod.split)
  qed
qed

setup \<open>add_forward_prfstep_cond @{thm bst_splay} [with_term "splay ?x ?t"]\<close>
setup \<open>add_rewrite_rule @{thm ST_set_splay}\<close>

lemma splay_tree_splay_rule [hoare_triple]:
  "<splay_tree_set S a * $(splay_atime (card S + 1))>
    splay_impl x a
   <splay_tree_set S>\<^sub>t" by auto2

setup \<open>add_forward_prfstep_cond @{thm bst_insert} [with_term "Splay_Tree.insert ?x ?t"]\<close>
setup \<open>add_rewrite_rule @{thm ST_set_insert}\<close>

lemma splay_tree_insert_rule [hoare_triple]:
  "<splay_tree_set S a * $(insert_atime (card S + 1))>
    insert_impl x a
   <splay_tree_set ({x} \<union> S)>\<^sub>t" by auto2

setup \<open>add_forward_prfstep_cond @{thm bst_delete} [with_term "Splay_Tree.delete ?a ?t"]\<close>
setup \<open>add_rewrite_rule @{thm ST_set_delete}\<close>

lemma splay_tree_delete_rule [hoare_triple]:
  "<splay_tree_set S a * $(delete_atime (card S + 1))>
    delete_impl x a
   <splay_tree_set (S - {x})>\<^sub>t" by auto2

end

author: bzhan


text:
(*  Title:      ZF/Sum.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge
*)

section\<open>Disjoint Sums\<close>

theory Sum imports Bool equalities begin

text\<open>And the "Part" primitive for simultaneous recursive type definitions\<close>

definition sum :: "[i,i]=>i" (infixr \<open>+\<close> 65) where
     "A+B == {0}*A \<union> {1}*B"

definition Inl :: "i=>i" where
     "Inl(a) == <0,a>"

definition Inr :: "i=>i" where
     "Inr(b) == <1,b>"

definition "case" :: "[i=>i, i=>i, i]=>i" where
     "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"

  (*operator for selecting out the various summands*)
definition Part :: "[i,i=>i] => i" where
     "Part(A,h) == {x \<in> A. \<exists>z. x = h(z)}"

subsection\<open>Rules for the \<^term>\<open>Part\<close> Primitive\<close>

lemma Part_iff:
    "a \<in> Part(A,h) \<longleftrightarrow> a \<in> A & (\<exists>y. a=h(y))"
apply (unfold Part_def)
apply (rule separation)
done

lemma Part_eqI [intro]:
    "[| a \<in> A;  a=h(b) |] ==> a \<in> Part(A,h)"
by (unfold Part_def, blast)

lemmas PartI = refl [THEN [2] Part_eqI]

lemma PartE [elim!]:
    "[| a \<in> Part(A,h);  !!z. [| a \<in> A;  a=h(z) |] ==> P
     |] ==> P"
apply (unfold Part_def, blast)
done

lemma Part_subset: "Part(A,h) \<subseteq> A"
apply (unfold Part_def)
apply (rule Collect_subset)
done

subsection\<open>Rules for Disjoint Sums\<close>

lemmas sum_defs = sum_def Inl_def Inr_def case_def

lemma Sigma_bool: "Sigma(bool,C) = C(0) + C(1)"
by (unfold bool_def sum_def, blast)

(** Introduction rules for the injections **)

lemma InlI [intro!,simp,TC]: "a \<in> A ==> Inl(a) \<in> A+B"
by (unfold sum_defs, blast)

lemma InrI [intro!,simp,TC]: "b \<in> B ==> Inr(b) \<in> A+B"
by (unfold sum_defs, blast)

(** Elimination rules **)

lemma sumE [elim!]:
    "[| u \<in> A+B;
        !!x. [| x \<in> A;  u=Inl(x) |] ==> P;
        !!y. [| y \<in> B;  u=Inr(y) |] ==> P
     |] ==> P"
by (unfold sum_defs, blast)

(** Injection and freeness equivalences, for rewriting **)

lemma Inl_iff [iff]: "Inl(a)=Inl(b) \<longleftrightarrow> a=b"
by (simp add: sum_defs)

lemma Inr_iff [iff]: "Inr(a)=Inr(b) \<longleftrightarrow> a=b"
by (simp add: sum_defs)

lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) \<longleftrightarrow> False"
by (simp add: sum_defs)

lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) \<longleftrightarrow> False"
by (simp add: sum_defs)

lemma sum_empty [simp]: "0+0 = 0"
by (simp add: sum_defs)

(*Injection and freeness rules*)

lemmas Inl_inject = Inl_iff [THEN iffD1]
lemmas Inr_inject = Inr_iff [THEN iffD1]
lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!]
lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!]

lemma InlD: "Inl(a): A+B ==> a \<in> A"
by blast

lemma InrD: "Inr(b): A+B ==> b \<in> B"
by blast

lemma sum_iff: "u \<in> A+B \<longleftrightarrow> (\<exists>x. x \<in> A & u=Inl(x)) | (\<exists>y. y \<in> B & u=Inr(y))"
by blast

lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)"
by auto

lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)"
by auto

lemma sum_subset_iff: "A+B \<subseteq> C+D \<longleftrightarrow> A<=C & B<=D"
by blast

lemma sum_equal_iff: "A+B = C+D \<longleftrightarrow> A=C & B=D"
by (simp add: extension sum_subset_iff, blast)

lemma sum_eq_2_times: "A+A = 2*A"
by (simp add: sum_def, blast)

subsection\<open>The Eliminator: \<^term>\<open>case\<close>\<close>

lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)"
by (simp add: sum_defs)

lemma case_Inr [simp]: "case(c, d, Inr(b)) = d(b)"
by (simp add: sum_defs)

lemma case_type [TC]:
    "[| u \<in> A+B;
        !!x. x \<in> A ==> c(x): C(Inl(x));
        !!y. y \<in> B ==> d(y): C(Inr(y))
     |] ==> case(c,d,u) \<in> C(u)"
by auto

lemma expand_case: "u \<in> A+B ==>
        R(case(c,d,u)) \<longleftrightarrow>
        ((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) &
        (\<forall>y\<in>B. u = Inr(y) \<longrightarrow> R(d(y))))"
by auto

lemma case_cong:
  "[| z \<in> A+B;
      !!x. x \<in> A ==> c(x)=c'(x);
      !!y. y \<in> B ==> d(y)=d'(y)
   |] ==> case(c,d,z) = case(c',d',z)"
by auto

lemma case_case: "z \<in> A+B ==>
        case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) =
        case(%x. c(c'(x)), %y. d(d'(y)), z)"
by auto

subsection\<open>More Rules for \<^term>\<open>Part(A,h)\<close>\<close>

lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)"
by blast

lemma Part_Collect: "Part(Collect(A,P), h) = Collect(Part(A,h), P)"
by blast

lemmas Part_CollectE =
     Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE]

lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x \<in> A}"
by blast

lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y \<in> B}"
by blast

lemma PartD1: "a \<in> Part(A,h) ==> a \<in> A"
by (simp add: Part_def)

lemma Part_id: "Part(A,%x. x) = A"
by blast

lemma Part_Inr2: "Part(A+B, %x. Inr(h(x))) = {Inr(y). y \<in> Part(B,h)}"
by blast

lemma Part_sum_equality: "C \<subseteq> A+B ==> Part(C,Inl) \<union> Part(C,Inr) = C"
by blast

end

author: landonf

repo: isabelle-legacy