equal
deleted
inserted
replaced
6 |
6 |
7 theory Sum_Cpo |
7 theory Sum_Cpo |
8 imports Bifinite |
8 imports Bifinite |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Ordering on type @{typ "'a + 'b"} *} |
11 subsection {* Ordering on sum type *} |
12 |
12 |
13 instantiation "+" :: (below, below) below |
13 instantiation "+" :: (below, below) below |
14 begin |
14 begin |
15 |
15 |
16 definition below_sum_def: |
16 definition below_sum_def: |
126 apply (rule exI) |
126 apply (rule exI) |
127 apply (rule is_lub_Inr) |
127 apply (rule is_lub_Inr) |
128 apply (erule cpo_lubI) |
128 apply (erule cpo_lubI) |
129 done |
129 done |
130 |
130 |
131 subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *} |
131 subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *} |
132 |
132 |
133 lemma cont_Inl: "cont Inl" |
133 lemma cont_Inl: "cont Inl" |
134 by (intro contI is_lub_Inl cpo_lubI) |
134 by (intro contI is_lub_Inl cpo_lubI) |
135 |
135 |
136 lemma cont_Inr: "cont Inr" |
136 lemma cont_Inr: "cont Inr" |