equal
deleted
inserted
replaced
1 (* Title: HOL/UNITY/Follows |
1 (* Title: HOL/UNITY/Follows.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1998 University of Cambridge |
3 Copyright 1998 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 header{*The Follows Relation of Charpentier and Sivilotte*} |
6 header{*The Follows Relation of Charpentier and Sivilotte*} |
37 lemma Follows_constant [iff]: "F \<in> (%s. c) Fols (%s. c)" |
37 lemma Follows_constant [iff]: "F \<in> (%s. c) Fols (%s. c)" |
38 by (simp add: Follows_def) |
38 by (simp add: Follows_def) |
39 |
39 |
40 lemma mono_Follows_o: "mono h ==> f Fols g \<subseteq> (h o f) Fols (h o g)" |
40 lemma mono_Follows_o: "mono h ==> f Fols g \<subseteq> (h o f) Fols (h o g)" |
41 by (auto simp add: Follows_def mono_Increasing_o [THEN [2] rev_subsetD] |
41 by (auto simp add: Follows_def mono_Increasing_o [THEN [2] rev_subsetD] |
42 mono_Always_o [THEN [2] rev_subsetD] |
42 mono_Always_o [THEN [2] rev_subsetD] |
43 mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D]) |
43 mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D]) |
44 |
44 |
45 lemma mono_Follows_apply: |
45 lemma mono_Follows_apply: |
46 "mono h ==> f Fols g \<subseteq> (%x. h (f x)) Fols (%x. h (g x))" |
46 "mono h ==> f Fols g \<subseteq> (%x. h (f x)) Fols (%x. h (g x))" |
47 apply (drule mono_Follows_o) |
47 apply (drule mono_Follows_o) |
48 apply (force simp add: o_def) |
48 apply (force simp add: o_def) |