diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Ssum.thy --- a/src/HOLCF/Ssum.thy Tue Mar 02 17:20:03 2010 -0800 +++ b/src/HOLCF/Ssum.thy Tue Mar 02 17:21:10 2010 -0800 @@ -12,22 +12,22 @@ subsection {* Definition of strict sum type *} -pcpodef (Ssum) ('a, 'b) "++" (infixr "++" 10) = +pcpodef (Ssum) ('a, 'b) ssum (infixr "++" 10) = "{p :: tr \ ('a \ 'b). (fst p \ TT \ snd (snd p) = \) \ (fst p \ FF \ fst (snd p) = \)}" by simp_all -instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po +instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po by (rule typedef_finite_po [OF type_definition_Ssum]) -instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin +instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def]) syntax (xsymbols) - "++" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) + ssum :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) syntax (HTML output) - "++" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) + ssum :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) subsection {* Definitions of constructors *} @@ -150,13 +150,13 @@ apply (simp add: sinr_Abs_Ssum Ssum_def) done -lemma ssumE [cases type: ++]: +lemma ssumE [cases type: ssum]: "\p = \ \ Q; \x. \p = sinl\x; x \ \\ \ Q; \y. \p = sinr\y; y \ \\ \ Q\ \ Q" by (cut_tac z=p in Exh_Ssum, auto) -lemma ssum_induct [induct type: ++]: +lemma ssum_induct [induct type: ssum]: "\P \; \x. x \ \ \ P (sinl\x); \y. y \ \ \ P (sinr\y)\ \ P x" @@ -203,7 +203,7 @@ subsection {* Strict sum preserves flatness *} -instance "++" :: (flat, flat) flat +instance ssum :: (flat, flat) flat apply (intro_classes, clarify) apply (case_tac x, simp) apply (case_tac y, simp_all add: flat_below_iff) @@ -296,7 +296,7 @@ subsection {* Strict sum is a bifinite domain *} -instantiation "++" :: (bifinite, bifinite) bifinite +instantiation ssum :: (bifinite, bifinite) bifinite begin definition