# Theory Transformers

Up to index of Isabelle/HOL/UNITY

theory Transformers
imports Comp
begin

    (*  Title:      HOL/UNITY/Transformers
        ID:         $Id: Transformers.thy,v 1.10 2005/06/17 14:13:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   2003  University of Cambridge

    Predicate Transformers.  From

        David Meier and Beverly Sanders,
        Composing Leads-to Properties
        Theoretical Computer Science 243:1-2 (2000), 339-361.

        David Meier,
        Progress Properties in Program Refinement and Parallel Composition
        Swiss Federal Institute of Technology Zurich (1997)
    *)

    header{*Predicate Transformers*}

    theory Transformers imports Comp begin

    subsection{*Defining the Predicate Transformers @{term wp},
       @{term awp} and  @{term wens}*}

    constdefs
      wp :: "[('a*'a) set, 'a set] => 'a set"
        --{*Dijkstra's weakest-precondition operator (for an individual command)*}
        "wp act B == - (act^-1 `` (-B))"

      awp :: "['a program, 'a set] => 'a set"
        --{*Dijkstra's weakest-precondition operator (for a program)*}
        "awp F B == (\<Inter>act ∈ Acts F. wp act B)"

      wens :: "['a program, ('a*'a) set, 'a set] => 'a set"
        --{*The weakest-ensures transformer*}
        "wens F act B == gfp(λX. (wp act B ∩ awp F (B ∪ X)) ∪ B)"

    text{*The fundamental theorem for wp*}
    theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
    by (force simp add: wp_def)

    text{*This lemma is a good deal more intuitive than the definition!*}
    lemma in_wp_iff: "(a ∈ wp act B) = (∀x. (a,x) ∈ act --> x ∈ B)"
    by (simp add: wp_def, blast)

    lemma Compl_Domain_subset_wp: "- (Domain act) ⊆ wp act B"
    by (force simp add: wp_def)

    lemma wp_empty [simp]: "wp act {} = - (Domain act)"
    by (force simp add: wp_def)

    text{*The identity relation is the skip action*}
    lemma wp_Id [simp]: "wp Id B = B"
    by (simp add: wp_def)

    lemma wp_totalize_act:
         "wp (totalize_act act) B = (wp act B ∩ Domain act) ∪ (B - Domain act)"
    by (simp add: wp_def totalize_act_def, blast)

    lemma awp_subset: "(awp F A ⊆ A)"
    by (force simp add: awp_def wp_def)

    lemma awp_Int_eq: "awp F (A∩B) = awp F A ∩ awp F B"
    by (simp add: awp_def wp_def, blast)

    text{*The fundamental theorem for awp*}
    theorem awp_iff_constrains: "(A <= awp F B) = (F ∈ A co B)"
    by (simp add: awp_def constrains_def wp_iff INT_subset_iff)

    lemma awp_iff_stable: "(A ⊆ awp F A) = (F ∈ stable A)"
    by (simp add: awp_iff_constrains stable_def)

    lemma stable_imp_awp_ident: "F ∈ stable A ==> awp F A = A"
    apply (rule equalityI [OF awp_subset])
    apply (simp add: awp_iff_stable)
    done

    lemma wp_mono: "(A ⊆ B) ==> wp act A ⊆ wp act B"
    by (simp add: wp_def, blast)

    lemma awp_mono: "(A ⊆ B) ==> awp F A ⊆ awp F B"
    by (simp add: awp_def wp_def, blast)

    lemma wens_unfold:
         "wens F act B = (wp act B ∩ awp F (B ∪ wens F act B)) ∪ B"
    apply (simp add: wens_def)
    apply (rule gfp_unfold)
    apply (simp add: mono_def wp_def awp_def, blast)
    done

    lemma wens_Id [simp]: "wens F Id B = B"
    by (simp add: wens_def gfp_def wp_def awp_def, blast)

    text{*These two theorems justify the claim that @{term wens} returns the
    weakest assertion satisfying the ensures property*}
    lemma ensures_imp_wens: "F ∈ A ensures B ==> ∃act ∈ Acts F. A ⊆ wens F act B"
    apply (simp add: wens_def ensures_def transient_def, clarify)
    apply (rule rev_bexI, assumption)
    apply (rule gfp_upperbound)
    apply (simp add: constrains_def awp_def wp_def, blast)
    done

    lemma wens_ensures: "act ∈ Acts F ==> F ∈ (wens F act B) ensures B"
    by (simp add: wens_def gfp_def constrains_def awp_def wp_def
                  ensures_def transient_def, blast)

    text{*These two results constitute assertion (4.13) of the thesis*}
    lemma wens_mono: "(A ⊆ B) ==> wens F act A ⊆ wens F act B"
    apply (simp add: wens_def wp_def awp_def)
    apply (rule gfp_mono, blast)
    done

    lemma wens_weakening: "B ⊆ wens F act B"
    by (simp add: wens_def gfp_def, blast)

    text{*Assertion (6), or 4.16 in the thesis*}
    lemma subset_wens: "A-B ⊆ wp act B ∩ awp F (B ∪ A) ==> A ⊆ wens F act B"
    apply (simp add: wens_def wp_def awp_def)
    apply (rule gfp_upperbound, blast)
    done

    text{*Assertion 4.17 in the thesis*}
    lemma Diff_wens_constrains: "F ∈ (wens F act A - A) co wens F act A"
    by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
      --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
          is declared as an iff-rule, then it's almost impossible to prove.
          One proof is via @{text meson} after expanding all definitions, but it's
          slow!*}

    text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
    hold for an arbitrary action.  We often do not require @{term "act ∈ Acts F"}*}
    lemma stable_wens: "F ∈ stable A ==> F ∈ stable (wens F act A)"
    apply (simp add: stable_def)
    apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]])
    apply (simp add: Un_Int_distrib2 Compl_partition2)
    apply (erule constrains_weaken, blast)
    apply (simp add: Un_subset_iff wens_weakening)
    done

    text{*Assertion 4.20 in the thesis.*}
    lemma wens_Int_eq_lemma:
          "[|T-B ⊆ awp F T; act ∈ Acts F|]
           ==> T ∩ wens F act B ⊆ wens F act (T∩B)"
    apply (rule subset_wens)
    apply (rule_tac P="λx. ?f x ⊆ ?b" in ssubst [OF wens_unfold])
    apply (simp add: wp_def awp_def, blast)
    done

    text{*Assertion (8): 4.21 in the thesis. Here we indeed require
          @{term "act ∈ Acts F"}*}
    lemma wens_Int_eq:
          "[|T-B ⊆ awp F T; act ∈ Acts F|]
           ==> T ∩ wens F act B = T ∩ wens F act (T∩B)"
    apply (rule equalityI)
     apply (simp_all add: Int_lower1 Int_subset_iff)
     apply (rule wens_Int_eq_lemma, assumption+)
    apply (rule subset_trans [OF _ wens_mono [of "T∩B" B]], auto)
    done

    subsection{*Defining the Weakest Ensures Set*}

    consts
      wens_set :: "['a program, 'a set] => 'a set set"

    inductive "wens_set F B"
     intros

      Basis: "B ∈ wens_set F B"

      Wens:  "[|X ∈ wens_set F B; act ∈ Acts F|] ==> wens F act X ∈ wens_set F B"

      Union: "W ≠ {} ==> ∀U ∈ W. U ∈ wens_set F B ==> \<Union>W ∈ wens_set F B"

    lemma wens_set_imp_co: "A ∈ wens_set F B ==> F ∈ (A-B) co A"
    apply (erule wens_set.induct)
      apply (simp add: constrains_def)
     apply (drule_tac act1=act and A1=X
            in constrains_Un [OF Diff_wens_constrains])
     apply (erule constrains_weaken, blast)
     apply (simp add: Un_subset_iff wens_weakening)
    apply (rule constrains_weaken)
    apply (rule_tac I=W and A="λv. v-B" and A'="λv. v" in constrains_UN, blast+)
    done

    lemma wens_set_imp_leadsTo: "A ∈ wens_set F B ==> F ∈ A leadsTo B"
    apply (erule wens_set.induct)
      apply (rule leadsTo_refl)
     apply (blast intro: wens_ensures leadsTo_Trans)
    apply (blast intro: leadsTo_Union)
    done

    lemma leadsTo_imp_wens_set: "F ∈ A leadsTo B ==> ∃C ∈ wens_set F B. A ⊆ C"
    apply (erule leadsTo_induct_pre)
      apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens)
     apply (clarify, drule ensures_weaken_R, assumption)
     apply (blast dest!: ensures_imp_wens intro: wens_set.Wens)
    apply (case_tac "S={}")
     apply (simp, blast intro: wens_set.Basis)
    apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def)
    apply (rule_tac x = "\<Union>{Z. ∃U∈S. Z = f U}" in exI)
    apply (blast intro: wens_set.Union)
    done

    text{*Assertion (9): 4.27 in the thesis.*}
    lemma leadsTo_iff_wens_set: "(F ∈ A leadsTo B) = (∃C ∈ wens_set F B. A ⊆ C)"
    by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo)

    text{*This is the result that requires the definition of @{term wens_set} to
      require @{term W} to be non-empty in the Unio case, for otherwise we should
      always have @{term "{} ∈ wens_set F B"}.*}
    lemma wens_set_imp_subset: "A ∈ wens_set F B ==> B ⊆ A"
    apply (erule wens_set.induct)
      apply (blast intro: wens_weakening [THEN subsetD])+
    done

    subsection{*Properties Involving Program Union*}

    text{*Assertion (4.30) of thesis, reoriented*}
    lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B ∩ awp G B"
    by (simp add: awp_def wp_def, blast)

    lemma wens_subset: "wens F act B - B ⊆ wp act B ∩ awp F (B ∪ wens F act B)"
    by (subst wens_unfold, fast)

    text{*Assertion (4.31)*}
    lemma subset_wens_Join:
          "[|A = T ∩ wens F act B;  T-B ⊆ awp F T; A-B ⊆ awp G (A ∪ B)|]
           ==> A ⊆ wens (F\<squnion>G) act B"
    apply (subgoal_tac "(T ∩ wens F act B) - B ⊆
                        wp act B ∩ awp F (B ∪ wens F act B) ∩ awp F T")
     apply (rule subset_wens)
     apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
     apply (simp add: awp_def wp_def, blast)
    apply (insert wens_subset [of F act B], blast)
    done

    text{*Assertion (4.32)*}
    lemma wens_Join_subset: "wens (F\<squnion>G) act B ⊆ wens F act B"
    apply (simp add: wens_def)
    apply (rule gfp_mono)
    apply (auto simp add: awp_Join_eq)
    done

    text{*Lemma, because the inductive step is just too messy.*}
    lemma wens_Union_inductive_step:
      assumes awpF: "T-B ⊆ awp F T"
          and awpG: "!!X. X ∈ wens_set F B ==> (T∩X) - B ⊆ awp G (T∩X)"
      shows "[|X ∈ wens_set F B; act ∈ Acts F; Y ⊆ X; T∩X = T∩Y|]
             ==> wens (F\<squnion>G) act Y ⊆ wens F act X ∧
                 T ∩ wens F act X = T ∩ wens (F\<squnion>G) act Y"
    apply (subgoal_tac "wens (F\<squnion>G) act Y ⊆ wens F act X")
     prefer 2
     apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
    apply (rule equalityI)
     prefer 2 apply blast
    apply (simp add: Int_lower1 Int_subset_iff)
    apply (frule wens_set_imp_subset)
    apply (subgoal_tac "T-X ⊆ awp F T")
     prefer 2 apply (blast intro: awpF [THEN subsetD])
    apply (rule_tac B = "wens (F\<squnion>G) act (T∩X)" in subset_trans)
     prefer 2 apply (blast intro!: wens_mono)
    apply (subst wens_Int_eq, assumption+)
    apply (rule subset_wens_Join [of _ T], simp, blast)
    apply (subgoal_tac "T ∩ wens F act (T∩X) ∪ T∩X = T ∩ wens F act X")
     prefer 2
     apply (subst wens_Int_eq [symmetric], assumption+)
     apply (blast intro: wens_weakening [THEN subsetD], simp)
    apply (blast intro: awpG [THEN subsetD] wens_set.Wens)
    done

    theorem wens_Union:
      assumes awpF: "T-B ⊆ awp F T"
          and awpG: "!!X. X ∈ wens_set F B ==> (T∩X) - B ⊆ awp G (T∩X)"
          and major: "X ∈ wens_set F B"
      shows "∃Y ∈ wens_set (F\<squnion>G) B. Y ⊆ X & T∩X = T∩Y"
    apply (rule wens_set.induct [OF major])
      txt{*Basis: trivial*}
      apply (blast intro: wens_set.Basis)
     txt{*Inductive step*}
     apply clarify
     apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI)
      apply (force intro: wens_set.Wens)
     apply (simp add: wens_Union_inductive_step [OF awpF awpG])
    txt{*Union: by Axiom of Choice*}
    apply (simp add: ball_conj_distrib Bex_def)
    apply (clarify dest!: bchoice)
    apply (rule_tac x = "\<Union>{Z. ∃U∈W. Z = f U}" in exI)
    apply (blast intro: wens_set.Union)
    done

    theorem leadsTo_Join:
      assumes leadsTo: "F ∈ A leadsTo B"
          and awpF: "T-B ⊆ awp F T"
          and awpG: "!!X. X ∈ wens_set F B ==> (T∩X) - B ⊆ awp G (T∩X)"
      shows "F\<squnion>G ∈ T∩A leadsTo B"
    apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE])
    apply (rule wens_Union [THEN bexE])
       apply (rule awpF)
      apply (erule awpG, assumption)
    apply (blast intro: wens_set_imp_leadsTo [THEN leadsTo_weaken_L])
    done

    subsection {*The Set @{term "wens_set F B"} for a Single-Assignment Program*}
    text{*Thesis Section 4.3.3*}

    text{*We start by proving laws about single-assignment programs*}
    lemma awp_single_eq [simp]:
         "awp (mk_program (init, {act}, allowed)) B = B ∩ wp act B"
    by (force simp add: awp_def wp_def)

    lemma wp_Un_subset: "wp act A ∪ wp act B ⊆ wp act (A ∪ B)"
    by (force simp add: wp_def)

    lemma wp_Un_eq: "single_valued act ==> wp act (A ∪ B) = wp act A ∪ wp act B"
    apply (rule equalityI)
     apply (force simp add: wp_def single_valued_def)
    apply (rule wp_Un_subset)
    done

    lemma wp_UN_subset: "(\<Union>i∈I. wp act (A i)) ⊆ wp act (\<Union>i∈I. A i)"
    by (force simp add: wp_def)

    lemma wp_UN_eq:
         "[|single_valued act; I≠{}|]
          ==> wp act (\<Union>i∈I. A i) = (\<Union>i∈I. wp act (A i))"
    apply (rule equalityI)
     prefer 2 apply (rule wp_UN_subset)
     apply (simp add: wp_def Image_INT_eq)
    done

    lemma wens_single_eq:
         "wens (mk_program (init, {act}, allowed)) act B = B ∪ wp act B"
    by (simp add: wens_def gfp_def wp_def, blast)

    text{*Next, we express the @{term "wens_set"} for single-assignment programs*}

    constdefs
      wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"
        "wens_single_finite act B k == \<Union>i ∈ atMost k. ((wp act)^i) B"

      wens_single :: "[('a*'a) set, 'a set] => 'a set"
        "wens_single act B == \<Union>i. ((wp act)^i) B"

    lemma wens_single_Un_eq:
          "single_valued act
           ==> wens_single act B ∪ wp act (wens_single act B) = wens_single act B"
    apply (rule equalityI)
     apply (simp_all add: Un_upper1 Un_subset_iff)
    apply (simp add: wens_single_def wp_UN_eq, clarify)
    apply (rule_tac a="Suc(i)" in UN_I, auto)
    done

    lemma atMost_nat_nonempty: "atMost (k::nat) ≠ {}"
    by force

    lemma wens_single_finite_0 [simp]: "wens_single_finite act B 0 = B"
    by (simp add: wens_single_finite_def)

    lemma wens_single_finite_Suc:
          "single_valued act
           ==> wens_single_finite act B (Suc k) =
               wens_single_finite act B k ∪ wp act (wens_single_finite act B k)"
    apply (simp add: wens_single_finite_def image_def
                     wp_UN_eq [OF _ atMost_nat_nonempty])
    apply (force elim!: le_SucE)
    done

    lemma wens_single_finite_Suc_eq_wens:
         "single_valued act
           ==> wens_single_finite act B (Suc k) =
               wens (mk_program (init, {act}, allowed)) act
                    (wens_single_finite act B k)"
    by (simp add: wens_single_finite_Suc wens_single_eq)

    lemma def_wens_single_finite_Suc_eq_wens:
         "[|F = mk_program (init, {act}, allowed); single_valued act|]
           ==> wens_single_finite act B (Suc k) =
               wens F act (wens_single_finite act B k)"
    by (simp add: wens_single_finite_Suc_eq_wens)

    lemma wens_single_finite_Un_eq:
          "single_valued act
           ==> wens_single_finite act B k ∪ wp act (wens_single_finite act B k)
               ∈ range (wens_single_finite act B)"
    by (simp add: wens_single_finite_Suc [symmetric])

    lemma wens_single_eq_Union:
          "wens_single act B = \<Union>range (wens_single_finite act B)"
    by (simp add: wens_single_finite_def wens_single_def, blast)

    lemma wens_single_finite_eq_Union:
         "wens_single_finite act B n = (\<Union>k∈atMost n. wens_single_finite act B k)"
    apply (auto simp add: wens_single_finite_def)
    apply (blast intro: le_trans)
    done

    lemma wens_single_finite_mono:
         "m ≤ n ==> wens_single_finite act B m ⊆ wens_single_finite act B n"
    by (force simp add:  wens_single_finite_eq_Union [of act B n])

    lemma wens_single_finite_subset_wens_single:
          "wens_single_finite act B k ⊆ wens_single act B"
    by (simp add: wens_single_eq_Union, blast)

    lemma subset_wens_single_finite:
          "[|W ⊆ wens_single_finite act B ` (atMost k); single_valued act; W≠{}|]
           ==> ∃m. \<Union>W = wens_single_finite act B m"
    apply (induct k)
     apply (rule_tac x=0 in exI, simp, blast)
    apply (auto simp add: atMost_Suc)
    apply (case_tac "wens_single_finite act B (Suc k) ∈ W")
     prefer 2 apply blast
    apply (drule_tac x="Suc k" in spec)
    apply (erule notE, rule equalityI)
     prefer 2 apply blast
    apply (subst wens_single_finite_eq_Union)
    apply (simp add: atMost_Suc, blast)
    done

    text{*lemma for Union case*}
    lemma Union_eq_wens_single:
          "[|∀k. ¬ W ⊆ wens_single_finite act B ` {..k};
            W ⊆ insert (wens_single act B)
                (range (wens_single_finite act B))|]
           ==> \<Union>W = wens_single act B"
    apply (case_tac "wens_single act B ∈ W")
     apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD])
    apply (simp add: wens_single_eq_Union)
    apply (rule equalityI, blast)
    apply (simp add: UN_subset_iff, clarify)
    apply (subgoal_tac "∃y∈W. ∃n. y = wens_single_finite act B n & i≤n")
     apply (blast intro: wens_single_finite_mono [THEN subsetD])
    apply (drule_tac x=i in spec)
    apply (force simp add: atMost_def)
    done

    lemma wens_set_subset_single:
          "single_valued act
           ==> wens_set (mk_program (init, {act}, allowed)) B ⊆
               insert (wens_single act B) (range (wens_single_finite act B))"
    apply (rule subsetI)
    apply (erule wens_set.induct)
      txt{*Basis*}
      apply (force simp add: wens_single_finite_def)
     txt{*Wens inductive step*}
     apply (case_tac "acta = Id", simp)
     apply (simp add: wens_single_eq)
     apply (elim disjE)
     apply (simp add: wens_single_Un_eq)
     apply (force simp add: wens_single_finite_Un_eq)
    txt{*Union inductive step*}
    apply (case_tac "∃k. W ⊆ wens_single_finite act B ` (atMost k)")
     apply (blast dest!: subset_wens_single_finite, simp)
    apply (rule disjI1 [OF Union_eq_wens_single], blast+)
    done

    lemma wens_single_finite_in_wens_set:
          "single_valued act ==>
             wens_single_finite act B k
             ∈ wens_set (mk_program (init, {act}, allowed)) B"
    apply (induct_tac k)
     apply (simp add: wens_single_finite_def wens_set.Basis)
    apply (simp add: wens_set.Wens
                     wens_single_finite_Suc_eq_wens [of act B _ init allowed])
    done

    lemma single_subset_wens_set:
          "single_valued act
           ==> insert (wens_single act B) (range (wens_single_finite act B)) ⊆
               wens_set (mk_program (init, {act}, allowed)) B"
    apply (simp add: wens_single_eq_Union UN_eq)
    apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
    done

    text{*Theorem (4.29)*}
    theorem wens_set_single_eq:
         "[|F = mk_program (init, {act}, allowed); single_valued act|]
          ==> wens_set F B =
              insert (wens_single act B) (range (wens_single_finite act B))"
    apply (rule equalityI)
     apply (simp add: wens_set_subset_single)
    apply (erule ssubst, erule single_subset_wens_set)
    done

    text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}

    lemma fp_leadsTo_Join:
        "[|T-B ⊆ awp F T; T-B ⊆ FP G; F ∈ A leadsTo B|] ==> F\<squnion>G ∈ T∩A leadsTo B"
    apply (rule leadsTo_Join, assumption, blast)
    apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast)
    done

    end

