Theory WFair

(*  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,
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*)
  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 *)
(* ⟦F ∈ program; A<=B;  st_set(A); st_set(B)⟧ ⟹ A ⟼ 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))
⟧ ⟹ 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))
⟧ ⟹ 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 ∈ 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 ∈ (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_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

(* ⟦F ∈ program;  st_set(B)⟧ ⟹ F ∈ wlt(F, B) ⟼ 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 ∈ 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