Session InfPathElimination

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)
   ((simp add : subpath_def, fast),
    (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
 

subsection ‹Adding Edges›

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


abbreviation add_edge :: 
  "('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 
modeling choices done later. Within Isabelle/HOL, nothing is known about this set. The set of 
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)"
by (simp add : finite_prod)

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 
operations: @{term adapt_aexp} and @{term adapt_bexp}.›

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 "σsym"} 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 "σsym"} 
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 σ σsym s  ( v. σsym (symvar v s) = σ v)"


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


lemma
  " σ σsym. consistent σ σsym 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 σ σsym s = ( sv  symvars s. σsym sv = σ (fst sv))"
by (auto simp add : consistent_def symvars_def symvar_def)


lemma consistent_eq2 :
  "consistent σ σsym store = (σ = (λ v. σsym (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. σsym (symvar v store)) σsym 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.›


definition adapt_aexp :: 
  "('v,'d) aexp  'v store  ('v symvar,'d) aexp" 
where
  "adapt_aexp e s = (λ σsym. e (λ v. σsym (symvar v s)))"


text ‹Given an arithmetic expression @{term "e"}, a program state @{term "σ"} and a symbolic 
state @{term "σsym"} coherent with a store @{term "s"}, the value associated to @{term "σsym"} 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.›


lemma adapt_aexp_is_subst :
  assumes "consistent σ σsym s" 
  shows   "(adapt_aexp e s) σsym = e σ"
using assms by (simp add : consistent_eq2 adapt_aexp_def)



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) 
     (simp add : adapt_aexp_is_subst)
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.›


lemma symvars_of_adapt_aexp :
  "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 σsym val 
  where "?e' (σsym (sv := val))  ?e' σsym" 
  by (simp add : Aexp.vars_def, blast)

  hence "(λ x. (σsym (sv := val)) (symvar x s))  (λ x. σsym (symvar x s))"
  proof (intro notI)
    assume "(λx. (σsym(sv := val)) (symvar x s)) = (λx. σsym (symvar x s))"
    
    hence "?e' (σsym (sv := val)) = ?e' σsym" 
    by (simp add : adapt_aexp_def)
    
    thus False 
    using ?e' (σsym (sv := val))  ?e' σsym 
    by (elim notE)
  qed

  then obtain v 
  where "(σsym (sv := val)) (symvar v s)  σsym (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)" 
  using assms(1) symvars_of_adapt_aexp 
  unfolding symvars_def symvar_def 
  by blast
  
  obtain σsym val where "?e' (σsym (sv := val))  ?e' σsym"
  using assms unfolding Aexp.vars_def by blast

  moreover
  have "(λ v. (σsym (sv := val)) (symvar v s)) = (λ v. σsym (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 σsym s] 
        consistentI2[of "σsym (sv := val)" s]
  unfolding Aexp.vars_def 
  by (simp add : adapt_aexp_is_subst) blast
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.›


lemma adapt_aexp_vars :
  "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" 
  using 1 symvars_of_adapt_aexp 
  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.›


lemma finite_vars_imp_finite_adapt_a :
  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.›


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


lemma adapt_bexp_is_subst :
  assumes "consistent σ σsym s" 
  shows   "(adapt_bexp e s) σsym = e σ"
using assms by (simp add : consistent_eq2 adapt_bexp_def)


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) 
     (simp add : adapt_bexp_is_subst)
qed


lemma symvars_of_adapt_bexp :
  "Bexp.vars (adapt_bexp e s)  symvars s" (is "Bexp.vars ?e'  ?SV")
proof
  fix sv
  assume "sv  Bexp.vars ?e'"

  then obtain σsym val 
  where "?e' (σsym (sv := val))  ?e' σsym"
  by (simp add : Bexp.vars_def, blast)

  hence "(λ x. (σsym (sv := val)) (symvar x s))  (λ x. σsym (symvar x s))"
  by (auto simp add : adapt_bexp_def)

  hence " v. (σsym (sv := val)) (symvar v s)  σsym (symvar v s)" by force

  then obtain v 
  where "(σsym (sv := val)) (symvar v s)  σsym (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)" 
  using assms symvars_of_adapt_bexp 
  unfolding symvars_def symvar_def 
  by blast
  
  obtain σsym val where "?e' (σsym (sv := val))  ?e' σsym"
  using assms unfolding vars_def by blast

  moreover
  have "(λ v. (σsym (sv := val)) (symvar v s)) = (λ v. σsym (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 σsym s] 
        consistentI2[of "σsym (sv := val)" s]
  unfolding vars_def by (simp add : adapt_bexp_is_subst) blast
qed


lemma adapt_bexp_vars :
  "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" 
  using 1 symvars_of_adapt_bexp 
  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 


lemma finite_vars_imp_finite_adapt_b :
  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 = {σ.  σsym. consistent σ σsym (store c)  conjunct (pred c) σsym}"


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 "c2"} is subsumed by a configuration @{term "c1"} if the set of 
states of @{term "c2"} is a subset of the set of states of @{term "c1"}.›


