equal
deleted
inserted
replaced
91 text{*Result (4.39): Applying the leadsTo-Join Theorem*} |
91 text{*Result (4.39): Applying the leadsTo-Join Theorem*} |
92 theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)" |
92 theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)" |
93 apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k") |
93 apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k") |
94 apply simp |
94 apply simp |
95 apply (rule_tac T = "atLeast 0" in leadsTo_Join) |
95 apply (rule_tac T = "atLeast 0" in leadsTo_Join) |
96 apply (simp add: awp_iff FF_def, constrains) |
96 apply (simp add: awp_iff FF_def, safety) |
97 apply (simp add: awp_iff GG_def wens_set_FF, constrains) |
97 apply (simp add: awp_iff GG_def wens_set_FF, safety) |
98 apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) |
98 apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) |
99 done |
99 done |
100 |
100 |
101 end |
101 end |