# Theory Graph

theory Graph
imports Main
begin

section‹Rooted Graphs›

text ‹In this section, we model rooted graphs and their sub\hyp{}paths and paths. We give a number
of lemmas that will help proofs in the following theories, but that are very specific to our
approach.›

text ‹First, we will need the following simple lemma, which is not graph related, but that will
prove useful when we will want to exhibit the last element of a non-empty sequence.›

lemma neq_Nil_conv2 :
"xs ≠ [] = (∃ x xs'. xs = xs' @ [x])"
by (induct xs rule : rev_induct, auto)

subsection ‹Basic Definitions and Properties›

subsubsection ‹Edges›

text ‹We model edges by a record ‹'v edge› which is parameterized by the type ‹'v›
of vertices. This allows us to represent the red part
of red-black graphs as well as the black part (i.e. LTS) using extensible records (more on this later). Edges have two
components, @{term "src"} and @{term "tgt"}, which respectively give their source and target.›

record 'v edge =
src   :: "'v"
tgt   :: "'v"

subsubsection ‹Rooted graphs›

text ‹We model rooted graphs by the record ‹'v rgraph›. It consists of two components: its
root and its set of edges.›

record 'v rgraph =
root  :: "'v"
edges :: "'v edge set"

subsubsection ‹Vertices›

text ‹The set of vertices of a rooted graph is made of its root and the endpoints of its
edges. Isabelle/HOL provides \emph{extensible records}, i.e.\ it is possible to define records using
existing records by adding components. The following definition suppose that @{term "g"} is of type
‹('v,'x) rgraph_scheme›, i.e.\ an object that has at least all the components of a
‹'v rgraph›. The second type parameter ‹'x› stands for the hypothetical type
parameters that such an object could have in addition of the type of vertices ‹'v›.
Using ‹('v,'x) rgraph_scheme› instead of ‹'v rgraph› allows to reuse the following
definition(s) for all type of objects that have at least the components of a rooted graph. For
example, we will reuse the following definition to characterize the set of locations of a LTS (see
\verb?LTS.thy?).›

definition vertices ::
"('v,'x) rgraph_scheme ⇒ 'v set"
where
"vertices g = {root g} ∪ src edges g ∪ tgt  edges g"

subsubsection ‹Basic properties of rooted graphs›

text ‹In the following, we will be only interested in loop free rooted graphs
and in what we call
\emph{well formed rooted graphs}. A well formed rooted graph is rooted graph that has an empty set
of edges or, if this is not the case, has at least one edge whose source is its root.›

abbreviation loop_free ::
"('v,'x) rgraph_scheme ⇒ bool"
where
"loop_free g ≡ ∀ e ∈ edges g. src e ≠ tgt e"

abbreviation wf_rgraph ::
"('v,'x) rgraph_scheme ⇒ bool"
where
"wf_rgraph g ≡ root g ∈ src  edges g = (edges g ≠ {})"

text ‹Even if we are only interested in this kind of rooted graphs, we will not assume the graphs
are loop free or well formed when this is not needed.›

subsubsection ‹Out-going edges›

text ‹This abbreviation will prove handy in the following.›

abbreviation out_edges ::
"('v,'x) rgraph_scheme ⇒ 'v ⇒ 'v edge set"
where
"out_edges g v ≡ {e ∈ edges g. src e = v}"

subsection ‹Consistent Edge Sequences, Sub-paths and Paths›

subsubsection ‹Consistency of a sequence of edges›

text ‹A sequence of edges @{term "es"} is consistent from
vertex @{term "v1"} to another vertex @{term "v2"} if @{term "v1 = v2"} if it is empty, or, if it is
not empty:
\begin{itemize}
\item @{term "v1"} is the source of its first element, and
\item @{term "v2"} is the target of its last element, and
\item the target of each of its elements is the source of its follower.
\end{itemize}›

fun ces ::
"'v ⇒ 'v edge list ⇒ 'v ⇒ bool"
where
"ces v1 [] v2 = (v1 = v2)"
| "ces v1 (e#es) v2 = (src e = v1 ∧ ces (tgt e) es v2)"

subsubsection ‹Sub-paths and paths›

text ‹Let @{term "g"} be a rooted graph, @{term "es"} a sequence of edges and @{term "v1"} and
‹v2› two vertices. @{term "es"} is a sub-path in @{term "g"} from @{term "v1"} to
@{term "v2"} if:
\begin{itemize}
\item it is consistent from @{term "v1"} to @{term "v2"},
\item @{term "v1"} is a vertex of @{term "g"},
\item all of its elements are edges of @{term "g"}.
\end{itemize}

The second constraint is needed in the case of the empty sequence: without it,
the empty sequence would be a sub-path of @{term "g"} even when @{term "v1"} is not one of
its vertices.›

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

text ‹Let @{term "es"} be a sub-path of @{term "g"} leading from @{term "v1"} to @{term "v2"}.
@{term "v1"} and @{term "v2"} are both vertices of @{term "g"}.›

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

lemma lst_of_sp_is_vert :
assumes "subpath g v1 es v2"
shows   "v2 ∈ vertices g"
using assms by (induction es arbitrary : v1, auto simp add: subpath_def vertices_def)

text ‹The empty sequence of edges is a sub-path from @{term "v1"} to @{term "v2"} if and only if
they are equal and belong to the graph.›

text ‹The empty sequence is a sub-path from the root of any rooted graph.›

lemma
"subpath g (root g) [] (root g)"
by (auto simp add : vertices_def subpath_def)

text ‹In the following, we will not always be interested in the final vertex of a sub-path. We
will use the abbreviation @{term "subpath_from"} whenever this final vertex has no importance, and
@{term subpath} otherwise.›

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

abbreviation subpaths_from ::
"('v,'x) rgraph_scheme ⇒ 'v ⇒ 'v edge list set"
where
"subpaths_from g v ≡ {es. subpath_from g v es}"

text ‹A path is a sub-path starting at the root of the graph.›

abbreviation path ::
"('v,'x) rgraph_scheme ⇒ 'v edge list ⇒ 'v ⇒ bool"
where
"path g es v ≡ subpath g (root g) es v"

abbreviation paths ::
"('a,'b) rgraph_scheme ⇒ 'a edge list set"
where
"paths g ≡ {es. ∃ v. path g es v}"

text ‹The empty sequence is a path of any rooted graph.›

lemma
"[] ∈ paths g"
by (auto simp add : subpath_def vertices_def)

text ‹Some useful simplification lemmas for @{term "subpath"}.›

lemma sp_one :
"subpath g v1 [e] v2 = (src e = v1 ∧ e ∈ edges g ∧ tgt e = v2)"
by (auto simp add : subpath_def vertices_def)

lemma sp_Cons :
"subpath g v1 (e#es) v2 = (src e = v1 ∧ e ∈ edges g ∧ subpath g (tgt e) es v2)"
by (auto simp add : subpath_def vertices_def)

lemma sp_append_one :
"subpath g v1 (es@[e]) v2 = (subpath g v1 es (src e) ∧ e ∈ edges g ∧ tgt e = v2)"
by (induct es arbitrary : v1, auto simp add : subpath_def vertices_def)

lemma sp_append :
"subpath g v1 (es1@es2) v2 = (∃ v. subpath g v1 es1 v ∧ subpath g v es2 v2)"
by (induct es1 arbitrary : v1)
(auto simp add : fst_of_sp_is_vert sp_Cons))

text ‹A sub-path leads to a unique vertex.›

lemma sp_same_src_imp_same_tgt :
assumes "subpath g v es v1"
assumes "subpath g v es v2"
shows   "v1 = v2"
using assms
by (induct es arbitrary : v)
(auto simp add :  sp_Cons subpath_def vertices_def)

text ‹In the following, we are interested in the evolution of the set of sub-paths of our symbolic
execution graph after symbolic execution of a transition from the LTS representation of the program
under analysis. Symbolic execution of a transition results in adding to the graph a new edge whose
source is already a vertex of this graph, but not its target. The following lemma describes
sub-paths ending in the target of such an edge.›