### Defining the Predicate Transformers @{term wp}, @{term awp} and @{term wens}

theorem wp_iff:

      (A ⊆ wp act B) = (act `` A ⊆ B)

lemma in_wp_iff:

      (a ∈ wp act B) = (∀x. (a, x) ∈ act --> x ∈ B)

lemma Compl_Domain_subset_wp:

      - Domain act ⊆ wp act B

lemma wp_empty:

      wp act {} = - Domain act

lemma wp_Id:

      wp Id B = B

lemma wp_totalize_act:

      wp (totalize_act act) B = wp act B ∩ Domain act ∪ (B - Domain act)

lemma awp_subset:

      awp F A ⊆ A

lemma awp_Int_eq:

      awp F (A ∩ B) = awp F A ∩ awp F B

theorem awp_iff_constrains:

      (A ⊆ awp F B) = (F ∈ A co B)

lemma awp_iff_stable:

      (A ⊆ awp F A) = (F ∈ stable A)

lemma stable_imp_awp_ident:

      F ∈ stable A ==> awp F A = A

lemma wp_mono:

      A ⊆ B ==> wp act A ⊆ wp act B

lemma awp_mono:

      A ⊆ B ==> awp F A ⊆ awp F B

lemma wens_unfold:

      wens F act B = wp act B ∩ awp F (B ∪ wens F act B) ∪ B

