equal
deleted
inserted
replaced
85 done |
85 done |
86 |
86 |
87 lemma ex_up_defined_iff: |
87 lemma ex_up_defined_iff: |
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 upE) |
91 apply simp |
91 apply simp |
92 apply fast |
92 apply fast |
93 apply (force intro!: up_defined) |
93 apply (force intro!: up_defined) |
94 done |
94 done |
95 |
95 |
107 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) = |
107 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) = |
108 (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)" |
108 (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)" |
109 apply safe |
109 apply safe |
110 apply (rule_tac p=y in sprodE) |
110 apply (rule_tac p=y in sprodE) |
111 apply simp |
111 apply simp |
112 apply (rule_tac p=x in upE1) |
112 apply (rule_tac p=x in upE) |
113 apply simp |
113 apply simp |
114 apply fast |
114 apply fast |
115 apply (force intro!: spair_defined) |
115 apply (force intro!: spair_defined) |
116 done |
116 done |
117 |
117 |