# HG changeset patch
# User nipkow
# Date 1352112051 -3600
# Node ID e48de041030714f56e76e79b9c0682aff7c1e658
# Parent  eb7f574d03032af996526a6871bfb753f2bab48b
tuned

diff -r eb7f574d0303 -r e48de0410307 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Sun Nov 04 18:41:27 2012 +0100
+++ b/src/HOL/IMP/Live.thy	Mon Nov 05 11:40:51 2012 +0100
@@ -66,14 +66,14 @@
   case (IfTrue b s c1 s' c2)
   hence "s = t on vars b" "s = t on L c1 X" by auto
   from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
-  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
+  from IfTrue.IH[OF `s = t on L c1 X`] obtain t' where
     "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
   thus ?case using `bval b t` by auto
 next
   case (IfFalse b s c2 s' c1)
   hence "s = t on vars b" "s = t on L c2 X" by auto
   from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
-  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
+  from IfFalse.IH[OF `s = t on L c2 X`] obtain t' where
     "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
   thus ?case using `~bval b t` by auto
 next
@@ -100,7 +100,7 @@
 text{* Burying assignments to dead variables: *}
 fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
 "bury SKIP X = SKIP" |
-"bury (x ::= a) X = (if x:X then x::= a else 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 (WHILE b DO c) X = WHILE b DO bury c (vars b \<union> X \<union> L c X)"
@@ -130,14 +130,14 @@
   case (IfTrue b s c1 s' c2)
   hence "s = t on vars b" "s = t on L c1 X" by auto
   from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
-  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
+  from IfTrue.IH[OF `s = t on L c1 X`] obtain t' where
     "(bury c1 X, t) \<Rightarrow> t'" "s' =t' on X" by auto
   thus ?case using `bval b t` by auto
 next
   case (IfFalse b s c2 s' c1)
   hence "s = t on vars b" "s = t on L c2 X" by auto
   from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
-  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
+  from IfFalse.IH[OF `s = t on L c2 X`] obtain t' where
     "(bury c2 X, t) \<Rightarrow> t'" "s' = t' on X" by auto
   thus ?case using `~bval b t` by auto
 next
diff -r eb7f574d0303 -r e48de0410307 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Sun Nov 04 18:41:27 2012 +0100
+++ b/src/HOL/IMP/Live_True.thy	Mon Nov 05 11:40:51 2012 +0100
@@ -8,10 +8,10 @@
 
 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
 "L SKIP X = X" |
-"L (x ::= a) X = (if x:X then X-{x} \<union> vars a else X)" |
+"L (x ::= a) X = (if x \<in> X then X - {x} \<union> vars a else X)" |
 "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> 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 (WHILE b DO c) X = lfp(%Y. vars b \<union> X \<union> L c Y)"
+"L (WHILE b DO c) X = lfp(\<lambda>Y. vars b \<union> X \<union> L c Y)"
 
 lemma L_mono: "mono (L c)"
 proof-
@@ -30,7 +30,7 @@
 qed
 
 lemma mono_union_L:
-  "mono (%Y. X \<union> L c Y)"
+  "mono (\<lambda>Y. X \<union> L c Y)"
 by (metis (no_types) L_mono mono_def order_eq_iff set_eq_subset sup_mono)
 
 lemma L_While_unfold:
@@ -59,16 +59,16 @@
   show ?case using t12 t23 s3t3 by auto
 next
   case (IfTrue b s c1 s' c2)
-  hence "s = t on vars b" "s = t on L c1 X" by auto
+  hence "s = t on vars b" and "s = t on L c1 X" by auto
   from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
-  from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
+  from IfTrue.IH[OF `s = t on L c1 X`] obtain t' where
     "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
   thus ?case using `bval b t` by auto
 next
   case (IfFalse b s c2 s' c1)
   hence "s = t on vars b" "s = t on L c2 X" by auto
   from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
-  from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
+  from IfFalse.IH[OF `s = t on L c2 X`] obtain t' where
     "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
   thus ?case using `~bval b t` by auto
 next
@@ -90,6 +90,7 @@
   with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
 qed
 
+
 subsection "Executability"
 
 instantiation com :: vars
@@ -109,7 +110,7 @@
 lemma L_subset_vars: "L c X \<subseteq> vars c \<union> X"
 proof(induction c arbitrary: X)
   case (While b c)
-  have "lfp(%Y. vars b \<union> X \<union> L c Y) \<subseteq> vars b \<union> vars c \<union> X"
+  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"]
     by (auto intro!: lfp_lowerbound)
   thus ?case by simp
@@ -169,7 +170,7 @@
 by eval
 
 
-subsection "Approximating WHILE"
+subsection "Limiting the number of iterations"
 
 text{* The final parameter is the default value: *}
 
@@ -182,11 +183,16 @@
 
 fun Lb :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
 "Lb SKIP X = X" |
-"Lb (x ::= a) X = (if x:X then X-{x} \<union> vars a else X)" |
+"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)"
 
+text{* @{const Lb} (and @{const iter}) is not monotone! *}
+lemma "let w = WHILE Bc False DO (''x'' ::= V ''y''; ''z'' ::= V ''x'')
+  in \<not> (Lb w {''z''} \<subseteq> Lb w {''y'',''z''})"
+by eval
+
 lemma lfp_subset_iter:
   "\<lbrakk> mono f; !!X. f X \<subseteq> f' X; lfp f \<subseteq> D \<rbrakk> \<Longrightarrow> lfp f \<subseteq> iter f' n A D"
 proof(induction n arbitrary: A)