lemma wens_Id:

      wens F Id B = B

lemma ensures_imp_wens:

      F ∈ A ensures B ==> ∃act∈Acts F. A ⊆ wens F act B

lemma wens_ensures:

      act ∈ Acts F ==> F ∈ wens F act B ensures B

lemma wens_mono:

      A ⊆ B ==> wens F act A ⊆ wens F act B

lemma wens_weakening:

      B ⊆ wens F act B

lemma subset_wens:

      A - B ⊆ wp act B ∩ awp F (B ∪ A) ==> A ⊆ wens F act B

lemma Diff_wens_constrains:

      F ∈ wens F act A - A co wens F act A

lemma stable_wens:

      F ∈ stable A ==> F ∈ stable (wens F act A)

lemma wens_Int_eq_lemma:

      [| T - B ⊆ awp F T; act ∈ Acts F |] ==> T ∩ wens F act B ⊆ wens F act (T ∩ B)

lemma wens_Int_eq:

      [| T - B ⊆ awp F T; act ∈ Acts F |]
      ==> T ∩ wens F act B = T ∩ wens F act (T ∩ B)

### Defining the Weakest Ensures Set

lemma wens_set_imp_co:

      A ∈ wens_set F B ==> F ∈ A - B co A

lemma wens_set_imp_leadsTo:

      A ∈ wens_set F B ==> F ∈ A leadsTo B

