# HG changeset patch
# User nipkow
# Date 1369014118 -7200
# Node ID c25764d7246ea041dd55f8086706777009c0fac1
# Parent  0e70511cbba91a57584471d44b1f940064732d4f
defined lvars and rvars of commands separately.

diff -r 0e70511cbba9 -r c25764d7246e src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Sun May 19 20:41:19 2013 +0200
+++ b/src/HOL/IMP/Fold.thy	Mon May 20 03:41:58 2013 +0200
@@ -1,6 +1,6 @@
 header "Constant Folding"
 
-theory Fold imports Sem_Equiv begin
+theory Fold imports Sem_Equiv Vars begin
 
 subsection "Simple folding of arithmetic expressions"
 
@@ -30,27 +30,20 @@
 definition
   "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"
 
-primrec lnames :: "com \<Rightarrow> vname set" where
-"lnames SKIP = {}" |
-"lnames (x ::= a) = {x}" |
-"lnames (c1;; c2) = lnames c1 \<union> lnames c2" |
-"lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2" |
-"lnames (WHILE b DO c) = lnames c"
-
 primrec "defs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
 "defs SKIP t = t" |
 "defs (x ::= a) t =
   (case afold a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
 "defs (c1;;c2) t = (defs c2 o defs c1) t" |
 "defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
-"defs (WHILE b DO c) t = t |` (-lnames c)"
+"defs (WHILE b DO c) t = t |` (-lvars c)"
 
 primrec fold where
 "fold SKIP _ = SKIP" |
 "fold (x ::= a) t = (x ::= (afold a t))" |
 "fold (c1;;c2) t = (fold c1 t;; fold c2 (defs c1 t))" |
 "fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" |
-"fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lnames c))"
+"fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lvars c))"
 
 lemma approx_merge:
   "approx t1 s \<or> approx t2 s \<Longrightarrow> approx (merge t1 t2) s"
@@ -78,33 +71,33 @@
 
 
 lemma defs_restrict:
-  "defs c t |` (- lnames c) = t |` (- lnames c)"
+  "defs c t |` (- lvars c) = t |` (- lvars c)"
 proof (induction c arbitrary: t)
   case (Seq c1 c2)
-  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)"
+  hence "defs c1 t |` (- lvars c1) = t |` (- lvars c1)"
     by simp
-  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
-         t |` (- lnames c1) |` (-lnames c2)" by simp
+  hence "defs c1 t |` (- lvars c1) |` (-lvars c2) =
+         t |` (- lvars c1) |` (-lvars c2)" by simp
   moreover
   from Seq
-  have "defs c2 (defs c1 t) |` (- lnames c2) =
-        defs c1 t |` (- lnames c2)"
+  have "defs c2 (defs c1 t) |` (- lvars c2) =
+        defs c1 t |` (- lvars c2)"
     by simp
-  hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) =
-         defs c1 t |` (- lnames c2) |` (- lnames c1)"
+  hence "defs c2 (defs c1 t) |` (- lvars c2) |` (- lvars c1) =
+         defs c1 t |` (- lvars c2) |` (- lvars c1)"
     by simp
   ultimately
   show ?case by (clarsimp simp: Int_commute)
 next
   case (If b c1 c2)
-  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
-  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
-         t |` (- lnames c1) |` (-lnames c2)" by simp
+  hence "defs c1 t |` (- lvars c1) = t |` (- lvars c1)" by simp
+  hence "defs c1 t |` (- lvars c1) |` (-lvars c2) =
+         t |` (- lvars c1) |` (-lvars c2)" by simp
   moreover
   from If
-  have "defs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
-  hence "defs c2 t |` (- lnames c2) |` (-lnames c1) =
-         t |` (- lnames c2) |` (-lnames c1)" by simp
+  have "defs c2 t |` (- lvars c2) = t |` (- lvars c2)" by simp
+  hence "defs c2 t |` (- lvars c2) |` (-lvars c1) =
+         t |` (- lvars c2) |` (-lvars c1)" by simp
   ultimately
   show ?case by (auto simp: Int_commute intro: merge_restrict)
 qed (auto split: aexp.split)
@@ -138,39 +131,39 @@
   case (WhileTrue b s1 c s2 s3)
   hence "approx (defs c t) s2" by simp
   with WhileTrue
-  have "approx (defs c t |` (-lnames c)) s3" by simp
+  have "approx (defs c t |` (-lvars c)) s3" by simp
   thus ?case by (simp add: defs_restrict)
 qed
 
 
 lemma big_step_pres_approx_restrict:
