# Theory WFair

Up to index of Isabelle/ZF/UNITY

theory WFair
imports UNITY Main_ZFC
begin

    (*  Title:      HOL/UNITY/WFair.thy
        ID:         $Id: WFair.thy,v 1.6 2005/03/28 14:19:58 paulson Exp $
        Author:     Sidi Ehmety, Computer Laboratory
        Copyright   1998  University of Cambridge
    *)

    header{*Progress under Weak Fairness*}

    theory WFair
    imports UNITY Main_ZFC
    begin

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

    constdefs

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

      ensures :: "[i,i] => i"       (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 :: "[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)) |] ==>
                  <Union(S),B>:leads(D, F)"

      monos        Pow_mono
      type_intros  Union_Pow_iff [THEN iffD2] UnionI PowI

    constdefs

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

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

    syntax (xsymbols)
      "leadsTo" :: "[i, i] => i" (infixl "\<longmapsto>" 60)

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

    lemma Int_Union_Union: "Union(B) Int A = (\<Union>b ∈ B. b Int A)"
    by auto

    lemma Int_Union_Union2: "A Int Union(B) = (\<Union>b ∈ B. A Int 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 Un 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 Un 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 Un 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 Int A) ensures (C Int 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 Un 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) Int 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 leadsTo B <= program"
    by (unfold leadsTo_def, auto)

    lemma leadsToD2:
    "F ∈ A leadsTo B ==> F ∈ program & st_set(A) & st_set(B)"
    apply (unfold 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 leadsTo B"
    apply (unfold 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 leadsTo B *)
    lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]

    lemma leadsTo_Trans: "[|F ∈ A leadsTo B;  F ∈ B leadsTo C |]==>F ∈ A leadsTo C"
    apply (unfold 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 leadsTo (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 leadsTo (A' Un A') ==> F ∈ A leadsTo A'"
    by simp

    lemma leadsTo_Un_duplicate2:
         "F ∈ A leadsTo (A' Un C Un C) ==> F ∈ A leadsTo (A' Un 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 leadsTo B; F ∈ program; st_set(B)|]
         ==> F ∈ Union(S) leadsTo B"
    apply (unfold leadsTo_def st_set_def)
    apply (blast intro: leads.Union dest: leads_left)
    done

    lemma leadsTo_Union_Int:
        "[|!!A. A ∈ S ==>F : (A Int C) leadsTo B; F ∈ program; st_set(B)|]
         ==> F : (Union(S)Int C)leadsTo B"
    apply (unfold 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) leadsTo B; F ∈ program; st_set(B)|]
         ==> F:(\<Union>i ∈ I. A(i)) leadsTo 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 leadsTo C; F ∈ B leadsTo C |] ==> F ∈ (A Un B) leadsTo C"
    apply (subst Un_eq_Union)
    apply (blast intro: leadsTo_Union dest: leadsToD2)
    done

    lemma single_leadsTo_I:
        "[|!!x. x ∈ A==> F:{x} leadsTo B; F ∈ program; st_set(B) |]
         ==> F ∈ A leadsTo 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 leadsTo A"
    by (blast intro: subset_imp_leadsTo)

    lemma leadsTo_refl_iff: "F ∈ A leadsTo A <-> F ∈ program & st_set(A)"
    by (auto intro: leadsTo_refl dest: leadsToD2)

    lemma empty_leadsTo: "F ∈ 0 leadsTo B <-> (F ∈ program & st_set(B))"
    by (auto intro: subset_imp_leadsTo dest: leadsToD2)
    declare empty_leadsTo [iff]

    lemma leadsTo_state: "F ∈ A leadsTo 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 leadsTo A'; A'<=B'; st_set(B') |] ==> F ∈ A leadsTo B'"
    by (blast dest: leadsToD2 intro: subset_imp_leadsTo leadsTo_Trans)

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

    lemma leadsTo_weaken: "[| F ∈ A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F ∈ B leadsTo 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 leadsTo 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 Un B) leadsTo C  <->  (F ∈ A leadsTo C & F ∈ B leadsTo C)"
    by (blast intro: leadsTo_Un leadsTo_weaken_L)

    lemma leadsTo_UN_distrib:
    "(F:(\<Union>i ∈ I. A(i)) leadsTo B)<-> ((∀i ∈ I. F ∈ A(i) leadsTo B) & F ∈ program & st_set(B))"
    apply (blast dest: leadsToD2 intro: leadsTo_UN leadsTo_weaken_L)
    done

    lemma leadsTo_Union_distrib: "(F ∈ Union(S) leadsTo B) <->  (∀A ∈ S. F ∈ A leadsTo B) & F ∈ program & st_set(B)"
    by (blast dest: leadsToD2 intro: leadsTo_Union leadsTo_weaken_L)

    text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}
    lemma leadsTo_Diff:
         "[| F: (A-B) leadsTo C; F ∈ B leadsTo C; st_set(C) |]
          ==> F ∈ A leadsTo C"
    by (blast intro: leadsTo_Un leadsTo_weaken dest: leadsToD2)

    lemma leadsTo_UN_UN:
        "[|!!i. i ∈ I ==> F ∈ A(i) leadsTo A'(i); F ∈ program |]
         ==> F: (\<Union>i ∈ I. A(i)) leadsTo (\<Union>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 leadsTo A'; F ∈ B leadsTo B' |] ==> F ∈ (A Un B) leadsTo (A' Un 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 leadsTo (A' Un B); F ∈ B leadsTo B'|] ==> F ∈ A leadsTo (A' Un 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 leadsTo (A' Un B); F ∈ (B-A') leadsTo B'|]==> F ∈ A leadsTo (A' Un B')"
    apply (rule leadsTo_cancel2)
    prefer 2 apply assumption
    apply (blast dest: leadsToD2 intro: leadsTo_weaken_R)
    done

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

    lemma leadsTo_cancel_Diff1:
         "[|F ∈ A leadsTo (B Un A'); F: (B-A') leadsTo B'|]==> F ∈ A leadsTo (B' Un 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 leadsTo 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 leadsTo B; P(A, B);
                                  F ∈ B leadsTo C; P(B, C) |] ==> P(A,C)"
          and union: "!!B S. [| ∀A ∈ S. F ∈ A leadsTo B; ∀A ∈ S. P(A,B);
                               st_set(B); ∀A ∈ S. st_set(A)|] ==> P(Union(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 leadsTo zb"
          and basis1: "!!A B. [| A<=B; st_set(B) |] ==> P(A, B)"
          and basis2: "!!A B. [| F ∈ A co A Un B; F ∈ transient(A); st_set(B) |]
                              ==> P(A, B)"
          and trans: "!!A B C. [| F ∈ A leadsTo B; P(A, B);
                                  F ∈ B leadsTo C; P(B, C) |] ==> P(A,C)"
          and union: "!!B S. [| ∀A ∈ S. F ∈ A leadsTo B; ∀A ∈ S. P(A,B);
                               st_set(B); ∀A ∈ S. st_set(A)|] ==> P(Union(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) Un 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=Union ({A - B, A Int 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 leadsTo 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(Union(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 leadsTo zb;
          P(zb);
          !!A B. [| F ∈ A ensures B;  F ∈ B leadsTo zb;  P(B); st_set(A) |] ==> P(A);
          !!S. ∀A ∈ S. F ∈ A leadsTo zb & P(A) & st_set(A) ==> P(Union(S))
       |] ==> P(za)"
    apply (subgoal_tac " (F ∈ za leadsTo 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 leadsTo 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 leadsTo A'; F ∈ stable(B) |] ==> F:(A Int B) leadsTo (A' Int B)"
    apply (unfold 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 leadsTo A'; F ∈ stable(B) |]==>F: (B Int A) leadsTo (B Int 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 Int B') ensures ((A' Int B) Un (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 leadsTo A'; F ∈ B co B'; st_set(B')|]==> F:(A Int B') leadsTo ((A' Int B) Un (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 leadsTo A'; F ∈ B co B'; st_set(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'; st_set(B); st_set(B') |]
        ==> F ∈ (A Int B) leadsTo ((A' Int B) Un 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)
    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 Int f-``{m}) leadsTo
                        ((A Int f-``(converse(r)``{m})) Un B) |]
          ==> F ∈ (A Int f-``{m}) leadsTo B"
    apply (erule_tac a = m in wf_induct2, simp_all)
    apply (subgoal_tac "F ∈ (A Int (f-`` (converse (r) ``{x}))) leadsTo 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 Int f-``{m}) leadsTo
                        ((A Int f-``(converse(r)``{m})) Un B) |]
          ==> F ∈ A leadsTo 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 (simp add: measure_def)
    apply (rule equalityI, force, clarify)
    apply (erule_tac V = "x∉range (?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 Int f-`(lessThan m)) leadsTo B*)
    lemma lessThan_induct:
     "[| A<=f-``nat;
         F ∈ program; st_set(A); st_set(B);
         ∀m ∈ nat. F:(A Int f-``{m}) leadsTo ((A Int f -`` m) Un B) |]
          ==> F ∈ A leadsTo 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))"
    apply (unfold st_set_def)
    apply (rule wlt_type)
    done
    declare wlt_st_set [iff]

    lemma wlt_leadsTo_iff: "F ∈ wlt(F, B) leadsTo B <-> (F ∈ program & st_set(B))"
    apply (unfold wlt_def)
    apply (blast dest: leadsToD2 intro!: leadsTo_Union)
    done

    (* [| F ∈ program;  st_set(B) |] ==> F ∈ wlt(F, B) leadsTo B  *)
    lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2], standard]

    lemma leadsTo_subset: "F ∈ A leadsTo B ==> A <= wlt(F, B)"
    apply (unfold wlt_def)
    apply (frule leadsToD2)
    apply (auto simp add: st_set_def)
    done

    (*Misra's property W2*)
    lemma leadsTo_eq_subset_wlt: "F ∈ A leadsTo 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 Un B);
           F ∈ (A2 - C) co (A2 Un C) |]
        ==> F ∈ (A1 Un A2 - C) co (A1 Un A2 Un 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 leadsTo A'
          ==> ∃B ∈ Pow(state). A<=B & F ∈ B leadsTo A' & F ∈ (B-A') co (B Un 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 Un 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 leadsTo B & F ∈ Ba - B co Ba Un 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 = "\<Union>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' 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 "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 Un B' Un 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 Int W - C) leadsTo (A' Int W Un C) ")
     prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
    (** step 13 **)
    apply (subgoal_tac "F ∈ (A' Int W Un C) leadsTo (A' Int B' Un 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 Int B <= A Int 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' Un C" in wlt_leadsTo[THEN psp2, THEN leadsTo_weaken])
    apply blast+
    done

    lemmas completion = refl [THEN completion_aux, standard]

    lemma finite_completion_aux:
         "[| I ∈ Fin(X); F ∈ program; st_set(C) |] ==>
           (∀i ∈ I. F ∈ (A(i)) leadsTo (A'(i) Un C)) -->
                         (∀i ∈ I. F ∈ (A'(i)) co (A'(i) Un C)) -->
                       F ∈ (\<Inter>i ∈ I. A(i)) leadsTo ((\<Inter>i ∈ I. A'(i)) Un 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) leadsTo (A'(i) Un C);
             !!i. i ∈ I ==> F ∈ A'(i) co (A'(i) Un C); F ∈ program; st_set(C)|]
          ==> F ∈ (\<Inter>i ∈ I. A(i)) leadsTo ((\<Inter>i ∈ I. A'(i)) Un C)"
    by (blast intro: finite_completion_aux [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 = 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) leadsTo A'(i));
             (!!i. i ∈ I ==> F ∈ stable(A'(i)));  F ∈ program |]
          ==> F ∈ (\<Inter>i ∈ I. A(i)) leadsTo (\<Inter>i ∈ I. A'(i))"
    apply (unfold stable_def)
    apply (subgoal_tac "st_set (\<Inter>i ∈ I. A' (i))")
    prefer 2 apply (blast dest: leadsToD2)
    apply (rule_tac C1 = 0 in finite_completion [THEN leadsTo_weaken_R], auto)
    done

    ML
    {*
    val Int_Union_Union = thm "Int_Union_Union";
    val Int_Union_Union2 = thm "Int_Union_Union2";
    val transient_type = thm "transient_type";
    val transientD2 = thm "transientD2";
    val stable_transient_empty = thm "stable_transient_empty";
    val transient_strengthen = thm "transient_strengthen";
    val transientI = thm "transientI";
    val transientE = thm "transientE";
    val transient_state = thm "transient_state";
    val transient_state2 = thm "transient_state2";
    val transient_empty = thm "transient_empty";
    val ensures_type = thm "ensures_type";
    val ensuresI = thm "ensuresI";
    val ensuresI2 = thm "ensuresI2";
    val ensuresD = thm "ensuresD";
    val ensures_weaken_R = thm "ensures_weaken_R";
    val stable_ensures_Int = thm "stable_ensures_Int";
    val stable_transient_ensures = thm "stable_transient_ensures";
    val ensures_eq = thm "ensures_eq";
    val subset_imp_ensures = thm "subset_imp_ensures";
    val leads_left = thm "leads_left";
    val leads_right = thm "leads_right";
    val leadsTo_type = thm "leadsTo_type";
    val leadsToD2 = thm "leadsToD2";
    val leadsTo_Basis = thm "leadsTo_Basis";
    val subset_imp_leadsTo = thm "subset_imp_leadsTo";
    val leadsTo_Trans = thm "leadsTo_Trans";
    val transient_imp_leadsTo = thm "transient_imp_leadsTo";
    val leadsTo_Un_duplicate = thm "leadsTo_Un_duplicate";
    val leadsTo_Un_duplicate2 = thm "leadsTo_Un_duplicate2";
    val leadsTo_Union = thm "leadsTo_Union";
    val leadsTo_Union_Int = thm "leadsTo_Union_Int";
    val leadsTo_UN = thm "leadsTo_UN";
    val leadsTo_Un = thm "leadsTo_Un";
    val single_leadsTo_I = thm "single_leadsTo_I";
    val leadsTo_refl = thm "leadsTo_refl";
    val leadsTo_refl_iff = thm "leadsTo_refl_iff";
    val empty_leadsTo = thm "empty_leadsTo";
    val leadsTo_state = thm "leadsTo_state";
    val leadsTo_weaken_R = thm "leadsTo_weaken_R";
    val leadsTo_weaken_L = thm "leadsTo_weaken_L";
    val leadsTo_weaken = thm "leadsTo_weaken";
    val transient_imp_leadsTo2 = thm "transient_imp_leadsTo2";
    val leadsTo_Un_distrib = thm "leadsTo_Un_distrib";
    val leadsTo_UN_distrib = thm "leadsTo_UN_distrib";
    val leadsTo_Union_distrib = thm "leadsTo_Union_distrib";
    val leadsTo_Diff = thm "leadsTo_Diff";
    val leadsTo_UN_UN = thm "leadsTo_UN_UN";
    val leadsTo_Un_Un = thm "leadsTo_Un_Un";
    val leadsTo_cancel2 = thm "leadsTo_cancel2";
    val leadsTo_cancel_Diff2 = thm "leadsTo_cancel_Diff2";
    val leadsTo_cancel1 = thm "leadsTo_cancel1";
    val leadsTo_cancel_Diff1 = thm "leadsTo_cancel_Diff1";
    val leadsTo_induct = thm "leadsTo_induct";
    val leadsTo_induct2 = thm "leadsTo_induct2";
    val leadsTo_induct_pre_aux = thm "leadsTo_induct_pre_aux";
    val leadsTo_induct_pre = thm "leadsTo_induct_pre";
    val leadsTo_empty = thm "leadsTo_empty";
    val psp_stable = thm "psp_stable";
    val psp_stable2 = thm "psp_stable2";
    val psp_ensures = thm "psp_ensures";
    val psp = thm "psp";
    val psp2 = thm "psp2";
    val psp_unless = thm "psp_unless";
    val leadsTo_wf_induct_aux = thm "leadsTo_wf_induct_aux";
    val leadsTo_wf_induct = thm "leadsTo_wf_induct";
    val nat_measure_field = thm "nat_measure_field";
    val Image_inverse_lessThan = thm "Image_inverse_lessThan";
    val lessThan_induct = thm "lessThan_induct";
    val wlt_type = thm "wlt_type";
    val wlt_st_set = thm "wlt_st_set";
    val wlt_leadsTo_iff = thm "wlt_leadsTo_iff";
    val wlt_leadsTo = thm "wlt_leadsTo";
    val leadsTo_subset = thm "leadsTo_subset";
    val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt";
    val wlt_increasing = thm "wlt_increasing";
    val leadsTo_123_aux = thm "leadsTo_123_aux";
    val leadsTo_123 = thm "leadsTo_123";
    val wlt_constrains_wlt = thm "wlt_constrains_wlt";
    val completion_aux = thm "completion_aux";
    val completion = thm "completion";
    val finite_completion_aux = thm "finite_completion_aux";
    val finite_completion = thm "finite_completion";
    val stable_completion = thm "stable_completion";
    val finite_stable_completion = thm "finite_stable_completion";
    *}

    end

lemma Int_Union_Union:

      \<Union>B ∩ A = (\<Union>b∈B. b ∩ A)

lemma Int_Union_Union2:

      A ∩ \<Union>B = (\<Union>b∈B. A ∩ b)

lemma transient_type:

      transient(A) ⊆ program

lemma transientD2:

      F ∈ transient(A) ==> F ∈ program ∧ st_set(A)

lemma stable_transient_empty:

      [| F ∈ stable(A); F ∈ transient(A) |] ==> A = 0

lemma transient_strengthen:

      [| F ∈ transient(A); B ⊆ A |] ==> F ∈ transient(B)

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

lemma transient_state2:

      state ⊆ B ==> transient(B) = 0

lemma transient_empty:

      transient(0) = program

lemma ensures_type:

      A ensures B ⊆ program

lemma ensuresI:

      [| F ∈ A - B co A ∪ B; F ∈ transient(A - B) |] ==> F ∈ A ensures B

lemma ensuresI2:

      [| F ∈ A co A ∪ B; F ∈ transient(A) |] ==> F ∈ A ensures B

lemma ensuresD:

      F ∈ A ensures B ==> F ∈ A - B co A ∪ B ∧ F ∈ transient(A - B)

lemma ensures_weaken_R:

      [| F ∈ A ensures A'; A' ⊆ B' |] ==> F ∈ A ensures B'

lemma stable_ensures_Int:

      [| F ∈ stable(C); F ∈ A ensures B |] ==> F ∈ C ∩ A ensures C ∩ B

lemma stable_transient_ensures:

      [| F ∈ stable(A); F ∈ transient(C); A ⊆ B ∪ C |] ==> F ∈ A ensures B

lemma ensures_eq:

      A ensures B = (A unless B) ∩ transient(A - B)

lemma subset_imp_ensures:

      [| F ∈ program; A ⊆ B |] ==> F ∈ A ensures B

lemmas leads_left:

      ⟨a, b⟩ ∈ leads(D2, F2) ==> a ∈ Pow(D2)

lemmas leads_left:

      ⟨a, b⟩ ∈ leads(D2, F2) ==> a ∈ Pow(D2)

lemmas leads_right:

      ⟨a, b⟩ ∈ leads(D2, F2) ==> b ∈ Pow(D2)

lemmas leads_right:

      ⟨a, b⟩ ∈ leads(D2, F2) ==> b ∈ Pow(D2)

lemma leadsTo_type:

      A leadsTo B ⊆ program

lemma leadsToD2:

      F ∈ A leadsTo B ==> F ∈ program ∧ st_set(A) ∧ st_set(B)

lemma leadsTo_Basis:

      [| F ∈ A ensures B; st_set(A); st_set(B) |] ==> F ∈ A leadsTo B

lemmas subset_imp_leadsTo:

      [| F ∈ program; A ⊆ B; st_set(A); st_set(B) |] ==> F ∈ A leadsTo B

lemmas subset_imp_leadsTo:

      [| F ∈ program; A ⊆ B; st_set(A); st_set(B) |] ==> F ∈ A leadsTo B

lemma leadsTo_Trans:

      [| F ∈ A leadsTo B; F ∈ B leadsTo C |] ==> F ∈ A leadsTo C

lemma transient_imp_leadsTo:

      F ∈ transient(A) ==> F ∈ A leadsTo state - A

lemma leadsTo_Un_duplicate:

      F ∈ A leadsTo A' ∪ A' ==> F ∈ A leadsTo A'

lemma leadsTo_Un_duplicate2:

      F ∈ A leadsTo A' ∪ C ∪ C ==> F ∈ A leadsTo A' ∪ C

lemma leadsTo_Union:

      [| !!A. A ∈ S ==> F ∈ A leadsTo B; F ∈ program; st_set(B) |]
      ==> F ∈ \<Union>S leadsTo B

lemma leadsTo_Union_Int:

      [| !!A. A ∈ S ==> F ∈ A ∩ C leadsTo B; F ∈ program; st_set(B) |]
      ==> F ∈ \<Union>S ∩ C leadsTo B

lemma leadsTo_UN:

      [| !!i. i ∈ I ==> F ∈ A(i) leadsTo B; F ∈ program; st_set(B) |]
      ==> F ∈ (\<Union>i∈I. A(i)) leadsTo B

lemma leadsTo_Un:

      [| F ∈ A leadsTo C; F ∈ B leadsTo C |] ==> F ∈ A ∪ B leadsTo C

lemma single_leadsTo_I:

      [| !!x. x ∈ A ==> F ∈ {x} leadsTo B; F ∈ program; st_set(B) |]
      ==> F ∈ A leadsTo B

lemma leadsTo_refl:

      [| F ∈ program; st_set(A) |] ==> F ∈ A leadsTo A

lemma leadsTo_refl_iff:

      F ∈ A leadsTo A <-> F ∈ program ∧ st_set(A)

lemma empty_leadsTo:

      F ∈ 0 leadsTo B <-> F ∈ program ∧ st_set(B)

lemma leadsTo_state:

      F ∈ A leadsTo state <-> F ∈ program ∧ st_set(A)

lemma leadsTo_weaken_R:

      [| F ∈ A leadsTo A'; A' ⊆ B'; st_set(B') |] ==> F ∈ A leadsTo B'

lemma leadsTo_weaken_L:

      [| F ∈ A leadsTo A'; B ⊆ A |] ==> F ∈ B leadsTo A'

lemma leadsTo_weaken:

      [| F ∈ A leadsTo A'; B ⊆ A; A' ⊆ B'; st_set(B') |] ==> F ∈ B leadsTo B'

lemma transient_imp_leadsTo2:

      [| F ∈ transient(A); state - A ⊆ B; st_set(B) |] ==> F ∈ A leadsTo B

lemma leadsTo_Un_distrib:

      F ∈ A ∪ B leadsTo C <-> F ∈ A leadsTo C ∧ F ∈ B leadsTo C

lemma leadsTo_UN_distrib:

      F ∈ (\<Union>i∈I. A(i)) leadsTo B <->
      (∀i∈I. F ∈ A(i) leadsTo B) ∧ F ∈ program ∧ st_set(B)

lemma leadsTo_Union_distrib:

      F ∈ \<Union>S leadsTo B <-> (∀A∈S. F ∈ A leadsTo B) ∧ F ∈ program ∧ st_set(B)

lemma leadsTo_Diff:

      [| F ∈ A - B leadsTo C; F ∈ B leadsTo C; st_set(C) |] ==> F ∈ A leadsTo C

lemma leadsTo_UN_UN:

      [| !!i. i ∈ I ==> F ∈ A(i) leadsTo A'(i); F ∈ program |]
      ==> F ∈ (\<Union>i∈I. A(i)) leadsTo (\<Union>i∈I. A'(i))

lemma leadsTo_Un_Un:

      [| F ∈ A leadsTo A'; F ∈ B leadsTo B' |] ==> F ∈ A ∪ B leadsTo A' ∪ B'

lemma leadsTo_cancel2:

      [| F ∈ A leadsTo A' ∪ B; F ∈ B leadsTo B' |] ==> F ∈ A leadsTo A' ∪ B'

lemma leadsTo_cancel_Diff2:

      [| F ∈ A leadsTo A' ∪ B; F ∈ B - A' leadsTo B' |] ==> F ∈ A leadsTo A' ∪ B'

lemma leadsTo_cancel1:

      [| F ∈ A leadsTo B ∪ A'; F ∈ B leadsTo B' |] ==> F ∈ A leadsTo B' ∪ A'

lemma leadsTo_cancel_Diff1:

      [| F ∈ A leadsTo B ∪ A'; F ∈ B - A' leadsTo B' |] ==> F ∈ A leadsTo B' ∪ A'

lemma leadsTo_induct:

      [| F ∈ za leadsTo zb;
         !!A B. [| F ∈ A ensures B; st_set(A); st_set(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. [| ∀A∈S. F ∈ A leadsTo B; ∀A∈S. P(A, B); st_set(B); ∀A∈S. st_set(A) |]
                ==> P(\<Union>S, B) |]
      ==> P(za, zb)

lemma leadsTo_induct2:

      [| F ∈ za leadsTo zb; !!A B. [| A ⊆ B; st_set(B) |] ==> P(A, B);
         !!A B. [| F ∈ A co A ∪ B; F ∈ transient(A); st_set(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. [| ∀A∈S. F ∈ A leadsTo B; ∀A∈S. P(A, B); st_set(B); ∀A∈S. st_set(A) |]
                ==> P(\<Union>S, B) |]
      ==> P(za, zb)

lemma leadsTo_induct_pre_aux:

      [| F ∈ za leadsTo 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(\<Union>S) |]
      ==> P(za)

lemma leadsTo_induct_pre:

      [| F ∈ za leadsTo zb; P(zb);
         !!A B. [| F ∈ A ensures B; F ∈ B leadsTo zb; P(B); st_set(A) |] ==> P(A);
         !!S. ∀A∈S. F ∈ A leadsTo zb ∧ P(A) ∧ st_set(A) ==> P(\<Union>S) |]
      ==> P(za)

lemma leadsTo_empty:

      F ∈ A leadsTo 0 ==> A = 0

### PSP: Progress-Safety-Progress

lemma psp_stable:

      [| F ∈ A leadsTo A'; F ∈ stable(B) |] ==> F ∈ A ∩ B leadsTo A' ∩ B

lemma psp_stable2:

      [| F ∈ A leadsTo A'; F ∈ stable(B) |] ==> F ∈ B ∩ A leadsTo B ∩ A'

lemma psp_ensures:

      [| F ∈ A ensures A'; F ∈ B co B' |] ==> F ∈ A ∩ B' ensures A' ∩ B ∪ (B' - B)

lemma psp:

      [| F ∈ A leadsTo A'; F ∈ B co B'; st_set(B') |]
      ==> F ∈ A ∩ B' leadsTo A' ∩ B ∪ (B' - B)

lemma psp2:

      [| F ∈ A leadsTo A'; F ∈ B co B'; st_set(B') |]
      ==> F ∈ B' ∩ A leadsTo B ∩ A' ∪ (B' - B)

lemma psp_unless:

      [| F ∈ A leadsTo A'; F ∈ B unless B'; st_set(B); st_set(B') |]
      ==> F ∈ A ∩ B leadsTo A' ∩ B ∪ B'

### Proving the induction rules

lemma leadsTo_wf_induct_aux:

      [| wf(r); m ∈ I; field(r) ⊆ I; F ∈ program; st_set(B);
         ∀m∈I. F ∈ A ∩ f -`` {m} leadsTo A ∩ f -`` (converse(r) `` {m}) ∪ B |]
      ==> F ∈ A ∩ f -`` {m} leadsTo B

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} leadsTo A ∩ f -`` (converse(r) `` {m}) ∪ B |]
      ==> F ∈ A leadsTo B

lemma nat_measure_field:

      field(measure(nat, %x. x)) = nat

lemma Image_inverse_lessThan:

      k < A ==> measure(A, %x. x) -`` {k} = k

lemma lessThan_induct:

      [| A ⊆ f -`` nat; F ∈ program; st_set(A); st_set(B);
         ∀m∈nat. F ∈ A ∩ f -`` {m} leadsTo A ∩ f -`` m ∪ B |]
      ==> F ∈ A leadsTo B

lemma wlt_type:

      wlt(F, B) ⊆ state

lemma wlt_st_set:

      st_set(wlt(F, B))

lemma wlt_leadsTo_iff:

      F ∈ wlt(F, B) leadsTo B <-> F ∈ program ∧ st_set(B)

lemmas wlt_leadsTo:

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

lemmas wlt_leadsTo:

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

lemma leadsTo_subset:

      F ∈ A leadsTo B ==> A ⊆ wlt(F, B)

lemma leadsTo_eq_subset_wlt:

      F ∈ A leadsTo B <-> A ⊆ wlt(F, B) ∧ F ∈ program ∧ st_set(B)

lemma wlt_increasing:

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

lemma leadsTo_123_aux:

      [| B ⊆ A2.0; F ∈ A1.0 - B co A1.0 ∪ B; F ∈ A2.0 - C co A2.0 ∪ C |]
      ==> F ∈ A1.0 ∪ A2.0 - C co A1.0 ∪ A2.0 ∪ C

lemma leadsTo_123:

      F ∈ A leadsTo A'
      ==> ∃B∈Pow(state). A ⊆ B ∧ F ∈ B leadsTo A' ∧ F ∈ B - A' co B ∪ A'

lemma wlt_constrains_wlt:

      [| F ∈ program; st_set(B) |] ==> F ∈ wlt(F, B) - B co wlt(F, B)

### Completion: Binary and General Finite versions

lemma completion_aux:

      [| W = wlt(F, B' ∪ C); F ∈ A leadsTo A' ∪ C; F ∈ A' co A' ∪ C;
         F ∈ B leadsTo B' ∪ C; F ∈ B' co B' ∪ C |]
      ==> F ∈ A ∩ B leadsTo A' ∩ B' ∪ C

lemmas completion:

      [| F ∈ A leadsTo A' ∪ C; F ∈ A' co A' ∪ C; F ∈ B leadsTo B' ∪ C;
         F ∈ B' co B' ∪ C |]
      ==> F ∈ A ∩ B leadsTo A' ∩ B' ∪ C

lemmas completion:

      [| F ∈ A leadsTo A' ∪ C; F ∈ A' co A' ∪ C; F ∈ B leadsTo B' ∪ C;
         F ∈ B' co B' ∪ C |]
      ==> F ∈ A ∩ B leadsTo A' ∩ B' ∪ C

lemma finite_completion_aux:

      [| I ∈ Fin(X); F ∈ program; st_set(C) |]
      ==> (∀i∈I. F ∈ A(i) leadsTo A'(i) ∪ C) -->
          (∀i∈I. F ∈ A'(i) co A'(i) ∪ C) -->
          F ∈ (\<Inter>i∈I. A(i)) leadsTo (\<Inter>i∈I. A'(i)) ∪ C

lemma finite_completion:

      [| I ∈ Fin(X); !!i. i ∈ I ==> F ∈ A(i) leadsTo A'(i) ∪ C;
         !!i. i ∈ I ==> F ∈ A'(i) co A'(i) ∪ C; F ∈ program; st_set(C) |]
      ==> F ∈ (\<Inter>i∈I. A(i)) leadsTo (\<Inter>i∈I. A'(i)) ∪ C

lemma stable_completion:

      [| F ∈ A leadsTo A'; F ∈ stable(A'); F ∈ B leadsTo B'; F ∈ stable(B') |]
      ==> F ∈ A ∩ B leadsTo A' ∩ B'

lemma finite_stable_completion:

      [| I ∈ Fin(X); !!i. i ∈ I ==> F ∈ A(i) leadsTo A'(i);
         !!i. i ∈ I ==> F ∈ stable(A'(i)); F ∈ program |]
      ==> F ∈ (\<Inter>i∈I. A(i)) leadsTo (\<Inter>i∈I. A'(i))