1.1 --- a/src/HOL/IMP/Abs_Int0.thy	Thu Dec 15 21:46:52 2011 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Fri Dec 16 12:00:59 2011 +0100
     1.3 @@ -103,7 +103,7 @@
     1.4    have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     1.5      by(simp add: strip_lpfpc[OF _ 1])
     1.6    have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     1.7 -  proof(rule lfp_lowerbound[OF 3])
     1.8 +  proof(rule lfp_lowerbound[simplified,OF 3])
     1.9      show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    1.10      proof(rule step_preserves_le[OF _ _ 3])
    1.11        show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp

     2.1 --- a/src/HOL/IMP/Abs_Int0_fun.thy	Thu Dec 15 21:46:52 2011 +0100
     2.2 +++ b/src/HOL/IMP/Abs_Int0_fun.thy	Fri Dec 16 12:00:59 2011 +0100
     2.3 @@ -358,7 +358,7 @@
     2.4    have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     2.5      by(simp add: strip_lpfpc[OF _ 1])
     2.6    have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     2.7 -  proof(rule lfp_lowerbound[OF 3])
     2.8 +  proof(rule lfp_lowerbound[simplified,OF 3])
     2.9      show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    2.10      proof(rule step_preserves_le[OF _ _ 3])
    2.11        show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp

     3.1 --- a/src/HOL/IMP/Abs_Int1.thy	Thu Dec 15 21:46:52 2011 +0100
     3.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Fri Dec 16 12:00:59 2011 +0100
     3.3 @@ -218,7 +218,7 @@
     3.4    have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     3.5      by(simp add: strip_lpfpc[OF _ 1])
     3.6    have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     3.7 -  proof(rule lfp_lowerbound[OF 3])
     3.8 +  proof(rule lfp_lowerbound[simplified,OF 3])
     3.9      show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    3.10      proof(rule step_preserves_le[OF _ _ 3])
    3.11        show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp

     4.1 --- a/src/HOL/IMP/Abs_Int2.thy	Thu Dec 15 21:46:52 2011 +0100
     4.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Fri Dec 16 12:00:59 2011 +0100
     4.3 @@ -193,7 +193,7 @@
     4.4    have 2: "step' \<top> c' \<sqsubseteq> c'" .
     4.5    have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1])
     4.6    have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     4.7 -  proof(rule lfp_lowerbound[OF 3])
     4.8 +  proof(rule lfp_lowerbound[simplified,OF 3])
     4.9      show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
    4.10      proof(rule step_preserves_le[OF _ _ 3])
    4.11        show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp

     5.1 --- a/src/HOL/IMP/Collecting.thy	Thu Dec 15 21:46:52 2011 +0100
     5.2 +++ b/src/HOL/IMP/Collecting.thy	Fri Dec 16 12:00:59 2011 +0100
     5.3 @@ -63,53 +63,74 @@
     5.4  
     5.5  end
     5.6  
     5.7 +fun sub1 :: "'a acom \<Rightarrow> 'a acom" where
     5.8 +"sub1(c1;c2) = c1" |
     5.9 +"sub1(IF b THEN c1 ELSE c2 {S}) = c1" |
    5.10 +"sub1({I} WHILE b DO c {P}) = c"
    5.11 +
    5.12 +fun sub2 :: "'a acom \<Rightarrow> 'a acom" where
    5.13 +"sub2(c1;c2) = c2" |
    5.14 +"sub2(IF b THEN c1 ELSE c2 {S}) = c2"
    5.15 +
    5.16 +fun invar :: "'a acom \<Rightarrow> 'a" where
    5.17 +"invar({I} WHILE b DO c {P}) = I"
    5.18 +
    5.19  fun lift :: "('a set set \<Rightarrow> 'a set) \<Rightarrow> com \<Rightarrow> 'a set acom set \<Rightarrow> 'a set acom"
    5.20  where
    5.21 -"lift F com.SKIP M = (SKIP {F {P. SKIP {P} : M}})" |
    5.22 -"lift F (x ::= a) M = (x ::= a {F {P. x::=a {P} : M}})" |
    5.23 +"lift F com.SKIP M = (SKIP {F (post ` M)})" |
    5.24 +"lift F (x ::= a) M = (x ::= a {F (post ` M)})" |
    5.25  "lift F (c1;c2) M =
    5.26 -  (lift F c1 {c1. \<exists>c2. c1;c2 : M}); (lift F c2 {c2. \<exists>c1. c1;c2 : M})" |
    5.27 +  lift F c1 (sub1 ` M); lift F c2 (sub2 ` M)" |
    5.28  "lift F (IF b THEN c1 ELSE c2) M =
    5.29 -  IF b THEN lift F c1 {c1. \<exists>c2 P. IF b THEN c1 ELSE c2 {P} : M}
    5.30 -       ELSE lift F c2 {c2. \<exists>c1 P. IF b THEN c1 ELSE c2 {P} : M}
    5.31 -  {F {P. \<exists>c1 c2. IF b THEN c1 ELSE c2 {P} : M}}" |
    5.32 +  IF b THEN lift F c1 (sub1 ` M) ELSE lift F c2 (sub2 ` M)
    5.33 +  {F (post ` M)}" |
    5.34  "lift F (WHILE b DO c) M =
    5.35 - {F {I. \<exists>c P. {I} WHILE b DO c {P} : M}}
    5.36 - WHILE b DO lift F c {c. \<exists>I P. {I} WHILE b DO c {P} : M}
    5.37 - {F {P. \<exists>I c. {I} WHILE b DO c {P} : M}}"
    5.38 + {F (invar ` M)}
    5.39 + WHILE b DO lift F c (sub1 ` M)
    5.40 + {F (post ` M)}"
    5.41  
    5.42 -interpretation Complete_Lattice_ix strip "lift Inter"
    5.43 +interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
    5.44  proof
    5.45    case goal1
    5.46    have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
    5.47    proof(induction a arbitrary: A)
    5.48 -    case Semi from Semi.prems show ?case by(fastforce intro!: Semi.IH)
    5.49 +    case Semi from Semi.prems show ?case by(force intro!: Semi.IH)
    5.50    next
    5.51 -    case If from If.prems show ?case by(fastforce intro!: If.IH)
    5.52 +    case If from If.prems show ?case by(force intro!: If.IH)
    5.53    next
    5.54 -    case While from While.prems show ?case by(fastforce intro!: While.IH)
    5.55 -  qed auto
    5.56 +    case While from While.prems show ?case by(force intro!: While.IH)
    5.57 +  qed force+
    5.58    with goal1 show ?case by auto
    5.59  next
    5.60    case goal2
    5.61    thus ?case
    5.62    proof(induction b arbitrary: i A)
    5.63 -    case Semi from Semi.prems show ?case by (fastforce intro!: Semi.IH)
    5.64 +    case SKIP thus ?case by (force simp:SKIP_le)
    5.65    next
    5.66 -    case If from If.prems show ?case by (fastforce intro!: If.IH)
    5.67 +    case Assign thus ?case by (force simp:Assign_le)
    5.68    next
    5.69 -    case While from While.prems show ?case by(fastforce intro: While.IH)
    5.70 -  qed fastforce+
    5.71 +    case Semi from Semi.prems show ?case
    5.72 +      by (force intro!: Semi.IH simp:Semi_le)
    5.73 +  next
    5.74 +    case If from If.prems show ?case by (force simp: If_le intro!: If.IH)
    5.75 +  next
    5.76 +    case While from While.prems show ?case
    5.77 +      by(fastforce simp: While_le intro: While.IH)
    5.78 +  qed
    5.79  next
    5.80    case goal3
    5.81 -  thus ?case
    5.82 +  have "strip(lift Inter i A) = i"
    5.83    proof(induction i arbitrary: A)
    5.84 -    case Semi from Semi.prems show ?case by (fastforce intro!: Semi.IH)
    5.85 +    case Semi from Semi.prems show ?case
    5.86 +      by (fastforce simp: strip_eq_Semi subset_iff intro!: Semi.IH)
    5.87    next
    5.88 -    case If from If.prems show ?case by (fastforce intro!: If.IH)
    5.89 +    case If from If.prems show ?case
    5.90 +      by (fastforce intro!: If.IH simp: strip_eq_If)
    5.91    next
    5.92 -    case While from While.prems show ?case by(fastforce intro: While.IH)
    5.93 +    case While from While.prems show ?case
    5.94 +      by(fastforce intro: While.IH simp: strip_eq_While)
    5.95    qed auto
    5.96 +  thus ?case by auto
    5.97  qed
    5.98  
    5.99  lemma le_post: "c \<le> d \<Longrightarrow> post c \<le> post d"
   5.100 @@ -169,12 +190,15 @@
   5.101  lemma strip_step: "strip(step S c) = strip c"
   5.102  by (induction c arbitrary: S) auto
   5.103  
   5.104 -lemmas lfp_cs_unfold = lfp_unfold[OF strip_step mono_step]
   5.105 +lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))"
   5.106 +apply(rule lfp_unfold[OF _  mono_step])
   5.107 +apply(simp add: strip_step)
   5.108 +done
   5.109  
   5.110  lemma CS_unfold: "CS S c = step S (CS S c)"
   5.111  by (metis CS_def lfp_cs_unfold)
   5.112  
   5.113  lemma strip_CS[simp]: "strip(CS S c) = c"
   5.114 -by(simp add: CS_def)
   5.115 +by(simp add: CS_def index_lfp[simplified])
   5.116  
   5.117  end

     6.1 --- a/src/HOL/IMP/Complete_Lattice_ix.thy	Thu Dec 15 21:46:52 2011 +0100
     6.2 +++ b/src/HOL/IMP/Complete_Lattice_ix.thy	Fri Dec 16 12:00:59 2011 +0100
     6.3 @@ -16,34 +16,34 @@
     6.4  special treatment. *}
     6.5  
     6.6  locale Complete_Lattice_ix =
     6.7 -fixes ix :: "'a::order \<Rightarrow> 'i"
     6.8 +fixes L :: "'i \<Rightarrow> 'a::order set"
     6.9  and Glb :: "'i \<Rightarrow> 'a set \<Rightarrow> 'a"
    6.10 -assumes Glb_lower: "\<forall>a\<in>A. ix a = i \<Longrightarrow> a \<in> A \<Longrightarrow> (Glb i A) \<le> a"
    6.11 -and Glb_greatest: "\<forall>a\<in>A. b \<le> a \<Longrightarrow> ix b = i \<Longrightarrow> b \<le> (Glb i A)"
    6.12 -and ix_Glb: "\<forall>a\<in>A. ix a = i \<Longrightarrow> ix(Glb i A) = i"
    6.13 +assumes Glb_lower: "A \<subseteq> L i \<Longrightarrow> a \<in> A \<Longrightarrow> (Glb i A) \<le> a"
    6.14 +and Glb_greatest: "b : L i \<Longrightarrow> \<forall>a\<in>A. b \<le> a \<Longrightarrow> b \<le> (Glb i A)"
    6.15 +and Glb_in_L: "A \<subseteq> L i \<Longrightarrow> Glb i A : L i"
    6.16  begin
    6.17  
    6.18  definition lfp :: "'i \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
    6.19 -"lfp i f = Glb i {a. ix a = i \<and> f a \<le> a}"
    6.20 +"lfp i f = Glb i {a : L i. f a \<le> a}"
    6.21  
    6.22 -lemma index_lfp[simp]: "ix(lfp i f) = i"
    6.23 -by(simp add: lfp_def ix_Glb)
    6.24 +lemma index_lfp: "lfp i f : L i"
    6.25 +by(auto simp: lfp_def intro: Glb_in_L)
    6.26  
    6.27  lemma lfp_lowerbound:
    6.28 -  "\<lbrakk> ix a = i;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp i f \<le> a"
    6.29 +  "\<lbrakk> a : L i;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp i f \<le> a"
    6.30  by (auto simp add: lfp_def intro: Glb_lower)
    6.31  
    6.32  lemma lfp_greatest:
    6.33 -  "\<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"
    6.34 +  "\<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"
    6.35  by (auto simp add: lfp_def intro: Glb_greatest)
    6.36  
    6.37 -lemma lfp_unfold: assumes "\<And>x. ix(f x) = ix x"
    6.38 +lemma lfp_unfold: assumes "\<And>x i. f x : L i \<longleftrightarrow> x : L i"
    6.39  and mono: "mono f" shows "lfp i f = f (lfp i f)"
    6.40  proof-
    6.41 -  note assms(1)[simp]
    6.42 +  note assms(1)[simp] index_lfp[simp]
    6.43    have 1: "f (lfp i f) \<le> lfp i f"
    6.44      apply(rule lfp_greatest)
    6.45 -    apply(simp)
    6.46 +    apply simp
    6.47      by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
    6.48    have "lfp i f \<le> f (lfp i f)"
    6.49      by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)