text ‹Let @{term "e"} be an edge whose target 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 "out_edges g (tgt e) = {}"
assumes "subpath g v1 es v2"
assumes "e ∈ set es"
shows   "∃ es'. es = es' @ [e] ∧ e ∉ set es'"
using assms(2,3)
proof (induction es arbitrary : v1)
case Nil thus ?case by simp
next
case (Cons e' es)

hence "e = e' ∨ (e ≠ e' ∧ e ∈ set es)" by auto

thus ?case
proof (elim disjE, goal_cases)
case 1 thus ?case
using assms(1) Cons
by (rule_tac ?x="[]" in exI) (cases es, auto simp add: sp_Cons)
next
case 2 thus ?case
using assms(1) Cons(1)[of "tgt e'"] Cons(2)
by (auto simp add : sp_Cons)
qed
qed

text ‹This definition and the following lemma are here mainly to ease the definitions and proofs
in the next theories.›

"('v,'x) rgraph_scheme ⇒ 'v edge ⇒ ('v,'x) rgraph_scheme"
where
"add_edge g e ≡ rgraph.edges_update (λ edges. edges ∪ {e}) g"

text ‹Let @{term "es"} be a sub-path from a vertex other than the target of @{term "e"} in the
graph obtained from @{term "g"} by the addition of edge @{term "e"}. Moreover, assume that the
target of @{term "e"} is not a vertex of @{term "g"}. Then @{term "e"} is an element of
@{term "es"}.›

lemma sp_ends_in_tgt_imp_mem :
assumes "tgt e ∉ vertices g"
assumes "v ≠ tgt e"
assumes "subpath (add_edge g e) v es (tgt e)"
shows   "e ∈ set es"
proof -
have "es ≠ []" using assms(2,3) by (auto simp add : subpath_def)

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

thus ?thesis using assms(1,3) by (auto simp add : sp_append_one vertices_def image_def)
qed

subsection ‹Trees›

text ‹We define trees as rooted-graphs in which there exists a unique path leading to each vertex.›

definition is_tree ::
"('v,'x) rgraph_scheme ⇒ bool"
where
"is_tree g ≡ ∀ l ∈ Graph.vertices g. ∃! p. Graph.path g p l"

text ‹The empty graph is thus a tree.›

lemma empty_graph_is_tree :
assumes "edges g = {}"
shows   "is_tree g"
using assms by (auto simp add : is_tree_def subpath_def vertices_def)

end


# Theory Aexp

theory Aexp
imports Main
begin

section‹Arithmetic Expressions›

text ‹In this section, we model arithmetic expressions as total functions from valuations of
program variables to values. This modeling does not take into consideration the syntactic aspects
of arithmetic expressions. Thus, our modeling holds for any operator. However, some classical
notions, like the set of variables occurring in a given expression for example, must be rethought
and defined accordingly.›

subsection‹Variables and their domain›

text ‹\textbf{Note}: in the following theories, we distinguish the set of \emph{program variables}
and the set
of \emph{symbolic variables}. A number of types we define are parameterized by a type of variables.
For example, we make a distinction between expressions (arithmetic or boolean) over program
variables and expressions over symbolic variables. This distinction eases some parts of the following
formalization.›

paragraph ‹Symbolic variables.›

text ‹A \emph{symbolic variable} is an indexed version of a program variable. In the following
type-synonym, we consider that the abstract type ‹'v› represent the set of program
variables. By set
of program variables, we do not mean \emph{the set of variables of a given program}, but
\emph{the set of variables of all possible programs}. This distinction justifies some of the
program variables is infinite, though it is not needed to make this assumption. On the other hand,
the set of symbolic variables is infinite, independently of the fact that the set of program
variables is finite or not.›

type_synonym 'v symvar = "'v × nat"

lemma
"¬ finite (UNIV::'v symvar set)"

text ‹The previous lemma has no name and thus cannot be referenced in the following. Indeed, it is
of no use for proving the properties we are interested in. In the following, we will give other
unnamed lemmas when we think they might help the reader to understand the ideas behind our modeling
choices.›

paragraph ‹Domain of variables.›

text ‹We call @{term "D"} the domain of program and symbolic variables. In the following, we
suppose that @{term "D"} is the set of integers.›

subsection‹Program and symbolic states›

text ‹A state is a total function giving values in @{term "D"} to variables. The latter are
represented by elements of type ‹'v›. Unlike in the ‹'v symvar› type-synonym, here
the type ‹'v› can stand for program variables as well as symbolic variables. States over
program variables are called \emph{program states}, and states over symbolic variables are called
\emph{symbolic states}.›
type_synonym ('v,'d) state = "'v ⇒ 'd"

subsection‹The \emph{aexp} type-synonym›

text ‹Arithmetic (and boolean, see \verb?Bexp.thy?) expressions are represented by their
semantics, i.e.\
total functions giving values in @{term "D"} to states. This way of representing expressions has
the benefit that it is not necessary to define the syntax of terms (and formulae) appearing
in program statements and path predicates.›

type_synonym ('v,'d) aexp =  "('v,'d) state ⇒ 'd"

text ‹In order to represent expressions over program variables as well as symbolic variables,
the type synonym @{type "aexp"} is parameterized by the type of variables. Arithmetic and boolean
expressions over program variables are used to express program statements. Arithmetic and boolean
expressions over symbolic variables are used to represent the constraints occurring in path
predicates during symbolic execution.›

subsection‹Variables of an arithmetic expression›

text‹Expressions being represented by total functions, one can not say that a given variable is
occurring in a given expression. We define the set of variables of an expression as the set of
variables that can actually have an influence on the value associated by an expression to a state.
For example, the set of variables of the expression @{term "λ σ. σ x - σ y"} is @{term "{x,y}"},
provided that @{term "x"} and @{term "y"} are distinct variables, and the empty set otherwise. In
the second case, this expression would evaluate to $0$ for any state @{term
"σ"}. Similarly, an expression like
@{term "λ σ.  σ x * (0::nat)"} is considered as having no
variable as if a static evaluation of the multiplication had occurred.
›

definition vars ::
"('v,'d) aexp ⇒ 'v set"
where
"vars e = {v. ∃ σ val. e (σ(v := val)) ≠ e σ}"

lemma vars_example_1 :
fixes e::"('v,integer) aexp"
assumes "e = (λ σ. σ x - σ y)"
assumes "x ≠ y"
shows   "vars e = {x,y}"
unfolding set_eq_iff
proof (intro allI iffI)
fix v assume "v ∈ vars e"

then obtain σ val
where "e (σ(v := val)) ≠ e σ"
unfolding vars_def by blast

thus "v ∈ {x, y}"
using assms by (case_tac "v = x", simp, (case_tac "v = y", simp+))
next
fix v assume "v ∈ {x,y}"

thus "v ∈ vars e"
using assms
by (auto simp add : vars_def)
(rule_tac ?x="λ v. 0" in exI, rule_tac ?x="1" in exI, simp)+
qed

lemma vars_example_2 :
fixes e::"('v,integer) aexp"
assumes "e = (λ σ. σ x - σ y)"
assumes "x = y"
shows   "vars e = {}"
using assms by (auto simp add : vars_def)

subsection‹Fresh variables›

text ‹Our notion of symbolic execution suppose \emph{static single assignment
form}. In order to symbolically execute an assignment, we require the existence of a fresh
symbolic variable for the configuration from which symbolic execution is performed. We define here
the notion of \emph{freshness} of a variable for an arithmetic expression.›

text ‹A variable is fresh for an expression if does not belong to its set of variables.›

abbreviation fresh ::
"'v ⇒ ('v,'d) aexp ⇒ bool"
where
"fresh v e ≡ v ∉ vars e"

end


# Theory Bexp

theory Bexp
imports Aexp
begin

section ‹Boolean Expressions›

text ‹We proceed as in \verb?Aexp.thy?.›

subsection‹Basic definitions›

subsubsection ‹The $\mathit{bexp}$ type-synonym›

text ‹We represent boolean expressions, their set of variables and the notion of freshness of a
variable in the same way than for arithmetic expressions.›

type_synonym ('v,'d) bexp = "('v,'d) state ⇒ bool"

definition vars ::
"('v,'d) bexp ⇒ 'v set"
where
"vars e = {v. ∃ σ val. e (σ(v := val)) ≠ e σ}"

abbreviation fresh ::
"'v ⇒ ('v,'d) bexp ⇒ bool"
where
"fresh v e ≡ v ∉ vars e"

subsubsection‹Satisfiability of an expression›

text ‹A boolean expression @{term "e"} is satisfiable if there exists a state @{term "σ"} such
that @{term "e σ"} is \emph{true}.›

definition sat ::
"('v,'d) bexp ⇒ bool"
where
"sat e = (∃ σ. e σ)"

subsubsection ‹Entailment›

text ‹A boolean expression @{term "φ"} entails another boolean expression @{term "ψ"} if all
states making @{term "φ"} true also make @{term "ψ"} true.›

definition entails ::
"('v,'d) bexp ⇒ ('v,'d) bexp ⇒ bool" (infixl "⊨⇩B" 55)
where
"φ ⊨⇩B ψ ≡ (∀ σ. φ σ ⟶ ψ σ)"

subsubsection ‹Conjunction›

text ‹In the following, path predicates are represented by sets of boolean expressions. We define
the conjunction of a set of boolean expressions @{term "E"} as the expression that
associates \emph{true} to a state @{term "σ"} if, for all elements ‹e› of
@{term "E"}, @{term "e"} associates \emph{true} to @{term "σ"}.›

definition conjunct ::
"('v,'d) bexp set ⇒ ('v,'d) bexp"
where
"conjunct E ≡ (λ σ. ∀ e ∈ E. e σ)"

subsection‹Properties about the variables of an expression›

text ‹As said earlier, our definition of symbolic execution requires the existence of a fresh
symbolic variable in the case of an assignment. In the following, a number of proof relies on this
fact. We will show the existence of such variables assuming the set of symbolic variables already in
use is finite and show that symbolic execution preserves the finiteness of this set, under certain
conditions. This in turn
requires a number of lemmas about the finiteness of boolean expressions.
More precisely, when symbolic execution goes through a guard or an assignment, it conjuncts a new
expression to the path predicate. In the case of an assignment, this new expression is an equality
linking the new symbolic variable associated to the defined program variable to its symbolic value.
In the following, we prove that:
\begin{enumerate}
\item the conjunction of a finite set of expressions whose sets of variables are finite has a
finite set of variables,
\item the equality of two arithmetic expressions whose sets of variables are finite has a finite
set of variables.
\end{enumerate}›

subsubsection ‹Variables of a conjunction›

text ‹The set of variables of the conjunction of two expressions is a subset of the union of the
sets of variables of the two sub-expressions. As a consequence, the set of variables of the conjunction
of a finite set of expressions whose sets of variables are finite is also finite.›

lemma vars_of_conj :
"vars (λ σ. e1 σ ∧ e2 σ) ⊆ vars e1 ∪ vars e2"
(is "vars ?e ⊆ vars e1 ∪ vars e2")
unfolding subset_iff
proof (intro allI impI)
fix v assume "v ∈ vars ?e"

then obtain σ val
where "?e (σ (v := val)) ≠ ?e σ"
unfolding vars_def by blast

hence "e1 (σ (v := val)) ≠ e1 σ ∨ e2 (σ (v := val)) ≠ e2 σ"
by auto

thus "v ∈ vars e1 ∪ vars e2" unfolding vars_def by blast
qed

lemma finite_conj :
assumes "finite E"
assumes "∀ e ∈ E. finite (vars e)"
shows   "finite (vars (conjunct E))"
using assms
proof (induct rule : finite_induct, goal_cases)
case 1 thus ?case by (simp add : vars_def conjunct_def)
next
case (2 e E)

thus ?case
using vars_of_conj[of e "conjunct E"]
by (rule_tac rev_finite_subset, auto simp add : conjunct_def)
qed

subsubsection ‹Variables of an equality›

text ‹We proceed analogously for the equality of two arithmetic expressions.›

lemma vars_of_eq_a :
shows  "vars (λ σ. e1 σ = e2 σ) ⊆ Aexp.vars e1 ∪ Aexp.vars e2"
(is "vars ?e ⊆ Aexp.vars e1 ∪ Aexp.vars e2")
unfolding subset_iff
proof (intro allI impI)

fix v assume "v ∈ vars ?e"

then obtain σ val where "?e (σ (v := val)) ≠ ?e σ"
unfolding vars_def by blast

hence "e1 (σ (v := val)) ≠ e1 σ ∨ e2 (σ (v := val)) ≠ e2 σ"
by auto

thus "v ∈ Aexp.vars e1 ∪ Aexp.vars e2"
unfolding Aexp.vars_def by blast
qed

lemma finite_vars_of_a_eq :
assumes "finite (Aexp.vars e1)"
assumes "finite (Aexp.vars e2)"
shows   "finite (vars (λ σ. e1 σ = e2 σ))"
using assms vars_of_eq_a[of e1 e2] by (rule_tac rev_finite_subset, auto)

end


# Theory Labels

theory Labels
imports Aexp Bexp
begin

(* DEF : 2 *)
(* LEM : 0 *)

section ‹Labels›

text ‹In the following, we model programs by control flow graphs where edges (rather than vertices) are labelled
with either assignments or with the condition associated with a branch of a conditional statement.
We put a label on every edge : statements that do not modify the program state (like \verb?jump?,
\verb?break?, etc) are labelled by a @{term Skip}.›

datatype ('v,'d) label = Skip | Assume "('v,'d) bexp" | Assign 'v "('v,'d) aexp"

text ‹We say that a label is \emph{finite} if the set of variables of its sub-expression is
finite (@{term Skip} labels are thus considered finite).›

definition finite_label ::
"('v,'d) label ⇒ bool"
where
"finite_label l ≡ case l of
Assume e   ⇒ finite (Bexp.vars e)
| Assign _ e ⇒ finite (Aexp.vars e)
| _          ⇒ True"

abbreviation finite_labels ::
"('v,'d) label list ⇒ bool"
where
"finite_labels ls ≡ (∀ l ∈ set ls. finite_label l)"

end


# Theory Store

theory Store
imports Aexp Bexp
begin

section‹Stores›

text ‹In this section, we introduce the type of stores, which we use to link program variables
with their symbolic counterpart during symbolic execution. We define the notion of consistency
of a pair of program and symbolic states w.r.t.\ a store. This notion will prove helpful when
defining various concepts and proving facts related to subsumption (see \verb?Conf.thy?). Finally, we
model substitutions that will be performed during symbolic execution (see \verb?SymExec.thy?) by two

subsection ‹Basic definitions›

subsubsection ‹The @{term "store"} type-synonym›

text ‹Symbolic execution performs over configurations (see \verb?Conf.thy?), which are pairs made
of:
\begin{itemize}
\item a \emph{store} mapping program variables to symbolic variables,
\item a set of boolean expressions which records constraints over symbolic variables and whose
conjunction is the actual path predicate of the configuration.
\end{itemize}
We define stores as total functions from program variables to indexes.›

type_synonym 'a store = "'a ⇒ nat"

subsubsection ‹Symbolic variables of a store›

text ‹The symbolic variable associated to a program variable @{term "v"} by a store
@{term "s"} is the couple @{term "(v,s v)"}.›

definition symvar ::
"'a ⇒ 'a store ⇒ 'a symvar"
where
"symvar v s ≡ (v,s v)"

text ‹The function associating symbolic variables to program variables obtained from
@{term "s"} is injective.›

lemma
"inj (λ v. symvar v s)"
by (auto simp add : inj_on_def symvar_def)

text ‹The sets of symbolic variables of a store is the image set of the function @{term "symvar"}.›

definition symvars ::
"'a store ⇒ 'a symvar set"
where
"symvars s = (λ v. symvar v s)  (UNIV::'a set)"

subsubsection ‹Fresh symbolic variables›

text ‹A symbolic variable is said to be fresh for a store if it is not a member of its set of
symbolic variables.›

definition fresh_symvar ::
"'v symvar ⇒ 'v store ⇒ bool"
where
"fresh_symvar sv s = (sv ∉ symvars s)"

subsection ‹Consistency›

text ‹We say that a program state @{term "σ"} and a symbolic state @{term "σ⇩s⇩y⇩m"} are
\emph{consistent} with respect to a store @{term "s"} if, for each variable @{term "v"}, the
value associated by @{term "σ"} to @{term "v"} is equal to the value associated by @{term "σ⇩s⇩y⇩m"}
to the symbolic variable associated to @{term "v"} by @{term "s"}.›

definition consistent ::
"('v,'d) state ⇒ ('v symvar, 'd) state ⇒ 'v store ⇒ bool"
where
"consistent σ σ⇩s⇩y⇩m s ≡ (∀ v. σ⇩s⇩y⇩m (symvar v s) = σ v)"

text ‹There always exists a couple of consistent states for a given store.›

lemma
"∃ σ σ⇩s⇩y⇩m. consistent σ σ⇩s⇩y⇩m s"
by (auto simp add : consistent_def)

text ‹Moreover, given a store and a program (resp. symbolic) state, one can always build a symbolic
(resp. program) state such that the two states are coherent wrt.\ the store. The four following
lemmas show how to build the second state given the first one.›

lemma consistent_eq1 :
"consistent σ σ⇩s⇩y⇩m s = (∀ sv ∈ symvars s. σ⇩s⇩y⇩m sv = σ (fst sv))"
by (auto simp add : consistent_def symvars_def symvar_def)

lemma consistent_eq2 :
"consistent σ σ⇩s⇩y⇩m store = (σ = (λ v. σ⇩s⇩y⇩m (symvar v store)))"
by (auto simp add : consistent_def)

lemma consistentI1 :
"consistent σ (λ sv. σ (fst sv)) store"
using consistent_eq1 by fast

lemma consistentI2 :
"consistent (λ v. σ⇩s⇩y⇩m (symvar v store)) σ⇩s⇩y⇩m store"
using consistent_eq2 by fast

subsection ‹Adaptation of an arithmetic expression to a store›

text ‹Suppose that @{term "e"} is a term representing an arithmetic expression over program
variables and let @{term "s"} be a store. We call \emph{adaptation of @{term "e"} to @{term "s"}}
the term obtained by substituting occurrences of program variables in @{term "e"} by their
symbolic counterpart given by @{term "s"}. Since we model arithmetic expressions by total
functions and not terms, we define the adaptation of such expressions as follows.›

"('v,'d) aexp ⇒ 'v store ⇒ ('v symvar,'d) aexp"
where
"adapt_aexp e s = (λ σ⇩s⇩y⇩m. e (λ v. σ⇩s⇩y⇩m (symvar v s)))"

text ‹Given an arithmetic expression @{term "e"}, a program state @{term "σ"} and a symbolic
state @{term "σ⇩s⇩y⇩m"} coherent with a store @{term "s"}, the value associated to @{term "σ⇩s⇩y⇩m"} by
the adaptation of @{term "e"} to @{term "s"} is the same than the value associated by @{term "e"} to
@{term "σ"}. This confirms the fact that @{term "adapt_aexp"} models the act of substituting
occurrences of program variables by their symbolic counterparts in a term over program variables.›

assumes "consistent σ σ⇩s⇩y⇩m s"
shows   "(adapt_aexp e s) σ⇩s⇩y⇩m = e σ"

text ‹As said earlier, we will later need to prove that symbolic execution preserves finiteness
of the set of symbolic variables in use, which requires that the adaptation of an arithmetic
expression to a store preserves finiteness of the set of variables of expressions. We proceed as
follows.›

text ‹First, we show that if @{term "v"} is a variable of an expression @{term "e"},
then the symbolic variable associated to @{term "v"} by a store is a variable of the adaptation of
@{term "e"} to this store.›

lemma var_imp_symvar_var :
assumes "v ∈ Aexp.vars e"
shows   "symvar v s ∈ Aexp.vars (adapt_aexp e s)" (is "?sv ∈ Aexp.vars ?e'")
proof -
obtain σ val where "e (σ (v := val)) ≠ e σ"
using assms unfolding Aexp.vars_def by blast

moreover
have "(λva. ((λsv. σ (fst sv))(?sv := val)) (symvar va s)) = (σ(v := val))"
by (auto simp add : symvar_def)

ultimately
show ?thesis
unfolding Aexp.vars_def mem_Collect_eq
using consistentI1[of σ s]
consistentI2[of "(λsv. σ (fst sv))(?sv:= val)" s]
by (rule_tac ?x="λsv. σ (fst sv)" in exI, rule_tac ?x="val" in exI)
qed

text ‹On the other hand, if @{term "sv"} is a symbolic variable in the adaptation of an expression
to a store, then the program variable it represents is a variable of this expression. This requires
to prove that the set of variables of the adaptation of an expression to a store is a subset of the
symbolic variables of this store.›

"Aexp.vars (adapt_aexp e s) ⊆ symvars s" (is "Aexp.vars ?e' ⊆ symvars s")
unfolding subset_iff
proof (intro allI impI)
fix sv

assume "sv ∈ Aexp.vars ?e'"

then obtain σ⇩s⇩y⇩m val
where "?e' (σ⇩s⇩y⇩m (sv := val)) ≠ ?e' σ⇩s⇩y⇩m"
by (simp add : Aexp.vars_def, blast)

hence "(λ x. (σ⇩s⇩y⇩m (sv := val)) (symvar x s)) ≠ (λ x. σ⇩s⇩y⇩m (symvar x s))"
proof (intro notI)
assume "(λx. (σ⇩s⇩y⇩m(sv := val)) (symvar x s)) = (λx. σ⇩s⇩y⇩m (symvar x s))"

hence "?e' (σ⇩s⇩y⇩m (sv := val)) = ?e' σ⇩s⇩y⇩m"

thus False
using ‹?e' (σ⇩s⇩y⇩m (sv := val)) ≠ ?e' σ⇩s⇩y⇩m›
by (elim notE)
qed

then obtain v
where "(σ⇩s⇩y⇩m (sv := val)) (symvar v s) ≠ σ⇩s⇩y⇩m (symvar v s)"
by blast

hence "sv = symvar v s" by (case_tac "sv = symvar v s", simp_all)

thus "sv ∈ symvars s" by (simp add : symvars_def)
qed

lemma symvar_var_imp_var :
assumes "sv ∈ Aexp.vars (adapt_aexp e s)" (is "sv ∈ Aexp.vars ?e'")
shows   "fst sv ∈ Aexp.vars e"
proof -
obtain v where "sv = (v, s v)"
unfolding symvars_def symvar_def
by blast

obtain σ⇩s⇩y⇩m val where "?e' (σ⇩s⇩y⇩m (sv := val)) ≠ ?e' σ⇩s⇩y⇩m"
using assms unfolding Aexp.vars_def by blast

moreover
have "(λ v. (σ⇩s⇩y⇩m (sv := val)) (symvar v s)) = (λ v. σ⇩s⇩y⇩m (symvar v s)) (v := val)"
using ‹sv = (v, s v)› by (auto simp add : symvar_def)

ultimately
show ?thesis
using ‹sv = (v, s v)›
consistentI2[of σ⇩s⇩y⇩m s]
consistentI2[of "σ⇩s⇩y⇩m (sv := val)" s]
unfolding Aexp.vars_def
qed

text ‹Thus, we have that the set of variables of the adaptation of an expression to a store is
the set of symbolic variables associated by this store to the variables of this
expression.›

"Aexp.vars (adapt_aexp e s) = (λ v. symvar v s)  Aexp.vars e"
unfolding set_eq_iff image_def mem_Collect_eq Bex_def
proof (intro allI iffI, goal_cases)
case (1 sv)

moreover
have "sv = symvar (fst sv) s"
by (force simp add:  symvar_def symvars_def)

ultimately
show ?case using symvar_var_imp_var by blast
next
case (2 sv) thus ?case using var_imp_symvar_var by fast
qed

text ‹The fact that the adaptation of an arithmetic expression to a store preserves finiteness
of the set of variables trivially follows the previous lemma.›

assumes "finite (Aexp.vars e)"
shows   "finite (Aexp.vars (adapt_aexp e s))"
unfolding adapt_aexp_vars using assms by auto

subsection ‹Adaptation of a boolean expression to a store›

text ‹We proceed analogously for the adaptation of boolean expressions to a store.›

"('v,'d) bexp ⇒ 'v store ⇒ ('v symvar,'d) bexp"
where
"adapt_bexp e s = (λ σ. e (λ x. σ (symvar x s)))"

assumes "consistent σ σ⇩s⇩y⇩m s"
shows   "(adapt_bexp e s) σ⇩s⇩y⇩m = e σ"

lemma var_imp_symvar_var2 :
assumes "v ∈ Bexp.vars e"
shows   "symvar v s ∈ Bexp.vars (adapt_bexp e s)" (is "?sv ∈ Bexp.vars ?e'")
proof -
obtain σ val where A : "e (σ (v := val)) ≠ e σ"
using assms unfolding Bexp.vars_def by blast

moreover
have "(λva. ((λsv. σ (fst sv))(?sv := val)) (symvar va s)) = (σ(v := val))"
by (auto simp add : symvar_def)

ultimately
show ?thesis
unfolding Bexp.vars_def mem_Collect_eq
using consistentI1[of σ s]
consistentI2[of "(λsv. σ (fst sv))(?sv:= val)" s]
by (rule_tac ?x="λsv. σ (fst sv)" in exI, rule_tac ?x="val" in exI)
qed

"Bexp.vars (adapt_bexp e s) ⊆ symvars s" (is "Bexp.vars ?e' ⊆ ?SV")
proof
fix sv
assume "sv ∈ Bexp.vars ?e'"

then obtain σ⇩s⇩y⇩m val
where "?e' (σ⇩s⇩y⇩m (sv := val)) ≠ ?e' σ⇩s⇩y⇩m"
by (simp add : Bexp.vars_def, blast)

hence "(λ x. (σ⇩s⇩y⇩m (sv := val)) (symvar x s)) ≠ (λ x. σ⇩s⇩y⇩m (symvar x s))"

hence "∃ v. (σ⇩s⇩y⇩m (sv := val)) (symvar v s) ≠ σ⇩s⇩y⇩m (symvar v s)" by force

then obtain v
where "(σ⇩s⇩y⇩m (sv := val)) (symvar v s) ≠ σ⇩s⇩y⇩m (symvar v s)"
by blast

hence "sv = symvar v s" by (case_tac "sv = symvar v s", simp_all)

thus "sv ∈ symvars s" by (simp add : symvars_def)
qed

lemma symvar_var_imp_var2 :
assumes "sv ∈ Bexp.vars (adapt_bexp e s)" (is "sv ∈ Bexp.vars ?e'")
shows   "fst sv ∈ Bexp.vars e"
proof -
obtain v where "sv = (v, s v)"
unfolding symvars_def symvar_def
by blast

obtain σ⇩s⇩y⇩m val where "?e' (σ⇩s⇩y⇩m (sv := val)) ≠ ?e' σ⇩s⇩y⇩m"
using assms unfolding vars_def by blast

moreover
have "(λ v. (σ⇩s⇩y⇩m (sv := val)) (symvar v s)) = (λ v. σ⇩s⇩y⇩m (symvar v s)) (v := val)"
using ‹sv = (v, s v)› by (auto simp add : symvar_def)

ultimately
show ?thesis
using ‹sv = (v, s v)›
consistentI2[of σ⇩s⇩y⇩m s]
consistentI2[of "σ⇩s⇩y⇩m (sv := val)" s]
qed

"Bexp.vars (adapt_bexp e s) = (λ v. symvar v s)  Bexp.vars e"
(is "Bexp.vars ?e' = ?R")
unfolding set_eq_iff image_def mem_Collect_eq Bex_def
proof (intro allI iffI, goal_cases)
case (1 sv)

hence "fst sv ∈ vars e" by (rule symvar_var_imp_var2)

moreover
have "sv = symvar (fst sv) s"
by (force simp add:  symvar_def symvars_def)

ultimately
show ?case by blast
next
case (2 sv)

then obtain v where "v ∈ vars e" "sv = symvar v s" by blast

thus ?case using var_imp_symvar_var2 by simp
qed

assumes "finite (Bexp.vars e)"
shows   "finite (Bexp.vars (adapt_bexp e s))"
unfolding adapt_bexp_vars using assms by auto

end


# Theory Conf

theory Conf
imports Store
begin

section ‹Configurations, Subsumption and Symbolic Execution›

text ‹In this section, we first introduce most elements related to our modeling of program
behaviors. We first define the type of configurations, on which symbolic execution performs, and
define the various concepts we will rely upon in the following and state and prove properties about
them. Then, we introduce symbolic execution. After giving a number of basic properties about
symbolic execution, we prove that symbolic execution is monotonic with respect to the subsumption
relation, which is a crucial point in order to prove the main theorems of \verb?RB.thy?. Moreover,
Isabelle/HOL requires the actual formalization of a number of facts one would not worry when
implementing or writing a sketch proof. Here, we will need to prove that there exist successors of
the configurations on which symbolic execution is performed. Although this seems quite obvious in
practice, proofs of such facts will be needed a number of times in the following theories. Finally,
we define the feasibility of a sequence of labels.›

subsection ‹Basic Definitions and Properties›

subsubsection‹Configurations›

text ‹Configurations are pairs @{term "(store,pred)"} where:
\begin{itemize}
\item @{term "store"} is a store mapping program variable to symbolic variables,
\item @{term "pred"} is a set of boolean expressions over program variables whose conjunction is
the actual path predicate.
\end{itemize}›

record ('v,'d) conf =
store :: "'v store"
pred  :: "('v symvar,'d) bexp set"

subsubsection ‹Symbolic variables of a configuration.›

text ‹The set of symbolic variables of a configuration is the union of the set of symbolic
variables of its store component with the set of variables of its path predicate.›

definition symvars ::
"('v,'d) conf ⇒ 'v symvar set"
where
"symvars c = Store.symvars (store c) ∪ Bexp.vars (conjunct (pred c))"

subsubsection ‹Freshness.›

text ‹A symbolic variable is said to be fresh for a configuration if it is not an element of its
set of symbolic variables.›

definition fresh_symvar ::
"'v symvar ⇒ ('v,'d) conf ⇒ bool"
where
"fresh_symvar sv c = (sv ∉ symvars c)"

subsubsection ‹Satisfiability›

text ‹A configuration is said to be satisfiable if its path predicate is satisfiable.›

abbreviation sat ::
"('v,'d) conf ⇒ bool"
where
"sat c ≡ Bexp.sat (conjunct (pred c))"

subsubsection ‹States of a configuration›

text ‹Configurations represent sets of program states. The set of program states represented by a
configuration, or simply its set of program states, is defined as the set of program states such that
consistent symbolic states wrt.\ the store component of the configuration satisfies its path
predicate.›

definition states ::
"('v,'d) conf ⇒ ('v,'d) state set"
where
"states c = {σ. ∃ σ⇩s⇩y⇩m. consistent σ σ⇩s⇩y⇩m (store c) ∧ conjunct (pred c) σ⇩s⇩y⇩m}"

text ‹A configuration is satisfiable if and only if its set of states is not empty.›

lemma sat_eq :
"sat c = (states c ≠ {})"
using consistentI2 by (simp add : sat_def states_def) fast

subsubsection ‹Subsumption›

text ‹A configuration @{term "c⇩2"} is subsumed by a configuration @{term "c⇩1"} if the set of
states of @{term "c⇩2"} is a subset of the set of states of @{term "c⇩1"}.›

definition subsums ::
"('v,'d) conf ⇒ ('v,'d) conf ⇒ bool" (infixl "⊑" 55)
where
"c⇩2 ⊑ c⇩1 ≡ (states c⇩2 ⊆ states c⇩1)"

text ‹The subsumption relation is reflexive and transitive.›

lemma subsums_refl :
"c ⊑ c"
by (simp only : subsums_def)

lemma subsums_trans :
"c1 ⊑ c2 ⟹ c2 ⊑ c3 ⟹ c1 ⊑ c3"
unfolding subsums_def by simp

text ‹However, it is not anti-symmetric. This is due to the fact that different configurations
can have the same sets of program states. However, the following lemma trivially follows the
definition of subsumption.›

lemma
assumes "c1 ⊑ c2"
assumes "c2 ⊑ c1"
shows   "states c1 = states c2"
using assms by (simp add : subsums_def)

text ‹A satisfiable configuration can only be subsumed by satisfiable configurations.›

lemma sat_sub_by_sat :
assumes "sat c⇩2"
and     "c⇩2 ⊑ c⇩1"
shows   "sat c⇩1"
using assms sat_eq[of c⇩1] sat_eq[of c⇩2]
by (simp add : subsums_def) fast

text ‹On the other hand, an unsatisfiable configuration can only subsume unsatisfiable
configurations.›

lemma unsat_subs_unsat :
assumes "¬ sat c1"
assumes "c2 ⊑ c1"
shows   "¬ sat c2"
using assms sat_eq[of c1] sat_eq[of c2]

subsubsection ‹Semantics of a configuration›

text ‹The semantics of a configuration @{term "c"} is a boolean expression @{term "e"} over
program states associating \emph{true} to a program state if it is a state of @{term "c"}. In
practice, given two configurations @{term "c⇩1"} and @{term "c⇩2"}, it is not possible to enumerate
their sets of states to establish the inclusion in order to detect a subsumption. We detect the
subsumption of the former by the latter by asking a constraint solver if @{term "sem c⇩1"} entails
@{term "sem c⇩2"}. The following theorem shows that the way we detect subsumption in practice is
correct.›

definition sem ::
"('v,'d) conf ⇒ ('v,'d) bexp"
where
"sem c = (λ σ. σ ∈ states c)"

theorem
"c⇩2 ⊑ c⇩1 ⟷ sem c⇩2 ⊨⇩B sem c⇩1"
unfolding subsums_def sem_def subset_iff entails_def by (rule refl)

subsubsection ‹Abstractions›

text ‹Abstracting a configuration consists in removing a given expression from its @{term "pred"}
component, i.e.\ weakening its path predicate. This definition of abstraction motivates the fact
that the @{term "pred"} component of configurations has been defined as a set of boolean expressions

definition abstract ::
"('v,'d) conf ⇒ ('v,'d) conf ⇒ bool"
where
"abstract c c⇩a ≡ c ⊑ c⇩a"

subsubsection ‹Entailment›

text ‹A configuration \emph{entails} a boolean expression if its semantics entails this expression.
This is equivalent to say that this expression holds for any state of this configuration.›

abbreviation entails ::
"('v,'d) conf ⇒ ('v,'d) bexp ⇒ bool" (infixl "⊨⇩c" 55)
where
"c ⊨⇩c φ ≡ sem c ⊨⇩B φ"

lemma
"sem c ⊨⇩B e ⟷ (∀ σ ∈ states c. e σ)"
by (auto simp add : states_def sem_def entails_def)

end


# Theory SymExec

theory SymExec
imports Conf Labels
begin

subsection ‹Symbolic Execution›

text ‹We model symbolic execution by an inductive predicate @{term "se"} which takes two
configurations @{term "c⇩1"} and @{term "c⇩2"} and a label @{term "l"} and evaluates to \emph{true} if
and only if @{term "c⇩2"} is a \emph{possible result} of the symbolic execution of @{term "l"} from
@{term "c⇩1"}. We say that @{term "c⇩2"} is a possible result because, when @{term "l"} is of the
form @{term "Assign v e"}, we associate a fresh symbolic variable to the program variable @{term "v"},
but we do no specify how this fresh variable is chosen (see the two assumptions in the third case).
We could have model @{term "se"} (and @{term "se_star"}) by a function producing the new
configuration, instead of using inductive predicates. However this would require to provide the two
said assumptions in each lemma involving @{term se}, which is not necessary using a predicate. Modeling
symbolic execution in this way has the advantage that it simplifies the following proofs while not

subsubsection ‹Definitions of $\mathit{se}$ and $\mathit{se\_star}$›

text ‹Symbolic execution of @{term "Skip"} does not change the configuration from which it is
performed.›

text ‹When the label
is of the form @{term "Assume e"}, the adaptation of @{term "e"} to the store is added to the
@{term "pred"} component.›

text ‹In the case of an assignment, the @{term "store"} component is updated
such that it now maps a fresh symbolic variable to the assigned program variable. A constraint
relating this program variable with its new symbolic value is added to the @{term "pred"}
component.›

text ‹The second assumption in the third case requires that there exists at least one fresh
symbolic variable for @{term "c"}. In the following, a number of theorems are needed
to show that such variables exist for the configurations on which symbolic execution is performed.
›

inductive se ::
"('v,'d) conf ⇒ ('v,'d) label ⇒ ('v,'d) conf ⇒ bool"
where
"se c Skip c"

| "se c (Assume e) ⦇ store = store c, pred = pred c ∪ {adapt_bexp e (store c)} ⦈"

| "fst sv = v        ⟹
fresh_symvar sv c ⟹
se c (Assign v e) ⦇ store = (store c)(v := snd sv),
pred  = pred c ∪ {(λ σ. σ sv = (adapt_aexp e (store c)) σ)} ⦈"

text ‹In the same spirit, we extend symbolic execution to sequence of labels.›

inductive se_star :: "('v,'d) conf ⇒ ('v,'d) label list ⇒ ('v,'d) conf ⇒ bool" where
"se_star c [] c"
| "se c1 l c2 ⟹ se_star c2 ls c3 ⟹ se_star c1 (l # ls) c3"

subsubsection ‹Basic properties of $\mathit{se}$›

text ‹If symbolic execution yields a satisfiable configuration, then it has been performed from
a satisfiable configuration.›

lemma se_sat_imp_sat :
assumes "se c l c'"
assumes "sat c'"
shows   "sat c"
using assms by cases (auto simp add : sat_def conjunct_def)

text ‹If symbolic execution is performed from an unsatisfiable configuration, then it will yield
an unsatisfiable configuration.›

lemma unsat_imp_se_unsat :
assumes "se c l c'"
assumes "¬ sat c"
shows   "¬ sat c'"
using assms by cases (simp add : sat_def conjunct_def)+

text ‹Given two configurations @{term "c"} and @{term "c'"} and a label @{term "l"} such that
@{term "se c l c'"}, the three following lemmas express @{term "c'"} as a function of @{term "c"}.›

lemma [simp] :
"se c Skip c' = (c' = c)"

lemma se_Assume_eq :
"se c (Assume e) c' = (c' = ⦇ store = store c, pred = pred c ∪ {adapt_bexp e (store c)} ⦈)"

lemma se_Assign_eq :
"se c (Assign v e) c' =
(∃ sv. fresh_symvar sv c
∧ fst sv = v
∧ c' = ⦇ store = (store c)(v := snd sv),
pred  = insert (λσ. σ sv = adapt_aexp e (store c) σ) (pred c)⦈)"
by (simp only : se.simps, blast)

text ‹Given two configurations @{term "c"} and @{term "c'"} and a label @{term "l"} such that
@{term "se c l c'"}, the two following lemmas express the path predicate of @{term "c'"} as
a function of the path predicate of @{term "c"} when @{term "l"} models a guard or an
assignment.›

lemma path_pred_of_se_Assume :
assumes "se c (Assume e) c'"
shows   "conjunct (pred c') =
(λ σ. conjunct (pred c) σ ∧ adapt_bexp e (store c) σ)"
using assms se_Assume_eq[of c e c']
by (auto simp add : conjunct_def)

lemma path_pred_of_se_Assign :
assumes "se c (Assign v e) c'"
shows   "∃ sv. conjunct (pred c') =
(λ σ. conjunct (pred c) σ ∧ σ sv = adapt_aexp e (store c) σ)"
using assms se_Assign_eq[of c v e c']
by (fastforce simp add : conjunct_def)

text ‹Let @{term "c"} and @{term "c'"} be two configurations  such that @{term "c'"} is obtained
from @{term "c"} by symbolic execution of a label of the form @{term "Assume e"}. The states of
@{term "c'"} are the states of @{term "c"} that satisfy @{term "e"}. This theorem will help prove
that symbolic execution is monotonic wrt.\ subsumption.›

theorem states_of_se_assume :
assumes "se c (Assume e) c'"
shows   "states c' = {σ ∈ states c. e σ}"
using assms se_Assume_eq[of c e c']

text ‹Let @{term "c"} and @{term "c'"} be two configurations  such that @{term "c'"} is obtained
from @{term "c"} by symbolic execution of a label of the form @{term "Assign v e"}. We want to
express the set of states of @{term "c'"} as a function of the set of states of @{term "c"}. Since
the proof requires a number of details, we split into two sub lemmas.›

text ‹First, we show that if @{term "σ'"} is a state of @{term "c'"}, then it has been obtain from
an adequate update of a state @{term "σ"} of @{term "c"}.›

lemma states_of_se_assign1 :
assumes "se c (Assign v e) c'"
assumes "σ' ∈ states c'"
shows   "∃ σ ∈ states c. σ' = (σ (v := e σ))"
proof -
obtain σ⇩s⇩y⇩m
where 1 : "consistent σ' σ⇩s⇩y⇩m (store c')"
and   2 : "conjunct (pred c') σ⇩s⇩y⇩m"
using assms(2) unfolding states_def by blast

then obtain σ
where 3 : "consistent σ σ⇩s⇩y⇩m (store c)"
using consistentI2 by blast

moreover
have "conjunct (pred c) σ⇩s⇩y⇩m"
using assms(1) 2 by (auto simp add : se_Assign_eq conjunct_def)

ultimately
have "σ ∈ states c" by (simp add : states_def) blast

moreover
have "σ' = σ (v := e σ)"
proof -
have "σ' v = e σ"
proof -
have "σ' v = σ⇩s⇩y⇩m (symvar v (store c'))"
using 1 by (simp add : consistent_def)

moreover
have "σ⇩s⇩y⇩m (symvar v (store c')) = (adapt_aexp e (store c)) σ⇩s⇩y⇩m"
using assms(1) 2 se_Assign_eq[of c v e c']
by (force simp add : symvar_def conjunct_def)

moreover
have "(adapt_aexp e (store c)) σ⇩s⇩y⇩m = e σ"

ultimately
show ?thesis by simp
qed

moreover
have "∀ x. x ≠ v ⟶ σ' x = σ x"
proof (intro allI impI)
fix x

assume "x ≠ v"

moreover
hence "σ' x = σ⇩s⇩y⇩m (symvar x (store c))"
using assms(1) 1 unfolding consistent_def symvar_def
by (drule_tac ?x="x" in spec) (auto simp add : se_Assign_eq)

moreover
have "σ⇩s⇩y⇩m (symvar x (store c)) = σ x"
using 3 by (auto simp add : consistent_def)

ultimately
show "σ' x = σ x" by simp
qed

ultimately
show ?thesis by auto
qed

ultimately
show ?thesis by (simp add : states_def) blast
qed

text ‹Then, we show that if there exists a state @{term "σ"} of @{term "c"} from which
@{term "σ'"} is obtained by an adequate update, then @{term "σ'"} is a state of @{term "c'"}.›

lemma states_of_se_assign2 :
assumes "se c (Assign v e) c'"
assumes "∃ σ ∈ states c. σ' = σ (v := e σ)"
shows   "σ' ∈ states c'"
proof -
obtain σ
where "σ ∈ states c"
and   "σ' = σ (v := e σ)"
using assms(2) by blast

then obtain σ⇩s⇩y⇩m
where 1 : "consistent σ σ⇩s⇩y⇩m (store c)"
and   2 : "conjunct (pred c) σ⇩s⇩y⇩m"
unfolding states_def by blast

obtain sv
where 3 : "fresh_symvar sv c"
and   4 : "fst sv = v"
and   5 : "c' = ⦇ store = (store c)(v := snd sv),
pred    = insert (λσ. σ sv = adapt_aexp e (store c) σ) (pred c) ⦈"
using assms(1) se_Assign_eq[of c v e c'] by blast

define σ⇩s⇩y⇩m' where "σ⇩s⇩y⇩m' = σ⇩s⇩y⇩m (sv := e σ)"

have "consistent σ' σ⇩s⇩y⇩m' (store c')"
using ‹σ' = σ (v := e σ)› 1 4 5
by (auto simp add : symvar_def consistent_def σ⇩s⇩y⇩m'_def)

moreover
have "conjunct (pred c') σ⇩s⇩y⇩m'"
proof -
have "conjunct (pred c) σ⇩s⇩y⇩m'"
using 2 3 by (simp add : fresh_symvar_def symvars_def Bexp.vars_def σ⇩s⇩y⇩m'_def)

moreover
have "σ⇩s⇩y⇩m' sv = (adapt_aexp e (store c)) σ⇩s⇩y⇩m'"
proof -
have "Aexp.fresh sv (adapt_aexp e (store c))"
using 3 symvars_of_adapt_aexp[of e "store c"]
by (auto simp add : fresh_symvar_def symvars_def)

thus ?thesis
by (simp add : Aexp.vars_def σ⇩s⇩y⇩m'_def)
qed

ultimately
show ?thesis using 5 by (simp add: conjunct_def)
qed

ultimately
show ?thesis unfolding states_def by blast
qed

text ‹The following theorem expressing the set of states of @{term c'} as a function of the set
of states of @{term c} trivially follows the two preceding lemmas.›

theorem states_of_se_assign :
assumes "se c (Assign v e) c'"
shows   "states c' = {σ (v := e σ) | σ. σ ∈ states c}"
using assms states_of_se_assign1 states_of_se_assign2 by fast

subsubsection ‹Monotonicity of $\mathit{se}$›

text ‹We are now ready to prove that symbolic execution is monotonic with respect to subsumption.
›

theorem se_mono_for_sub :
assumes "se c1 l c1'"
assumes "se c2 l c2'"
assumes "c2 ⊑ c1"
shows   "c2' ⊑ c1'"
using assms
by ((cases l),
(simp add : states_of_se_assume subsums_def, blast),
(simp add : states_of_se_assign subsums_def, blast))

text ‹A stronger version of the previous theorem: symbolic execution is monotonic with respect to
states equality.›

theorem se_mono_for_states_eq :
assumes "states c1 = states c2"
assumes "se c1 l c1'"
assumes "se c2 l c2'"
shows   "states c2' = states c1'"
using assms(1)
se_mono_for_sub[OF assms(2,3)]
se_mono_for_sub[OF assms(3,2)]

text ‹The previous theorem confirms the fact that the way the fresh symbolic variable is chosen
in the case of symbolic execution of an assignment does not matter as long as the new symbolic
variable is indeed fresh, which is more precisely expressed by the following lemma.›

lemma se_succs_states :
assumes "se c l c1"
assumes "se c l c2"
shows   "states c1 = states c2"
using assms se_mono_for_states_eq by fast

subsubsection ‹Basic properties of $\mathit{se\_star}$›

text ‹Some simplification lemmas for @{term "se_star"}.›

lemma [simp] :
"se_star c [] c' = (c' = c)"
by (subst se_star.simps) auto

lemma se_star_Cons :
"se_star c1 (l # ls) c2 = (∃ c. se c1 l c ∧ se_star c ls c2)"
by (subst (1) se_star.simps) blast

lemma se_star_one :
"se_star c1 [l] c2 = se c1 l c2"
using se_star_Cons by force

lemma se_star_append :
"se_star c1 (ls1 @ ls2) c2 = (∃ c. se_star c1 ls1 c ∧ se_star c ls2 c2)"
by (induct ls1 arbitrary : c1, simp_all add : se_star_Cons) blast

lemma se_star_append_one :
"se_star c1 (ls @ [l]) c2 = (∃ c. se_star c1 ls c ∧ se c l c2)"
unfolding se_star_append se_star_one by (rule refl)

text ‹Symbolic execution of a sequence of labels from an unsatisfiable configuration yields
an unsatisfiable configuration.›

lemma unsat_imp_se_star_unsat :
assumes "se_star c ls c'"
assumes "¬ sat c"
shows   "¬ sat c'"
using assms
by (induct ls arbitrary : c)
(simp, force simp add : se_star_Cons unsat_imp_se_unsat)

text ‹If symbolic execution yields a satisfiable configuration, then it has been performed from
a satisfiable configuration.›

lemma se_star_sat_imp_sat :
assumes "se_star c ls c'"
assumes "sat c'"
shows   "sat c"
using assms
by (induct ls arbitrary : c)
(simp, force simp add : se_star_Cons se_sat_imp_sat)

subsubsection ‹Monotonicity of $\mathit{se\_star}$›

text ‹Monotonicity of @{term "se"} extends to @{term "se_star"}.›

theorem se_star_mono_for_sub :
assumes "se_star c1 ls c1'"
assumes "se_star c2 ls c2'"
assumes "c2  ⊑ c1"
shows   "c2' ⊑ c1'"
using assms
by (induct ls arbitrary : c1 c2)
(auto simp add :  se_star_Cons se_mono_for_sub)

lemma se_star_mono_for_states_eq :
assumes "states c1 = states c2"
assumes "se_star c1 ls c1'"
assumes "se_star c2 ls c2'"
shows   "states c2' = states c1'"
using assms(1)
se_star_mono_for_sub[OF assms(2,3)]
se_star_mono_for_sub[OF assms(3,2)]

lemma se_star_succs_states :
assumes "se_star c ls c1"
assumes "se_star c ls c2"
shows   "states c1 = states c2"
using assms se_star_mono_for_states_eq by fast

subsubsection ‹Existence of successors›

text ‹Here, we are interested in proving that, under certain assumptions, there will always exist
fresh symbolic variables for configurations on which symbolic execution is performed. Thus symbolic
execution cannot block'' when an assignment is met. For symbolic execution not to block in this
case, the configuration from which it is performed must be such that there exist fresh symbolic
variables for each program variable. Such configurations are said to be \emph{updatable}.›

definition updatable ::
"('v,'d) conf ⇒ bool"
where
"updatable c ≡ ∀ v. ∃ sv. fst sv = v ∧ fresh_symvar sv c"

text ‹The following lemma shows that being updatable is a sufficient condition for a configuration
in order for @{term "se"} not to block.›

lemma updatable_imp_ex_se_suc :
assumes "updatable c"
shows   "∃ c'. se c l c'"
using assms
by (cases l, simp_all add :  se_Assume_eq se_Assign_eq updatable_def)

text ‹A sufficient condition for a configuration to be updatable is that its path predicate has
a finite number of variables. The @{term "store"} component has no influence here, since its set of
symbolic variables is always a strict subset of the set of symbolic variables (i.e.\ there always
exist fresh symbolic variables for a store). To establish this proof, we need the following
intermediate lemma.›

text ‹We want to prove that if the set of symbolic variables of the path predicate of a
configuration is finite, then we can find a fresh symbolic variable for it. However, we express this
with a more general lemma. We show that given a finite set of symbolic variables @{term "SV"} and a
program variable @{term "v"} such that there exist symbolic variables in @{term "SV"} that are
indexed versions of @{term "v"}, then there exists a symbolic variable for @{term "v"} whose index
is greater or equal than the index of any other symbolic variable for @{term "v"} in @{term SV}.›

lemma finite_symvars_imp_ex_greatest_symvar :
fixes SV :: "'a symvar set"
assumes "finite SV"
assumes "∃ sv ∈ SV. fst sv = v"
shows   "∃ sv  ∈ {sv ∈ SV. fst sv = v}.
∀ sv' ∈ {sv ∈ SV. fst sv = v}. snd sv' ≤ snd sv"
proof -
have "finite (snd  {sv ∈ SV. fst sv = v})"
and  "snd  {sv ∈ SV. fst sv = v} ≠ {}"
using assms by auto

moreover
have "∀ (E::nat set). finite E ∧ E ≠ {} ⟶ (∃ n ∈ E. ∀ m ∈ E. m ≤ n)"
by (intro allI impI, induct_tac rule : finite_ne_induct)
(simp+, force)

ultimately
obtain n
where "n ∈ snd  {sv ∈ SV. fst sv = v}"
and   "∀ m ∈ snd  {sv ∈ SV. fst sv = v}. m ≤ n"
by blast

moreover
then obtain sv
where "sv ∈ {sv ∈ SV. fst sv = v}" and "snd sv = n"
by blast

ultimately
show ?thesis by blast
qed

text ‹Thus, a configuration whose path predicate has a finite set of variables is updatable. For
example, for any program variable @{term "v"}, the symbolic variable  ‹(v,i+1)› is fresh for
this configuration, where @{term "i"} is the greater index associated to @{term "v"} among the
symbolic variables of this configuration. In practice, this is how we choose the fresh symbolic
variable.›

lemma finite_pred_imp_se_updatable :
assumes "finite (Bexp.vars (conjunct (pred c)))" (is "finite ?V")
shows   "updatable c"
unfolding updatable_def
proof (intro allI)
fix v

show "∃sv. fst sv = v ∧ fresh_symvar sv c"
proof (case_tac "∃ sv ∈ ?V. fst sv = v", goal_cases)
case 1

then obtain max_sv
where       "max_sv ∈ ?V"
and         "fst max_sv = v"
and   max : "∀sv'∈{sv ∈ ?V. fst sv = v}. snd sv' ≤ snd max_sv"
using assms finite_symvars_imp_ex_greatest_symvar[of ?V v]
by blast

show ?thesis
using max
unfolding fresh_symvar_def symvars_def Store.symvars_def symvar_def
proof (case_tac "snd max_sv ≤ store c v", goal_cases)
case 1 thus ?case by (rule_tac ?x="(v,Suc (store c v))" in exI) auto
next
case 2 thus ?case by (rule_tac ?x="(v,Suc (snd max_sv))" in exI) auto
qed
next
case 2 thus ?thesis
by (rule_tac ?x="(v, Suc (store c v))" in exI)
(auto simp add : fresh_symvar_def symvars_def Store.symvars_def symvar_def)
qed
qed

text ‹The path predicate of a configuration whose @{term "pred"} component is finite and whose
elements all have finite sets of variables has a finite set of variables. Thus, this configuration
is updatable, and it has a successor by symbolic execution of any label. The following lemma
starts from these two assumptions and use the previous ones in order to directly get to the
conclusion (this will ease some of the following proofs).›

lemma finite_imp_ex_se_succ :
assumes "finite (pred c)"
assumes "∀ e ∈ pred c. finite (Bexp.vars e)"
shows   "∃ c'. se c l c'"
using finite_pred_imp_se_updatable[OF finite_conj[OF assms(1,2)]]
by (rule updatable_imp_ex_se_suc)

text ‹For symbolic execution not to block \emph{along a sequence of labels}, it is not sufficient
for the first configuration to be updatable. It must also be such that (all) its successors are
updatable. A sufficient condition for this is that the set of variables of its path predicate is
finite and that the sub-expression of the label that is executed also has a finite set of variables.
Under these assumptions, symbolic execution preserves finiteness of the @{term "pred"} component and
of the sets of variables of its elements. Thus, successors @{term "se"} are also updatable because
they also have a path predicate with a finite set of variables. In the following, to prove
this we need two intermediate lemmas:
\begin{itemize}
\item one stating that symbolic execution perserves the finiteness of the set of variables of the
elements of the @{term "pred"} component, provided that the sub expression of the label that is
executed has a finite set of variables,
\item one stating that symbolic execution preserves the finiteness of the @{term "pred"}
component.
\end{itemize}›

lemma se_preserves_finiteness1 :
assumes "finite_label l"
assumes "se c l c'"
assumes "∀ e ∈ pred c.  finite (Bexp.vars e)"
shows   "∀ e ∈ pred c'. finite (Bexp.vars e)"
proof (cases l)
case Skip thus ?thesis using assms by (simp add : )
next
case (Assume e) thus ?thesis
by (auto simp add : se_Assume_eq finite_label_def)
next
case (Assign v e)

then obtain sv
where "fresh_symvar sv c"
and   "fst sv = v"
and   "c' = ⦇ store = (store c)(v := snd sv),
pred  = insert (λσ. σ sv = adapt_aexp e (store c) σ) (pred c)⦈"
using assms(2) se_Assign_eq[of c v e c'] by blast

moreover
have "finite (Bexp.vars (λσ. σ sv = adapt_aexp e (store c) σ))"
proof -
have "finite (Aexp.vars (λσ. σ sv))"
by (auto simp add : Aexp.vars_def)

moreover
have "finite (Aexp.vars (adapt_aexp e (store c)))"
by (auto simp add : finite_label_def)

ultimately
show ?thesis using finite_vars_of_a_eq by auto
qed

ultimately
show ?thesis using assms by auto
qed

lemma se_preserves_finiteness2 :
assumes "se c l c'"
assumes "finite (pred c)"
shows   "finite (pred c')"
using assms
by (cases l)
(auto simp add :  se_Assume_eq se_Assign_eq)

text ‹We are now ready to prove that a sufficient condition for symbolic execution not to block
along a sequence of labels is that the @{term "pred"} component of the initial
configuration'' is finite, as well as the set of variables of its elements,  and that the
sub-expression of the label that is executed also has a finite set of variables.›

lemma finite_imp_ex_se_star_succ :
assumes "finite (pred c)"
assumes "∀ e ∈ pred c. finite (Bexp.vars e)"
assumes "finite_labels ls"
shows   "∃ c'. se_star c ls c'"
using assms
proof (induct ls arbitrary : c, goal_cases)
case 1 show ?case using se_star.simps by blast
next
case (2 l ls c)

then obtain c1 where "se c l c1" using finite_imp_ex_se_succ by blast

hence "finite (pred c1)"
and   "∀ e ∈ pred c1. finite (Bexp.vars e)"
using 2 se_preserves_finiteness1 se_preserves_finiteness2 by fastforce+

moreover
have "finite_labels ls" using 2 by simp

ultimately
obtain c2 where "se_star c1 ls c2" using 2 by blast

thus ?case using ‹se c l c1› using se_star_Cons by blast
qed

subsection ‹Feasibility of a sequence of labels›

text ‹A sequence of labels @{term "ls"} is said to be feasible from a configuration @{term "c"}
if there exists a satisfiable configuration @{term "c'"} obtained by symbolic execution of
@{term "ls"} from @{term "c"}.›

definition feasible :: "('v,'d) conf ⇒ ('v,'d) label list ⇒ bool" where
"feasible c ls ≡ (∃ c'. se_star c ls c' ∧ sat c')"

text ‹A simplification lemma for the case where @{term "ls"} is not empty.›

lemma feasible_Cons :
"feasible c (l#ls) = (∃ c'. se c l c' ∧ sat c' ∧ feasible c' ls)"
proof (intro iffI, goal_cases)
case 1 thus ?case
using se_star_sat_imp_sat by (simp add : feasible_def se_star_Cons) blast
next
case 2 thus ?case
unfolding feasible_def se_star_Cons by blast
qed

text ‹The following theorem is very important for the rest of this formalization. It states that,
given two
configurations @{term "c1"} and @{term "c2"} such that @{term "c1"} subsums @{term "c2"}, then
any feasible sequence of labels from @{term "c2"} is also feasible from @{term "c1"}. This is a crucial
point in order to prove that our approach preserves the set of feasible paths of the original LTS.
This proof requires a number of assumptions about the finiteness of the sequence of labels, of
the path predicates of the two configurations and of their states of variables.
Those assumptions are needed in order to show that there exist successors of
both configurations by symbolic execution of the sequence of labels.›

lemma subsums_imp_feasible :
assumes "finite_labels ls"
assumes "finite (pred c1)"
assumes "finite (pred c2)"
assumes "∀ e ∈ pred c1. finite (Bexp.vars e)"
assumes "∀ e ∈ pred c2. finite (Bexp.vars e)"
assumes "c2 ⊑ c1"
assumes "feasible c2 ls"
shows   "feasible c1 ls"
using assms
proof (induct ls arbitrary : c1 c2)
case Nil thus ?case by (simp add : feasible_def sat_sub_by_sat)
next
case (Cons l ls c1 c2)

then obtain c2' where "se c2 l c2'"
and   "sat c2'"
and   "feasible c2' ls"
using feasible_Cons by blast

obtain c1' where "se c1 l c1'"
using finite_conj[OF Cons(3,5)]
finite_pred_imp_se_updatable
updatable_imp_ex_se_suc
by blast

moreover
hence "sat c1'"
using  se_mono_for_sub[OF _ ‹se c2 l c2'› Cons(7)]
sat_sub_by_sat[OF ‹sat c2'›]
by fast

moreover
have "feasible c1' ls"
proof -

have "finite_label  l"
and  "finite_labels ls" using Cons(2) by simp_all

have "finite (pred c1')"
by (rule se_preserves_finiteness2[OF ‹se c1 l c1'› Cons(3)])

moreover
have "finite (pred c2')"
by (rule se_preserves_finiteness2[OF ‹se c2 l c2'› Cons(4)])

moreover
have "∀e∈pred c1'. finite (Bexp.vars e)"
by (rule se_preserves_finiteness1[OF ‹finite_label l› ‹se c1 l c1'› Cons(5)])

moreover
have "∀e∈pred c2'. finite (Bexp.vars e)"
by (rule se_preserves_finiteness1[OF ‹finite_label l› ‹se c2 l c2'› Cons(6)])

moreover
have "c2' ⊑ c1'"
by (rule se_mono_for_sub[OF ‹se c1 l c1'› ‹se c2 l c2'› Cons(7)])

ultimately
show ?thesis using Cons(1) ‹feasible c2' ls› ‹finite_labels ls› by fast
qed

ultimately
show ?case by (auto simp add : feasible_Cons)
qed

subsection ‹Concrete execution›

text ‹We illustrate our notion of symbolic execution by relating it with @{term ce}, an inductive
predicate describing concrete execution. Unlike symbolic execution, concrete execution describes
program behavior given program states, i.e.\ concrete valuations for program variables. The
goal of this section is to show that our notion of symbolic execution is correct, that is: given two
configurations such that one results from the symbolic execution of a sequence of labels from the
other, then the resulting configuration represents the set of states that are reachable by
concrete execution from the states of the original configuration.›

inductive ce ::
"('v,'d) state ⇒ ('v,'d) label ⇒ ('v,'d) state ⇒ bool"
where
"ce σ Skip σ"
| "e σ ⟹ ce σ (Assume e) σ"
| "ce σ (Assign v e) (σ(v := e σ))"

inductive ce_star :: "('v,'d) state ⇒ ('v,'d) label list ⇒ ('v,'d) state ⇒ bool" where
"ce_star c [] c"
| "ce c1 l c2 ⟹ ce_star c2 ls c3 ⟹ ce_star c1 (l # ls) c3"

lemma [simp] :
"ce σ Skip σ' = (σ' = σ)"
by (auto simp add : ce.simps)

lemma [simp] :
"ce σ (Assume e) σ' = (σ' = σ ∧ e σ)"
by (auto simp add : ce.simps)

lemma [simp] :
"ce σ (Assign v e) σ' = (σ' = σ(v := e σ))"
by (auto simp add : ce.simps)

lemma se_as_ce :
assumes "se c l c'"
shows   "states c' = {σ'. ∃ σ ∈ states c. ce σ l σ'} "
using assms
by (cases l)

lemma [simp] :
"ce_star σ [] σ' = (σ' = σ)"
by (subst ce_star.simps) simp

lemma ce_star_Cons :
"ce_star σ1 (l # ls) σ2 = (∃ σ. ce σ1 l σ ∧ ce_star σ ls σ2)"
by (subst (1) ce_star.simps) blast

lemma se_star_as_ce_star :
assumes "se_star c ls c'"
shows   "states c' = {σ'. ∃ σ ∈ states c. ce_star σ ls σ'}"
using assms
proof (induct ls arbitrary : c)
case Nil thus ?case by simp
next
case (Cons l ls c)

then obtain c'' where "se c l c''"
and   "se_star c'' ls c'"
using se_star_Cons by blast

show ?case
unfolding set_eq_iff Bex_def mem_Collect_eq
proof (intro allI iffI, goal_cases)
case (1 σ')

then obtain σ'' where "σ'' ∈ states c''"
and   "ce_star σ'' ls σ'"
using Cons(1) ‹se_star c'' ls c'› by blast

moreover
then obtain σ where "σ ∈ states c"
and   "ce σ l σ''"
using ‹se c l c''›  se_as_ce by blast

ultimately
show ?case by (simp add: ce_star_Cons) blast
next
case (2 σ')

then obtain σ where "σ ∈ states c"
and   "ce_star σ (l#ls) σ'"
by blast

moreover
then obtain σ'' where "ce σ l σ''"
and   "ce_star σ'' ls σ'"
using ce_star_Cons by blast

ultimately
show ?case
using Cons(1) ‹se_star c'' ls c'› ‹se c l c''› by (auto simp add : se_as_ce)
qed
qed

end


# Theory LTS

theory LTS
imports Graph Labels SymExec
begin

section‹Labelled Transition Systems›

text‹This theory is motivated by the need of an  abstract representation of control-flow graphs
(CFG). It is a refinement of the prior theory of (unlabelled) graphs and proceeds by decorating
their edges with \emph{labels} expressing assumptions and effects (assignments) on an underlying
state. In this theory, we define LTSs and introduce a number of abbreviations that will ease
stating and proving lemmas in the following theories.›

subsection‹Basic definitions›

text‹The labelled transition systems (LTS) we are heading for are constructed by
extending  ‹rgraph›'s by a labelling function of the edges, using Isabelle extensible
records.›

record ('vert,'var,'d) lts = "'vert rgraph" +
labelling :: "'vert edge ⇒ ('var,'d) label"

text ‹We call \emph{initial location} the root of the underlying graph.›

abbreviation init ::
"('vert,'var,'d,'x) lts_scheme ⇒ 'vert"
where
"init lts ≡ root lts"

text ‹The set of labels of a LTS is the image set of its labelling function over its set of edges.
›

abbreviation labels ::
"('vert,'var,'d,'x) lts_scheme ⇒ ('var,'d) label set"
where
"labels lts ≡ labelling lts  edges lts"

text ‹In the following, we will sometimes need to use the notion of \emph{trace} of
a given sequence of edges with respect to the transition relation of an LTS.›

abbreviation trace ::
"'vert edge list ⇒ ('vert edge ⇒ ('var,'d) label) ⇒ ('var,'d) label list"
where
"trace as L ≡ map L as"

text‹We are interested in a special form of Labelled Transition Systems; the prior
record definition is too liberal. We will constrain it to \emph{well-formed labelled transition
systems}.›

text ‹We first define an application that, given an LTS, returns its underlying graph.›

abbreviation graph ::
"('vert,'var,'d,'x) lts_scheme ⇒ 'vert rgraph"
where
"graph lts ≡ rgraph.truncate lts"

text‹An LTS is well-formed if its underlying ‹rgraph› is well-formed.›

abbreviation wf_lts ::
"('vert,'var,'d,'x) lts_scheme ⇒ bool"
where
"wf_lts lts ≡ wf_rgraph (graph lts)"

text ‹In the following theories, we will sometimes need to account for the fact that we consider
LTSs with a finite number of edges.›

abbreviation finite_lts ::
"('vert,'var,'d,'x) lts_scheme ⇒ bool"
where
"finite_lts lts ≡ ∀ l ∈ range (labelling lts). finite_label l"

subsection ‹Feasible sub-paths and paths›

text ‹A sequence of edges is a feasible sub-path of an LTS ‹lts› from a configuration
‹c› if it is a sub-path of the underlying graph of ‹lts› and if it is feasible
from the configuration ‹c›.›

abbreviation feasible_subpath ::
"('vert,'var,'d,'x) lts_scheme ⇒ ('var,'d) conf ⇒ 'vert ⇒ 'vert edge list ⇒ 'vert ⇒ bool"
where
"feasible_subpath lts pc l1 as l2 ≡ Graph.subpath lts l1 as l2
∧ feasible pc (trace as (labelling lts))"

text ‹Similarly to sub-paths in rooted-graphs, we will not be always interested in the final
vertex of a feasible sub-path. We use the following notion when we are not interested in this
vertex.›

abbreviation feasible_subpath_from ::
"('vert,'var,'d,'x) lts_scheme ⇒ ('var,'d) conf ⇒ 'vert ⇒ 'vert edge list ⇒ bool"
where
"feasible_subpath_from lts pc l as ≡ ∃ l'. feasible_subpath lts pc l as l'"

abbreviation feasible_subpaths_from ::
"('vert,'var,'d,'x) lts_scheme ⇒ ('var,'d) conf ⇒ 'vert ⇒ 'vert edge list set"
where
"feasible_subpaths_from lts pc l ≡ {ts. feasible_subpath_from lts pc l ts}"

text ‹As earlier, feasible paths are defined as feasible sub-paths starting at the initial
location of the LTS.›

abbreviation feasible_path ::
"('vert,'var,'d,'x) lts_scheme ⇒ ('var,'d) conf ⇒ 'vert edge list ⇒ 'vert ⇒ bool"
where
"feasible_path lts pc as l ≡ feasible_subpath lts pc (init lts) as l"

abbreviation feasible_paths ::
"('vert,'var,'d,'x) lts_scheme ⇒ ('var,'d) conf ⇒ 'vert edge list set"
where
"feasible_paths lts pc ≡ {as. ∃ l. feasible_path lts pc as l}"

end


# 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)

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


# Theory ArcExt

theory ArcExt
imports SubRel
begin

section ‹Extending rooted graphs with edges›

text ‹In this section, we formalize the operation of adding to a rooted graph an edge whose source
is already a vertex of the given graph but not its target. We call this operation an extension of the given graph by adding
an edge. This corresponds to an abstraction of
the act of adding an edge to the red part of a red\hyp{}black graph as a result of symbolic execution
of the corresponding transition in the LTS under analysis, where all details about symbolic
execution would have been abstracted.  We then state and prove a number of facts
describing the evolution of the set of paths of the given graph, first without considering
subsumption links then in the case of rooted graph equipped with a subsumption relation.›

subsection ‹Definition and Basic properties›

text ‹Extending a rooted graph with an edge consists in adding to its set of edges an edge whose
source is a vertex of this graph but whose target is not.›

abbreviation extends ::
"('v,'x) rgraph_scheme ⇒ 'v edge ⇒ ('v,'x) rgraph_scheme ⇒ bool"
where
"extends g e g' ≡ src e ∈ Graph.vertices g
∧ tgt e ∉ Graph.vertices g
∧ g' = (add_edge g e)"

text ‹After such an extension, the set of out-edges of the target of the new edge is empty.›

lemma extends_tgt_out_edges :
assumes "extends g e g'"
shows   "out_edges g' (tgt e) = {}"
using assms unfolding vertices_def image_def by force

text ‹Consider a graph equipped with a sub-relation. This relation is also a sub-relation of any
extension of this graph.›

lemma (in sub_rel_of)
assumes "extends g e g'"
shows   "sub_rel_of g' subs"
using assms sub_rel_of by (auto simp add : sub_rel_of_def vertices_def)

text ‹Extending a graph with an edge preserves the existing sub-paths.›

lemma sp_in_extends :
assumes "extends g e g'"
assumes "Graph.subpath g  v1 es v2"
shows   "Graph.subpath g' v1 es v2"
using assms by (auto simp add : Graph.subpath_def vertices_def)

subsection ‹Extending trees›

text ‹We show that extending a rooted graph that is already a tree yields a new tree. Since
the empty rooted graph is a tree, all graphs produced using only the extension by edge are trees.›

lemma extends_is_tree :
assumes "is_tree g"
assumes "extends g e g'"
shows   "is_tree g'"
unfolding is_tree_def Ball_def
proof (intro allI impI)
fix v

have "root g' = root g" using assms(2) by simp

assume "v ∈ Graph.vertices g'"

hence "v ∈ Graph.vertices g ∨ v = tgt e"
using assms(2) by (auto simp add : vertices_def)

thus "∃!es. path g' es v"
proof (elim disjE, goal_cases)
case 1

then obtain es
where "Graph.path g es v"
and   "∀ es'. Graph.path g es' v ⟶ es' = es"
using assms(1) unfolding Ex1_def is_tree_def by blast

hence "Graph.path g' es v"
using assms(2) sp_in_extends[OF assms(2)]
by (subst ‹root g' = root g›)

moreover
have "∀ es'. Graph.path g' es' v ⟶ es' =  es"
proof (intro allI impI)
fix es'

assume "Graph.path g' es' v"

thus "es' = es"
proof (case_tac "e ∈ set es'", goal_cases)
case 1

then obtain es''
where "es' = es'' @ [e]"
and   "e ∉ set es''"
using ‹Graph.path g' es' v›
Graph.sp_through_de_decomp[OF extends_tgt_out_edges[OF assms(2)]]
by blast

hence "v = tgt e"
using ‹Graph.path g' es' v›

thus ?thesis
using assms(2)
Graph.lst_of_sp_is_vert[OF ‹Graph.path g es v›]
by simp
next
case 2 thus ?thesis
using assms
‹∀ es'. Graph.path g es' v ⟶ es' = es› ‹Graph.path g' es' v›
by (auto simp add : Graph.subpath_def vertices_def)
qed
qed

ultimately
show ?thesis by auto

next
case 2

then obtain es
where "Graph.path g es (src e)"
and   "∀ es'. Graph.path g es' (src e) ⟶ es' = es"
using assms(1,2) unfolding is_tree_def by blast

hence "Graph.path g' es (src e)"
using sp_in_extends[OF assms(2)]
by (subst ‹root g' = root g›)

hence "Graph.path g' (es @ [e]) (tgt e)"
using assms(2) by (auto simp add : Graph.sp_append_one)

moreover
have "∀ es'. Graph.path g' es' (tgt e) ⟶ es' = es @ [e]"
proof (intro allI impI)
fix es'

assume "Graph.path g' es' (tgt e)"

moreover
hence "e ∈ set es'"
using assms
sp_ends_in_tgt_imp_mem[of e g "root g" es']
by (auto simp add : Graph.subpath_def vertices_def)

moreover
have   "out_edges g' (tgt e) = {}"
using assms
by (intro extends_tgt_out_edges)

ultimately
have "∃ es''. es' = es'' @ [e] ∧ e ∉ set es''"
by (elim Graph.sp_through_de_decomp)

then obtain es''
where "es' = es'' @ [e]"
and   "e ∉ set es''"
by blast

hence "Graph.path g' es'' (src e)"
using ‹Graph.path g' es'  (tgt e)›
by (auto simp add : Graph.sp_append_one)

hence "Graph.path g es'' (src e)"
using assms(2) ‹e ∉ set es''›
by (auto simp add : Graph.subpath_def vertices_def)

hence "es'' = es"
using ‹∀ as'. Graph.path g as' (src e) ⟶ as' = es›
by simp

thus "es' = es @ [e]" using ‹es' = es'' @ [e]› by simp
qed

ultimately
show ?thesis using 2 by auto
qed
qed

subsection ‹Properties of sub-paths in an extension›

text ‹Extending a graph by an edge preserves the existing sub-paths.›

lemma sp_in_extends_w_subs :
assumes "extends g a g'"
assumes "subpath g  v1 es v2 subs"
shows   "subpath g' v1 es v2 subs"
using assms by (auto simp add : subpath_def sub_rel_of_def vertices_def)

text ‹In an extension, the target of the new edge has no out-edges. Thus sub-paths of the
extension starting and ending in old vertices are sub-paths of the graph prior to its extension.›

lemma (in sub_rel_of) sp_from_old_verts_imp_sp_in_old :
assumes "extends g e g'"
assumes "v1 ∈ Graph.vertices g"
assumes "v2 ∈ Graph.vertices g"
assumes "subpath g' v1 es v2 subs"
shows   "subpath g  v1 es v2 subs"
proof -
have "e ∉ set es"
proof (intro notI)
assume "e ∈ set es"

have "v2 = tgt e"
proof -
have "tgt e ∉ subsumees subs" using sub_rel_of assms(1) by fast

moreover
have  "out_edges g' (tgt e) = {}" using assms(1) by (rule extends_tgt_out_edges)

ultimately
have "∃ es'. es = es' @ [e] ∧ e ∉ set es'"
using  assms(4) ‹e ∈ set es›
by (intro sp_through_de_decomp)

then obtain es' where "es = es' @ [e]" "e ∉ set es'" by blast

hence "tgt e = v2 ∨ (tgt e,v2) ∈ subs⇧+"
using assms(4) by (simp add : sp_append_one)

thus ?thesis using ‹tgt e ∉ subsumees subs› tranclD[of "tgt e" v2 subs] by force
qed

thus False using assms(1,3) by simp
qed

thus ?thesis
using sub_rel_of assms
unfolding subpath_def sub_rel_of_def by auto
qed

text ‹For the same reason, sub-paths starting at the target of the new edge are empty.›

lemma (in sub_rel_of) sp_from_tgt_in_extends_is_Nil :
assumes "extends g e g'"
assumes "subpath g' (tgt e) es v subs"
shows   "es = []"
using sub_rel_of assms
extends_tgt_out_edges
sp_from_de_empty[of "tgt e" subs g' es v]
by fast

text ‹Moreover, a sub-path @{term es} starting in another vertex than the target of the new edge
@{term e} but ending in this target has @{term e} as last element. This occurrence of @{term e} is
unique among @{term es}. The prefix of @{term es} preceding @{term e} is a sub-path leading at the
source of @{term e} in the original graph.›

lemma (in sub_rel_of) sp_to_new_edge_tgt_imp :
assumes "extends g e g'"
assumes "subpath g' v es (tgt e) subs"
assumes "v ≠ tgt e"
shows   "∃ es'. es = es' @ [e] ∧ e ∉ set es' ∧ subpath g v es' (src e) subs"
proof -
obtain es' where "es = es' @ [e]" and "e ∉ set es'"
using sub_rel_of assms(1,2,3)
extends_tgt_out_edges[OF assms(1)]
sp_through_de_decomp[of e subs g' v es "tgt e"]
sp_ends_in_tgt_imp_mem[of e v es]
by blast

moreover
have "subpath g v es' (src e) subs"
proof -
have "v ∈ Graph.vertices g"
using assms(1,3) fst_of_sp_is_vert[OF assms(2)]
by (auto simp add : vertices_def)

moreover
have "SubRel.subpath g' v es' (src e) subs"
using assms(2) ‹es = es' @ [e]› by (simp add : sp_append_one)

ultimately
show ?thesis
using assms(1) sub_rel_of ‹e ∉ set es'›
unfolding subpath_def by (auto simp add : sub_rel_of_def)
qed

ultimately
show ?thesis by blast
qed

end


# 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)]

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

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


# Theory RB

theory RB
imports LTS ArcExt SubExt
begin

section ‹Red-Black Graphs›

text ‹In this section we define red\hyp{}black graphs and the five operators that perform over
them. Then, we state and prove a number of intermediate lemmas about red\hyp{}black graphs
built using only these five operators, in other words: invariants about our method of transformation
of red\hyp{}black graphs.

Then, we define the notion of red\hyp{}black paths and state and prove the main properties of our
method, namely its correctness and the fact that it preserves the set of feasible paths of the
program under analysis.›

subsection ‹Basic Definitions›

subsubsection ‹The type of Red-Black Graphs›

text ‹We represent red-black graph with the following record. We detail its fields:
\begin{itemize}
\item @{term "red"} is the red graph, called \emph{red part}, which represents the unfolding of
the black part. Its vertices are indexed black vertices,
\item @{term "black"} is the original LTS, the \emph{black part},
\item @{term "subs"} is the subsumption relation over the vertices of @{term "red"},
\item @{term "init_conf"} is the initial configuration,
\item @{term "confs"} is a function associating configurations to the vertices of @{term "red"},
\item @{term "marked"} is a function associating truth values to the vertices of @{term "red"}.
We use it to represent the fact that a particular configuration (associated to a red location) is
known to be unsatisfiable,
\item @{term "strengthenings"} is a function associating boolean expressions over program
variables to vertices of the red graph. Those boolean expressions can be seen as invariants that
the configuration associated to the strengthened'' red vertex has to model.
\end{itemize}

We are only interested by red-black graphs obtained by the inductive relation
@{term "RedBlack"}. From now on, we call red-black graphs" the @{term pre_RedBlack}'s
obtained by @{term "RedBlack"} and pre-red-black graphs" all other ones.›

record ('vert,'var,'d) pre_RedBlack =
red            :: "('vert × nat) rgraph"
black          :: "('vert,'var,'d) lts"
subs           :: "'vert sub_rel_t"
init_conf      :: "('var,'d) conf"
confs          :: "('vert × nat) ⇒ ('var,'d) conf"
marked         :: "('vert × nat) ⇒ bool"
strengthenings :: "('vert × nat) ⇒ ('var,'d) bexp"

text‹We call \emph{red vertices} the set of vertices of the red graph.›

abbreviation red_vertices ::
"('vert,'var,'d,'x) pre_RedBlack_scheme ⇒ ('vert × nat) set"
where
"red_vertices lts ≡ Graph.vertices (red lts)"

text‹@{term "ui_edge"} is the operation of unindexing'' the ends of a red edge, thus giving the
corresponding black edge.›

abbreviation ui_edge ::
"('vert × nat) edge ⇒ 'vert edge"
where
"ui_edge e ≡ ⦇ src = fst (src e), tgt = fst (tgt e) ⦈"

text ‹We extend this idea to sequences of edges.›

abbreviation ui_es ::
"('vert × nat) edge list ⇒ 'vert edge list"
where
"ui_es es ≡ map ui_edge es"

subsubsection ‹Well-formed and finite red-black graphs›

locale pre_RedBlack =
fixes prb :: "('vert,'var,'d) pre_RedBlack" (structure)

text ‹A pre-red-black graph is well-formed if :
\begin{itemize}
\item its red and black parts are well-formed,
\item the root of its red part is an indexed version of the root of its black part,
\item all red edges are indexed versions of black edges.
\end{itemize}›

locale wf_pre_RedBlack = pre_RedBlack +
assumes red_wf           : "wf_rgraph (red prb)"
assumes black_wf         : "wf_lts (black prb)"
assumes consistent_roots : "fst (root (red prb)) = root (black prb)"
assumes ui_re_are_be     : "e ∈ edges (red prb) ⟹ ui_edge e ∈ edges (black prb)"
begin
lemmas wf_pre_RedBlack = red_wf black_wf consistent_roots ui_re_are_be
end

text‹We say that a pre-red-black graph is finite if :
\begin{itemize}
\item the path predicate of its initial configuration contains a finite number of constraints,
\item each of these constraints contains a finite number of variables,
\item its black part is finite (cf. definition of @{term "finite_lts"}.).
\end{itemize}›

locale finite_RedBlack = pre_RedBlack +
assumes finite_init_pred         : "finite (pred (init_conf prb))"
assumes finite_init_pred_symvars : "∀ e ∈ pred (init_conf prb). finite (Bexp.vars e)"
assumes finite_lts               : "finite_lts (black prb)"
begin
lemmas finite_RedBlack = finite_init_pred finite_init_pred_symvars finite_lts
end

subsection ‹Extensions of Red-Black Graphs›

text ‹We now define the five basic operations that can be performed over red-black graphs. Since
we do not want to model the heuristics part of our prototype, a number of conditions must be met
for each operator to apply. For example, in our prototype abstractions are performed at nodes that
actually have successors, and these abstractions must be propagated to these successors in order to
keep the symbolic execution graph consistent. Propagation is a complex task, and it is hard to model
in Isabelle/HOL. This is partially due to the fact that we model the red part as a graph, in which
propagation might not terminate. Instead, we suppose that abstraction must be performed only at
leaves of the red part. This is equivalent to implicitly assume the existence of an oracle that
would tell that we will need to abstract some red vertex and how to abstract it, as soon as this red
vertex is added to the red part.›

text ‹As in the previous theories, we use predicates instead of functions to model these
transformations to ease writing and reading definitions, proofs, etc.›

subsubsection ‹Extension by symbolic execution›

text‹The core abstract operation of symbolic execution: take a black edge and
turn it red, by symbolic execution of its label. In the following abbreviation, @{term re} is the
red edge obtained from the (hypothetical) black edge @{term e} that we want to symbolically execute
and @{term c} the configuration obtained by symbolic execution of the label of @{term e}. Note that
this extension could have been defined as a
predicate that takes only two @{term pre_RedBlack}s and evaluates to \emph{true} if and only if
the second has been obtained by adding a red edge as a result of symbolic execution. However,
making the red edge and the configuration explicit allows for lighter definitions, lemmas and proofs
in the following.›

abbreviation se_extends ::
"('vert,'var,'d) pre_RedBlack
⇒ ('vert × nat) edge
⇒ ('var,'d) conf
⇒ ('vert,'var,'d) pre_RedBlack ⇒ bool"
where
"se_extends prb re c prb' ≡
ui_edge re ∈ edges (black prb)
∧ ArcExt.extends (red prb) re (red prb')
∧ src re ∉ subsumees (subs prb)
∧ se  (confs prb (src re)) (labelling (black prb) (ui_edge re)) c
∧ prb' = ⦇ red       = red prb',
black     = black prb,
subs      = subs prb,
init_conf = init_conf prb,
confs     = (confs prb) (tgt re := c),
marked    = (marked prb)(tgt re := marked prb (src re)),
strengthenings = strengthenings prb ⦈"

text ‹Hiding the new red edge (using an existential quantifier) and the new configuration makes
the following abbreviation more
intuitive. However, this would require using \verb?obtain? or \verb?let ... = ... in ...? constructs
in the following lemmas and proofs, making them harder to read and write.›

abbreviation se_extends2 ::
"('vert,'var,'d) pre_RedBlack ⇒ ('vert,'var,'d) pre_RedBlack ⇒ bool"
where
"se_extends2 prb prb' ≡
∃ re ∈ edges (red prb').
ui_edge re ∈ edges (black prb)
∧ ArcExt.extends (red prb) re (red prb')
∧ src re ∉ subsumees (subs prb)
∧ se (confs prb (src re)) (labelling (black prb) (ui_edge re)) (confs prb' (tgt re))
∧ black prb' = black prb
∧ subs prb'  = subs prb
∧ init_conf prb' = init_conf prb
∧ confs prb' = (confs prb) (tgt re := confs prb' (tgt re))
∧ marked prb' = (marked prb)(tgt re := marked prb (src re))
∧ strengthenings prb' = strengthenings prb"

subsubsection ‹Extension by marking›

text‹The abstract operation of mark-as-unsat. It manages the information
- provided, for example, by an external automated prover -, that the
configuration of the red vertex @{term rv} has been proved unsatisfiable.›

abbreviation mark_extends ::
"('vert,'var,'d) pre_RedBlack ⇒ ('vert × nat) ⇒ ('vert,'var,'d) pre_RedBlack ⇒ bool"
where
"mark_extends prb rv prb' ≡
rv ∈ red_vertices prb
∧ out_edges (red prb) rv = {}
∧ rv ∉ subsumees (subs prb)
∧ rv ∉ subsumers (subs prb)
∧ ¬ sat (confs prb rv)
∧ prb' = ⦇ red       = red prb,
black     = black prb,
subs      = subs prb,
init_conf = init_conf prb,
confs     = confs prb,
marked    = (λ rv'. if rv' = rv then True else marked prb rv'),
strengthenings = strengthenings prb,
…        = more prb ⦈ "

subsubsection ‹Extension by subsumption›

text‹The abstract operation of introducing a subsumption link.›

abbreviation subsum_extends ::
"('vert,'var,'d) pre_RedBlack ⇒ 'vert sub_t ⇒ ('vert,'var,'d) pre_RedBlack ⇒ bool"
where
"subsum_extends prb sub prb' ≡
SubExt.extends (red prb) (subs prb) sub (subs prb')
∧ ¬ marked prb (subsumer sub)
∧ ¬ marked prb (subsumee sub)
∧ confs prb (subsumee sub) ⊑ confs prb (subsumer sub)
∧ prb' = ⦇ red       = red prb,
black     = black prb,
subs      = insert sub (subs prb),
init_conf = init_conf prb,
confs     = confs prb,
marked    = marked prb,
strengthenings = strengthenings prb,
…        = more prb ⦈"

subsubsection ‹Extension by abstraction›

text‹This operation replaces the configuration of a red vertex @{term rv} by an abstraction of
this configuration. The way the abstraction is computed is not specified. However, besides a number
of side conditions, it must subsume the former configuration of @{term rv} and must entail its
safeguard condition, if any.›

abbreviation abstract_extends ::
"('vert,'var,'d) pre_RedBlack
⇒ ('vert × nat)
⇒ ('var,'d) conf
⇒ ('vert,'var,'d) pre_RedBlack
⇒ bool"
where
"abstract_extends prb rv c⇩a prb' ≡
rv ∈ red_vertices prb
∧ ¬ marked prb rv
∧ out_edges (red prb) rv = {}
∧ rv ∉ subsumees (subs prb)
∧ abstract (confs prb rv) c⇩a
∧ c⇩a ⊨⇩c (strengthenings prb rv)
∧ finite (pred c⇩a)
∧ (∀ e ∈ pred c⇩a. finite (vars e))
∧ prb' =  ⦇ red       = red prb,
black     = black prb,
subs      = subs prb,
init_conf = init_conf prb,
confs     = (confs prb)(rv := c⇩a),
marked    = marked prb,
strengthenings = strengthenings prb,
…        = more prb ⦈"

subsubsection ‹Extension by strengthening›

text ‹This operation consists in labeling a red vertex with a safeguard condition. It does not
actually change the red part, but model the mechanism of preventing too crude abstractions.›

abbreviation strengthen_extends ::
"('vert,'var,'d) pre_RedBlack
⇒ ('vert × nat)
⇒ ('var,'d) bexp
⇒ ('vert,'var,'d) pre_RedBlack
⇒ bool"
where
"strengthen_extends prb rv e prb' ≡
rv ∈ red_vertices prb
∧ rv ∉ subsumees (subs prb)
∧ confs prb rv ⊨⇩c e
∧ prb' =  ⦇ red       = red prb,
black     = black prb,
subs      = subs prb,
init_conf = init_conf prb,
confs     = confs prb,
marked    = marked prb,
strengthenings = (strengthenings prb)(rv := (λ σ. (strengthenings prb rv) σ ∧ e σ)),
…        = more prb ⦈"

subsection ‹Building Red-Black Graphs using Extensions›

text‹Red-black graphs are pre-red-black graphs built with the following inductive relation, i.e.\
using only the five previous pre-red-black graphs transformation operators, starting from an
empty red part.›

inductive RedBlack ::
"('vert,'var,'d) pre_RedBlack ⇒ bool"
where
base :
"fst (root (red prb)) = init (black prb)      ⟹
edges (red prb) = {}                         ⟹
subs prb = {}                                ⟹
(confs prb) (root (red prb)) = init_conf prb ⟹
marked prb = (λ rv. False)                   ⟹
strengthenings prb = (λ rv. (λ σ. True))     ⟹ RedBlack prb"

| se_step :
"RedBlack prb                                 ⟹
se_extends prb re p' prb'                    ⟹ RedBlack prb'"

| mark_step :
"RedBlack prb                                 ⟹
mark_extends prb rv prb'                     ⟹ RedBlack prb'"

| subsum_step :
"RedBlack prb                                 ⟹
subsum_extends prb sub prb'                  ⟹ RedBlack prb'"

| abstract_step :
"RedBlack prb                                 ⟹
abstract_extends prb rv c⇩a prb'             ⟹ RedBlack prb'"

| strengthen_step :
"RedBlack prb                                 ⟹
strengthen_extends prb rv e prb'             ⟹ RedBlack prb'"

subsection ‹Properties of Red-Black-Graphs›

subsubsection‹Invariants of the Red\hyp{}Black Graphs›

text‹The red part of a red-black graph is loop free.›

lemma
assumes "RedBlack prb"
shows   "loop_free (red prb)"
using assms by (induct prb) auto

text‹A red edge can not lead to the (red) root.›

lemma
assumes "RedBlack prb"
assumes "re ∈ edges (red prb)"
shows   "tgt re ≠ root (red prb)"
using assms by (induct prb) (auto simp add : vertices_def)

text‹Red edges are specific versions of black edges.›

lemma ui_re_is_be :
assumes "RedBlack prb"
assumes "re ∈ edges (red prb)"
shows   "ui_edge re ∈ edges (black prb)"
using assms by (induct rule : RedBlack.induct) auto

text‹The set of out-going edges from a red vertex is a subset of the set of out-going edges from
the black location it represents.›

lemma red_OA_subset_black_OA :
assumes "RedBlack prb"
shows   "ui_edge  out_edges (red prb) rv ⊆ out_edges (black prb) (fst rv)"
using assms by (induct prb) (fastforce simp add : vertices_def)+

text ‹The red root is an indexed version of the black initial location.›

lemma consistent_roots :
assumes "RedBlack prb"
shows   "fst (root (red prb)) = init (black prb)"
using assms by (induct prb) auto

text‹The red part of a red-black graph is a tree.›

lemma
assumes "RedBlack prb"
shows   "is_tree (red prb)"
using assms
by (induct prb) (auto simp add : empty_graph_is_tree ArcExt.extends_is_tree)

text ‹A red-black graph whose black part is well-formed is also well-formed.›

lemma
assumes "RedBlack prb"
assumes "wf_lts (black prb)"
shows   "wf_pre_RedBlack prb"
proof -
have "wf_rgraph (red prb)"
using assms by (induct prb) (force simp add : vertices_def)+

thus ?thesis
using assms consistent_roots ui_re_is_be
by (auto simp add : wf_pre_RedBlack_def)
qed

text ‹Red locations of a red-black graph are indexed versions of its black locations.›

lemma ui_rv_is_bv :
assumes "RedBlack prb"
assumes "rv ∈ red_vertices prb"
shows   "fst rv ∈ Graph.vertices (black prb)"
using assms consistent_roots ui_re_is_be
by (auto simp add : vertices_def image_def Bex_def) fastforce+

text ‹The subsumption of a red-black graph is a sub-relation of its red part.›

lemma subs_sub_rel_of :
assumes "RedBlack prb"
shows   "sub_rel_of (red prb) (subs prb)"
using assms unfolding sub_rel_of_def
proof (induct prb)
case base thus ?case by simp
next
case se_step thus ?case by (elim conjE) (auto simp add : vertices_def)
next
case mark_step thus ?case by auto
next
case subsum_step thus ?case by auto
next
case abstract_step thus ?case by simp
next
case strengthen_step thus ?case by simp
qed

text‹The subsumption relation of red-black graph is well-formed.›

lemma subs_wf_sub_rel :
assumes "RedBlack prb"
shows   "wf_sub_rel (subs prb)"
using assms
proof (induct prb)
case base thus ?case by (simp add : wf_sub_rel_def)
next
case se_step thus ?case by force
next
case mark_step thus ?case by (auto simp add : wf_sub_rel_def)
next
case subsum_step thus ?case by (auto simp add : wf_sub_rel.extends_imp_wf_sub_rel)
next
case abstract_step thus ?case by simp
next
case strengthen_step thus ?case by simp
qed

text ‹Using the two previous lemmas, we have that the subsumption relation of a red-black graph
is a well-formed sub-relation of its red-part.›

lemma subs_wf_sub_rel_of :
assumes "RedBlack prb"
shows   "wf_sub_rel_of (red prb) (subs prb)"
using assms subs_sub_rel_of subs_wf_sub_rel by (simp add : wf_sub_rel_of_def) fast

text‹Subsumptions only involve red locations representing the same black location.›

lemma subs_to_same_BL :
assumes "RedBlack prb"
assumes "sub ∈ subs prb"
shows   "fst (subsumee sub) = fst (subsumer sub)"
using assms subs_wf_sub_rel unfolding wf_sub_rel_def by fast

text‹If a red edge sequence @{term "res"} is consistent between red locations @{term "rv1"} and
@{term "rv2"} with respect to the subsumption relation of a red-black graph, then its unindexed
version is consistent between the black locations represented by @{term "rv1"} and @{term "rv2"}.›

lemma rces_imp_bces :
assumes "RedBlack prb"
assumes "SubRel.ces rv1 res rv2 (subs prb)"
shows   "Graph.ces (fst rv1) (ui_es res) (fst rv2)"
using assms
proof (induct res arbitrary : rv1)
case (Nil rv1) thus ?case
using wf_sub_rel.in_trancl_imp[OF subs_wf_sub_rel] subs_to_same_BL
by fastforce
next
case (Cons re res rv1)

hence 1 : "rv1 = src re ∨ (rv1, src re) ∈ (subs prb)⇧+"
and   2 : "ces (tgt re) res rv2 (subs prb)" by simp_all

have "src (ui_edge re) = fst rv1"
using 1  wf_sub_rel.in_trancl_imp[OF subs_wf_sub_rel[OF assms(1)], of rv1 "src re"]
subs_to_same_BL[OF assms(1), of "(rv1,src re)"]
by auto

moreover
have "Graph.ces (tgt (ui_edge re)) (ui_es res) (fst rv2)"
using assms(1) Cons(1) 2 by simp

ultimately
show ?case by simp
qed

text‹The unindexed version of a subpath in the red part of a red-black graph is a subpath in its
black part. This is an important fact: in the end, it helps proving that set of paths we consider
in red-black graphs are paths of the original LTS. Thus, the same states are computed along
these paths.›

theorem red_sp_imp_black_sp :
assumes "RedBlack prb"
assumes "subpath (red prb) rv1 res rv2 (subs prb)"
shows   "Graph.subpath (black prb) (fst rv1) (ui_es res) (fst rv2)"
using assms rces_imp_bces ui_rv_is_bv ui_re_is_be
unfolding subpath_def Graph.subpath_def by (intro conjI) (fast, fast, fastforce)

text‹Any constraint in the path predicate of a configuration associated to a red location of a
red-black graph contains a finite number of variables.›

lemma finite_pred_constr_symvars :
assumes "RedBlack prb"
assumes "finite_RedBlack prb"
assumes "rv ∈ red_vertices prb"
shows   "∀ e ∈ pred (confs prb rv). finite (Bexp.vars e)"
using assms
proof (induct prb arbitrary : rv)
case base thus ?case by (simp add : vertices_def finite_RedBlack_def)
next
case (se_step prb re c' prb')

hence "rv ∈ red_vertices prb ∨ rv = tgt re" by (auto simp add : vertices_def)

thus ?case
proof (elim disjE)
assume "rv ∈ red_vertices prb"

moreover
have "finite_RedBlack prb"
using se_step(3,4) by (auto simp add : finite_RedBlack_def)

ultimately
show ?thesis
using se_step(2,3) by (elim conjE) (auto simp add : vertices_def)
next
assume "rv = tgt re"

moreover
have "finite_label (labelling (black prb) (ui_edge re))"
using se_step by (auto simp add : finite_RedBlack_def)

moreover
have "∀ e ∈ pred (confs prb (src re)). finite (Bexp.vars e)"
using se_step se_step(2)[of "src re"] unfolding finite_RedBlack_def
by (elim conjE) auto

moreover
have "se (confs prb (src re)) (labelling (black prb) (ui_edge re)) c'"
using se_step by auto

ultimately
show ?thesis using se_step se_preserves_finiteness1 by fastforce
qed
next
case mark_step thus ?case by (simp add : finite_RedBlack_def)
next
case subsum_step thus ?case by (simp add : finite_RedBlack_def)
next
case abstract_step thus ?case by (auto simp add : finite_RedBlack_def)
next
case strengthen_step thus ?case by (simp add : finite_RedBlack_def)
qed

text ‹The path predicate of a configuration associated to a red location of a
red-black graph contains a finite number of constraints.›

lemma finite_pred :
assumes "RedBlack prb"
assumes "finite_RedBlack prb"
assumes "rv ∈ red_vertices prb"
shows   "finite (pred (confs prb rv))"
using assms
proof (induct prb arbitrary : rv)
case base thus ?case by (simp add : vertices_def finite_RedBlack_def)
next
case (se_step prb re c' prb')

hence "rv ∈ red_vertices prb ∨ rv = tgt re"
by (auto simp add : vertices_def)

thus ?case
proof (elim disjE, goal_cases)
case 1 thus ?thesis
using se_step(2)[of rv] se_step(3,4)
by (auto simp add : finite_RedBlack_def)
next
case 2
moreover
hence "src re ∈ red_vertices prb"
and   "finite (pred (confs prb (src re)))"
using se_step(2)[of "src re"] se_step(3,4)
by (auto simp add : finite_RedBlack_def)

ultimately
show ?thesis
using se_step(3) se_preserves_finiteness2 by auto
qed
next
case mark_step thus ?case by (simp add : finite_RedBlack_def)
next
case subsum_step thus ?case by (simp add : finite_RedBlack_def)
next
case abstract_step thus ?case by (simp add : finite_RedBlack_def)
next
case strengthen_step thus ?case by (simp add : finite_RedBlack_def)
qed

text‹Hence, for a red location @{term "rv"} of a red-black graph and any label @{term "l"},
there exists a configuration that can be obtained by symbolic execution of @{term "l"} from the
configuration associated to @{term "rv"}.›

lemma (in finite_RedBlack) ex_se_succ :
assumes "RedBlack prb"
assumes "rv ∈ red_vertices prb"
shows   "∃ c'. se (confs prb rv) l c'"
using finite_RedBlack assms
finite_imp_ex_se_succ[of "confs prb rv"]
finite_pred[of prb rv ]
finite_pred_constr_symvars[of prb rv]
unfolding finite_RedBlack_def by fast

text‹Generalization of the previous lemma to a list of labels.›

lemma (in finite_RedBlack) ex_se_star_succ :
assumes "RedBlack prb"
assumes "rv ∈ red_vertices prb"
assumes "finite_labels ls"
shows   "∃ c'. se_star (confs prb rv) ls c'"
using finite_RedBlack assms
finite_imp_ex_se_star_succ[of "confs prb rv" ls]
finite_pred[OF assms(1), of rv]
finite_pred_constr_symvars[OF assms(1), of rv]
unfolding finite_RedBlack_def by simp

text‹Hence, for any red sub-path, there exists a configuration that can be obtained by symbolic
execution of its trace from the configuration associated to its source.›

lemma (in finite_RedBlack) sp_imp_ex_se_star_succ :
assumes "RedBlack prb"
assumes "subpath (red prb) rv1 res rv2 (subs prb)"
shows   "∃ c. se_star
(confs prb rv1)
(trace (ui_es res) (labelling (black prb)))
c"
using finite_RedBlack assms ex_se_star_succ
by (simp add : subpath_def finite_RedBlack_def)

text‹The configuration associated to a red location @{term "rl"} is update-able.›

lemma (in finite_RedBlack)
assumes "RedBlack prb"
assumes "rv ∈ red_vertices prb"
shows   "updatable (confs prb rv)"
using finite_RedBlack assms
finite_conj[OF finite_pred[OF assms(1)]
finite_pred_constr_symvars[OF assms(1)]]
finite_pred_imp_se_updatable
unfolding finite_RedBlack_def by fast

text‹The configuration associated to the first member of a subsumption is subsumed by the
configuration at its second member.›

lemma sub_subsumed :
assumes "RedBlack prb"
assumes "sub ∈ subs prb"
shows   "confs prb (subsumee sub) ⊑ confs prb (subsumer sub)"
using assms
proof (induct prb)
case base thus ?case by simp
next
case (se_step prb re c' prb')

moreover
hence "sub ∈ subs prb" by auto

hence "subsumee sub ∈ red_vertices prb"
and   "subsumer sub ∈ red_vertices prb"
using se_step(1) subs_sub_rel_of
unfolding sub_rel_of_def by fast+

moreover
have "tgt re ∉ red_vertices prb" using se_step by auto

ultimately
show ?case by auto
next
case mark_step thus ?case by simp
next
case (subsum_step prb sub prb') thus ?case by auto
next
case (abstract_step prb rv c⇩a prb')

hence "rv ≠ subsumee sub" by auto

show ?case
proof (case_tac "rv = subsumer sub")
assume "rv = subsumer sub"

moreover
hence  "confs prb (subsumer sub) ⊑ confs prb' (subsumer sub)"
using abstract_step abstract_def by auto

ultimately
show ?thesis
using abstract_step
subsums_trans[of "confs prb  (subsumee sub)"
"confs prb  (subsumer sub)"
"confs prb' (subsumer sub)"]
next
assume "rv ≠ subsumer sub" thus ?thesis using abstract_step ‹rv ≠ subsumee sub› by simp
qed
next
case strengthen_step thus ?case by simp
qed

subsubsection‹Simplification lemmas for sub-paths of the red part.›

lemma rb_Nil_sp :
assumes "RedBlack prb"
shows   "subpath (red prb) rv1 [] rv2 (subs prb) =
(rv1 ∈ red_vertices prb ∧ (rv1 = rv2 ∨ (rv1,rv2) ∈ (subs prb)))"
using assms subs_wf_sub_rel subs_sub_rel_of wf_sub_rel.Nil_sp by fast

lemma rb_sp_one :
assumes "RedBlack prb"
shows "subpath (red prb) rv1 [re] rv2 (subs prb) =
( sub_rel_of (red prb) (subs prb)
∧ (rv1 = src re ∨ (rv1, src re) ∈ (subs prb))
∧ re ∈ edges (red prb) ∧ (tgt re = rv2 ∨ (tgt re, rv2) ∈ (subs prb)))"
using assms subs_wf_sub_rel_of wf_sub_rel_of.sp_one by fast

lemma rb_sp_Cons :
assumes "RedBlack prb"
shows   "subpath (red prb) rv1 (re # res) rv2 (subs prb) =
( sub_rel_of (red prb) (subs prb)
∧ (rv1 = src re ∨ (rv1, src re) ∈ subs prb)
∧ re ∈ edges (red prb)
∧ subpath (red prb) (tgt re) res rv2 (subs prb))"
using assms subs_wf_sub_rel_of wf_sub_rel_of.sp_Cons by fast

lemma rb_sp_append_one :
assumes "RedBlack prb"
shows   "subpath (red prb) rv1 (res @ [re]) rv2 (subs prb) =
( subpath (red prb) rv1 res (src re) (subs prb)
∧ re ∈ edges (red prb)
∧ (tgt re = rv2 ∨ (tgt re, rv2) ∈ subs prb))"
using assms subs_wf_sub_rel wf_sub_rel.sp_append_one sp_append_one by fast

subsection ‹Relation between red-vertices›

text‹The following key-theorem describes the relation between two red locations that are linked by
a red sub-path. In a classical symbolic execution tree, the configuration at the end should be the
result of symbolic execution of the trace of the sub-path from the configuration at its source.
Here, due to the facts that abstractions might have occurred and that we consider sub-paths going
through subsumption links, the configuration at the end subsumes the configuration one would obtain
by symbolic execution of the trace. Note however that this is only true for configurations computed
during the analysis: concrete execution of the sub-paths would yield the same program states
than their counterparts in the original LTS.›

thm RedBlack.induct[of x P]

theorem (in finite_RedBlack) SE_rel :
assumes "RedBlack prb"
assumes "subpath (red prb) rv1 res rv2 (subs prb)"
assumes "se_star (confs prb rv1) (trace (ui_es res) (labelling (black prb))) c"
shows   "c ⊑ (confs prb rv2)"
using assms finite_RedBlack
proof (induct arbitrary : rv1 res rv2 c rule : RedBlack.induct)
(* If the red part is empty, then @{term "rv1 = rv2 = root (red prb)"}, and
@{term "confs prb rv1 = confs prb rv2"} which prooves the goal, subsumption
being reflexive. *)
case (base prb rv1 res rv2 c) thus ?case
by (force simp add : subpath_def Nil_sp subsums_refl)

next
(* We split the goal into four cases :
- rv1 and rv2 are vertices of the old red part,
- rv1 is a vertex in the old red part, rv2 is the target of ra,
- rv1 is the target of ra, rv2 is a vertex of the old red part,
- rv1 are rv2 both equal to the target of ra. *)
case (se_step prb re c' prb' rv1 res rv2 c)

have "rv1 ∈ red_vertices prb'"
and  "rv2 ∈ red_vertices prb'"
using fst_of_sp_is_vert[OF se_step(4)]
lst_of_sp_is_vert[OF se_step(4)]
by simp_all

hence "rv1 ∈ red_vertices prb ∧ rv1 ≠ tgt re ∨ rv1 = tgt re"
and   "rv2 ∈ red_vertices prb ∧ rv2 ≠ tgt re ∨ rv2 = tgt re"
using se_step by (auto simp add : vertices_def)

thus ?case
proof (elim disjE conjE, goal_cases)
(* rv1 are rv2 vertices of the old red part *)
case 1

(* hence res is also a subpath from rv1 to rv2 in the old red part *)
moreover
hence "subpath (red prb) rv1 res rv2 (subs prb)"
using se_step(1,3,4)
sub_rel_of.sp_from_old_verts_imp_sp_in_old
[OF subs_sub_rel_of, of prb re "red prb'" rv1 rv2 res]
by auto

(* thus, the IH can be used to conclude. *)
ultimately
show ?thesis using se_step
by (fastforce simp add : finite_RedBlack_def)

next
(* rv1 is a vertex of the old red part, rv2 is the target of ra. *)
case 2

(* hence res is empty or ra occurs only one time in res : at its end. *)
hence  "∃ res'. res = res' @ [re]
∧ re ∉ set res'
∧ subpath (red prb) rv1 res' (src re) (subs prb)"
using se_step
sub_rel_of.sp_to_new_edge_tgt_imp[OF subs_sub_rel_of, of prb re "red prb'" rv1 res]
by auto

thus ?thesis
proof (elim exE conjE)
(* If res = res'@[ra], then there exists a configuration c' such that :
- c' is obtained from (confs prb rv1) by symbolic execution of (the trace of) res,
- c' is subsumed by (confs prb (src ra)) (by IH),
- c is obtained from c' by symbolic execution of (the label of) ra.

Moreover, we have :
- (confs prb rv2) is obtained from (confs prb (src ra) by symbolic execution
of (the label of) ra.

Ultimately, we proof the goal by monotonicity of symbolic execution wrt subsumption. *)
fix res'

assume "res = res' @ [re]"
and    "re ∉ set res'"
and    "subpath (red prb) rv1 res' (src re) (subs prb)"

moreover
then obtain c'
where "se_star (confs prb rv1) (trace (ui_es res') (labelling (black prb))) c'"
and   "se c' (labelling (black prb) (ui_edge re)) c"
using se_step 2 se_star_append_one by auto blast

ultimately
have "c' ⊑ (confs prb (src re))" using se_step by fastforce

thus ?thesis
using se_step ‹rv1 ≠ tgt re› 2
‹se c' (labelling (black prb) (ui_edge re)) c›
by (auto simp add : se_mono_for_sub)
qed
next
(* rv1 is the target of ra. Hence res is empty and rv2 also equals (tgt ra),
case 3

moreover
have "rv1 = rv2"
proof -
have  "(rv1,rv2) ∈ (subs prb')"
using se_step 3
sub_rel_of.sp_from_tgt_in_extends_is_Nil
[OF subs_sub_rel_of[OF se_step(1)], of re "red prb'" res rv2]
rb_Nil_sp[OF RedBlack.se_step[OF se_step(1,3)], of rv1 rv2]
by auto

hence "rv1 ∈ subsumees (subs prb)" using se_step(3) by force

thus ?thesis
using se_step ‹rv1 = tgt re› subs_sub_rel_of[OF se_step(1)]
by (auto simp add  : sub_rel_of_def)
qed

ultimately
show ?thesis by simp
next
(* Finally, if rv1 and rv2 both equal (tgt ra), then we conclude using the fact that
the subsumption is reflexive. *)
case 4

moreover
hence "res = []"
using se_step
sub_rel_of.sp_from_tgt_in_extends_is_Nil
[OF subs_sub_rel_of[OF se_step(1)], of re "red prb'" res rv2]
by auto

ultimately
show ?thesis using se_step by (simp add : subsums_refl)
qed

next
(* Marking a red vertex does not affect the configurations associated to red vertices,
hence this case is trivial when observing that a subpath after marking is a subpath
before marking (which allows to apply the IH). *)
case (mark_step prb rv prb') thus ?case by simp

next
case (subsum_step prb sub prb' rv1 res rv2 c)

(* The fact that prb' is also red-black will be needed several times in the following. *)
have RB' : "RedBlack prb'" by (rule RedBlack.subsum_step[OF subsum_step(1,3)])

(* First, we suppose that res starts at the newly subsumed red vertex. *)
show ?case
proof (case_tac "rv1 = subsumee sub")

(* In this case, res is either empty, or a subpath starting at the subsumer of the new
subsumption. *)

assume "rv1 = subsumee sub"

hence "res = [] ∨ subpath (red prb') (subsumer sub) res rv2 (subs prb')"
using subsum_step(3,4)
wf_sub_rel_of.sp_in_extends_imp1 [ OF subs_wf_sub_rel_of[OF subsum_step(1)],
of "subsumee sub" "subsumer sub" ]
by simp

thus ?thesis
proof (elim disjE)
(* If res is empty, then rv1 equals rv2 or (rv1,rv2) is in the new subsumption relation. *)
assume "res = []"

hence  "rv1 = rv2 ∨ (rv1,rv2) ∈ (subs prb')"
using subsum_step rb_Nil_sp[OF RB'] by fast

thus ?thesis
proof (elim disjE)
(* If rv1 = rv2, "their" configurations are also equal. Moreover, res being empty, c is the
configuration at rv1. We conclude using reflexivity of subsumption. *)
assume "rv1 = rv2"
thus ?thesis
using subsum_step(5) ‹res = []›
next
(* If (rv1, rv2) is in the new subsumption relation, then the configuration at rv1 is
subsumed by the configuration at rv2. We conclude using the fact c is the configuration
at rv1. *)
assume "(rv1, rv2) ∈ (subs prb')"
thus ?thesis
using subsum_step(5) ‹res = []›
sub_subsumed[OF RB', of "(rv1,rv2)"]
by simp
qed

next
(* If res is also a subpath from the subsumer of the new subsumption, we show the goal
by (backward) induction on res *)
assume "subpath (red prb') (subsumer sub) res rv2 (subs prb')"

thus ?thesis
using subsum_step(5)
proof (induct res arbitrary : rv2 c rule : rev_induct, goal_cases)
(* If the red subpath is empty, then (rv1,rv2) is the new subsumption, which gives the goal
by definition of subsum_extends. *)
case (1 rv2 c)

have "rv2 = subsumer sub"
proof -
have "(subsumer sub,rv2) ∉ subs prb'"
proof (intro notI)
assume "(subsumer sub,rv2) ∈ subs prb'"

hence "subsumer sub ∈ subsumees (subs prb')" by force

moreover
have  "subsumer sub ∈ subsumers (subs prb')"
using subsum_step(3) by force

ultimately
show False
using subs_wf_sub_rel[OF RB']
unfolding wf_sub_rel_def
by auto
qed

thus ?thesis using 1(1) rb_Nil_sp[OF RB'] by auto
qed

thus ?case
using subsum_step(3) 1(2) ‹rv1 = subsumee sub› by simp

next
(* Inductive case : the red subpath has the form res@[ra]. *)
case (2 re res rv2 c)

(* We call :
- c' the configuration obtained by symbolic execution of res from the configuration at
rv1,
- c'' the configuration obtained by symbolic execution of ra from the configuration at
the source of ra.

We show that c' is subsumed by the configuration at the source of ra (using "internal"
IH), hence c is subsumed by c'', by monotonicity of symbolic execution for subsumption.

Moreover, we show that c'' is subsumed by the configuration at the target of ra,
using the fact that [ra] is subpath from the source of ra to its target in the old
red part with the "external" IH.

Finally, we show that the configuration at the target of ra is subsumed by the
configuration at rv2 by observing that the target of ra is either rv2, either subsumed
by rv2.

We conclude using transitivity of subsumption.  *)

hence A : "subpath (red prb') (subsumer sub) res (src re) (subs prb')"
and   B : "subpath (red prb') (src re) [re] (tgt re) (subs prb')"
using subs_sub_rel_of[OF RB'] by (auto simp add : sp_append_one sp_one)

obtain c'
where C : "se_star (confs prb' rv1) (trace (ui_es res) (labelling (black prb'))) c'"
and   D : "se c' (labelling (black prb') (ui_edge re)) c"
using 2 by (simp add : se_star_append_one) blast

obtain c''
where E : "se (confs prb' (src re)) (labelling (black prb') (ui_edge re)) c''"
using subsum_step(6-8)
‹subpath (red prb') (src re) [re] (tgt re) (subs prb')›
RB' finite_RedBlack.ex_se_succ[of prb' "src re"]
unfolding finite_RedBlack_def
by (simp add : se_star_one fst_of_sp_is_vert) blast

have "c ⊑ c''"
proof -
have "c' ⊑ confs prb' (src re)" using 2(1) A B C D by fast
thus ?thesis using D E se_mono_for_sub by fast
qed

moreover
have "c'' ⊑ confs prb' (tgt re)"
proof -
have "subpath (red prb) (src re) [re] (tgt re) (subs prb)"
proof -
have "src re ∈ red_vertices prb'"
and  "tgt re ∈ red_vertices prb'"
and  "re ∈ edges (red prb')"
using B by (auto simp add : vertices_def sp_one)

hence "src re ∈ red_vertices prb"
and   "tgt re ∈ red_vertices prb"
and   "re ∈ edges (red prb)"
using subsum_step(3) by auto

thus ?thesis
using subs_sub_rel_of[OF subsum_step(1)]
qed

thus ?thesis
using subsum_step(2,3,6-8) E
qed

moreover
have "confs prb' (tgt re) ⊑ confs prb' rv2"
proof -
have "tgt re = rv2 ∨ (tgt re,rv2) ∈ subs prb'"
using 2(2) rb_sp_append_one[OF RB'] by auto

thus ?thesis
proof (elim disjE)
assume "tgt re = rv2"
thus ?thesis by (simp add : subsums_refl)
next
assume "(tgt re, rv2) ∈ (subs prb')"
thus ?thesis using sub_subsumed RB' by fastforce
qed
qed

ultimately
show ?case using subsums_trans subsums_trans by fast
qed
qed

next

(* If res does not start at the newly subsumed red vertex, then either res is a subpath in
the old red part, either it can be splitted into two parts res1 and res2 such that :
- res1 is a subpath in the old red part from rv1 to the newly subsumed vertex,
- res2 is a subpath in the new red part from the newly subsumed vertex to rv2. *)

assume "rv1 ≠ subsumee sub"

hence  "subpath (red prb) rv1 res rv2 (subs prb) ∨
(∃ res1 res2. res = res1 @ res2
∧ res1 ≠ []
∧ subpath (red prb) rv1 res1 (subsumee sub) (subs prb)
∧ subpath (red prb') (subsumee sub) res2 rv2 (subs prb'))"
using subsum_step(3,4)
wf_sub_rel_of.sp_in_extends_imp2  [OF subs_wf_sub_rel_of[OF subsum_step(1)],
of "subsumee sub" "subsumer sub"]
by auto

thus ?thesis
proof (elim disjE exE conjE)
(* In the first case, we conclude by "external" IH. *)
assume "subpath (red prb) rv1 res rv2 (subs prb)"
thus ?thesis using subsum_step by simp

next
(* We call :
- c1 the configuration obtained from the configuration at rv1 by symbolic execution
of res1 and such that c is obtained from c1 by symbolic execution of res2,
- c2 the configuration obtained from the configuration at the newly subsumed red vertex
by symbolic execution of res2.

We show that c is subsumed by c2 and that c2 is subsumed by the configuration at rv2.
We conclude by transitivity of subsumption. *)
fix res1 res2

define t_res1 where "t_res1 = trace (ui_es res1) (labelling (black prb'))"
define t_res2 where "t_res2 = trace (ui_es res2) (labelling (black prb'))"

assume "res = res1 @ res2"
and    "res1 ≠ []"
and    "subpath (red prb) rv1 res1 (subsumee sub) (subs prb)"
and    "subpath (red prb') (subsumee sub) res2 rv2 (subs prb')"

then obtain c1 c2
where "se_star (confs prb' rv1) t_res1 c1"
and   "se_star c1 t_res2 c"
and   "se_star (confs prb' (subsumee sub)) t_res2 c2"
using subsum_step(1,3,5,6-8) RB'
finite_RedBlack.ex_se_star_succ[of prb rv1 t_res1]
finite_RedBlack.ex_se_star_succ[of prb' "subsumee sub" t_res2]
unfolding finite_RedBlack_def t_res1_def t_res2_def
by (simp  add : fst_of_sp_is_vert  se_star_append) blast

then have "c ⊑ c2"
proof -
have "c1 ⊑ confs prb' (subsumee sub)"
using subsum_step(2,3,6-8)
‹subpath (red prb) rv1 res1 (subsumee sub) (subs prb)›
‹se_star (confs prb' rv1) t_res1 c1›
by (auto simp add : t_res1_def t_res2_def)

thus ?thesis
using ‹se_star c1 t_res2 c›
‹se_star (confs prb' (subsumee sub)) t_res2 c2›
se_star_mono_for_sub
by fast
qed

moreover
(* Here we have to proceed by beckward induction on res2. *)
have "c2 ⊑ confs prb' rv2"
using ‹subpath (red prb') (subsumee sub) res2 rv2 (subs prb')›
‹se_star (confs prb' (subsumee sub)) t_res2 c2›
unfolding t_res2_def
proof (induct res2 arbitrary : rv2 c2 rule : rev_induct, goal_cases)
(* If the suffix is empty, then either subsumee sub equals rv2, either
(subsumee sub,rv2) is in the new subsumption relation. *)
case (1 rv2 c2)

hence "subsumee sub = rv2 ∨ (subsumee sub, rv2)∈subs prb'"
using rb_Nil_sp[OF RB'] by simp

thus ?case
proof (elim disjE)
(* In the first case, we have :
c = confs prb' (subsumee sub) = confs prb' rv2.
We conclude by reflexivity of the subsumption. *)
assume "subsumee sub = rv2"
thus ?thesis
using 1(2) by (simp add : subsums_refl)
next
(* In the second case, we have :
c = confs prb' (subsumee sub) ⊑ confs prb' rv2,
qed.  *)
assume "(subsumee sub, rv2) ∈ subs prb'"
thus ?thesis
using 1(2)
sub_subsumed[OF RB', of "(subsumee sub, rv2)"]
by simp
qed

next
(* Inductive case : the suffix has the form res2@[ra]. *)
case (2 re res2 rv2 c2)

(* We call :
- c3 the configuration obtained from the configuration at the newly subsumed red
vertex. c2 is obtained from c3 by symbolic execution of ra,
- c4 the configuration obtained from the configuration at the source of ra by
symbolic execution of ra.

By internal IH, we first show that c3 is subsumed by the configuration at the source of
ra. Thus c2 is subsumed by c4, by monotonicity of symbolic execution for the
subsumption.

Then we show that c4 is subsumed by the configuration at the target of ra, using the
external IH.

Finally, we show that the configuration at the target of ra is subsumed by the
configuration at rv2, by observing that either tgt ra = rv2, either (tgt ra,rv2)
is in the new subsumption relation.

We conclude by transitivity of the subsumption relation. *)

have A : "subpath (red prb') (subsumee sub) res2 (src re) (subs prb')"
and  B : "subpath (red prb') (src re) [re] rv2 (subs prb')"
using 2(2) subs_wf_sub_rel[OF RB'] subs_wf_sub_rel_of[OF RB']
by (simp_all only: wf_sub_rel.sp_append_one)

obtain c3
where C : "se_star (confs prb' (subsumee sub))
(trace (ui_es res2) (labelling (black prb')))
(c3)"
and   D : "se c3 (labelling (black prb') (ui_edge re)) c2"
using 2(3) subsum_step(6-8) RB'
finite_RedBlack.ex_se_succ[of prb' "src re"]
by (simp add : se_star_append_one) blast

obtain c4
where E : "se (confs prb' (src re)) (labelling (black prb') (ui_edge re)) c4"
using subsum_step(6-8) RB' B
finite_RedBlack.ex_se_succ[of prb' "src re"]
unfolding finite_RedBlack_def
by (simp  add : fst_of_sp_is_vert se_star_append) blast

have "c2 ⊑ c4"
proof -
have "c3 ⊑ confs prb' (src re)" using 2(1) A C by fast

thus ?thesis using D E se_mono_for_sub by fast
qed

moreover
have "c4 ⊑ confs prb' (tgt re)"
proof -
have "subpath (red prb) (src re) [re] (tgt re) (subs prb)"
proof -
have "src re ∈ red_vertices prb'"
and  "tgt re ∈ red_vertices prb'"
and  "re ∈ edges (red prb')"
using B by (auto simp add : vertices_def sp_one)

hence "src re ∈ red_vertices prb"
and   "tgt re ∈ red_vertices prb"
and   "re ∈ edges (red prb)"
using subsum_step(3) by auto

thus ?thesis
using subs_sub_rel_of[OF subsum_step(1)]
qed

thus  ?thesis
using subsum_step(2,3,6-8) E
qed

moreover
have "confs prb' (tgt re) ⊑ confs prb' rv2"
proof -
have "tgt re = rv2 ∨ (tgt re, rv2) ∈ (subs prb')"
using subsum_step 2 rb_sp_append_one[OF RB', of "subsumee sub" res2 re]
by (auto simp add : vertices_def subpath_def)

thus ?thesis
proof (elim disjE)
assume "tgt re = rv2"
thus ?thesis by (simp add : subsums_refl)
next
assume "(tgt re, rv2) ∈ (subs prb')"
thus ?thesis
using sub_subsumed RB'
by fastforce
qed
qed

ultimately
show ?case using subsums_trans subsums_trans by fast
qed

ultimately
show ?thesis by (rule subsums_trans)
qed
qed

next
case (abstract_step prb rv c⇩a prb' rv1 res rv2 c)

show ?case
proof (case_tac "rv1 = rv", goal_cases)
(* We first suppose that rv1 is the red vertex where the abstraction took place. In this case,
we have that res is empty and rv2 = rv1. Hence c is the configuration at rv2 (after
abstraction). We conclude using reflexivity of subsumption. *)
case 1

moreover
hence "res = []"
using abstract_step
sp_from_de_empty[of rv1 "subs prb" "red prb" res rv2]
by simp

moreover
have  "rv2 = rv"
proof -
have "rv1 = rv2 ∨ (rv1, rv2) ∈ (subs prb)"
using abstract_step ‹res = []›
rb_Nil_sp[OF RedBlack.abstract_step[OF abstract_step(1,3)]]
by simp

moreover
have "(rv1, rv2) ∉ (subs prb)"
using abstract_step 1
unfolding Ball_def subsumees_conv
by (intro notI) blast

ultimately
show ?thesis using 1 by simp
qed

ultimately
show ?thesis using abstract_step(5) by (simp add : subsums_refl)
next
(* Suppose that rv1 is not the red vertex where the subsumption took place. *)
case 2

show ?thesis
proof (case_tac "rv2 = rv")
(* We first suppose that rv2 is the newly abstracted red vertex. Then we have that the new
configuration at rv2 subsums the old configuration at this red vertex. We conclude
by use of IH and transitivity of subsumption. *)
assume "rv2 = rv"

hence  "confs prb rv2 ⊑ confs prb' rv2"
using abstract_step by (simp add : abstract_def)

moreover
have   "c ⊑ confs prb rv2"
using abstract_step 2 by auto

ultimately
show ?thesis using subsums_trans by fast
next
assume "rv2 ≠ rv" thus ?thesis using abstract_step 2 by simp
qed
qed

next
(* Strengthening a red vertex does not affect the red part, thus this case is trivial. *)
case strengthen_step thus ?case by simp
qed

text ‹A configuration which is indeed satisfiable can not be marked.›

lemma sat_not_marked :
assumes "RedBlack prb"
assumes "rv ∈ red_vertices prb"
assumes "sat (confs prb rv)"
shows   "¬ marked prb rv"
using assms
proof (induct prb arbitrary : rv)
case base thus ?case by simp
next
case (se_step prb re c prb')

hence "rv ∈ red_vertices prb ∨ rv = tgt re" by (auto simp add : vertices_def)

thus ?case
proof (elim disjE, goal_cases)
case 1
moreover
hence "rv ≠ tgt re" using se_step(3) by (auto simp add : vertices_def)
ultimately
show ?thesis using se_step by (elim conjE) auto
next
case 2

moreover
hence "sat (confs prb (src re))" using se_step(3,5) se_sat_imp_sat by auto

ultimately
show ?thesis using se_step(2,3) by (elim conjE) auto
qed
next
case (mark_step prb rv' prb')

moreover
hence "rv ≠ rv'" and "(rv,rv') ∉ subs prb"
using sub_subsumed[OF mark_step(1), of "(rv,rv')"] unsat_subs_unsat by auto

ultimately
show ?case by auto
next
case subsum_step thus ?case by auto

next
case (abstract_step prb rv' c⇩a prb') thus ?case by (case_tac "rv' = rv") simp+

next
case strengthen_step thus ?case by simp
qed

text‹On the other hand, a red-location which is marked unsat is indeed logically unsatisfiable.›

lemma
assumes "RedBlack prb"
assumes "rv ∈ red_vertices prb"
assumes "marked prb rv"
shows   "¬ sat (confs prb rv)"
using assms
proof (induct prb arbitrary : rv)
case base thus ?case by simp
next
case (se_step prb re c prb')

hence "rv ∈ red_vertices prb ∨ rv = tgt re" by (auto simp add : vertices_def)

thus ?case
proof (elim disjE, goal_cases)
case 1

moreover
hence "rv ≠ tgt re" using se_step(3) by auto
hence "marked prb rv" using se_step by auto

ultimately
have "¬ sat (confs prb rv)" by (rule se_step(2))

thus ?thesis using se_step(3) ‹rv ≠ tgt re› by auto
next
case 2

moreover
hence "marked prb (src re)" using se_step(3,5) by auto

ultimately
have "¬ sat (confs prb (src re))" using se_step(2,3) by auto

thus ?thesis using se_step(3) ‹rv = tgt re› unsat_imp_se_unsat by (elim conjE) auto
qed
next
case (mark_step prb rv' prb') thus ?case by (case_tac "rv' = rv") auto
next
case subsum_step thus ?case by simp

next
case (abstract_step _ rv' _) thus ?case by (case_tac "rv' = rv") simp+

next
case strengthen_step thus ?case by simp
qed

text‹Red vertices involved in subsumptions are not marked.›

lemma subsumee_not_marked :
assumes "RedBlack prb"
assumes "sub ∈ subs prb"
shows   "¬ marked prb (subsumee sub)"
using assms
proof (induct prb)
case base thus ?case by simp
next
case (se_step prb re c prb')

moreover
hence "subsumee sub ≠ tgt re"
using subs_wf_sub_rel_of[OF se_step(1)]
by (elim conjE, auto simp add : wf_sub_rel_of_def sub_rel_of_def)

ultimately
show ?case by auto
next
case mark_step thus ?case by auto
next
case subsum_step thus ?case by auto

next
case abstract_step thus ?case by auto

next
case strengthen_step thus ?case by simp
qed

lemma subsumer_not_marked :
assumes "RedBlack prb"
assumes "sub ∈ subs prb"
shows   "¬ marked prb (subsumer sub)"
using assms
proof (induct prb)
case base thus ?case by simp
next
case (se_step prb re c prb')

moreover
hence "subsumer sub ≠ tgt re"
using subs_wf_sub_rel_of[OF se_step(1)]
by (elim conjE, auto simp add : wf_sub_rel_of_def sub_rel_of_def)

ultimately
show ?case by auto
next
case (mark_step prb rv prb') thus ?case by auto
next
case (subsum_step prb sub' prb') thus ?case by auto

next
case abstract_step thus ?case by simp

next
case strengthen_step thus ?case by simp
qed

text‹If the target of a red edge is not marked, then its source is also not marked.›

lemma tgt_not_marked_imp :
assumes "RedBlack prb"
assumes "re ∈ edges (red prb)"
assumes "¬ marked prb (tgt re)"
shows   "¬ marked prb (src re)"
using assms
proof (induct prb arbitrary : re)
case base thus ?case by simp
next
case se_step thus ?case by (force simp add : vertices_def image_def)
next
case (mark_step prb rv prb' re) thus ?case by (case_tac "tgt re = rv") auto
next
case subsum_step thus ?case by simp

next
case abstract_step thus ?case by simp

next
case strengthen_step thus ?case by simp
qed

text‹Given a red subpath leading from red location @{term "rv1"} to red location @{term "rv2"},
if @{term "rv2"} is not marked, then @{term "rv1"} is also not marked (this
lemma is not used).›

lemma
assumes "RedBlack prb"
assumes "subpath (red prb) rv1 res rv2 (subs prb)"
assumes "¬ marked prb rv2"
shows   "¬ marked prb rv1"
using assms
proof (induct res arbitrary : rv1)
case Nil

hence "rv1 = rv2 ∨ (rv1,rv2) ∈ subs prb" by (simp add : rb_Nil_sp)

thus ?case
proof (elim disjE, goal_cases)
case 1 thus ?case using Nil by simp
next
case 2 show ?case using Nil subsumee_not_marked[OF Nil(1) 2] by simp
qed
next
case (Cons re res)

thus ?case
unfolding rb_sp_Cons[OF Cons(2), of rv1 re res rv2]
proof (elim conjE disjE, goal_cases)
case 1

moreover
hence "¬ marked prb (tgt re)" by simp

moreover
have "re ∈ edges (red prb)" using Cons(3) rb_sp_Cons[OF Cons(2), of rv1 re res rv2] by fast

ultimately
show ?thesis using tgt_not_marked_imp[OF Cons(2)] by fast
next
case 2 thus ?thesis using subsumee_not_marked[OF Cons(2)] by fastforce
qed
qed

subsection‹Fringe of a red-black graph›

text ‹We have stated and proved a number of properties of red-black graphs. In the end, we are
mainly interested in proving that the set of paths of such red-black graphs are subsets of the set
of feasible paths of their black part. Before defining the set of paths of red-black graphs, we
first introduce the intermediate concept of \emph{fringe} of the red part. Intuitively, the fringe
is the set of red vertices from which we can approximate more precisely the set of feasible paths of
the black part. This includes red vertices that have not been subsumed yet, that are not marked and
from which some black edges have not been yet symbolically executed (i.e.\ that have no red
counterpart from these red vertices).›

subsubsection ‹Definition›

text‹The fringe is the set of red locations from which there exist black edges that have not
been followed yet.›

definition fringe ::
"('vert, 'var, 'd, 'x) pre_RedBlack_scheme ⇒ ('vert × nat) set"
where
"fringe prb ≡ {rv ∈ red_vertices prb.
rv ∉ subsumees (subs prb) ∧
¬ marked prb rv           ∧
ui_edge  out_edges (red prb) rv ⊂ out_edges (black prb) (fst rv)}"

subsubsection ‹Fringe of an empty red-part›

text‹At the beginning of the analysis, i.e.\ when the red part is empty, the fringe consists of the
red root.›

lemma fringe_of_empty_red1 :
assumes "edges (red prb) = {}"
assumes "subs prb = {}"
assumes "marked prb = (λ rv. False)"
assumes "out_edges (black prb) (fst (root (red prb))) ≠ {}"
shows   "fringe prb = {root (red prb)}"
using assms by (auto simp add : fringe_def vertices_def)

subsubsection ‹Evolution of the fringe after extension›

text‹Simplification lemmas for the fringe of the new red-black graph after adding an edge by
symbolic execution. If the configuration from which symbolic execution is performed is not marked
yet, and if there exists black edges going out of the target of the executed edge, the target of
the new red edge enters the fringe. Moreover, if there still exist black edges that have no red
counterpart yet at the source of the new edge, then its source was and stays in the fringe.›

lemma seE_fringe1 :
assumes "sub_rel_of (red prb) (subs prb)"
assumes "se_extends prb re c' prb'"
assumes "¬ marked prb (src re)"
assumes "ui_edge  (out_edges (red prb') (src re)) ⊂ out_edges (black prb) (fst (src re))"
assumes "out_edges (black prb) (fst (tgt re)) ≠ {}"
shows   "fringe prb' = fringe prb ∪ {tgt re}"
unfolding set_eq_iff Un_iff singleton_iff
proof (intro allI iffI, goal_cases)
case (1 rv)

moreover
hence "rv ∈ red_vertices prb ∨ rv = tgt re"
using assms(2) by (auto simp add : fringe_def vertices_def)

ultimately
show ?case using assms(2) by (auto simp add : fringe_def)
next
case (2 rv)

hence  "rv ∈ red_vertices prb'" using assms(2) by (auto simp add : fringe_def vertices_def)

moreover
have "rv ∉ subsumees (subs prb')"
using 2
proof (elim disjE)
assume "rv ∈ fringe prb" thus ?thesis using assms(2) by (auto simp add : fringe_def)
next
assume "rv = tgt re" thus ?thesis
using assms(1,2) unfolding sub_rel_of_def by force
qed

moreover
have "ui_edge  (out_edges (red prb') rv) ⊂ out_edges (black prb') (fst rv)"
using 2
proof (elim disjE)
assume "rv ∈ fringe prb"

thus ?thesis
proof (case_tac "rv = src re")
assume "rv = src re" thus ?thesis using assms(2,4) by auto
next
assume "rv ≠ src re" thus ?thesis
using assms(2) ‹rv ∈ fringe prb›
by (auto simp add : fringe_def)
qed
next
assume "rv = tgt re" thus ?thesis
using assms(2,5) extends_tgt_out_edges[of re "red prb" "red prb'"] by (elim conjE) auto
qed

moreover
have "¬ marked prb' rv"
using 2
proof (elim disjE, goal_cases)
case 1

moreover
hence "rv ≠ tgt re" using assms(2) by (auto simp add : fringe_def)

ultimately
show ?thesis using assms(2) by (auto simp add : fringe_def)
next
case 2 thus ?thesis using assms(2,3) by auto
qed

ultimately
show ?case by (simp add : fringe_def)
qed

text ‹On the other hand, if all possible black edges have been executed from the source of the new
edge after the extension, then the source is removed from the fringe.›

lemma  seE_fringe4 :
assumes "sub_rel_of (red prb) (subs prb)"
assumes "se_extends prb re c' prb'"
assumes "¬ marked prb (src re)"
assumes "¬ (ui_edge  (out_edges (red prb') (src re)) ⊂ out_edges (black prb) (fst (src re)))"
assumes "out_edges (black prb) (fst (tgt re)) ≠ {}"
shows   "fringe prb' = fringe prb - {src re} ∪ {tgt re}"
unfolding set_eq_iff Un_iff singleton_iff Diff_iff
proof (intro allI iffI, goal_cases)
case (1 rv)

hence "rv ∈ red_vertices prb ∨ rv = tgt re"
and   "rv ≠ src re"
using assms(2,3,4,5) by (auto simp add : fringe_def vertices_def)

with 1 show ?case using assms(2) by (auto simp add : fringe_def)

next
case (2 rv)

hence  "rv ∈ red_vertices prb'" using assms(2) by (auto simp add : fringe_def vertices_def)

moreover
have "rv ∉ subsumees (subs prb')"
using 2
proof (elim disjE)
assume "rv ∈ fringe prb ∧ rv ≠ src re"
thus ?thesis using assms(2) by (auto simp add : fringe_def)
next
assume "rv = tgt re" thus ?thesis
using assms(1,2) unfolding sub_rel_of_def by fastforce
qed

moreover
have "ui_edge  (out_edges (red prb') rv) ⊂ out_edges (black prb') (fst rv)"
using 2
proof (elim disjE)
assume "rv ∈ fringe prb ∧ rv ≠ src re" thus ?thesis
using assms(2) by (auto simp add : fringe_def)
next
assume "rv = tgt re" thus ?thesis
using assms(2,5) extends_tgt_out_edges[of re "red prb" "red prb'"] by (elim conjE) auto
qed

moreover
have "¬ marked prb' rv"
using 2
proof (elim disjE, goal_cases)
case 1

moreover
hence "rv ≠ tgt re" using assms by (auto simp add : fringe_def)

ultimately
show ?thesis
using assms 1 by (auto simp add : fringe_def)
next
case 2 thus ?thesis using assms by auto
qed

ultimately
show ?case by (simp add : fringe_def)
qed

text ‹If the source of the new edge is marked, then its target does not enter the fringe (and the
source was not part of it in the first place).›

lemma seE_fringe2 :
assumes "se_extends prb re c prb'"
assumes "marked prb (src re)"
shows   "fringe prb' = fringe prb"
unfolding set_eq_iff Un_iff singleton_iff
proof (intro allI iffI, goal_cases)
case (1 rv)

thus ?case
unfolding fringe_def mem_Collect_eq
using assms
proof (intro conjI, goal_cases)
case 1 thus ?case by (auto simp add : fringe_def vertices_def)
next
case 2 thus ?case by auto
next
case 3

moreover
hence "rv ≠ tgt re" by auto

ultimately
show ?case by auto
next
case 4 thus ?case by auto
qed
next
case (2 rv)

thus ?case unfolding fringe_def mem_Collect_eq
using assms
proof (intro conjI, goal_cases)
case 1 thus ?case by (auto simp add : vertices_def)
next
case 2 thus ?case by auto
next
case 3
moreover
hence "rv ≠ tgt re" by auto
ultimately
show ?case by auto
next
case 4 thus ?case by auto
qed
qed

text ‹If there exists no black edges going out of the target of the new edge, then this target
does not enter the fringe.›

lemma seE_fringe3 :
assumes "se_extends prb re c' prb'"
assumes "ui_edge  (out_edges (red prb') (src re)) ⊂ out_edges (black prb) (fst (src re))"
assumes "out_edges (black prb) (fst (tgt re)) = {}"
shows   "fringe prb' = fringe prb"
unfolding set_eq_iff Un_iff singleton_iff
proof (intro allI iffI, goal_cases)
case (1 rv)

thus ?case using assms(1,3)
unfolding fringe_def mem_Collect_eq
proof (intro conjI, goal_cases)
case 1 thus ?case by (auto simp add : fringe_def vertices_def)
next
case 2 thus ?case by (auto simp add : fringe_def)
next
case 3 thus ?case by (case_tac "rv = tgt re") (auto simp add : fringe_def)
next
case 4 thus ?case by (auto simp add : fringe_def)
qed

next
case (2 rv)

moreover
hence "rv ∈ red_vertices prb'"
and   "rv ≠ tgt re"
using assms(1) by (auto simp add : fringe_def vertices_def)

moreover
have "ui_edge  (out_edges (red prb') rv) ⊂ out_edges (black prb) (fst rv)"
proof (case_tac "rv = src re")
assume "rv = src re" thus ?thesis using assms(2) by simp
next
assume "rv ≠ src re"
thus ?thesis using assms(1) 2
by (auto simp add : fringe_def)
qed

ultimately
show ?case using assms(1) by (auto simp add : fringe_def)
qed

text ‹Moreover, if all possible black edges have been executed from the source of the new edge
after the extension, then this source is removed from the fringe.›

lemma seE_fringe5 :
assumes "se_extends prb re c' prb'"
assumes "¬ (ui_edge  (out_edges (red prb') (src re)) ⊂ out_edges (black prb) (fst (src re)))"
assumes "out_edges (black prb) (fst (tgt re)) = {}"
shows   "fringe prb' = fringe prb - {src re}"
unfolding set_eq_iff Un_iff singleton_iff Diff_iff
proof (intro allI iffI, goal_cases)
case (1 rv)

moreover
have "rv ∈ red_vertices prb" and "rv ≠ src re"
using 1 assms by (auto simp add : fringe_def vertices_def)  (* slow *)

moreover
have "¬ marked prb rv"
proof (intro notI)
assume "marked prb rv"

have "marked prb' rv"
proof -
have "rv ≠ tgt re" using assms(1) ‹rv ∈ red_vertices prb› by auto

thus ?thesis using assms(1) ‹marked prb rv› by auto
qed

thus False using 1 by (auto simp add : fringe_def)
qed

ultimately
show ?case using assms(1) by (auto simp add : fringe_def)

next
case (2 rv)

hence  "rv ∈ red_vertices prb'" using assms(1) by (auto simp add : fringe_def vertices_def)

moreover
have "rv ∉ subsumees (subs prb')" using 2 assms(1) by (auto simp add : fringe_def)

moreover
have "ui_edge  (out_edges (red prb') rv) ⊂ out_edges (black prb') (fst rv)"
using 2 assms(1) by (auto simp add : fringe_def)

moreover
have "¬ marked prb' rv"
proof -
have "rv ≠ tgt re" using assms(1) 2 by (auto simp add : fringe_def)

thus ?thesis using assms(1) 2 by (auto simp add : fringe_def)
qed

ultimately
show ?case by (simp add : fringe_def)
qed

text‹Adding a subsumption to the subsumption relation removes the first member of the
subsumption from the fringe.›

lemma subsumE_fringe :
assumes "subsum_extends prb sub prb'"
shows   "fringe prb' = fringe prb - {subsumee sub}"
using assms by (auto simp add : fringe_def)

subsection‹Red-Black Sub-Paths and Paths›

text‹The set of red-black subpaths starting in red location @{term "rv"} is the union of :
\begin{itemize}
\item the set of black sub-paths that have a red counterpart starting at @{term "rv"} and leading
to a non-marked red location,
\item the set of black sub-paths that have a prefix represented in the red part starting
at @{term "rv"} and leading to an element of the fringe. Moreover, the remainings of these black
sub-paths must have no non-empty counterpart in the red part. Otherwise, the set of red-black paths
would simply be the set of paths of the black part.
\end{itemize}
›

definition RedBlack_subpaths_from ::
"('vert, 'var, 'd, 'x) pre_RedBlack_scheme ⇒ ('vert × nat) ⇒ 'vert edge list set"
where
"RedBlack_subpaths_from prb rv ≡
ui_es  {res. ∃ rv'. subpath (red prb) rv res rv' (subs prb) ∧ ¬ marked prb rv'}
∪ {ui_es res1 @ bes2
| res1 bes2. ∃ rv1. rv1 ∈ fringe prb
∧ subpath (red prb) rv res1 rv1 (subs prb)
∧ ¬ (∃ res21 bes22. bes2 = ui_es res21 @ bes22
∧ res21 ≠ []
∧ subpath_from (red prb) rv1 res21 (subs prb))
∧ Graph.subpath_from (black prb) (fst rv1) bes2}"

text‹Red-black paths are red-black subpaths starting at the root of the red part.›

abbreviation RedBlack_paths ::
"('vert, 'var, 'd, 'x) pre_RedBlack_scheme ⇒ 'vert edge list set"
where
"RedBlack_paths prb ≡ RedBlack_subpaths_from prb (root (red prb))"

text‹When the red part is empty, the set of red-black subpaths starting at the red root is the set
of black paths.›

lemma (in finite_RedBlack) base_RedBlack_paths :
assumes "fst (root (red prb)) = init (black prb)"
assumes "edges (red prb) = {}"
assumes "subs prb = {}"
assumes "confs prb (root (red prb)) = init_conf prb"
assumes "marked prb = (λ rv. False)"
assumes "strengthenings prb = (λ rv. (λ σ. True))"

shows   "RedBlack_paths prb = Graph.paths (black prb)"

proof -
show ?thesis
unfolding set_eq_iff
proof (intro allI iffI)

fix    bes
assume "bes ∈ RedBlack_subpaths_from prb (root (red prb))"
thus   "bes ∈ Graph.paths (black prb)"
unfolding  RedBlack_subpaths_from_def Un_iff
proof (elim disjE exE conjE, goal_cases)
case 1

hence "bes = []" using assms by (auto simp add: subpath_def)

thus ?thesis
by (auto simp add : Graph.subpath_def vertices_def)
next
case 2

then obtain res1 bes2 rv where "bes = ui_es res1 @ bes2"
and   "rv ∈ fringe prb"
and   "subpath (red prb) (root (red prb)) res1 rv (subs prb)"
and   "Graph.subpath_from (black prb) (fst rv) bes2"
by blast

moreover
hence "res1 = []" using assms by (simp add : subpath_def)

ultimately
show ?thesis using assms ‹rv ∈ fringe prb› by (simp add : fringe_def vertices_def)
qed
next
fix bes
assume "bes ∈ Graph.paths (black prb)"
show "bes ∈ RedBlack_subpaths_from prb (root (red prb))"
proof (case_tac "out_edges (black prb) (init (black prb)) = {}")
assume "out_edges (black prb) (init (black prb)) = {}"
show ?thesis
unfolding RedBlack_subpaths_from_def Un_iff image_def Bex_def mem_Collect_eq
apply