Theory SubExt
theory SubExt
imports SubRel
begin
section ‹Extending subsomption relations›
text ‹In this section, we are interested in the evolution of the set of sub-paths of a rooted
graph equipped with a subsumption relation after adding a subsumption to this relation. We are
only interested in adding subsumptions such that the resulting relation is a well-formed
sub-relation of the graph (provided the original relation was such). As
for the extension
by edges, a number of side conditions must be met for the new subsumption to be added.›
subsection ‹Definition›
text ‹Extending a subsumption relation @{term subs} consists in adding a subsumption @{term "sub"}
such that:
\begin{itemize}
\item the two vertices involved are distinct,
\item they are occurrences of the same vertex,
\item they are both vertices of the graph,
\item the subsumee must not already be a subsumer or a subsumee,
\item the subsumer must not be a subsumee (but it can already be a subsumer),
\item the subsumee must have no out-edges.
\end{itemize}›
text ‹Once again, in order to ease proofs, we use a predicate stating when a
subsumpion relation is the extension of another instead of using a function that would produce the
extension.›
abbreviation extends ::
"(('v × nat),'x) rgraph_scheme ⇒ 'v sub_rel_t ⇒ 'v sub_t ⇒ 'v sub_rel_t ⇒ bool"
where
"extends g subs sub subs' ≡ (
subsumee sub ≠ subsumer sub
∧ fst (subsumee sub) = fst (subsumer sub)
∧ subsumee sub ∈ Graph.vertices g
∧ subsumee sub ∉ subsumers subs
∧ subsumee sub ∉ subsumees subs
∧ subsumer sub ∈ Graph.vertices g
∧ subsumer sub ∉ subsumees subs
∧ out_edges g (subsumee sub) = {}
∧ subs' = subs ∪ {sub})"
subsection ‹Properties of extensions›
text ‹First, we show that such extensions yield sub-relations (resp.\ well-formed relations),
provided the original relation is a sub-relation (resp.\ well-formed relation).›
text ‹Extending the sub-relation of a graph yields a new sub-relation for this graph.›
lemma (in sub_rel_of)
assumes "extends g subs sub subs'"
shows "sub_rel_of g subs'"
using assms sub_rel_of unfolding sub_rel_of_def by force
text ‹Extending a well-formed relation yields a well-formed relation.›
lemma (in wf_sub_rel) extends_imp_wf_sub_rel :
assumes "extends g subs sub subs'"
shows "wf_sub_rel subs'"
unfolding wf_sub_rel_def
proof (intro conjI, goal_cases)
case 1 show ?case using wf_sub_rel assms by auto
next
case 2 show ?case
unfolding Ball_def
proof (intro allI impI)
fix v
assume "v ∈ subsumees subs'"
hence "v = subsumee sub ∨ v ∈ subsumees subs" using assms by auto
thus "∃! v'. (v,v') ∈ subs'"
proof (elim disjE, goal_cases)
case 1 show ?thesis
unfolding Ex1_def
proof (rule_tac ?x="subsumer sub" in exI, intro conjI)
show "(v, subsumer sub) ∈ subs'" using 1 assms by simp
next
have "v ∉ subsumees subs" using assms 1 by auto
thus "∀ v'. (v, v') ∈ subs' ⟶ v' = subsumer sub"
using assms by auto force
qed
next
case 2
then obtain v' where "(v,v') ∈ subs" by auto
hence "v ≠ subsumee sub"
using assms unfolding subsumees_conv by (force simp del : split_paired_All split_paired_Ex)
show ?thesis
using assms
‹v ≠ subsumee sub›
‹(v,v') ∈ subs› subsumed_by_one
unfolding subsumees_conv Ex1_def
by (rule_tac ?x="v'" in exI)
(auto simp del : split_paired_All split_paired_Ex)
qed
qed
next
case 3 show ?case using wf_sub_rel assms by auto
qed
text ‹Thus, extending a well-formed sub-relation yields a well-formed sub-relation.›
lemma (in wf_sub_rel_of) extends_imp_wf_sub_rel_of :
assumes "extends g subs sub subs'"
shows "wf_sub_rel_of g subs'"
using sub_rel_of assms
wf_sub_rel.extends_imp_wf_sub_rel[OF wf_sub_rel assms]
by (simp add : wf_sub_rel_of_def sub_rel_of_def)
subsection ‹Properties of sub-paths in an extension›
text ‹Extending a sub-relation of a graph preserves the existing sub-paths.›
lemma sp_in_extends :
assumes "extends g subs sub subs'"
assumes "subpath g v1 es v2 subs"
shows "subpath g v1 es v2 subs'"
using assms ces_Un[of v1 es v2 subs "{sub}"]
by (simp add : subpath_def sub_rel_of_def)
text ‹We want to describe how the addition of a subsumption modifies the set of sub-paths in the
graph. As in the previous theories, we will focus on a small number of theorems expressing
sub-paths in extensions as functions of sub-paths in the graphs before extending them (their
subsumption relations).
We first express sub-paths starting at the subsumee of the new subsumption, then the sub-paths
starting at any other vertex.›
text ‹First, we are interested in sub-paths starting at the subsumee of the new subsumption. Since
such vertices have no out-edges, these sub-paths must be either empty or must be sub-paths from
the subsumer of this subsumption.›
lemma (in wf_sub_rel_of) sp_in_extends_imp1 :
assumes "extends g subs (v1,v2) subs'"
assumes "subpath g v1 es v subs'"
shows "es = [] ∨ subpath g v2 es v subs'"
using assms
extends_imp_wf_sub_rel_of[OF assms(1)]
wf_sub_rel_of.sp_from_subsumee[of g subs' v1 v2 es v]
by simp
text ‹After an extension, sub-paths starting at any other vertex than the new subsumee are either:
\begin{itemize}
\item sub-paths of the graph before the extension if they do not ``use'' the new subsumption,
\item made of a finite number of sub-paths of the graph before the extension if they use the
new subsumption.
\end{itemize}
In order to state the lemmas expressing these facts, we first need to introduce the concept of
\emph{usage} of a subsumption by a sub-path.›
text ‹The idea is that, if a sequence of edges that uses a subsumption @{term sub} is consistent
wrt.\ a subsumption relation @{term subs}, then @{term sub} must occur in the transitive closure
of @{term subs} i.e.\ the consistency of the sequence directly (and partially) depends on
@{term sub}. In the case of well-formed subsumption relations, whose transitive
closures equal the relations themselves, the dependency of the consistency reduces to the fact that
@{term sub} is a member of @{term subs}.›
fun uses_sub ::
"('v × nat) ⇒ ('v × nat) edge list ⇒ ('v × nat) ⇒ (('v × nat) × ('v × nat)) ⇒ bool"
where
"uses_sub v1 [] v2 sub = (v1 ≠ v2 ∧ sub = (v1,v2))"
| "uses_sub v1 (e#es) v2 sub = (v1 ≠ src e ∧ sub = (v1,src e) ∨ uses_sub (tgt e) es v2 sub)"
text ‹In order for a sequence @{term es} using the subsumption @{term sub} to be consistent wrt.\
to a subsumption relation @{term subs}, the subsumption @{term sub} must occur in the transitive
closure of @{term subs}.›
lemma
assumes "uses_sub v1 es v2 sub"
assumes "ces v1 es v2 subs"
shows "sub ∈ subs⇧+"
using assms by (induction es arbitrary : v1) fastforce+
text ‹This reduces to the membership of @{term sub} to @{term subs} when the latter is
well-formed.›
lemma (in wf_sub_rel)
assumes "uses_sub v1 es v2 sub"
assumes "ces v1 es v2 subs"
shows "sub ∈ subs"
using assms trancl_eq by (induction es arbitrary : v1) fastforce+
text ‹Sub-paths prior to the extension do not use the new subsumption.›
lemma extends_and_sp_imp_not_using_sub :
assumes "extends g subs (v,v') subs'"
assumes "subpath g v1 es v2 subs"
shows "¬ uses_sub v1 es v2 (v,v')"
proof (intro notI)
assume "uses_sub v1 es v2 (v,v')"
moreover
have "ces v1 es v2 subs" using assms(2) by (simp add : subpath_def)
ultimately
have "(v,v') ∈ subs⇧+" by (induction es arbitrary : v1) fastforce+
thus False
using assms(1) unfolding subsumees_conv
by (elim conjE) (frule tranclD, force)
qed
text ‹Suppose that the empty sequence is a sub-path leading from @{term v1} to @{term v2} after
the extension. Then, the empty sequence is a sub-path leading from @{term v1} to @{term v2}
in the graph before the extension if and only if @{term "(v1,v2)"} is not the new subsumption.›
lemma (in wf_sub_rel_of) sp_Nil_in_extends_imp :
assumes "extends g subs (v,v') subs'"
assumes "subpath g v1 [] v2 subs'"
shows "subpath g v1 [] v2 subs ⟷ (v1 ≠ v ∨ v2 ≠ v')"
proof (intro iffI, goal_cases)
case 1 thus ?case
using assms(1)
extends_and_sp_imp_not_using_sub[OF assms(1), of v1 "[]" v2]
by auto
next
case 2
have "v1 = v2 ∨ (v1,v2) ∈ subs'"
and "v1 ∈ Graph.vertices g"
using assms(2)
wf_sub_rel.extends_imp_wf_sub_rel[OF wf_sub_rel assms(1)]
by (simp_all add : wf_sub_rel.Nil_sp)
moreover
hence "v1 = v2 ∨ (v1,v2) ∈ subs"
using assms(1) 2 by auto
moreover
have "v2 ∈ Graph.vertices g"
using assms(2) by (intro lst_of_sp_is_vert)
ultimately
show "subpath g v1 [] v2 subs"
using sub_rel_of by (auto simp add : subpath_def)
qed
text ‹Thus, sub-paths after the extension that do not use the new subsumption are also sub-paths
before the extension.›
lemma (in wf_sub_rel_of) sp_in_extends_not_using_sub :
assumes "extends g subs (v,v') subs'"
assumes "subpath g v1 es v2 subs'"
assumes "¬ uses_sub v1 es v2 (v,v')"
shows "subpath g v1 es v2 subs"
using sub_rel_of assms extends_imp_wf_sub_rel_of
by (induction es arbitrary : v1)
(auto simp add : sp_Nil_in_extends_imp wf_sub_rel_of.sp_Cons sp_Cons)
text ‹We are finally able to describe sub-paths starting at any other vertex than the new
subsumee after the extension. Such sub-paths are made of a finite number of sub-paths before the
extension: the usage of the new subsumption between such (sub-)sub-paths makes them sub-paths
after the extension. We express this idea as follows. Sub-paths starting at any other vertex
than the new subsumee are either:
\begin{itemize}
\item sub-paths of the graph before the extension,
\item made of a non-empty prefix that is a sub-path leading to the new subsumee in the original
graph and a (potentially empty) suffix that is a sub-path starting at the new subsumer after
the extension.
\end{itemize}
For the second case, the lemma \verb?sp_in_extends_imp1? as well as the following lemma could be
applied to the suffix in order to decompose it into sub-paths of the graph before extension
(combined with the fact that we only consider finite sub-paths, we indirectly obtain that sub-paths
after the extension are made of a finite number of sub-paths before the extension, that are made
consistent with the new relation by using the new subsumption).›
lemma (in wf_sub_rel_of) sp_in_extends_imp2 :
assumes "extends g subs (v,v') subs'"
assumes "subpath g v1 es v2 subs'"
assumes "v1 ≠ v"
shows "subpath g v1 es v2 subs ∨ (∃ es1 es2. es = es1 @ es2
∧ es1 ≠ []
∧ subpath g v1 es1 v subs
∧ subpath g v es2 v2 subs')"
(is "?P es v1")
proof (case_tac "uses_sub v1 es v2 (v,v')", goal_cases)
case 1
thus ?thesis
using assms(2,3)
proof (induction es arbitrary : v1)
case (Nil v1) thus ?case by auto
next
case (Cons edge es v1)
hence "v1 = src edge ∨ (v1, src edge) ∈ subs'"
and "edge ∈ edges g"
and "subpath g (tgt edge) es v2 subs'"
using assms(1) extends_imp_wf_sub_rel_of
by (simp_all add : wf_sub_rel_of.sp_Cons)
hence "subpath g v1 [edge] (tgt edge) subs'"
using wf_sub_rel_of.sp_one[OF extends_imp_wf_sub_rel_of[OF assms(1)]]
by (simp add : subpath_def) fast
have "subpath g v1 [edge] (tgt edge) subs"
proof -
have "¬ uses_sub v1 [edge] (tgt edge) (v,v')"
using assms(1) Cons(2,4) by auto
thus ?thesis
using assms(1) ‹subpath g v1 [edge] (tgt edge) subs'›
by (elim sp_in_extends_not_using_sub)
qed
thus ?case
proof (case_tac "tgt edge = v", goal_cases)
case 1 thus ?thesis
using ‹subpath g v1 [edge] (tgt edge) subs›
‹subpath g (tgt edge) es v2 subs'›
by (intro disjI2, rule_tac ?x="[edge]" in exI) auto
next
case 2
moreover
have "uses_sub (tgt edge) es v2 (v,v')" using Cons(2,4) by simp
ultimately
have "?P es (tgt edge)"
using ‹subpath g (tgt edge) es v2 subs'›
by (intro Cons.IH)
thus ?thesis
proof (elim disjE exE conjE, goal_cases)
case 1 thus ?thesis
using ‹subpath g (tgt edge) es v2 subs'›
‹uses_sub (tgt edge) es v2 (v,v')›
extends_and_sp_imp_not_using_sub[OF assms(1)]
by fast
next
case (2 es1 es2) thus ?thesis
using ‹es = es1 @ es2›
‹subpath g v1 [edge] (tgt edge) subs›
‹subpath g v es2 v2 subs'›
by (intro disjI2, rule_tac ?x="edge # es1" in exI) (auto simp add : sp_Cons)
qed
qed
qed
next
case 2 thus ?thesis
using assms(1,2) by (simp add : sp_in_extends_not_using_sub)
qed
end