Theory Impl_RBT_Map

header {* \isaheader{Red-Black Tree based Maps} *}
theory Impl_RBT_Map
imports 
  "~~/src/HOL/Library/RBT_Impl"
  "../../Lib/RBT_add"
  "../../../Automatic_Refinement/Automatic_Refinement"
  "../../Iterator/Iterator"
  "../Intf/Intf_Comp"
  "../Intf/Intf_Map"
begin

(* TODO: Move to common/RBT_add (replace) *)

subsection {* Standard Setup *}

  inductive_set color_rel where
    "(color.R,color.R) ∈ color_rel"
   | "(color.B,color.B) ∈ color_rel"

  inductive_cases color_rel_elims:
    "(x,color.R) ∈ color_rel"
    "(x,color.B) ∈ color_rel"
    "(color.R,y) ∈ color_rel"
    "(color.B,y) ∈ color_rel"

  thm color_rel_elims

  lemma param_color[param]:
    "(color.R,color.R)∈color_rel"
    "(color.B,color.B)∈color_rel"
    "(case_color,case_color)∈R -> R -> color_rel -> R"
    by (auto 
      intro: color_rel.intros
      elim: color_rel.cases
      split: color.split)

  inductive_set rbt_rel_aux for Ra Rb where
    "(rbt.Empty,rbt.Empty)∈rbt_rel_aux Ra Rb"
  | "[| (c,c')∈color_rel; 
       (l,l')∈rbt_rel_aux Ra Rb; (a,a')∈Ra; (b,b')∈Rb; 
       (r,r')∈rbt_rel_aux Ra Rb |]
    ==> (rbt.Branch c l a b r, rbt.Branch c' l' a' b' r')∈rbt_rel_aux Ra Rb"

  inductive_cases rbt_rel_aux_elims:  (* Argh! This seems to use 
    the default simpset to simplify the result. If relators are in this 
    simpset, we get an undesired result! *)
    "(x,rbt.Empty)∈rbt_rel_aux Ra Rb"
    "(rbt.Empty,x')∈rbt_rel_aux Ra Rb"
    "(rbt.Branch c l a b r,x')∈rbt_rel_aux Ra Rb"
    "(x,rbt.Branch c' l' a' b' r')∈rbt_rel_aux Ra Rb"

  definition "rbt_rel ≡ rbt_rel_aux"
  lemma rbt_rel_aux_fold: "rbt_rel_aux Ra Rb ≡ ⟨Ra,Rb⟩rbt_rel"
    by (simp add: rbt_rel_def relAPP_def)

  lemmas rbt_rel_intros = rbt_rel_aux.intros[unfolded rbt_rel_aux_fold]
  lemmas rbt_rel_cases = rbt_rel_aux.cases[unfolded rbt_rel_aux_fold]
  lemmas rbt_rel_induct[induct set] 
    = rbt_rel_aux.induct[unfolded rbt_rel_aux_fold]
  lemmas rbt_rel_elims = rbt_rel_aux_elims[unfolded rbt_rel_aux_fold]

  lemma param_rbt1[param]: 
    "(rbt.Empty,rbt.Empty) ∈ ⟨Ra,Rb⟩rbt_rel"
    "(rbt.Branch,rbt.Branch) ∈ 
      color_rel -> ⟨Ra,Rb⟩rbt_rel -> Ra -> Rb -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
    by (auto intro: rbt_rel_intros)

  lemma param_case_rbt[param]:
    "(case_rbt,case_rbt) ∈ 
      Ra -> (color_rel -> ⟨Rb,Rc⟩rbt_rel -> Rb -> Rc -> ⟨Rb,Rc⟩rbt_rel -> Ra) 
        -> ⟨Rb,Rc⟩rbt_rel -> Ra"
    apply clarsimp
    apply (erule rbt_rel_cases)
    apply simp
    apply simp
    apply parametricity
    done

  lemma param_rec_rbt[param]: "(rec_rbt, rec_rbt) ∈ 
    Ra -> (color_rel -> ⟨Rb,Rc⟩rbt_rel -> Rb -> Rc -> ⟨Rb,Rc⟩rbt_rel
     -> Ra -> Ra -> Ra) -> ⟨Rb,Rc⟩rbt_rel -> Ra"
  proof (intro fun_relI)
    case (goal1 s s' f f' t t') from goal1(3,1,2) show ?case
      apply (induct arbitrary: s s')
      apply simp
      apply simp
      apply parametricity
      done
  qed

  lemma param_paint[param]: 
    "(paint,paint)∈color_rel -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
    unfolding paint_def
    by parametricity

  lemma param_balance[param]: 
    shows "(balance,balance) ∈ 
      ⟨Ra,Rb⟩rbt_rel -> Ra -> Rb -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
  proof (intro fun_relI)
    case (goal1 t1 t1' a a' b b' t2 t2')
    thus ?case
      apply (induct t1' a' b' t2' arbitrary: t1 a b t2 rule: balance.induct)
      apply (elim_all rbt_rel_elims color_rel_elims)
      apply (simp_all only: balance.simps)
      apply (parametricity)+
      done
  qed


  lemma param_rbt_ins[param]:
    fixes less
    assumes param_less[param]: "(less,less') ∈ Ra -> Ra -> Id"
    shows "(ord.rbt_ins less,ord.rbt_ins less') ∈ 
             (Ra->Rb->Rb->Rb) -> Ra -> Rb -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
  proof (intro fun_relI)
    case (goal1 f f' a a' b b' t t')
    thus ?case
      apply (induct f' a' b' t' arbitrary: f a b t rule: ord.rbt_ins.induct)
      apply (elim_all rbt_rel_elims color_rel_elims)
      apply (simp_all only: ord.rbt_ins.simps rbt_ins.simps)
      apply parametricity+
      done
  qed

  term rbt_insert
  lemma param_rbt_insert[param]:
    fixes less
    assumes param_less[param]: "(less,less') ∈ Ra -> Ra -> Id"
    shows "(ord.rbt_insert less,ord.rbt_insert less') ∈ 
      Ra -> Rb -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
    unfolding rbt_insert_def ord.rbt_insert_def
    unfolding rbt_insert_with_key_def[abs_def] 
      ord.rbt_insert_with_key_def[abs_def] 
    by parametricity

  lemma param_rbt_lookup[param]:
    fixes less
    assumes param_less[param]: "(less,less') ∈ Ra -> Ra -> Id"
    shows "(ord.rbt_lookup less,ord.rbt_lookup less') ∈ 
             ⟨Ra,Rb⟩rbt_rel -> Ra -> ⟨Rb⟩option_rel"
    unfolding rbt_lookup_def ord.rbt_lookup_def
    by parametricity

  term balance_left
  lemma param_balance_left[param]: 
    "(balance_left, balance_left) ∈ 
      ⟨Ra,Rb⟩rbt_rel -> Ra -> Rb -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
  proof (intro fun_relI)
    case (goal1 l l' a a' b b' r r')
    thus ?case
      apply (induct l a b r arbitrary: l' a' b' r' rule: balance_left.induct)
      apply (elim_all rbt_rel_elims color_rel_elims)
      apply (simp_all only: balance_left.simps)
      apply parametricity+
      done
  qed

  term balance_right
  lemma param_balance_right[param]: 
    "(balance_right, balance_right) ∈ 
      ⟨Ra,Rb⟩rbt_rel -> Ra -> Rb -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
  proof (intro fun_relI)
    case (goal1 l l' a a' b b' r r')
    thus ?case
      apply (induct l a b r arbitrary: l' a' b' r' rule: balance_right.induct)
      apply (elim_all rbt_rel_elims color_rel_elims)
      apply (simp_all only: balance_right.simps)
      apply parametricity+
      done
  qed

  lemma param_combine[param]:
    "(combine,combine)∈⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
  proof (intro fun_relI)
    case (goal1 t1 t1' t2 t2')
    thus ?case
      apply (induct t1 t2 arbitrary: t1' t2' rule: combine.induct)
      apply (elim_all rbt_rel_elims color_rel_elims)
      apply (simp_all only: combine.simps)
      apply parametricity+
      done
  qed

  lemma ih_aux1: "[| (a',b)∈R; a'=a |] ==> (a,b)∈R" by auto
  lemma is_eq: "a=b ==> a=b" .

  lemma param_rbt_del_aux:
    fixes br
    fixes less
    assumes param_less[param]: "(less,less') ∈ Ra -> Ra -> Id"
    shows
    "[| (ak1,ak1')∈Ra; (al,al')∈⟨Ra,Rb⟩rbt_rel; (ak,ak')∈Ra;
      (av,av')∈Rb; (ar,ar')∈⟨Ra,Rb⟩rbt_rel 
    |] ==> (ord.rbt_del_from_left less ak1 al ak av ar, 
      ord.rbt_del_from_left less' ak1' al' ak' av' ar') 
    ∈ ⟨Ra,Rb⟩rbt_rel"
    "[| (bk1,bk1')∈Ra; (bl,bl')∈⟨Ra,Rb⟩rbt_rel; (bk,bk')∈Ra;
      (bv,bv')∈Rb; (br,br')∈⟨Ra,Rb⟩rbt_rel 
    |] ==> (ord.rbt_del_from_right less bk1 bl bk bv br, 
      ord.rbt_del_from_right less' bk1' bl' bk' bv' br') 
    ∈ ⟨Ra,Rb⟩rbt_rel"
    "[| (ck,ck')∈Ra; (ct,ct')∈⟨Ra,Rb⟩rbt_rel |] 
      ==> (ord.rbt_del less ck ct, ord.rbt_del less' ck' ct') ∈ ⟨Ra,Rb⟩rbt_rel"
    apply (induct 
      ak1' al' ak' av' ar' and bk1' bl' bk' bv' br' and ck' ct'
      arbitrary: ak1 al ak av ar and bk1 bl bk bv br and ck ct
      rule: ord.rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
    (* TODO/FIXME: We do not have 'deep' elimination rules, thus
      we have to do some ughly hack to apply the rbt_rel-elimination inside
      the induction hypothesis. *)
    apply (assumption
      | elim rbt_rel_elims color_rel_elims 
      | simp (no_asm_use) only: rbt_del.simps ord.rbt_del.simps
          rbt_del_from_left.simps ord.rbt_del_from_left.simps
          rbt_del_from_right.simps ord.rbt_del_from_right.simps
      | parametricity
      | rule rbt_rel_intros
      | hypsubst
      | (simp, rule ih_aux1, rprems)
      | (rule is_eq, simp)
    ) +
    done

  lemma param_rbt_del[param]:
    fixes less
    assumes param_less: "(less,less') ∈ Ra -> Ra -> Id"
    shows
    "(ord.rbt_del_from_left less, ord.rbt_del_from_left less') ∈ 
      Ra -> ⟨Ra,Rb⟩rbt_rel -> Ra -> Rb -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
    "(ord.rbt_del_from_right less, ord.rbt_del_from_right less') ∈
      Ra -> ⟨Ra,Rb⟩rbt_rel -> Ra -> Rb -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
    "(ord.rbt_del less,ord.rbt_del less') ∈ 
      Ra -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
    by (intro fun_relI, blast intro: param_rbt_del_aux[OF param_less])+

  lemma param_rbt_delete[param]:
    fixes less
    assumes param_less[param]: "(less,less') ∈ Ra -> Ra -> Id"
    shows "(ord.rbt_delete less, ord.rbt_delete less') 
      ∈ Ra -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
    unfolding rbt_delete_def[abs_def] ord.rbt_delete_def[abs_def]
    by parametricity

  term ord.rbt_insert_with_key

  abbreviation compare_rel :: "(RBT_Impl.compare × _) set" 
    where "compare_rel ≡ Id"

  lemma param_compare[param]:
    "(RBT_Impl.LT,RBT_Impl.LT)∈compare_rel"
    "(RBT_Impl.GT,RBT_Impl.GT)∈compare_rel"
    "(RBT_Impl.EQ,RBT_Impl.EQ)∈compare_rel"
    "(RBT_Impl.case_compare,RBT_Impl.case_compare)∈R->R->R->compare_rel->R"
    by (auto split: RBT_Impl.compare.split)

  lemma param_rbtreeify_aux[param]:
    "[|n≤length kvs; (n,n')∈nat_rel; (kvs,kvs')∈⟨⟨Ra,Rb⟩prod_rel⟩list_rel|] 
    ==> (rbtreeify_f n kvs,rbtreeify_f n' kvs')
      ∈ ⟨⟨Ra,Rb⟩rbt_rel, ⟨⟨Ra,Rb⟩prod_rel⟩list_rel⟩prod_rel"
    "[|n≤Suc (length kvs); (n,n')∈nat_rel; (kvs,kvs')∈⟨⟨Ra,Rb⟩prod_rel⟩list_rel|]
    ==> (rbtreeify_g n kvs,rbtreeify_g n' kvs')
      ∈ ⟨⟨Ra,Rb⟩rbt_rel, ⟨⟨Ra,Rb⟩prod_rel⟩list_rel⟩prod_rel"
    apply (induct n kvs and n kvs 
      arbitrary: n' kvs' and n' kvs'
      rule: rbtreeify_induct)

    (* TODO: Still requires some manual proof! *)
    apply (simp only: pair_in_Id_conv)
    apply (simp (no_asm_use) only: rbtreeify_f_simps rbtreeify_g_simps)
    apply parametricity

    apply (elim list_relE prod_relE)
    apply (simp only: pair_in_Id_conv)
    apply hypsubst
    apply (simp (no_asm_use) only: rbtreeify_f_simps rbtreeify_g_simps)
    apply parametricity

    apply clarsimp
    apply (subgoal_tac "(rbtreeify_f n kvs, rbtreeify_f n kvs'a) 
      ∈ ⟨⟨Ra, Rb⟩rbt_rel, ⟨⟨Ra, Rb⟩prod_rel⟩list_rel⟩prod_rel")
    apply (clarsimp elim!: list_relE prod_relE)
    apply parametricity
    apply (rule refl)
    apply rprems
    apply (rule refl)
    apply assumption

    apply clarsimp
    apply (subgoal_tac "(rbtreeify_f n kvs, rbtreeify_f n kvs'a) 
      ∈ ⟨⟨Ra, Rb⟩rbt_rel, ⟨⟨Ra, Rb⟩prod_rel⟩list_rel⟩prod_rel")
    apply (clarsimp elim!: list_relE prod_relE)
    apply parametricity
    apply (rule refl)
    apply rprems
    apply (rule refl)
    apply assumption

    apply simp
    apply parametricity

    apply clarsimp
    apply parametricity

    apply clarsimp
    apply (subgoal_tac "(rbtreeify_g n kvs, rbtreeify_g n kvs'a) 
      ∈ ⟨⟨Ra, Rb⟩rbt_rel, ⟨⟨Ra, Rb⟩prod_rel⟩list_rel⟩prod_rel")
    apply (clarsimp elim!: list_relE prod_relE)
    apply parametricity
    apply (rule refl)
    apply parametricity
    apply (rule refl)

    apply clarsimp
    apply (subgoal_tac "(rbtreeify_f n kvs, rbtreeify_f n kvs'a) 
      ∈ ⟨⟨Ra, Rb⟩rbt_rel, ⟨⟨Ra, Rb⟩prod_rel⟩list_rel⟩prod_rel")
    apply (clarsimp elim!: list_relE prod_relE)
    apply parametricity
    apply (rule refl)
    apply parametricity
    apply (rule refl)
    done    

  lemma param_rbtreeify[param]:
    "(rbtreeify, rbtreeify) ∈ ⟨⟨Ra,Rb⟩prod_rel⟩list_rel -> ⟨Ra,Rb⟩rbt_rel"
    unfolding rbtreeify_def[abs_def]
    apply parametricity
    by simp

  lemma param_sunion_with[param]:
    fixes less
    shows "[| (less,less') ∈ Ra -> Ra -> Id; 
      (f,f')∈(Ra->Rb->Rb->Rb); (a,a')∈⟨⟨Ra,Rb⟩prod_rel⟩list_rel;
      (b,b')∈⟨⟨Ra,Rb⟩prod_rel⟩list_rel |] 
    ==> (ord.sunion_with less f a b, ord.sunion_with less' f' a' b') ∈ 
      ⟨⟨Ra,Rb⟩prod_rel⟩list_rel"
    apply (induct f' a' b' arbitrary: f a b 
      rule: ord.sunion_with.induct[of less'])
    apply (elim_all list_relE prod_relE)
    apply (simp_all only: ord.sunion_with.simps)
    apply parametricity
    apply simp_all
    done

  lemma skip_red_alt:
    "RBT_Impl.skip_red t = (case t of 
      (Branch color.R l k v r) => l
    | _ => t)"
    by (auto split: rbt.split color.split)

  function compare_height :: 
    "('a, 'b) RBT_Impl.rbt => ('a, 'b) RBT_Impl.rbt => ('a, 'b) RBT_Impl.rbt => ('a, 'b) RBT_Impl.rbt => RBT_Impl.compare"
    where
    "compare_height sx s t tx =
  (case (RBT_Impl.skip_red sx, RBT_Impl.skip_red s, RBT_Impl.skip_red t, RBT_Impl.skip_red tx) of
     (Branch _ sx' _ _ _, Branch _ s' _ _ _, Branch _ t' _ _ _, Branch _ tx' _ _ _) => 
       compare_height (RBT_Impl.skip_black sx') s' t' (RBT_Impl.skip_black tx')
   | (_, rbt.Empty, _, Branch _ _ _ _ _) => RBT_Impl.LT
   | (Branch _ _ _ _ _, _, rbt.Empty, _) => RBT_Impl.GT
   | (Branch _ sx' _ _ _, Branch _ s' _ _ _, Branch _ t' _ _ _, rbt.Empty) =>
       compare_height (RBT_Impl.skip_black sx') s' t' rbt.Empty
   | (rbt.Empty, Branch _ s' _ _ _, Branch _ t' _ _ _, Branch _ tx' _ _ _) =>
       compare_height rbt.Empty s' t' (RBT_Impl.skip_black tx')
   | _ => RBT_Impl.EQ)"
    by pat_completeness auto

  lemma skip_red_size: "size (RBT_Impl.skip_red b) ≤ size b"
    by (auto simp add: skip_red_alt split: rbt.split color.split)

  lemma skip_black_size: "size (RBT_Impl.skip_black b) ≤ size b"
    unfolding RBT_Impl.skip_black_def
    apply (auto 
      simp add: Let_def 
      split: rbt.split color.split
    )
    using skip_red_size[of b]
    apply auto
    done
    
  termination 
  proof -
    {
      fix s t x
      assume A: "s = RBT_Impl.skip_red t"
        and B: "x < size s"
      note B
      also note A
      also note skip_red_size
      finally have "x < size t" .
    } note AUX=this

    show "All compare_height_dom"
      apply (relation 
        "measure (λ(a, b, c, d). size a + size b + size c + size d)")
      apply rule

      (* FIXME: This is solved by
        apply (smt rbt.size(4) skip_black_size skip_red_size)+
        which is, however, not allowed for afp.
        *)

      apply (clarsimp simp: Let_def split: rbt.splits color.splits)
      apply (intro add_less_mono trans_less_add2 
        order_le_less_trans[OF skip_black_size], (erule AUX, simp)+) []

      apply (clarsimp simp: Let_def split: rbt.splits color.splits)
      apply (rule trans_less_add1)
      apply (intro add_less_mono trans_less_add2 
        order_le_less_trans[OF skip_black_size], (erule AUX, simp)+) []

      apply (clarsimp simp: Let_def split: rbt.splits color.splits)
      apply (intro add_less_mono trans_less_add2 
        order_le_less_trans[OF skip_black_size], (erule AUX, simp)+) []
      done
  qed

  lemmas [simp del] = compare_height.simps

  lemma compare_height_alt: 
    "RBT_Impl.compare_height sx s t tx = compare_height sx s t tx"
    apply (induct sx s t tx rule: compare_height.induct)
    apply (subst RBT_Impl.compare_height.simps)
    apply (subst compare_height.simps)
    apply (auto split: rbt.split)
    done

  term RBT_Impl.skip_red
  lemma param_skip_red[param]: "(RBT_Impl.skip_red,RBT_Impl.skip_red) 
    ∈ ⟨Rk,Rv⟩rbt_rel -> ⟨Rk,Rv⟩rbt_rel"
    unfolding skip_red_alt[abs_def] by parametricity

  lemma param_skip_black[param]: "(RBT_Impl.skip_black,RBT_Impl.skip_black) 
    ∈ ⟨Rk,Rv⟩rbt_rel -> ⟨Rk,Rv⟩rbt_rel"
    unfolding RBT_Impl.skip_black_def[abs_def] by parametricity

  term case_rbt
  lemma param_case_rbt':
    assumes "(t,t')∈⟨Rk,Rv⟩rbt_rel"
    assumes "[|t=rbt.Empty; t'=rbt.Empty|] ==> (fl,fl')∈R"
    assumes "!!c l k v r c' l' k' v' r'. [| 
      t = Branch c l k v r; t' = Branch c' l' k' v' r'; 
      (c,c')∈color_rel;
      (l,l')∈⟨Rk,Rv⟩rbt_rel; (k,k')∈Rk; (v,v')∈Rv; (r,r')∈⟨Rk,Rv⟩rbt_rel
    |] ==> (fb c l k v r, fb' c' l' k' v' r') ∈ R"
    shows "(case_rbt fl fb t, case_rbt fl' fb' t') ∈ R"
    using assms by (auto split: rbt.split elim: rbt_rel_elims)
      
  lemma compare_height_param_aux[param]:
    "[| (sx,sx')∈⟨Rk,Rv⟩rbt_rel; (s,s')∈⟨Rk,Rv⟩rbt_rel;
       (t,t')∈⟨Rk,Rv⟩rbt_rel; (tx,tx')∈⟨Rk,Rv⟩rbt_rel |]
    ==> (compare_height sx s t tx, compare_height sx' s' t' tx') ∈ compare_rel"
    apply (induct sx' s' t' tx' arbitrary: sx s t tx 
      rule: compare_height.induct)
    apply (subst (2) compare_height.simps)
    apply (subst compare_height.simps)
    apply (parametricity add: param_case_prod' param_case_rbt', (simp only: Pair_eq)+) []
    done

  lemma compare_height_param[param]:
    "(RBT_Impl.compare_height,RBT_Impl.compare_height) ∈ 
      ⟨Rk,Rv⟩rbt_rel -> ⟨Rk,Rv⟩rbt_rel -> ⟨Rk,Rv⟩rbt_rel -> ⟨Rk,Rv⟩rbt_rel 
      -> compare_rel"
    unfolding compare_height_alt[abs_def]
    by parametricity

  lemma param_rbt_union[param]:
    fixes less
    assumes param_less[param]: "(less,less') ∈ Ra -> Ra -> Id"
    shows "(ord.rbt_union less, ord.rbt_union less') 
      ∈ ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel -> ⟨Ra,Rb⟩rbt_rel"
    unfolding ord.rbt_union_def[abs_def] ord.rbt_union_with_key_def[abs_def]
      ord.rbt_insert_with_key_def[abs_def]
    unfolding RBT_Impl.fold_def RBT_Impl.entries_def
    by parametricity

term rm_iterateoi
lemma param_rm_iterateoi[param]: "(rm_iterateoi,rm_iterateoi) 
  ∈ ⟨Ra,Rb⟩rbt_rel -> (Rc->Id) -> (⟨Ra,Rb⟩prod_rel -> Rc -> Rc) -> Rc -> Rc"
  unfolding rm_iterateoi_def
  by (parametricity)

lemma param_rm_reverse_iterateoi[param]: 
  "(rm_reverse_iterateoi,rm_reverse_iterateoi) 
    ∈ ⟨Ra,Rb⟩rbt_rel -> (Rc->Id) -> (⟨Ra,Rb⟩prod_rel -> Rc -> Rc) -> Rc -> Rc"
  unfolding rm_reverse_iterateoi_def
  by (parametricity)


lemma param_color_eq[param]: 
  "(op =, op =)∈color_rel->color_rel->Id"
  by (auto elim: color_rel.cases)

lemma param_color_of[param]: 
  "(color_of, color_of)∈⟨Rk,Rv⟩rbt_rel->color_rel"
  unfolding color_of_def
  by parametricity

term bheight
lemma param_bheight[param]:
  "(bheight,bheight)∈⟨Rk,Rv⟩rbt_rel->Id"
  unfolding bheight_def
  by (parametricity)

lemma inv1_param[param]: "(inv1,inv1)∈⟨Rk,Rv⟩rbt_rel->Id"
  unfolding inv1_def
  by (parametricity)

lemma inv2_param[param]: "(inv2,inv2)∈⟨Rk,Rv⟩rbt_rel->Id"
  unfolding inv2_def
  by (parametricity)

term ord.rbt_less
lemma rbt_less_param[param]: "(ord.rbt_less,ord.rbt_less) ∈ 
  (Rk->Rk->Id) -> Rk -> ⟨Rk,Rv⟩rbt_rel -> Id"
  unfolding ord.rbt_less_prop[abs_def]
  apply (parametricity add: param_list_ball)
  unfolding RBT_Impl.keys_def RBT_Impl.entries_def
  apply (parametricity)
  done

term ord.rbt_greater
lemma rbt_greater_param[param]: "(ord.rbt_greater,ord.rbt_greater) ∈ 
  (Rk->Rk->Id) -> Rk -> ⟨Rk,Rv⟩rbt_rel -> Id"
  unfolding ord.rbt_greater_prop[abs_def]
  apply (parametricity add: param_list_ball)
  unfolding RBT_Impl.keys_def RBT_Impl.entries_def
  apply (parametricity)
  done

lemma rbt_sorted_param[param]:
  "(ord.rbt_sorted,ord.rbt_sorted)∈(Rk->Rk->Id)->⟨Rk,Rv⟩rbt_rel->Id"
  unfolding ord.rbt_sorted_def[abs_def]
  by (parametricity)

lemma is_rbt_param[param]: "(ord.is_rbt,ord.is_rbt) ∈ 
  (Rk->Rk->Id) -> ⟨Rk,Rv⟩rbt_rel -> Id"
  unfolding ord.is_rbt_def[abs_def]
  by (parametricity)

definition "rbt_map_rel' lt = br (ord.rbt_lookup lt) (ord.is_rbt lt)"

lemma (in linorder) rbt_map_impl:
  "(rbt.Empty,Map.empty) ∈ rbt_map_rel' op <"
  "(rbt_insert,λk v m. m(k\<mapsto>v)) 
    ∈ Id -> Id -> rbt_map_rel' op < -> rbt_map_rel' op <"
  "(rbt_lookup,λm k. m k) ∈ rbt_map_rel' op < -> Id -> ⟨Id⟩option_rel"
  "(rbt_delete,λk m. m|`(-{k})) ∈ Id -> rbt_map_rel' op < -> rbt_map_rel' op <"
  "(rbt_union,op ++) 
    ∈ rbt_map_rel' op < -> rbt_map_rel' op < -> rbt_map_rel' op <"
  by (auto simp add: 
    rbt_lookup_rbt_insert rbt_lookup_rbt_delete rbt_lookup_rbt_union
    rbt_union_is_rbt
    rbt_map_rel'_def br_def)

lemma sorted_by_rel_keys_true[simp]: "sorted_by_rel (λ(_,_) (_,_). True) l"
  apply (induct l)
  apply auto
  done

(*
lemma (in linorder) rbt_it_linord_impl: 
  "is_map_iterator_linord (rbt_map_rel' op <) Id Id Id 
    (rm_iterateoi::_ => ('a,'v,'s) map_iterator)"
  unfolding is_map_iterator_genord_def is_map_iterator_linord_def 
    gen_map_iterator_genord_def[abs_def]
  apply (intro fun_relI)
  apply (clarsimp intro!: chooseR.intros[OF _ IdI])
proof -
  case (goal1 t s' c f s)
  hence "is_rbt t" and [simp]: "s'=(rbt_lookup t)" 
    unfolding rbt_map_rel'_def br_def by simp_all
  hence RSORTED: "rbt_sorted t" by (simp add: is_rbt_def)
 
  thm rm_iterateoi_correct
  from rm_iterateoi_correct[OF RSORTED,
    unfolded set_iterator_map_linord_def
      set_iterator_genord_def
  ] obtain l where 
      "distinct l" 
      and "map_to_set (rbt_lookup t) = set l"
      and "sorted_by_rel (λ(k,_) (k',_). k ≤ k') l"
      and "(rm_iterateoi t::('a,'v,'s) map_iterator) = foldli l"
    by blast
  thus ?case 
    apply (rule_tac exI[where x=l])
    apply (simp add: sorted_by_rel_keys_map_fst)
    by (metis iterate_to_list_foldli map_iterator_foldli_conv rev_rev_ident 
      set_iterator_foldli_correct)
qed

lemma (in linorder) rbt_it_rev_linord_impl: 
  "is_map_iterator_rev_linord (rbt_map_rel' op <) Id Id Id 
    (rm_reverse_iterateoi::_ => ('a,'v,'s) map_iterator)"
  unfolding is_map_iterator_genord_def is_map_iterator_rev_linord_def 
    gen_map_iterator_genord_def[abs_def]
  apply (intro fun_relI)
  apply (clarsimp intro!: chooseR.intros[OF _ IdI])
proof -
  case (goal1 t s' c f s)
  hence "is_rbt t" and [simp]: "s'=(rbt_lookup t)" 
    unfolding rbt_map_rel'_def br_def by simp_all
  hence RSORTED: "rbt_sorted t" by (simp add: is_rbt_def)
  
  from rm_reverse_iterateoi_correct[unfolded 
    set_iterator_map_rev_linord_def
    set_iterator_genord_def,
    OF RSORTED
  ] obtain l where 
      "distinct l" 
      and "map_to_set (rbt_lookup t) = set l"
      and "sorted_by_rel (λ(k,_) (k',_). k ≥ k') l"
      and "(rm_reverse_iterateoi t::('a,'v,'s) map_iterator) = foldli l"
    by blast
  thus ?case 
    apply (rule_tac exI[where x=l])
    apply (simp add: sorted_by_rel_keys_map_fst)
    by (metis iterate_to_list_foldli map_iterator_foldli_conv rev_rev_ident 
      set_iterator_foldli_correct)
qed

lemma (in linorder) rbt_it_impl: 
  "is_map_iterator (rbt_map_rel' op <) Id Id Id rm_iterateoi"
  unfolding is_map_iterator_def 
  apply (rule is_map_iterator_genord_weaken)
  apply (rule rbt_it_linord_impl[unfolded is_map_iterator_linord_def])
  ..

*)

definition rbt_map_rel_def_internal:
  "rbt_map_rel lt Rk Rv ≡ ⟨Rk,Rv⟩rbt_rel O rbt_map_rel' lt"

lemma rbt_map_rel_def: 
  "⟨Rk,Rv⟩rbt_map_rel lt ≡ ⟨Rk,Rv⟩rbt_rel O rbt_map_rel' lt"
  by (simp add: rbt_map_rel_def_internal relAPP_def)

(*
lemma (in linorder) autoref_gen_rbt_iterate_linord:
  "is_map_iterator_linord 
    (⟨Rk,Rv⟩rbt_map_rel op <) (Rk::(_×'a) set) Rv Rσ rm_iterateoi"
proof -
  note param_rm_iterateoi[of Rk Rv Rσ]
  also note rbt_it_linord_impl[
    unfolded is_map_iterator_linord_def is_map_iterator_genord_def]
  finally (relcompI) show ?thesis
    unfolding is_map_iterator_linord_def is_map_iterator_genord_def
    apply -
    apply (erule set_rev_mp)
    apply (simp add: rbt_map_rel_def rbt_map_rel'_def)
    apply (
      rule Orderings.order_trans[OF fun_rel_comp_dist] fun_rel_mono subset_refl
      | simp
    )+
    done
qed

lemma (in linorder) autoref_gen_rbt_iterate_rev_linord:
  "is_map_iterator_rev_linord 
    (⟨Rk,Rv⟩rbt_map_rel op <) (Rk::(_×'a) set) Rv Rσ rm_reverse_iterateoi"
proof -
  note param_rm_reverse_iterateoi[of Rk Rv Rσ]
  also note rbt_it_rev_linord_impl[
    unfolded is_map_iterator_rev_linord_def is_map_iterator_genord_def]
  finally (relcompI) show ?thesis
    unfolding is_map_iterator_rev_linord_def is_map_iterator_genord_def
    apply -
    apply (erule set_rev_mp)
    apply (simp add: rbt_map_rel_def rbt_map_rel'_def)
    apply (
      rule Orderings.order_trans[OF fun_rel_comp_dist] fun_rel_mono subset_refl
      | simp
    )+
    done
qed

lemma (in linorder) autoref_gen_rbt_iterate:
  "is_map_iterator 
    (⟨Rk,Rv⟩rbt_map_rel op <) (Rk::(_×'a) set) Rv Rσ rm_iterateoi"
proof -
  note param_rm_iterateoi[of Rk Rv Rσ]
  also note rbt_it_impl[
    unfolded is_map_iterator_def is_map_iterator_genord_def]
  finally (relcompI) show ?thesis
    unfolding is_map_iterator_def is_map_iterator_genord_def
    apply -
    apply (erule set_rev_mp)
    apply (simp add: rbt_map_rel_def rbt_map_rel'_def)
    apply (
      rule Orderings.order_trans[OF fun_rel_comp_dist] fun_rel_mono subset_refl
      | simp
    )+
    done
qed
*)

lemma (in linorder) autoref_gen_rbt_empty: 
  "(rbt.Empty,Map.empty) ∈ ⟨Rk,Rv⟩rbt_map_rel op <"
  by (auto simp: rbt_map_rel_def 
    intro!: rbt_map_impl rbt_rel_intros)

lemma (in linorder) autoref_gen_rbt_insert:
  fixes less_impl
  assumes param_less: "(less_impl,op <) ∈ Rk -> Rk -> Id"
  shows "(ord.rbt_insert less_impl,λk v m. m(k\<mapsto>v)) ∈ 
    Rk -> Rv -> ⟨Rk,Rv⟩rbt_map_rel op < -> ⟨Rk,Rv⟩rbt_map_rel op <"
  apply (intro fun_relI)
  unfolding rbt_map_rel_def
  apply (auto intro!: relcomp.intros)
  apply (rule param_rbt_insert[OF param_less, param_fo])
  apply assumption+
  apply (rule rbt_map_impl[param_fo])
  apply (rule IdI | assumption)+
  done

lemma (in linorder) autoref_gen_rbt_lookup:
  fixes less_impl
  assumes param_less: "(less_impl,op <) ∈ Rk -> Rk -> Id"
  shows "(ord.rbt_lookup less_impl, λm k. m k) ∈ 
    ⟨Rk,Rv⟩rbt_map_rel op < -> Rk -> ⟨Rv⟩option_rel"
  unfolding rbt_map_rel_def
  apply (intro fun_relI)
  apply (elim relcomp.cases)
  apply hypsubst
  apply (subst R_O_Id[symmetric])
  apply (rule relcompI)
  apply (rule param_rbt_lookup[OF param_less, param_fo])
  apply assumption+
  apply (subst option_rel_id_simp[symmetric])
  apply (rule rbt_map_impl[param_fo])
  apply assumption
  apply (rule IdI)
  done

lemma (in linorder) autoref_gen_rbt_delete:
  fixes less_impl
  assumes param_less: "(less_impl,op <) ∈ Rk -> Rk -> Id"
  shows "(ord.rbt_delete less_impl, λk m. m |`(-{k})) ∈ 
    Rk -> ⟨Rk,Rv⟩rbt_map_rel op < -> ⟨Rk,Rv⟩rbt_map_rel op <"
  unfolding rbt_map_rel_def
  apply (intro fun_relI)
  apply (elim relcomp.cases)
  apply hypsubst
  apply (rule relcompI)
  apply (rule param_rbt_delete[OF param_less, param_fo])
  apply assumption+
  apply (rule rbt_map_impl[param_fo])
  apply (rule IdI)
  apply assumption
  done

lemma (in linorder) autoref_gen_rbt_union:
  fixes less_impl
  assumes param_less: "(less_impl,op <) ∈ Rk -> Rk -> Id"
  shows "(ord.rbt_union less_impl, op ++) ∈ 
    ⟨Rk,Rv⟩rbt_map_rel op < -> ⟨Rk,Rv⟩rbt_map_rel op < -> ⟨Rk,Rv⟩rbt_map_rel op <"
  unfolding rbt_map_rel_def
  apply (intro fun_relI)
  apply (elim relcomp.cases)
  apply hypsubst
  apply (rule relcompI)
  apply (rule param_rbt_union[OF param_less, param_fo])
  apply assumption+
  apply (rule rbt_map_impl[param_fo])
  apply assumption+
  done

subsection {* A linear ordering on red-black trees *}

abbreviation "rbt_to_list t ≡ it_to_list rm_iterateoi t"

lemma (in linorder) rbt_to_list_correct: 
  assumes SORTED: "rbt_sorted t"
  shows "rbt_to_list t = sorted_list_of_map (rbt_lookup t)" (is "?tl = _")
proof -
  from map_it_to_list_linord_correct[where it=rm_iterateoi, OF 
    rm_iterateoi_correct[OF SORTED]
  ] have 
      M: "map_of ?tl = rbt_lookup t"
      and D: "distinct (map fst ?tl)"
      and S: "sorted (map fst ?tl)"
    by (simp_all)

  from the_sorted_list_of_map[OF D S] M show ?thesis
    by simp
qed

definition 
  "cmp_rbt cmpk cmpv ≡ cmp_img rbt_to_list (cmp_lex (cmp_prod cmpk cmpv))"

lemma (in linorder) param_rbt_sorted_list_of_map[param]:
  shows "(rbt_to_list, sorted_list_of_map) ∈ 
  ⟨Rk, Rv⟩rbt_map_rel op < -> ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
  apply (auto simp: rbt_map_rel_def rbt_map_rel'_def br_def
    rbt_to_list_correct[symmetric]
  )
  by (parametricity)

lemma param_rbt_sorted_list_of_map'[param]:
  assumes ELO: "eq_linorder cmp'"
  shows "(rbt_to_list,linorder.sorted_list_of_map (comp2le cmp')) ∈ 
    ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp') -> ⟨⟨Rk,Rv⟩prod_rel⟩list_rel"
proof -
  interpret linorder "comp2le cmp'" "comp2lt cmp'"
    using ELO by (simp add: eq_linorder_class_conv)
  show ?thesis
    by parametricity
qed

lemma rbt_linorder_impl:
  assumes ELO: "eq_linorder cmp'"
  assumes [param]: "(cmp,cmp')∈Rk->Rk->Id"
  shows 
  "(cmp_rbt cmp, cmp_map cmp') ∈ 
    (Rv->Rv->Id) 
    -> ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp') 
    -> ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp') -> Id"
proof -
  interpret linorder "comp2le cmp'" "comp2lt cmp'"
    using ELO by (simp add: eq_linorder_class_conv)

  show ?thesis
    unfolding cmp_map_def[abs_def] cmp_rbt_def[abs_def]
    apply (parametricity add: param_cmp_extend param_cmp_img)
    unfolding rbt_map_rel_def[abs_def] rbt_map_rel'_def br_def
    by auto
qed

lemma color_rel_sv[relator_props]: "single_valued color_rel"
  by (auto intro!: single_valuedI elim: color_rel.cases)

lemma rbt_rel_sv_aux:
  assumes SK: "single_valued Rk" 
  assumes SV: "single_valued Rv"
  assumes I1: "(a,b)∈(⟨Rk, Rv⟩rbt_rel)"
  assumes I2: "(a,c)∈(⟨Rk, Rv⟩rbt_rel)"
  shows "b=c"
  using I1 I2
  apply (induct arbitrary: c)
  apply (elim rbt_rel_elims)
  apply simp
  apply (elim rbt_rel_elims)
  apply (simp add: single_valuedD[OF color_rel_sv] 
    single_valuedD[OF SK] single_valuedD[OF SV])
  done

lemma rbt_rel_sv[relator_props]:
  assumes SK: "single_valued Rk" 
  assumes SV: "single_valued Rv"
  shows "single_valued (⟨Rk, Rv⟩rbt_rel)"
  by (auto intro: single_valuedI rbt_rel_sv_aux[OF SK SV])

lemma rbt_map_rel_sv[relator_props]:
  "[|single_valued Rk; single_valued Rv|] 
  ==> single_valued (⟨Rk,Rv⟩rbt_map_rel lt)"
  apply (auto simp: rbt_map_rel_def rbt_map_rel'_def)
  apply (rule single_valued_relcomp)
  apply (rule rbt_rel_sv, assumption+)
  apply (rule br_sv)
  done

lemmas [autoref_rel_intf] = REL_INTFI[of "rbt_map_rel x" i_map] for x


subsection {* Second Part: Binding *}
lemma autoref_rbt_empty[autoref_rules]:
  assumes ELO: "SIDE_GEN_ALGO (eq_linorder cmp')"
  assumes [simplified,param]: "GEN_OP cmp cmp' (Rk->Rk->Id)"
  shows "(rbt.Empty,op_map_empty) ∈ 
    ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp')"
proof -
  interpret linorder "comp2le cmp'" "comp2lt cmp'"
    using ELO by (simp add: eq_linorder_class_conv)
  show ?thesis
    by (simp) (rule autoref_gen_rbt_empty)
qed

lemma autoref_rbt_update[autoref_rules]:
  assumes ELO: "SIDE_GEN_ALGO (eq_linorder cmp')"
  assumes [simplified,param]: "GEN_OP cmp cmp' (Rk->Rk->Id)"
  shows "(ord.rbt_insert (comp2lt cmp),op_map_update) ∈ 
    Rk->Rv->⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp') 
    -> ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp')"
proof -
  interpret linorder "comp2le cmp'" "comp2lt cmp'"
    using ELO by (simp add: eq_linorder_class_conv)
  show ?thesis
    unfolding op_map_update_def[abs_def]
    apply (rule autoref_gen_rbt_insert)
    unfolding comp2lt_def[abs_def]
    by (parametricity)
qed

lemma autoref_rbt_lookup[autoref_rules]:
  assumes ELO: "SIDE_GEN_ALGO (eq_linorder cmp')"
  assumes [simplified,param]: "GEN_OP cmp cmp' (Rk->Rk->Id)"
  shows "(λk t. ord.rbt_lookup (comp2lt cmp) t k, op_map_lookup) ∈ 
    Rk -> ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp') -> ⟨Rv⟩option_rel"
proof -
  interpret linorder "comp2le cmp'" "comp2lt cmp'"
    using ELO by (simp add: eq_linorder_class_conv)
  show ?thesis
    unfolding op_map_lookup_def[abs_def]
    apply (intro fun_relI)
    apply (rule autoref_gen_rbt_lookup[param_fo])
    apply (unfold comp2lt_def[abs_def]) []
    apply (parametricity)
    apply assumption+
    done
qed

lemma autoref_rbt_delete[autoref_rules]:
  assumes ELO: "SIDE_GEN_ALGO (eq_linorder cmp')"
  assumes [simplified,param]: "GEN_OP cmp cmp' (Rk->Rk->Id)"
  shows "(ord.rbt_delete (comp2lt cmp),op_map_delete) ∈
    Rk -> ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp') 
       -> ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp')"
proof -
  interpret linorder "comp2le cmp'" "comp2lt cmp'"
    using ELO by (simp add: eq_linorder_class_conv)
  show ?thesis
    unfolding op_map_delete_def[abs_def]
    apply (intro fun_relI)
    apply (rule autoref_gen_rbt_delete[param_fo])
    apply (unfold comp2lt_def[abs_def]) []
    apply (parametricity)
    apply assumption+
    done
qed

lemma autoref_rbt_union[autoref_rules]:
  assumes ELO: "SIDE_GEN_ALGO (eq_linorder cmp')"
  assumes [simplified,param]: "GEN_OP cmp cmp' (Rk->Rk->Id)"
  shows "(ord.rbt_union (comp2lt cmp),op ++) ∈
    ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp') -> ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp')
       -> ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmp')"
proof -
  interpret linorder "comp2le cmp'" "comp2lt cmp'"
    using ELO by (simp add: eq_linorder_class_conv)
  show ?thesis
    apply (intro fun_relI)
    apply (rule autoref_gen_rbt_union[param_fo])
    apply (unfold comp2lt_def[abs_def]) []
    apply (parametricity)
    apply assumption+
    done
qed

lemma autoref_rbt_is_iterator[autoref_ga_rules]: 
  assumes ELO: "GEN_ALGO_tag (eq_linorder cmp')"
  shows "is_map_to_sorted_list (comp2le cmp') Rk Rv (rbt_map_rel (comp2lt cmp'))
    rbt_to_list"
proof -
  interpret linorder "comp2le cmp'" "comp2lt cmp'"
    using ELO by (simp add: eq_linorder_class_conv)

  show ?thesis
    unfolding is_map_to_sorted_list_def
      it_to_sorted_list_def
    apply auto
  proof -
    fix r m'
    assume "(r, m') ∈ ⟨Rk, Rv⟩rbt_map_rel (comp2lt cmp')"
    then obtain r' where R1: "(r,r')∈⟨Rk,Rv⟩rbt_rel" 
      and R2: "(r',m') ∈ rbt_map_rel' (comp2lt cmp')"
      unfolding rbt_map_rel_def by blast
    
    from R2 have "is_rbt r'" and M': "m' = rbt_lookup r'"
      unfolding rbt_map_rel'_def
      by (simp_all add: br_def)
    hence SORTED: "rbt_sorted r'"
      by (simp add: is_rbt_def)

    from map_it_to_list_linord_correct[where it = rm_iterateoi, OF 
      rm_iterateoi_correct[OF SORTED]
    ] have 
        M: "map_of (rbt_to_list r') = rbt_lookup r'"
        and D: "distinct (map fst (rbt_to_list r'))"
        and S: "sorted (map fst (rbt_to_list r'))"
      by (simp_all)

    show "∃l'. (rbt_to_list r, l') ∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel ∧
            distinct l' ∧
            map_to_set m' = set l' ∧
            sorted_by_rel (key_rel (comp2le cmp')) l'"
    proof (intro exI conjI)
      from D show "distinct (rbt_to_list r')" by (rule distinct_mapI)
      from S show "sorted_by_rel (key_rel (comp2le cmp')) (rbt_to_list r')"
        unfolding key_rel_def[abs_def]
        by simp
      show "(rbt_to_list r, rbt_to_list r') ∈ ⟨⟨Rk, Rv⟩prod_rel⟩list_rel"
        by (parametricity add: R1)
      from M show "map_to_set m' = set (rbt_to_list r')"
        by (simp add: M' map_of_map_to_set[OF D])
    qed
  qed
qed
        
(* TODO: Reverse iterator *)

lemmas [autoref_ga_rules] = class_to_eq_linorder

lemma (in linorder) dflt_cmp_id:
  "(dflt_cmp op ≤ op <, dflt_cmp op ≤ op <)∈Id->Id->Id"
  by auto

lemmas [autoref_rules] = dflt_cmp_id

lemma rbt_linorder_autoref[autoref_rules]:
  assumes "SIDE_GEN_ALGO (eq_linorder cmpk')"
  assumes "SIDE_GEN_ALGO (eq_linorder cmpv')"
  assumes "GEN_OP cmpk cmpk' (Rk->Rk->Id)"
  assumes "GEN_OP cmpv cmpv' (Rv->Rv->Id)"
  shows 
  "(cmp_rbt cmpk cmpv, cmp_map cmpk' cmpv') ∈ 
       ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmpk') 
    -> ⟨Rk,Rv⟩rbt_map_rel (comp2lt cmpk') -> Id"
  apply (intro fun_relI)
  apply (rule rbt_linorder_impl[param_fo])
  using assms 
  apply simp_all
  done

(* TODO: Move. This belongs to generic algorithms for orders *)
lemma map_linorder_impl[autoref_ga_rules]:
  assumes "GEN_ALGO_tag (eq_linorder cmpk)"
  assumes "GEN_ALGO_tag (eq_linorder cmpv)"
  shows "eq_linorder (cmp_map cmpk cmpv)"
  using assms apply simp_all
  using map_ord_eq_linorder .

lemma set_linorder_impl[autoref_ga_rules]:
  assumes "GEN_ALGO_tag (eq_linorder cmpk)"
  shows "eq_linorder (cmp_set cmpk)"
  using assms apply simp_all
  using set_ord_eq_linorder .

lemma (in linorder) rbt_map_rel_finite_aux:
  "finite_map_rel (⟨Rk,Rv⟩rbt_map_rel op <)"
  unfolding finite_map_rel_def
  by (auto simp: rbt_map_rel_def rbt_map_rel'_def br_def)

lemma rbt_map_rel_finite[relator_props]: 
  assumes ELO: "GEN_ALGO_tag (eq_linorder cmpk)"
  shows "finite_map_rel (⟨Rk,Rv⟩rbt_map_rel (comp2lt cmpk))"
proof -
  interpret linorder "comp2le cmpk" "comp2lt cmpk"
    using ELO by (simp add: eq_linorder_class_conv)
  show ?thesis
    using rbt_map_rel_finite_aux .
qed

abbreviation 
  "dflt_rm_rel ≡ rbt_map_rel (comp2lt (dflt_cmp op ≤ op <))"

lemmas [autoref_post_simps] = dflt_cmp_inv2 dflt_cmp_2inv

lemma [simp,autoref_post_simps]: "ord.rbt_ins op < = rbt_ins"
proof (intro ext)
  case goal1 thus ?case
    apply (induct x xa xb xc rule: rbt_ins.induct)
    apply (simp_all add: ord.rbt_ins.simps)
    done
qed

lemma [simp,autoref_post_simps]:
  "ord.rbt_insert_with_key op < = rbt_insert_with_key"
  "ord.rbt_insert op < = rbt_insert"
  unfolding 
    ord.rbt_insert_with_key_def[abs_def] rbt_insert_with_key_def[abs_def]
    ord.rbt_insert_def[abs_def] rbt_insert_def[abs_def]
  by simp_all

(* TODO: Move, probably to some orderings setup theory *)
lemma autoref_comp2eq[autoref_rules_raw]:
  assumes PRIO_TAG_GEN_ALGO
  assumes ELC: "SIDE_GEN_ALGO (eq_linorder cmp')"
  assumes [simplified,param]: "GEN_OP cmp cmp' (R->R->Id)"
  shows "(comp2eq cmp, op =) ∈ R->R->Id"
proof -
  from ELC have 1: "eq_linorder cmp'" by simp
  show ?thesis
    apply (subst eq_linorder_comp2eq_eq[OF 1,symmetric])
    by parametricity
qed

lemma pi'_rm[icf_proper_iteratorI]: 
  "proper_it' rm_iterateoi rm_iterateoi"
  "proper_it' rm_reverse_iterateoi rm_reverse_iterateoi"
  apply (rule proper_it'I)
  apply (rule pi_rm)
  apply (rule proper_it'I)
  apply (rule pi_rm_rev)
  done

declare pi'_rm[proper_it]


lemmas autoref_rbt_rules = 
  autoref_rbt_empty
  autoref_rbt_lookup
  autoref_rbt_update
  autoref_rbt_delete
  autoref_rbt_union

lemmas autoref_rbt_rules_linorder[autoref_rules_raw] = 
  autoref_rbt_rules[where Rk="Rk"] for Rk :: "(_×_::linorder) set"

end