Theory HOL-IMP.Vars

(* Author: Tobias Nipkow *)

section "Definite Initialization Analysis"

theory Vars imports Com
begin

subsection "The Variables in an Expression"

text‹We need to collect the variables in both arithmetic and boolean
expressions. For a change we do not introduce two functions, e.g.\ ‹avars› and ‹bvars›, but we overload the name ‹vars›
via a \emph{type class}, a device that originated with Haskell:›
 
class vars =
fixes vars :: "'a ⇒ vname set"

text‹This defines a type class ``vars'' with a single
function of (coincidentally) the same name. Then we define two separated
instances of the class, one for \<^typ>‹aexp› and one for \<^typ>‹bexp›:›

instantiation aexp :: vars
begin

fun vars_aexp :: "aexp ⇒ vname set" where
"vars (N n) = {}" |
"vars (V x) = {x}" |
"vars (Plus a⇩1 a⇩2) = vars a⇩1 ∪ vars a⇩2"

instance ..

end

value "vars (Plus (V ''x'') (V ''y''))"

instantiation bexp :: vars
begin

fun vars_bexp :: "bexp ⇒ vname set" where
"vars (Bc v) = {}" |
"vars (Not b) = vars b" |
"vars (And b⇩1 b⇩2) = vars b⇩1 ∪ vars b⇩2" |
"vars (Less a⇩1 a⇩2) = vars a⇩1 ∪ vars a⇩2"

instance ..

end

value "vars (Less (Plus (V ''z'') (V ''y'')) (V ''x''))"

abbreviation
  eq_on :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a set ⇒ bool"
 (‹(_ =/ _/ on _)› [50,0,50] 50) where
"f = g on X == ∀ x ∈ X. f x = g x"

lemma aval_eq_if_eq_on_vars[simp]:
  "s⇩1 = s⇩2 on vars a ⟹ aval a s⇩1 = aval a s⇩2"
apply(induction a)
apply simp_all
done

lemma bval_eq_if_eq_on_vars:
  "s⇩1 = s⇩2 on vars b ⟹ bval b s⇩1 = bval b s⇩2"
proof(induction b)
  case (Less a1 a2)
  hence "aval a1 s⇩1 = aval a1 s⇩2" and "aval a2 s⇩1 = aval a2 s⇩2" by simp_all
  thus ?case by simp
qed simp_all

fun lvars :: "com ⇒ vname set" where
"lvars SKIP = {}" |
"lvars (x::=e) = {x}" |
"lvars (c1;;c2) = lvars c1 ∪ lvars c2" |
"lvars (IF b THEN c1 ELSE c2) = lvars c1 ∪ lvars c2" |
"lvars (WHILE b DO c) = lvars c"

fun rvars :: "com ⇒ vname set" where
"rvars SKIP = {}" |
"rvars (x::=e) = vars e" |
"rvars (c1;;c2) = rvars c1 ∪ rvars c2" |
"rvars (IF b THEN c1 ELSE c2) = vars b ∪ rvars c1 ∪ rvars c2" |
"rvars (WHILE b DO c) = vars b ∪ rvars c"

instantiation com :: vars
begin

definition "vars_com c = lvars c ∪ rvars c"

instance ..

end

lemma vars_com_simps[simp]:
  "vars SKIP = {}"
  "vars (x::=e) = {x} ∪ vars e"
  "vars (c1;;c2) = vars c1 ∪ vars c2"
  "vars (IF b THEN c1 ELSE c2) = vars b ∪ vars c1 ∪ vars c2"
  "vars (WHILE b DO c) = vars b ∪ vars c"
by(auto simp: vars_com_def)

lemma finite_avars[simp]: "finite(vars(a::aexp))"
by(induction a) simp_all

lemma finite_bvars[simp]: "finite(vars(b::bexp))"
by(induction b) simp_all

lemma finite_lvars[simp]: "finite(lvars(c))"
by(induction c) simp_all

lemma finite_rvars[simp]: "finite(rvars(c))"
by(induction c) simp_all

lemma finite_cvars[simp]: "finite(vars(c::com))"
by(simp add: vars_com_def)

end