(* 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
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)
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
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
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