Quelle  WFair.thy

(*  Title:      ZF/UNITY/WFair.thy
    Author:     Sidi Ehmety, Computer Laboratory
    Copyright   1998  University of Cambridge
*)

section‹Progress under Weak Fairness›

theory WFair
imports UNITY ZFC
begin

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

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*)
  leads :: "[i, i]==>i"

inductive
  domains
     "leads(D, F)" ⊆ "Pow(D)*Pow(D)"
  intros
    Basis:  "[F ∈ A ensures B; A ∈ Pow(D); B ∈ Pow(D)] ==> ⟨A,B⟩:leads(D, F)"
    Trans:  "[⟨A,B⟩ ∈ leads(D, F); ⟨B,C⟩ ∈ leads(D, F)] ==> ⟨A,C⟩:leads(D, F)"
    Union:   "[S ∈ Pow({A ∈ S. ⟨A, B⟩:leads(D, F)}); B ∈ Pow(D); S ∈ Pow(Pow(D))] ==>
              <∪(S),B>:leads(D, F)"

  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})"

(** Ad-hoc set-theory rules **)

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)"
by (simp add: transient_def, blast)

lemma transientE:
     "[F ∈ transient(A);
         ∧act. [act ∈ Acts(F); A ⊆ domain(act); act``A ⊆ state-A]==>P]
      ==>P"
by (simp add: transient_def, blast)

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

lemma transient_state2: "state<=B ==> transient(B) = 0"
apply (simp add: transient_def st_set_def)
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"
by (auto simp add: transient_def)

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"
  unfolding 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'"
  unfolding 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)"

  unfolding 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 (simp add: ensures_def stable_def)
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)

(*** leadsTo ***)
lemmas leads_left = leads.dom_subset [THEN subsetD, THEN SigmaD1]
lemmas leads_right = leads.dom_subset [THEN subsetD, THEN SigmaD2]

lemma leadsTo_type: "A ⟼ B ⊆ program"
by (unfold leadsTo_def, auto)

lemma leadsToD2:
"F ∈ A ⟼ B ==> F ∈ program ∧ st_set(A) ∧ st_set(B)"
  unfolding leadsTo_def st_set_def
apply (blast dest: leads_left leads_right)
done

lemma leadsTo_Basis:
    "[F ∈ A ensures B; st_set(A); st_set(B)] ==> F ∈ A ⟼ B"
  unfolding leadsTo_def st_set_def
apply (cut_tac ensures_type)
apply (auto intro: leads.Basis)
done
declare leadsTo_Basis [intro]

(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *)
(* \<lbrakk>F \<in> program; A<=B;  st_set(A); st_set(B)\<rbrakk> \<Longrightarrow> A \<longmapsto> B *)
lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]

lemma leadsTo_Trans: "[F ∈ A ⟼ B; F ∈ B ⟼ C]==>F ∈ A ⟼ C"
  unfolding leadsTo_def
apply (auto intro: leads.Trans)
done

(* Better when used in association with leadsTo_weaken_R *)
lemma transient_imp_leadsTo: "F ∈ transient(A) ==> F ∈ A ⟼ (state-A)"
  unfolding 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

lemma leadsTo_Un_duplicate2:
     "F ∈ A ⟼ (A' ∪ C ∪ C) ==> F ∈ A ⟼ (A' ∪ C)"
by (simp add: Un_ac)

(*The Union introduction rule as we should have liked to state it*)
lemma leadsTo_Union:
    "[∧A. A ∈ S ==> F ∈ A ⟼ B; F ∈ program; st_set(B)]
     ==> F ∈ ∪(S) ⟼ B"
  unfolding leadsTo_def st_set_def
apply (blast intro: leads.Union dest: leads_left)
done

lemma leadsTo_Union_Int:
    "[∧A. A ∈ S ==>F ∈ (A ∩ C) ⟼ B; F ∈ program; st_set(B)]
     ==> F ∈ (∪(S)Int C)⟼ B"
  unfolding leadsTo_def st_set_def
apply (simp only: Int_Union_Union)
apply (blast dest: leads_left intro: leads.Union)
done

lemma leadsTo_UN:
    "[∧i. i ∈ I ==> F ∈ A(i) ⟼ B; F ∈ program; st_set(B)]
     ==> F:(∪i ∈ I. A(i)) ⟼ B"
apply (simp add: Int_Union_Union leadsTo_def st_set_def)
apply (blast dest: leads_left intro: leads.Union)
done

(* Binary union introduction rule *)
lemma leadsTo_Un:
     "[F ∈ A ⟼ C; F ∈ B ⟼ C] ==> F ∈ (A ∪ B) ⟼ C"
apply (subst Un_eq_Union)
apply (blast intro: leadsTo_Union dest: leadsToD2)
done

lemma single_leadsTo_I:
    "[∧x. x ∈ A==> F:{x} ⟼ B; F ∈ program; st_set(B)]
     ==> F ∈ A ⟼ B"
apply (rule_tac b = A in UN_singleton [THEN subst])
apply (rule leadsTo_UN, auto)
done

