Theory Impl_RBT_Map

section ‹\isaheader{Red-Black Tree based Maps}›
theory Impl_RBT_Map
imports 
  "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, goal_cases)
    case (1 s s' f f' t t') from this(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, goal_cases)
    case (1 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, goal_cases)
    case (1 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, goal_cases)
    case (1 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, goal_cases)
    case (1 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, goal_cases)
    case (1 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: prod.inject)+) []
    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 rbt_rel_bheight: "(t, t') ∈ ⟨Ra, Rb⟩rbt_rel ⟹ bheight t = bheight t'"
  by (induction t arbitrary: t') (auto elim!: rbt_rel_elims color_rel.cases)

lemma param_rbt_baliL[param]: "(rbt_baliL,rbt_baliL) ∈ ⟨Ra,Rb⟩rbt_rel → Ra → Rb → ⟨Ra,Rb⟩rbt_rel → ⟨Ra,Rb⟩rbt_rel"
proof (intro fun_relI, goal_cases)
  case (1 l l' a a' b b' r r')
  thus ?case
    apply (induct l a b r arbitrary: l' a' b' r' rule: rbt_baliL.induct)
    apply (elim_all rbt_rel_elims color_rel_elims)
    apply (simp_all only: rbt_baliL.simps)
    apply parametricity+
    done
qed

lemma param_rbt_baliR[param]: "(rbt_baliR,rbt_baliR) ∈ ⟨Ra,Rb⟩rbt_rel → Ra → Rb → ⟨Ra,Rb⟩rbt_rel → ⟨Ra,Rb⟩rbt_rel"
proof (intro fun_relI, goal_cases)
  case (1 l l' a a' b b' r r')
  thus ?case
    apply (induction l a b r arbitrary: l' a' b' r' rule: rbt_baliR.induct)
    apply (elim_all rbt_rel_elims color_rel_elims)
    apply (simp_all only: rbt_baliR.simps)
    apply parametricity+
    done
qed

lemma param_rbt_joinL[param]: "(rbt_joinL,rbt_joinL) ∈ ⟨Ra,Rb⟩rbt_rel → Ra → Rb → ⟨Ra,Rb⟩rbt_rel → ⟨Ra,Rb⟩rbt_rel"
proof (intro fun_relI, goal_cases)
  case (1 l l' a a' b b' r r')
  thus ?case
  proof (induction l a b r arbitrary: l' a' b' r' rule: rbt_joinL.induct)
    case (1 l a b r)
    have "bheight l < bheight r ⟹ r = RBT_Impl.MB ll k v rr ⟹ (ll, ll') ∈ ⟨Ra, Rb⟩rbt_rel ⟹
       (k, k') ∈ Ra ⟹ (v, v') ∈ Rb ⟹ (rr, rr') ∈ ⟨Ra, Rb⟩rbt_rel ⟹
       (rbt_baliL (rbt_joinL l a b ll) k v rr, rbt_baliL (rbt_joinL l' a' b' ll') k' v' rr') ∈ ⟨Ra, Rb⟩rbt_rel"
      for ll ll' k k' v v' rr rr'
      by parametricity (auto intro: 1)
    then show ?case
      using 1
      by (auto simp: rbt_joinL.simps[of l a b r] rbt_joinL.simps[of l' a' b' r'] rbt_rel_bheight
          intro: rbt_rel_intros color_rel.intros elim!: rbt_rel_elims color_rel_elims
          split: rbt.splits color.splits)
  qed
qed

lemma param_rbt_joinR[param]:
  "(rbt_joinR,rbt_joinR) ∈ ⟨Ra,Rb⟩rbt_rel → Ra → Rb → ⟨Ra,Rb⟩rbt_rel → ⟨Ra,Rb⟩rbt_rel"
proof (intro fun_relI, goal_cases)
  case (1 l l' a a' b b' r r')
  thus ?case
  proof (induction l a b r arbitrary: l' a' b' r' rule: rbt_joinR.induct)
    case (1 l a b r)
    have "bheight r < bheight l ⟹ l = RBT_Impl.MB ll k v rr ⟹ (ll, ll') ∈ ⟨Ra, Rb⟩rbt_rel ⟹
       (k, k') ∈ Ra ⟹ (v, v') ∈ Rb ⟹ (rr, rr') ∈ ⟨Ra, Rb⟩rbt_rel ⟹
       (rbt_baliR ll k v (rbt_joinR rr a b r), rbt_baliR ll' k' v' (rbt_joinR rr' a' b' r')) ∈ ⟨Ra, Rb⟩rbt_rel"
      for ll ll' k k' v v' rr rr'
      by parametricity (auto intro: 1)
    then show ?case
      using 1
      by (auto simp: rbt_joinR.simps[of l] rbt_joinR.simps[of l'] rbt_rel_bheight[symmetric]
          intro: rbt_rel_intros color_rel.intros elim!: rbt_rel_elims color_rel_elims
          split: rbt.splits color.splits)
  qed
qed

lemma param_rbt_join[param]: "(rbt_join,rbt_join) ∈ ⟨Ra,Rb⟩rbt_rel → Ra → Rb → ⟨Ra,Rb⟩rbt_rel → ⟨Ra,Rb⟩rbt_rel"
  by (auto simp: rbt_join_def Let_def rbt_rel_bheight) parametricity+

lemma param_split[param]:
  fixes less
  assumes [param]: "(less,less') ∈ Ra → Ra → Id"
  shows "(ord.rbt_split less, ord.rbt_split less') ∈ ⟨Ra,Rb⟩rbt_rel → Ra → ⟨⟨Ra,Rb⟩rbt_rel,⟨⟨Rb⟩option_rel,⟨Ra,Rb⟩rbt_rel⟩prod_rel⟩prod_rel"
proof (intro fun_relI)
  fix t t' a a'
  assume "(t, t') ∈ ⟨Ra, Rb⟩rbt_rel" "(a, a') ∈ Ra"
  then show "(ord.rbt_split less t a, ord.rbt_split less' t' a') ∈ ⟨⟨Ra,Rb⟩rbt_rel,⟨⟨Rb⟩option_rel,⟨Ra,Rb⟩rbt_rel⟩prod_rel⟩prod_rel"
  proof (induction t a arbitrary: t' rule: ord.rbt_split.induct[where ?less=less])
    case (2 c l k b r a)
    obtain c' l' k' b' r' where t'_def: "t' = Branch c' l' k' b' r'"
      using 2(3)
      by (auto elim: rbt_rel_elims)
    have sub_rel: "(l, l') ∈ ⟨Ra, Rb⟩rbt_rel" "(k, k') ∈ Ra" "(b, b') ∈ Rb" "(r, r') ∈ ⟨Ra, Rb⟩rbt_rel"
      using 2(3)
      by (auto simp: t'_def elim: rbt_rel_elims)
    have less_iff: "less a k ⟷ less' a' k'" "less k a ⟷ less' k' a'"
      using assms 2(4) sub_rel(2)
      by (auto dest: fun_relD)
    show ?case
      using 2(1)[OF _ sub_rel(1) 2(4)] 2(2)[OF _ _ sub_rel(4) 2(4)] sub_rel
      unfolding t'_def less_iff ord.rbt_split.simps(2)[of less c] ord.rbt_split.simps(2)[of less' c']
      by (auto split: prod.splits) parametricity+
  qed (auto simp: ord.rbt_split.simps elim!: rbt_rel_elims intro: rbt_rel_intros)
qed

lemma param_rbt_union_swap_rec[param]:
  fixes less
  assumes [param]: "(less,less') ∈ Ra → Ra → Id"
  shows "(ord.rbt_union_swap_rec less, ord.rbt_union_swap_rec less') ∈
    (Ra → Rb → Rb → Rb) → Id → ⟨Ra,Rb⟩rbt_rel → ⟨Ra,Rb⟩rbt_rel → ⟨Ra,Rb⟩rbt_rel"
proof (intro fun_relI)
  fix f f' b b' t1 t1' t2 t2'
  assume "(f, f') ∈ Ra → Rb → Rb → Rb" "(b, b') ∈ bool_rel" "(t1, t1') ∈ ⟨Ra, Rb⟩rbt_rel" "(t2, t2') ∈ ⟨Ra, Rb⟩rbt_rel"
  then show "(ord.rbt_union_swap_rec less f b t1 t2, ord.rbt_union_swap_rec less' f' b' t1' t2') ∈ ⟨Ra, Rb⟩rbt_rel"
  proof (induction f b t1 t2 arbitrary: b' t1' t2' rule: ord.rbt_union_swap_rec.induct[where ?less=less])
    case (1 f b t1 t2)
    obtain γ s1 s2 where flip1: "(γ, s2, s1) =
      (if flip_rbt t2 t1 then (¬b, t1, t2) else (b, t2, t1))"
      by fastforce
    obtain γ' s1' s2' where flip2: "(γ', s2', s1') =
      (if flip_rbt t2' t1' then (¬b', t1', t2') else (b', t2', t1'))"
      by fastforce
    define g where "g = (if γ then λk v v'. f k v' v else f)"
    define g' where "g' = (if γ' then λk v v'. f' k v' v else f')"
    note bheight_cong = rbt_rel_bheight[OF 1(5)] rbt_rel_bheight[OF 1(6)]
    have flip_cong: "flip_rbt t2 t1 ⟷ flip_rbt t2' t1'"
      by (auto simp: flip_rbt_def bheight_cong)
    have gamma_cong: "γ = γ'"
      using flip1 flip2 1(4)
      by (auto simp: flip_cong split: if_splits)
    have small_rbt_cong: "small_rbt s2 ⟷ small_rbt s2'"
      using flip1 flip2
      by (auto simp: small_rbt_def flip_cong bheight_cong split: if_splits)
    have rbt_rel_s: "(s1, s1') ∈ ⟨Ra, Rb⟩rbt_rel" "(s2, s2') ∈ ⟨Ra, Rb⟩rbt_rel"
      using flip1 flip2 1(5,6)
      by (auto simp: flip_cong split: if_splits)
    have fun_rel_g: "(g, g') ∈ Ra → Rb → Rb → Rb"
      using flip1 flip2 1(3,4)
      by (auto simp: flip_cong g_def g'_def intro: fun_relD[OF fun_relD[OF fun_relD]] split: if_splits)
    have rbt_rel_fold: "(RBT_Impl.fold (ord.rbt_insert_with_key less g) s2 s1, RBT_Impl.fold (ord.rbt_insert_with_key less' g') s2' s1') ∈ ⟨Ra, Rb⟩rbt_rel"
      unfolding RBT_Impl.fold_def RBT_Impl.entries_def ord.rbt_insert_with_key_def
      using rbt_rel_s fun_rel_g
      by parametricity
    {
      fix c l k v r c' l' k' v' r' ll β rr ll' β' rr'
      assume defs: "s1 = Branch c l k v r" "s1' = Branch c' l' k' v' r'"
        "ord.rbt_split less s2 k = (ll, β, rr)" "ord.rbt_split less' s2' k' = (ll', β', rr')"
        "¬small_rbt s2"
      have split_rel: "(ord.rbt_split less s2 k, ord.rbt_split less' s2' k') ∈ ⟨⟨Ra,Rb⟩rbt_rel,⟨⟨Rb⟩option_rel,⟨Ra,Rb⟩rbt_rel⟩prod_rel⟩prod_rel"
        using defs(1,2) param_split[OF assms, of Rb] rbt_rel_s
        by (auto elim: rbt_rel_elims dest: fun_relD)
      have IH1: "(ord.rbt_union_swap_rec less f γ l ll, ord.rbt_union_swap_rec less' f' γ' l' ll') ∈ ⟨Ra,Rb⟩rbt_rel"
        apply (rule 1(1)[OF refl flip1 refl refl _ _ _ refl])
        using 1(3) split_rel rbt_rel_s(1) defs
        by (auto simp: gamma_cong elim: rbt_rel_elims)
      have IH2: "(ord.rbt_union_swap_rec less f γ r rr, ord.rbt_union_swap_rec less' f' γ' r' rr') ∈ ⟨Ra,Rb⟩rbt_rel"
        apply (rule 1(2)[OF refl flip1 refl refl _ _ _ refl])
        using 1(3) split_rel rbt_rel_s(1) defs
        by (auto simp: gamma_cong elim: rbt_rel_elims)
      have fun_rel_g_app: "(g k v, g' k' v') ∈ Rb → Rb"
        using fun_rel_g rbt_rel_s
        by (auto simp: defs elim: rbt_rel_elims dest: fun_relD)
      have "(rbt_join (ord.rbt_union_swap_rec less f γ l ll) k (case β of None ⇒ v | Some x ⇒ g k v x) (ord.rbt_union_swap_rec less f γ r rr),
      rbt_join (ord.rbt_union_swap_rec less' f' γ' l' ll') k' (case β' of None ⇒ v' | Some x ⇒ g' k' v' x) (ord.rbt_union_swap_rec less' f' γ' r' rr')) ∈ ⟨Ra, Rb⟩rbt_rel"
        apply parametricity
        using IH1 IH2 rbt_rel_s fun_rel_g_app split_rel
        by (auto simp: defs elim!: rbt_rel_elims)
    }
    then show ?case
      unfolding ord.rbt_union_swap_rec.simps[of _ _ _ t1] ord.rbt_union_swap_rec.simps[of _ _ _ t1']
      using rbt_rel_fold rbt_rel_s
      by (auto simp: flip1[symmetric] flip2[symmetric] g_def[symmetric] g'_def[symmetric] small_rbt_cong
          split: rbt.splits prod.splits elim: rbt_rel_elims)
  qed
qed

  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]
    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]: 
  "((=), (=))∈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' (<)"
  "(rbt_insert,λk v m. m(k↦v)) 
    ∈ Id → Id → rbt_map_rel' (<) → rbt_map_rel' (<)"
  "(rbt_lookup,λm k. m k) ∈ rbt_map_rel' (<) → Id → ⟨Id⟩option_rel"
  "(rbt_delete,λk m. m|`(-{k})) ∈ Id → rbt_map_rel' (<) → rbt_map_rel' (<)"
  "(rbt_union,(++)) 
    ∈ rbt_map_rel' (<) → rbt_map_rel' (<) → rbt_map_rel' (<)"
  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_wrt_keys_true[simp]: "sorted_wrt (λ(_,_) (_,_). True) l"
  apply (induct l)
  apply auto
  done

(*
lemma (in linorder) rbt_it_linord_impl: 
  "is_map_iterator_linord (rbt_map_rel' (<)) 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_wrt (λ(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_wrt_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' (<)) 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_wrt (λ(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_wrt_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' (<)) 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 (<)) (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 rev_subsetD)
    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 (<)) (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 rev_subsetD)
    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 (<)) (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 rev_subsetD)
    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 (<)"
  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,(<)) ∈ Rk → Rk → Id"
  shows "(ord.rbt_insert less_impl,λk v m. m(k↦v)) ∈ 
    Rk → Rv → ⟨Rk,Rv⟩rbt_map_rel (<) → ⟨Rk,Rv⟩rbt_map_rel (<)"
  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,(<)) ∈ Rk → Rk → Id"
  shows "(ord.rbt_lookup less_impl, λm k. m k) ∈ 
    ⟨Rk,Rv⟩rbt_map_rel (<) → 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,(<)) ∈ Rk → Rk → Id"
  shows "(ord.rbt_delete less_impl, λk m. m |`(-{k})) ∈ 
    Rk → ⟨Rk,Rv⟩rbt_map_rel (<) → ⟨Rk,Rv⟩rbt_map_rel (<)"
  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,(<)) ∈ Rk → Rk → Id"
  shows "(ord.rbt_union less_impl, (++)) ∈ 
    ⟨Rk,Rv⟩rbt_map_rel (<) → ⟨Rk,Rv⟩rbt_map_rel (<) → ⟨Rk,Rv⟩rbt_map_rel (<)"
  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 (<) → ⟨⟨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),(++)) ∈
    ⟨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_wrt (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_wrt (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 (≤) (<), dflt_cmp (≤) (<))∈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 (<))"
  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 (≤) (<)))"

lemmas [autoref_post_simps] = dflt_cmp_inv2 dflt_cmp_2inv

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

lemma [autoref_post_simps]: "ord.rbt_lookup ((<)::_::linorder⇒_) = rbt_lookup"
  unfolding ord.rbt_lookup_def rbt_lookup_def ..

lemma [simp,autoref_post_simps]:
  "ord.rbt_insert_with_key (<) = rbt_insert_with_key"
  "ord.rbt_insert (<) = 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, (=)) ∈ 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