--- a/src/HOL/IMP/Live.thy Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/IMP/Live.thy Tue Aug 13 16:25:47 2013 +0200
@@ -10,8 +10,8 @@
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
"L SKIP X = X" |
"L (x ::= a) X = vars a \<union> (X - {x})" |
-"L (c\<^isub>1;; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
-"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
+"L (c\<^sub>1;; c\<^sub>2) X = L c\<^sub>1 (L c\<^sub>2 X)" |
+"L (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = vars b \<union> L c\<^sub>1 X \<union> L c\<^sub>2 X" |
"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
value "show (L (''y'' ::= V ''z'';; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
@@ -21,15 +21,15 @@
fun "kill" :: "com \<Rightarrow> vname set" where
"kill SKIP = {}" |
"kill (x ::= a) = {x}" |
-"kill (c\<^isub>1;; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
-"kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
+"kill (c\<^sub>1;; c\<^sub>2) = kill c\<^sub>1 \<union> kill c\<^sub>2" |
+"kill (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = kill c\<^sub>1 \<inter> kill c\<^sub>2" |
"kill (WHILE b DO c) = {}"
fun gen :: "com \<Rightarrow> vname set" where
"gen SKIP = {}" |
"gen (x ::= a) = vars a" |
-"gen (c\<^isub>1;; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
-"gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
+"gen (c\<^sub>1;; c\<^sub>2) = gen c\<^sub>1 \<union> (gen c\<^sub>2 - kill c\<^sub>1)" |
+"gen (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = vars b \<union> gen c\<^sub>1 \<union> gen c\<^sub>2" |
"gen (WHILE b DO c) = vars b \<union> gen c"
lemma L_gen_kill: "L c X = gen c \<union> (X - kill c)"
@@ -110,8 +110,8 @@
fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
"bury SKIP X = SKIP" |
"bury (x ::= a) X = (if x \<in> X then x ::= a else SKIP)" |
-"bury (c\<^isub>1;; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X);; bury c\<^isub>2 X)" |
-"bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" |
+"bury (c\<^sub>1;; c\<^sub>2) X = (bury c\<^sub>1 (L c\<^sub>2 X);; bury c\<^sub>2 X)" |
+"bury (IF b THEN c\<^sub>1 ELSE c\<^sub>2) X = IF b THEN bury c\<^sub>1 X ELSE bury c\<^sub>2 X" |
"bury (WHILE b DO c) X = WHILE b DO bury c (L (WHILE b DO c) X)"
text{* We could prove the analogous lemma to @{thm[source]L_correct}, and the
@@ -182,8 +182,8 @@
lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
by (cases c) auto
-lemma Seq_bury[simp]: "bc\<^isub>1;;bc\<^isub>2 = bury c X \<longleftrightarrow>
- (EX c\<^isub>1 c\<^isub>2. c = c\<^isub>1;;c\<^isub>2 & bc\<^isub>2 = bury c\<^isub>2 X & bc\<^isub>1 = bury c\<^isub>1 (L c\<^isub>2 X))"
+lemma Seq_bury[simp]: "bc\<^sub>1;;bc\<^sub>2 = bury c X \<longleftrightarrow>
+ (EX c\<^sub>1 c\<^sub>2. c = c\<^sub>1;;c\<^sub>2 & bc\<^sub>2 = bury c\<^sub>2 X & bc\<^sub>1 = bury c\<^sub>1 (L c\<^sub>2 X))"
by (cases c) auto
lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \<longleftrightarrow>