(* Title: HOL/UNITY/ProgressSets.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2003 University of Cambridge
Progress Sets. 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{*Progress Sets*}
theory ProgressSets imports Transformers begin
subsection {*Complete Lattices and the Operator @{term cl}*}
definition lattice :: "'a set set => bool" where
--{*Meier calls them closure sets, but they are just complete lattices*}
"lattice L ==
(\M. M \ L --> \M \ L) & (\M. M \ L --> \M \ L)"
definition cl :: "['a set set, 'a set] => 'a set" where
--{*short for ``closure''*}
"cl L r == \{x. x\L & r \ x}"
lemma UNIV_in_lattice: "lattice L ==> UNIV \ L"
by (force simp add: lattice_def)
lemma empty_in_lattice: "lattice L ==> {} \ L"
by (force simp add: lattice_def)
lemma Union_in_lattice: "[|M \ L; lattice L|] ==> \M \ L"
by (simp add: lattice_def)
lemma Inter_in_lattice: "[|M \ L; lattice L|] ==> \M \ L"
by (simp add: lattice_def)
lemma UN_in_lattice:
"[|lattice L; !!i. i\I ==> r i \ L|] ==> (\i\I. r i) \ L"
apply (unfold SUP_def)
apply (blast intro: Union_in_lattice)
done
lemma INT_in_lattice:
"[|lattice L; !!i. i\I ==> r i \ L|] ==> (\i\I. r i) \ L"
apply (unfold INF_def)
apply (blast intro: Inter_in_lattice)
done
lemma Un_in_lattice: "[|x\L; y\L; lattice L|] ==> x\y \ L"
using Union_in_lattice [of "{x, y}" L] by simp
lemma Int_in_lattice: "[|x\L; y\L; lattice L|] ==> x\y \ L"
using Inter_in_lattice [of "{x, y}" L] by simp
lemma lattice_stable: "lattice {X. F \ stable X}"
by (simp add: lattice_def stable_def constrains_def, blast)
text{*The next three results state that @{term "cl L r"} is the minimal
element of @{term L} that includes @{term r}.*}
lemma cl_in_lattice: "lattice L ==> cl L r \ L"
apply (simp add: lattice_def cl_def)
apply (erule conjE)
apply (drule spec, erule mp, blast)
done
lemma cl_least: "[|c\L; r\c|] ==> cl L r \ c"
by (force simp add: cl_def)
text{*The next three lemmas constitute assertion (4.61)*}
lemma cl_mono: "r \ r' ==> cl L r \ cl L r'"
by (simp add: cl_def, blast)
lemma subset_cl: "r \ cl L r"
by (simp add: cl_def le_Inf_iff)
text{*A reformulation of @{thm subset_cl}*}
lemma clI: "x \ r ==> x \ cl L r"
by (simp add: cl_def, blast)
text{*A reformulation of @{thm cl_least}*}
lemma clD: "[|c \ cl L r; B \ L; r \ B|] ==> c \ B"
by (force simp add: cl_def)
lemma cl_UN_subset: "(\i\I. cl L (r i)) \ cl L (\i\I. r i)"
by (simp add: cl_def, blast)
lemma cl_Un: "lattice L ==> cl L (r\s) = cl L r \ cl L s"
apply (rule equalityI)
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])
done
lemma cl_UN: "lattice L ==> cl L (\i\I. r i) = (\i\I. cl L (r i))"
apply (rule equalityI)
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])
done
lemma cl_Int_subset: "cl L (r\s) \ cl L r \ cl L s"
by (simp add: cl_def, blast)
lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
by (simp add: cl_def, blast)
lemma cl_ident: "r\L ==> cl L r = r"
by (force simp add: cl_def)
lemma cl_empty [simp]: "lattice L ==> cl L {} = {}"
by (simp add: cl_ident empty_in_lattice)
lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
by (simp add: cl_ident UNIV_in_lattice)
text{*Assertion (4.62)*}
lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\L)"
apply (rule iffI)
apply (erule subst)
apply (erule cl_in_lattice)
apply (erule cl_ident)
done
lemma cl_subset_in_lattice: "[|cl L r \ r; lattice L|] ==> r\L"
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
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"}.*}
definition closed :: "['a program, 'a set, 'a set, 'a set set] => bool" where
"closed F T B L == \M. \act \ Acts F. B\M & T\M \ L -->
T \ (B \ wp act M) \ L"
definition progress_set :: "['a program, 'a set, 'a set] => 'a set set set" where
"progress_set F T B ==
{L. lattice L & B \ L & T \ L & closed F T B L}"
lemma closedD:
"[|closed F T B L; act \ Acts F; B\M; T\M \ L|]
==> T \ (B \ wp act M) \ 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 \ Acts F"}.*}
lemma lattice_awp_lemma:
assumes TXC: "T\X \ C" --{*induction hypothesis in theorem below*}
and BsubX: "B \ X" --{*holds in inductive step*}
and latt: "lattice C"
and TC: "T \ C"
and BC: "B \ C"
and clos: "closed F T B C"
shows "T \ (B \ awp F (X \ cl C (T\r))) \ 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 BsubX Un_upper1])
apply (subgoal_tac "T \ (X \ cl C (T\r)) = (T\X) \ cl C (T\r)")
prefer 2 apply (blast intro: TC clD)
apply (erule ssubst)
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 TXC: "T\X \ C" --{*induction hypothesis in theorem below*}
and BsubX: "B \ X" --{*holds in inductive step*}
and act: "act \ Acts F"
and latt: "lattice C"
and TC: "T \ C"
and BC: "B \ C"
and clos: "closed F T B C"
shows "T \ (wp act X \ awp F (X \ cl C (T\r)) \ X) \ C"
apply (subgoal_tac "T \ (B \ wp act X) \ C")
prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
apply (drule Int_in_lattice
[OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
latt])
apply (subgoal_tac
"T \ (B \ wp act X) \ (T \ (B \ awp F (X \ cl C (T\r)))) =
T \ (B \ wp act X \ awp F (X \ cl C (T\r)))")
prefer 2 apply blast
apply simp
apply (drule Un_in_lattice [OF _ TXC latt])
apply (subgoal_tac
"T \ (B \ wp act X \ awp F (X \ cl C (T\r))) \ T\X =
T \ (wp act X \ awp F (X \ cl C (T\r)) \ X)")
apply simp
apply (blast intro: BsubX [THEN subsetD])
done
text{*Induction step for the main lemma*}
lemma progress_induction_step:
assumes TXC: "T\X \ C" --{*induction hypothesis in theorem below*}
and act: "act \ Acts F"
and Xwens: "X \ wens_set F B"
and latt: "lattice C"
and TC: "T \ C"
and BC: "B \ C"
and clos: "closed F T B C"
and Fstable: "F \ stable T"
shows "T \ wens F act X \ C"
proof -
from Xwens have BsubX: "B \ X"
by (rule wens_set_imp_subset)
let ?r = "wens F act X"
have "?r \ (wp act X \ awp F (X\?r)) \ X"
by (simp add: wens_unfold [symmetric])
then have "T\?r \ T \ ((wp act X \ awp F (X\?r)) \ X)"
by blast
then have "T\?r \ T \ ((wp act X \ awp F (T \ (X\?r))) \ X)"
by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast)
then have "T\?r \ T \ ((wp act X \ awp F (X \ cl C (T\?r))) \ X)"
by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
then have "cl C (T\?r) \
cl C (T \ ((wp act X \ awp F (X \ cl C (T\?r))) \ X))"
by (rule cl_mono)
then have "cl C (T\?r) \
T \ ((wp act X \ awp F (X \ cl C (T\?r))) \ X)"
by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
then have "cl C (T\?r) \ (wp act X \ awp F (X \ cl C (T\?r))) \ X"
by blast
then have "cl C (T\?r) \ ?r"
by (blast intro!: subset_wens)
then have cl_subset: "cl C (T\?r) \ T\?r"
by (simp add: 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{*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 \ progress_set F T B; r \ wens_set F B; F \ stable T|] ==> T\r \ C"
apply (simp add: progress_set_def, clarify)
apply (erule wens_set.induct)
txt{*Base*}
apply (simp add: Int_in_lattice)
txt{*The difficult @{term wens} case*}
apply (simp add: progress_induction_step)
txt{*Disjunctive case*}
apply (subgoal_tac "(\U\W. T \ U) \ C")
apply simp
apply (blast intro: UN_in_lattice)
done
subsection {*The Progress Set Union Theorem*}
lemma closed_mono:
assumes BB': "B \ B'"
and TBwp: "T \ (B \ wp act M) \ C"
and B'C: "B' \ C"
and TC: "T \ C"
and latt: "lattice C"
shows "T \ (B' \ wp act M) \ C"
proof -
from TBwp have "(T\B) \ (T \ wp act M) \ C"
by (simp add: Int_Un_distrib)
then have TBBC: "(T\B') \ ((T\B) \ (T \ wp act M)) \ 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 \ B'"
shows
"[| B' \ C; C \ progress_set F T B|]
==> C \ 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 leadsTo: "F \ A leadsTo B'"
and prog: "C \ progress_set F T B"
and Fstable: "F \ stable T"
and BB': "B \ B'"
and B'C: "B' \ C"
and Gco: "!!X. X\C ==> G \ X-B co X"
shows "F\G \ T\A leadsTo B'"
apply (insert prog Fstable)
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
subsection {*Some Progress Sets*}
lemma UNIV_in_progress_set: "UNIV \ progress_set F T B"
by (simp add: progress_set_def lattice_def closed_def)
subsubsection {*Lattices and Relations*}
text{*From Meier's thesis, section 4.5.3*}
definition relcl :: "'a set set => ('a * 'a) set" where
-- {*Derived relation from a lattice*}
"relcl L == {(x,y). y \ cl L {x}}"
definition latticeof :: "('a * 'a) set => 'a set set" where
-- {*Derived lattice from a relation: the set of upwards-closed sets*}
"latticeof r == {X. \s t. s \ X & (s,t) \ r --> t \ X}"
lemma relcl_refl: "(a,a) \ relcl L"
by (simp add: relcl_def subset_cl [THEN subsetD])
lemma relcl_trans:
"[| (a,b) \ relcl L; (b,c) \ relcl L; lattice L |] ==> (a,c) \ relcl L"
apply (simp add: relcl_def)
apply (blast intro: clD cl_in_lattice)
done
lemma refl_relcl: "lattice L ==> refl (relcl L)"
by (simp add: refl_onI relcl_def subset_cl [THEN subsetD])
lemma trans_relcl: "lattice L ==> trans (relcl L)"
by (blast intro: relcl_trans transI)
lemma lattice_latticeof: "lattice (latticeof r)"
by (auto simp add: lattice_def latticeof_def)
lemma lattice_singletonI:
"[|lattice L; !!s. s \ X ==> {s} \