# HG changeset patch
# User nipkow
# Date 1344611825 -7200
# Node ID ff570720ba1c73015f08b34abc2f61b8e868ee66
# Parent  c197b3c3e7fa7326c262d221d53b1ba84bdfa956
Improved complete lattice formalisation - no more index set.

diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Fri Aug 10 17:17:05 2012 +0200
@@ -363,7 +363,7 @@
   have 2: "step' \<top> C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> C)) = c"
     by(simp add: strip_lpfp[OF _ 1])
-  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> C)"
+  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> C)"
   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 _ _])
@@ -371,7 +371,7 @@
       show "\<gamma>\<^isub>c (step' \<top> C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
     qed
   qed
-  with 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c C"
+  with 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
     by (blast intro: mono_gamma_c order_trans)
 qed
 
diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Fri Aug 10 17:17:05 2012 +0200
@@ -143,7 +143,7 @@
   have 2: "step' (top c) C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
     by(simp add: strip_lpfp[OF _ 1])
-  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' (top c) C)"
+  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' (top c) C)"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"
     proof(rule step_preserves_le[OF _ _ `wt C (vars c)` wt_top])
@@ -151,7 +151,7 @@
       show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
     qed
   qed
-  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c C"
+  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
     by (blast intro: mono_gamma_c order_trans)
 qed
 
diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Fri Aug 10 17:17:05 2012 +0200
@@ -238,7 +238,7 @@
   have 2: "step' (top c) C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
     by(simp add: strip_lpfp[OF _ 1])
-  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' (top c) C)"
+  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' (top c) C)"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"
     proof(rule step_preserves_le[OF _ _ `wt C (vars c)` wt_top])
@@ -246,7 +246,7 @@
       show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
     qed
   qed
-  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c C"
+  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
     by (blast intro: mono_gamma_c order_trans)
 qed
 
diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Fri Aug 10 17:17:05 2012 +0200
@@ -356,7 +356,7 @@
     by(rule pfp_wn_pfp[where c=c])
       (simp_all add: 1 mono_step'_top wt_widen_c wt_narrow_c)
   have 3: "strip (\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)) = c" by(simp add: strip_pfp_wn[OF _ 1])
-  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
+  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)) \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
     proof(rule step_preserves_le[OF _ _ _ wt_top])
@@ -365,7 +365,7 @@
       show "wt C (vars c)" using 2 by blast
     qed
   qed
-  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c C"
+  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
     by (blast intro: mono_gamma_c order_trans)
 qed
 
diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Fri Aug 10 17:17:05 2012 +0200
@@ -5,7 +5,7 @@
 theory Abs_Int0_ITP
 imports "~~/src/HOL/ex/Interpretation_with_Defs"
         "~~/src/HOL/Library/While_Combinator"
-        "../Collecting"
+        "Collecting_ITP"
 begin
 
 subsection "Orderings"
diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Fri Aug 10 17:17:05 2012 +0200
@@ -0,0 +1,183 @@
+theory Collecting_ITP
+imports Complete_Lattice_ix "../ACom"
+begin
+
+subsection "Collecting Semantics of Commands"
+
+subsubsection "Annotated commands as a complete lattice"
+
+(* Orderings could also be lifted generically (thus subsuming the
+instantiation for preord and order), but then less_eq_acom would need to
+become a definition, eg less_eq_acom = lift2 less_eq, and then proofs would
+need to unfold this defn first. *)
+
+instantiation acom :: (order) order
+begin
+
+fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
+"(SKIP {S}) \<le> (SKIP {S'}) = (S \<le> S')" |
+"(x ::= e {S}) \<le> (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<le> S')" |
+"(c1;c2) \<le> (c1';c2') = (c1 \<le> c1' \<and> c2 \<le> c2')" |
+"(IF b THEN c1 ELSE c2 {S}) \<le> (IF b' THEN c1' ELSE c2' {S'}) =
+  (b=b' \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')" |
+"({Inv} WHILE b DO c {P}) \<le> ({Inv'} WHILE b' DO c' {P'}) =
+  (b=b' \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')" |
+"less_eq_acom _ _ = False"
+
+lemma SKIP_le: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
+by (cases c) auto
+
+lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
+by (cases c) auto
+
+lemma Seq_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
+by (cases c) auto
+
+lemma If_le: "IF b THEN c1 ELSE c2 {S} \<le> c \<longleftrightarrow>
+  (\<exists>c1' c2' S'. c= IF b THEN c1' ELSE c2' {S'} \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')"
+by (cases c) auto
+
+lemma While_le: "{Inv} WHILE b DO c {P} \<le> w \<longleftrightarrow>
+  (\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')"
+by (cases w) auto
+
+definition less_acom :: "'a acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
+"less_acom x y = (x \<le> y \<and> \<not> y \<le> x)"
+
+instance
+proof
+  case goal1 show ?case by(simp add: less_acom_def)
+next
+  case goal2 thus ?case by (induct x) auto
+next
+  case goal3 thus ?case
+  apply(induct x y arbitrary: z rule: less_eq_acom.induct)
+  apply (auto intro: le_trans simp: SKIP_le Assign_le Seq_le If_le While_le)
+  done
+next
+  case goal4 thus ?case
+  apply(induct x y rule: less_eq_acom.induct)
+  apply (auto intro: le_antisym)
+  done
+qed
+
+end
+
+fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where
+"sub\<^isub>1(c1;c2) = c1" |
+"sub\<^isub>1(IF b THEN c1 ELSE c2 {S}) = c1" |
+"sub\<^isub>1({I} WHILE b DO c {P}) = c"
+
+fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where
+"sub\<^isub>2(c1;c2) = c2" |
+"sub\<^isub>2(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 \<Rightarrow> 'b) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'b acom"
+where
+"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 (sub\<^isub>1 ` M); lift F c2 (sub\<^isub>2 ` M)" |
+"lift F (IF b THEN c1 ELSE c2) M =
+  IF b THEN lift F c1 (sub\<^isub>1 ` M) ELSE lift F c2 (sub\<^isub>2 ` M)
+  {F (post ` M)}" |
+"lift F (WHILE b DO c) M =
+ {F (invar ` M)}
+ WHILE b DO lift F c (sub\<^isub>1 ` M)
+ {F (post ` M)}"
+
+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 Seq from Seq.prems show ?case by(force intro!: Seq.IH)
+  next
+    case If from If.prems show ?case by(force intro!: If.IH)
+  next
+    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 SKIP thus ?case by (force simp:SKIP_le)
+  next
+    case Assign thus ?case by (force simp:Assign_le)
+  next
+    case Seq from Seq.prems show ?case
+      by (force intro!: Seq.IH simp:Seq_le)
+  next
+    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
+  have "strip(lift Inter i A) = i"
+  proof(induction i arbitrary: A)
+    case Seq from Seq.prems show ?case
+      by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH)
+  next
+    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 simp: strip_eq_While)
+  qed auto
+  thus ?case by auto
+qed
+
+lemma le_post: "c \<le> d \<Longrightarrow> post c \<le> post d"
+by(induction c d rule: less_eq_acom.induct) auto
+
+subsubsection "Collecting semantics"
+
+fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
+"step S (SKIP {P}) = (SKIP {S})" |
+"step S (x ::= e {P}) =
+  (x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" |
+"step S (c1; c2) = step S c1; step (post c1) c2" |
+"step S (IF b THEN c1 ELSE c2 {P}) =
+   IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. \<not> bval b s} c2
+   {post c1 \<union> post c2}" |
+"step S ({Inv} WHILE b DO c {P}) =
+  {S \<union> post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
+
+definition CS :: "com \<Rightarrow> state set acom" where
+"CS c = lfp (step UNIV) c"
+
+lemma mono2_step: "c1 \<le> c2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 c1 \<le> step S2 c2"
+proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct)
+  case 2 thus ?case by fastforce
+next
+  case 3 thus ?case by(simp add: le_post)
+next
+  case 4 thus ?case by(simp add: subset_iff)(metis le_post set_mp)+
+next
+  case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp)
+qed auto
+
+lemma mono_step: "mono (step S)"
+by(blast intro: monoI mono2_step)
+
+lemma strip_step: "strip(step S c) = strip c"
+by (induction c arbitrary: S) auto
+
+lemma lfp_cs_unfold: "lfp (step S) c = step S (lfp (step S) c)"
+apply(rule lfp_unfold[OF _  mono_step])
+apply(simp add: strip_step)
+done
+
+lemma CS_unfold: "CS c = step UNIV (CS c)"
+by (metis CS_def lfp_cs_unfold)
+
+lemma strip_CS[simp]: "strip(CS c) = c"
+by(simp add: CS_def index_lfp[simplified])
+
+end
diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy	Fri Aug 10 17:17:05 2012 +0200
@@ -0,0 +1,61 @@
+(* Author: Tobias Nipkow *)
+
+header "Abstract Interpretation"
+
+theory Complete_Lattice_ix
+imports Main
+begin
+
+subsection "Complete Lattice (indexed)"
+
+text{* A complete lattice is an ordered type where every set of elements has
+a greatest lower (and thus also a leats upper) bound. Sets are the
+prototypical complete lattice where the greatest lower bound is
+intersection. Sometimes that set of all elements of a type is not a complete
+lattice although all elements of the same shape form a complete lattice, for
+example lists of the same length, where the list elements come from a
+complete lattice. We will have exactly this situation with annotated
+commands. This theory introduces a slightly generalised version of complete
+lattices where elements have an ``index'' and only the set of elements with
+the same index form a complete lattice; the type as a whole is a disjoint
+union of complete lattices. Because sets are not types, this requires a
+special treatment. *}
+
+locale Complete_Lattice_ix =
+fixes L :: "'i \<Rightarrow> 'a::order set"
+and Glb :: "'i \<Rightarrow> 'a set \<Rightarrow> 'a"
+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 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'i \<Rightarrow> 'a" where
+"lfp f i = Glb i {a : L i. f a \<le> a}"
+
+lemma index_lfp: "lfp f i : L i"
+by(auto simp: lfp_def intro: Glb_in_L)
+
+lemma lfp_lowerbound:
+  "\<lbrakk> a : L i;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp f i \<le> a"
+by (auto simp add: lfp_def intro: Glb_lower)
+
+lemma lfp_greatest:
+  "\<lbrakk> a : L i;  \<And>u. \<lbrakk> u : L i; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp f i"
+by (auto simp add: lfp_def intro: Glb_greatest)
+
+lemma lfp_unfold: assumes "\<And>x i. f x : L i \<longleftrightarrow> x : L i"
+and mono: "mono f" shows "lfp f i = f (lfp f i)"
+proof-
+  note assms(1)[simp] index_lfp[simp]
+  have 1: "f (lfp f i) \<le> lfp f i"
+    apply(rule lfp_greatest)
+    apply simp
+    by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
+  have "lfp f i \<le> f (lfp f i)"
+    by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)
+  with 1 show ?thesis by(blast intro: order_antisym)
+qed
+
+end
+
+end
diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/HOL/IMP/Collecting.thy	Fri Aug 10 17:17:05 2012 +0200
@@ -1,5 +1,5 @@
 theory Collecting