lemma leadsTo_imp_wens_set:

      F ∈ A leadsTo B ==> ∃C∈wens_set F B. A ⊆ C

lemma leadsTo_iff_wens_set:

      (F ∈ A leadsTo B) = (∃C∈wens_set F B. A ⊆ C)

lemma wens_set_imp_subset:

      A ∈ wens_set F B ==> B ⊆ A

### Properties Involving Program Union

lemma awp_Join_eq:

      awp (F Join G) B = awp F B ∩ awp G B

lemma wens_subset:

      wens F act B - B ⊆ wp act B ∩ awp F (B ∪ wens F act B)

lemma subset_wens_Join:

      [| A = T ∩ wens F act B; T - B ⊆ awp F T; A - B ⊆ awp G (A ∪ B) |]
      ==> A ⊆ wens (F Join G) act B

lemma wens_Join_subset:

      wens (F Join G) act B ⊆ wens F act B

lemma wens_Union_inductive_step:

      [| T - B ⊆ awp F T; !!X. X ∈ wens_set F B ==> T ∩ X - B ⊆ awp G (T ∩ X);
         X ∈ wens_set F B; act ∈ Acts F; Y ⊆ X; T ∩ X = T ∩ Y |]
      ==> wens (F Join G) act Y ⊆ wens F act X ∧
          T ∩ wens F act X = T ∩ wens (F Join G) act Y

