Quelle Vars.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

section "Definite Initialization Analysis"

theory Vars imports Com
begin

subsection "The Variables in an Expression"

text\<open>We need to collect the variables in both arithmetic and boolean
expressions. For a change we do not introduce two functions, e.g.\ \<open>avars\<close> and \<open>bvars\<close>, but we overload the name \<open>vars\<close>
via a \emph{type class}, a device that originated with Haskell:\<close>

class vars =
fixes vars :: "'a \ vname set"

text\<open>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>\<open>aexp\<close> and one for \<^typ>\<open>bexp\<close>:\<close>

instantiation aexp :: vars
begin

fun vars_aexp :: "aexp \ vname set" where
"vars (N n) = {}" |
"vars (V x) = {x}" |
"vars (Plus a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \ vars a\<^sub>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\<^sub>1 b\<^sub>2) = vars b\<^sub>1 \ vars b\<^sub>2" |
"vars (Less a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \ vars a\<^sub>2"

instance ..

end

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

abbreviation
  eq_on :: "('a \ 'b) \ ('a \ 'b) \ 'a set \ bool"
(\<open>(_ =/ _/ on _)\<close> [50,0,50] 50) where
"f = g on X == \ x \ X. f x = g x"

lemma aval_eq_if_eq_on_vars[simp]:
  "s\<^sub>1 = s\<^sub>2 on vars a \ aval a s\<^sub>1 = aval a s\<^sub>2"
apply(induction a)
apply simp_all
done

lemma bval_eq_if_eq_on_vars:
  "s\<^sub>1 = s\<^sub>2 on vars b \ bval b s\<^sub>1 = bval b s\<^sub>2"
proof(induction b)
  case (Less a1 a2)
  hence "aval a1 s\<^sub>1 = aval a1 s\<^sub>2" and "aval a2 s\<^sub>1 = aval a2 s\<^sub>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

quality95%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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 ist noch experimentell.