Theory SubRel

theory SubRel
imports Graph
begin 

section ‹Graphs equipped with a subsumption relation›

text ‹In this section, we define subsumption relations and the notion of sub\hyp{}paths in 
rooted graphs equipped with such relations. Sub-paths are defined in the same way than in 
\verb?Graph.thy?: first we define the consistency of a sequence of edges in presence of a 
subsumption relation, then sub-paths. We are interested in subsumptions taking places between red 
vertices of red-black graphs (see \verb?RB.thy?), i.e.\ occurrences of locations of LTSs. Here 
subsumptions are defined as pairs of indexed vertices of a LTS, and subsumption relations as sets 
of subsumptions. The type of vertices of such LTSs is represented by the abstract type ‹'v› 
in the following.›

subsection ‹Basic definitions and properties›

subsubsection ‹Subsumptions and subsumption relations›

text ‹Subsumptions take place between occurrences of the vertices of a graph. We represent 
such occurrences by indexed versions of vertices. A subsumption is defined as pair of indexed 
vertices.›


type_synonym 'v sub_t = "(('v × nat) × ('v × nat))"


text ‹A subsumption relation is a set of subsumptions.›


type_synonym 'v sub_rel_t = "'v sub_t set"


text ‹We consider the left member to be subsumed by the right one. The left member of a 
subsumption is called its \emph{subsumee}, the right member its \emph{subsumer}.›


abbreviation subsumee :: 
  "'v sub_t ⇒ ('v × nat)" 
where 
  "subsumee sub ≡ fst sub"


abbreviation subsumer :: 
  "'v sub_t ⇒ ('v × nat)" 
where 
  "subsumer sub ≡ snd sub"


text ‹We will need to talk about the sets of subsumees and subsumers of a subsumption relation.›


abbreviation subsumees :: 
  "'v sub_rel_t ⇒ ('v × nat) set" 
where 
  "subsumees subs ≡ subsumee ` subs"


abbreviation subsumers :: 
  "'v sub_rel_t ⇒ ('v × nat) set" 
where 
  "subsumers subs ≡ subsumer ` subs"


text ‹The two following lemmas will prove useful in the following.›


lemma subsumees_conv :
  "subsumees subs = {v. ∃ v'. (v,v') ∈ subs}"
by force


lemma subsumers_conv :
  "subsumers subs = {v'. ∃ v. (v,v') ∈ subs}"
by force



text ‹We call set of vertices of the relation the union of its sets of subsumees and subsumers.›


abbreviation vertices ::
  "'v sub_rel_t ⇒ ('v × nat) set" 
where
  "vertices subs ≡ subsumers subs ∪ subsumees subs"


subsection ‹Well-formed subsumption relation of a graph›

subsubsection ‹Well-formed subsumption relations›

text ‹In the following, we make an intensive use of \emph{locales}. We use them as a convenient 
way to add assumptions to the following lemmas, in order to ease their reading. Locales can be 
built from locales, allowing some modularity in the formalization. The following locale simply 
states that we suppose there exists  a subsumption relation called \emph{subs}. It will 
be used later in order to constrain subsumption relations.›


locale sub_rel =
  fixes subs :: "'v sub_rel_t" (structure)


text ‹We are only interested in subsumptions involving two different
occurrences of the same LTS 
location. Moreover, once a vertex has been subsumed, there is no point in trying to subsume it again
by another subsumer: subsumees must have a unique subsumer. Finally, we do not allow chains of 
subsumptions, thus the intersection of the sets of subsumers and subsumees must be empty. Such 
subsumption relations are said to be \emph{well-formed}.›


locale wf_sub_rel = sub_rel +
  assumes sub_imp_same_verts : 
    "sub ∈ subs ⟹ fst (subsumee sub) = fst (subsumer sub)"
  
  assumes subsumed_by_one : 
    "∀ v ∈ subsumees subs. ∃! v'. (v,v') ∈ subs"
  
  assumes inter_empty : 
    "subsumers subs ∩ subsumees subs = {}"

begin
  lemmas wf_sub_rel = sub_imp_same_verts subsumed_by_one inter_empty

  text ‹A rephrasing of the assumption @{term "subsumed_by_one"}.›

  lemma (in wf_sub_rel) subsumed_by_two_imp : 
    assumes "(v,v1) ∈ subs"
    assumes "(v,v2) ∈ subs" 
    shows   "v1 = v2"
  using assms wf_sub_rel unfolding subsumees_conv by blast
  
  text ‹A well-formed subsumption relation is equal to its transitive closure. We will see in the 
  following one has to handle transitive closures of such relations.›

  lemma in_trancl_imp :
    assumes "(v,v') ∈ subs⇧+"
    shows   "(v,v') ∈ subs"
  using tranclD[OF assms] tranclD[of _ v' subs]
        rtranclD[of _ v' subs]  
        inter_empty 
  by force

  lemma trancl_eq :
    "subs⇧+ = subs"
  using in_trancl_imp r_into_trancl[of _ _ subs] by fast
end


text ‹The empty subsumption relation is well-formed.›


lemma
  "wf_sub_rel {}"
by (auto simp add : wf_sub_rel_def)


subsubsection ‹Subsumption relation of a graph›

text ‹We consider subsumption relations to equip rooted graphs. However, nothing in the previous 
definitions relates these relations to graphs: subsumptions relations involve objects that are of 
the type of indexed vertices, but that might to not be vertices of an actual graph. We equip 
graphs with subsumption relations using the notion of \emph{sub-relation of a graph}. Such a 
relation must only involve vertices of the graph it equips.›


locale rgraph = 
  fixes g :: "('v,'x) rgraph_scheme" (structure)


locale sub_rel_of = rgraph + sub_rel +
  assumes related_are_verts : "vertices subs ⊆ Graph.vertices g"
begin
  lemmas sub_rel_of = related_are_verts

  text ‹The transitive closure of a sub-relation of a graph @{term "g"} is also a sub-relation of 
  @{term "g"}.›

  lemma trancl_sub_rel_of :
     "sub_rel_of g (subs⇧+)"
  using tranclD[of _ _ subs] tranclD2[of _ _ subs] sub_rel_of
  unfolding sub_rel_of_def subsumers_conv subsumees_conv by blast
end


text ‹The empty relation is a sub-relation of any graph.›


lemma
  "sub_rel_of g {}"
by (auto simp add : sub_rel_of_def)


subsubsection ‹Well-formed sub-relations›

text ‹We pack both previous locales into a third one. We speak about 
\emph{well-formed sub-relations}.›


locale wf_sub_rel_of = rgraph + sub_rel +
  assumes sub_rel_of : "sub_rel_of g subs"
  assumes wf_sub_rel : "wf_sub_rel subs"
begin
  lemmas wf_sub_rel_of = sub_rel_of wf_sub_rel                                                       
end


text ‹The empty relation is a well-formed sub-relation of any graph.›


lemma
  "wf_sub_rel_of g {}"
by (auto simp add : sub_rel_of_def wf_sub_rel_def wf_sub_rel_of_def)


text ‹As previously, even if, in the end, we are only interested by well-formed sub-relations, we 
assume the relation is such only when needed.›

subsection ‹Consistent Edge Sequences, Sub-paths›

subsubsection ‹Consistency in presence of a subsumption relation›

text ‹We model sub-paths in the same spirit than in \verb?Graph.thy?, by starting with 
defining the consistency of a sequence of edges wrt.\ a subsumption relation. The idea is 
that subsumption links can ``fill the gaps'' between subsequent edges that would have made 
the sequence inconsistent otherwise. For now, we define consistency of a sequence wrt.\ any 
subsumption relation. Thus, we cannot account yet for the fact that we only consider relations 
without chains of subsumptions. The empty sequence is consistent wrt.\ to a subsumption relation 
from @{term "v1"} to @{term "v2"} if these two vertices are equal or if they belong to the 
transitive closure of the relation. A non-empty sequence is consistent if it is made of consistent 
sequences whose extremities are linked in the transitive closure of the subsumption relation.›


fun ces :: "('v × nat) ⇒ ('v × nat) edge list ⇒ ('v × nat) ⇒ 'v sub_rel_t ⇒ bool" where
  "ces v1 [] v2 subs = (v1 = v2  ∨ (v1,v2) ∈ subs⇧+)"
| "ces v1 (e#es) v2 subs = ((v1 = src e ∨ (v1,src e) ∈ subs⇧+) ∧ ces (tgt e) es v2 subs)"


text ‹A consistent sequence from @{term "v1"} to @{term "v2"} without a  subsumption relation is 
consistent between these two vertices in presence of any relation.›


lemma
  assumes "Graph.ces v1 es v2"
  shows   "ces v1 es v2 subs"
using assms by (induct es arbitrary : v1, auto)


text ‹Consistency in presence of the empty subsumption relation reduces to consistency as defined 
in \verb?Graph.thy?.›


lemma
  assumes "ces v1 es v2 {}"
  shows   "Graph.ces v1 es v2"
using assms by (induct es arbitrary : v1, auto)


text ‹Let @{term "(v1,v2)"} be an element of a subsumption relation, and @{term "es"} a sequence of 
edges consistent wrt.\ this relation from vertex @{term "v2"}. Then @{term "es"} is also consistent 
from @{term "v1"}. Even if this lemma will not be used much in the following, this is the base fact 
for saying that paths feasible from a subsumee are also feasible from its subsumer.›


lemma acas_imp_dcas :
  assumes "(v1,v2) ∈ subs"
  assumes "ces v2 es v subs"
  shows   "ces v1 es v subs"
using assms by (cases es, simp_all) (intro disjI2, force)+


text ‹Let @{term "es"} be a sequence of edges consistent wrt. a subsumption relation. Extending 
this relation preserves the consistency of @{term "es"}.›


lemma ces_Un :
  assumes "ces v1 es v2  subs1"
  shows   "ces v1 es v2 (subs1 ∪ subs2)"
using assms by (induct es arbitrary : v1, auto simp add : trancl_mono)


text ‹A rephrasing of the previous lemma.›


lemma cas_subset :
  assumes "ces v1 es v2  subs1"
  assumes "subs1 ⊆ subs2"
  shows   "ces v1 es v2 subs2"
using assms by (induct es arbitrary : v1, auto simp add : trancl_mono)


text ‹Simplification lemmas for @{term "ces"}.›


lemma ces_append_one :
  "ces v1 (es @ [e]) v2 subs = (ces v1 es (src e) subs ∧ ces (src e) [e] v2 subs)"
by (induct es arbitrary : v1, auto)


lemma ces_append :
  "ces v1 (es1 @ es2) v2 subs = (∃ v. ces v1 es1 v subs ∧ ces v es2 v2 subs)"
proof (intro iffI, goal_cases)
  case 1 thus ?case 
  by (induct es1 arbitrary : v1)  
     (simp_all del : split_paired_Ex, blast)
next
  case 2 thus ?case
  proof (induct es1 arbitrary : v1)
    case (Nil v1)

    then obtain v where "ces v1 [] v subs" 
                  and   "ces v es2 v2 subs" 
    by blast

    thus ?case
    unfolding ces.simps
    proof (elim disjE, goal_cases)
      case 1 thus ?case by simp
    next
      case 2 thus ?case by (cases es2) (simp, intro disjI2, fastforce)+
    qed
  next
    case Cons thus ?case by auto
  qed
qed


text ‹Let @{term "es"} be a sequence of edges consistent from @{term "v1"} to @{term "v2"} wrt.\ a 
sub-relation @{term "subs"} of a graph @{term "g"}. Suppose elements of this sequence are edges of 
@{term "g"}. If @{term "v1"} is a vertex of @{term "g"} then @{term "v2"} is also a vertex of 
@{term "g"}.›


lemma (in sub_rel_of) ces_imp_ends_vertices :
  assumes "ces v1 es v2 subs"
  assumes "set es ⊆ edges g"
  assumes "v1 ∈ Graph.vertices g"
  shows   "v2 ∈ Graph.vertices g"
using assms trancl_sub_rel_of 
unfolding sub_rel_of_def subsumers_conv vertices_def
by (induct es arbitrary : v1) (force, (simp del : split_paired_Ex, fast))


subsubsection ‹Sub-paths›

text ‹A sub-path leading from @{term "v1"} to @{term "v2"}, two vertices of a graph @{term "g"} 
equipped with a subsumption relation @{term "subs"}, is a sequence of edges consistent wrt.\ 
@{term "subs"} from @{term "v1"} to @{term "v2"} whose elements are edges of @{term "g"}. 
Moreover, we must assume that @{term "subs"} is a sub-relation of @{term "g"}, otherwise 
@{term "es"} could ``exit'' @{term "g"} through subsumption links.›


definition subpath :: 
  "(('v × nat),'x) rgraph_scheme ⇒ ('v × nat) ⇒ ('v × nat) edge list ⇒ ('v × nat) ⇒ (('v × nat) × ('v × nat)) set ⇒ bool" 
where
  "subpath g v1 es v2 subs ≡ sub_rel_of g subs 
                           ∧ v1 ∈ Graph.vertices g
                           ∧ ces v1 es v2 subs  
                           ∧ set es ⊆ edges g"


text ‹Once again, in some cases, we will not be interested in the ending vertex of a sub-path.›


abbreviation subpath_from ::
  "(('v × nat),'x) rgraph_scheme ⇒ ('v × nat) ⇒ ('v × nat) edge list ⇒ 'v sub_rel_t ⇒ bool"
where
  "subpath_from g v es subs ≡ ∃ v'. subpath g v es v' subs"


text ‹Simplification lemmas for @{term subpath}.›


lemma Nil_sp :
  "subpath g v1 [] v2 subs ⟷ sub_rel_of g subs 
                             ∧ v1 ∈ Graph.vertices g 
                             ∧ (v1 = v2 ∨ (v1,v2) ∈ subs⇧+)"
by (auto simp add : subpath_def)


text ‹When the subsumption relation is well-formed (denoted by ‹(in wf_sub_rel)›), 
there is no need to account for the transitive closure of the relation.›


lemma (in wf_sub_rel) Nil_sp :
  "subpath g v1 [] v2 subs ⟷ sub_rel_of g subs 
                             ∧ v1 ∈ Graph.vertices g 
                             ∧ (v1 = v2 ∨ (v1,v2) ∈ subs)"
using trancl_eq by (simp add : Nil_sp)


text ‹Simplification lemma for the one-element sequence.›


lemma sp_one :
  shows   "subpath g v1 [e] v2 subs ⟷ sub_rel_of g subs 
                                      ∧ (v1 = src e ∨ (v1,src e) ∈ subs⇧+) 
                                      ∧ e ∈ edges g 
                                      ∧ (tgt e = v2 ∨ (tgt e,v2) ∈ subs⇧+)"
using sub_rel_of.trancl_sub_rel_of[of g subs]
by (intro iffI, auto simp add : vertices_def sub_rel_of_def subpath_def) 


text ‹Once again, when the subsumption relation is well-formed, the previous lemma can be 
simplified since, in this case, the transitive closure of the relation is the relation itself.›


lemma (in wf_sub_rel_of) sp_one :
  shows "subpath g v1 [e] v2 subs ⟷ sub_rel_of g subs 
                                    ∧ (v1 = src e ∨ (v1,src e) ∈ subs) 
                                    ∧ e ∈ edges g 
                                    ∧ (tgt e = v2 ∨ (tgt e,v2) ∈ subs)"
using sp_one wf_sub_rel.trancl_eq[OF wf_sub_rel] by fast


text ‹Simplification lemma for the non-empty sequence (which might contain more than one element).›


lemma sp_Cons :
  shows   "subpath g v1 (e # es) v2 subs ⟷ sub_rel_of g subs 
                                           ∧ (v1 = src e  ∨ (v1,src e) ∈ subs⇧+) 
                                           ∧ e ∈ edges g 
                                           ∧ subpath g (tgt e) es v2 subs"
using sub_rel_of.trancl_sub_rel_of[of g subs] 
by (intro iffI, auto simp add : subpath_def vertices_def sub_rel_of_def)


text ‹The same lemma when the subsumption relation is well-formed.›


lemma (in wf_sub_rel_of) sp_Cons :
  "subpath g v1 (e # es) v2 subs ⟷ sub_rel_of g subs 
                                   ∧ (v1 = src e ∨ (v1,src e) ∈ subs) 
                                   ∧ e ∈ edges g 
                                   ∧ subpath g (tgt e) es v2 subs"
using sp_Cons wf_sub_rel.trancl_eq[OF wf_sub_rel] by fast


text ‹Simplification lemma for @{term "subpath"} when the sequence is known to end by a given 
edge.›


lemma sp_append_one :
  "subpath g v1 (es @ [e]) v2 subs ⟷ subpath g v1 es (src e) subs 
                                     ∧ e ∈ edges g  
                                     ∧ (tgt e = v2 ∨ (tgt e, v2) ∈ subs⇧+)"
unfolding subpath_def by (auto simp add :  ces_append_one)


text ‹Simpler version in the case of a well-formed subsumption relation.›


lemma (in wf_sub_rel) sp_append_one :
  "subpath g v1 (es @ [e]) v2 subs ⟷ subpath g v1 es (src e) subs 
                                     ∧ e ∈ edges g  
                                     ∧ (tgt e = v2 ∨ (tgt e, v2) ∈ subs)"
using sp_append_one in_trancl_imp by fast


text ‹Simplification lemma when the sequence is known to be the concatenation of two 
sub-sequences.›


lemma sp_append :
  "subpath g v1 (es1 @ es2) v2 subs ⟷ 
   (∃ v. subpath g v1 es1 v subs ∧ subpath g v es2 v2 subs)"
proof (intro iffI, goal_cases)
  case 1 thus ?case 
  using sub_rel_of.ces_imp_ends_vertices 
  by (simp add : subpath_def ces_append) blast
next
  case 2 thus ?case 
  unfolding subpath_def 
  by (simp only : ces_append) fastforce
qed


text ‹Let @{term "es"} be a sub-path of a graph @{term "g"} starting at vertex @{term "v1"}. 
By definition of @{term "subpath"}, @{term "v1"} is a vertex of @{term "g"}. Even if this is a 
direct consequence of the definition of @{term "subpath"}, this lemma will ease the proofs of some 
goals in the following.›


lemma fst_of_sp_is_vert :
  assumes "subpath g v1 es v2 subs"
  shows   "v1 ∈ Graph.vertices g"
using assms by (simp add : subpath_def)


text ‹The same property (which also follows the definition of @{term "subpath"}, but not as 
trivially as the previous lemma) can be established for the final vertex @{term "v2"}.›


lemma lst_of_sp_is_vert :
  assumes "subpath g v1 es v2 subs"
  shows   "v2 ∈ Graph.vertices g"
using assms sub_rel_of.trancl_sub_rel_of[of g subs]
by (induction es arbitrary : v1) 
   (force simp add : subpath_def sub_rel_of_def, (simp add : sp_Cons, fast))


text ‹A sub-path ending in a subsumed vertex can be extended to the subsumer of this vertex, 
provided that the subsumption relation is a sub-relation of the graph it equips.›


lemma sp_append_sub :
  assumes "subpath g v1 es v2 subs"
  assumes "(v2,v3) ∈ subs"
  shows   "subpath g v1 es v3 subs"
proof (cases es)
  case Nil

  moreover
  hence "v1 ∈ Graph.vertices g" 
  and   "v1 = v2 ∨ (v1,v2) ∈ subs⇧+" 
  using assms(1) by (simp_all add : Nil_sp)

  ultimately
  show ?thesis 
  using assms(1,2) 
        Nil_sp[of g v1 v2 subs] 
        trancl_into_trancl[of v1 v2 subs v3] 
  by (auto simp add : subpath_def)
next
  case Cons

  then obtain es' e where "es = es' @ [e]" using neq_Nil_conv2[of es] by blast

  thus ?thesis using assms trancl_into_trancl by (simp add : sp_append_one) fast
qed


text ‹Let @{term "g"} be a graph equipped with a well-formed sub-relation. A sub-path starting at 
a subsumed vertex @{term "v1"} whose set of out-edges is empty is either:
\begin{enumerate}
  \item empty,
  \item a sub-path starting at the subsumer @{term "v2"} of @{term "v1"}.
\end{enumerate}
The third assumption represent the fact that, when building red-black graphs, we do not allow to 
build the successor of a subsumed vertex.›


lemma (in wf_sub_rel_of) sp_from_subsumee :
  assumes "(v1,v2) ∈ subs"
  assumes "subpath g v1 es v subs"
  assumes "out_edges g v1 = {}"               
  shows   "es = [] ∨ subpath g v2 es v subs"
using assms
      wf_sub_rel.subsumed_by_two_imp[OF wf_sub_rel assms(1)] 
by (cases es) 
   (fast, (intro disjI2, fastforce simp add : sp_Cons))


text ‹Note that it is not possible to split this lemma into two lemmas (one for each member of the 
disjunctive conclusion). Suppose @{term "v"} is @{term "v1"}, then 
@{term "es"} could be empty or it could also be a non-empty sub-path leading from @{term "v2"} to 
@{term "v1"}. If @{term "v"} is not @{term "v1"}, it could be @{term "v2"} and @{term "es"} could 
be empty or not.›


text ‹A sub-path starting at a non-subsumed vertex whose set of out-edges is empty is also empty.›


lemma sp_from_de_empty :
  assumes "v1 ∉ subsumees subs"
  assumes "out_edges g v1 = {}"
  assumes "subpath g v1 es v2 subs"
  shows   "es = []"
using assms tranclD by (cases es) (auto simp add : sp_Cons, force)


text ‹Let @{term "e"} be an edge whose target is not subsumed and has not out-going edges. A 
sub-path @{term "es"} containing @{term "e"} ends by @{term "e"} and this occurrence of @{term "e"} 
is unique along @{term "es"}.›


lemma sp_through_de_decomp :
  assumes "tgt e ∉ subsumees subs"
  assumes "out_edges g (tgt e) = {}"
  assumes "subpath g v1 es v2 subs"
  assumes "e ∈ set es"
  shows   "∃ es'. es = es' @ [e] ∧ e ∉ set es'"
using assms(3,4)
proof (induction es arbitrary : v1)
  case (Nil v1) thus ?case by simp
next
  case (Cons e' es v1)

  hence "subpath g (tgt e') es v2 subs" 
  and  "e = e' ∨ (e ≠ e' ∧ e ∈ set es)" by (auto simp add : sp_Cons)

  thus ?case 
  proof (elim disjE, goal_cases)
    case 1 thus ?case 
    using sp_from_de_empty[OF assms(1,2)] by fastforce
  next
    case 2 thus ?case using Cons(1)[of "tgt e'"] by force
  qed
qed


text ‹Consider a sub-path ending at the target of a recently added edge @{term "e"}, whose target 
did not belong to the graph prior to its addition. If @{term "es"} starts in another vertex than 
the target of @{term "e"}, then it contains @{term "e"}.›


lemma (in sub_rel_of) sp_ends_in_tgt_imp_mem :
  assumes "tgt e ∉ Graph.vertices g"
  assumes "v ≠ tgt e"
  assumes "subpath (add_edge g e) v es (tgt e) subs"
  shows   "e ∈ set es"
proof -
  have "tgt e ∉ subsumers subs" using assms(1) sub_rel_of by auto

  hence "(v,tgt e) ∉ subs⇧+" using tranclD2 by force

  hence "es ≠ []" using assms(2,3) by (auto simp add : Nil_sp)

  then obtain es' e' where "es = es' @ [e']" by (simp add : neq_Nil_conv2) blast

  moreover
  hence "e' ∈ edges (add_edge g e)" using assms(3) by (auto simp add: subpath_def)
  
  moreover
  have "tgt e' = tgt e"  
  using tranclD2 assms(3) ‹tgt e ∉ subsumers subs› ‹es = es' @ [e']›
  by (force simp add : sp_append_one)
  
  ultimately
  show ?thesis using assms(1) unfolding vertices_def image_def by force
qed

end