Theory Vars

(* Author: Tobias Nipkow *)

header "Definite Initialization Analysis"

theory Vars imports BExp
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.\ @{text
avars} and @{text bvars}, but we overload the name @{text 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

end