Theory Pair_Graph_Specs

theory Pair_Graph_Specs
  imports Vwalk "Map_Addons" "Set_Addons"
 begin

section ‹A Digraph Representation for Efficient Executable Functions›

text ‹We develop a locale modelling an abstract data type (ADT) which abstractly models a graph as an
      adjacency map: i.e.\ every vertex is mapped to a ‹set› of adjacent vertices, and this latter
      set is again modelled using the ADT of sets provided in Isabelle/HOL's distribution.

      We then show that this ADT can be implemented using existing implementations of the ‹set› ADT.
›

(*
record ('a, 's) Set_Rec = empty :: "'s" insert :: "'a ⇒ 's ⇒ 's" delete :: "'a ⇒ 's ⇒ 's"
                          isin :: "'s ⇒ 'a ⇒ bool" set :: "'s ⇒ 'a set" invar :: "'s ⇒ bool"

locale Set_Rec =
  fixes set_rec:: "('a,'s) Set_Rec"
  assumes "Set (empty set_rec) (insert set_rec) (delete set_rec) (isin set_rec)
               (set set_rec) (invar set_rec)"
    
record ('a,'s) Set_Choose_Rec = "('a,'s) Set_Rec" + sel :: "'s ⇒ 'a"



locale Set_Choose = Set_Rec set_rec
  for set_rec::"('a,'m) Set_Rec" + 

fixes sel ::"'m ⇒ 'a"
assumes choose: "s ≠ (empty set_rec) ⟹ (isin set_rec) s (sel s)"
begin


locale Set_Map = Set
  where set = t_set for t_set +
fixes t_map ::"('a ⇒ 'a) ⇒ 'm ⇒ 'm"
assumes map: "bij_betw f (t_set s) t  ⟹ t_set (t_map f s) = t"
*)

locale Set_Choose = set: Set 
  where set = t_set for t_set ("[_]⇩s") +
fixes sel ::"'s ⇒ 'a"

assumes choose [simp]: "s ≠ empty ⟹ isin s (sel s)"


begin
context
  includes set.automation
begin

(*
declare set_empty[simp] set_isin[simp] set_insert[simp] set_delete[simp]
        invar_empty[simp] invar_insert[simp] invar_delete[simp] choose[simp]
*)

subsection ‹Abstraction lemmas›

text ‹These are lemmas for automation. Their purpose is to remove any mention of the locale set ADT
      constructs and replace it with Isabelle's native sets.›

lemma choose'[simp, intro,dest]:
  "s ≠ empty ⟹ invar s ⟹ sel s ∈ t_set s"
  by(auto simp flip: set.set_isin)

lemma choose''[intro]:
  "invar s ⟹ s ≠ empty ⟹ t_set s ⊆ s' ⟹ sel s ∈ s'"
  by(auto simp flip: set.set_isin)

lemma emptyD[dest]:
           "s = empty ⟹ t_set s = {}"
           "s ≠ empty ⟹ invar s ⟹ t_set s ≠ {}"
           "empty = s ⟹ t_set s = {}"
           "empty ≠ s ⟹ invar s ⟹ t_set s ≠ {}"
 using set.set_empty
 by auto
end
end
(*
locale Adjmap_Map_Specs = 
 adjmap: Map 
 where update = update and invar = adjmap_inv +


 vset: Set_Choose
 where empty = vset_empty and delete = vset_delete and insert = vset_insert and invar = vset_inv
      and isin = isin

 for update :: "'a ⇒ 'vset ⇒ 'adjmap ⇒ 'adjmap" and adjmap_inv :: "'adjmap ⇒ bool"  and

     vset_empty :: "'vset"  ("∅⇩N") and vset_delete :: "'a ⇒ 'vset ⇒ 'vset" and
     vset_insert and vset_inv and isin


  ― ‹Why do we need ann efficient neghbourhood test?›


begin


end
*)


named_theorems Graph_Spec_Elims
named_theorems Graph_Spec_Intros
named_theorems Graph_Spec_Simps

locale Pair_Graph_Specs = 
 adjmap: Map 
 where update = update and invar = adjmap_inv +


 vset: Set_Choose
 where empty = vset_empty and delete = vset_delete and invar = vset_inv

 for update :: "'v ⇒ 'vset ⇒ 'adjmap ⇒ 'adjmap" and adjmap_inv :: "'adjmap ⇒ bool"  and

     vset_empty :: "'vset" and vset_delete :: "'v ⇒ 'vset ⇒ 'vset" and
     vset_inv
