equal
deleted
inserted
replaced
138 "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. \<not> Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> (P x \<and> Q x))" |
138 "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. \<not> Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> (P x \<and> Q x))" |
139 by (simp add: adm_imp) |
139 by (simp add: adm_imp) |
140 |
140 |
141 text {* admissibility and continuity *} |
141 text {* admissibility and continuity *} |
142 |
142 |
|
143 declare range_composition [simp del] |
|
144 |
143 lemma adm_less: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)" |
145 lemma adm_less: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)" |
144 apply (rule admI) |
146 apply (rule admI) |
145 apply (simp add: cont2contlubE) |
147 apply (simp add: cont2contlubE) |
146 apply (rule lub_mono) |
148 apply (rule lub_mono) |
147 apply (erule (1) ch2ch_cont) |
149 apply (erule (1) ch2ch_cont) |
163 lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)" |
165 lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)" |
164 apply (rule admI) |
166 apply (rule admI) |
165 apply (drule_tac x=0 in spec) |
167 apply (drule_tac x=0 in spec) |
166 apply (erule contrapos_nn) |
168 apply (erule contrapos_nn) |
167 apply (erule rev_trans_less) |
169 apply (erule rev_trans_less) |
168 apply (erule cont2mono [THEN monofun_fun_arg]) |
170 apply (erule cont2mono [THEN monofunE]) |
169 apply (erule is_ub_thelub) |
171 apply (erule is_ub_thelub) |
170 done |
172 done |
171 |
173 |
172 text {* admissibility and compactness *} |
174 text {* admissibility and compactness *} |
173 |
175 |