22 syntax (xsymbols) |
22 syntax (xsymbols) |
23 "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) |
23 "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) |
24 syntax (HTML output) |
24 syntax (HTML output) |
25 "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) |
25 "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) |
26 |
26 |
27 lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>" |
|
28 by (simp add: Abs_Ssum_strict cpair_strict) |
|
29 |
|
30 |
27 |
31 subsection {* Definitions of constructors *} |
28 subsection {* Definitions of constructors *} |
32 |
29 |
33 constdefs |
30 constdefs |
34 sinl :: "'a \<rightarrow> ('a ++ 'b)" |
31 sinl :: "'a \<rightarrow> ('a ++ 'b)" |
85 lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>" |
82 lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>" |
86 by simp |
83 by simp |
87 |
84 |
88 subsection {* Case analysis *} |
85 subsection {* Case analysis *} |
89 |
86 |
90 lemma Exh_Ssum1: |
87 lemma Exh_Ssum: |
91 "z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)" |
88 "z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)" |
92 apply (rule_tac x=z in Abs_Ssum_induct) |
89 apply (rule_tac x=z in Abs_Ssum_induct) |
93 apply (rule_tac p=y in cprodE) |
90 apply (rule_tac p=y in cprodE) |
94 apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum UU_Abs_Ssum) |
91 apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum) |
95 apply (auto simp add: Ssum_def) |
92 apply (simp add: Abs_Ssum_inject Ssum_def) |
|
93 apply (auto simp add: cpair_strict Abs_Ssum_strict) |
96 done |
94 done |
97 |
95 |
98 lemma ssumE: |
96 lemma ssumE: |
99 "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; |
97 "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; |
100 \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q; |
98 \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q; |
101 \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
99 \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
102 by (cut_tac z=p in Exh_Ssum1, auto) |
100 by (cut_tac z=p in Exh_Ssum, auto) |
103 |
101 |
104 lemma ssumE2: |
102 lemma ssumE2: |
105 "\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
103 "\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
106 apply (rule_tac p=p in ssumE) |
104 apply (rule_tac p=p in ssumE) |
107 apply (simp only: sinl_strict [symmetric]) |
105 apply (simp only: sinl_strict [symmetric]) |