theorem wens_Union:

      [| T - B ⊆ awp F T; !!X. X ∈ wens_set F B ==> T ∩ X - B ⊆ awp G (T ∩ X);
         X ∈ wens_set F B |]
      ==> ∃Y∈wens_set (F Join G) B. Y ⊆ X ∧ T ∩ X = T ∩ Y

theorem leadsTo_Join:

      [| F ∈ A leadsTo B; T - B ⊆ awp F T;
         !!X. X ∈ wens_set F B ==> T ∩ X - B ⊆ awp G (T ∩ X) |]
      ==> F Join G ∈ T ∩ A leadsTo B

### The Set @{term "wens_set F B"} for a Single-Assignment Program

lemma awp_single_eq:

      awp (mk_program (init, {act}, allowed)) B = B ∩ wp act B

lemma wp_Un_subset:

      wp act A ∪ wp act B ⊆ wp act (A ∪ B)

lemma wp_Un_eq:

      single_valued act ==> wp act (A ∪ B) = wp act A ∪ wp act B

lemma wp_UN_subset:

      (UN i:I. wp act (A i)) ⊆ wp act (UN i:I. A i)

lemma wp_UN_eq:

      [| single_valued act; I ≠ {} |]
      ==> wp act (UN i:I. A i) = (UN i:I. wp act (A i))

