diff -r 0e70511cbba9 -r c25764d7246e src/HOL/IMP/Vars.thy
--- a/src/HOL/IMP/Vars.thy	Sun May 19 20:41:19 2013 +0200
+++ b/src/HOL/IMP/Vars.thy	Mon May 20 03:41:58 2013 +0200
@@ -67,29 +67,50 @@
   thus ?case by simp
 qed simp_all
 
+fun lvars :: "com \<Rightarrow> vname set" where
+"lvars SKIP = {}" |
+"lvars (x::=e) = {x}" |
+"lvars (c1;;c2) = lvars c1 \<union> lvars c2" |
+"lvars (IF b THEN c1 ELSE c2) = lvars c1 \<union> lvars c2" |
+"lvars (WHILE b DO c) = lvars c"
+
+fun rvars :: "com \<Rightarrow> vname set" where
+"rvars SKIP = {}" |
+"rvars (x::=e) = vars e" |
+"rvars (c1;;c2) = rvars c1 \<union> rvars c2" |
+"rvars (IF b THEN c1 ELSE c2) = vars b \<union> rvars c1 \<union> rvars c2" |
+"rvars (WHILE b DO c) = vars b \<union> rvars c"
 
 instantiation com :: vars
 begin
 
-fun vars_com :: "com \<Rightarrow> vname set" where
-"vars SKIP = {}" |
-"vars (x::=e) = {x} \<union> vars e" |
-"vars (c1;;c2) = vars c1 \<union> vars c2" |
-"vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2" |
-"vars (WHILE b DO c) = vars b \<union> vars c"
+definition "vars_com c = lvars c \<union> rvars c"
 
 instance ..
 
 end
 
+lemma vars_com_simps[simp]:
+  "vars SKIP = {}"
+  "vars (x::=e) = {x} \<union> vars e"
+  "vars (c1;;c2) = vars c1 \<union> vars c2"
+  "vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2"
+  "vars (WHILE b DO c) = vars b \<union> 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 add: finite_avars)
+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(induction c) (simp_all add: finite_avars finite_bvars)
+by(simp add: vars_com_def)
 
 end