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