lemma wens_single_eq:

      wens (mk_program (init, {act}, allowed)) act B = B ∪ wp act B

lemma wens_single_Un_eq:

      single_valued act
      ==> wens_single act B ∪ wp act (wens_single act B) = wens_single act B

lemma atMost_nat_nonempty:

      {..k} ≠ {}

lemma wens_single_finite_0:

      wens_single_finite act B 0 = B

lemma wens_single_finite_Suc:

      single_valued act
      ==> wens_single_finite act B (Suc k) =
          wens_single_finite act B k ∪ wp act (wens_single_finite act B k)

lemma wens_single_finite_Suc_eq_wens:

      single_valued act
      ==> wens_single_finite act B (Suc k) =
          wens (mk_program (init, {act}, allowed)) act (wens_single_finite act B k)

lemma def_wens_single_finite_Suc_eq_wens:

      [| F = mk_program (init, {act}, allowed); single_valued act |]
      ==> wens_single_finite act B (Suc k) = wens F act (wens_single_finite act B k)

lemma wens_single_finite_Un_eq:

      single_valued act
      ==> wens_single_finite act B k ∪ wp act (wens_single_finite act B k)
          ∈ range (wens_single_finite act B)

lemma wens_single_eq_Union:

      wens_single act B = Union (range (wens_single_finite act B))

