# Theory Transformers

theory Transformers
imports Comp
```(*  Title:      HOL/UNITY/Transformers.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Predicate Transformers.  From

David Meier and Beverly Sanders,
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)
*)

section‹Predicate Transformers›

theory Transformers imports Comp begin

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

definition wp :: "[('a*'a) set, 'a set] => 'a set" where
― ‹Dijkstra's weakest-precondition operator (for an individual command)›
"wp act B == - (act¯ `` (-B))"

definition awp :: "['a program, 'a set] => 'a set" where
― ‹Dijkstra's weakest-precondition operator (for a program)›
"awp F B == (⋂act ∈ Acts F. wp act B)"

definition wens :: "['a program, ('a*'a) set, 'a set] => 'a set" where
― ‹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)"

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

lemma Compl_Domain_subset_wp: "- (Domain act) ⊆ wp act B"

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

text‹The identity relation is the skip action›
lemma wp_Id [simp]: "wp Id B = B"

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

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

lemma wp_mono: "(A ⊆ B) ==> wp act A ⊆ wp act B"

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 (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 ‹Un_subset_iff›
is declared as an iff-rule, then it's almost impossible to prove.
One proof is via ‹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 (drule constrains_Un [OF Diff_wens_constrains [of F act A]])
apply (erule constrains_weaken, blast)
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" for f 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 (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›

inductive_set
wens_set :: "['a program, 'a set] => 'a set set"
for F :: "'a program" and B :: "'a set"
where

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 ==> ⋃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 (drule_tac act1=act and A1=X
in constrains_Un [OF Diff_wens_constrains])
apply (erule constrains_weaken, blast)
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)
done

lemma leadsTo_imp_wens_set: "F ∈ A leadsTo B ==> ∃C ∈ wens_set F B. A ⊆ C"
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 = "⋃{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)"

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⊔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⊔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 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⊔G) act B ⊆ wens F act B"
apply (rule gfp_mono)
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⊔G) act Y ⊆ wens F act X ∧
T ∩ wens F act X = T ∩ wens (F⊔G) act Y"
apply (subgoal_tac "wens (F⊔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 (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⊔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⊔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⊔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 (clarify dest!: bchoice)
apply (rule_tac x = "⋃{Z. ∃U∈W. Z = f U}" in exI)
apply (blast intro: wens_set.Union)
done

and awpF: "T-B ⊆ awp F T"
and awpG: "!!X. X ∈ wens_set F B ==> (T∩X) - B ⊆ awp G (T∩X)"
shows "F⊔G ∈ T∩A leadsTo B"
apply (rule wens_Union [THEN bexE])
apply (rule awpF)
apply (erule awpG, assumption)
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)"

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: "(⋃i∈I. wp act (A i)) ⊆ wp act (⋃i∈I. A i)"

lemma wp_UN_eq:
"[|single_valued act; I≠{}|]
==> wp act (⋃i∈I. A i) = (⋃i∈I. wp act (A i))"
apply (rule equalityI)
prefer 2 apply (rule wp_UN_subset)
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›

definition wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set" where
"wens_single_finite act B k == ⋃i ∈ atMost k. (wp act ^^ i) B"

definition wens_single :: "[('a*'a) set, 'a set] => 'a set" where
"wens_single act B == ⋃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 add: wens_single_def wp_UN_eq, clarify)
apply (rule_tac a="Suc xa" 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"

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

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 = ⋃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 = (⋃k∈atMost n. wens_single_finite act B k)"
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"

lemma subset_wens_single_finite:
"[|W ⊆ wens_single_finite act B ` (atMost k); single_valued act; W≠{}|]
==> ∃m. ⋃W = wens_single_finite act B m"
apply (induct k)
apply (rule_tac x=0 in exI, simp, blast)
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)
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))⟧
⟹ ⋃W = wens_single act B"
apply (cases "wens_single act B ∈ W")
apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD])
apply (rule equalityI, blast)
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)
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›
txt‹Wens inductive step›
apply (case_tac "acta = Id", simp)
apply (elim disjE)
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)
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 (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)