--- 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"
--- 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"
--- 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
--- 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
--- 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