-  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
+  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lvars c)) s \<Longrightarrow> approx (t |` (-lvars c)) s'"
 proof (induction arbitrary: t rule: big_step_induct)
   case Assign
   thus ?case by (clarsimp simp: approx_def)
 next
   case (Seq c1 s1 s2 c2 s3)
-  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1"
+  hence "approx (t |` (-lvars c2) |` (-lvars c1)) s1"
     by (simp add: Int_commute)
-  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
+  hence "approx (t |` (-lvars c2) |` (-lvars c1)) s2"
     by (rule Seq)
-  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2"
+  hence "approx (t |` (-lvars c1) |` (-lvars c2)) s2"
     by (simp add: Int_commute)
-  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3"
+  hence "approx (t |` (-lvars c1) |` (-lvars c2)) s3"
     by (rule Seq)
   thus ?case by simp
 next
   case (IfTrue b s c1 s' c2)
-  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s"
+  hence "approx (t |` (-lvars c2) |` (-lvars c1)) s"
     by (simp add: Int_commute)
-  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'"
+  hence "approx (t |` (-lvars c2) |` (-lvars c1)) s'"
     by (rule IfTrue)
   thus ?case by (simp add: Int_commute)
 next
   case (IfFalse b s c2 s' c1)
-  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s"
+  hence "approx (t |` (-lvars c1) |` (-lvars c2)) s"
     by simp
-  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'"
+  hence "approx (t |` (-lvars c1) |` (-lvars c2)) s'"
     by (rule IfFalse)
   thus ?case by simp
 qed auto
@@ -193,8 +186,8 @@
   thus ?case by (auto intro!: equiv_up_to_if_weak)
 next
   case (While b c)
-  hence "approx (t |` (- lnames c)) \<Turnstile>
-         WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lnames c))"
+  hence "approx (t |` (- lvars c)) \<Turnstile>
+         WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lvars c))"
     by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict)
   thus ?case
     by (auto intro: equiv_up_to_weaken approx_map_le)
@@ -264,7 +257,7 @@
     Bc True \<Rightarrow> bdefs c1 t
   | Bc False \<Rightarrow> bdefs c2 t
   | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
-"bdefs (WHILE b DO c) t = t |` (-lnames c)"
+"bdefs (WHILE b DO c) t = t |` (-lvars c)"
 
 
 primrec fold' where
@@ -277,37 +270,37 @@
   | _ \<Rightarrow> IF bfold b t THEN fold' c1 t ELSE fold' c2 t)" |
 "fold' (WHILE b DO c) t = (case bfold b t of
     Bc False \<Rightarrow> SKIP
-  | _ \<Rightarrow> WHILE bfold b (t |` (-lnames c)) DO fold' c (t |` (-lnames c)))"
+  | _ \<Rightarrow> WHILE bfold b (t |` (-lvars c)) DO fold' c (t |` (-lvars c)))"
 
 
 lemma bdefs_restrict:
-  "bdefs c t |` (- lnames c) = t |` (- lnames c)"
+  "bdefs c t |` (- lvars c) = t |` (- lvars c)"
 proof (induction c arbitrary: t)
   case (Seq c1 c2)
-  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)"
+  hence "bdefs c1 t |` (- lvars c1) = t |` (- lvars c1)"
     by simp
-  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
-         t |` (- lnames c1) |` (-lnames c2)" by simp
+  hence "bdefs c1 t |` (- lvars c1) |` (-lvars c2) =
+         t |` (- lvars c1) |` (-lvars c2)" by simp
   moreover
   from Seq
-  have "bdefs c2 (bdefs c1 t) |` (- lnames c2) =
-        bdefs c1 t |` (- lnames c2)"
+  have "bdefs c2 (bdefs c1 t) |` (- lvars c2) =
+        bdefs c1 t |` (- lvars c2)"
     by simp
-  hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) =
-         bdefs c1 t |` (- lnames c2) |` (- lnames c1)"
+  hence "bdefs c2 (bdefs c1 t) |` (- lvars c2) |` (- lvars c1) =
+         bdefs c1 t |` (- lvars c2) |` (- lvars c1)"
     by simp
   ultimately
   show ?case by (clarsimp simp: Int_commute)
 next
   case (If b c1 c2)
-  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
-  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
-         t |` (- lnames c1) |` (-lnames c2)" by simp
+  hence "bdefs c1 t |` (- lvars c1) = t |` (- lvars c1)" by simp
+  hence "bdefs c1 t |` (- lvars c1) |` (-lvars c2) =
+         t |` (- lvars c1) |` (-lvars c2)" by simp
   moreover
   from If
-  have "bdefs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
-  hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) =
-         t |` (- lnames c2) |` (-lnames c1)" by simp
+  have "bdefs c2 t |` (- lvars c2) = t |` (- lvars c2)" by simp
+  hence "bdefs c2 t |` (- lvars c2) |` (-lvars c1) =
+         t |` (- lvars c2) |` (-lvars c1)" by simp
   ultimately
   show ?case
     by (auto simp: Int_commute intro: merge_restrict
@@ -349,7 +342,7 @@
   case (WhileTrue b s1 c s2 s3)
   hence "approx (bdefs c t) s2" by simp
   with WhileTrue
-  have "approx (bdefs c t |` (- lnames c)) s3"
+  have "approx (bdefs c t |` (- lvars c)) s3"
     by simp
   thus ?case
     by (simp add: bdefs_restrict)