(*  Adjmap_Map_Specs where update = update
for update :: "'a ⇒ 'vset ⇒ 'adjmap ⇒ 'adjmap"*) 
begin

notation vset_empty ("∅⇩V")
notation empty ("∅⇩G")

abbreviation isin' (infixl "∈⇩G" 50) where "isin' G v ≡ isin v G" 
abbreviation not_isin' (infixl "∉⇩G" 50) where "not_isin' G v ≡ ¬ isin' G v"

definition "set_of_map (m::'adjmap) = {(u,v). case (lookup m u) of Some vs ⇒ v ∈⇩G vs}"

definition "graph_inv G = (adjmap_inv G ∧ (∀v vset. lookup G v = Some vset ⟶ vset_inv vset))"
definition "finite_graph G = (finite {v. (lookup G v) ≠ None})"
definition "finite_vsets = (∀vset. finite (t_set vset))"


definition neighb::"'adjmap ⇒ 'v ⇒ 'vset" where
  "(neighb G v) = (case (lookup G v) of Some vset ⇒ vset | _ ⇒ vset_empty)"

lemmas [code] = neighb_def

notation "neighb" ("𝒩⇩G _ _" 100)

definition digraph_abs ("[_]⇩G") where "digraph_abs G = {(u,v). v ∈⇩G (𝒩⇩G G u)}" 

definition "add_edge G u v =
( 
  case (lookup G u) of Some vset ⇒ 
  let
    vset = the (lookup G u);
    vset' = insert v vset;
    digraph' = update u vset' G
  in
    digraph'
  | _ ⇒
  let
    vset' = insert v vset_empty;
    digraph' = update u vset' G
  in
    digraph'
)"

definition "delete_edge G u v =
( 
  case (lookup G u) of Some vset ⇒ 
  let
    vset = the (lookup G u);
    vset' = vset_delete v vset;
    digraph' = update u vset' G
  in
    digraph'
  | _ ⇒ G 
)"
(*
function (domintros) recursive_union where
"recursive_union us vs = (if us = vset_empty then vs
                          else let x= sel us in recursive_union (vset_delete x us) (insert x vs))"
  by pat_completeness auto

partial_function (tailrec) recursive_union_impl where
"recursive_union_impl us vs = (if us = vset_empty then vs
                          else let x= sel us in recursive_union_impl (vset_delete x us) (insert x vs))"

lemmas [code] = recursive_union_impl.simps

lemma recursive_union_same:
  assumes "recursive_union_dom (us, vs)"
  shows "recursive_union_impl us vs = recursive_union us vs"
  by(induction rule: recursive_union.pinduct[OF assms])
    (auto simp add: recursive_union.psimps recursive_union_impl.simps)

lemma recursive_union_finite_dom:
  assumes "card (t_set us) = n " "finite (t_set us)" "vset_inv us"
  shows "recursive_union_dom (us, vs)"
  using assms
proof(induction n arbitrary: us vs )
  case 0
  then show ?case by(auto intro: recursive_union.domintros)
next
  case (Suc n)
  show ?case 
  apply(rule recursive_union.domintros)
  using Suc(2-) 
  by (auto intro:  recursive_union.domintros Suc(1) 
        simp add: vset.set.set_delete Suc.prems(3) vset.set.invar_delete)
qed

lemma recursive_union_inv:
  assumes "recursive_union_dom (us, vs)"  "vset_inv us"  "vset_inv vs"
  shows "vset_inv ()"


definition "union_impl us vs = (if vs = vset_empty then us else recursive_union_impl us vs)"
*)

context ―‹Locale properties›
  includes vset.set.automation and adjmap.automation
  fixes G::'adjmap
begin

lemma graph_invE[elim]: 
  "graph_inv G ⟹ (⟦adjmap_inv G; (⋀v vset. lookup G v = Some vset ⟹ vset_inv vset)⟧ ⟹ P) ⟹ P"
  by (auto simp: graph_inv_def)

lemma graph_invI[intro]: 
  "⟦adjmap_inv G; (⋀v vset. lookup G v = Some vset ⟹ vset_inv vset)⟧ ⟹ graph_inv G"
  by (auto simp: graph_inv_def)

lemma finite_graphE[elim]: 
  "finite_graph G ⟹ (finite {v. (lookup G v) ≠ None} ⟹ P) ⟹ P"
  by (auto simp: finite_graph_def)

