HOL/Sum: rotated arguments of sum_case; added translation for case macro
HOL/Sum: now has Part primitives, moved from ex/Simult, with extra
laws from ZF/Sum

--- a/Sum.ML	Thu Aug 18 11:40:54 1994 +0200
+++ b/Sum.ML	Thu Aug 18 11:43:40 1994 +0200
@@ -1,9 +1,9 @@
-(*  Title: 	HOL/sum
+(*  Title: 	HOL/Sum.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-For sum.ML.  The disjoint sum of two types
+For Sum.thy.  The disjoint sum of two types
 *)
 
 open Sum;
@@ -43,6 +43,15 @@
 val Inl_neq_Inr = standard (Inl_not_Inr RS notE);
 val Inr_neq_Inl = sym RS Inl_neq_Inr;
 
+goal Sum.thy "(Inl(a)=Inr(b)) = False";
+by (simp_tac (HOL_ss addsimps [Inl_not_Inr]) 1);
+val Inl_Inr_eq = result();
+
+goal Sum.thy "(Inr(b)=Inl(a))  =  False";
+by (simp_tac (HOL_ss addsimps [Inl_not_Inr RS not_sym]) 1);
+val Inr_Inl_eq = result();
+
+
 (** Injectiveness of Inl and Inr **)
 
 val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
@@ -72,29 +81,25 @@
 val Inr_inject = inj_Inr RS injD;
 
 goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
-br iffI 1;
-be (rewrite_rule [inj_def] Inl_inject) 1;
-be ssubst 1;
-br refl 1;
-val Inl_inj = result();
+by (fast_tac (HOL_cs addSEs [Inl_inject]) 1);
+val Inl_eq = result();
 
 goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
-br iffI 1;
-be (rewrite_rule [inj_def] Inr_inject) 1;
-be ssubst 1;
-br refl 1;
-val Inr_inj = result();
+by (fast_tac (HOL_cs addSEs [Inr_inject]) 1);
+val Inr_eq = result();
+
+val sum_cs = set_cs addSEs [Inl_neq_Inr, Inr_neq_Inl]
+                    addSDs [Inl_inject, Inr_inject];
+
 
 (** sum_case -- the selection operator for sums **)
 
-goalw Sum.thy [sum_case_def] "sum_case(Inl(x), f, g) = f(x)";
-by (fast_tac (set_cs addIs [select_equality] 
-		     addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
+goalw Sum.thy [sum_case_def] "sum_case(f, g, Inl(x)) = f(x)";
+by (fast_tac (sum_cs addIs [select_equality]) 1);
 val sum_case_Inl = result();
 
-goalw Sum.thy [sum_case_def] "sum_case(Inr(x), f, g) = g(x)";
-by (fast_tac (set_cs addIs [select_equality] 
-		     addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
+goalw Sum.thy [sum_case_def] "sum_case(f, g, Inr(x)) = g(x)";
+by (fast_tac (sum_cs addIs [select_equality]) 1);
 val sum_case_Inr = result();
 
 (** Exhaustion rule for sums -- a degenerate form of induction **)
@@ -109,13 +114,13 @@
 		    rtac (Rep_Sum_inverse RS sym)]));
 val sumE = result();
 
-goal Sum.thy "sum_case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)";
+goal Sum.thy "sum_case(%x::'a. f(Inl(x)), %y::'b. f(Inr(y)), s) = f(s)";
 by (EVERY1 [res_inst_tac [("s","s")] sumE, 
 	    etac ssubst, rtac sum_case_Inl,
 	    etac ssubst, rtac sum_case_Inr]);
 val surjective_sum = result();
 
-goal Sum.thy "R(sum_case(s,f,g)) = \
+goal Sum.thy "R(sum_case(f,g,s)) = \
 \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
 by (rtac sumE 1);
 by (etac ssubst 1);
@@ -126,9 +131,46 @@
 by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
 val expand_sum_case = result();
 
-val sum_ss = pair_ss addsimps [sum_case_Inl, sum_case_Inr];
+val sum_ss = prod_ss addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, 
+			       sum_case_Inl, sum_case_Inr];
 
 (*Prevents simplification of f and g: much faster*)
 val sum_case_weak_cong = prove_goal Sum.thy
-  "s=t ==> sum_case(s,f,g) = sum_case(t,f,g)"
+  "s=t ==> sum_case(f,g,s) = sum_case(f,g,t)"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
+
+(** Rules for the Part primitive **)
+
+goalw Sum.thy [Part_def]
+    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
+by (fast_tac set_cs 1);
+val Part_eqI = result();
+
+val PartI = refl RSN (2,Part_eqI);
+
+val major::prems = goalw Sum.thy [Part_def]
+    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
+\    |] ==> P";
+by (rtac (major RS IntE) 1);
+by (etac CollectE 1);
+by (etac exE 1);
+by (REPEAT (ares_tac prems 1));
+val PartE = result();
+
+goalw Sum.thy [Part_def] "Part(A,h) <= A";
+by (rtac Int_lower1 1);
+val Part_subset = result();
+
+goal Sum.thy "!!A B. A<=B ==> Part(A,h) <= Part(B,h)";
+by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
+val Part_mono = result();
+
+goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
+by (etac IntD1 1);
+val PartD1 = result();
+
+goal Sum.thy "Part(A,%x.x) = A";
+by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+val Part_id = result();
+

--- a/Sum.thy	Thu Aug 18 11:40:54 1994 +0200
+++ b/Sum.thy	Thu Aug 18 11:43:40 1994 +0200
@@ -22,19 +22,29 @@
   Abs_Sum  :: "(['a,'b,bool] => bool) => 'a+'b"
   Inl	   :: "'a => 'a+'b"
   Inr	   :: "'b => 'a+'b"
-  sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c"
+  sum_case :: "['a=>'c,'b=>'c, 'a+'b] =>'c"
+  Part     :: "['a set, 'a=>'a] => 'a set"
+
+translations
+  "case p of Inl(x) => a | Inr(y) => b" == "sum_case(%x.a, %y.b, p)"
 
 rules
   Inl_Rep_def	"Inl_Rep == (%a. %x y p. x=a & p)"
   Inr_Rep_def	"Inr_Rep == (%b. %x y p. y=b & ~p)"
+
   Sum_def "Sum == {f. (? a. f = Inl_Rep(a)) | (? b. f = Inr_Rep(b))}"
     (*faking a type definition...*)
   Rep_Sum 		"Rep_Sum(s): Sum"
   Rep_Sum_inverse 	"Abs_Sum(Rep_Sum(s)) = s"
   Abs_Sum_inverse 	"f: Sum ==> Rep_Sum(Abs_Sum(f)) = f"
+
     (*defining the abstract constants*)
   Inl_def  		"Inl == (%a. Abs_Sum(Inl_Rep(a)))"
   Inr_def 		"Inr == (%b. Abs_Sum(Inr_Rep(b)))"
-  sum_case_def	"sum_case == (%p f g. @z.  (!x. p=Inl(x) --> z=f(x))\
-\                                        & (!y. p=Inr(y) --> z=g(y)))"
+  sum_case_def	"sum_case(f,g,p) == @z.  (!x. p=Inl(x) --> z=f(x))	\
+\                                      & (!y. p=Inr(y) --> z=g(y))"
+
+  (*for selecting out the components of a mutually recursive definition*)
+  Part_def	"Part(A,h) == A Int {x. ? z. x = h(z)}"
+
 end