Theory Bexp

theory Bexp
imports Aexp
begin

section ‹Boolean Expressions›

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

subsection‹Basic definitions›

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

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

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


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


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


subsubsection‹Satisfiability of an expression›

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


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


subsubsection ‹Entailment›

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

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


subsubsection ‹Conjunction›

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


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



subsection‹Properties about the variables of an expression›

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

subsubsection ‹Variables of a conjunction›

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


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

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

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

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


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

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


subsubsection ‹Variables of an equality›

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


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

  fix v assume "v ∈ vars ?e"

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

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

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


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

end