definition subsums :: 
  "('v,'d) conf  ('v,'d) conf  bool" (infixl "" 55) 
where     
  "c2  c1  (states c2  states c1)"


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 c2"
  and     "c2  c1"
  shows   "sat c1"
using assms sat_eq[of c1] sat_eq[of c2] 
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] 
by (simp add : subsums_def)


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 "c1"} and @{term "c2"}, 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 c1"} entails 
@{term "sem c2"}. 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
  "c2  c1  sem c2 B sem c1"
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 
instead of a boolean expression.›


definition abstract ::
  "('v,'d) conf  ('v,'d) conf  bool"
where
  "abstract c ca  c  ca"


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 "c1"} and @{term "c2"} and a label @{term "l"} and evaluates to \emph{true} if 
and only if @{term "c2"} is a \emph{possible result} of the symbolic execution of @{term "l"} from 
@{term "c1"}. We say that @{term "c2"} 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 
requiring additional lemmas.›

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)"
by (simp add : se.simps)


lemma se_Assume_eq :
  "se c (Assume e) c' = (c' =  store = store c, pred = pred c  {adapt_bexp e (store c)} )"
by (simp add : se.simps)


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'] 
by (auto simp add : adapt_bexp_is_subst states_def 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 "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 σsym
  where 1 : "consistent σ' σsym (store c')"
  and   2 : "conjunct (pred c') σsym"
  using assms(2) unfolding states_def by blast

  then obtain σ 
  where 3 : "consistent σ σsym (store c)" 
  using consistentI2 by blast

  moreover
  have "conjunct (pred c) σsym" 
  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 = σsym (symvar v (store c'))" 
      using 1 by (simp add : consistent_def)

      moreover
      have "σsym (symvar v (store c')) = (adapt_aexp e (store c)) σsym"
      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)) σsym = e σ" 
      using 3 by (rule adapt_aexp_is_subst)
    
      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 = σsym (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 "σsym (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 σsym 
  where 1 : "consistent σ σsym (store c)"
  and   2 : "conjunct (pred c) σsym"
  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 σsym' where "σsym' = σsym (sv := e σ)"
  
  have "consistent σ' σsym' (store c')"
  using σ' = σ (v := e σ) 1 4 5 
  by (auto simp add : symvar_def consistent_def σsym'_def)
  
  moreover
  have "conjunct (pred c') σsym'"
  proof -
    have "conjunct (pred c) σsym'" 
    using 2 3 by (simp add : fresh_symvar_def symvars_def Bexp.vars_def σsym'_def)

    moreover
    have "σsym' sv = (adapt_aexp e (store c)) σsym'"
    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 
      using adapt_aexp_is_subst[OF 1, of e] 
      by (simp add : Aexp.vars_def σsym'_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 : ),
    (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)]
by (simp add : subsums_def)


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)]
by (simp add : subsums_def)


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 
  using assms finite_vars_imp_finite_adapt_b
  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)))"
    using assms(1) Assign finite_vars_imp_finite_adapt_a
    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 "epred c1'. finite (Bexp.vars e)" 
    by (rule se_preserves_finiteness1[OF ‹finite_label l ‹se c1 l c1' Cons(5)])

    moreover
    have "epred 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)
   (auto simp add: states_of_se_assume states_of_se_assign)


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) 
   (force simp add : subpath_def sub_rel_of_def, (simp add : sp_Cons, fast))


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


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

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

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

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

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


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


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


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


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


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


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


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

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

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


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


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

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

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

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

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

end

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 
        by (simp add : Graph.sp_append_one)
  
        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)]
  by (simp_all add : wf_sub_rel.Nil_sp)
  
  moreover
  hence "v1 = v2  (v1,v2)  subs"
  using assms(1) 2 by auto

  moreover
  have "v2  Graph.vertices g"
  using assms(2) by (intro lst_of_sp_is_vert)

  ultimately
  show "subpath g v1 [] v2 subs" 
  using sub_rel_of by (auto simp add : subpath_def)
qed


text ‹Thus, sub-paths after the extension that do not use the new subsumption are also sub-paths 
before the extension.›

lemma (in wf_sub_rel_of) sp_in_extends_not_using_sub :
  assumes "extends g subs (v,v') subs'"
  assumes "subpath g v1 es v2 subs'"
  assumes "¬ uses_sub v1 es v2 (v,v')"
  shows   "subpath g v1 es v2 subs"
using sub_rel_of assms extends_imp_wf_sub_rel_of 
by (induction es arbitrary : v1) 
   (auto simp add : sp_Nil_in_extends_imp wf_sub_rel_of.sp_Cons sp_Cons)



