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› a
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 🍋‹aexp› a
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 ?caseby 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
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
