src/HOL/UNITY/WFair.thy
 author paulson Thu, 30 Jan 2003 18:08:09 +0100 changeset 13797 baefae13ad37 parent 10834 a7897aebbffc child 13798 4c1a53627500 permissions -rw-r--r--
conversion of UNITY theories to new-style
```
(*  Title:      HOL/UNITY/WFair
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Weak Fairness versions of transient, ensures, leadsTo.

From Misra, "A Logic for Concurrent Programming", 1994
*)

theory WFair = UNITY:

constdefs

(*This definition specifies weak fairness.  The rest of the theory
is generic to all forms of fairness.*)
transient :: "'a set => 'a program set"
"transient A == {F. EX act: Acts F. A <= Domain act & act``A <= -A}"

ensures :: "['a set, 'a set] => 'a program set"       (infixl "ensures" 60)
"A ensures B == (A-B co A Un B) Int transient (A-B)"

consts

(*LEADS-TO constant for the inductive definition*)
leads :: "'a program => ('a set * 'a set) set"

intros

Basis:  "F : A ensures B ==> (A,B) : leads F"

Union:  "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F"

constdefs

(*visible version of the LEADS-TO relation*)
leadsTo :: "['a set, 'a set] => 'a program set"    (infixl "leadsTo" 60)

(*wlt F B is the largest set that leads to B*)
wlt :: "['a program, 'a set] => 'a set"
"wlt F B == Union {A. F: A leadsTo B}"

syntax (xsymbols)
"op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)

(*** transient ***)

lemma stable_transient_empty:
"[| F : stable A; F : transient A |] ==> A = {}"

by (unfold stable_def constrains_def transient_def, blast)

lemma transient_strengthen:
"[| F : transient A; B<=A |] ==> F : transient B"
apply (unfold transient_def, clarify)
apply (blast intro!: rev_bexI)
done

lemma transientI:
"[| act: Acts F;  A <= Domain act;  act``A <= -A |] ==> F : transient A"
by (unfold transient_def, blast)

lemma transientE:
"[| F : transient A;
!!act. [| act: Acts F;  A <= Domain act;  act``A <= -A |] ==> P |]
==> P"
by (unfold transient_def, blast)

lemma transient_UNIV [simp]: "transient UNIV = {}"
by (unfold transient_def, blast)

lemma transient_empty [simp]: "transient {} = UNIV"
by (unfold transient_def, auto)

(*** ensures ***)

lemma ensuresI:
"[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B"
by (unfold ensures_def, blast)

lemma ensuresD:
"F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"
by (unfold ensures_def, blast)

lemma ensures_weaken_R:
"[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'"
apply (unfold ensures_def)
apply (blast intro: constrains_weaken transient_strengthen)
done

(*The L-version (precondition strengthening) fails, but we have this*)
lemma stable_ensures_Int:
"[| F : stable C;  F : A ensures B |]
==> F : (C Int A) ensures (C Int B)"
apply (unfold ensures_def)
apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
prefer 2 apply (blast intro: transient_strengthen)
apply (blast intro: stable_constrains_Int constrains_weaken)
done

lemma stable_transient_ensures:
"[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B"
apply (blast intro: constrains_weaken transient_strengthen)
done

lemma ensures_eq: "(A ensures B) = (A unless B) Int transient (A-B)"
by (simp (no_asm) add: ensures_def unless_def)

lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B"
done

"[| F : A leadsTo B;  F : B leadsTo C |] ==> F : A leadsTo C"
done

lemma transient_imp_leadsTo: "F : transient A ==> F : A leadsTo (-A)"

(*Useful with cancellation, disjunction*)

"F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"

(*The Union introduction rule as we should have liked to state it*)
"(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B"
done

"(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B"
apply (simp only: Int_Union_Union)
done

"(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B"
apply (subst Union_image_eq [symmetric])
done

(*Binary union introduction rule*)
"[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C"
apply (subst Un_eq_Union)
done

"(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B"
by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)

(*The INDUCTION rule as we should have liked to state it*)
"[| F : za leadsTo zb;
!!A B. F : A ensures B ==> P A B;
!!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |]
==> P A C;
!!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B
|] ==> P za zb"
apply (blast+)
done

lemma subset_imp_ensures: "A<=B ==> F : A ensures B"
by (unfold ensures_def constrains_def transient_def, blast)

(** Variant induction rule: on the preconditions for B **)

(*Lemma is the weak version: can't see how to do it in one step*)
"[| F : za leadsTo zb;
P zb;
!!A B. [| F : A ensures B;  P B |] ==> P A;
!!S. ALL A:S. P A ==> P (Union S)
|] ==> P za"
(*by induction on this formula*)
apply (subgoal_tac "P zb --> P za")
(*now solve first subgoal: this formula is sufficient*)
apply (blast+)
done

"[| F : za leadsTo zb;
P zb;
!!A B. [| F : A ensures B;  F : B leadsTo zb;  P B |] ==> P A;
!!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S)
|] ==> P za"
apply (subgoal_tac "F : za leadsTo zb & P za")
apply (erule conjunct2)
prefer 3 apply (blast intro: leadsTo_Union)
prefer 2 apply (blast intro: leadsTo_Trans)
done

"[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"

(*Distributes over binary unions*)
"F : (A Un B) leadsTo C  =  (F : A leadsTo C & F : B leadsTo C)"

"F : (UN i:I. A i) leadsTo B  =  (ALL i : I. F : (A i) leadsTo B)"

"F : (Union S) leadsTo B  =  (ALL A : S. F : A leadsTo B)"

"[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'"

(*Set difference: maybe combine with leadsTo_weaken_L?*)
"[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C"

"(!! i. i:I ==> F : (A i) leadsTo (A' i))
==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"
apply (simp only: Union_image_eq [symmetric])
done

(*Binary union version*)
"[| F : A leadsTo A'; F : B leadsTo B' |]
==> F : (A Un B) leadsTo (A' Un B')"

(** The cancellation law **)

"[| F : A leadsTo (A' Un B); F : B leadsTo B' |]
==> F : A leadsTo (A' Un B')"

"[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |]
==> F : A leadsTo (A' Un B')"
prefer 2 apply assumption
apply (simp_all (no_asm_simp))
done

"[| F : A leadsTo (B Un A'); F : B leadsTo B' |]
==> F : A leadsTo (B' Un A')"
done

"[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |]
==> F : A leadsTo (B' Un A')"
prefer 2 apply assumption
apply (simp_all (no_asm_simp))
done

(** The impossibility law **)

apply (simp_all add: ensures_def constrains_def transient_def, blast)
done

(** PSP: Progress-Safety-Progress **)

(*Special case of PSP: Misra's "stable conjunction"*)
lemma psp_stable:
"[| F : A leadsTo A'; F : stable B |]
==> F : (A Int B) leadsTo (A' Int B)"
apply (unfold stable_def)
prefer 3 apply (blast intro: leadsTo_Union_Int)
prefer 2 apply (blast intro: leadsTo_Trans)
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
apply (blast intro: transient_strengthen constrains_Int)
done

lemma psp_stable2:
"[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')"

lemma psp_ensures:
"[| F : A ensures A'; F : B co B' |]
==> F : (A Int B') ensures ((A' Int B) Un (B' - B))"
apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*)
apply (blast intro: transient_strengthen)
done

lemma psp:
"[| F : A leadsTo A'; F : B co B' |]
==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))"
prefer 3 apply (blast intro: leadsTo_Union_Int)
txt{*Basis case*}
apply (blast intro: psp_ensures)
txt{*Transitivity case has a delicate argument involving "cancellation"*}
apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset)
done

lemma psp2:
"[| F : A leadsTo A'; F : B co B' |]
==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))"
by (simp (no_asm_simp) add: psp Int_ac)

lemma psp_unless:
"[| F : A leadsTo A';  F : B unless B' |]
==> F : (A Int B) leadsTo ((A' Int B) Un B')"

apply (unfold unless_def)
apply (drule psp, assumption)
done

(*** Proving the induction rules ***)

(** The most general rule: r is any wf relation; f is any variant function **)

"[| wf r;
ALL m. F : (A Int f-`{m}) leadsTo
((A Int f-`(r^-1 `` {m})) Un B) |]
==> F : (A Int f-`{m}) leadsTo B"
apply (erule_tac a = m in wf_induct)
apply (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B")
apply (subst vimage_eq_UN)
apply (simp only: UN_simps [symmetric])
done

(** Meta or object quantifier ? **)
"[| wf r;
ALL m. F : (A Int f-`{m}) leadsTo
((A Int f-`(r^-1 `` {m})) Un B) |]
==> F : A leadsTo B"
apply (rule_tac t = A in subst)
defer 1
apply assumption
apply fast (*Blast_tac: Function unknown's argument not a parameter*)
done

lemma bounded_induct:
"[| wf r;
ALL m:I. F : (A Int f-`{m}) leadsTo
((A Int f-`(r^-1 `` {m})) Un B) |]
==> F : A leadsTo ((A - (f-`I)) Un B)"
apply (case_tac "m:I")
done

(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
lemma lessThan_induct:
"[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |]
==> F : A leadsTo B"
apply (simp (no_asm_simp))
apply blast
done

lemma lessThan_bounded_induct:
"!!l::nat. [| ALL m:(greaterThan l).
F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |]
==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)"
apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
apply (rule wf_less_than [THEN bounded_induct])
apply (simp (no_asm_simp))
done

lemma greaterThan_bounded_induct:
"!!l::nat. [| ALL m:(lessThan l).
F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |]
==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)"
apply (rule_tac f = f and f1 = "%k. l - k"
in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
apply (simp (no_asm) add: inv_image_def Image_singleton)
apply clarify
apply (case_tac "m<l")
prefer 2 apply (blast intro: not_leE subset_imp_leadsTo)
done

(*** wlt ****)

(*Misra's property W3*)
apply (unfold wlt_def)
done

lemma leadsTo_subset: "F : A leadsTo B ==> A <= wlt F B"
apply (unfold wlt_def)
done

(*Misra's property W2*)
lemma leadsTo_eq_subset_wlt: "F : A leadsTo B = (A <= wlt F B)"

(*Misra's property W4*)
lemma wlt_increasing: "B <= wlt F B"
done

(*Used in the Trans case below*)
lemma lemma1:
"[| B <= A2;
F : (A1 - B) co (A1 Un B);
F : (A2 - C) co (A2 Un C) |]
==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"
by (unfold constrains_def, clarify,  blast)

(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')"
(*Basis*)
apply (blast dest: ensuresD)
(*Trans*)
apply clarify
apply (rule_tac x = "Ba Un Bb" in exI)
(*Union*)
apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
apply (rule_tac x = "UN A:S. f A" in exI)
(*Blast_tac says PROOF FAILED*)
apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B"
in constrains_UN [THEN constrains_weaken])
apply (auto );
done

(*Misra's property W5*)
lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)"
apply (subgoal_tac "Ba = wlt F B")
prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify)
done

(*** Completion: Binary and General Finite versions ***)

lemma completion_lemma :
"[| W = wlt F (B' Un C);
F : A leadsTo (A' Un C);  F : A' co (A' Un C);
F : B leadsTo (B' Un C);  F : B' co (B' Un C) |]
==> F : (A Int B) leadsTo ((A' Int B') Un C)"
apply (subgoal_tac "F : (W-C) co (W Un B' Un C) ")
prefer 2
apply (blast intro: wlt_constrains_wlt [THEN  constrains_Un,
THEN constrains_weaken])
apply (subgoal_tac "F : (W-C) co W")
prefer 2
apply (simp add: wlt_increasing Un_assoc Un_absorb2)
apply (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C) ")
(** LEVEL 6 **)
apply (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C) ")
prefer 2
apply (subgoal_tac "A Int B <= A Int W")
prefer 2
apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
done

lemmas completion = completion_lemma [OF refl]

lemma finite_completion_lemma:
"finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) -->
(ALL i:I. F : (A' i) co (A' i Un C)) -->
F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
apply (erule finite_induct, auto)
apply (rule completion)
prefer 4
apply (simp only: INT_simps [symmetric])
apply (rule constrains_INT, auto)
done

lemma finite_completion:
"[| finite I;
!!i. i:I ==> F : (A i) leadsTo (A' i Un C);
!!i. i:I ==> F : (A' i) co (A' i Un C) |]
==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
by (blast intro: finite_completion_lemma [THEN mp, THEN mp])

lemma stable_completion:
"[| F : A leadsTo A';  F : stable A';
F : B leadsTo B';  F : stable B' |]
==> F : (A Int B) leadsTo (A' Int B')"
apply (unfold stable_def)
apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R])
apply (force+)
done

lemma finite_stable_completion:
"[| finite I;
!!i. i:I ==> F : (A i) leadsTo (A' i);
!!i. i:I ==> F : stable (A' i) |]
==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"
apply (unfold stable_def)
apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R])
apply (simp_all (no_asm_simp))
apply blast+
done

end
```