text ‹We are finally able to describe sub-paths starting at any other vertex than the new 
subsumee after the extension. Such sub-paths are made of a finite number of sub-paths before the 
extension: the usage of the new subsumption between such (sub-)sub-paths makes them sub-paths 
after the extension. We express this idea as follows. Sub-paths starting at any other vertex 
than the new subsumee are either: 
\begin{itemize}
  \item sub-paths of the graph before the extension,
  \item made of a non-empty prefix that is a sub-path leading to the new subsumee in the original 
graph and a (potentially empty) suffix that is a sub-path starting at the new subsumer after 
the extension.
\end{itemize}
For the second case, the lemma \verb?sp_in_extends_imp1? as well as the following lemma could be 
applied to the suffix in order to decompose it into sub-paths of the graph before extension 
(combined with the fact that we only consider finite sub-paths, we indirectly obtain that sub-paths 
after the extension are made of a finite number of sub-paths before the extension, that are made 
consistent with the new relation by using the new subsumption).›

lemma (in wf_sub_rel_of) sp_in_extends_imp2 : 
  assumes "extends g subs (v,v') subs'"
  assumes "subpath g v1 es v2 subs'"
  assumes "v1  v"
 
  shows   "subpath g v1 es v2 subs  ( es1 es2. es = es1 @ es2 
                                                es1  [] 
                                                subpath g v1 es1 v subs 
                                                subpath g v es2 v2 subs')"
          (is "?P es v1")
proof (case_tac "uses_sub v1 es v2 (v,v')", goal_cases)
  case 1

  thus ?thesis
  using assms(2,3)
  proof (induction es arbitrary : v1)
    case (Nil v1) thus ?case by auto
  next
    case (Cons edge es v1)

    hence "v1 = src edge  (v1, src edge)  subs'"
    and   "edge  edges g" 
    and   "subpath g (tgt edge) es v2 subs'"
    using assms(1) extends_imp_wf_sub_rel_of 
    by (simp_all add : wf_sub_rel_of.sp_Cons)

    hence "subpath g v1 [edge] (tgt edge) subs'" 
    using  wf_sub_rel_of.sp_one[OF extends_imp_wf_sub_rel_of[OF assms(1)]]
    by (simp add : subpath_def) fast

    have "subpath g v1 [edge] (tgt edge) subs"
    proof -
      have "¬ uses_sub v1 [edge] (tgt edge) (v,v')" 
      using assms(1) Cons(2,4) by auto

      thus ?thesis
      using assms(1) ‹subpath g v1 [edge] (tgt edge) subs' 
      by (elim sp_in_extends_not_using_sub)
    qed

    thus ?case
    proof (case_tac "tgt edge = v", goal_cases)  
      case 1 thus ?thesis 
      using ‹subpath g v1 [edge] (tgt edge) subs  
            ‹subpath g (tgt edge) es v2 subs'
      by (intro disjI2, rule_tac ?x="[edge]" in exI) auto
    next
      case 2

      moreover
      have "uses_sub (tgt edge) es v2 (v,v')" using Cons(2,4) by simp

      ultimately
      have "?P es (tgt edge)" 
      using ‹subpath g (tgt edge) es v2 subs' 
      by (intro Cons.IH)

      thus ?thesis
      proof (elim disjE exE conjE, goal_cases)
        case 1 thus ?thesis 
        using ‹subpath g (tgt edge) es v2 subs' 
              ‹uses_sub (tgt edge) es v2 (v,v') 
              extends_and_sp_imp_not_using_sub[OF assms(1)]
        by fast
      next
        case (2 es1 es2) thus ?thesis 
        using es = es1 @ es2 
              ‹subpath g v1 [edge] (tgt edge) subs 
              ‹subpath g v es2 v2 subs'
        by (intro disjI2, rule_tac ?x="edge # es1" in exI) (auto simp add : sp_Cons)
      qed
    qed 
  qed
next
  case 2 thus ?thesis 
  using assms(1,2) by (simp add : sp_in_extends_not_using_sub)
qed

end

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 ca prb'  
     rv  red_vertices prb
    ¬ marked prb rv  
    out_edges (red prb) rv = {} 
    rv  subsumees (subs prb)
    abstract (confs prb rv) ca
    ca c (strengthenings prb rv)
    finite (pred ca)
    ( e  pred ca. finite (vars e))
    prb' =   red       = red prb, 
               black     = black prb, 
               subs      = subs prb, 
               init_conf = init_conf prb,
               confs     = (confs prb)(rv := ca),
               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 ca 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 ca 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)"]
         by (simp add : subsums_refl)
  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), 
       which contradicts our hypothesis. *) 
    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 = [] 
             by (simp add : subsums_refl)
      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)] 
                 by (simp add : sp_one)
          qed

          thus ?thesis 
               using subsum_step(2,3,6-8) E 
               by (simp add : se_star_one)
        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)
                    (simp add : wf_sub_rel_of.sp_one wf_sub_rel_of_def)

        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)] 
                 by (simp add : sp_one)
          qed

          thus  ?thesis 
                using subsum_step(2,3,6-8) E 
                by (simp add : se_star_one)
        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 ca 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









subsection‹Properties about marking.›

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' ca 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