# Theory Digraph_Impl

```section ‹Implementing Graphs›
(* Author: Peter Lammich *)
theory Digraph_Impl
imports Digraph
begin

subsection ‹Directed Graphs by Successor Function›
type_synonym 'a slg = "'a ⇒ 'a list"

definition slg_rel :: "('a×'b) set ⇒ ('a slg × 'b digraph) set" where
slg_rel_def_internal: "slg_rel R ≡
(R → ⟨R⟩list_set_rel) O br (λsuccs. {(u,v). v∈succs u}) (λ_. True)"

lemma slg_rel_def: "⟨R⟩slg_rel =
(R → ⟨R⟩list_set_rel) O br (λsuccs. {(u,v). v∈succs u}) (λ_. True)"
unfolding slg_rel_def_internal relAPP_def by simp

lemma slg_rel_sv[relator_props]:
"⟦single_valued R; Range R = UNIV⟧ ⟹ single_valued (⟨R⟩slg_rel)"
unfolding slg_rel_def
by (tagged_solver)

consts i_slg :: "interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of slg_rel i_slg]

definition [simp]: "op_slg_succs E v ≡ E``{v}"

lemma [autoref_itype]: "op_slg_succs ::⇩i ⟨I⟩⇩ii_slg →⇩i I →⇩i ⟨I⟩⇩ii_set" by simp

context begin interpretation autoref_syn .
lemma [autoref_op_pat]: "E``{v} ≡ op_slg_succs\$E\$v" by simp
end

lemma refine_slg_succs[autoref_rules_raw]:
"(λsuccs v. succs v,op_slg_succs)∈⟨R⟩slg_rel→R→⟨R⟩list_set_rel"
apply (intro fun_relI)
apply (auto simp add: slg_rel_def br_def dest: fun_relD)
done

definition "E_of_succ succ ≡ { (u,v). v∈succ u }"
definition "succ_of_E E ≡ (λu. {v . (u,v)∈E})"

lemma E_of_succ_of_E[simp]: "E_of_succ (succ_of_E E) = E"
unfolding E_of_succ_def succ_of_E_def
by auto

lemma succ_of_E_of_succ[simp]: "succ_of_E (E_of_succ E) = E"
unfolding E_of_succ_def succ_of_E_def
by auto

context begin interpretation autoref_syn .
lemma [autoref_itype]: "E_of_succ ::⇩i (I →⇩i ⟨I⟩⇩ii_set) →⇩i ⟨I⟩⇩ii_slg" by simp
lemma [autoref_itype]: "succ_of_E ::⇩i ⟨I⟩⇩ii_slg →⇩i I →⇩i ⟨I⟩⇩ii_set" by simp
end

lemma E_of_succ_refine[autoref_rules]:
"(λx. x, E_of_succ) ∈ (R → ⟨R⟩list_set_rel) → ⟨R⟩slg_rel"
"(λx. x, succ_of_E) ∈ ⟨R⟩slg_rel → (R → ⟨R⟩list_set_rel)"
unfolding E_of_succ_def[abs_def] succ_of_E_def[abs_def] slg_rel_def br_def
apply auto []
apply clarsimp
apply (blast dest: fun_relD)
done

subsubsection ‹Restricting Edges›
definition op_graph_restrict :: "'v set ⇒ 'v set ⇒ ('v × 'v) set ⇒ ('v × 'v) set"
where [simp]: "op_graph_restrict Vl Vr E ≡ E ∩ Vl × Vr"

definition op_graph_restrict_left :: "'v set ⇒ ('v × 'v) set ⇒ ('v × 'v) set"
where [simp]: "op_graph_restrict_left Vl E ≡ E ∩ Vl × UNIV"

definition op_graph_restrict_right :: "'v set ⇒ ('v × 'v) set ⇒ ('v × 'v) set"
where [simp]: "op_graph_restrict_right Vr E ≡ E ∩ UNIV × Vr"

lemma [autoref_op_pat]:
"E ∩ (Vl × Vr) ≡ op_graph_restrict Vl Vr E"
"E ∩ (Vl × UNIV) ≡ op_graph_restrict_left Vl E"
"E ∩ (UNIV × Vr) ≡ op_graph_restrict_right Vr E"
by simp_all

lemma graph_restrict_aimpl: "op_graph_restrict Vl Vr E =
E_of_succ (λv. if v∈Vl then {x ∈ E``{v}. x∈Vr} else {})"
by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm)
lemma graph_restrict_left_aimpl: "op_graph_restrict_left Vl E =
E_of_succ (λv. if v∈Vl then E``{v} else {})"
by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm)
lemma graph_restrict_right_aimpl: "op_graph_restrict_right Vr E =
E_of_succ (λv. {x ∈ E``{v}. x∈Vr})"
by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm)

schematic_goal graph_restrict_impl_aux:
fixes Rsl Rsr
notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set]
assumes [autoref_rules]: "(meml, (∈)) ∈ R → ⟨R⟩Rsl → bool_rel"
assumes [autoref_rules]: "(memr, (∈)) ∈ R → ⟨R⟩Rsr → bool_rel"
shows "(?c, op_graph_restrict) ∈ ⟨R⟩Rsl → ⟨R⟩Rsr → ⟨R⟩slg_rel → ⟨R⟩slg_rel"
unfolding graph_restrict_aimpl[abs_def]
apply (autoref (keep_goal))
done

schematic_goal graph_restrict_left_impl_aux:
fixes Rsl Rsr
notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set]
assumes [autoref_rules]: "(meml, (∈)) ∈ R → ⟨R⟩Rsl → bool_rel"
shows "(?c, op_graph_restrict_left) ∈ ⟨R⟩Rsl → ⟨R⟩slg_rel → ⟨R⟩slg_rel"
unfolding graph_restrict_left_aimpl[abs_def]
apply (autoref (keep_goal, trace))
done

schematic_goal graph_restrict_right_impl_aux:
fixes Rsl Rsr
notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set]
assumes [autoref_rules]: "(memr, (∈)) ∈ R → ⟨R⟩Rsr → bool_rel"
shows "(?c, op_graph_restrict_right) ∈ ⟨R⟩Rsr → ⟨R⟩slg_rel → ⟨R⟩slg_rel"
unfolding graph_restrict_right_aimpl[abs_def]
apply (autoref (keep_goal, trace))
done

concrete_definition graph_restrict_impl uses graph_restrict_impl_aux
concrete_definition graph_restrict_left_impl uses graph_restrict_left_impl_aux
concrete_definition graph_restrict_right_impl uses graph_restrict_right_impl_aux

context begin interpretation autoref_syn .
lemma [autoref_itype]:
"op_graph_restrict ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_slg →⇩i ⟨I⟩⇩ii_slg"
"op_graph_restrict_right ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_slg →⇩i ⟨I⟩⇩ii_slg"
"op_graph_restrict_left ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_slg →⇩i ⟨I⟩⇩ii_slg"
by auto
end

lemmas [autoref_rules_raw] =
graph_restrict_impl.refine[OF GEN_OP_D GEN_OP_D]
graph_restrict_left_impl.refine[OF GEN_OP_D]
graph_restrict_right_impl.refine[OF GEN_OP_D]

schematic_goal "(?c::?'c, λ(E::nat digraph) x. E``{x}) ∈ ?R"
apply (autoref (keep_goal))
done

lemma graph_minus_aimpl:
fixes E1 E2 :: "'a rel"
shows "E1-E2 = E_of_succ (λx. E1``{x} - E2``{x})"
by (auto simp: E_of_succ_def)

schematic_goal graph_minus_impl_aux:
fixes R :: "('vi×'v) set"
assumes [autoref_rules]: "(eq,(=))∈R→R→bool_rel"
shows "(?c, (-)) ∈ ⟨R⟩slg_rel → ⟨R⟩slg_rel → ⟨R⟩slg_rel"
apply (subst graph_minus_aimpl[abs_def])
apply (autoref (keep_goal,trace))
done

lemmas [autoref_rules] = graph_minus_impl_aux[OF GEN_OP_D]

lemma graph_minus_set_aimpl:
fixes E1 E2 :: "'a rel"
shows "E1-E2 = E_of_succ (λu. {v∈E1``{u}. (u,v)∉E2})"
by (auto simp: E_of_succ_def)

schematic_goal graph_minus_set_impl_aux:
fixes R :: "('vi×'v) set"
assumes [autoref_rules]: "(eq,(=))∈R→R→bool_rel"
assumes [autoref_rules]: "(mem,(∈)) ∈ R ×⇩r R → ⟨R ×⇩r R⟩Rs → bool_rel"
shows "(?c, (-)) ∈ ⟨R⟩slg_rel → ⟨R×⇩rR⟩Rs → ⟨R⟩slg_rel"
apply (subst graph_minus_set_aimpl[abs_def])
apply (autoref (keep_goal,trace))
done

lemmas [autoref_rules (overloaded)] = graph_minus_set_impl_aux[OF GEN_OP_D GEN_OP_D]

subsection ‹Rooted Graphs›

subsubsection ‹Operation Identification Setup›

consts
i_g_ext :: "interface ⇒ interface ⇒ interface"

abbreviation "i_frg ≡ ⟨i_unit⟩⇩ii_g_ext"

context begin interpretation autoref_syn .

lemma g_type[autoref_itype]:
"g_V ::⇩i ⟨Ie,I⟩⇩ii_g_ext →⇩i ⟨I⟩⇩ii_set"
"g_E ::⇩i ⟨Ie,I⟩⇩ii_g_ext →⇩i ⟨I⟩⇩ii_slg"
"g_V0 ::⇩i ⟨Ie,I⟩⇩ii_g_ext →⇩i ⟨I⟩⇩ii_set"
"graph_rec_ext
::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_slg →⇩i ⟨I⟩⇩ii_set →⇩i iE →⇩i ⟨Ie,I⟩⇩ii_g_ext"
by simp_all

end

subsubsection ‹Generic Implementation›
record ('vi,'ei,'v0i) gen_g_impl =
gi_V :: 'vi
gi_E :: 'ei
gi_V0 :: 'v0i

definition gen_g_impl_rel_ext_internal_def: "⋀ Rm Rv Re Rv0. gen_g_impl_rel_ext Rm Rv Re Rv0
≡ { (gen_g_impl_ext Vi Ei V0i mi, graph_rec_ext V E V0 m)
| Vi Ei V0i mi V E V0 m.
(Vi,V)∈Rv ∧ (Ei,E)∈Re ∧ (V0i,V0)∈Rv0 ∧ (mi,m)∈Rm
}"

lemma gen_g_impl_rel_ext_def: "⋀Rm Rv Re Rv0. ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext
≡ { (gen_g_impl_ext Vi Ei V0i mi, graph_rec_ext V E V0 m)
| Vi Ei V0i mi V E V0 m.
(Vi,V)∈Rv ∧ (Ei,E)∈Re ∧ (V0i,V0)∈Rv0 ∧ (mi,m)∈Rm
}"
unfolding gen_g_impl_rel_ext_internal_def relAPP_def by simp

lemma gen_g_impl_rel_sv[relator_props]:
"⋀Rm Rv Re Rv0. ⟦single_valued Rv; single_valued Re; single_valued Rv0; single_valued Rm ⟧ ⟹
single_valued (⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext)"
unfolding gen_g_impl_rel_ext_def
apply (auto
intro!: single_valuedI
dest: single_valuedD slg_rel_sv list_set_rel_sv)
done

lemma gen_g_refine:
"⋀Rm Rv Re Rv0. (gi_V,g_V) ∈ ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext → Rv"
"⋀Rm Rv Re Rv0. (gi_E,g_E) ∈ ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext → Re"
"⋀Rm Rv Re Rv0. (gi_V0,g_V0) ∈ ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext → Rv0"
"⋀Rm Rv Re Rv0. (gen_g_impl_ext, graph_rec_ext)
∈ Rv → Re → Rv0 → Rm → ⟨Rm,Rv,Re,Rv0⟩gen_g_impl_rel_ext"
unfolding gen_g_impl_rel_ext_def
by auto

subsubsection ‹Implementation with list-set for Nodes›
type_synonym ('v,'m) frgv_impl_scheme =
"('v list, 'v ⇒ 'v list, 'v list, 'm) gen_g_impl_scheme"

definition frgv_impl_rel_ext_internal_def:
"frgv_impl_rel_ext Rm Rv
≡ ⟨Rm,⟨Rv⟩list_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext"

lemma frgv_impl_rel_ext_def: "⟨Rm,Rv⟩frgv_impl_rel_ext
≡ ⟨Rm,⟨Rv⟩list_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext"
unfolding frgv_impl_rel_ext_internal_def relAPP_def by simp

lemma [autoref_rel_intf]: "REL_INTF frgv_impl_rel_ext i_g_ext"
by (rule REL_INTFI)

lemma [relator_props, simp]:
"⟦single_valued Rv; Range Rv = UNIV; single_valued Rm⟧
⟹ single_valued (⟨Rm,Rv⟩frgv_impl_rel_ext)"
unfolding frgv_impl_rel_ext_def by tagged_solver

lemmas [param, autoref_rules] = gen_g_refine[where
Rv = "⟨Rv⟩list_set_rel" and Re = "⟨Rv⟩slg_rel" and ?Rv0.0 = "⟨Rv⟩list_set_rel"
for Rv, folded frgv_impl_rel_ext_def]

subsubsection ‹Implementation with Cfun for Nodes›
text ‹This implementation allows for the universal node set.›
type_synonym ('v,'m) g_impl_scheme =
"('v ⇒ bool, 'v ⇒ 'v list, 'v list, 'm) gen_g_impl_scheme"

definition g_impl_rel_ext_internal_def:
"g_impl_rel_ext Rm Rv
≡ ⟨Rm,⟨Rv⟩fun_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext"

lemma g_impl_rel_ext_def: "⟨Rm,Rv⟩g_impl_rel_ext
≡ ⟨Rm,⟨Rv⟩fun_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel⟩gen_g_impl_rel_ext"
unfolding g_impl_rel_ext_internal_def relAPP_def by simp

lemma [autoref_rel_intf]: "REL_INTF g_impl_rel_ext i_g_ext"
by (rule REL_INTFI)

lemma [relator_props, simp]:
"⟦single_valued Rv; Range Rv = UNIV; single_valued Rm⟧
⟹ single_valued (⟨Rm,Rv⟩g_impl_rel_ext)"
unfolding g_impl_rel_ext_def by tagged_solver

lemmas [param, autoref_rules] = gen_g_refine[where
Rv = "⟨Rv⟩fun_set_rel"
and Re = "⟨Rv⟩slg_rel"
and ?Rv0.0 = "⟨Rv⟩list_set_rel"
for Rv, folded g_impl_rel_ext_def]

lemma [autoref_rules]: "(gi_V_update, g_V_update) ∈ (⟨Rv⟩fun_set_rel → ⟨Rv⟩fun_set_rel) →
⟨Rm, Rv⟩g_impl_rel_ext → ⟨Rm, Rv⟩g_impl_rel_ext"
unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def
by (auto, metis (full_types) tagged_fun_relD_both)
lemma [autoref_rules]: "(gi_E_update, g_E_update) ∈ (⟨Rv⟩slg_rel → ⟨Rv⟩slg_rel) →
⟨Rm, Rv⟩g_impl_rel_ext → ⟨Rm, Rv⟩g_impl_rel_ext"
unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def
by (auto, metis (full_types) tagged_fun_relD_both)
lemma [autoref_rules]: "(gi_V0_update, g_V0_update) ∈ (⟨Rv⟩list_set_rel → ⟨Rv⟩list_set_rel) →
⟨Rm, Rv⟩g_impl_rel_ext → ⟨Rm, Rv⟩g_impl_rel_ext"
unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def
by (auto, metis (full_types) tagged_fun_relD_both)

(* HACK: The homgeneity rule heuristics erronously creates a homogeneity rule that
equalizes Rv and Rv0, out of the frv-implementation, which happens to be the
first. This declaration counters the undesired effects caused by this. *)
lemma [autoref_hom]:
"CONSTRAINT graph_rec_ext (⟨Rv⟩Rvs → ⟨Rv⟩Res → ⟨Rv⟩Rv0s → Rm → ⟨Rm,Rv⟩Rg)"
by simp

schematic_goal "(?c::?'c, λG x. g_E G `` {x})∈?R"
apply (autoref (keep_goal))
done

schematic_goal "(?c,λV0 E.
⦇ g_V = UNIV, g_E = E, g_V0 = V0 ⦈  )
∈⟨R⟩list_set_rel → ⟨R⟩slg_rel → ⟨unit_rel,R⟩g_impl_rel_ext"
apply (autoref (keep_goal))
done

schematic_goal "(?c,λV V0 E.
⦇ g_V = V, g_E = E, g_V0 = V0 ⦈  )
∈⟨R⟩list_set_rel → ⟨R⟩list_set_rel → ⟨R⟩slg_rel → ⟨unit_rel,R⟩frgv_impl_rel_ext"
apply (autoref (keep_goal))
done

subsubsection ‹Renaming›

definition "the_inv_into_map V f x
= (if x ∈ f`V then Some (the_inv_into V f x) else None)"