lemma leadsTo_refl: "[F ∈ program; st_set(A)] ==> F ∈ A ⟼ A"
by (blast intro: subset_imp_leadsTo)

lemma leadsTo_refl_iff: "F ∈ A ⟼ A ⟷ F ∈ program ∧ st_set(A)"
by (auto intro: leadsTo_refl dest: leadsToD2)

lemma empty_leadsTo: "F ∈ 0 ⟼ B ⟷ (F ∈ program ∧ st_set(B))"
by (auto intro: subset_imp_leadsTo dest: leadsToD2)
declare empty_leadsTo [iff]

lemma leadsTo_state: "F ∈ A ⟼ state ⟷ (F ∈ program ∧ st_set(A))"
by (auto intro: subset_imp_leadsTo dest: leadsToD2 st_setD)
declare leadsTo_state [iff]

lemma leadsTo_weaken_R: "[F ∈ A ⟼ A'; A'<=B'; st_set(B')] ==> F ∈ A ⟼ B'"
by (blast dest: leadsToD2 intro: subset_imp_leadsTo leadsTo_Trans)

lemma leadsTo_weaken_L: "[F ∈ A ⟼ A'; B<=A] ==> F ∈ B ⟼ A'"
apply (frule leadsToD2)
apply (blast intro: leadsTo_Trans subset_imp_leadsTo st_set_subset)
done

lemma leadsTo_weaken: "[F ∈ A ⟼ A'; B<=A; A'<=B'; st_set(B')]==> F ∈ B ⟼ B'"
apply (frule leadsToD2)
apply (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans leadsTo_refl)
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)
apply (rule leadsTo_weaken_R)
apply (auto simp add: transient_imp_leadsTo)
done

(*Distributes over binary unions*)
lemma leadsTo_Un_distrib: "F:(A ∪ B) ⟼ C ⟷ (F ∈ A ⟼ C ∧ F ∈ B ⟼ C)"
by (blast intro: leadsTo_Un leadsTo_weaken_L)

lemma leadsTo_UN_distrib:
"(F:(∪i ∈ I. A(i)) ⟼ B)⟷ ((∀i ∈ I. F ∈ A(i) ⟼ B) ∧ F ∈ program ∧ st_set(B))"
apply (blast dest: leadsToD2 intro: leadsTo_UN leadsTo_weaken_L)
done

lemma leadsTo_Union_distrib: "(F ∈ ∪(S) ⟼ B) ⟷ (∀A ∈ S. F ∈ A ⟼ B) ∧ F ∈ program ∧ st_set(B)"
by (blast dest: leadsToD2 intro: leadsTo_Union leadsTo_weaken_L)

text‹Set difference: maybe combine with ‹leadsTo_weaken_L›??›
lemma leadsTo_Diff:
     "[F: (A-B) ⟼ C; F ∈ B ⟼ C; st_set(C)]
      ==> F ∈ A ⟼ C"
by (blast intro: leadsTo_Un leadsTo_weaken dest: leadsToD2)

lemma leadsTo_UN_UN:
    "[∧i. i ∈ I ==> F ∈ A(i) ⟼ A'(i); F ∈ program]
     ==> F: (∪i ∈ I. A(i)) ⟼ (∪i ∈ I. A'(i))"
apply (rule leadsTo_Union)
apply (auto intro: leadsTo_weaken_R dest: leadsToD2)
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)
apply (blast intro: leadsTo_Un leadsTo_weaken_R)
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)
apply (blast intro: leadsTo_Trans leadsTo_Un_Un leadsTo_refl)
done

lemma leadsTo_cancel_Diff2: "[F ∈ A ⟼ (A' ∪ B); F ∈ (B-A') ⟼ B']==> F ∈ A ⟼ (A' ∪ B')"
apply (rule leadsTo_cancel2)
prefer 2 apply assumption
apply (blast dest: leadsToD2 intro: leadsTo_weaken_R)
done


lemma leadsTo_cancel1: "[F ∈ A ⟼ (B ∪ A'); F ∈ B ⟼ B'] ==> F ∈ A ⟼ (B' ∪ A')"
apply (simp add: Un_commute)
apply (blast intro!: leadsTo_cancel2)
done

lemma leadsTo_cancel_Diff1:
     "[F ∈ A ⟼ (B ∪ A'); F: (B-A') ⟼ B']==> F ∈ A ⟼ (B' ∪ A')"
apply (rule leadsTo_cancel1)
prefer 2 apply assumption
apply (blast intro: leadsTo_weaken_R dest: leadsToD2)
done

(*The INDUCTION rule as we should have liked to state it*)
lemma leadsTo_induct:
  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 (unfold leadsTo_def, clarify)
apply (erule leads.induct)
  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 *)
lemma leadsTo_induct2:
  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 (erule leadsTo_induct)
apply (auto intro: trans union)
apply (simp add: ensures_def, clarify)
apply (frule constrainsD2)
apply (drule_tac B' = " (A-B) ∪ B" in constrains_weaken_R)
apply blast
apply (frule ensuresI2 [THEN leadsTo_Basis])
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)
apply (auto intro: subset_imp_leadsTo)
done


