49 typedef_cont_Rep [OF type_definition_Ssum less_ssum_def adm_Ssum] |
49 typedef_cont_Rep [OF type_definition_Ssum less_ssum_def adm_Ssum] |
50 |
50 |
51 lemmas cont_Abs_Ssum = |
51 lemmas cont_Abs_Ssum = |
52 typedef_cont_Abs [OF type_definition_Ssum less_ssum_def adm_Ssum] |
52 typedef_cont_Abs [OF type_definition_Ssum less_ssum_def adm_Ssum] |
53 |
53 |
54 lemmas strict_Rep_Ssum = |
54 lemmas Rep_Ssum_strict = |
55 typedef_strict_Rep [OF type_definition_Ssum less_ssum_def UU_Ssum] |
55 typedef_Rep_strict [OF type_definition_Ssum less_ssum_def UU_Ssum] |
56 |
56 |
57 lemmas strict_Abs_Ssum = |
57 lemmas Abs_Ssum_strict = |
58 typedef_strict_Abs [OF type_definition_Ssum less_ssum_def UU_Ssum] |
58 typedef_Abs_strict [OF type_definition_Ssum less_ssum_def UU_Ssum] |
59 |
59 |
60 lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>" |
60 lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>" |
61 by (simp add: strict_Abs_Ssum inst_cprod_pcpo2 [symmetric]) |
61 by (simp add: Abs_Ssum_strict inst_cprod_pcpo2 [symmetric]) |
62 |
62 |
63 |
63 |
64 subsection {* Definitions of constructors *} |
64 subsection {* Definitions of constructors *} |
65 |
65 |
66 constdefs |
66 constdefs |
82 by (unfold sinl_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def) |
82 by (unfold sinl_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def) |
83 |
83 |
84 lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = <\<bottom>, b>" |
84 lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = <\<bottom>, b>" |
85 by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def) |
85 by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def) |
86 |
86 |
87 lemma strict_sinl [simp]: "sinl\<cdot>\<bottom> = \<bottom>" |
87 lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>" |
88 by (simp add: sinl_Abs_Ssum UU_Abs_Ssum) |
88 by (simp add: sinl_Abs_Ssum UU_Abs_Ssum) |
89 |
89 |
90 lemma strict_sinr [simp]: "sinr\<cdot>\<bottom> = \<bottom>" |
90 lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>" |
91 by (simp add: sinr_Abs_Ssum UU_Abs_Ssum) |
91 by (simp add: sinr_Abs_Ssum UU_Abs_Ssum) |
92 |
92 |
93 lemma noteq_sinlsinr: "sinl\<cdot>a = sinr\<cdot>b \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>" |
93 lemma noteq_sinlsinr: "sinl\<cdot>a = sinr\<cdot>b \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>" |
94 apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum) |
94 apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum) |
95 apply (simp add: Abs_Ssum_inject Ssum_def) |
95 apply (simp add: Abs_Ssum_inject Ssum_def) |
96 done |
96 done |
97 |
97 |
98 lemma inject_sinl: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y" |
98 lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y" |
99 by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def) |
99 by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def) |
100 |
100 |
101 lemma inject_sinr: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y" |
101 lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y" |
102 by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def) |
102 by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def) |
103 |
103 |
104 lemma sinl_eq: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)" |
104 lemma sinl_eq: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)" |
105 by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def) |
105 by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def) |
106 |
106 |
107 lemma sinr_eq: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)" |
107 lemma sinr_eq: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)" |
108 by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def) |
108 by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def) |
109 |
109 |
110 lemma defined_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>" |
110 lemma sinl_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>" |
111 apply (erule contrapos_nn) |
111 apply (erule contrapos_nn) |
112 apply (rule inject_sinl) |
112 apply (rule sinl_inject) |
113 apply auto |
113 apply auto |
114 done |
114 done |
115 |
115 |
116 lemma defined_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>" |
116 lemma sinr_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>" |
117 apply (erule contrapos_nn) |
117 apply (erule contrapos_nn) |
118 apply (rule inject_sinr) |
118 apply (rule sinr_inject) |
119 apply auto |
119 apply auto |
120 done |
120 done |
121 |
121 |
122 subsection {* Case analysis *} |
122 subsection {* Case analysis *} |
123 |
123 |
136 by (cut_tac z=p in Exh_Ssum1, auto) |
136 by (cut_tac z=p in Exh_Ssum1, auto) |
137 |
137 |
138 lemma ssumE2: |
138 lemma ssumE2: |
139 "\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
139 "\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
140 apply (rule_tac p=p in ssumE) |
140 apply (rule_tac p=p in ssumE) |
141 apply (simp only: strict_sinl [symmetric]) |
141 apply (simp only: sinl_strict [symmetric]) |
142 apply simp |
142 apply simp |
143 apply simp |
143 apply simp |
144 done |
144 done |
145 |
145 |
146 subsection {* Ordering properties of @{term sinl} and @{term sinr} *} |
146 subsection {* Ordering properties of @{term sinl} and @{term sinr} *} |
204 if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>" |
204 if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>" |
205 |
205 |
206 text {* rewrites for @{term Iwhen} *} |
206 text {* rewrites for @{term Iwhen} *} |
207 |
207 |
208 lemma Iwhen1 [simp]: "Iwhen f g \<bottom> = \<bottom>" |
208 lemma Iwhen1 [simp]: "Iwhen f g \<bottom> = \<bottom>" |
209 by (simp add: Iwhen_def strict_Rep_Ssum) |
209 by (simp add: Iwhen_def Rep_Ssum_strict) |
210 |
210 |
211 lemma Iwhen2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinl\<cdot>x) = f\<cdot>x" |
211 lemma Iwhen2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinl\<cdot>x) = f\<cdot>x" |
212 by (simp add: Iwhen_def Rep_Ssum_sinl) |
212 by (simp add: Iwhen_def Rep_Ssum_sinl) |
213 |
213 |
214 lemma Iwhen3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinr\<cdot>y) = g\<cdot>y" |
214 lemma Iwhen3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinr\<cdot>y) = g\<cdot>y" |
215 by (simp add: Iwhen_def Rep_Ssum_sinr) |
215 by (simp add: Iwhen_def Rep_Ssum_sinr) |
216 |
216 |
217 lemma Iwhen4: "Iwhen f g (sinl\<cdot>x) = strictify\<cdot>f\<cdot>x" |
217 lemma Iwhen4: "Iwhen f g (sinl\<cdot>x) = strictify\<cdot>f\<cdot>x" |
218 by (case_tac "x = \<bottom>", simp_all) |
218 by (simp add: strictify_conv_if) |
219 |
219 |
220 lemma Iwhen5: "Iwhen f g (sinr\<cdot>y) = strictify\<cdot>g\<cdot>y" |
220 lemma Iwhen5: "Iwhen f g (sinr\<cdot>y) = strictify\<cdot>g\<cdot>y" |
221 by (case_tac "y = \<bottom>" , simp_all) |
221 by (simp add: strictify_conv_if) |
222 |
222 |
223 subsection {* Continuity of @{term Iwhen} *} |
223 subsection {* Continuity of @{term Iwhen} *} |
224 |
224 |
225 text {* @{term Iwhen} is continuous in all arguments *} |
225 text {* @{term Iwhen} is continuous in all arguments *} |
226 |
226 |
229 |
229 |
230 lemma cont_Iwhen2: "cont (\<lambda>g. Iwhen f g s)" |
230 lemma cont_Iwhen2: "cont (\<lambda>g. Iwhen f g s)" |
231 by (rule_tac p=s in ssumE, simp_all) |
231 by (rule_tac p=s in ssumE, simp_all) |
232 |
232 |
233 lemma cont_Iwhen3: "cont (\<lambda>s. Iwhen f g s)" |
233 lemma cont_Iwhen3: "cont (\<lambda>s. Iwhen f g s)" |
234 apply (rule contI [rule_format]) |
234 apply (rule contI) |
235 apply (drule ssum_chain_lemma, safe) |
235 apply (drule ssum_chain_lemma, safe) |
236 apply (simp add: contlub_cfun_arg [symmetric]) |
236 apply (simp add: contlub_cfun_arg [symmetric]) |
237 apply (simp add: Iwhen4) |
237 apply (simp add: Iwhen4) |
238 apply (simp add: contlub_cfun_arg) |
238 apply (simp add: contlub_cfun_arg) |
239 apply (simp add: thelubE chain_monofun) |
239 apply (simp add: thelubE chain_monofun) |