-imports Complete_Lattice_ix ACom
+imports Complete_Lattice ACom
 begin
 
 subsection "Collecting Semantics of Commands"
@@ -89,7 +89,7 @@
  WHILE b DO lift F c (sub\<^isub>1 ` M)
  {F (post ` M)}"
 
-interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
+interpretation Complete_Lattice "{C. strip C = c}" "lift Inter c" for c
 proof
   case goal1
   have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
@@ -104,31 +104,26 @@
 next
   case goal2
   thus ?case
-  proof(induction b arbitrary: i A)
+  proof(simp, induction b arbitrary: c A)
     case SKIP thus ?case by (force simp:SKIP_le)
   next
     case Assign thus ?case by (force simp:Assign_le)
   next
-    case Seq from Seq.prems show ?case
-      by (force intro!: Seq.IH simp:Seq_le)
+    case Seq from Seq.prems show ?case by(force intro!: Seq.IH simp:Seq_le)
   next
     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)
+    case While from While.prems show ?case by(fastforce simp: While_le intro: While.IH)
   qed
 next
   case goal3
-  have "strip(lift Inter i A) = i"
-  proof(induction i arbitrary: A)
-    case Seq from Seq.prems show ?case
-      by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH)
+  have "strip(lift Inter c A) = c"
+  proof(induction c arbitrary: A)
+    case Seq from Seq.prems show ?case by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH)
   next
-    case If from If.prems show ?case
-      by (fastforce intro!: If.IH simp: strip_eq_If)
+    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 simp: strip_eq_While)
+    case While from While.prems show ?case by(fastforce intro: While.IH simp: strip_eq_While)
   qed auto
   thus ?case by auto
 qed
@@ -150,7 +145,7 @@
   {S \<union> post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
 
 definition CS :: "com \<Rightarrow> state set acom" where
-"CS c = lfp (step UNIV) c"
+"CS c = lfp c (step UNIV)"
 
 lemma mono2_step: "c1 \<le> c2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 c1 \<le> step S2 c2"
 proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct)
