equal
deleted
inserted
replaced
86 lemma FF_leadsTo: "FF \<in> UNIV leadsTo atLeast (k::int)" |
86 lemma FF_leadsTo: "FF \<in> UNIV leadsTo atLeast (k::int)" |
87 apply (subst UN_atLeast_UNIV [symmetric]) |
87 apply (subst UN_atLeast_UNIV [symmetric]) |
88 apply (rule leadsTo_UN [OF atLeast_leadsTo]) |
88 apply (rule leadsTo_UN [OF atLeast_leadsTo]) |
89 done |
89 done |
90 |
90 |
91 text{*Result (4.39): Applying the Union 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_Union) |
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, constrains) |
97 apply (simp add: awp_iff GG_def wens_set_FF, constrains) |
97 apply (simp add: awp_iff GG_def wens_set_FF, constrains) |
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 |