diff -r ded12c9e88c2 -r 16094ed8ac6b src/HOLCF/Ssum.thy --- a/src/HOLCF/Ssum.thy Tue Jul 26 18:27:16 2005 +0200 +++ b/src/HOLCF/Ssum.thy Tue Jul 26 18:28:11 2005 +0200 @@ -24,9 +24,6 @@ syntax (HTML output) "++" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) -lemma UU_Abs_Ssum: "\ = Abs_Ssum <\, \>" -by (simp add: Abs_Ssum_strict cpair_strict) - subsection {* Definitions of constructors *} @@ -87,19 +84,20 @@ subsection {* Case analysis *} -lemma Exh_Ssum1: +lemma Exh_Ssum: "z = \ \ (\a. z = sinl\a \ a \ \) \ (\b. z = sinr\b \ b \ \)" apply (rule_tac x=z in Abs_Ssum_induct) apply (rule_tac p=y in cprodE) -apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum UU_Abs_Ssum) -apply (auto simp add: Ssum_def) +apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum) +apply (simp add: Abs_Ssum_inject Ssum_def) +apply (auto simp add: cpair_strict Abs_Ssum_strict) done lemma ssumE: "\p = \ \ Q; \x. \p = sinl\x; x \ \\ \ Q; \y. \p = sinr\y; y \ \\ \ Q\ \ Q" -by (cut_tac z=p in Exh_Ssum1, auto) +by (cut_tac z=p in Exh_Ssum, auto) lemma ssumE2: "\\x. p = sinl\x \ Q; \y. p = sinr\y \ Q\ \ Q"