# HG changeset patch
# User nipkow
# Date 1324033270 -3600
# Node ID c9ae2bc95fadc7992904087dc07186ebbf8bbfff
# Parent  b619242b0439e8c81ff6dd7d4a87644f281ace78# Parent  02dd9319dcb7bd23eba5fca8b2e05aa919098cbd
merged

diff -r b619242b0439 -r c9ae2bc95fad src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Fri Dec 16 11:02:55 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Fri Dec 16 12:01:10 2011 +0100
@@ -103,7 +103,7 @@
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     by(simp add: strip_lpfpc[OF _ 1])
   have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
-  proof(rule lfp_lowerbound[OF 3])
+  proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
       show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
diff -r b619242b0439 -r c9ae2bc95fad src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Fri Dec 16 11:02:55 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Fri Dec 16 12:01:10 2011 +0100
@@ -358,7 +358,7 @@
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     by(simp add: strip_lpfpc[OF _ 1])
   have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
-  proof(rule lfp_lowerbound[OF 3])
+  proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
       show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
diff -r b619242b0439 -r c9ae2bc95fad src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Fri Dec 16 11:02:55 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Fri Dec 16 12:01:10 2011 +0100
@@ -218,7 +218,7 @@
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     by(simp add: strip_lpfpc[OF _ 1])
   have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
-  proof(rule lfp_lowerbound[OF 3])
+  proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
       show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
diff -r b619242b0439 -r c9ae2bc95fad src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Fri Dec 16 11:02:55 2011 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Fri Dec 16 12:01:10 2011 +0100
@@ -193,7 +193,7 @@
   have 2: "step' \<top> c' \<sqsubseteq> c'" .
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1])
   have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
-  proof(rule lfp_lowerbound[OF 3])
+  proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
       show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp
diff -r b619242b0439 -r c9ae2bc95fad src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Fri Dec 16 11:02:55 2011 +0100
+++ b/src/HOL/IMP/Collecting.thy	Fri Dec 16 12:01:10 2011 +0100
@@ -63,53 +63,74 @@
 
 end
 
+fun sub1 :: "'a acom \<Rightarrow> 'a acom" where
+"sub1(c1;c2) = c1" |
+"sub1(IF b THEN c1 ELSE c2 {S}) = c1" |
+"sub1({I} WHILE b DO c {P}) = c"
+
+fun sub2 :: "'a acom \<Rightarrow> 'a acom" where
+"sub2(c1;c2) = c2" |
+"sub2(IF b THEN c1 ELSE c2 {S}) = c2"
+
+fun invar :: "'a acom \<Rightarrow> 'a" where
+"invar({I} WHILE b DO c {P}) = I"
+
 fun lift :: "('a set set \<Rightarrow> 'a set) \<Rightarrow> com \<Rightarrow> 'a set acom set \<Rightarrow> 'a set acom"
 where
-"lift F com.SKIP M = (SKIP {F {P. SKIP {P} : M}})" |
-"lift F (x ::= a) M = (x ::= a {F {P. x::=a {P} : M}})" |
+"lift F com.SKIP M = (SKIP {F (post ` M)})" |
+"lift F (x ::= a) M = (x ::= a {F (post ` M)})" |
 "lift F (c1;c2) M =
-  (lift F c1 {c1. \<exists>c2. c1;c2 : M}); (lift F c2 {c2. \<exists>c1. c1;c2 : M})" |
+  lift F c1 (sub1 ` M); lift F c2 (sub2 ` M)" |
 "lift F (IF b THEN c1 ELSE c2) M =
-  IF b THEN lift F c1 {c1. \<exists>c2 P. IF b THEN c1 ELSE c2 {P} : M}
-       ELSE lift F c2 {c2. \<exists>c1 P. IF b THEN c1 ELSE c2 {P} : M}
-  {F {P. \<exists>c1 c2. IF b THEN c1 ELSE c2 {P} : M}}" |
+  IF b THEN lift F c1 (sub1 ` M) ELSE lift F c2 (sub2 ` M)
+  {F (post ` M)}" |
 "lift F (WHILE b DO c) M =
- {F {I. \<exists>c P. {I} WHILE b DO c {P} : M}}
- WHILE b DO lift F c {c. \<exists>I P. {I} WHILE b DO c {P} : M}
- {F {P. \<exists>I c. {I} WHILE b DO c {P} : M}}"
+ {F (invar ` M)}
+ WHILE b DO lift F c (sub1 ` M)
+ {F (post ` M)}"
 
-interpretation Complete_Lattice_ix strip "lift Inter"
+interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
 proof
   case goal1
   have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
   proof(induction a arbitrary: A)
-    case Semi from Semi.prems show ?case by(fastforce intro!: Semi.IH)
+    case Semi from Semi.prems show ?case by(force intro!: Semi.IH)
   next
-    case If from If.prems show ?case by(fastforce intro!: If.IH)
+    case If from If.prems show ?case by(force intro!: If.IH)
   next
-    case While from While.prems show ?case by(fastforce intro!: While.IH)
-  qed auto
+    case While from While.prems show ?case by(force intro!: While.IH)
+  qed force+
   with goal1 show ?case by auto
 next
   case goal2
   thus ?case
   proof(induction b arbitrary: i A)
