# 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 "σ⇩_{s}⇩_{y}⇩_{m}"} are \emph{consistent} with respect to a store @{term "s"} if, for each variable @{term "v"}, the value associated by @{term "σ"} to @{term "v"} is equal to the value associated by @{term "σ⇩_{s}⇩_{y}⇩_{m}"} to the symbolic variable associated to @{term "v"} by @{term "s"}.› definition consistent :: "('v,'d) state ⇒ ('v symvar, 'd) state ⇒ 'v store ⇒ bool" where "consistent σ σ⇩_{s}⇩_{y}⇩_{m}s ≡ (∀ v. σ⇩_{s}⇩_{y}⇩_{m}(symvar v s) = σ v)" text ‹There always exists a couple of consistent states for a given store.› lemma "∃ σ σ⇩_{s}⇩_{y}⇩_{m}. consistent σ σ⇩_{s}⇩_{y}⇩_{m}s" by (auto simp add : consistent_def) text ‹Moreover, given a store and a program (resp. symbolic) state, one can always build a symbolic (resp. program) state such that the two states are coherent wrt.\ the store. The four following lemmas show how to build the second state given the first one.› lemma consistent_eq1 : "consistent σ σ⇩_{s}⇩_{y}⇩_{m}s = (∀ sv ∈ symvars s. σ⇩_{s}⇩_{y}⇩_{m}sv = σ (fst sv))" by (auto simp add : consistent_def symvars_def symvar_def) lemma consistent_eq2 : "consistent σ σ⇩_{s}⇩_{y}⇩_{m}store = (σ = (λ v. σ⇩_{s}⇩_{y}⇩_{m}(symvar v store)))" by (auto simp add : consistent_def) lemma consistentI1 : "consistent σ (λ sv. σ (fst sv)) store" using consistent_eq1 by fast lemma consistentI2 : "consistent (λ v. σ⇩_{s}⇩_{y}⇩_{m}(symvar v store)) σ⇩_{s}⇩_{y}⇩_{m}store" using consistent_eq2 by fast subsection ‹Adaptation of an arithmetic expression to a store› text ‹Suppose that @{term "e"} is a term representing an arithmetic expression over program variables and let @{term "s"} be a store. We call \emph{adaptation of @{term "e"} to @{term "s"}} the term obtained by substituting occurrences of program variables in @{term "e"} by their symbolic counterpart given by @{term "s"}. Since we model arithmetic expressions by total functions and not terms, we define the adaptation of such expressions as follows.› definition adapt_aexp :: "('v,'d) aexp ⇒ 'v store ⇒ ('v symvar,'d) aexp" where "adapt_aexp e s = (λ σ⇩_{s}⇩_{y}⇩_{m}. e (λ v. σ⇩_{s}⇩_{y}⇩_{m}(symvar v s)))" text ‹Given an arithmetic expression @{term "e"}, a program state @{term "σ"} and a symbolic state @{term "σ⇩_{s}⇩_{y}⇩_{m}"} coherent with a store @{term "s"}, the value associated to @{term "σ⇩_{s}⇩_{y}⇩_{m}"} by the adaptation of @{term "e"} to @{term "s"} is the same than the value associated by @{term "e"} to @{term "σ"}. This confirms the fact that @{term "adapt_aexp"} models the act of substituting occurrences of program variables by their symbolic counterparts in a term over program variables.› lemma adapt_aexp_is_subst : assumes "consistent σ σ⇩_{s}⇩_{y}⇩_{m}s" shows "(adapt_aexp e s) σ⇩_{s}⇩_{y}⇩_{m}= 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 σ⇩_{s}⇩_{y}⇩_{m}val where "?e' (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) ≠ ?e' σ⇩_{s}⇩_{y}⇩_{m}" by (simp add : Aexp.vars_def, blast) hence "(λ x. (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) (symvar x s)) ≠ (λ x. σ⇩_{s}⇩_{y}⇩_{m}(symvar x s))" proof (intro notI) assume "(λx. (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) (symvar x s)) = (λx. σ⇩_{s}⇩_{y}⇩_{m}(symvar x s))" hence "?e' (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) = ?e' σ⇩_{s}⇩_{y}⇩_{m}" by (simp add : adapt_aexp_def) thus False using ‹?e' (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) ≠ ?e' σ⇩_{s}⇩_{y}⇩_{m}› by (elim notE) qed then obtain v where "(σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) (symvar v s) ≠ σ⇩_{s}⇩_{y}⇩_{m}(symvar v s)" by blast hence "sv = symvar v s" by (case_tac "sv = symvar v s", simp_all) thus "sv ∈ symvars s" by (simp add : symvars_def) qed lemma symvar_var_imp_var : assumes "sv ∈ Aexp.vars (adapt_aexp e s)" (is "sv ∈ Aexp.vars ?e'") shows "fst sv ∈ Aexp.vars e" proof - obtain v where "sv = (v, s v)" using assms(1) symvars_of_adapt_aexp unfolding symvars_def symvar_def by blast obtain σ⇩_{s}⇩_{y}⇩_{m}val where "?e' (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) ≠ ?e' σ⇩_{s}⇩_{y}⇩_{m}" using assms unfolding Aexp.vars_def by blast moreover have "(λ v. (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) (symvar v s)) = (λ v. σ⇩_{s}⇩_{y}⇩_{m}(symvar v s)) (v := val)" using ‹sv = (v, s v)› by (auto simp add : symvar_def) ultimately show ?thesis using ‹sv = (v, s v)› consistentI2[of σ⇩_{s}⇩_{y}⇩_{m}s] consistentI2[of "σ⇩_{s}⇩_{y}⇩_{m}(sv := val)" s] unfolding Aexp.vars_def 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 σ σ⇩_{s}⇩_{y}⇩_{m}s" shows "(adapt_bexp e s) σ⇩_{s}⇩_{y}⇩_{m}= 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 σ⇩_{s}⇩_{y}⇩_{m}val where "?e' (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) ≠ ?e' σ⇩_{s}⇩_{y}⇩_{m}" by (simp add : Bexp.vars_def, blast) hence "(λ x. (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) (symvar x s)) ≠ (λ x. σ⇩_{s}⇩_{y}⇩_{m}(symvar x s))" by (auto simp add : adapt_bexp_def) hence "∃ v. (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) (symvar v s) ≠ σ⇩_{s}⇩_{y}⇩_{m}(symvar v s)" by force then obtain v where "(σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) (symvar v s) ≠ σ⇩_{s}⇩_{y}⇩_{m}(symvar v s)" by blast hence "sv = symvar v s" by (case_tac "sv = symvar v s", simp_all) thus "sv ∈ symvars s" by (simp add : symvars_def) qed lemma symvar_var_imp_var2 : assumes "sv ∈ Bexp.vars (adapt_bexp e s)" (is "sv ∈ Bexp.vars ?e'") shows "fst sv ∈ Bexp.vars e" proof - obtain v where "sv = (v, s v)" using assms symvars_of_adapt_bexp unfolding symvars_def symvar_def by blast obtain σ⇩_{s}⇩_{y}⇩_{m}val where "?e' (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) ≠ ?e' σ⇩_{s}⇩_{y}⇩_{m}" using assms unfolding vars_def by blast moreover have "(λ v. (σ⇩_{s}⇩_{y}⇩_{m}(sv := val)) (symvar v s)) = (λ v. σ⇩_{s}⇩_{y}⇩_{m}(symvar v s)) (v := val)" using ‹sv = (v, s v)› by (auto simp add : symvar_def) ultimately show ?thesis using ‹sv = (v, s v)› consistentI2[of σ⇩_{s}⇩_{y}⇩_{m}s] consistentI2[of "σ⇩_{s}⇩_{y}⇩_{m}(sv := val)" s] 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 = {σ. ∃ σ⇩_{s}⇩_{y}⇩_{m}. consistent σ σ⇩_{s}⇩_{y}⇩_{m}(store c) ∧ conjunct (pred c) σ⇩_{s}⇩_{y}⇩_{m}}" text ‹A configuration is satisfiable if and only if its set of states is not empty.› lemma sat_eq : "sat c = (states c ≠ {})" using consistentI2 by (simp add : sat_def states_def) fast subsubsection ‹Subsumption› text ‹A configuration @{term "c⇩_{2}"} is subsumed by a configuration @{term "c⇩_{1}"} if the set of states of @{term "c⇩_{2}"} is a subset of the set of states of @{term "c⇩_{1}"}.› definition subsums :: "('v,'d) conf ⇒ ('v,'d) conf ⇒ bool" (infixl "⊑" 55) where "c⇩_{2}⊑ c⇩_{1}≡ (states c⇩_{2}⊆ states c⇩_{1})" text ‹The subsumption relation is reflexive and transitive.› lemma subsums_refl : "c ⊑ c" by (simp only : subsums_def) lemma subsums_trans : "c1 ⊑ c2 ⟹ c2 ⊑ c3 ⟹ c1 ⊑ c3" unfolding subsums_def by simp text ‹However, it is not anti-symmetric. This is due to the fact that different configurations can have the same sets of program states. However, the following lemma trivially follows the definition of subsumption.› lemma assumes "c1 ⊑ c2" assumes "c2 ⊑ c1" shows "states c1 = states c2" using assms by (simp add : subsums_def) text ‹A satisfiable configuration can only be subsumed by satisfiable configurations.› lemma sat_sub_by_sat : assumes "sat c⇩_{2}" and "c⇩_{2}⊑ c⇩_{1}" shows "sat c⇩_{1}" using assms sat_eq[of c⇩_{1}] sat_eq[of c⇩_{2}] by (simp add : subsums_def) fast text ‹On the other hand, an unsatisfiable configuration can only subsume unsatisfiable configurations.› lemma unsat_subs_unsat : assumes "¬ sat c1" assumes "c2 ⊑ c1" shows "¬ sat c2" using assms sat_eq[of c1] sat_eq[of c2] 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 "c⇩_{1}"} and @{term "c⇩_{2}"}, it is not possible to enumerate their sets of states to establish the inclusion in order to detect a subsumption. We detect the subsumption of the former by the latter by asking a constraint solver if @{term "sem c⇩_{1}"} entails @{term "sem c⇩_{2}"}. The following theorem shows that the way we detect subsumption in practice is correct.› definition sem :: "('v,'d) conf ⇒ ('v,'d) bexp" where "sem c = (λ σ. σ ∈ states c)" theorem "c⇩_{2}⊑ c⇩_{1}⟷ sem c⇩_{2}⊨⇩_{B}sem c⇩_{1}" unfolding subsums_def sem_def subset_iff entails_def by (rule refl) subsubsection ‹Abstractions› text ‹Abstracting a configuration consists in removing a given expression from its @{term "pred"} component, i.e.\ weakening its path predicate. This definition of abstraction motivates the fact that the @{term "pred"} component of configurations has been defined as a set of boolean expressions instead of a boolean expression.› definition abstract :: "('v,'d) conf ⇒ ('v,'d) conf ⇒ bool" where "abstract c c⇩_{a}≡ c ⊑ c⇩_{a}" subsubsection ‹Entailment› text ‹A configuration \emph{entails} a boolean expression if its semantics entails this expression. This is equivalent to say that this expression holds for any state of this configuration.› abbreviation entails :: "('v,'d) conf ⇒ ('v,'d) bexp ⇒ bool" (infixl "⊨⇩_{c}" 55) where "c ⊨⇩_{c}φ ≡ sem c ⊨⇩_{B}φ" lemma "sem c ⊨⇩_{B}e ⟷ (∀ σ ∈ states c. e σ)" by (auto simp add : states_def sem_def entails_def) end

