src/HOL/IMP/ACom.thy
changeset 46157 3d518b508bbb
parent 46068 b9d4ec0f79ac
child 46225 d0a2c4a80a00
--- a/src/HOL/IMP/ACom.thy	Sat Jan 07 20:44:23 2012 +0100
+++ b/src/HOL/IMP/ACom.thy	Mon Jan 09 11:41:38 2012 +0100
@@ -84,6 +84,14 @@
 lemma strip_anno[simp]: "strip (anno a c) = c"
 by(induct c) simp_all
 
+lemma strip_eq_SKIP:
+  "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})"
+by (cases c) simp_all
+
+lemma strip_eq_Assign:
+  "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
+by (cases c) simp_all
+
 lemma strip_eq_Semi:
   "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
 by (cases c) simp_all