equal
deleted
inserted
replaced
119 apply (assumption) |
119 apply (assumption) |
120 done |
120 done |
121 |
121 |
122 lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. |
122 lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. |
123 enat l <= #x --> (x::'a::flat stream) << y --> x:(F ^^ i) top --> y:(F ^^ i) top; |
123 enat l <= #x --> (x::'a::flat stream) << y --> x:(F ^^ i) top --> y:(F ^^ i) top; |
124 down_continuous F |] ==> adm (%x. x:gfp F)" |
124 inf_continuous F |] ==> adm (%x. x:gfp F)" |
125 apply (erule down_continuous_gfp[of F, THEN ssubst]) |
125 apply (erule inf_continuous_gfp[of F, THEN ssubst]) |
126 apply (simp (no_asm)) |
126 apply (simp (no_asm)) |
127 apply (rule adm_lemmas) |
127 apply (rule adm_lemmas) |
128 apply (rule flatstream_admI) |
128 apply (rule flatstream_admI) |
129 apply (erule allE) |
129 apply (erule allE) |
130 apply (erule exE) |
130 apply (erule exE) |
168 apply (drule (1) mp) |
168 apply (drule (1) mp) |
169 apply (assumption) |
169 apply (assumption) |
170 done |
170 done |
171 |
171 |
172 lemma stream_antiP2_non_gfp_admI: |
172 lemma stream_antiP2_non_gfp_admI: |
173 "!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; down_continuous F |] |
173 "!!X. [|!i x y. x << y --> y:(F ^^ i) top --> x:(F ^^ i) top; inf_continuous F |] |
174 ==> adm (%u. ~ u:gfp F)" |
174 ==> adm (%u. ~ u:gfp F)" |
175 apply (unfold adm_def) |
175 apply (unfold adm_def) |
176 apply (simp add: down_continuous_gfp) |
176 apply (simp add: inf_continuous_gfp) |
177 apply (fast dest!: is_ub_thelub) |
177 apply (fast dest!: is_ub_thelub) |
178 done |
178 done |
179 |
179 |
180 lemmas fstream_non_gfp_admI = stream_antiP2I [THEN stream_antiP2_non_gfp_admI] |
180 lemmas fstream_non_gfp_admI = stream_antiP2I [THEN stream_antiP2_non_gfp_admI] |
181 |
181 |