# Theory SymExec

theory SymExec imports Conf Labels begin subsection ‹Symbolic Execution› text ‹We model symbolic execution by an inductive predicate @{term "se"} which takes two configurations @{term "c⇩_{1}"} and @{term "c⇩_{2}"} and a label @{term "l"} and evaluates to \emph{true} if and only if @{term "c⇩_{2}"} is a \emph{possible result} of the symbolic execution of @{term "l"} from @{term "c⇩_{1}"}. We say that @{term "c⇩_{2}"} is a possible result because, when @{term "l"} is of the form @{term "Assign v e"}, we associate a fresh symbolic variable to the program variable @{term "v"}, but we do no specify how this fresh variable is chosen (see the two assumptions in the third case). We could have model @{term "se"} (and @{term "se_star"}) by a function producing the new configuration, instead of using inductive predicates. However this would require to provide the two said assumptions in each lemma involving @{term se}, which is not necessary using a predicate. Modeling symbolic execution in this way has the advantage that it simplifies the following proofs while not 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 σ⇩_{s}⇩_{y}⇩_{m}where 1 : "consistent σ' σ⇩_{s}⇩_{y}⇩_{m}(store c')" and 2 : "conjunct (pred c') σ⇩_{s}⇩_{y}⇩_{m}" using assms(2) unfolding states_def by blast then obtain σ where 3 : "consistent σ σ⇩_{s}⇩_{y}⇩_{m}(store c)" using consistentI2 by blast moreover have "conjunct (pred c) σ⇩_{s}⇩_{y}⇩_{m}" using assms(1) 2 by (auto simp add : se_Assign_eq conjunct_def) ultimately have "σ ∈ states c" by (simp add : states_def) blast moreover have "σ' = σ (v := e σ)" proof - have "σ' v = e σ" proof - have "σ' v = σ⇩_{s}⇩_{y}⇩_{m}(symvar v (store c'))" using 1 by (simp add : consistent_def) moreover have "σ⇩_{s}⇩_{y}⇩_{m}(symvar v (store c')) = (adapt_aexp e (store c)) σ⇩_{s}⇩_{y}⇩_{m}" using assms(1) 2 se_Assign_eq[of c v e c'] by (force simp add : symvar_def conjunct_def) moreover have "(adapt_aexp e (store c)) σ⇩_{s}⇩_{y}⇩_{m}= e σ" 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 = σ⇩_{s}⇩_{y}⇩_{m}(symvar x (store c))" using assms(1) 1 unfolding consistent_def symvar_def by (drule_tac ?x="x" in spec) (auto simp add : se_Assign_eq) moreover have "σ⇩_{s}⇩_{y}⇩_{m}(symvar x (store c)) = σ x" using 3 by (auto simp add : consistent_def) ultimately show "σ' x = σ x" by simp qed ultimately show ?thesis by auto qed ultimately show ?thesis by (simp add : states_def) blast qed text ‹Then, we show that if there exists a state @{term "σ"} of @{term "c"} from which @{term "σ'"} is obtained by an adequate update, then @{term "σ'"} is a state of @{term "c'"}.› lemma states_of_se_assign2 : assumes "se c (Assign v e) c'" assumes "∃ σ ∈ states c. σ' = σ (v := e σ)" shows "σ' ∈ states c'" proof - obtain σ where "σ ∈ states c" and "σ' = σ (v := e σ)" using assms(2) by blast then obtain σ⇩_{s}⇩_{y}⇩_{m}where 1 : "consistent σ σ⇩_{s}⇩_{y}⇩_{m}(store c)" and 2 : "conjunct (pred c) σ⇩_{s}⇩_{y}⇩_{m}" unfolding states_def by blast obtain sv where 3 : "fresh_symvar sv c" and 4 : "fst sv = v" and 5 : "c' = ⦇ store = (store c)(v := snd sv), pred = insert (λσ. σ sv = adapt_aexp e (store c) σ) (pred c) ⦈" using assms(1) se_Assign_eq[of c v e c'] by blast define σ⇩_{s}⇩_{y}⇩_{m}' where "σ⇩_{s}⇩_{y}⇩_{m}' = σ⇩_{s}⇩_{y}⇩_{m}(sv := e σ)" have "consistent σ' σ⇩_{s}⇩_{y}⇩_{m}' (store c')" using ‹σ' = σ (v := e σ)› 1 4 5 by (auto simp add : symvar_def consistent_def σ⇩_{s}⇩_{y}⇩_{m}'_def) moreover have "conjunct (pred c') σ⇩_{s}⇩_{y}⇩_{m}'" proof - have "conjunct (pred c) σ⇩_{s}⇩_{y}⇩_{m}'" using 2 3 by (simp add : fresh_symvar_def symvars_def Bexp.vars_def σ⇩_{s}⇩_{y}⇩_{m}'_def) moreover have "σ⇩_{s}⇩_{y}⇩_{m}' sv = (adapt_aexp e (store c)) σ⇩_{s}⇩_{y}⇩_{m}'" proof - have "Aexp.fresh sv (adapt_aexp e (store c))" using 3 symvars_of_adapt_aexp[of e "store c"] by (auto simp add : fresh_symvar_def symvars_def) thus ?thesis using adapt_aexp_is_subst[OF 1, of e] by (simp add : Aexp.vars_def σ⇩_{s}⇩_{y}⇩_{m}'_def) qed ultimately show ?thesis using 5 by (simp add: conjunct_def) qed ultimately show ?thesis unfolding states_def by blast qed text ‹The following theorem expressing the set of states of @{term c'} as a function of the set of states of @{term c} trivially follows the two preceding lemmas.› theorem states_of_se_assign : assumes "se c (Assign v e) c'" shows "states c' = {σ (v := e σ) | σ. σ ∈ states c}" using assms states_of_se_assign1 states_of_se_assign2 by fast subsubsection ‹Monotonicity of $\mathit{se}$› text ‹We are now ready to prove that symbolic execution is monotonic with respect to subsumption. › theorem se_mono_for_sub : assumes "se c1 l c1'" assumes "se c2 l c2'" assumes "c2 ⊑ c1" shows "c2' ⊑ c1'" using assms by ((cases l), (simp add : ), (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 "∀e∈pred c1'. finite (Bexp.vars e)" by (rule se_preserves_finiteness1[OF ‹finite_label l› ‹se c1 l c1'› Cons(5)]) moreover have "∀e∈pred c2'. finite (Bexp.vars e)" by (rule se_preserves_finiteness1[OF ‹finite_label l› ‹se c2 l c2'› Cons(6)]) moreover have "c2' ⊑ c1'" by (rule se_mono_for_sub[OF ‹se c1 l c1'› ‹se c2 l c2'› Cons(7)]) ultimately show ?thesis using Cons(1) ‹feasible c2' ls› ‹finite_labels ls› by fast qed ultimately show ?case by (auto simp add : feasible_Cons) qed subsection ‹Concrete execution› text ‹We illustrate our notion of symbolic execution by relating it with @{term ce}, an inductive predicate describing concrete execution. Unlike symbolic execution, concrete execution describes program behavior given program states, i.e.\ concrete valuations for program variables. The goal of this section is to show that our notion of symbolic execution is correct, that is: given two configurations such that one results from the symbolic execution of a sequence of labels from the other, then the resulting configuration represents the set of states that are reachable by concrete execution from the states of the original configuration.› inductive ce :: "('v,'d) state ⇒ ('v,'d) label ⇒ ('v,'d) state ⇒ bool" where "ce σ Skip σ" | "e σ ⟹ ce σ (Assume e) σ" | "ce σ (Assign v e) (σ(v := e σ))" inductive ce_star :: "('v,'d) state ⇒ ('v,'d) label list ⇒ ('v,'d) state ⇒ bool" where "ce_star c [] c" | "ce c1 l c2 ⟹ ce_star c2 ls c3 ⟹ ce_star c1 (l # ls) c3" lemma [simp] : "ce σ Skip σ' = (σ' = σ)" by (auto simp add : ce.simps) lemma [simp] : "ce σ (Assume e) σ' = (σ' = σ ∧ e σ)" by (auto simp add : ce.simps) lemma [simp] : "ce σ (Assign v e) σ' = (σ' = σ(v := e σ))" by (auto simp add : ce.simps) lemma se_as_ce : assumes "se c l c'" shows "states c' = {σ'. ∃ σ ∈ states c. ce σ l σ'} " using assms by (cases l) (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 c⇩_{a}prb' ≡ rv ∈ red_vertices prb ∧ ¬ marked prb rv ∧ out_edges (red prb) rv = {} ∧ rv ∉ subsumees (subs prb) ∧ abstract (confs prb rv) c⇩_{a}∧ c⇩_{a}⊨⇩_{c}(strengthenings prb rv) ∧ finite (pred c⇩_{a}) ∧ (∀ e ∈ pred c⇩_{a}. finite (vars e)) ∧ prb' = ⦇ red = red prb, black = black prb, subs = subs prb, init_conf = init_conf prb, confs = (confs prb)(rv := c⇩_{a}), marked = marked prb, strengthenings = strengthenings prb, … = more prb ⦈" subsubsection ‹Extension by strengthening› text ‹This operation consists in labeling a red vertex with a safeguard condition. It does not actually change the red part, but model the mechanism of preventing too crude abstractions.› abbreviation strengthen_extends :: "('vert,'var,'d) pre_RedBlack ⇒ ('vert × nat) ⇒ ('var,'d) bexp ⇒ ('vert,'var,'d) pre_RedBlack ⇒ bool" where "strengthen_extends prb rv e prb' ≡ rv ∈ red_vertices prb ∧ rv ∉ subsumees (subs prb) ∧ confs prb rv ⊨⇩_{c}e ∧ prb' = ⦇ red = red prb, black = black prb, subs = subs prb, init_conf = init_conf prb, confs = confs prb, marked = marked prb, strengthenings = (strengthenings prb)(rv := (λ σ. (strengthenings prb rv) σ ∧ e σ)), … = more prb ⦈" subsection ‹Building Red-Black Graphs using Extensions› text‹Red-black graphs are pre-red-black graphs built with the following inductive relation, i.e.\ using only the five previous pre-red-black graphs transformation operators, starting from an empty red part.› inductive RedBlack :: "('vert,'var,'d) pre_RedBlack ⇒ bool" where base : "fst (root (red prb)) = init (black prb) ⟹ edges (red prb) = {} ⟹ subs prb = {} ⟹ (confs prb) (root (red prb)) = init_conf prb ⟹ marked prb = (λ rv. False) ⟹ strengthenings prb = (λ rv. (λ σ. True)) ⟹ RedBlack prb" | se_step : "RedBlack prb ⟹ se_extends prb re p' prb' ⟹ RedBlack prb'" | mark_step : "RedBlack prb ⟹ mark_extends prb rv prb' ⟹ RedBlack prb'" | subsum_step : "RedBlack prb ⟹ subsum_extends prb sub prb' ⟹ RedBlack prb'" | abstract_step : "RedBlack prb ⟹ abstract_extends prb rv c⇩_{a}prb' ⟹ RedBlack prb'" | strengthen_step : "RedBlack prb ⟹ strengthen_extends prb rv e prb' ⟹ RedBlack prb'" subsection ‹Properties of Red-Black-Graphs› subsubsection‹Invariants of the Red\hyp{}Black Graphs› text‹The red part of a red-black graph is loop free.› lemma assumes "RedBlack prb" shows "loop_free (red prb)" using assms by (induct prb) auto text‹A red edge can not lead to the (red) root.› lemma assumes "RedBlack prb" assumes "re ∈ edges (red prb)" shows "tgt re ≠ root (red prb)" using assms by (induct prb) (auto simp add : vertices_def) text‹Red edges are specific versions of black edges.› lemma ui_re_is_be : assumes "RedBlack prb" assumes "re ∈ edges (red prb)" shows "ui_edge re ∈ edges (black prb)" using assms by (induct rule : RedBlack.induct) auto text‹The set of out-going edges from a red vertex is a subset of the set of out-going edges from the black location it represents.› lemma red_OA_subset_black_OA : assumes "RedBlack prb" shows "ui_edge ` out_edges (red prb) rv ⊆ out_edges (black prb) (fst rv)" using assms by (induct prb) (fastforce simp add : vertices_def)+ text ‹The red root is an indexed version of the black initial location.› lemma consistent_roots : assumes "RedBlack prb" shows "fst (root (red prb)) = init (black prb)" using assms by (induct prb) auto text‹The red part of a red-black graph is a tree.› lemma assumes "RedBlack prb" shows "is_tree (red prb)" using assms by (induct prb) (auto simp add : empty_graph_is_tree ArcExt.extends_is_tree) text ‹A red-black graph whose black part is well-formed is also well-formed.› lemma assumes "RedBlack prb" assumes "wf_lts (black prb)" shows "wf_pre_RedBlack prb" proof - have "wf_rgraph (red prb)" using assms by (induct prb) (force simp add : vertices_def)+ thus ?thesis using assms consistent_roots ui_re_is_be by (auto simp add : wf_pre_RedBlack_def) qed text ‹Red locations of a red-black graph are indexed versions of its black locations.› lemma ui_rv_is_bv : assumes "RedBlack prb" assumes "rv ∈ red_vertices prb" shows "fst rv ∈ Graph.vertices (black prb)" using assms consistent_roots ui_re_is_be by (auto simp add : vertices_def image_def Bex_def) fastforce+ text ‹The subsumption of a red-black graph is a sub-relation of its red part.› lemma subs_sub_rel_of : assumes "RedBlack prb" shows "sub_rel_of (red prb) (subs prb)" using assms unfolding sub_rel_of_def proof (induct prb) case base thus ?case by simp next case se_step thus ?case by (elim conjE) (auto simp add : vertices_def) next case mark_step thus ?case by auto next case subsum_step thus ?case by auto next case abstract_step thus ?case by simp next case strengthen_step thus ?case by simp qed text‹The subsumption relation of red-black graph is well-formed.› lemma subs_wf_sub_rel : assumes "RedBlack prb" shows "wf_sub_rel (subs prb)" using assms proof (induct prb) case base thus ?case by (simp add : wf_sub_rel_def) next case se_step thus ?case by force next case mark_step thus ?case by (auto simp add : wf_sub_rel_def) next case subsum_step thus ?case by (auto simp add : wf_sub_rel.extends_imp_wf_sub_rel) next case abstract_step thus ?case by simp next case strengthen_step thus ?case by simp qed text ‹Using the two previous lemmas, we have that the subsumption relation of a red-black graph is a well-formed sub-relation of its red-part.› lemma subs_wf_sub_rel_of : assumes "RedBlack prb" shows "wf_sub_rel_of (red prb) (subs prb)" using assms subs_sub_rel_of subs_wf_sub_rel by (simp add : wf_sub_rel_of_def) fast text‹Subsumptions only involve red locations representing the same black location.› lemma subs_to_same_BL : assumes "RedBlack prb" assumes "sub ∈ subs prb" shows "fst (subsumee sub) = fst (subsumer sub)" using assms subs_wf_sub_rel unfolding wf_sub_rel_def by fast text‹If a red edge sequence @{term "res"} is consistent between red locations @{term "rv1"} and @{term "rv2"} with respect to the subsumption relation of a red-black graph, then its unindexed version is consistent between the black locations represented by @{term "rv1"} and @{term "rv2"}.› lemma rces_imp_bces : assumes "RedBlack prb" assumes "SubRel.ces rv1 res rv2 (subs prb)" shows "Graph.ces (fst rv1) (ui_es res) (fst rv2)" using assms proof (induct res arbitrary : rv1) case (Nil rv1) thus ?case using wf_sub_rel.in_trancl_imp[OF subs_wf_sub_rel] subs_to_same_BL by fastforce next case (Cons re res rv1) hence 1 : "rv1 = src re ∨ (rv1, src re) ∈ (subs prb)⇧^{+}" and 2 : "ces (tgt re) res rv2 (subs prb)" by simp_all have "src (ui_edge re) = fst rv1" using 1 wf_sub_rel.in_trancl_imp[OF subs_wf_sub_rel[OF assms(1)], of rv1 "src re"] subs_to_same_BL[OF assms(1), of "(rv1,src re)"] by auto moreover have "Graph.ces (tgt (ui_edge re)) (ui_es res) (fst rv2)" using assms(1) Cons(1) 2 by simp ultimately show ?case by simp qed text‹The unindexed version of a subpath in the red part of a red-black graph is a subpath in its black part. This is an important fact: in the end, it helps proving that set of paths we consider in red-black graphs are paths of the original LTS. Thus, the same states are computed along these paths.› theorem red_sp_imp_black_sp : assumes "RedBlack prb" assumes "subpath (red prb) rv1 res rv2 (subs prb)" shows "Graph.subpath (black prb) (fst rv1) (ui_es res) (fst rv2)" using assms rces_imp_bces ui_rv_is_bv ui_re_is_be unfolding subpath_def Graph.subpath_def by (intro conjI) (fast, fast, fastforce) text‹Any constraint in the path predicate of a configuration associated to a red location of a red-black graph contains a finite number of variables.› lemma finite_pred_constr_symvars : assumes "RedBlack prb" assumes "finite_RedBlack prb" assumes "rv ∈ red_vertices prb" shows "∀ e ∈ pred (confs prb rv). finite (Bexp.vars e)" using assms proof (induct prb arbitrary : rv) case base thus ?case by (simp add : vertices_def finite_RedBlack_def) next case (se_step prb re c' prb') hence "rv ∈ red_vertices prb ∨ rv = tgt re" by (auto simp add : vertices_def) thus ?case proof (elim disjE) assume "rv ∈ red_vertices prb" moreover have "finite_RedBlack prb" using se_step(3,4) by (auto simp add : finite_RedBlack_def) ultimately show ?thesis using se_step(2,3) by (elim conjE) (auto simp add : vertices_def) next assume "rv = tgt re" moreover have "finite_label (labelling (black prb) (ui_edge re))" using se_step by (auto simp add : finite_RedBlack_def) moreover have "∀ e ∈ pred (confs prb (src re)). finite (Bexp.vars e)" using se_step se_step(2)[of "src re"] unfolding finite_RedBlack_def by (elim conjE) auto moreover have "se (confs prb (src re)) (labelling (black prb) (ui_edge re)) c'" using se_step by auto ultimately show ?thesis using se_step se_preserves_finiteness1 by fastforce qed next case mark_step thus ?case by (simp add : finite_RedBlack_def) next case subsum_step thus ?case by (simp add : finite_RedBlack_def) next case abstract_step thus ?case by (auto simp add : finite_RedBlack_def) next case strengthen_step thus ?case by (simp add : finite_RedBlack_def) qed text ‹The path predicate of a configuration associated to a red location of a red-black graph contains a finite number of constraints.› lemma finite_pred : assumes "RedBlack prb" assumes "finite_RedBlack prb" assumes "rv ∈ red_vertices prb" shows "finite (pred (confs prb rv))" using assms proof (induct prb arbitrary : rv) case base thus ?case by (simp add : vertices_def finite_RedBlack_def) next case (se_step prb re c' prb') hence "rv ∈ red_vertices prb ∨ rv = tgt re" by (auto simp add : vertices_def) thus ?case proof (elim disjE, goal_cases) case 1 thus ?thesis using se_step(2)[of rv] se_step(3,4) by (auto simp add : finite_RedBlack_def) next case 2 moreover hence "src re ∈ red_vertices prb" and "finite (pred (confs prb (src re)))" using se_step(2)[of "src re"] se_step(3,4) by (auto simp add : finite_RedBlack_def) ultimately show ?thesis using se_step(3) se_preserves_finiteness2 by auto qed next case mark_step thus ?case by (simp add : finite_RedBlack_def) next case subsum_step thus ?case by (simp add : finite_RedBlack_def) next case abstract_step thus ?case by (simp add : finite_RedBlack_def) next case strengthen_step thus ?case by (simp add : finite_RedBlack_def) qed text‹Hence, for a red location @{term "rv"} of a red-black graph and any label @{term "l"}, there exists a configuration that can be obtained by symbolic execution of @{term "l"} from the configuration associated to @{term "rv"}.› lemma (in finite_RedBlack) ex_se_succ : assumes "RedBlack prb" assumes "rv ∈ red_vertices prb" shows "∃ c'. se (confs prb rv) l c'" using finite_RedBlack assms finite_imp_ex_se_succ[of "confs prb rv"] finite_pred[of prb rv ] finite_pred_constr_symvars[of prb rv] unfolding finite_RedBlack_def by fast text‹Generalization of the previous lemma to a list of labels.› lemma (in finite_RedBlack) ex_se_star_succ : assumes "RedBlack prb" assumes "rv ∈ red_vertices prb" assumes "finite_labels ls" shows "∃ c'. se_star (confs prb rv) ls c'" using finite_RedBlack assms finite_imp_ex_se_star_succ[of "confs prb rv" ls] finite_pred[OF assms(1), of rv] finite_pred_constr_symvars[OF assms(1), of rv] unfolding finite_RedBlack_def by simp text‹Hence, for any red sub-path, there exists a configuration that can be obtained by symbolic execution of its trace from the configuration associated to its source.› lemma (in finite_RedBlack) sp_imp_ex_se_star_succ : assumes "RedBlack prb" assumes "subpath (red prb) rv1 res rv2 (subs prb)" shows "∃ c. se_star (confs prb rv1) (trace (ui_es res) (labelling (black prb))) c" using finite_RedBlack assms ex_se_star_succ by (simp add : subpath_def finite_RedBlack_def) text‹The configuration associated to a red location @{term "rl"} is update-able.› lemma (in finite_RedBlack) assumes "RedBlack prb" assumes "rv ∈ red_vertices prb" shows "updatable (confs prb rv)" using finite_RedBlack assms finite_conj[OF finite_pred[OF assms(1)] finite_pred_constr_symvars[OF assms(1)]] finite_pred_imp_se_updatable unfolding finite_RedBlack_def by fast text‹The configuration associated to the first member of a subsumption is subsumed by the configuration at its second member.› lemma sub_subsumed : assumes "RedBlack prb" assumes "sub ∈ subs prb" shows "confs prb (subsumee sub) ⊑ confs prb (subsumer sub)" using assms proof (induct prb) case base thus ?case by simp next case (se_step prb re c' prb') moreover hence "sub ∈ subs prb" by auto hence "subsumee sub ∈ red_vertices prb" and "subsumer sub ∈ red_vertices prb" using se_step(1) subs_sub_rel_of unfolding sub_rel_of_def by fast+ moreover have "tgt re ∉ red_vertices prb" using se_step by auto ultimately show ?case by auto next case mark_step thus ?case by simp next case (subsum_step prb sub prb') thus ?case by auto next case (abstract_step prb rv c⇩_{a}prb') hence "rv ≠ subsumee sub" by auto show ?case proof (case_tac "rv = subsumer sub") assume "rv = subsumer sub" moreover hence "confs prb (subsumer sub) ⊑ confs prb' (subsumer sub)" using abstract_step abstract_def by auto ultimately show ?thesis using abstract_step subsums_trans[of "confs prb (subsumee sub)" "confs prb (subsumer sub)" "confs prb' (subsumer sub)"] 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 c⇩_{a}prb' rv1 res rv2 c) show ?case proof (case_tac "rv1 = rv", goal_cases) (* We first suppose that rv1 is the red vertex where the abstraction took place. In this case, we have that res is empty and rv2 = rv1. Hence c is the configuration at rv2 (after abstraction). We conclude using reflexivity of subsumption. *) case 1 moreover hence "res = []" using abstract_step sp_from_de_empty[of rv1 "subs prb" "red prb" res rv2] by simp moreover have "rv2 = rv" proof - have "rv1 = rv2 ∨ (rv1, rv2) ∈ (subs prb)" using abstract_step ‹res = []› rb_Nil_sp[OF RedBlack.abstract_step[OF abstract_step(1,3)]] by simp moreover have "(rv1, rv2) ∉ (subs prb)" using abstract_step 1 unfolding Ball_def subsumees_conv by (intro notI) blast ultimately show ?thesis using 1 by simp qed ultimately show ?thesis using abstract_step(5) by (simp add : subsums_refl) next (* Suppose that rv1 is not the red vertex where the subsumption took place. *) case 2 show ?thesis proof (case_tac "rv2 = rv") (* We first suppose that rv2 is the newly abstracted red vertex. Then we have that the new configuration at rv2 subsums the old configuration at this red vertex. We conclude by use of IH and transitivity of subsumption. *) assume "rv2 = rv" hence "confs prb rv2 ⊑ confs prb' rv2" using abstract_step by (simp add : abstract_def) moreover have "c ⊑ confs prb rv2" using abstract_step 2 by auto ultimately show ?thesis using subsums_trans by fast next assume "rv2 ≠ rv" thus ?thesis using abstract_step 2 by simp qed qed next (* Strengthening a red vertex does not affect the red part, thus this case is trivial. *) case strengthen_step thus ?case by simp qed 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' c⇩_{a}prb') thus ?case by (case_tac "rv' = rv") simp+ next case strengthen_step thus ?case by simp qed text‹On the other hand, a red-location which is marked unsat is indeed logically unsatisfiable.› lemma assumes "RedBlack prb" assumes "rv ∈ red_vertices prb" assumes "marked prb rv" shows "¬ sat (confs prb rv)" using assms proof (induct prb arbitrary : rv) case base thus ?case by simp next case (se_step prb re c prb') hence "rv ∈ red_vertices prb ∨ rv = tgt re" by (auto simp add : vertices_def) thus ?case proof (elim disjE, goal_cases) case 1 moreover hence "rv ≠ tgt re" using se_step(3) by auto hence "marked prb rv" using se_step by auto ultimately have "¬ sat (confs prb rv)" by (rule se_step(2)) thus ?thesis using se_step(3) ‹rv ≠ tgt re› by auto next case 2 moreover hence "marked prb (src re)" using se_step(3,5) by auto ultimately have "¬ sat (confs prb (src re))" using se_step(2,3) by auto thus ?thesis using se_step(3) ‹rv = tgt re› unsat_imp_se_unsat by (elim conjE) auto qed next case (mark_step prb rv' prb') thus ?case by (case_tac "rv' = rv") auto next case subsum_step thus ?case by simp next case (abstract_step _ rv' _) thus ?case by (case_tac "rv' = rv") simp+ next case strengthen_step thus ?case by simp qed text‹Red vertices involved in subsumptions are not marked.› lemma subsumee_not_marked : assumes "RedBlack prb" assumes "sub ∈ subs prb" shows "¬ marked prb (subsumee sub)" using assms proof (induct prb) case base thus ?case by simp next case (se_step prb re c prb') moreover hence "subsumee sub ≠ tgt re" using subs_wf_sub_rel_of[OF se_step(1)] by (elim conjE, auto simp add : wf_sub_rel_of_def sub_rel_of_def) ultimately show ?case by auto next case mark_step thus ?case by auto next case subsum_step thus ?case by auto next case abstract_step thus ?case by auto next case strengthen_step thus ?case by simp qed lemma subsumer_not_marked : assumes "RedBlack prb" assumes "sub ∈ subs prb" shows "¬ marked prb (subsumer sub)" using assms proof (induct prb) case base thus ?case by simp next case (se_step prb re c prb') moreover hence "subsumer sub ≠ tgt re" using subs_wf_sub_rel_of[OF se_step(1)] by (elim conjE, auto simp add : wf_sub_rel_of_def sub_rel_of_def) ultimately show ?case by auto next case (mark_step prb rv prb') thus ?case by auto next case (subsum_step prb sub' prb') thus ?case by auto next case abstract_step thus ?case by simp next case strengthen_step thus ?case by simp qed text‹If the target of a red edge is not marked, then its source is also not marked.› lemma tgt_not_marked_imp : assumes "RedBlack prb" assumes "re ∈ edges (red prb)" assumes "¬ marked prb (tgt re)" shows "¬ marked prb (src re)" using assms proof (induct prb arbitrary : re) case base thus ?case by simp next case se_step thus ?case by (force simp add : vertices_def image_def) next case (mark_step prb rv prb' re) thus ?case by (case_tac "tgt re = rv") auto next case subsum_step thus ?case by simp next case abstract_step thus ?case by simp next case strengthen_step thus ?case by simp qed text‹Given a red subpath leading from red location @{term "rv1"} to red location @{term "rv2"}, if @{term "rv2"} is not marked, then @{term "rv1"} is also not marked (this lemma is not used).› lemma assumes "RedBlack prb" assumes "subpath (red prb) rv1 res rv2 (subs prb)" assumes "¬ marked prb rv2" shows "¬ marked prb rv1" using assms proof (induct res arbitrary : rv1) case Nil hence "rv1 = rv2 ∨ (rv1,rv2) ∈ subs prb" by (simp add : rb_Nil_sp) thus ?case proof (elim disjE, goal_cases) case 1 thus ?case using Nil by simp next case 2 show ?case using Nil subsumee_not_marked[OF Nil(1) 2] by simp qed next case (Cons re res) thus ?case unfolding rb_sp_Cons[OF Cons(2), of rv1 re res rv2] proof (elim conjE disjE, goal_cases) case 1 moreover hence "¬ marked prb (tgt re)" by simp moreover have "re ∈ edges (red prb)" using Cons(3) rb_sp_Cons[OF Cons(2), of rv1 re res rv2] by fast ultimately show ?thesis using tgt_not_marked_imp[OF Cons(2)] by fast next case 2 thus ?thesis using subsumee_not_marked[OF Cons(2)] by fastforce qed qed subsection‹Fringe of a red-black graph› text ‹We have stated and proved a number of properties of red-black graphs. In the end, we are mainly interested in proving that the set of paths of such red-black graphs are subsets of the set of feasible paths of their black part. Before defining the set of paths of red-black graphs, we first introduce the intermediate concept of \emph{fringe} of the red part. Intuitively, the fringe is the set of red vertices from which we can approximate more precisely the set of feasible paths of the black part. This includes red vertices that have not been subsumed yet, that are not marked and from which some black edges have not been yet symbolically executed (i.e.\ that have no red counterpart from these red vertices).› subsubsection ‹Definition› text‹The fringe is the set of red locations from which there exist black edges that have not been followed yet.› definition fringe :: "('vert, 'var, 'd, 'x) pre_RedBlack_scheme ⇒ ('vert × nat) set" where "fringe prb ≡ {rv ∈ red_vertices prb. rv ∉ subsumees (subs prb) ∧ ¬ marked prb rv ∧ ui_edge ` out_edges (red prb) rv ⊂ out_edges (black prb) (fst rv)}" subsubsection ‹Fringe of an empty red-part› text‹At the beginning of the analysis, i.e.\ when the red part is empty, the fringe consists of the red root.› lemma fringe_of_empty_red1 : assumes "edges (red prb) = {}" assumes "subs prb = {}" assumes "marked prb = (λ rv. False)" assumes "out_edges (black prb) (fst (root (red prb))) ≠ {}" shows "fringe prb = {root (red prb)}" using assms by (auto simp add : fringe_def vertices_def) subsubsection ‹Evolution of the fringe after extension› text‹Simplification lemmas for the fringe of the new red-black graph after adding an edge by symbolic execution. If the configuration from which symbolic execution is performed is not marked yet, and if there exists black edges going out of the target of the executed edge, the target of the new red edge enters the fringe. Moreover, if there still exist black edges that have no red counterpart yet at the source of the new edge, then its source was and stays in the fringe.› lemma seE_fringe1 : assumes "sub_rel_of (red prb) (subs prb)" assumes "se_extends prb re c' prb'" assumes "¬ marked prb (src re)" assumes "ui_edge ` (out_edges (red prb') (src re)) ⊂ out_edges (black prb) (fst (src re))" assumes "out_edges (black prb) (fst (tgt re)) ≠ {}" shows "fringe prb' = fringe prb ∪ {tgt re}" unfolding set_eq_iff Un_iff singleton_iff proof (intro allI iffI, goal_cases) case (1 rv) moreover hence "rv ∈ red_vertices prb ∨ rv = tgt re" using assms(2) by (auto simp add : fringe_def vertices_def) ultimately show ?case using assms(2) by (auto simp add : fringe_def) next case (2 rv) hence "rv ∈ red_vertices prb'" using assms(2) by (auto simp add : fringe_def vertices_def) moreover have "rv ∉ subsumees (subs prb')" using 2 proof (elim disjE) assume "rv ∈ fringe prb" thus ?thesis using assms(2) by (auto simp add : fringe_def) next assume "rv = tgt re" thus ?thesis using assms(1,2) unfolding sub_rel_of_def by force qed moreover have "ui_edge ` (out_edges (red prb') rv) ⊂ out_edges (black prb') (fst rv)" using 2 proof (elim disjE) assume "rv ∈ fringe prb" thus ?thesis proof (case_tac "rv = src re") assume "rv = src re" thus ?thesis using assms(2,4) by auto next assume "rv ≠ src re" thus ?thesis using assms(2) ‹rv ∈ fringe prb› by (auto simp add : fringe_def) qed next assume "rv = tgt re" thus ?thesis using assms(2,5) extends_tgt_out_edges[of re "red prb" "red prb'"] by (elim conjE) auto qed moreover have "¬ marked prb' rv" using 2 proof (elim disjE, goal_cases) case 1 moreover hence "rv ≠ tgt re" using assms(2) by (auto simp add : fringe_def) ultimately show ?thesis using assms(2) by (auto simp add : fringe_def) next case 2 thus ?thesis using assms(2,3) by auto qed ultimately show ?case by (simp add : fringe_def) qed text ‹On the other hand, if all possible black edges have been executed from the source of the new edge after the extension, then the source is removed from the fringe.› lemma seE_fringe4 : assumes "sub_rel_of (red prb) (subs prb)" assumes "se_extends prb re c' prb'" assumes "¬ marked prb (src re)" assumes "¬ (ui_edge ` (out_edges (red prb') (src re)) ⊂ out_edges (black prb) (fst (src re)))" assumes "out_edges (black prb) (fst (tgt re)) ≠ {}" shows "fringe prb' = fringe prb - {src re} ∪ {tgt re}" unfolding set_eq_iff Un_iff singleton_iff Diff_iff proof (intro allI iffI, goal_cases) case (1 rv) hence "rv ∈ red_vertices prb ∨ rv = tgt re" and "rv ≠ src re" using assms(2,3,4,5) by (auto simp add : fringe_def vertices_def) with 1 show ?case using assms(2) by (auto simp add : fringe_def) next case (2 rv) hence "rv ∈ red_vertices prb'" using assms(2) by (auto simp add : fringe_def vertices_def) moreover have "rv ∉ subsumees (subs prb')" using 2 proof (elim disjE) assume "rv ∈ fringe prb ∧ rv ≠ src re" thus ?thesis using assms(2) by (auto simp add : fringe_def) next assume "rv = tgt re" thus ?thesis using assms(1,2) unfolding sub_rel_of_def by fastforce qed moreover have "ui_edge ` (out_edges (red prb') rv) ⊂ out_edges (black prb') (fst rv)" using 2 proof (elim disjE) assume "rv ∈ fringe prb ∧ rv ≠ src re" thus ?thesis using assms(2) by (auto simp add : fringe_def) next assume "rv = tgt re" thus ?thesis using assms(2,5) extends_tgt_out_edges[of re "red prb" "red prb'"] by (elim conjE) auto qed moreover have "¬ marked prb' rv" using 2 proof (elim disjE, goal_cases) case 1 moreover hence "rv ≠ tgt re" using assms by (auto simp add : fringe_def) ultimately show ?thesis using assms 1 by (auto simp add : fringe_def) next case 2 thus ?thesis using assms by auto qed ultimately show ?case by (simp add : fringe_def) qed text ‹If the source of the new edge is marked, then its target does not enter the fringe (and the source was not part of it in the first place).› lemma seE_fringe2 : assumes "se_extends prb re c prb'" assumes "marked prb (src re)" shows "fringe prb' = fringe prb" unfolding set_eq_iff Un_iff singleton_iff proof (intro allI iffI, goal_cases) case (1 rv) thus ?case unfolding fringe_def mem_Collect_eq using assms proof (intro conjI, goal_cases) case 1 thus ?case by (auto simp add : fringe_def vertices_def) next case 2 thus ?case by auto next case 3 moreover hence "rv ≠ tgt re" by auto ultimately show ?case by auto next case 4 thus ?case by auto qed next case (2 rv) thus ?case unfolding fringe_def mem_Collect_eq using assms proof (intro conjI, goal_cases) case 1 thus ?case by (auto simp add : vertices_def) next case 2 thus ?case by auto next case 3 moreover hence "rv ≠ tgt re" by auto ultimately show ?case by auto next case 4 thus ?case by auto qed qed text ‹If there exists no black edges going out of the target of the new edge, then this target does not enter the fringe.› lemma seE_fringe3 : assumes "se_extends prb re c' prb'" assumes "ui_edge ` (out_edges (red prb') (src re)) ⊂ out_edges (black prb) (fst (src re))" assumes "out_edges (black prb) (fst (tgt re)) = {}" shows "fringe prb' = fringe prb" unfolding set_eq_iff Un_iff singleton_iff proof (intro allI iffI, goal_cases) case (1 rv) thus ?case using assms(1,3) unfolding fringe_def mem_Collect_eq proof (intro conjI, goal_cases) case 1 thus ?case by (auto simp add : fringe_def vertices_def) next case 2 thus ?case by (auto simp add : fringe_def) next case 3 thus ?case by (case_tac "rv = tgt re") (auto simp add : fringe_def) next case 4 thus ?case by (auto simp add : fringe_def) qed next case (2 rv) moreover hence "rv ∈ red_vertices prb'" and "rv ≠ tgt re" using assms(1) by (auto simp add : fringe_def vertices_def) moreover have "ui_edge ` (out_edges (red prb') rv) ⊂ out_edges (black prb) (fst rv)" proof (case_tac "rv = src re") assume "rv = src re" thus ?thesis using assms(2) by simp next assume "rv ≠ src re" thus ?thesis using assms(1) 2 by (auto simp add : fringe_def) qed ultimately show ?case using assms(1) by (auto simp add : fringe_def) qed text ‹Moreover, if all possible black edges have been executed from the source of the new edge after the extension, then this source is removed from the fringe.› lemma seE_fringe5 : assumes "se_extends prb re c' prb'" assumes "¬ (ui_edge ` (out_edges (red prb') (src re)) ⊂ out_edges (black prb) (fst (src re)))" assumes "out_edges (black prb) (fst (tgt re)) = {}" shows "fringe prb' = fringe prb - {src re}" unfolding set_eq_iff Un_iff singleton_iff Diff_iff proof (intro allI iffI, goal_cases) case (1 rv) moreover have "rv ∈ red_vertices prb" and "rv ≠ src re" using 1 assms by (auto simp add : fringe_def vertices_def) (* slow *) moreover have "¬ marked prb rv" proof (intro notI) assume "marked prb rv" have "marked prb' rv" proof - have "rv ≠ tgt re" using assms(1) ‹rv ∈ red_vertices prb› by auto thus ?thesis using assms(1) ‹marked prb rv› by auto qed thus False using 1 by (auto simp add : fringe_def) qed ultimately show ?case using assms(1) by (auto simp add : fringe_def) next case (2 rv) hence "rv ∈ red_vertices prb'" using assms(1) by (auto simp add : fringe_def vertices_def) moreover have "rv ∉ subsumees (subs prb')" using 2 assms(1) by (auto simp add : fringe_def) moreover have "ui_edge ` (out_edges (red prb') rv) ⊂ out_edges (black prb') (fst rv)" using 2 assms(1) by (auto simp add : fringe_def) moreover have "¬ marked prb' rv" proof - have "rv ≠ tgt re" using assms(1) 2 by (auto simp add : fringe_def) thus ?thesis using assms(1) 2 by (auto simp add : fringe_def) qed ultimately show ?case by (simp add : fringe_def) qed text‹Adding a subsumption to the subsumption relation removes the first member of the subsumption from the fringe.› lemma subsumE_fringe : assumes "subsum_extends prb sub prb'" shows "fringe prb' = fringe prb - {subsumee sub}" using assms by (auto simp add : fringe_def) subsection‹Red-Black Sub-Paths and Paths› text‹The set of red-black subpaths starting in red location @{term "rv"} is the union of : \begin{itemize} \item the set of black sub-paths that have a red counterpart starting at @{term "rv"} and leading to a non-marked red location, \item the set of black sub-paths that have a prefix represented in the red part starting at @{term "rv"} and leading to an element of the fringe. Moreover, the remainings of these black sub-paths must have no non-empty counterpart in the red part. Otherwise, the set of red-black paths would simply be the set of paths of the black part. \end{itemize} › definition RedBlack_subpaths_from :: "('vert, 'var, 'd, 'x) pre_RedBlack_scheme ⇒ ('vert × nat) ⇒ 'vert edge list set" where "RedBlack_subpaths_from prb rv ≡ ui_es ` {res. ∃ rv'. subpath (red prb) rv res rv' (subs prb) ∧ ¬ marked prb rv'} ∪ {ui_es res1 @ bes2 | res1 bes2. ∃ rv1. rv1 ∈ fringe prb ∧ subpath (red prb) rv res1 rv1 (subs prb) ∧ ¬ (∃ res21 bes22. bes2 = ui_es res21 @ bes22 ∧ res21 ≠ [] ∧ subpath_from (red prb) rv1 res21 (subs prb)) ∧ Graph.subpath_from (black prb) (fst rv1) bes2}" text‹Red-black paths are red-black subpaths starting at the root of the red part.› abbreviation RedBlack_paths :: "('vert, 'var, 'd, 'x) pre_RedBlack_scheme ⇒ 'vert edge list set" where "RedBlack_paths prb ≡ RedBlack_subpaths_from prb (root (red prb))" text‹When the red part is empty, the set of red-black subpaths starting at the red root is the set of black paths.› lemma (in finite_RedBlack) base_RedBlack_paths : assumes "fst (root (red prb)) = init (black prb)" assumes "edges (red prb) = {}" assumes "subs prb = {}" assumes "confs prb (root (red prb)) = init_conf prb" assumes "marked prb = (λ rv. False)" assumes "strengthenings prb = (λ rv. (λ σ. True))" shows "RedBlack_paths prb = Graph.paths (black prb)" proof - show ?thesis unfolding set_eq_iff proof (intro allI iffI) fix bes assume "bes ∈ RedBlack_subpaths_from prb (root (red prb))" thus "bes ∈ Graph.paths (black prb)" unfolding RedBlack_subpaths_from_def Un_iff proof (elim disjE exE conjE, goal_cases) case 1 hence "bes = []" using assms by (auto simp add: subpath_def) thus ?thesis by (auto simp add : Graph.subpath_def vertices_def) next case 2 then obtain res1 bes2 rv where "bes = ui_es res1 @ bes2" and "rv ∈ fringe prb" and "subpath (red prb) (root (red prb)) res1 rv (subs prb)" and "Graph.subpath_from (black prb) (fst rv) bes2" by blast moreover hence "res1 = []" using assms by (simp add : subpath_def) ultimately show ?thesis using assms ‹rv ∈ fringe prb› by (simp add : fringe_def vertices_def) qed next fix bes assume "bes ∈ Graph.paths (black prb)" show "bes ∈ RedBlack_subpaths_from prb (root (red prb))" proof (case_tac "out_edges (black prb) (init (black prb)) = {}") assume "out_edges (black prb) (init (black prb)) = {}" show ?thesis unfolding RedBlack_subpaths_from_def Un_iff image_def Bex_def mem_Collect_eq apply