lemma the_inv_into_map_None[simp]:
"the_inv_into_map V f x = None ⟷ x ∉ f`V"
unfolding the_inv_into_map_def by auto

lemma the_inv_into_map_Some':
"the_inv_into_map V f x = Some y ⟷ x ∈ f`V ∧ y=the_inv_into V f x"
unfolding the_inv_into_map_def by auto

lemma the_inv_into_map_Some[simp]:
"inj_on f V ⟹ the_inv_into_map V f x = Some y ⟷ y∈V ∧ x=f y"
by (auto simp: the_inv_into_map_Some' the_inv_into_f_f)

definition "the_inv_into_map_impl V f =
FOREACH V (λx m. RETURN (m(f x ↦ x))) Map.empty"

lemma the_inv_into_map_impl_correct:
assumes [simp]: "finite V"
assumes INJ: "inj_on f V"
shows "the_inv_into_map_impl V f ≤ SPEC (λr. r = the_inv_into_map V f)"
unfolding the_inv_into_map_impl_def
apply (refine_rcg
FOREACH_rule[where I="λit m. m=the_inv_into_map (V - it) f"]
refine_vcg
)

apply (vc_solve
simp: the_inv_into_map_def[abs_def] it_step_insert_iff
intro!: ext)

apply (intro allI impI conjI)

apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], auto) []

apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], auto) []

apply safe []
apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], (auto) [2])+
apply simp
done

schematic_goal the_inv_into_map_code_aux:
fixes Rv' :: "('vti × 'vt) set"
assumes [autoref_ga_rules]: "is_bounded_hashcode Rv' eq bhc"
assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('vti) (def_size)"
assumes [autoref_rules]: "(Vi,V)∈⟨Rv⟩list_set_rel"
assumes [autoref_rules]: "(fi,f)∈Rv→Rv'"
shows "(RETURN ?c, the_inv_into_map_impl V f) ∈ ⟨⟨Rv',Rv⟩ahm_rel bhc⟩nres_rel"
unfolding the_inv_into_map_impl_def[abs_def]
done

concrete_definition the_inv_into_map_code uses the_inv_into_map_code_aux
export_code the_inv_into_map_code checking SML

thm the_inv_into_map_code.refine

context begin interpretation autoref_syn .
lemma autoref_the_inv_into_map[autoref_rules]:
fixes Rv' :: "('vti × 'vt) set"
assumes "SIDE_GEN_ALGO (is_bounded_hashcode Rv' eq bhc)"
assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('vti) def_size)"
assumes INJ: "SIDE_PRECOND (inj_on f V)"
assumes V: "(Vi,V)∈⟨Rv⟩list_set_rel"
assumes F: "(fi,f)∈Rv→Rv'"
shows "(the_inv_into_map_code eq bhc def_size Vi fi,
(OP the_inv_into_map
::: ⟨Rv⟩list_set_rel → (Rv→Rv') → ⟨Rv', Rv⟩Impl_Array_Hash_Map.ahm_rel bhc)
\$V\$f) ∈ ⟨Rv', Rv⟩Impl_Array_Hash_Map.ahm_rel bhc"
proof simp

from V have FIN: "finite V" using list_set_rel_range by auto

note the_inv_into_map_code.refine[
OF assms(1-2,4-5)[unfolded autoref_tag_defs], THEN nres_relD
]
also note the_inv_into_map_impl_correct[OF FIN INJ[unfolded autoref_tag_defs]]
finally show "(the_inv_into_map_code eq bhc def_size Vi fi, the_inv_into_map V f)
∈ ⟨Rv', Rv⟩Impl_Array_Hash_Map.ahm_rel bhc"
qed

end

schematic_goal "(?c::?'c, do {
let s = {1,2,3::nat};
⌦‹ASSERT (inj_on Suc s);›
RETURN (the_inv_into_map s Suc) }) ∈ ?R"
apply (autoref (keep_goal))
done

