Theory Succ_Graph

section ‹Graphs defined by Successor Functions›
theory Succ_Graph
imports 
  Collections.Refine_Dflt
begin

text ‹
  This code is used in various examples
›

type_synonym 'a slg = "'a  'a list"
definition slg_rel_def_internal: "slg_rel R  
  {(succs,G). v. (succs v, G``{v})  Rlist_set_rel}"

lemma slg_rel_def: "Rslg_rel  
  {(succs,G). v. (succs v, G``{v})  Rlist_set_rel}" 
  by (auto simp: slg_rel_def_internal relAPP_def)

lemma [relator_props]: "single_valued R  single_valued (Rslg_rel)"
  unfolding slg_rel_def
  apply (rule single_valuedI)
  apply (auto dest: single_valuedD[OF list_set_rel_sv])
  done

consts i_slg :: "interface  interface"

lemmas [autoref_rel_intf] =
  REL_INTFI[of slg_rel i_slg]

definition [simp]: "slg_succs E v  E``{v}"

lemma [autoref_itype]: "slg_succs ::i Iii_slg i I i Iii_set" by simp

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

definition [code_unfold, simp]: "slg_succs_impl succs v  succs v"

lemma refine_slg_succs[autoref_rules_raw]: 
  "(slg_succs_impl,slg_succs)Idslg_relIdIdlist_set_rel"
  apply (intro fun_relI)
  apply (simp add: slg_succs_def slg_rel_def)
  done


subsection "Graph Representations"
(* TODO: Correctness proofs *)

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)
    
"
    
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 checking SML

definition acc_of_list :: "nat list  nat set" 
  where "acc_of_list l  fold insert l {}"

schematic_goal acc_of_list_impl:
  notes [autoref_tyrel] = 
    ty_REL[where 'a="nat set" and R="nat_reliam_set_rel" for R]

  shows "(?f::?'c,acc_of_list)  ?R"
  unfolding acc_of_list_def[abs_def]
  apply (autoref (keep_goal))
  done

concrete_definition acc_of_list_impl uses acc_of_list_impl
export_code acc_of_list_impl checking SML

end