Theory Succ_Graph

header {* Graphs defined by Successor Functions *}
theory Succ_Graph
imports 
  "../../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

lemma refine_slg_succs[autoref_rules_raw]: 
  "(λsuccs v. succs v,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\<mapsto>{v})
          | Some s => g(u\<mapsto>insert v s)
        ) l Map.empty
  in
    (λu. case m u of None => {} | Some s => s)
    
"
    
schematic_lemma succ_of_list_impl:
  notes [autoref_tyrel] = 
    ty_REL[where 'a="nat\<rightharpoonup>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

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

schematic_lemma 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 in SML

end