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, safety) |
96 oops |
97 apply (simp add: awp_iff GG_def wens_set_FF, safety) |
97 (* FIXME rotten proof |
|
98 apply (simp add: awp_iff_constrains FF_def, safety) |
|
99 apply (simp add: awp_iff_constrains GG_def wens_set_FF, safety) |
98 apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) |
100 apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) |
99 done |
101 done |
|
102 *) |
100 |
103 |
101 end |
104 end |