lemma wens_single_finite_eq_Union:

      wens_single_finite act B n = (UN k<=n. wens_single_finite act B k)

lemma wens_single_finite_mono:

      m ≤ n ==> wens_single_finite act B m ⊆ wens_single_finite act B n

lemma wens_single_finite_subset_wens_single:

      wens_single_finite act B k ⊆ wens_single act B

lemma subset_wens_single_finite:

      [| W ⊆ wens_single_finite act B ` {..k}; single_valued act; W ≠ {} |]
      ==> ∃m. Union W = wens_single_finite act B m

lemma Union_eq_wens_single:

      [| ∀k. ¬ W ⊆ wens_single_finite act B ` {..k};
         W ⊆ insert (wens_single act B) (range (wens_single_finite act B)) |]
      ==> Union W = wens_single act B

lemma wens_set_subset_single:

      single_valued act
      ==> wens_set (mk_program (init, {act}, allowed)) B
          ⊆ insert (wens_single act B) (range (wens_single_finite act B))

lemma wens_single_finite_in_wens_set:

      single_valued act
      ==> wens_single_finite act B k ∈ wens_set (mk_program (init, {act}, allowed)) B

lemma single_subset_wens_set:

      single_valued act
      ==> insert (wens_single act B) (range (wens_single_finite act B))
          ⊆ wens_set (mk_program (init, {act}, allowed)) B

theorem wens_set_single_eq:

      [| F = mk_program (init, {act}, allowed); single_valued act |]
      ==> wens_set F B = insert (wens_single act B) (range (wens_single_finite act B))

lemma fp_leadsTo_Join:

      [| T - B ⊆ awp F T; T - B ⊆ FP G; F ∈ A leadsTo B |]
      ==> F Join G ∈ T ∩ A leadsTo B