Theory ICF_Autoref

section ‹ICF-setup for Automatic Refinement›
theory ICF_Autoref
imports 
  ICF_Refine_Monadic 
  "../GenCF/Intf/Intf_Set"
  "../GenCF/Intf/Intf_Map"
begin

subsection ‹Unique Priority Queue›
consts i_prio :: "interface  interface  interface"
definition [simp]: "op_uprio_empty  Map.empty"
definition [simp]: "op_uprio_is_empty x  x = Map.empty"
definition [simp]: "op_uprio_insert s e a  s(e  a)"
definition op_uprio_prio :: "('e'a)'e'a"
  where [simp]: "op_uprio_prio s e  s e"

(* FIXME: Tune id-(phase) such that it can distinguish those patterns!
  For now: Only include this patterns on demand!
*)
context begin interpretation autoref_syn .

lemma uprio_pats:
  fixes s :: "'e'a"
  shows
  "Map.empty::'e'a  op_uprio_empty"
  "s e  op_uprio_prio$s$e"
  "s(ea)  op_uprio_insert$s$e$a"

  "dom s = {}  op_uprio_is_empty$s"
  "{} = dom s  op_uprio_is_empty$s"
  "s=Map.empty  op_uprio_is_empty$s"
  "Map.empty=s  op_uprio_is_empty$s"
  by (auto intro!: eq_reflection)

end

term prio_pop_min

lemma [autoref_itype]:
  "op_uprio_empty ::i Ie,Iaii_prio"
  "op_uprio_prio ::i Ie,Iaii_prio i Ie i Iaii_option"
  "op_uprio_is_empty ::i Ie,Iaii_prio i i_bool"
  "op_uprio_insert ::i Ie,Iaii_prio i Ie i Ia i Ie,Iaii_prio"
  "prio_pop_min ::i Ie,Iaii_prio i Ie,Ia,Ie,Iaii_prioii_prodii_prodii_nres"
  by simp_all

context uprio begin
  definition rel_def_internal: 
    "Re Ra. rel Re Ra  br α invar O (Re  Ra option_rel)"
  lemma rel_def:
    "Re Ra. Re,Rarel  br α invar O (Re  Ra option_rel)" 
    by (simp add: rel_def_internal relAPP_def)
    
  lemma rel_id[simp]: "Id,Idrel = br α invar" 
    by (simp add: rel_def)

  lemma rel_sv[relator_props]: 
    "Re Ra. Range Re = UNIV; single_valued Ra  single_valued (Re,Rarel)"
    unfolding rel_def by tagged_solver

  lemmas [autoref_rel_intf] = REL_INTFI[of rel i_prio]
end


lemma (in uprio) rel_alt: "Id,Rvrel = 
  { (c,a). x. (α c x,a x)Rvoption_rel  invar c }"
  by (auto simp: rel_def br_def dest: fun_relD)

lemma (in uprio_empty) autoref_empty[autoref_rules]:
  "Re Ra. PREFER_id Re  (empty (),op_uprio_empty)Re,Rarel"
  by (auto simp: empty_correct rel_alt)

lemma (in uprio_isEmpty) autoref_is_empty[autoref_rules]:
  "Re Ra. PREFER_id Re  (isEmpty,op_uprio_is_empty)Re,Rarelbool_rel"
  by (auto simp: isEmpty_correct rel_alt intro!: ext)

lemma (in uprio_prio) autoref_prio[autoref_rules]:
  "Re Ra. PREFER_id Re  (prio,op_uprio_prio)Re,RarelReRaoption_rel"
  by (auto simp: prio_correct rel_alt intro!: ext)

lemma (in uprio_insert) autoref_insert[autoref_rules]:
  "Re Ra. PREFER_id Re  (insert,op_uprio_insert)Re,RarelReRaRe,Rarel"
  by (auto simp: insert_correct rel_alt intro!: ext)

lemma (in uprio_pop) autoref_prio_pop_min[autoref_rules]:
  "Re Ra. PREFER_id Re; PREFER_id Ra  
   (λs. RETURN (pop s),prio_pop_min)Re,RarelRe,Ra,Re,Rarelprod_relprod_relnres_rel"
  apply simp
  apply (intro fun_relI nres_relI)
  by (rule prio_pop_min_refine)




