Theory FiniteListGraph_Impl

theory FiniteListGraph_Impl
imports 
  FiniteListGraph
  (*"../../Collections/ICF/impl/RBTSetImpl" (*red black trees*)*)
    "HOL-Library.RBT_Impl"
    "HOL-Library.RBT"
  "HOL-Library.Product_Lexorder"
  (*maybe import the following only at the end*)
  Efficient_Distinct
  "HOL-Library.Code_Target_Nat"
begin



text ‹A graph's well-formed-ness can be tested with an executable function.›  
  fun wf_list_graph_impl::"'v list ⇒ ('v × 'v) list ⇒ bool" where
    "wf_list_graph_impl V [] = True" |
    "wf_list_graph_impl V ((v1,v2)#Es) = (v1 ∈ set V ∧ v2 ∈ set V ∧ wf_list_graph_impl V Es)"


  lemma wf_list_graph_impl_axioms_locale_props: 
    "wf_list_graph_impl V E ⟷ fst` set E ⊆ set V ∧ snd` set E ⊆ set V"
  by (induction E) auto


definition rbt_fromlist :: "'a list ⇒ ('a::linorder, unit) RBT.rbt" where 
  "rbt_fromlist ls ≡ RBT.bulkload (map (λl. (l, ())) ls)"
definition "rbt_contains a rbt ≡ RBT.lookup rbt a ≠ None"

lemma rbt_contains: "rbt_contains a (rbt_fromlist V) ⟷ a ∈ set V"
  apply(simp add: rbt_contains_def rbt_fromlist_def)
  apply(induction V)
   by(simp)+

  (*making the ∈ more efficient*)
  fun wf_list_graph_impl_rs::"('v::linorder,unit) RBT.rbt ⇒ ('v × 'v) list ⇒ bool" where
    "wf_list_graph_impl_rs V [] = True" |
    "wf_list_graph_impl_rs V ((v1,v2)#Es) = (rbt_contains v1 V ∧ rbt_contains v2 V ∧ wf_list_graph_impl_rs V Es)"

    
 lemma[code]: "wf_list_graph_impl V E = wf_list_graph_impl_rs (rbt_fromlist V) E"
   apply(induction E)
    apply(simp; fail)
   apply(rename_tac e Es)
   apply(case_tac e)
   by(simp add: rbt_contains)

  lemma[code]: "FiniteListGraph.wf_list_graph_axioms G = wf_list_graph_impl (nodesL G) (edgesL G)"
    by(simp add: FiniteListGraph.wf_list_graph_axioms_def wf_list_graph_impl_axioms_locale_props)

  text‹The list implementation matches the @{term "wf_graph"} definition›
  theorem wf_list_graph_iff_wf_graph: 
    "wf_graph (list_graph_to_graph G) ⟷ wf_list_graph_axioms G"
  apply(unfold list_graph_to_graph_def wf_graph_def wf_list_graph_axioms_def wf_list_graph_impl_axioms_locale_props)
    by simp
  corollary wf_list_graph_iff_wf_graph_simplified: 
  "wf_graph ⦇nodes = set (nodesL G), edges = set (edgesL G)⦈ ⟷ wf_list_graph_axioms G"
  apply(simp add: wf_list_graph_iff_wf_graph[unfolded list_graph_to_graph_def, simplified])
  done


 
text ‹Code examples.›
  definition wf_graph_example where
  "wf_graph_example ≡ ⦇ nodesL = [1::nat,4,6], edgesL = [(1,4), (1,6), (6,4)] ⦈"

  value "wf_list_graph wf_graph_example"

  definition wf_graph_impl_example where
  "wf_graph_impl_example ≡ wf_list_graph wf_graph_example"


  export_code wf_list_graph empty add_node delete_node add_edge delete_edge checking Scala


end