(** Variant induction rule: on the preconditions for B **)
(*Lemma is the weak version: can't see how to do it in one step*)
lemma leadsTo_induct_pre_aux:
  "[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))
\<rbrakk> ==> 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 intro: leadsTo_refl)
apply (erule leadsTo_induct)
apply (blast+)
done


lemma leadsTo_induct_pre:
  "[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))
\<rbrakk> ==> P(za)"
apply (subgoal_tac " (F ∈ za ⟼ zb) ∧ P (za) ")
apply (erule conjunct2)
apply (frule leadsToD2)
apply (erule leadsTo_induct_pre_aux)
prefer 3 apply (blast dest: leadsToD2 intro: leadsTo_Union)
prefer 2 apply (blast intro: leadsTo_Trans leadsTo_Basis)
apply (blast intro: leadsTo_refl)
done

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

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)"
  unfolding stable_def
apply (frule leadsToD2)
apply (erule leadsTo_induct)
prefer 3 apply (blast intro: leadsTo_Union_Int)
prefer 2 apply (blast intro: leadsTo_Trans)
apply (rule leadsTo_Basis)
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))"
  unfolding 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)
apply (erule leadsTo_induct)
prefer 3 apply (blast intro: leadsTo_Union_Int)
 txt‹Basis case›
 apply (blast intro: psp_ensures leadsTo_Basis)
txt‹Transitivity case has a delicate argument involving "cancellation"›
apply (rule leadsTo_Un_duplicate2)
apply (erule leadsTo_cancel_Diff1)
apply (simp add: Int_Diff Diff_triv)
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')"
  unfolding unless_def
apply (subgoal_tac "st_set (A) ∧st_set (A') ")
prefer 2 apply (blast dest: leadsToD2)
apply (drule psp, assumption, blast)
apply (blast intro: leadsTo_weaken)
done


subsection‹Proving the induction rules›

(** The most general rule \<in> r is any wf relation; f is any variant function **)
lemma leadsTo_wf_induct_aux: "[wf(r);
         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 (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
apply (subst vimage_eq_UN)
apply (simp del: UN_simps add: Int_UN_distrib)
apply (auto intro: leadsTo_UN simp del: UN_simps simp add: Int_UN_distrib)
done

(** Meta or object quantifier ? **)
lemma leadsTo_wf_induct: "[wf(r);
         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"
  unfolding field_def
apply (simp add: measure_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 (auto simp add: measure_def)
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 \<in> (A \<inter> f-`(lessThan m)) \<longmapsto> 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_all add: nat_measure_field)
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))"
  unfolding 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))"
  unfolding wlt_def
apply (blast dest: leadsToD2 intro!: leadsTo_Union)
done

(* \<lbrakk>F \<in> program;  st_set(B)\<rbrakk> \<Longrightarrow> F \<in> wlt(F, B) \<longmapsto> B  *)
lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2]]

lemma leadsTo_subset: "F ∈ A ⟼ B ==> A ⊆ wlt(F, B)"
  unfolding wlt_def
apply (frule leadsToD2)
apply (auto simp add: st_set_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
apply (blast dest: leadsToD2 leadsTo_subset intro: leadsTo_weaken_L wlt_leadsTo)+
done

(*Misra's property W4*)
lemma wlt_increasing: "[F ∈ program; st_set(B)] ==> B ⊆ wlt(F,B)"
apply (rule leadsTo_subset)
apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [THEN iff_sym] subset_imp_leadsTo)
done

(*Used in the Trans case below*)
lemma leadsTo_123_aux:
   "[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 \<in> B here is bounded *)
lemma leadsTo_123: "F ∈ A ⟼ A'
      ==> ∃B ∈ Pow(state). A<=B ∧ F ∈ B ⟼ A' ∧ F ∈ (B-A') co (B ∪ A')"
apply (frule leadsToD2)
apply (erule leadsTo_induct)
  txt‹Basis›
  apply (blast dest: ensuresD constrainsD2 st_setD)
 txt‹Trans›
 apply clarify
 apply (rule_tac x = "Ba ∪ Bb" in bexI)
 apply (blast intro: leadsTo_123_aux leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate, blast)
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])
apply (rule_tac [2] leadsTo_Union)
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 (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], assumption, blast)
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 (blast dest!: leadsToD2)
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) ")
 prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
(** step 13 **)
apply (subgoal_tac "F ∈ (A' ∩ W ∪ C) ⟼ (A' ∩ B' ∪ C) ")
apply (drule leadsTo_Diff)
apply (blast intro: subset_imp_leadsTo dest: leadsToD2 constrainsD2)
apply (force simp add: st_set_def)
apply (subgoal_tac "A ∩ B ⊆ A ∩ W")
prefer 2 apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
apply (blast intro: leadsTo_Trans subset_imp_leadsTo)
txt‹last subgoal›
apply (rule_tac leadsTo_Un_duplicate2)
apply (rule_tac leadsTo_Un_Un)
 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 (auto simp add: Inter_0)
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')"
  unfolding stable_def
apply (rule_tac C1 = 0 in completion [THEN leadsTo_weaken_R], simp+)
apply (blast dest: leadsToD2)
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))"
  unfolding 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