Moved sum_case stuff from Sum to Datatype.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype.ML	Thu Aug 19 19:00:42 1999 +0200
@@ -0,0 +1,34 @@
+(*  Title:      HOL/Datatype.ML
+    ID:         $Id$
+    Author:     Stefan Berghofer
+    Copyright   1999  TU Muenchen
+*)
+
+(** sum_case -- the selection operator for sums **)
+
+(*compatibility*)
+val [sum_case_Inl, sum_case_Inr] = sum.cases;
+
+Goal "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]);
+qed "surjective_sum";
+
+(*Prevents simplification of f and g: much faster*)
+Goal "s=t ==> sum_case f g s = sum_case f g t";
+by (etac arg_cong 1);
+qed "sum_case_weak_cong";
+
+val [p1,p2] = Goal
+  "[| sum_case f1 f2 = sum_case g1 g2;  \
+\     [| f1 = g1; f2 = g2 |] ==> P |] \
+\  ==> P";
+by (rtac p2 1);
+by (rtac ext 1);
+by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
+by (Asm_full_simp_tac 1);
+by (rtac ext 1);
+by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
+by (Asm_full_simp_tac 1);
+qed "sum_case_inject";

--- a/src/HOL/Sum.ML	Thu Aug 19 18:36:41 1999 +0200
+++ b/src/HOL/Sum.ML	Thu Aug 19 19:00:42 1999 +0200
@@ -114,18 +114,6 @@
 AddSEs [PlusE];
 
 
-(** sum_case -- the selection operator for sums **)
-
-Goalw [sum_case_def] "basic_sum_case f g (Inl x) = f(x)";
-by (Blast_tac 1);
-qed "sum_case_Inl";
-
-Goalw [sum_case_def] "basic_sum_case f g (Inr x) = g(x)";
-by (Blast_tac 1);
-qed "sum_case_Inr";
-
-Addsimps [sum_case_Inl, sum_case_Inr];
-
 (** Exhaustion rule for sums -- a degenerate form of induction **)
 
 val prems = Goalw [Inl_def,Inr_def]
@@ -143,42 +131,6 @@
 by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
 qed "sum_induct";
 
-Goal "basic_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]);
-qed "surjective_sum";
-
-Goal "R(basic_sum_case f g s) = \
-\             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
-by (res_inst_tac [("s","s")] sumE 1);
-by Auto_tac;
-qed "split_sum_case";
-
-Goal "P (basic_sum_case f g s) = \
-\     (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))";
-by (stac split_sum_case 1);
-by (Blast_tac 1);
-qed "split_sum_case_asm";
-
-(*Prevents simplification of f and g: much faster*)
-Goal "s=t ==> basic_sum_case f g s = basic_sum_case f g t";
-by (etac arg_cong 1);
-qed "sum_case_weak_cong";
-
-val [p1,p2] = Goal
-  "[| basic_sum_case f1 f2 = basic_sum_case g1 g2;  \
-\     [| f1 = g1; f2 = g2 |] ==> P |] \
-\  ==> P";
-by (rtac p2 1);
-by (rtac ext 1);
-by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
-by (Asm_full_simp_tac 1);
-by (rtac ext 1);
-by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
-by (Asm_full_simp_tac 1);
-qed "sum_case_inject";
-
 
 (** Rules for the Part primitive **)
 
@@ -222,7 +174,6 @@
 by (Blast_tac 1);
 qed "Part_Int";
 
-(*For inductive definitions*)
 Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
 by (Blast_tac 1);
 qed "Part_Collect";

--- a/src/HOL/Sum.thy	Thu Aug 19 18:36:41 1999 +0200
+++ b/src/HOL/Sum.thy	Thu Aug 19 19:00:42 1999 +0200
@@ -29,7 +29,6 @@
 consts
   Inl            :: "'a => 'a + 'b"
   Inr            :: "'b => 'a + 'b"
-  basic_sum_case :: "['a => 'c, 'b => 'c, 'a + 'b] => 'c"
 
   (*disjoint sum for sets; the operator + is overloaded with wrong type!*)
   Plus          :: "['a set, 'b set] => ('a + 'b) set"        (infixr 65)
@@ -40,8 +39,6 @@
 defs
   Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
   Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
-  sum_case_def  "basic_sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      
-                                      & (!y. p=Inr(y) --> z=g(y))"
 
   sum_def       "A Plus B == (Inl``A) Un (Inr``B)"
 

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Aug 19 18:36:41 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Aug 19 19:00:42 1999 +0200
@@ -47,16 +47,16 @@
     val Datatype_thy = theory "Datatype";
     val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
     val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name,
-      Funs_name, o_name] =
+      Funs_name, o_name, sum_case_name] =
       map (Sign.intern_const (Theory.sign_of Datatype_thy))
-        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o"];
+        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o", "sum_case"];
 
     val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
          In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
-         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty] = map (get_thm Datatype_thy)
+         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy)
         ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
          "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
-         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty"];
+         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty", "sum_case_inject"];
 
     val Funs_IntE = (Int_lower2 RS Funs_mono RS
       (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
@@ -124,7 +124,7 @@
           let
             val n2 = n div 2;
             val Type (_, [T1, T2]) = T;
-            val sum_case = Const ("basic_sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
+            val sum_case = Const (sum_case_name, [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
           in
             if i <= n2 then
               sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)

--- a/src/HOL/Tools/inductive_package.ML	Thu Aug 19 18:36:41 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 19 19:00:42 1999 +0200
@@ -455,6 +455,10 @@
 
     val sign = Theory.sign_of thy;
 
+    val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
+        None => []
+      | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
+
     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
 
     (* make predicate for instantiation of abstract induction rule *)
@@ -463,7 +467,7 @@
       | mk_ind_pred T Ps =
          let val n = (length Ps) div 2;
              val Type (_, [T1, T2]) = T
-         in Const ("basic_sum_case",
+         in Const ("Datatype.sum.sum_case",
            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
          end;
@@ -482,8 +486,7 @@
           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
              nth_elem (find_index_eq c cs, preds)))))
-        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
-           (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
+        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
           rtac refl 1])) cs;
 
     val induct = prove_goalw_cterm [] (cterm_of sign
@@ -498,7 +501,7 @@
            some premise involves disjunction.*)
          REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 
                      ORELSE' hyp_subst_tac)),
-         rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
+         rewrite_goals_tac sum_case_rewrites,
          EVERY (map (fn prem =>
            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
 
@@ -508,7 +511,7 @@
          REPEAT (EVERY
            [REPEAT (resolve_tac [conjI, impI] 1),
             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
-            rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
+            rewrite_goals_tac sum_case_rewrites,
             atac 1])])
 
   in standard (split_rule (induct RS lemma))