92 lemma Always_Follows1: |
92 lemma Always_Follows1: |
93 "[| F \<in> Always {s. f s = f' s}; F \<in> f Fols g |] ==> F \<in> f' Fols g" |
93 "[| F \<in> Always {s. f s = f' s}; F \<in> f Fols g |] ==> F \<in> f' Fols g" |
94 |
94 |
95 apply (simp add: Follows_def Increasing_def Stable_def, auto) |
95 apply (simp add: Follows_def Increasing_def Stable_def, auto) |
96 apply (erule_tac [3] Always_LeadsTo_weaken) |
96 apply (erule_tac [3] Always_LeadsTo_weaken) |
97 apply (erule_tac A = "{s. z \<le> f s}" and A' = "{s. z \<le> f s}" |
97 apply (erule_tac A = "{s. x \<le> f s}" and A' = "{s. x \<le> f s}" |
98 in Always_Constrains_weaken, auto) |
98 in Always_Constrains_weaken, auto) |
99 apply (drule Always_Int_I, assumption) |
99 apply (drule Always_Int_I, assumption) |
100 apply (force intro: Always_weaken) |
100 apply (force intro: Always_weaken) |
101 done |
101 done |
102 |
102 |
103 lemma Always_Follows2: |
103 lemma Always_Follows2: |
104 "[| F \<in> Always {s. g s = g' s}; F \<in> f Fols g |] ==> F \<in> f Fols g'" |
104 "[| F \<in> Always {s. g s = g' s}; F \<in> f Fols g |] ==> F \<in> f Fols g'" |
105 apply (simp add: Follows_def Increasing_def Stable_def, auto) |
105 apply (simp add: Follows_def Increasing_def Stable_def, auto) |
106 apply (erule_tac [3] Always_LeadsTo_weaken) |
106 apply (erule_tac [3] Always_LeadsTo_weaken) |
107 apply (erule_tac A = "{s. z \<le> g s}" and A' = "{s. z \<le> g s}" |
107 apply (erule_tac A = "{s. x \<le> g s}" and A' = "{s. x \<le> g s}" |
108 in Always_Constrains_weaken, auto) |
108 in Always_Constrains_weaken, auto) |
109 apply (drule Always_Int_I, assumption) |
109 apply (drule Always_Int_I, assumption) |
110 apply (force intro: Always_weaken) |
110 apply (force intro: Always_weaken) |
111 done |
111 done |
112 |
112 |
113 |
113 |
114 subsection{*Union properties (with the subset ordering)*} |
114 subsection{*Union properties (with the subset ordering)*} |
115 |
115 |
116 (*Can replace "Un" by any sup. But existing max only works for linorders.*) |
116 (*Can replace "Un" by any sup. But existing max only works for linorders.*) |
|
117 |
117 lemma increasing_Un: |
118 lemma increasing_Un: |
118 "[| F \<in> increasing f; F \<in> increasing g |] |
119 "[| F \<in> increasing f; F \<in> increasing g |] |
119 ==> F \<in> increasing (%s. (f s) \<union> (g s))" |
120 ==> F \<in> increasing (%s. (f s) \<union> (g s))" |
120 apply (simp add: increasing_def stable_def constrains_def, auto) |
121 apply (simp add: increasing_def stable_def constrains_def, auto) |
121 apply (drule_tac x = "f xa" in spec) |
122 apply (drule_tac x = "f xb" in spec) |
122 apply (drule_tac x = "g xa" in spec) |
123 apply (drule_tac x = "g xb" in spec) |
123 apply (blast dest!: bspec) |
124 apply (blast dest!: bspec) |
124 done |
125 done |
125 |
126 |
126 lemma Increasing_Un: |
127 lemma Increasing_Un: |
127 "[| F \<in> Increasing f; F \<in> Increasing g |] |
128 "[| F \<in> Increasing f; F \<in> Increasing g |] |
128 ==> F \<in> Increasing (%s. (f s) \<union> (g s))" |
129 ==> F \<in> Increasing (%s. (f s) \<union> (g s))" |
129 apply (auto simp add: Increasing_def Stable_def Constrains_def |
130 apply (auto simp add: Increasing_def Stable_def Constrains_def |
130 stable_def constrains_def) |
131 stable_def constrains_def) |
131 apply (drule_tac x = "f xa" in spec) |
132 apply (drule_tac x = "f xb" in spec) |
132 apply (drule_tac x = "g xa" in spec) |
133 apply (drule_tac x = "g xb" in spec) |
133 apply (blast dest!: bspec) |
134 apply (blast dest!: bspec) |
134 done |
135 done |
135 |
136 |
136 |
137 |
137 lemma Always_Un: |
138 lemma Always_Un: |
170 |
171 |
171 lemma increasing_union: |
172 lemma increasing_union: |
172 "[| F \<in> increasing f; F \<in> increasing g |] |
173 "[| F \<in> increasing f; F \<in> increasing g |] |
173 ==> F \<in> increasing (%s. (f s) + (g s :: ('a::order) multiset))" |
174 ==> F \<in> increasing (%s. (f s) + (g s :: ('a::order) multiset))" |
174 apply (simp add: increasing_def stable_def constrains_def, auto) |
175 apply (simp add: increasing_def stable_def constrains_def, auto) |
175 apply (drule_tac x = "f xa" in spec) |
176 apply (drule_tac x = "f xb" in spec) |
176 apply (drule_tac x = "g xa" in spec) |
177 apply (drule_tac x = "g xb" in spec) |
177 apply (drule bspec, assumption) |
178 apply (drule bspec, assumption) |
178 apply (blast intro: add_mono order_trans) |
179 apply (blast intro: add_mono order_trans) |
179 done |
180 done |
180 |
181 |
181 lemma Increasing_union: |
182 lemma Increasing_union: |
182 "[| F \<in> Increasing f; F \<in> Increasing g |] |
183 "[| F \<in> Increasing f; F \<in> Increasing g |] |
183 ==> F \<in> Increasing (%s. (f s) + (g s :: ('a::order) multiset))" |
184 ==> F \<in> Increasing (%s. (f s) + (g s :: ('a::order) multiset))" |
184 apply (auto simp add: Increasing_def Stable_def Constrains_def |
185 apply (auto simp add: Increasing_def Stable_def Constrains_def |
185 stable_def constrains_def) |
186 stable_def constrains_def) |
186 apply (drule_tac x = "f xa" in spec) |
187 apply (drule_tac x = "f xb" in spec) |
187 apply (drule_tac x = "g xa" in spec) |
188 apply (drule_tac x = "g xb" in spec) |
188 apply (drule bspec, assumption) |
189 apply (drule bspec, assumption) |
189 apply (blast intro: add_mono order_trans) |
190 apply (blast intro: add_mono order_trans) |
190 done |
191 done |
191 |
192 |
192 lemma Always_union: |
193 lemma Always_union: |