Theory CAVA_Automata.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  Rlist_set_rel) O br (λsuccs. {(u,v). vsuccs u}) (λ_. True)"

lemma slg_rel_def: "Rslg_rel = 
  (R  Rlist_set_rel) O br (λsuccs. {(u,v). vsuccs 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 (Rslg_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 Iii_slg i I i Iii_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)Rslg_relRRlist_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). vsucc 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 Iii_set) i Iii_slg" by simp
  lemma [autoref_itype]: "succ_of_E ::i Iii_slg i I i Iii_set" by simp
end

lemma E_of_succ_refine[autoref_rules]:
  "(λx. x, E_of_succ)  (R  Rlist_set_rel)  Rslg_rel"
  "(λx. x, succ_of_E)  Rslg_rel  (R  Rlist_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 vVl then {x  E``{v}. xVr} 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 vVl 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}. xVr})"
  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  RRsl  bool_rel"
  assumes [autoref_rules]: "(memr, (∈))  R  RRsr  bool_rel"
  shows "(?c, op_graph_restrict)  RRsl  RRsr  Rslg_rel  Rslg_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  RRsl  bool_rel"
  shows "(?c, op_graph_restrict_left)  RRsl  Rslg_rel  Rslg_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  RRsr  bool_rel"
  shows "(?c, op_graph_restrict_right)  RRsr  Rslg_rel  Rslg_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 Iii_set i Iii_set i Iii_slg i Iii_slg"
    "op_graph_restrict_right ::i Iii_set i Iii_slg i Iii_slg"
    "op_graph_restrict_left ::i Iii_set i Iii_slg i Iii_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,(=))RRbool_rel"
  shows "(?c, (-))  Rslg_rel  Rslg_rel  Rslg_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. {vE1``{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,(=))RRbool_rel"
  assumes [autoref_rules]: "(mem,(∈))  R ×r R  R ×r RRs  bool_rel"
  shows "(?c, (-))  Rslg_rel  R×rRRs  Rslg_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_unitii_g_ext"

context begin interpretation autoref_syn .

lemma g_type[autoref_itype]:
  "g_V ::i Ie,Iii_g_ext i Iii_set"
  "g_E ::i Ie,Iii_g_ext i Iii_slg"
  "g_V0 ::i Ie,Iii_g_ext i Iii_set"
  "graph_rec_ext
    ::i Iii_set i Iii_slg i Iii_set i iE i Ie,Iii_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,Rv0gen_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,Rv0gen_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,Rv0gen_g_impl_rel_ext  Rv"
  "Rm Rv Re Rv0. (gi_E,g_E)  Rm,Rv,Re,Rv0gen_g_impl_rel_ext  Re"
  "Rm Rv Re Rv0. (gi_V0,g_V0)  Rm,Rv,Re,Rv0gen_g_impl_rel_ext  Rv0"
  "Rm Rv Re Rv0. (gen_g_impl_ext, graph_rec_ext) 
     Rv  Re  Rv0  Rm  Rm,Rv,Re,Rv0gen_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,Rvlist_set_rel,Rvslg_rel,Rvlist_set_relgen_g_impl_rel_ext"

lemma frgv_impl_rel_ext_def: "Rm,Rvfrgv_impl_rel_ext
   Rm,Rvlist_set_rel,Rvslg_rel,Rvlist_set_relgen_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,Rvfrgv_impl_rel_ext)"
  unfolding frgv_impl_rel_ext_def by tagged_solver

lemmas [param, autoref_rules] = gen_g_refine[where 
  Rv = "Rvlist_set_rel" and Re = "Rvslg_rel" and ?Rv0.0 = "Rvlist_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,Rvfun_set_rel,Rvslg_rel,Rvlist_set_relgen_g_impl_rel_ext"

lemma g_impl_rel_ext_def: "Rm,Rvg_impl_rel_ext
   Rm,Rvfun_set_rel,Rvslg_rel,Rvlist_set_relgen_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,Rvg_impl_rel_ext)"
  unfolding g_impl_rel_ext_def by tagged_solver

lemmas [param, autoref_rules] = gen_g_refine[where 
  Rv = "Rvfun_set_rel" 
  and Re = "Rvslg_rel" 
  and ?Rv0.0 = "Rvlist_set_rel" 
  for Rv, folded g_impl_rel_ext_def]

lemma [autoref_rules]: "(gi_V_update, g_V_update)  (Rvfun_set_rel  Rvfun_set_rel) 
  Rm, Rvg_impl_rel_ext  Rm, Rvg_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)  (Rvslg_rel  Rvslg_rel) 
  Rm, Rvg_impl_rel_ext  Rm, Rvg_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)  (Rvlist_set_rel  Rvlist_set_rel) 
  Rm, Rvg_impl_rel_ext  Rm, Rvg_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 (RvRvs  RvRes  RvRv0s  Rm  Rm,RvRg)"
  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   )
  Rlist_set_rel  Rslg_rel  unit_rel,Rg_impl_rel_ext"
  apply (autoref (keep_goal))
  done

schematic_goal "(?c,λV V0 E.
    g_V = V, g_E = E, g_V0 = V0   )
  Rlist_set_rel  Rlist_set_rel  Rslg_rel  unit_rel,Rfrgv_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  yV  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)Rvlist_set_rel"
  assumes [autoref_rules]: "(fi,f)RvRv'"
  shows "(RETURN ?c, the_inv_into_map_impl V f)  Rv',Rvahm_rel bhcnres_rel"
  unfolding the_inv_into_map_impl_def[abs_def]
  apply (autoref_monadic (plain))
  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)Rvlist_set_rel"
  assumes F: "(fi,f)RvRv'"
  shows "(the_inv_into_map_code eq bhc def_size Vi fi, 
    (OP the_inv_into_map 
      ::: Rvlist_set_rel  (RvRv')  Rv', RvImpl_Array_Hash_Map.ahm_rel bhc)
    $V$f)  Rv', RvImpl_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', RvImpl_Array_Hash_Map.ahm_rel bhc"
    by (simp add: refine_pw_simps pw_le_iff)
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)  uf`V  fi u = v"
    unfolding fi_map_def by (auto split: if_split_asm)

  lemma fi_map_None: "(fi_map u = None)  uf`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',Rvahm_rel bhc)  Re,Rvfrgv_impl_rel_ext  Re'nres_rel)    
    (RvRv') 
    Re,Rvfrgv_impl_rel_ext  
    Re',Rv'frgv_impl_rel_extnres_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(uinsert 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). vsuccs u}) (λ_. True)"
proof -

  term the_default

  { fix m
    have "fold (λ(u,v) g. 
            case g u of 
              None  g(u{v})
            | Some s  g(uinsert 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="natnat set" and R="nat_rel,Riam_map_rel" for R]
    ty_REL[where 'a="nat set" and R="nat_rellist_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  Idslg_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