definition "fr_rename_ext_aimpl ecnv f G ≡ do {
ASSERT (inj_on f (g_V G));
ASSERT (inj_on f (g_V0 G));
let fi_map = the_inv_into_map (g_V G) f;
e ← ecnv fi_map G;
RETURN ⦇
g_V = f`(g_V G),
g_E = (E_of_succ (λv. case fi_map v of
Some u ⇒ f ` (succ_of_E (g_E G) u) | None ⇒ {})),
g_V0 = (f`g_V0 G),
… = e
⦈
}"

context g_rename_precond begin

definition "fi_map x = (if x ∈ f`V then Some (fi x) else None)"
lemma fi_map_alt: "fi_map = the_inv_into_map V f"
apply (rule ext)
unfolding fi_map_def the_inv_into_map_def fi_def
by simp

lemma fi_map_Some: "(fi_map u = Some v) ⟷ u∈f`V ∧ fi u = v"
unfolding fi_map_def by (auto split: if_split_asm)

lemma fi_map_None: "(fi_map u = None) ⟷ u∉f`V"
unfolding fi_map_def by (auto split: if_split_asm)

lemma rename_E_aimpl_alt: "rename_E f E = E_of_succ (λv. case fi_map v of
Some u ⇒ f ` (succ_of_E E u) | None ⇒ {})"
unfolding E_of_succ_def succ_of_E_def
using E_ss
by (force
simp: fi_f f_fi fi_map_Some fi_map_None
split: if_split_asm option.splits)

lemma frv_rename_ext_aimpl_alt:
assumes ECNV: "ecnv' fi_map G ≤ SPEC (λr. r = ecnv G)"
shows "fr_rename_ext_aimpl ecnv' f G
≤ SPEC (λr. r = fr_rename_ext ecnv f G)"
proof -
(*have [simp]: "⦇ g_E =
E_of_succ
(λv. case the_inv_into_map V f v of None ⇒ {}
| Some u ⇒ f ` succ_of_E (g_E G) u),
g_V0 = f ` g_V0 G, … = ecnv Gv⦈
= frv_G (frv_rename_ext ecnv f Gv)"
unfolding frv_rename_ext_def
by (auto simp: rename_E_aimpl_alt fi_map_alt)

have [simp]: "⦇frv_V = f ` V, frv_G = frv_G Gv'⦈ = Gv'"
unfolding frv_rename_ext_def
by simp*)