context set begin
  definition rel_def_internal: "rel R  br α invar O Rset_rel"
  lemma rel_def: "Rrel  br α invar O Rset_rel" 
    by (simp add: rel_def_internal relAPP_def)
    
  lemma rel_id[simp]: "Idrel = br α invar" by (simp add: rel_def)

  lemma rel_sv[relator_props]: "single_valued R  single_valued (Rrel)"
    unfolding rel_def by tagged_solver

  lemmas [autoref_rel_intf] = REL_INTFI[of rel i_set]

end

context map begin
  definition rel_def_internal: 
    "rel Rk Rv  br α invar O (Rk  Rv option_rel)"
  lemma rel_def: 
    "Rk,Rvrel  br α invar O (Rk  Rv option_rel)" 
    by (simp add: rel_def_internal relAPP_def)
    
  lemma rel_id[simp]: "Id,Idrel = br α invar" 
    by (simp add: rel_def)

  lemma rel_sv[relator_props]: 
    "Range Rk = UNIV; single_valued Rv  single_valued (Rk,Rvrel)"
    unfolding rel_def 
    by (tagged_solver (trace))

  lemmas [autoref_rel_intf] = REL_INTFI[of rel i_map]

end


(*
context list begin
  definition rel_def_internal: 
    "rel R ≡ br α invar O R"
  lemma rel_def: "⟨R⟩rel ≡ br α invar O R" 
    by (simp add: rel_def_internal relAPP_def)
    
  lemma rel_id[simp]: "⟨Id⟩rel = br α invar" 
    by (simp add: rel_def)

  lemma rel_sv[relator_props]: "single_valued R ⟹ single_valued (⟨R⟩rel)"
    unfolding rel_def by refine_post
end

context al begin
  definition rel_def_internal: 
    "rel Re Ra ≡ br α invar O ⟨⟨Re,Ra⟩ prod_rel⟩list_rel"
  lemma rel_def: 
    "⟨Re,Ra⟩rel ≡ br α invar O ⟨⟨Re,Ra⟩ prod_rel⟩list_rel" 
    by (simp add: rel_def_internal relAPP_def)
    
  lemma rel_id[simp]: "⟨Id,Id⟩rel = br α invar" 
    by (simp add: rel_def)

  lemma rel_sv[relator_props]: 
    "⟦single_valued Re; single_valued Ra⟧ ⟹ single_valued (⟨Re,Ra⟩rel)"
    unfolding rel_def by refine_post

end

context prio begin
  (* TODO: Fix that to use multiset_rel! *)
  definition rel_def[simp]: "rel ≡ br α invar"
  lemma rel_sv: "single_valued rel" unfolding rel_def by refine_post
end

context uprio begin
  definition rel_def_internal: 
    "rel Re Ra ≡ br α invar O (Re → ⟨Ra⟩ option_rel)"
  lemma rel_def:
    "⟨Re,Ra⟩rel ≡ br α invar O (Re → ⟨Ra⟩ option_rel)" 
    by (simp add: rel_def_internal relAPP_def)
    
  lemma rel_id[simp]: "⟨Id,Id⟩rel = br α invar" 
    by (simp add: rel_def)

  lemma rel_sv[relator_props]: 
    "⟦Range Re = UNIV; single_valued Ra⟧ ⟹ single_valued (⟨Re,Ra⟩rel)"
    unfolding rel_def by refine_post

end
*)


setup Revert_Abbrev.revert_abbrev "Autoref_Binding_ICF.*.rel"




(* TODO: Move *)
lemma Collect_x_x_pairs_rel_image[simp]: "{p. x. p = (x, x)}``x = x" 
    by auto


subsection "Set"

lemma (in set_empty) empty_autoref[autoref_rules]: 
  "PREFER_id Rk  (empty (), {})  Rkrel"
  by (simp add: br_def empty_correct)

lemma (in set_memb) memb_autoref[autoref_rules]: 
  "PREFER_id Rk  (memb,(∈))RkRkrelId"
  apply simp
  by (auto simp add: memb_correct br_def)

lemma (in set_ins) ins_autoref[autoref_rules]: 
  "PREFER_id Rk  (ins,Set.insert)RkRkrelRkrel"
  by simp (auto simp add: ins_correct br_def)