-    case Semi from Semi.prems show ?case by (fastforce intro!: Semi.IH)
+    case SKIP thus ?case by (force simp:SKIP_le)
+  next
+    case Assign thus ?case by (force simp:Assign_le)
   next
-    case If from If.prems show ?case by (fastforce intro!: If.IH)
+    case Semi from Semi.prems show ?case
+      by (force intro!: Semi.IH simp:Semi_le)
   next
-    case While from While.prems show ?case by(fastforce intro: While.IH)
-  qed fastforce+
+    case If from If.prems show ?case by (force simp: If_le intro!: If.IH)
+  next
+    case While from While.prems show ?case
+      by(fastforce simp: While_le intro: While.IH)
+  qed
 next
   case goal3
-  thus ?case
+  have "strip(lift Inter i A) = i"
   proof(induction i arbitrary: A)
-    case Semi from Semi.prems show ?case by (fastforce intro!: Semi.IH)
+    case Semi from Semi.prems show ?case
+      by (fastforce simp: strip_eq_Semi subset_iff intro!: Semi.IH)
   next
-    case If from If.prems show ?case by (fastforce intro!: If.IH)
+    case If from If.prems show ?case
+      by (fastforce intro!: If.IH simp: strip_eq_If)
   next
-    case While from While.prems show ?case by(fastforce intro: While.IH)
+    case While from While.prems show ?case
+      by(fastforce intro: While.IH simp: strip_eq_While)
   qed auto
+  thus ?case by auto
 qed
 
 lemma le_post: "c \<le> d \<Longrightarrow> post c \<le> post d"
@@ -169,12 +190,15 @@
 lemma strip_step: "strip(step S c) = strip c"
 by (induction c arbitrary: S) auto
 
-lemmas lfp_cs_unfold = lfp_unfold[OF strip_step mono_step]
+lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))"
+apply(rule lfp_unfold[OF _  mono_step])
+apply(simp add: strip_step)
+done
 
 lemma CS_unfold: "CS S c = step S (CS S c)"
 by (metis CS_def lfp_cs_unfold)
 
 lemma strip_CS[simp]: "strip(CS S c) = c"
-by(simp add: CS_def)
+by(simp add: CS_def index_lfp[simplified])
 
 end
diff -r b619242b0439 -r c9ae2bc95fad src/HOL/IMP/Complete_Lattice_ix.thy
--- a/src/HOL/IMP/Complete_Lattice_ix.thy	Fri Dec 16 11:02:55 2011 +0100
+++ b/src/HOL/IMP/Complete_Lattice_ix.thy	Fri Dec 16 12:01:10 2011 +0100
@@ -16,34 +16,34 @@
 special treatment. *}
 
 locale Complete_Lattice_ix =
-fixes ix :: "'a::order \<Rightarrow> 'i"
+fixes L :: "'i \<Rightarrow> 'a::order set"
 and Glb :: "'i \<Rightarrow> 'a set \<Rightarrow> 'a"
-assumes Glb_lower: "\<forall>a\<in>A. ix a = i \<Longrightarrow> a \<in> A \<Longrightarrow> (Glb i A) \<le> a"
-and Glb_greatest: "\<forall>a\<in>A. b \<le> a \<Longrightarrow> ix b = i \<Longrightarrow> b \<le> (Glb i A)"
-and ix_Glb: "\<forall>a\<in>A. ix a = i \<Longrightarrow> ix(Glb i A) = i"
+assumes Glb_lower: "A \<subseteq> L i \<Longrightarrow> a \<in> A \<Longrightarrow> (Glb i A) \<le> a"
+and Glb_greatest: "b : L i \<Longrightarrow> \<forall>a\<in>A. b \<le> a \<Longrightarrow> b \<le> (Glb i A)"
+and Glb_in_L: "A \<subseteq> L i \<Longrightarrow> Glb i A : L i"
 begin
 
 definition lfp :: "'i \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
-"lfp i f = Glb i {a. ix a = i \<and> f a \<le> a}"
+"lfp i f = Glb i {a : L i. f a \<le> a}"
 
-lemma index_lfp[simp]: "ix(lfp i f) = i"
-by(simp add: lfp_def ix_Glb)
+lemma index_lfp: "lfp i f : L i"
+by(auto simp: lfp_def intro: Glb_in_L)
 
 lemma lfp_lowerbound:
-  "\<lbrakk> ix a = i;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp i f \<le> a"
+  "\<lbrakk> a : L i;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp i f \<le> a"
 by (auto simp add: lfp_def intro: Glb_lower)
 
 lemma lfp_greatest:
-  "\<lbrakk> ix a = i;  \<And>u. \<lbrakk>ix u = i; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp i f"
+  "\<lbrakk> a : L i;  \<And>u. \<lbrakk> u : L i; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp i f"
 by (auto simp add: lfp_def intro: Glb_greatest)
 
-lemma lfp_unfold: assumes "\<And>x. ix(f x) = ix x"
+lemma lfp_unfold: assumes "\<And>x i. f x : L i \<longleftrightarrow> x : L i"
 and mono: "mono f" shows "lfp i f = f (lfp i f)"
 proof-
-  note assms(1)[simp]
+  note assms(1)[simp] index_lfp[simp]
   have 1: "f (lfp i f) \<le> lfp i f"
     apply(rule lfp_greatest)
-    apply(simp)
+    apply simp
     by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
   have "lfp i f \<le> f (lfp i f)"
     by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)