Theory Collections.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(e↦a) ≡ 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,Ia⟩⇩ii_prio"
  "op_uprio_prio ::⇩i ⟨Ie,Ia⟩⇩ii_prio →⇩i Ie →⇩i ⟨Ia⟩⇩ii_option"
  "op_uprio_is_empty ::⇩i ⟨Ie,Ia⟩⇩ii_prio →⇩i i_bool"
  "op_uprio_insert ::⇩i ⟨Ie,Ia⟩⇩ii_prio →⇩i Ie →⇩i Ia →⇩i ⟨Ie,Ia⟩⇩ii_prio"
  "prio_pop_min ::⇩i ⟨Ie,Ia⟩⇩ii_prio →⇩i ⟨⟨Ie,⟨Ia,⟨Ie,Ia⟩⇩ii_prio⟩⇩ii_prod⟩⇩ii_prod⟩⇩ii_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,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]: 
    "⋀Re Ra. ⟦Range Re = UNIV; single_valued Ra⟧ ⟹ single_valued (⟨Re,Ra⟩rel)"
    unfolding rel_def by tagged_solver

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


lemma (in uprio) rel_alt: "⟨Id,Rv⟩rel = 
  { (c,a). ∀x. (α c x,a x)∈⟨Rv⟩option_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,Ra⟩rel"
  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,Ra⟩rel→bool_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,Ra⟩rel→Re→⟨Ra⟩option_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,Ra⟩rel→Re→Ra→⟨Re,Ra⟩rel"
  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,Ra⟩rel→⟨⟨Re,⟨Ra,⟨Re,Ra⟩rel⟩prod_rel⟩prod_rel⟩nres_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 ⟨R⟩set_rel"
  lemma rel_def: "⟨R⟩rel ≡ br α invar O ⟨R⟩set_rel" 
    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 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,Rv⟩rel ≡ br α invar O (Rk → ⟨Rv⟩ 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 Rk = UNIV; single_valued Rv⟧ ⟹ single_valued (⟨Rk,Rv⟩rel)"
    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 (), {}) ∈ ⟨Rk⟩rel"
  by (simp add: br_def empty_correct)

lemma (in set_memb) memb_autoref[autoref_rules]: 
  "PREFER_id Rk ⟹ (memb,(∈))∈Rk→⟨Rk⟩rel→Id"
  apply simp
  by (auto simp add: memb_correct br_def)

lemma (in set_ins) ins_autoref[autoref_rules]: 
  "PREFER_id Rk ⟹ (ins,Set.insert)∈Rk→⟨Rk⟩rel→⟨Rk⟩rel"
  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')∈⟨Rk⟩rel"
  shows "(ins_dj x s,(OP Set.insert ::: Rk → ⟨Rk⟩rel → ⟨Rk⟩rel)$x'$s')∈⟨Rk⟩rel"
  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)∈Rk→⟨Rk⟩rel→⟨Rk⟩rel"
  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) ∈ ⟨Rk⟩rel→Id"
  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) ∈ ⟨Rk⟩rel→Id"
  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) ∈ ⟨Rk⟩rel→(Rk→Id)→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) ∈ ⟨Rk⟩rel→(Rk→Id)→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) ∈ ⟨Rk⟩rel → 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 → ⟨Rk⟩rel → 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,(∪))∈⟨Rk⟩s1.rel→⟨Rk⟩s2.rel→⟨Rk⟩s3.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')∈⟨Rk⟩s1.rel"
  assumes "(b,b')∈⟨Rk⟩s2.rel"
  shows "(union_dj a b,(OP (∪) ::: ⟨Rk⟩s1.rel → ⟨Rk⟩s2.rel → ⟨Rk⟩s3.rel)$a'$b')
    ∈⟨Rk⟩s3.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,(-))∈⟨Rk⟩s1.rel→⟨Rk⟩s2.rel→⟨Rk⟩s1.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) → ⟨Rk⟩s1.rel→⟨Rk⟩s2.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,(∩))∈⟨Rk⟩s1.rel→⟨Rk⟩s2.rel→⟨Rk⟩s3.rel"
  by simp (auto simp add: inter_correct br_def)