context set_ins_dj begin
context begin interpretation autoref_syn .
lemma ins_dj_autoref[autoref_rules]: 
  assumes "SIDE_PRECOND_OPT (x's')"
  assumes "PREFER_id Rk"
  assumes "(x,x')Rk"
  assumes "(s,s')Rkrel"
  shows "(ins_dj x s,(OP Set.insert ::: Rk  Rkrel  Rkrel)$x'$s')Rkrel"
  using assms 
  apply simp
  apply (auto simp add: ins_dj_correct br_def)
  done
end
end

lemma (in set_delete) delete_autoref[autoref_rules]: 
  "PREFER_id Rk  (delete,op_set_delete)RkRkrelRkrel"
  by simp (auto simp add: delete_correct op_set_delete_def br_def)
 
lemma (in set_isEmpty) isEmpty_autoref[autoref_rules]: 
  "PREFER_id Rk  (isEmpty,op_set_isEmpty)  RkrelId"
  apply (simp add: br_def)
  apply (fastforce simp: isEmpty_correct)
  done

lemma (in set_isSng) isSng_autoref[autoref_rules]: 
  "PREFER_id Rk  (isSng,op_set_isSng)  RkrelId"
  by simp
    (auto simp add: isSng_correct op_set_isSng_def br_def card_Suc_eq)

lemma (in set_ball) ball_autoref[autoref_rules]: 
  "PREFER_id Rk  (ball,Set.Ball)  Rkrel(RkId)Id"
  by simp (auto simp add: ball_correct fun_rel_def br_def)

lemma (in set_bex) bex_autoref[autoref_rules]: 
  "PREFER_id Rk  (bex,Set.Bex)  Rkrel(RkId)Id"
  apply simp
  apply (auto simp: bex_correct fun_rel_def br_def intro!: ext)
  done

lemma (in set_size) size_autoref[autoref_rules]: 
  "PREFER_id Rk  (size,card)  Rkrel  Id"
  by simp (auto simp add: size_correct br_def)

lemma (in set_size_abort) size_abort_autoref[autoref_rules]: 
  "PREFER_id Rk  (size_abort,op_set_size_abort)  Id  Rkrel  Id"
  by simp
    (auto simp add: size_abort_correct op_set_size_abort_def br_def)

lemma (in set_union) union_autoref[autoref_rules]: 
  "PREFER_id Rk  (union,(∪))Rks1.relRks2.relRks3.rel"
  by simp (auto simp add: union_correct br_def)

context set_union_dj begin
context begin interpretation autoref_syn .

lemma union_dj_autoref[autoref_rules]:
  assumes "PREFER_id Rk"
  assumes "SIDE_PRECOND_OPT (a'b'={})"
  assumes "(a,a')Rks1.rel"
  assumes "(b,b')Rks2.rel"
  shows "(union_dj a b,(OP (∪) ::: Rks1.rel  Rks2.rel  Rks3.rel)$a'$b')
    Rks3.rel"
  using assms 
  by simp (auto simp: union_dj_correct br_def)
end 
end

lemma (in set_diff) diff_autoref[autoref_rules]: 
  "PREFER_id Rk  (diff,(-))Rks1.relRks2.relRks1.rel"
  by simp (auto simp add: diff_correct br_def)

lemma (in set_filter) filter_autoref[autoref_rules]: 
  "PREFER_id Rk  (filter,op_set_filter)(Rk  Id)  Rks1.relRks2.rel"
  by simp (auto simp add: filter_correct op_set_filter_def fun_rel_def 
    br_def)

lemma (in set_inter) inter_autoref[autoref_rules]: 
  "PREFER_id Rk  (inter,(∩))Rks1.relRks2.relRks3.rel"
  by simp (auto simp add: inter_correct br_def)

lemma (in set_subset) subset_autoref[autoref_rules]: 
  "PREFER_id Rk  (subset,(⊆))Rks1.relRks2.relId"
  by simp (auto simp add: subset_correct br_def)

lemma (in set_equal) equal_autoref[autoref_rules]: 
  "PREFER_id Rk  (equal,(=))Rks1.relRks2.relId"
  by simp (auto simp add: equal_correct br_def)

