# HG changeset patch
# User nipkow
# Date 1365748063 -7200
# Node ID c0af8bbc58256a2120c9c3702161bf4ea0426a55
# Parent  1ce319118d59ed36a0f764cd2c97fa1c660125f5
reduced duplication

diff -r 1ce319118d59 -r c0af8bbc5825 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Thu Apr 11 16:58:54 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Fri Apr 12 08:27:43 2013 +0200
@@ -18,29 +18,6 @@
 
 end
 
-instantiation com :: vars
-begin
-
-fun vars_com :: "com \<Rightarrow> vname set" where
-"vars com.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"
-
-instance ..
-
-end
-
-lemma finite_avars: "finite(vars(a::aexp))"
-by(induction a) simp_all
-
-lemma finite_bvars: "finite(vars(b::bexp))"
-by(induction b) (simp_all add: finite_avars)
-
-lemma finite_cvars: "finite(vars(c::com))"
-by(induction c) (simp_all add: finite_avars finite_bvars)
-
 
 subsection "Backward Analysis of Expressions"
 
diff -r 1ce319118d59 -r c0af8bbc5825 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Thu Apr 11 16:58:54 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Fri Apr 12 08:27:43 2013 +0200
@@ -6,30 +6,6 @@
 
 subsubsection "Set-based lattices"
 
-instantiation com :: vars
-begin
-
-fun vars_com :: "com \<Rightarrow> vname set" where
-"vars com.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"
-
-instance ..
-
-end
-
-
-lemma finite_avars: "finite(vars(a::aexp))"
-by(induction a) simp_all
-
-lemma finite_bvars: "finite(vars(b::bexp))"
-by(induction b) (simp_all add: finite_avars)
-
-lemma finite_cvars: "finite(vars(c::com))"
-by(induction c) (simp_all add: finite_avars finite_bvars)
-
 
 class L =
 fixes L :: "vname set \<Rightarrow> 'a set"
diff -r 1ce319118d59 -r c0af8bbc5825 src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Thu Apr 11 16:58:54 2013 +0200
+++ b/src/HOL/IMP/Collecting_Examples.thy	Fri Apr 12 08:27:43 2013 +0200
@@ -9,14 +9,6 @@
 lemma insert_code [code]:  "insert x (set xs) = set (x#xs)"
 by simp
 
-text{* Collect variables in acom: *}
-fun cvars :: "'a acom \<Rightarrow> vname set" where
-"cvars (SKIP {P})= {}" |
-"cvars (x::=e {P}) = {x} \<union> vars e" |
-"cvars (c1;c2) = cvars c1 \<union> cvars c2" |
-"cvars (IF b THEN {P1} c1 ELSE {P2} c2 {Q}) = vars b \<union> cvars c1 \<union> cvars c2" |
-"cvars ({I} WHILE b DO {P} c {Q}) = vars b \<union> cvars c"
-
 text{* Compensate for the fact that sets may now have duplicates: *}
 definition compact :: "'a set \<Rightarrow> 'a set" where
 "compact X = X"
@@ -24,7 +16,7 @@
 lemma [code]: "compact(set xs) = set(remdups xs)"
 by(simp add: compact_def)
 
-definition "vars_acom = compact o cvars"
+definition "vars_acom = compact o vars o strip"
 
 text{* In order to display commands annotated with state sets, states must be
 translated into a printable format as sets of variable-state pairs, for the
diff -r 1ce319118d59 -r c0af8bbc5825 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Thu Apr 11 16:58:54 2013 +0200
+++ b/src/HOL/IMP/Live_True.thy	Fri Apr 12 08:27:43 2013 +0200
@@ -107,20 +107,6 @@
 
 subsection "Executability"
 
-instantiation com :: vars
-begin
-
-fun vars_com :: "com \<Rightarrow> vname set" where
-"vars SKIP = {}" |
-"vars (x::=e) = vars e" |
-"vars (c\<^isub>1; c\<^isub>2) = vars c\<^isub>1 \<union> vars c\<^isub>2" |
-"vars (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> vars c\<^isub>1 \<union> vars c\<^isub>2" |
-"vars (WHILE b DO c) = vars b \<union> vars c"
-
-instance ..
-
-end
-
 lemma L_subset_vars: "L c X \<subseteq> vars c \<union> X"
 proof(induction c arbitrary: X)
   case (While b c)
@@ -130,16 +116,6 @@
   thus ?case by (simp add: L.simps(5))
 qed auto
 
-lemma afinite[simp]: "finite(vars(a::aexp))"
-by (induction a) auto
-
-lemma bfinite[simp]: "finite(vars(b::bexp))"
-by (induction b) auto
-
-lemma cfinite[simp]: "finite(vars(c::com))"
-by (induction c) auto
-
-
 text{* Make @{const L} executable by replacing @{const lfp} with the @{const
 while} combinator from theory @{theory While_Combinator}. The @{const while}
 combinator obeys the recursion equation
diff -r 1ce319118d59 -r c0af8bbc5825 src/HOL/IMP/Vars.thy
--- a/src/HOL/IMP/Vars.thy	Thu Apr 11 16:58:54 2013 +0200
+++ b/src/HOL/IMP/Vars.thy	Fri Apr 12 08:27:43 2013 +0200
@@ -2,7 +2,7 @@
 
 header "Definite Initialization Analysis"
 
-theory Vars imports BExp
+theory Vars imports Com
 begin
 
 subsection "The Variables in an Expression"
@@ -67,4 +67,29 @@
   thus ?case by simp
 qed simp_all
 
+
+instantiation com :: vars
+begin
+
+fun vars_com :: "com \<Rightarrow> vname set" where
+"vars com.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"
+
+instance ..
+
 end
+
+
+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)
+
+lemma finite_cvars[simp]: "finite(vars(c::com))"
+by(induction c) (simp_all add: finite_avars finite_bvars)
+
+end