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