# HG changeset patch
# User lcp
# Date 789876250 -3600
# Node ID b87867b3fd91287ae1af8f85e61066b3056147d1
# Parent  f5314a7c93f299dbe636859517d069a3cb4c40dd
Proved case_cong and case_case.

diff -r f5314a7c93f2 -r b87867b3fd91 src/ZF/Sum.ML
--- a/src/ZF/Sum.ML	Thu Jan 12 03:03:45 1995 +0100
+++ b/src/ZF/Sum.ML	Thu Jan 12 03:04:10 1995 +0100
@@ -151,6 +151,23 @@
 by (fast_tac sum_cs 1);
 qed "expand_case";
 
+val major::prems = goal Sum.thy
+  "[| z: A+B; 	\
+\     !!x. x:A ==> c(x)=c'(x); 	\
+\     !!y. y:B ==> d(y)=d'(y) 	\
+\  |] ==> case(c,d,z) = case(c',d',z)";
+by (resolve_tac [major RS sumE] 1);
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([case_Inl, case_Inr] @ prems))));
+qed "case_cong";
+
+val [major] = goal Sum.thy
+  "z: A+B ==> 	\
+\  case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \
+\  case(%x. c(c'(x)), %y. d(d'(y)), z)";
+by (resolve_tac [major RS sumE] 1);
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [case_Inl, case_Inr])));
+qed "case_case";
+
 val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff, 
 			     Inl_Inr_iff, Inr_Inl_iff,
 			     case_Inl, case_Inr];