# HG changeset patch
# User nipkow
# Date 1223983411 -7200
# Node ID 9bb9791bdc18b62fb6fbab1f81c47b876fe9ca92
# Parent  c269a3045fdf6802b051fdf8af30e93f124eb471
Added liveness analysis

diff -r c269a3045fdf -r 9bb9791bdc18 src/HOL/IMP/Live.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Live.thy	Tue Oct 14 13:23:31 2008 +0200
@@ -0,0 +1,108 @@
+theory Live imports Natural
+begin
+
+text{* Which variables/locations does an expression depend on?
+Any set of variables that completely determine the value of the expression,
+in the worst case all locations: *}
+
+consts Dep :: "((loc \<Rightarrow> 'a) \<Rightarrow> 'b) \<Rightarrow> loc set"
+specification (Dep)
+dep_on: "(\<forall>x\<in>Dep e. s x = t x) \<Longrightarrow> e s = e t"
+by(rule_tac x="%x. UNIV" in exI)(simp add: expand_fun_eq[symmetric])
+
+text{* The following definition of @{const Dep} looks very tempting
+@{prop"Dep e = {a. EX s t. (ALL x. x\<noteq>a \<longrightarrow> s x = t x) \<and> e s \<noteq> e t}"}
+but does not work in case @{text e} depends on an infinite set of variables.
+For example, if @{term"e s"} tests if @{text s} is 0 at infinitely many locations. Then @{term"Dep e"} incorrectly yields the empty set!
+
+If we had a concrete representation of expressions, we would simply write
+a recursive free-variables function.
+*}
+
+primrec L :: "com \<Rightarrow> loc set \<Rightarrow> loc set" where
+"L SKIP A = A" |
+"L (x :== e) A = A-{x} \<union> Dep e" |
+"L (c1; c2) A = (L c1 \<circ> L c2) A" |
+"L (IF b THEN c1 ELSE c2) A = Dep b \<union> L c1 A \<union> L c2 A" |
+"L (WHILE b DO c) A = Dep b \<union> A \<union> L c A"
+
+primrec "kill" :: "com \<Rightarrow> loc set" where
+"kill SKIP = {}" |
+"kill (x :== e) = {x}" |
+"kill (c1; c2) = kill c1 \<union> kill c2" |
+"kill (IF b THEN c1 ELSE c2) = Dep b \<union> kill c1 \<inter>  kill c2" |
+"kill (WHILE b DO c) = {}"
+
+primrec gen :: "com \<Rightarrow> loc set" where
+"gen SKIP = {}" |
+"gen (x :== e) = Dep e" |
+"gen (c1; c2) = gen c1 \<union> (gen c2-kill c1)" |
+"gen (IF b THEN c1 ELSE c2) = Dep b \<union> gen c1 \<union> gen c2" |
+"gen (WHILE b DO c) = Dep b \<union> gen c"
+
+lemma L_gen_kill: "L c A = gen c \<union> (A - kill c)"
+by(induct c arbitrary:A) auto
+
+lemma L_idemp: "L c (L c A) \<subseteq> L c A"
+by(fastsimp simp add:L_gen_kill)
+
+theorem L_sound: "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
+ \<forall>x\<in>A. s' x = t' x"
+proof (induct c arbitrary: A s t s' t')
+  case SKIP then show ?case by auto
+next
+  case (Assign x e) then show ?case
+    by (auto simp:update_def ball_Un dest!: dep_on)
+next
+  case (Semi c1 c2)
+  from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
+    by auto
+  from Semi(5) obtain t'' where t1: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>c2,t''\<rangle> \<longrightarrow>\<^sub>c t'"
+    by auto
+  show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
+next
+  case (Cond b c1 c2)
+  show ?case
+  proof cases
+    assume "b s"
+    hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
+    have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
+    hence t: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
+    show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
+  next
+    assume "\<not> b s"
+    hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
+    have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
+    hence t: "\<langle>c2,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
+    show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
+  qed
+next
+  case (While b c) note IH = this
+  { fix cw
+    have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>cw,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
+          \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
+    proof (induct arbitrary: t A pred:evalc)
+      case WhileFalse
+      have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
+      then have "t' = t" using WhileFalse by auto
+      then show ?case using WhileFalse by auto
+    next
+      case (WhileTrue _ s _ s'' s')
+      have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
+      have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
+      then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
+        using WhileTrue(6,7) by auto
+      note IH1 = IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`]
+      have L1: "\<forall>x\<in>A. s'' x = t'' x" using IH1 WhileTrue(6,8)
+	by(simp  add: ball_Un) (metis)
+      have L2: "\<forall>x\<in>Dep b. s'' x = t'' x"
+	using IH1 WhileTrue(6,8) by (auto simp:L_gen_kill)
+      have L3: "\<forall>x\<in>L c A. s'' x = t'' x"
+	using IH1 L_idemp[of c A] WhileTrue(6,8) by auto
+      have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" using L1 L2 L3 by auto
+      then show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
+    qed auto }
+  from this[OF IH(3) _ IH(4,2)] show ?case by metis
+qed
+
+end
\ No newline at end of file
diff -r c269a3045fdf -r 9bb9791bdc18 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Tue Oct 14 13:01:58 2008 +0200
+++ b/src/HOL/IMP/ROOT.ML	Tue Oct 14 13:23:31 2008 +0200
@@ -6,4 +6,4 @@
 Caveat: HOLCF/IMP depends on HOL/IMP
 *)
 
-use_thys ["Expr", "Transition", "VC", "Examples", "Compiler0", "Compiler"];
+use_thys ["Expr", "Transition", "VC", "Examples", "Compiler0", "Compiler", "Live"];