author paulson Mon, 31 Mar 2003 12:29:54 +0200 changeset 13888 16f424af58a2 parent 13887 54a0c675c423 child 13889 6676ac2527fa
```--- a/src/HOL/UNITY/ProgressSets.thy	Mon Mar 31 12:29:26 2003 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy	Mon Mar 31 12:29:54 2003 +0200
@@ -141,6 +141,8 @@

subsection {*Progress Sets and the Main Lemma*}
+text{*A progress set satisfies certain closure conditions and is a
+simple way of including the set @{term "wens_set F B"}.*}

constdefs
closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
@@ -249,7 +251,9 @@
by (rule cl_subset_in_lattice [OF cl_subset latt])
qed

-text{*The Lemma proved on page 96*}
+text{*Proved on page 96 of Meier's thesis.  The special case when
+   @{term "T=UNIV"} states that every progress set for the program @{term F}
+   and set @{term B} includes the set @{term "wens_set F B"}.*}
lemma progress_set_lemma:
"[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
@@ -465,6 +469,7 @@

subsection{*Composition Theorems Based on Monotonicity and Commutativity*}

+subsubsection{*Commutativity of @{term "cl L"} and assignment.*}
constdefs
commutes :: "['a program, 'a set, 'a set,  'a set set] => bool"
"commutes F T B L ==
@@ -472,6 +477,7 @@
cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"

+text{*From Meier's thesis, section 4.5.6*}
lemma commutativity1_lemma:
assumes commutes: "commutes F T B L"
and lattice:  "lattice L"
@@ -490,6 +496,7 @@
apply (blast intro: rev_subsetD [OF _ wp_mono])
done

+text{*Version packaged with @{thm progress_set_Union}*}
lemma commutativity1:
and lattice:  "lattice L"
@@ -528,6 +535,7 @@
text{*Thesis, page 109*}

(*FIXME: this proof is an ungodly mess*)
+text{*From Meier's thesis, section 4.5.6*}
lemma commutativity2_lemma:
assumes dcommutes:
"\<forall>act \<in> Acts F.
@@ -570,6 +578,7 @@
done

+text{*Version packaged with @{thm progress_set_Union}*}
lemma commutativity2: