# Theory WFair

theory WFair
imports UNITY ZFC
```(*  Title:      ZF/UNITY/WFair.thy
Author:     Sidi Ehmety, Computer Laboratory
*)

section‹Progress under Weak Fairness›

theory WFair
imports UNITY ZFC
begin

text‹This theory defines the operators transient, ensures and leadsTo,
assuming weak fairness. From Misra, "A Logic for Concurrent Programming",
1994.›

definition
(* This definition specifies weak fairness.  The rest of the theory
is generic to all forms of fairness.*)
transient :: "i=>i"  where
"transient(A) =={F ∈ program. (∃act∈Acts(F). A<=domain(act) &
act``A ⊆ state-A) & st_set(A)}"

definition
ensures :: "[i,i] => i"       (infixl "ensures" 60)  where
"A ensures B == ((A-B) co (A ∪ B)) ∩ transient(A-B)"

consts

(*LEADS-TO constant for the inductive definition*)

inductive
domains
intros
Basis:  "[| F ∈ A ensures B;  A ∈ Pow(D); B ∈ Pow(D) |] ==> <A,B>:leads(D, F)"
Union:   "[| S ∈ Pow({A ∈ S. <A, B>:leads(D, F)}); B ∈ Pow(D); S ∈ Pow(Pow(D)) |] ==>

monos        Pow_mono
type_intros  Union_Pow_iff [THEN iffD2] UnionI PowI

definition
(* The Visible version of the LEADS-TO relation*)
leadsTo :: "[i, i] => i"       (infixl "⟼" 60)  where
"A ⟼ B == {F ∈ program. <A,B>:leads(state, F)}"

definition
(* wlt(F, B) is the largest set that leads to B*)
wlt :: "[i, i] => i"  where
"wlt(F, B) == ⋃({A ∈ Pow(state). F ∈ A ⟼ B})"

lemma Int_Union_Union: "⋃(B) ∩ A = (⋃b ∈ B. b ∩ A)"
by auto

lemma Int_Union_Union2: "A ∩ ⋃(B) = (⋃b ∈ B. A ∩ b)"
by auto

(*** transient ***)

lemma transient_type: "transient(A)<=program"
by (unfold transient_def, auto)

lemma transientD2:
"F ∈ transient(A) ==> F ∈ program & st_set(A)"
apply (unfold transient_def, auto)
done

lemma stable_transient_empty: "[| F ∈ stable(A); F ∈ transient(A) |] ==> A = 0"
by (simp add: stable_def constrains_def transient_def, fast)

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

lemma transientI:
"[|act ∈ Acts(F); A ⊆ domain(act); act``A ⊆ state-A;
F ∈ program; st_set(A)|] ==> F ∈ transient(A)"

lemma transientE:
"[| F ∈ transient(A);
!!act. [| act ∈ Acts(F);  A ⊆ domain(act); act``A ⊆ state-A|]==>P|]
==>P"

lemma transient_state: "transient(state) = 0"
apply (rule equalityI, auto)
apply (cut_tac F = x in Acts_type)
apply (auto intro: st0_in_state)
done

lemma transient_state2: "state<=B ==> transient(B) = 0"
apply (rule equalityI, auto)
apply (cut_tac F = x in Acts_type)
apply (subgoal_tac "B=state")
apply (auto intro: st0_in_state)
done

lemma transient_empty: "transient(0) = program"

declare transient_empty [simp] transient_state [simp] transient_state2 [simp]

(*** ensures ***)

lemma ensures_type: "A ensures B <=program"
by (simp add: ensures_def constrains_def, auto)

lemma ensuresI:
"[|F:(A-B) co (A ∪ B); F ∈ transient(A-B)|]==>F ∈ A ensures B"
apply (unfold ensures_def)
apply (auto simp add: transient_type [THEN subsetD])
done

(* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *)
lemma ensuresI2: "[| F ∈ A co A ∪ B; F ∈ transient(A) |] ==> F ∈ A ensures B"
apply (drule_tac B = "A-B" in constrains_weaken_L)
apply (drule_tac [2] B = "A-B" in transient_strengthen)
apply (auto simp add: ensures_def transient_type [THEN subsetD])
done

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

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

(*The L-version (precondition strengthening) fails, but we have this*)
lemma stable_ensures_Int:
"[| F ∈ stable(C);  F ∈ A ensures B |] ==> F:(C ∩ A) ensures (C ∩ B)"

apply (unfold ensures_def)
apply (simp (no_asm) add: Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
apply (blast intro: transient_strengthen stable_constrains_Int constrains_weaken)
done

lemma stable_transient_ensures: "[|F ∈ stable(A);  F ∈ transient(C); A<=B ∪ C|] ==> F ∈ A ensures B"
apply (frule stable_type [THEN subsetD])
apply (blast intro: transient_strengthen constrains_weaken)
done

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

lemma subset_imp_ensures: "[| F ∈ program; A<=B  |] ==> F ∈ A ensures B"
by (auto simp add: ensures_def constrains_def transient_def st_set_def)

lemma leadsTo_type: "A ⟼ B ⊆ program"

"F ∈ A ⟼ B ==> F ∈ program & st_set(A) & st_set(B)"
done

"[|F ∈ A ensures B; st_set(A); st_set(B)|] ==> F ∈ A ⟼ B"
apply (cut_tac ensures_type)
done

(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *)
(* [| F ∈ program; A<=B;  st_set(A); st_set(B) |] ==> A ⟼ B *)

lemma leadsTo_Trans: "[|F ∈ A ⟼ B;  F ∈ B ⟼ C |]==>F ∈ A ⟼ C"
done

(* Better when used in association with leadsTo_weaken_R *)
lemma transient_imp_leadsTo: "F ∈ transient(A) ==> F ∈ A ⟼ (state-A)"
apply (unfold transient_def)
apply (blast intro: ensuresI [THEN leadsTo_Basis] constrains_weaken transientI)
done

(*Useful with cancellation, disjunction*)
lemma leadsTo_Un_duplicate: "F ∈ A ⟼ (A' ∪ A') ==> F ∈ A ⟼ A'"
by simp

"F ∈ A ⟼ (A' ∪ C ∪ C) ==> F ∈ A ⟼ (A' ∪ C)"

(*The Union introduction rule as we should have liked to state it*)
"[|!!A. A ∈ S ==> F ∈ A ⟼ B; F ∈ program; st_set(B)|]
==> F ∈ ⋃(S) ⟼ B"
done

"[|!!A. A ∈ S ==>F ∈ (A ∩ C) ⟼ B; F ∈ program; st_set(B)|]
==> F ∈ (⋃(S)Int C)⟼ B"
apply (simp only: Int_Union_Union)
done

"[| !!i. i ∈ I ==> F ∈ A(i) ⟼ B; F ∈ program; st_set(B)|]
==> F:(⋃i ∈ I. A(i)) ⟼ B"
done

(* Binary union introduction rule *)
"[| F ∈ A ⟼ C; F ∈ B ⟼ C |] ==> F ∈ (A ∪ B) ⟼ C"
apply (subst Un_eq_Union)
done

"[|!!x. x ∈ A==> F:{x} ⟼ B; F ∈ program; st_set(B) |]
==> F ∈ A ⟼ B"
apply (rule_tac b = A in UN_singleton [THEN subst])
done

lemma leadsTo_refl: "[| F ∈ program; st_set(A) |] ==> F ∈ A ⟼ A"

lemma leadsTo_refl_iff: "F ∈ A ⟼ A ⟷ F ∈ program & st_set(A)"

lemma empty_leadsTo: "F ∈ 0 ⟼ B ⟷ (F ∈ program & st_set(B))"

lemma leadsTo_state: "F ∈ A ⟼ state ⟷ (F ∈ program & st_set(A))"

lemma leadsTo_weaken_R: "[| F ∈ A ⟼ A'; A'<=B'; st_set(B') |] ==> F ∈ A ⟼ B'"

lemma leadsTo_weaken_L: "[| F ∈ A ⟼ A'; B<=A |] ==> F ∈ B ⟼ A'"
done

lemma leadsTo_weaken: "[| F ∈ A ⟼ A'; B<=A; A'<=B'; st_set(B')|]==> F ∈ B ⟼ B'"
done

(* This rule has a nicer conclusion *)
lemma transient_imp_leadsTo2: "[| F ∈ transient(A); state-A<=B; st_set(B)|] ==> F ∈ A ⟼ B"
apply (frule transientD2)
done

(*Distributes over binary unions*)
lemma leadsTo_Un_distrib: "F:(A ∪ B) ⟼ C  ⟷  (F ∈ A ⟼ C & F ∈ B ⟼ C)"

"(F:(⋃i ∈ I. A(i)) ⟼ B)⟷ ((∀i ∈ I. F ∈ A(i) ⟼ B) & F ∈ program & st_set(B))"
done

lemma leadsTo_Union_distrib: "(F ∈ ⋃(S) ⟼ B) ⟷  (∀A ∈ S. F ∈ A ⟼ B) & F ∈ program & st_set(B)"

text‹Set difference: maybe combine with ‹leadsTo_weaken_L›??›
"[| F: (A-B) ⟼ C; F ∈ B ⟼ C; st_set(C) |]
==> F ∈ A ⟼ C"

"[|!!i. i ∈ I ==> F ∈ A(i) ⟼ A'(i); F ∈ program |]
==> F: (⋃i ∈ I. A(i)) ⟼ (⋃i ∈ I. A'(i))"
done

(*Binary union version*)
lemma leadsTo_Un_Un: "[| F ∈ A ⟼ A'; F ∈ B ⟼ B' |] ==> F ∈ (A ∪ B) ⟼ (A' ∪ B')"
apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') ")
prefer 2 apply (blast dest: leadsToD2)
done

(** The cancellation law **)
lemma leadsTo_cancel2: "[|F ∈ A ⟼ (A' ∪ B); F ∈ B ⟼ B'|] ==> F ∈ A ⟼ (A' ∪ B')"
apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') &F ∈ program")
prefer 2 apply (blast dest: leadsToD2)
done

lemma leadsTo_cancel_Diff2: "[|F ∈ A ⟼ (A' ∪ B); F ∈ (B-A') ⟼ B'|]==> F ∈ A ⟼ (A' ∪ B')"
prefer 2 apply assumption
done

lemma leadsTo_cancel1: "[| F ∈ A ⟼ (B ∪ A'); F ∈ B ⟼ B' |] ==> F ∈ A ⟼ (B' ∪ A')"
done

"[|F ∈ A ⟼ (B ∪ A'); F: (B-A') ⟼ B'|]==> F ∈ A ⟼ (B' ∪ A')"
prefer 2 apply assumption
done

(*The INDUCTION rule as we should have liked to state it*)
assumes major: "F ∈ za ⟼ zb"
and basis: "!!A B. [|F ∈ A ensures B; st_set(A); st_set(B)|] ==> P(A,B)"
and trans: "!!A B C. [| F ∈ A ⟼ B; P(A, B);
F ∈ B ⟼ C; P(B, C) |] ==> P(A,C)"
and union: "!!B S. [| ∀A ∈ S. F ∈ A ⟼ B; ∀A ∈ S. P(A,B);
st_set(B); ∀A ∈ S. st_set(A)|] ==> P(⋃(S), B)"
shows "P(za, zb)"
apply (cut_tac major)
apply (blast intro: basis [unfolded st_set_def])
apply (blast intro: trans [unfolded leadsTo_def])
apply (force intro: union [unfolded st_set_def leadsTo_def])
done

(* Added by Sidi, an induction rule without ensures *)
assumes major: "F ∈ za ⟼ zb"
and basis1: "!!A B. [| A<=B; st_set(B) |] ==> P(A, B)"
and basis2: "!!A B. [| F ∈ A co A ∪ B; F ∈ transient(A); st_set(B) |]
==> P(A, B)"
and trans: "!!A B C. [| F ∈ A ⟼ B; P(A, B);
F ∈ B ⟼ C; P(B, C) |] ==> P(A,C)"
and union: "!!B S. [| ∀A ∈ S. F ∈ A ⟼ B; ∀A ∈ S. P(A,B);
st_set(B); ∀A ∈ S. st_set(A)|] ==> P(⋃(S), B)"
shows "P(za, zb)"
apply (cut_tac major)
apply (auto intro: trans union)
apply (frule constrainsD2)
apply (drule_tac B' = " (A-B) ∪ B" in constrains_weaken_R)
apply blast
apply (drule_tac [4] basis2, simp_all)
apply (frule_tac A1 = A and B = B in Int_lower2 [THEN basis1])
apply (subgoal_tac "A=⋃({A - B, A ∩ B}) ")
prefer 2 apply blast
apply (erule ssubst)
apply (rule union)
done

(** 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 ⟼ zb;
P(zb);
!!A B. [| F ∈ A ensures B;  P(B); st_set(A); st_set(B) |] ==> P(A);
!!S. [| ∀A ∈ S. P(A); ∀A ∈ S. st_set(A) |] ==> P(⋃(S))
|] ==> P(za)"
txt‹by induction on this formula›
apply (subgoal_tac "P (zb) ⟶ P (za) ")
txt‹now solve first subgoal: this formula is sufficient›
apply (blast+)
done

"[| F ∈ za ⟼ zb;
P(zb);
!!A B. [| F ∈ A ensures B;  F ∈ B ⟼ zb;  P(B); st_set(A) |] ==> P(A);
!!S. ∀A ∈ S. F ∈ A ⟼ zb & P(A) & st_set(A) ==> P(⋃(S))
|] ==> P(za)"
apply (subgoal_tac " (F ∈ za ⟼ zb) & P (za) ")
apply (erule conjunct2)
done

(** The impossibility law **)
"F ∈ A ⟼ 0 ==> A=0"
apply (auto simp add: ensures_def constrains_def transient_def st_set_def)
apply (drule bspec, assumption)+
apply blast
done

subsection‹PSP: Progress-Safety-Progress›

text‹Special case of PSP: Misra's "stable conjunction"›

lemma psp_stable:
"[| F ∈ A ⟼ A'; F ∈ stable(B) |] ==> F:(A ∩ B) ⟼ (A' ∩ 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 (auto intro: transient_strengthen constrains_Int)
done

lemma psp_stable2: "[|F ∈ A ⟼ A'; F ∈ stable(B) |]==>F: (B ∩ A) ⟼ (B ∩ A')"
apply (simp (no_asm_simp) add: psp_stable Int_ac)
done

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

lemma psp:
"[|F ∈ A ⟼ A'; F ∈ B co B'; st_set(B')|]==> F:(A ∩ B') ⟼ ((A' ∩ B) ∪ (B' - B))"
apply (subgoal_tac "F ∈ program & st_set (A) & st_set (A') & st_set (B) ")
prefer 2 apply (blast dest!: constrainsD2 leadsToD2)
prefer 3 apply (blast intro: leadsTo_Union_Int)
txt‹Basis case›
txt‹Transitivity case has a delicate argument involving "cancellation"›
apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset)
done

lemma psp2: "[| F ∈ A ⟼ A'; F ∈ B co B'; st_set(B') |]
==> F ∈ (B' ∩ A) ⟼ ((B ∩ A') ∪ (B' - B))"
by (simp (no_asm_simp) add: psp Int_ac)

lemma psp_unless:
"[| F ∈ A ⟼ A';  F ∈ B unless B'; st_set(B); st_set(B') |]
==> F ∈ (A ∩ B) ⟼ ((A' ∩ B) ∪ B')"
apply (unfold unless_def)
apply (subgoal_tac "st_set (A) &st_set (A') ")
prefer 2 apply (blast dest: leadsToD2)
apply (drule psp, assumption, blast)
done

subsection‹Proving the induction rules›

(** The most general rule ∈ r is any wf relation; f is any variant function **)
m ∈ I;
field(r)<=I;
F ∈ program; st_set(B);
∀m ∈ I. F ∈ (A ∩ f-``{m}) ⟼
((A ∩ f-``(converse(r)``{m})) ∪ B) |]
==> F ∈ (A ∩ f-``{m}) ⟼ B"
apply (erule_tac a = m in wf_induct2, simp_all)
apply (subgoal_tac "F ∈ (A ∩ (f-`` (converse (r) ``{x}))) ⟼ B")
apply (subst vimage_eq_UN)
apply (simp del: UN_simps add: Int_UN_distrib)
done

(** Meta or object quantifier ? **)
field(r)<=I;
A<=f-``I;
F ∈ program; st_set(A); st_set(B);
∀m ∈ I. F ∈ (A ∩ f-``{m}) ⟼
((A ∩ f-``(converse(r)``{m})) ∪ B) |]
==> F ∈ A ⟼ B"
apply (rule_tac b = A in subst)
defer 1
apply (rule_tac I = I in leadsTo_UN)
apply (erule_tac I = I in leadsTo_wf_induct_aux, assumption+, best)
done

lemma nat_measure_field: "field(measure(nat, %x. x)) = nat"
apply (unfold field_def)
apply (rule equalityI, force, clarify)
apply (erule_tac V = "x∉range (y)" for y in thin_rl)
apply (erule nat_induct)
apply (rule_tac [2] b = "succ (succ (xa))" in domainI)
apply (rule_tac b = "succ (0) " in domainI)
apply simp_all
done

lemma Image_inverse_lessThan: "k<A ==> measure(A, %x. x) -`` {k} = k"
apply (rule equalityI)
apply (blast intro: ltD)
apply (rule vimageI)
prefer 2 apply blast
apply (simp add: lt_Ord lt_Ord2 Ord_mem_iff_lt)
apply (blast intro: lt_trans)
done

(*Alternative proof is via the lemma F ∈ (A ∩ f-`(lessThan m)) ⟼ B*)
lemma lessThan_induct:
"[| A<=f-``nat;
F ∈ program; st_set(A); st_set(B);
∀m ∈ nat. F:(A ∩ f-``{m}) ⟼ ((A ∩ f -`` m) ∪ B) |]
==> F ∈ A ⟼ B"
apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN leadsTo_wf_induct])
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
done

(*** wlt ****)

(*Misra's property W3*)
lemma wlt_type: "wlt(F,B) <=state"
by (unfold wlt_def, auto)

lemma wlt_st_set: "st_set(wlt(F, B))"
apply (unfold st_set_def)
apply (rule wlt_type)
done
declare wlt_st_set [iff]

lemma wlt_leadsTo_iff: "F ∈ wlt(F, B) ⟼ B ⟷ (F ∈ program & st_set(B))"
apply (unfold wlt_def)
done

(* [| F ∈ program;  st_set(B) |] ==> F ∈ wlt(F, B) ⟼ B  *)

lemma leadsTo_subset: "F ∈ A ⟼ B ==> A ⊆ wlt(F, B)"
apply (unfold wlt_def)
done

(*Misra's property W2*)
lemma leadsTo_eq_subset_wlt: "F ∈ A ⟼ B ⟷ (A ⊆ wlt(F,B) & F ∈ program & st_set(B))"
apply auto
done

(*Misra's property W4*)
lemma wlt_increasing: "[| F ∈ program; st_set(B) |] ==> B ⊆ wlt(F,B)"
done

(*Used in the Trans case below*)
"[| B ⊆ A2;
F ∈ (A1 - B) co (A1 ∪ B);
F ∈ (A2 - C) co (A2 ∪ C) |]
==> F ∈ (A1 ∪ A2 - C) co (A1 ∪ A2 ∪ C)"
apply (unfold constrains_def st_set_def, blast)
done

(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
(* slightly different from the HOL one ∈ B here is bounded *)
lemma leadsTo_123: "F ∈ A ⟼ A'
==> ∃B ∈ Pow(state). A<=B & F ∈ B ⟼ A' & F ∈ (B-A') co (B ∪ A')"
txt‹Basis›
apply (blast dest: ensuresD constrainsD2 st_setD)
txt‹Trans›
apply clarify
apply (rule_tac x = "Ba ∪ Bb" in bexI)
txt‹Union›
apply (clarify dest!: ball_conj_distrib [THEN iffD1])
apply (subgoal_tac "∃y. y ∈ Pi (S, %A. {Ba ∈ Pow (state) . A<=Ba & F ∈ Ba ⟼ B & F ∈ Ba - B co Ba ∪ B}) ")
defer 1
apply (rule AC_ball_Pi, safe)
apply (rotate_tac 1)
apply (drule_tac x = x in bspec, blast, blast)
apply (rule_tac x = "⋃A ∈ S. y`A" in bexI, safe)
apply (rule_tac [3] I1 = S in constrains_UN [THEN constrains_weaken])
prefer 5 apply (blast dest!: apply_type, simp_all)
apply (force dest!: apply_type)+
done

(*Misra's property W5*)
lemma wlt_constrains_wlt: "[| F ∈ program; st_set(B) |] ==>F ∈ (wlt(F, B) - B) co (wlt(F,B))"
apply clarify
apply (subgoal_tac "Ba = wlt (F,B) ")
prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify)
apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]])
done

subsection‹Completion: Binary and General Finite versions›

lemma completion_aux: "[| W = wlt(F, (B' ∪ C));
F ∈ A ⟼ (A' ∪ C);  F ∈ A' co (A' ∪ C);
F ∈ B ⟼ (B' ∪ C);  F ∈ B' co (B' ∪ C) |]
==> F ∈ (A ∩ B) ⟼ ((A' ∩ B') ∪ C)"
apply (subgoal_tac "st_set (C) &st_set (W) &st_set (W-C) &st_set (A') &st_set (A) & st_set (B) & st_set (B') & F ∈ program")
prefer 2
apply simp
apply (subgoal_tac "F ∈ (W-C) co (W ∪ B' ∪ C) ")
prefer 2
apply (blast intro!: constrains_weaken [OF constrains_Un [OF _ wlt_constrains_wlt]])
apply (subgoal_tac "F ∈ (W-C) co W")
prefer 2
apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]] Un_assoc)
apply (subgoal_tac "F ∈ (A ∩ W - C) ⟼ (A' ∩ W ∪ C) ")
(** step 13 **)
apply (subgoal_tac "F ∈ (A' ∩ W ∪ C) ⟼ (A' ∩ B' ∪ C) ")
apply (subgoal_tac "A ∩ B ⊆ A ∩ W")
prefer 2 apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
txt‹last subgoal›
prefer 2 apply (blast intro: leadsTo_refl)
apply (rule_tac A'1 = "B' ∪ C" in wlt_leadsTo[THEN psp2, THEN leadsTo_weaken])
apply blast+
done

lemmas completion = refl [THEN completion_aux]

lemma finite_completion_aux:
"[| I ∈ Fin(X); F ∈ program; st_set(C) |] ==>
(∀i ∈ I. F ∈ (A(i)) ⟼ (A'(i) ∪ C)) ⟶
(∀i ∈ I. F ∈ (A'(i)) co (A'(i) ∪ C)) ⟶
F ∈ (⋂i ∈ I. A(i)) ⟼ ((⋂i ∈ I. A'(i)) ∪ C)"
apply (erule Fin_induct)
apply (rule completion)
apply (auto simp del: INT_simps simp add: INT_extend_simps)
apply (blast intro: constrains_INT)
done

lemma finite_completion:
"[| I ∈ Fin(X);
!!i. i ∈ I ==> F ∈ A(i) ⟼ (A'(i) ∪ C);
!!i. i ∈ I ==> F ∈ A'(i) co (A'(i) ∪ C); F ∈ program; st_set(C)|]
==> F ∈ (⋂i ∈ I. A(i)) ⟼ ((⋂i ∈ I. A'(i)) ∪ C)"
by (blast intro: finite_completion_aux [THEN mp, THEN mp])

lemma stable_completion:
"[| F ∈ A ⟼ A';  F ∈ stable(A');
F ∈ B ⟼ B';  F ∈ stable(B') |]
==> F ∈ (A ∩ B) ⟼ (A' ∩ B')"
apply (unfold stable_def)
apply (rule_tac C1 = 0 in completion [THEN leadsTo_weaken_R], simp+)
done

lemma finite_stable_completion:
"[| I ∈ Fin(X);
(!!i. i ∈ I ==> F ∈ A(i) ⟼ A'(i));
(!!i. i ∈ I ==> F ∈ stable(A'(i)));  F ∈ program |]
==> F ∈ (⋂i ∈ I. A(i)) ⟼ (⋂i ∈ I. A'(i))"
apply (unfold stable_def)
apply (subgoal_tac "st_set (⋂i ∈ I. A' (i))")
prefer 2 apply (blast dest: leadsToD2)
apply (rule_tac C1 = 0 in finite_completion [THEN leadsTo_weaken_R], auto)
done

end
```