lemma (in set_subset) subset_autoref[autoref_rules]: 
  "PREFER_id Rk ⟹ (subset,(⊆))∈⟨Rk⟩s1.rel→⟨Rk⟩s2.rel→Id"
  by simp (auto simp add: subset_correct br_def)

lemma (in set_equal) equal_autoref[autoref_rules]: 
  "PREFER_id Rk ⟹ (equal,(=))∈⟨Rk⟩s1.rel→⟨Rk⟩s2.rel→Id"
  by simp (auto simp add: equal_correct br_def)

lemma (in set_disjoint) disjoint_autoref[autoref_rules]: 
  "PREFER_id Rk ⟹ (disjoint,op_set_disjoint)∈⟨Rk⟩s1.rel→⟨Rk⟩s2.rel→Id"
  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)∈⟨Rk⟩list_rel → ⟨Rk⟩rel"
  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')∈⟨Rk⟩rel"
  shows "(RETURN (the (sel' s (λ_. True))), 
          (OP op_set_pick ::: ⟨Rk⟩rel → ⟨Rk⟩nres_rel) $ s')
    ∈ ⟨Rk⟩nres_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,Rv⟩rel = 
  { (c,a). ∀x. (α c x,a x)∈⟨Rv⟩option_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,Rv⟩rel"
  by (auto simp: empty_correct rel_alt)
  
lemma (in map_lookup) lookup_autoref[autoref_rules]: 
  "PREFER_id Rk ⟹ (lookup,op_map_lookup)∈Rk→⟨Rk,Rv⟩rel→⟨Rv⟩option_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)∈Rk→Rv→⟨Rk,Rv⟩rel→⟨Rk,Rv⟩rel"
  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,Rv⟩rel"
  shows "(update_dj k v m,
    (OP op_map_update ::: Rk → Rv → ⟨Rk,Rv⟩rel → ⟨Rk,Rv⟩rel)$k'$v'$m'
  )∈⟨Rk,Rv⟩rel"
  using assms
  apply (subgoal_tac "k∉dom (α 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)∈Rk→⟨Rk,Rv⟩rel→⟨Rk,Rv⟩rel"
  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,Rv⟩prod_rel → Id) → ⟨Rk,Rv⟩m1.rel → ⟨Rk,Rv⟩m2.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,Rv⟩rel→⟨Rk,Rv⟩rel→⟨Rk,Rv⟩rel"
  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,Rv⟩rel"
  assumes "(b,b')∈⟨Rk,Rv⟩rel"
  shows "(add_dj a b, (OP (++) ::: ⟨Rk,Rv⟩rel → ⟨Rk,Rv⟩rel → ⟨Rk,Rv⟩rel) $ a' $ b')∈⟨Rk,Rv⟩rel"
  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,Rv⟩rel→Id"
  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 = [k↦v]"
  using assms
  by (auto intro!: ext)

lemma (in map_isSng) isSng_autoref[autoref_rules]: 
  "PREFER_id Rk ⟹ (isSng,op_map_isSng)∈⟨Rk,Rv⟩rel→Id"
  (* 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,Rv⟩rel→(⟨Rk,Rv⟩prod_rel→Id)→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,Rv⟩rel→(⟨Rk,Rv⟩prod_rel→Id)→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,Rv⟩rel→Id"
  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)∈Id→⟨Rk,Rv⟩rel→Id"
  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,Rv⟩prod_rel⟩list_rel → ⟨Rk,Rv⟩rel"
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,Rv⟩prod_rel⟩list_rel"
  thus "(to_map l, map_of l') ∈ ⟨Rk,Rv⟩rel"
    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