@@ -375,10 +368,10 @@
                  intro: equiv_up_to_trans)
   next
   case (While b c)
-  hence "approx (t |` (- lnames c)) \<Turnstile>
+  hence "approx (t |` (- lvars c)) \<Turnstile>
                    WHILE b DO c \<sim>
-                   WHILE bfold b (t |` (- lnames c))
-                      DO fold' c (t |` (- lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'")
+                   WHILE bfold b (t |` (- lvars c))
+                      DO fold' c (t |` (- lvars c))" (is "_ \<Turnstile> ?W \<sim> ?W'")
     by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict
              simp: bequiv_up_to_def)
   hence "approx t \<Turnstile> ?W \<sim> ?W'"
diff -r 0e70511cbba9 -r c25764d7246e src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Sun May 19 20:41:19 2013 +0200
+++ b/src/HOL/IMP/Live_True.thy	Mon May 20 03:41:58 2013 +0200
@@ -46,7 +46,7 @@
 lemma L_While_X: "X \<subseteq> L (WHILE b DO c) X"
 using L_While_unfold by blast
 
-text{* Disable L WHILE equation and reason only with L WHILE constraints *}
+text{* Disable @{text "L WHILE"} equation and reason only with @{text "L WHILE"} constraints: *}
 declare L.simps(5)[simp del]
 
 
@@ -102,16 +102,14 @@
   with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
 qed
 
-(*declare L.simps(5)[simp]*)
-
 
 subsection "Executability"
 
-lemma L_subset_vars: "L c X \<subseteq> vars c \<union> X"
+lemma L_subset_vars: "L c X \<subseteq> rvars c \<union> X"
 proof(induction c arbitrary: X)
   case (While b c)
-  have "lfp(\<lambda>Y. vars b \<union> X \<union> L c Y) \<subseteq> vars b \<union> vars c \<union> X"
-    using While.IH[of "vars b \<union> vars c \<union> X"]
+  have "lfp(\<lambda>Y. vars b \<union> X \<union> L c Y) \<subseteq> vars b \<union> rvars c \<union> X"
+    using While.IH[of "vars b \<union> rvars c \<union> X"]
     by (auto intro!: lfp_lowerbound)
   thus ?case by (simp add: L.simps(5))
 qed auto
@@ -126,7 +124,7 @@
 assumes "finite X" defines "f == \<lambda>Y. vars b \<union> X \<union> L c Y"
 shows "L (WHILE b DO c) X = while (\<lambda>Y. f Y \<noteq> Y) f {}" (is "_ = ?r")
 proof -
-  let ?V = "vars b \<union> vars c \<union> X"
+  let ?V = "vars b \<union> rvars c \<union> X"
   have "lfp f = ?r"
   proof(rule lfp_while[where C = "?V"])
     show "mono f" by(simp add: f_def mono_union_L)
@@ -175,7 +173,7 @@
 "Lb (x ::= a) X = (if x \<in> X then X - {x} \<union> vars a else X)" |
 "Lb (c\<^isub>1;; c\<^isub>2) X = (Lb c\<^isub>1 \<circ> Lb c\<^isub>2) X" |
 "Lb (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> Lb c\<^isub>1 X \<union> Lb c\<^isub>2 X" |
-"Lb (WHILE b DO c) X = iter (\<lambda>A. vars b \<union> X \<union> Lb c A) 2 {} (vars b \<union> vars c \<union> X)"
+"Lb (WHILE b DO c) X = iter (\<lambda>A. vars b \<union> X \<union> Lb c A) 2 {} (vars b \<union> rvars c \<union> X)"
 
 text{* @{const Lb} (and @{const iter}) is not monotone! *}
 lemma "let w = WHILE Bc False DO (''x'' ::= V ''y'';; ''z'' ::= V ''x'')
@@ -198,8 +196,8 @@
   show ?case
   proof (simp add: L.simps(5), rule lfp_subset_iter[OF mono_union_L])
     show "!!X. ?f X \<subseteq> ?fb X" using While.IH by blast
-    show "lfp ?f \<subseteq> vars b \<union> vars c \<union> X"
-      by (metis (full_types) L.simps(5) L_subset_vars vars_com.simps(5))
+    show "lfp ?f \<subseteq> vars b \<union> rvars c \<union> X"
+      by (metis (full_types) L.simps(5) L_subset_vars rvars.simps(5))
   qed
 next
   case Seq thus ?case by simp (metis (full_types) L_mono monoD subset_trans)
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