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}) ∈ ⟨R⟩list_set_rel}"

lemma slg_rel_def: "⟨R⟩slg_rel ≡ 
  {(succs,G). ∀v. (succs v, G``{v}) ∈ ⟨R⟩list_set_rel}" 
  by (auto simp: slg_rel_def_internal relAPP_def)

lemma [relator_props]: "single_valued R ⟹ single_valued (⟨R⟩slg_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 ⟨I⟩⇩ii_slg →⇩i I →⇩i ⟨I⟩⇩ii_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)∈⟨Id⟩slg_rel→Id→⟨Id⟩list_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(u↦insert 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="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 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_rel⟩iam_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