1 (* Title: ZF/UNITY/Follows |
1 (* Title: ZF/UNITY/Follows.thy |
2 ID: $Id \<in> Follows.thy,v 1.1 2003/05/28 16:13:42 paulson Exp $ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
4 Copyright 2002 University of Cambridge |
3 Copyright 2002 University of Cambridge |
5 |
4 |
6 Theory ported from HOL. |
5 Theory ported from HOL. |
7 *) |
6 *) |
277 "[| F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h); |
276 "[| F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h); |
278 \<forall>x \<in> state. g(x):A |] ==> F \<in> Follows(A, r, g, h)" |
277 \<forall>x \<in> state. g(x):A |] ==> F \<in> Follows(A, r, g, h)" |
279 apply (unfold Follows_def Increasing_def Stable_def) |
278 apply (unfold Follows_def Increasing_def Stable_def) |
280 apply (simp add: INT_iff, auto) |
279 apply (simp add: INT_iff, auto) |
281 apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}" |
280 apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}" |
282 and A = "{s \<in> state. <k, h (s)> \<in> r}" |
281 and A = "{s \<in> state. <k, h (s)> \<in> r}" |
283 and A' = "{s \<in> state. <k, f(s)> \<in> r}" in Always_LeadsTo_weaken) |
282 and A' = "{s \<in> state. <k, f(s)> \<in> r}" in Always_LeadsTo_weaken) |
284 apply (erule_tac A = "{s \<in> state. <k,f(s) > \<in> r}" |
283 apply (erule_tac A = "{s \<in> state. <k,f(s) > \<in> r}" |
285 and A' = "{s \<in> state. <k,f(s) > \<in> r}" in Always_Constrains_weaken) |
284 and A' = "{s \<in> state. <k,f(s) > \<in> r}" in Always_Constrains_weaken) |
286 apply auto |
285 apply auto |
287 apply (drule Always_Int_I, assumption) |
286 apply (drule Always_Int_I, assumption) |
288 apply (erule_tac A = "{s \<in> state. f(s)=g(s)} \<inter> {s \<in> state. <f(s), h(s)> \<in> r}" |
287 apply (erule_tac A = "{s \<in> state. f(s)=g(s)} \<inter> {s \<in> state. <f(s), h(s)> \<in> r}" |