86 apply (rule gfp_unfold) |
86 apply (rule gfp_unfold) |
87 apply (simp add: mono_def wp_def awp_def, blast) |
87 apply (simp add: mono_def wp_def awp_def, blast) |
88 done |
88 done |
89 |
89 |
90 lemma wens_Id [simp]: "wens F Id B = B" |
90 lemma wens_Id [simp]: "wens F Id B = B" |
91 by (simp add: wens_def gfp_def wp_def awp_def Join_set_eq, blast) |
91 by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast) |
92 |
92 |
93 text{*These two theorems justify the claim that @{term wens} returns the |
93 text{*These two theorems justify the claim that @{term wens} returns the |
94 weakest assertion satisfying the ensures property*} |
94 weakest assertion satisfying the ensures property*} |
95 lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B" |
95 lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B" |
96 apply (simp add: wens_def ensures_def transient_def, clarify) |
96 apply (simp add: wens_def ensures_def transient_def, clarify) |
99 apply (simp add: constrains_def awp_def wp_def, blast) |
99 apply (simp add: constrains_def awp_def wp_def, blast) |
100 done |
100 done |
101 |
101 |
102 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B" |
102 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B" |
103 by (simp add: wens_def gfp_def constrains_def awp_def wp_def |
103 by (simp add: wens_def gfp_def constrains_def awp_def wp_def |
104 ensures_def transient_def Join_set_eq, blast) |
104 ensures_def transient_def Sup_set_eq, blast) |
105 |
105 |
106 text{*These two results constitute assertion (4.13) of the thesis*} |
106 text{*These two results constitute assertion (4.13) of the thesis*} |
107 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B" |
107 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B" |
108 apply (simp add: wens_def wp_def awp_def) |
108 apply (simp add: wens_def wp_def awp_def) |
109 apply (rule gfp_mono, blast) |
109 apply (rule gfp_mono, blast) |
110 done |
110 done |
111 |
111 |
112 lemma wens_weakening: "B \<subseteq> wens F act B" |
112 lemma wens_weakening: "B \<subseteq> wens F act B" |
113 by (simp add: wens_def gfp_def Join_set_eq, blast) |
113 by (simp add: wens_def gfp_def Sup_set_eq, blast) |
114 |
114 |
115 text{*Assertion (6), or 4.16 in the thesis*} |
115 text{*Assertion (6), or 4.16 in the thesis*} |
116 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" |
116 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" |
117 apply (simp add: wens_def wp_def awp_def) |
117 apply (simp add: wens_def wp_def awp_def) |
118 apply (rule gfp_upperbound, blast) |
118 apply (rule gfp_upperbound, blast) |
119 done |
119 done |
120 |
120 |
121 text{*Assertion 4.17 in the thesis*} |
121 text{*Assertion 4.17 in the thesis*} |
122 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" |
122 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" |
123 by (simp add: wens_def gfp_def wp_def awp_def constrains_def Join_set_eq, blast) |
123 by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast) |
124 --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff} |
124 --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff} |
125 is declared as an iff-rule, then it's almost impossible to prove. |
125 is declared as an iff-rule, then it's almost impossible to prove. |
126 One proof is via @{text meson} after expanding all definitions, but it's |
126 One proof is via @{text meson} after expanding all definitions, but it's |
127 slow!*} |
127 slow!*} |
128 |
128 |
330 apply (simp add: wp_def Image_INT_eq) |
330 apply (simp add: wp_def Image_INT_eq) |
331 done |
331 done |
332 |
332 |
333 lemma wens_single_eq: |
333 lemma wens_single_eq: |
334 "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B" |
334 "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B" |
335 by (simp add: wens_def gfp_def wp_def Join_set_eq, blast) |
335 by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast) |
336 |
336 |
337 |
337 |
338 text{*Next, we express the @{term "wens_set"} for single-assignment programs*} |
338 text{*Next, we express the @{term "wens_set"} for single-assignment programs*} |
339 |
339 |
340 constdefs |
340 constdefs |