equal
deleted
inserted
replaced
88 "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))" |
88 "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))" |
89 apply safe |
89 apply safe |
90 apply (rule_tac p=x in upE1) |
90 apply (rule_tac p=x in upE1) |
91 apply simp |
91 apply simp |
92 apply fast |
92 apply fast |
93 apply (force intro!: defined_up) |
93 apply (force intro!: up_defined) |
94 done |
94 done |
95 |
95 |
96 lemma ex_sprod_defined_iff: |
96 lemma ex_sprod_defined_iff: |
97 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) = |
97 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) = |
98 (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)" |
98 (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)" |