111 "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
111 "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
112 by (cut_tac z=p in Exh_Sprod2, auto) |
112 by (cut_tac z=p in Exh_Sprod2, auto) |
113 |
113 |
114 subsection {* Properties of @{term spair} *} |
114 subsection {* Properties of @{term spair} *} |
115 |
115 |
116 lemma spair_strict1 [simp]: "(:\<bottom>, b:) = \<bottom>" |
116 lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>" |
117 by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if) |
117 by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if) |
118 |
118 |
119 lemma spair_strict2 [simp]: "(:a, \<bottom>:) = \<bottom>" |
119 lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>" |
120 by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if) |
120 by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if) |
121 |
121 |
122 lemma spair_strict: "a = \<bottom> \<or> b = \<bottom> \<Longrightarrow> (:a, b:) = \<bottom>" |
122 lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>" |
123 by auto |
123 by auto |
124 |
124 |
125 lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>" |
125 lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>" |
126 by (erule contrapos_np, auto) |
126 by (erule contrapos_np, auto) |
127 |
127 |
128 lemma spair_defined [simp]: |
128 lemma spair_defined [simp]: |
129 "\<lbrakk>a \<noteq> \<bottom>; b \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:a, b:) \<noteq> \<bottom>" |
129 "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>" |
130 apply (simp add: spair_Abs_Sprod UU_Abs_Sprod) |
130 apply (simp add: spair_Abs_Sprod UU_Abs_Sprod) |
131 apply (subst Abs_Sprod_inject) |
131 apply (subst Abs_Sprod_inject) |
132 apply (simp add: Sprod_def) |
132 apply (simp add: Sprod_def) |
133 apply (simp add: Sprod_def inst_cprod_pcpo2) |
133 apply (simp add: Sprod_def inst_cprod_pcpo2) |
134 apply simp |
134 apply simp |
135 done |
135 done |
136 |
136 |
137 lemma spair_defined_rev: "(:a, b:) = \<bottom> \<Longrightarrow> a = \<bottom> \<or> b = \<bottom>" |
137 lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>" |
138 by (erule contrapos_pp, simp) |
138 by (erule contrapos_pp, simp) |
139 |
139 |
|
140 lemma spair_eq: |
|
141 "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)" |
|
142 apply (simp add: spair_Abs_Sprod) |
|
143 apply (simp add: Abs_Sprod_inject [OF _ spair_lemma] Sprod_def) |
|
144 apply (simp add: strictify_conv_if) |
|
145 done |
|
146 |
140 lemma spair_inject: |
147 lemma spair_inject: |
141 "\<lbrakk>aa \<noteq> \<bottom>; ba \<noteq> \<bottom>; (:a,b:) = (:aa,ba:)\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba" |
148 "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; (:x, y:) = (:a, b:)\<rbrakk> \<Longrightarrow> x = a \<and> y = b" |
142 apply (simp add: spair_Abs_Sprod) |
149 by (rule spair_eq [THEN iffD1]) |
143 apply (simp add: Abs_Sprod_inject [OF spair_lemma] Sprod_def) |
|
144 apply (simp add: strictify_conv_if split: split_if_asm) |
|
145 done |
|
146 |
150 |
147 lemma inst_sprod_pcpo2: "UU = (:UU,UU:)" |
151 lemma inst_sprod_pcpo2: "UU = (:UU,UU:)" |
148 by simp |
152 by simp |
149 |
153 |
150 subsection {* Properties of @{term sfst} and @{term ssnd} *} |
154 subsection {* Properties of @{term sfst} and @{term ssnd} *} |
167 lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y" |
171 lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y" |
168 by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair) |
172 by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair) |
169 |
173 |
170 lemma sfstssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>" |
174 lemma sfstssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>" |
171 by (rule_tac p=p in sprodE, simp_all) |
175 by (rule_tac p=p in sprodE, simp_all) |
172 |
176 |
173 lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p" |
177 lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p" |
174 by (rule_tac p=p in sprodE, simp_all) |
178 by (rule_tac p=p in sprodE, simp_all) |
175 |
179 |
|
180 lemma less_sprod: "p1 \<sqsubseteq> p2 = (sfst\<cdot>p1 \<sqsubseteq> sfst\<cdot>p2 \<and> ssnd\<cdot>p1 \<sqsubseteq> ssnd\<cdot>p2)" |
|
181 apply (simp add: less_sprod_def sfst_def ssnd_def cont_Rep_Sprod) |
|
182 apply (rule less_cprod) |
|
183 done |
|
184 |
|
185 lemma spair_less: |
|
186 "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)" |
|
187 apply (case_tac "a = \<bottom>") |
|
188 apply (simp add: eq_UU_iff [symmetric]) |
|
189 apply (case_tac "b = \<bottom>") |
|
190 apply (simp add: eq_UU_iff [symmetric]) |
|
191 apply (simp add: less_sprod) |
|
192 done |
|
193 |
|
194 |
176 subsection {* Properties of @{term ssplit} *} |
195 subsection {* Properties of @{term ssplit} *} |
177 |
196 |
178 lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>" |
197 lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>" |
179 by (simp add: ssplit_def) |
198 by (simp add: ssplit_def) |
180 |
199 |