diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Ssum.thy --- a/src/HOLCF/Ssum.thy Thu Jan 03 23:59:51 2008 +0100 +++ b/src/HOLCF/Ssum.thy Fri Jan 04 00:01:02 2008 +0100 @@ -21,6 +21,12 @@ (cfst\p \ FF \ cfst\(csnd\p) = \)}" by simp +instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po +by (rule typedef_finite_po [OF type_definition_Ssum]) + +instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin +by (rule typedef_chfin [OF type_definition_Ssum less_Ssum_def]) + syntax (xsymbols) "++" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) syntax (HTML output) @@ -186,4 +192,18 @@ lemma sscase4 [simp]: "sscase\sinl\sinr\z = z" by (cases z, simp_all) +subsection {* Strict sum preserves flatness *} + +lemma flat_less_iff: + fixes x y :: "'a::flat" + shows "(x \ y) = (x = \ \ x = y)" +by (safe dest!: ax_flat [rule_format]) + +instance "++" :: (flat, flat) flat +apply (intro_classes, clarify) +apply (rule_tac p=x in ssumE, simp) +apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff) +apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff) +done + end