lemma (in set_disjoint) disjoint_autoref[autoref_rules]: 
  "PREFER_id Rk  (disjoint,op_set_disjoint)Rks1.relRks2.relId"
  by simp (auto simp add: disjoint_correct op_set_disjoint_def br_def)

lemma (in list_to_set) to_set_autoref[autoref_rules]: 
  "PREFER_id Rk  (to_set,set)Rklist_rel  Rkrel"
  apply simp
  apply (auto simp add: to_set_correct br_def)
  done

context set_sel' begin
context begin interpretation autoref_syn .

lemma autoref_op_set_pick[autoref_rules]: 
  assumes "SIDE_PRECOND (s'{})"
  assumes "PREFER_id Rk"
  assumes "(s,s')Rkrel"
  shows "(RETURN (the (sel' s (λ_. True))), 
          (OP op_set_pick ::: Rkrel  Rknres_rel) $ s')
     Rknres_rel"
  using assms
  apply (clarsimp simp add: br_def nres_rel_def ex_in_conv[symmetric])
  apply (erule (1) sel'E[OF _ _ TrueI])
  apply (auto intro: RES_refine)
  done
end
end

lemma (in poly_set_iteratei) proper[proper_it]:
  "proper_it' iteratei iteratei"
  apply (rule proper_it'I)
  by (rule pi_iteratei)

lemma (in poly_set_iteratei) autoref_iteratei[autoref_ga_rules]: 
  "REL_IS_ID Rk  is_set_to_list Rk rel (it_to_list iteratei)"
  unfolding is_set_to_list_def is_set_to_sorted_list_def it_to_list_def 
    it_to_sorted_list_def
  apply (simp add: br_def, intro allI impI)
  apply (drule iteratei_correct)
  unfolding set_iterator_def set_iterator_genord_foldli_conv
  apply (elim exE)
  apply clarsimp
  apply (drule fun_cong[where x="λ_::'x list. True"])
  apply simp
  done

lemma (in poly_set_iterateoi) proper_o[proper_it]:
  "proper_it' iterateoi iterateoi"
  apply (rule proper_it'I)
  by (rule pi_iterateoi)

lemma (in poly_set_iterateoi) autoref_iterateoi[autoref_ga_rules]: 
  "REL_IS_ID Rk  
    is_set_to_sorted_list (≤) Rk rel (it_to_list iterateoi)"
  unfolding is_set_to_sorted_list_def it_to_list_def it_to_sorted_list_def
  apply (simp add: br_def, intro allI impI)
  apply (drule iterateoi_correct)
  unfolding set_iterator_linord_def set_iterator_genord_foldli_conv
  apply (elim exE)
  apply clarsimp
  apply (drule fun_cong[where x="λ_::'x list. True"])
  apply simp
  done

lemma (in poly_set_rev_iterateoi) autoref_rev_iterateoi[autoref_ga_rules]: 
  "REL_IS_ID Rk  
    is_set_to_sorted_list (≥) Rk rel (it_to_list rev_iterateoi)"
  unfolding is_set_to_sorted_list_def it_to_list_def it_to_sorted_list_def
  apply (simp add: br_def, intro allI impI)
  apply (drule rev_iterateoi_correct)
  unfolding set_iterator_rev_linord_def set_iterator_genord_foldli_conv
  apply (elim exE)
  apply clarsimp
  apply (drule fun_cong[where x="λ_::'x list. True"])
  apply simp
  done

lemma (in poly_set_rev_iterateoi) proper_ro[proper_it]:
  "proper_it' rev_iterateoi rev_iterateoi"
  apply (rule proper_it'I)
  by (rule pi_rev_iterateoi)

subsection "Map"

lemma (in map) rel_alt: "Id,Rvrel = 
  { (c,a). x. (α c x,a x)Rvoption_rel  invar c }"
  by (auto simp: rel_def br_def dest: fun_relD)

lemma (in map_empty) empty_autoref[autoref_rules]: 
  "PREFER_id Rk  (empty (),op_map_empty)Rk,Rvrel"
  by (auto simp: empty_correct rel_alt)
  
lemma (in map_lookup) lookup_autoref[autoref_rules]: 
  "PREFER_id Rk  (lookup,op_map_lookup)RkRk,RvrelRvoption_rel"
  apply (intro fun_relI option_relI)
  apply (auto simp: lookup_correct rel_alt
    dest: fun_relD2)
  done

lemma (in map_update) update_autoref[autoref_rules]: 
  "PREFER_id Rk  (update,op_map_update)RkRvRk,RvrelRk,Rvrel"
  apply (intro fun_relI)
  apply (simp add: update_correct rel_alt)
  done

context map_update_dj begin
context begin interpretation autoref_syn .

lemma update_dj_autoref[autoref_rules]: 
  assumes "SIDE_PRECOND_OPT (k'dom m')"
  assumes "PREFER_id Rk"
  assumes "(k,k')Rk"
  assumes "(v,v')Rv"
  assumes "(m,m')Rk,Rvrel"
  shows "(update_dj k v m,
    (OP op_map_update ::: Rk  Rv  Rk,Rvrel  Rk,Rvrel)$k'$v'$m'
  )Rk,Rvrel"
  using assms
  apply (subgoal_tac "kdom (α m)")
  apply (simp add: update_dj_correct rel_alt)
  apply (auto simp add: rel_alt option_rel_def)
  apply (metis option.simps(3))
  done
end
end

lemma (in map_delete) delete_autoref[autoref_rules]: 
  "PREFER_id Rk  (delete,op_map_delete)RkRk,RvrelRk,Rvrel"
  apply (intro fun_relI)
  apply (simp add: delete_correct restrict_map_def rel_alt)
  done

lemma (in map_restrict) restrict_autoref[autoref_rules]: 
  "PREFER_id Rk  
    (restrict,op_map_restrict) 
     (Rk,Rvprod_rel  Id)  Rk,Rvm1.rel  Rk,Rvm2.rel"
  apply (intro fun_relI)
  apply (simp add: restrict_correct br_comp_alt m1.rel_def m2.rel_def )
  apply (intro fun_relI)
  apply (auto simp: restrict_map_def split: if_split_asm)
  apply (drule (1) fun_relD1)
  apply (auto simp: option_rel_def) []
  apply (drule (1) fun_relD1)
  apply (auto simp: option_rel_def) []
  apply (drule (1) fun_relD1)
  apply (auto simp: option_rel_def prod_rel_def fun_rel_def) []
  apply (drule (1) fun_relD2)
  apply (auto simp: option_rel_def prod_rel_def fun_rel_def) []
  done

lemma (in map_add) add_autoref[autoref_rules]: 
  "PREFER_id Rk  (add,(++))Rk,RvrelRk,RvrelRk,Rvrel"
  apply (auto simp add: add_correct rel_alt Map.map_add_def
    split: option.split)
  apply (drule_tac x=x in spec)+
  apply simp
  apply (metis option.simps(3) option_rel_simp(2))
  by (metis (lifting) option_rel_simp(3))


context map_add_dj begin
context begin interpretation autoref_syn .

lemma add_dj_autoref[autoref_rules]: 
  assumes "PREFER_id Rk"
  assumes "SIDE_PRECOND_OPT (dom a'  dom b' = {})"
  assumes "(a,a')Rk,Rvrel"
  assumes "(b,b')Rk,Rvrel"
  shows "(add_dj a b, (OP (++) ::: Rk,Rvrel  Rk,Rvrel  Rk,Rvrel) $ a' $ b')Rk,Rvrel"
  using assms
  apply simp
  apply (subgoal_tac "dom (α a)  dom (α b) = {}")
  apply (clarsimp simp add: add_dj_correct rel_def br_comp_alt)
  apply (auto 
    simp add: rel_def br_comp_alt Map.map_add_def
    split: option.split
    elim: fun_relE1 dest: fun_relD1 intro: option_relI
  ) []

  apply (clarsimp simp add: rel_def br_comp_alt)

  apply (auto simp: dom_def)
  apply (drule (1) fun_relD1)
  apply (drule (1) fun_relD1)
  apply (auto simp: option_rel_def)
  done
end
end

lemma (in map_isEmpty) isEmpty_autoref[autoref_rules]: 
  "PREFER_id Rk  (isEmpty,op_map_isEmpty)Rk,RvrelId"
  by (auto simp: isEmpty_correct rel_alt
    intro!: ext)

lemma sngI: 
  assumes "m k = Some v"
  assumes "k'. k'k  m k' = None"
  shows "m = [kv]"
  using assms
  by (auto intro!: ext)

lemma (in map_isSng) isSng_autoref[autoref_rules]: 
  "PREFER_id Rk  (isSng,op_map_isSng)Rk,RvrelId"
  (* TODO: Clean up this mess *)
  apply (auto simp add: isSng_correct rel_alt)
  apply (rule_tac x=k in exI)
  apply (rule_tac x="the (a' k)" in exI)
  apply (rule sngI)
  apply (drule_tac x=k in spec)
  apply (auto elim: option_relE) []
  apply (force elim: option_relE) []

  apply (rule_tac x=k in exI)
  apply (rule_tac x="the (α a k)" in exI)
  apply (rule sngI)
  apply (drule_tac x=k in spec)
  apply (auto elim: option_relE) []
  apply (force elim: option_relE) []
  done

lemma (in map_ball) ball_autoref[autoref_rules]:
  "PREFER_id Rk  (ball,op_map_ball)Rk,Rvrel(Rk,Rvprod_relId)Id"
  apply (auto simp: ball_correct rel_alt map_to_set_def
    option_rel_def prod_rel_def fun_rel_def)
  apply (metis option.inject option.simps(3))+
  done

lemma (in map_bex) bex_autoref[autoref_rules]:
  "PREFER_id Rk  (bex,op_map_bex)Rk,Rvrel(Rk,Rvprod_relId)Id"
  apply (auto simp: bex_correct map_to_set_def rel_alt 
    option_rel_def prod_rel_def fun_rel_def)
  apply (metis option.inject option.simps(3))+
  done

lemma (in map_size) size_autoref[autoref_rules]:
  "PREFER_id Rk  (size,op_map_size)Rk,RvrelId"
  apply (auto simp: size_correct rel_alt option_rel_def dom_def 
    intro!: arg_cong[where f=card])
  apply (metis option.simps(3))+
  done

lemma (in map_size_abort) size_abort_autoref[autoref_rules]:
  "PREFER_id Rk  (size_abort,op_map_size_abort)IdRk,RvrelId"
  apply (auto simp: size_abort_correct  
    rel_alt option_rel_def
    dom_def intro!: arg_cong[where f=card] cong[OF arg_cong[where f=min]])
  apply (metis option.simps(3))+
  done

lemma (in list_to_map) to_map_autoref[autoref_rules]:
  "PREFER_id Rk  (to_map,map_of) Rk,Rvprod_rellist_rel  Rk,Rvrel"
proof (intro fun_relI)
  fix l :: "('u×'v) list" and l' :: "('u×'a) list"
  assume "PREFER_id Rk" hence [simp]: "Rk=Id" by simp
  assume "(l,l')Rk,Rvprod_rellist_rel"
  thus "(to_map l, map_of l')  Rk,Rvrel"
    apply (simp add: list_rel_def)
  proof (induct rule: list_all2_induct)
    case Nil thus ?case 
      by (auto simp add: to_map_correct rel_alt)
  next
    case (Cons x x' l l') thus ?case
      by (auto simp add: to_map_correct 
        rel_alt prod_rel_def)
  qed
qed

(* TODO: Move *)
lemma key_rel_true[simp]: "key_rel (λ_ _. True) = (λ_ _. True)"
  by (auto intro!: ext simp: key_rel_def)


lemma (in poly_map_iteratei) proper[proper_it]:
  "proper_it' iteratei iteratei"
  apply (rule proper_it'I)
  by (rule pi_iteratei)

lemma (in poly_map_iteratei) autoref_iteratei[autoref_ga_rules]: 
  assumes ID: "REL_IS_ID Rk"
    "REL_IS_ID Rv" (* TODO: Unnecessary*)
  shows "is_map_to_list Rk Rv rel (it_to_list iteratei)"
proof -
  from ID have [simp]: "Rk=Id" "Rv = Id" by simp_all

  show ?thesis
    unfolding is_map_to_sorted_list_def is_map_to_list_def
      it_to_sorted_list_def
    apply simp
    apply (intro allI impI conjI)
  proof -
    fix m m'
    assume "(m, m')  br α invar"
    hence I: "invar m" and M': "m' = α m" by (simp_all add: br_def)

    have [simp]: "c. (λ(_,_). c) = (λ_. c)" by auto

    from map_it_to_list_genord_correct[where it = iteratei, 
      where R="λ_ _. True", simplified, OF 
      iteratei_correct[OF I, unfolded set_iterator_def]
    ] have 
        M: "Map.map_of (it_to_list iteratei m) = α m"
        and D: "distinct (List.map fst (it_to_list iteratei m))"
      by (simp_all)

    from D show "distinct (it_to_list iteratei m)"
      by (rule distinct_mapI)

    from M show "map_to_set m' = set (it_to_list iteratei m)"
      by (simp add: M' map_of_map_to_set[OF D])
  qed
qed

lemma (in poly_map_iterateoi) proper_o[proper_it]:
  "proper_it' iterateoi iterateoi"
  apply (rule proper_it'I)
  by (rule pi_iterateoi)

lemma (in poly_map_iterateoi) autoref_iterateoi[autoref_ga_rules]: 
  assumes ID: "REL_IS_ID Rk"
    "REL_IS_ID Rv" (* TODO: Unnecessary*)
  shows "is_map_to_sorted_list (≤) Rk Rv rel (it_to_list iterateoi)"
proof -
  from ID have [simp]: "Rk=Id" "Rv = Id" by simp_all

  show ?thesis
    unfolding is_map_to_sorted_list_def
      it_to_sorted_list_def
    apply simp
    apply (intro allI impI conjI)
  proof -
    fix m m'
    assume "(m, m')  br α invar"
    hence I: "invar m" and M': "m' = α m" by (simp_all add: br_def)

    have [simp]: "c. (λ(_,_). c) = (λ_. c)" by auto

    from map_it_to_list_linord_correct[where it = iterateoi, 
      OF iterateoi_correct[OF I]
    ] have 
        M: "map_of (it_to_list iterateoi m) = α m"
        and D: "distinct (map fst (it_to_list iterateoi m))"
        and S: "sorted (map fst (it_to_list iterateoi m))"
      by (simp_all)

    from D show "distinct (it_to_list iterateoi m)"
      by (rule distinct_mapI)

    from M show "map_to_set m' = set (it_to_list iterateoi m)"
      by (simp add: M' map_of_map_to_set[OF D])

    from S show "sorted_wrt (key_rel (≤)) (it_to_list iterateoi m)"
      by (simp add: key_rel_def[abs_def])

  qed
qed

lemma (in poly_map_rev_iterateoi) proper_ro[proper_it]:
  "proper_it' rev_iterateoi rev_iterateoi"
  apply (rule proper_it'I)
  by (rule pi_rev_iterateoi)

lemma (in poly_map_rev_iterateoi) autoref_rev_iterateoi[autoref_ga_rules]: 
  assumes ID: "REL_IS_ID Rk"
    "REL_IS_ID Rv" (* TODO: Unnecessary*)
  shows "is_map_to_sorted_list (≥) Rk Rv rel (it_to_list rev_iterateoi)"
proof -
  from ID have [simp]: "Rk=Id" "Rv = Id" by simp_all

  show ?thesis
    unfolding is_map_to_sorted_list_def
      it_to_sorted_list_def
    apply simp
    apply (intro allI impI conjI)
  proof -
    fix m m'
    assume "(m, m')  br α invar"
    hence I: "invar m" and M': "m' = α m" by (simp_all add: br_def)

    have [simp]: "c. (λ(_,_). c) = (λ_. c)" by auto

    from map_it_to_list_rev_linord_correct[where it = rev_iterateoi, 
      OF rev_iterateoi_correct[OF I]
    ] have 
        M: "map_of (it_to_list rev_iterateoi m) = α m"
        and D: "distinct (map fst (it_to_list rev_iterateoi m))"
        and S: "sorted (rev (map fst (it_to_list rev_iterateoi m)))"
      by (simp_all)

    from D show "distinct (it_to_list rev_iterateoi m)"
      by (rule distinct_mapI)

    from M show "map_to_set m' = set (it_to_list rev_iterateoi m)"
      by (simp add: M' map_of_map_to_set[OF D])

    from S show "sorted_wrt (key_rel (≥)) (it_to_list rev_iterateoi m)"
      by (simp add: key_rel_def[abs_def])

  qed
qed

end