--- a/src/HOL/UNITY/Comp/Progress.thy Mon Mar 17 17:37:20 2003 +0100
+++ b/src/HOL/UNITY/Comp/Progress.thy Mon Mar 17 17:37:48 2003 +0100
@@ -88,11 +88,11 @@
apply (rule leadsTo_UN [OF atLeast_leadsTo])
done
-text{*Result (4.39): Applying the Union Theorem*}
+text{*Result (4.39): Applying the leadsTo-Join Theorem*}
theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)"
apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
apply simp
-apply (rule_tac T = "atLeast 0" in leadsTo_Union)
+apply (rule_tac T = "atLeast 0" in leadsTo_Join)
apply (simp add: awp_iff FF_def, constrains)
apply (simp add: awp_iff GG_def wens_set_FF, constrains)
apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp)
--- a/src/HOL/UNITY/ProgressSets.thy Mon Mar 17 17:37:20 2003 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy Mon Mar 17 17:37:48 2003 +0100
@@ -18,6 +18,8 @@
theory ProgressSets = Transformers:
+subsection {*Complete Lattices and the Operator @{term cl}*}
+
constdefs
lattice :: "'a set set => bool"
--{*Meier calls them closure sets, but they are just complete lattices*}
@@ -97,8 +99,7 @@
lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))"
apply (rule equalityI)
- prefer 2
- apply (simp add: cl_def, blast)
+ prefer 2 apply (simp add: cl_def, blast)
apply (rule cl_least)
apply (blast intro: UN_in_lattice cl_in_lattice)
apply (blast intro: subset_cl [THEN subsetD])
@@ -122,6 +123,8 @@
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
+subsection {*Progress Sets and the Main Lemma*}
+
constdefs
closed :: "['a program, 'a set, 'a set, 'a set set] => bool"
"closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
@@ -136,93 +139,102 @@
==> T \<inter> (B \<union> wp act M) \<in> L"
by (simp add: closed_def)
+text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
+and @{term m} by @{term X}. *}
+
+text{*Part of the proof of the claim at the bottom of page 97. It's
+proved separately because the argument requires a generalization over
+all @{term "act \<in> Acts F"}.*}
lemma lattice_awp_lemma:
- assumes tmc: "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
- and qsm: "q \<subseteq> m" --{*holds in inductive step*}
+ assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
+ and BsubX: "B \<subseteq> X" --{*holds in inductive step*}
and latt: "lattice C"
- and tc: "T \<in> C"
- and qc: "q \<in> C"
- and clos: "closed F T q C"
- shows "T \<inter> (q \<union> awp F (m \<union> cl C (T\<inter>r))) \<in> C"
+ and TC: "T \<in> C"
+ and BC: "B \<in> C"
+ and clos: "closed F T B C"
+ shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C"
apply (simp del: INT_simps add: awp_def INT_extend_simps)
apply (rule INT_in_lattice [OF latt])
apply (erule closedD [OF clos])
-apply (simp add: subset_trans [OF qsm Un_upper1])
-apply (subgoal_tac "T \<inter> (m \<union> cl C (T\<inter>r)) = (T\<inter>m) \<union> cl C (T\<inter>r)")
- prefer 2 apply (blast intro: tc rev_subsetD [OF _ cl_least])
+apply (simp add: subset_trans [OF BsubX Un_upper1])
+apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
+ prefer 2 apply (blast intro: TC rev_subsetD [OF _ cl_least])
apply (erule ssubst)
-apply (blast intro: Un_in_lattice latt cl_in_lattice tmc)
+apply (blast intro: Un_in_lattice latt cl_in_lattice TXC)
done
+text{*Remainder of the proof of the claim at the bottom of page 97.*}
lemma lattice_lemma:
- assumes tmc: "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
- and qsm: "q \<subseteq> m" --{*holds in inductive step*}
+ assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
+ and BsubX: "B \<subseteq> X" --{*holds in inductive step*}
and act: "act \<in> Acts F"
and latt: "lattice C"
- and tc: "T \<in> C"
- and qc: "q \<in> C"
- and clos: "closed F T q C"
- shows "T \<inter> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)) \<union> m) \<in> C"
-apply (subgoal_tac "T \<inter> (q \<union> wp act m) \<in> C")
- prefer 2 apply (simp add: closedD [OF clos] act qsm tmc)
+ and TC: "T \<in> C"
+ and BC: "B \<in> C"
+ and clos: "closed F T B C"
+ shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C"
+apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C")
+ prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
apply (drule Int_in_lattice
- [OF _ lattice_awp_lemma [OF tmc qsm latt tc qc clos, of r]
+ [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
latt])
apply (subgoal_tac
- "T \<inter> (q \<union> wp act m) \<inter> (T \<inter> (q \<union> awp F (m \<union> cl C (T\<inter>r)))) =
- T \<inter> (q \<union> wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)))")
+ "T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) =
+ T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))")
prefer 2 apply blast
apply simp
-apply (drule Un_in_lattice [OF _ tmc latt])
+apply (drule Un_in_lattice [OF _ TXC latt])
apply (subgoal_tac
- "T \<inter> (q \<union> wp act m \<inter> awp F (m \<union> cl C (T\<inter>r))) \<union> T\<inter>m =
- T \<inter> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>r)) \<union> m)")
- prefer 2 apply (blast intro: qsm [THEN subsetD], simp)
+ "T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X =
+ T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)")
+ apply simp
+apply (blast intro: BsubX [THEN subsetD])
done
+text{*Induction step for the main lemma*}
lemma progress_induction_step:
- assumes tmc: "T\<inter>m \<in> C" --{*induction hypothesis in theorem below*}
+ assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
and act: "act \<in> Acts F"
- and mwens: "m \<in> wens_set F q"
+ and Xwens: "X \<in> wens_set F B"
and latt: "lattice C"
- and tc: "T \<in> C"
- and qc: "q \<in> C"
- and clos: "closed F T q C"
+ and TC: "T \<in> C"
+ and BC: "B \<in> C"
+ and clos: "closed F T B C"
and Fstable: "F \<in> stable T"
- shows "T \<inter> wens F act m \<in> C"
+ shows "T \<inter> wens F act X \<in> C"
proof -
-from mwens have qsm: "q \<subseteq> m"
- by (rule wens_set_imp_subset)
-let ?r = "wens F act m"
-have "?r \<subseteq> (wp act m \<inter> awp F (m\<union>?r)) \<union> m"
- by (simp add: wens_unfold [symmetric])
-then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (m\<union>?r)) \<union> m)"
- by blast
-then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (T \<inter> (m\<union>?r))) \<union> m)"
- by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast)
-then have "T\<inter>?r \<subseteq> T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m)"
- by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
-then have "cl C (T\<inter>?r) \<subseteq>
- cl C (T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m))"
- by (rule cl_mono)
-then have "cl C (T\<inter>?r) \<subseteq>
- T \<inter> ((wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m)"
- by (simp add: cl_ident lattice_lemma [OF tmc qsm act latt tc qc clos])
-then have "cl C (T\<inter>?r) \<subseteq> (wp act m \<inter> awp F (m \<union> cl C (T\<inter>?r))) \<union> m"
- by blast
-then have "cl C (T\<inter>?r) \<subseteq> ?r"
- by (blast intro!: subset_wens)
-then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
- by (simp add: Int_subset_iff cl_ident tc
- subset_trans [OF cl_mono [OF Int_lower1]])
-show ?thesis
- by (rule cl_subset_in_lattice [OF cl_subset latt])
+ from Xwens have BsubX: "B \<subseteq> X"
+ by (rule wens_set_imp_subset)
+ let ?r = "wens F act X"
+ have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X"
+ by (simp add: wens_unfold [symmetric])
+ then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)"
+ by blast
+ then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)"
+ by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast)
+ then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
+ by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
+ then have "cl C (T\<inter>?r) \<subseteq>
+ cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))"
+ by (rule cl_mono)
+ then have "cl C (T\<inter>?r) \<subseteq>
+ T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)"
+ by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
+ then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X"
+ by blast
+ then have "cl C (T\<inter>?r) \<subseteq> ?r"
+ by (blast intro!: subset_wens)
+ then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
+ by (simp add: Int_subset_iff cl_ident TC
+ subset_trans [OF cl_mono [OF Int_lower1]])
+ show ?thesis
+ by (rule cl_subset_in_lattice [OF cl_subset latt])
qed
-
+text{*The Lemma proved on page 96*}
lemma progress_set_lemma:
- "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
+ "[|C \<in> progress_set F T B; r \<in> wens_set F B|] ==> T\<inter>r \<in> C"
apply (simp add: progress_set_def, clarify)
apply (erule wens_set.induct)
txt{*Base*}
@@ -235,4 +247,49 @@
apply (blast intro: UN_in_lattice)
done
+
+subsection {*The Progress Set Union Theorem*}
+
+lemma closed_mono:
+ assumes BB': "B \<subseteq> B'"
+ and TBwp: "T \<inter> (B \<union> wp act M) \<in> C"
+ and B'C: "B' \<in> C"
+ and TC: "T \<in> C"
+ and latt: "lattice C"
+ shows "T \<inter> (B' \<union> wp act M) \<in> C"
+proof -
+ from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C"
+ by (simp add: Int_Un_distrib)
+ then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C"
+ by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt)
+ show ?thesis
+ by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC],
+ blast intro: BB' [THEN subsetD])
+qed
+
+
+lemma progress_set_mono:
+ assumes BB': "B \<subseteq> B'"
+ shows
+ "[| B' \<in> C; C \<in> progress_set F T B|]
+ ==> C \<in> progress_set F T B'"
+by (simp add: progress_set_def closed_def closed_mono [OF BB']
+ subset_trans [OF BB'])
+
+theorem progress_set_Union:
+ assumes prog: "C \<in> progress_set F T B"
+ and BB': "B \<subseteq> B'"
+ and B'C: "B' \<in> C"
+ and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
+ and leadsTo: "F \<in> A leadsTo B'"
+ shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
+apply (insert prog)
+apply (rule leadsTo_Join [OF leadsTo])
+ apply (force simp add: progress_set_def awp_iff_stable [symmetric])
+apply (simp add: awp_iff_constrains)
+apply (drule progress_set_mono [OF BB' B'C])
+apply (blast intro: progress_set_lemma Gco constrains_weaken_L
+ BB' [THEN subsetD])
+done
+
end
--- a/src/HOL/UNITY/Transformers.thy Mon Mar 17 17:37:20 2003 +0100
+++ b/src/HOL/UNITY/Transformers.thy Mon Mar 17 17:37:48 2003 +0100
@@ -3,11 +3,15 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2003 University of Cambridge
-Predicate Transformers from
+Predicate Transformers. From
David Meier and Beverly Sanders,
Composing Leads-to Properties
Theoretical Computer Science 243:1-2 (2000), 339-361.
+
+ David Meier,
+ Progress Properties in Program Refinement and Parallel Composition
+ Swiss Federal Institute of Technology Zurich (1997)
*)
header{*Predicate Transformers*}
@@ -274,10 +278,10 @@
apply (blast intro: wens_set.Union)
done
-theorem leadsTo_Union:
- assumes awpF: "T-B \<subseteq> awp F T"
+theorem leadsTo_Join:
+ assumes leadsTo: "F \<in> A leadsTo B"
+ and awpF: "T-B \<subseteq> awp F T"
and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
- and leadsTo: "F \<in> A leadsTo B"
shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE])
apply (rule wens_Union [THEN bexE])
@@ -472,10 +476,10 @@
text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}
-lemma fp_leadsTo_Union:
+lemma fp_leadsTo_Join:
"[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B"
-apply (rule leadsTo_Union, assumption)
- apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast, assumption)
+apply (rule leadsTo_Join, assumption, blast)
+apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast)
done
end