lemma finite_graphI[intro]: 
  "finite {v. (lookup G v) ≠ None}  ⟹ finite_graph G"
  by (auto simp: finite_graph_def)

lemma finite_vsetsE[elim]: 
  "finite_vsets ⟹ ((⋀N. finite (t_set N)) ⟹ P) ⟹ P"
  by (auto simp: finite_vsets_def)

lemma finite_vsetsI[intro]: 
  "(⋀N. finite (t_set N)) ⟹ finite_vsets"
  by (auto simp: finite_vsets_def)


lemma neighbourhood_invars'[simp,dest]:
   "graph_inv G ⟹ vset_inv (𝒩⇩G G v)"
  by (auto simp add: graph_inv_def neighb_def split: option.splits)


lemma finite_graph[intro!]:
  assumes "graph_inv G" "finite_graph G" "finite_vsets"
  shows "finite (digraph_abs G)"
proof-

  have "digraph_abs G ⊆ {v. lookup G v ≠ None} × (⋃ (t_set ` {N | N v. lookup G v = Some N}))"
    using assms 
    by (fastforce simp: digraph_abs_def neighb_def graph_inv_def split: option.splits)

  moreover have "finite {v. lookup G v ≠ None}"
    using assms
    by fastforce

  moreover have "finite (⋃ (t_set ` {N | N v. lookup G v = Some N}))"
    using assms
    by (force elim!: finite_vsetsE finite_graphE
              intro!: finite_imageI 
                      rev_finite_subset
                        [where B = "(the o lookup G) ` {v. ∃y. lookup G v = Some y}"])
  ultimately show ?thesis
    by(fastforce intro!: finite_cartesian_product dest: finite_subset)+

qed

corollary finite_vertices[intro!]:
  assumes "graph_inv G" "finite_graph G" "finite_vsets"
  shows "finite (dVs (digraph_abs G))"
  using finite_graph[OF assms]
  by (simp add: finite_vertices_iff)

subsection ‹Abstraction lemmas›

text ‹These are lemmas for automation. Their purpose is to remove any mention of the neighbourhood
      concept implemented using the locale constructs and replace it with abstract terms
      on pair graphs.›

lemma are_connected_abs[simp]: 
  "graph_inv G ⟹ v ∈ t_set (𝒩⇩G G u) ⟷ (u,v) ∈ digraph_abs G"
  by(auto simp: digraph_abs_def neighbourhood_def option.discI graph_inv_def
          split: option.split)

lemma are_connected_absD[dest]: 
  "⟦v ∈ t_set (𝒩⇩G G u); graph_inv G⟧ ⟹ (u,v) ∈ digraph_abs G"
  by (auto simp: are_connected_abs)

lemma are_connected_absI[intro]: 
  "⟦(u,v) ∈ digraph_abs G; graph_inv G⟧ ⟹ v ∈ t_set (𝒩⇩G G u)"
  by (auto simp: are_connected_abs)

lemma neighbourhood_absD[dest!]:
  "⟦t_set (𝒩⇩G G x) ≠ {}; graph_inv G⟧ ⟹ x ∈ dVs (digraph_abs G)"
  by blast

lemma neighbourhood_abs[simp]:
  "graph_inv G ⟹ t_set (𝒩⇩G G u) = neighbourhood (digraph_abs G) u"
  by(auto simp: digraph_abs_def neighb_def Pair_Graph.neighbourhood_def option.discI graph_inv_def
          split: option.split)

lemma adjmap_inv_insert[intro]: "graph_inv G ⟹ graph_inv (add_edge G u v)"
  by (auto simp: add_edge_def graph_inv_def split: option.splits)

lemma digraph_abs_insert[simp]: "graph_inv G ⟹ digraph_abs (add_edge G u v) = Set.insert (u,v) (digraph_abs G)"
  by (fastforce simp add: digraph_abs_def set_of_map_def neighb_def add_edge_def split: option.splits if_splits)

lemma adjmap_inv_delete[intro]: "graph_inv G ⟹ graph_inv (delete_edge G u v)"
  by (auto simp: delete_edge_def graph_inv_def split: option.splits)

lemma digraph_abs_delete[simp]:  "graph_inv G ⟹ digraph_abs (delete_edge G u v) = (digraph_abs G) - {(u,v)}"
  by (fastforce simp add: digraph_abs_def set_of_map_def neighb_def delete_edge_def split: option.splits if_splits)


end ― ‹Properties context›  

end text ‹@{const Pair_Graph_Specs}›

end