@@ -169,7 +164,7 @@
 lemma strip_step: "strip(step S c) = strip c"
 by (induction c arbitrary: S) auto
 
-lemma lfp_cs_unfold: "lfp (step S) c = step S (lfp (step S) c)"
+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
diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Complete_Lattice.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Complete_Lattice.thy	Fri Aug 10 17:17:05 2012 +0200
@@ -0,0 +1,42 @@
+theory Complete_Lattice
+imports Main
+begin
+
+locale Complete_Lattice =
+fixes L :: "'a::order set" and Glb :: "'a set \<Rightarrow> 'a"
+assumes Glb_lower: "A \<subseteq> L \<Longrightarrow> a \<in> A \<Longrightarrow> Glb A \<le> a"
+and Glb_greatest: "b : L \<Longrightarrow> \<forall>a\<in>A. b \<le> a \<Longrightarrow> b \<le> Glb A"
+and Glb_in_L: "A \<subseteq> L \<Longrightarrow> Glb A : L"
+begin
+
+definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
+"lfp f = Glb {a : L. f a \<le> a}"
+
+lemma index_lfp: "lfp f : L"
+by(auto simp: lfp_def intro: Glb_in_L)
+
+lemma lfp_lowerbound:
+  "\<lbrakk> a : L;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp f \<le> a"
+by (auto simp add: lfp_def intro: Glb_lower)
+
+lemma lfp_greatest:
+  "\<lbrakk> a : L;  \<And>u. \<lbrakk> u : L; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp f"
+by (auto simp add: lfp_def intro: Glb_greatest)
+
+lemma lfp_unfold: assumes "\<And>x. f x : L \<longleftrightarrow> x : L"
+and mono: "mono f" shows "lfp f = f (lfp f)"
+proof-
+  note assms(1)[simp] index_lfp[simp]
+  have 1: "f (lfp f) \<le> lfp f"
+    apply(rule lfp_greatest)
+    apply simp
+    by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
+  have "lfp f \<le> f (lfp f)"
+    by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)
+  with 1 show ?thesis by(blast intro: order_antisym)
+qed
+
+end
+
+end
+
diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Complete_Lattice_ix.thy
--- a/src/HOL/IMP/Complete_Lattice_ix.thy	Thu Aug 09 22:31:04 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-header "Abstract Interpretation"
-
-theory Complete_Lattice_ix
-imports Main
-begin
-
-subsection "Complete Lattice (indexed)"
-
-text{* A complete lattice is an ordered type where every set of elements has
-a greatest lower (and thus also a leats upper) bound. Sets are the
-prototypical complete lattice where the greatest lower bound is
-intersection. Sometimes that set of all elements of a type is not a complete
-lattice although all elements of the same shape form a complete lattice, for
-example lists of the same length, where the list elements come from a
-complete lattice. We will have exactly this situation with annotated
-commands. This theory introduces a slightly generalised version of complete
-lattices where elements have an ``index'' and only the set of elements with
-the same index form a complete lattice; the type as a whole is a disjoint
-union of complete lattices. Because sets are not types, this requires a
-special treatment. *}
-
-locale Complete_Lattice_ix =
-fixes L :: "'i \<Rightarrow> 'a::order set"
-and Glb :: "'i \<Rightarrow> 'a set \<Rightarrow> 'a"
-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 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'i \<Rightarrow> 'a" where
-"lfp f i = Glb i {a : L i. f a \<le> a}"
-
-lemma index_lfp: "lfp f i : L i"
-by(auto simp: lfp_def intro: Glb_in_L)
-
-lemma lfp_lowerbound:
-  "\<lbrakk> a : L i;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp f i \<le> a"
-by (auto simp add: lfp_def intro: Glb_lower)
-
-lemma lfp_greatest:
-  "\<lbrakk> a : L i;  \<And>u. \<lbrakk> u : L i; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp f i"
-by (auto simp add: lfp_def intro: Glb_greatest)
-
-lemma lfp_unfold: assumes "\<And>x i. f x : L i \<longleftrightarrow> x : L i"
-and mono: "mono f" shows "lfp f i = f (lfp f i)"
-proof-
-  note assms(1)[simp] index_lfp[simp]
-  have 1: "f (lfp f i) \<le> lfp f i"
-    apply(rule lfp_greatest)
-    apply simp
-    by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
-  have "lfp f i \<le> f (lfp f i)"
-    by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)
-  with 1 show ?thesis by(blast intro: order_antisym)
-qed
-
-end
-
-end