show ?thesis
unfolding fr_rename_ext_def fr_rename_ext_aimpl_def
apply (refine_rcg
order_trans[OF ECNV[unfolded fi_map_alt]]
refine_vcg)
using subset_inj_on[OF _ V0_ss]
apply (auto intro: INJ simp: rename_E_aimpl_alt fi_map_alt)
done
qed
end

term frv_rename_ext_aimpl
schematic_goal fr_rename_ext_impl_aux:
fixes Re and Rv' :: "('vti × 'vt) set"
assumes [autoref_rules]: "(eq, (=)) ∈ Rv' → Rv' → bool_rel"
assumes [autoref_ga_rules]: "is_bounded_hashcode Rv' eq bhc"
assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('vti) def_size"
shows "(?c,fr_rename_ext_aimpl) ∈
((⟨Rv',Rv⟩ahm_rel bhc) → ⟨Re,Rv⟩frgv_impl_rel_ext → ⟨Re'⟩nres_rel) →
(Rv→Rv') →
⟨Re,Rv⟩frgv_impl_rel_ext →
⟨⟨Re',Rv'⟩frgv_impl_rel_ext⟩nres_rel"
unfolding fr_rename_ext_aimpl_def[abs_def]
apply (autoref (keep_goal))
done

concrete_definition fr_rename_ext_impl uses fr_rename_ext_impl_aux

thm fr_rename_ext_impl.refine[OF GEN_OP_D SIDE_GEN_ALGO_D SIDE_GEN_ALGO_D]

subsection ‹Graphs from Lists›

definition succ_of_list :: "(nat×nat) list ⇒ nat ⇒ nat set"
where
"succ_of_list l ≡ let
m = fold (λ(u,v) g.
case g u of
None ⇒ g(u↦{v})
| Some s ⇒ g(u↦insert v s)
) l Map.empty
in
(λu. case m u of None ⇒ {} | Some s ⇒ s)"

lemma succ_of_list_correct_aux:
"(succ_of_list l, set l) ∈ br (λsuccs. {(u,v). v∈succs u}) (λ_. True)"
proof -

term the_default

{ fix m
have "fold (λ(u,v) g.
case g u of
None ⇒ g(u↦{v})
| Some s ⇒ g(u↦insert v s)
) l m
= (λu. let s=set l `` {u} in
if s={} then m u else Some (the_default {} (m u) ∪ s))"
apply (induction l arbitrary: m)
apply (auto
split: option.split if_split
simp: Let_def Image_def
intro!: ext)
done
} note aux=this

show ?thesis
unfolding succ_of_list_def aux
by (auto simp: br_def Let_def split: option.splits if_split_asm)
qed

schematic_goal succ_of_list_impl:
notes [autoref_tyrel] =
ty_REL[where 'a="nat⇀nat set" and R="⟨nat_rel,R⟩iam_map_rel" for R]
ty_REL[where 'a="nat set" and R="⟨nat_rel⟩list_set_rel"]

shows "(?f::?'c,succ_of_list) ∈ ?R"
unfolding succ_of_list_def[abs_def]
apply (autoref (keep_goal))
done

concrete_definition succ_of_list_impl uses succ_of_list_impl
export_code succ_of_list_impl in SML

lemma succ_of_list_impl_correct: "(succ_of_list_impl,set) ∈ Id → ⟨Id⟩slg_rel"
apply rule
unfolding slg_rel_def
apply rule
apply (rule succ_of_list_impl.refine[THEN fun_relD])
apply simp
apply (rule succ_of_list_correct_aux)
done

end

```