# HG changeset patch
# User nipkow
# Date 878887502 -3600
# Node ID 23a09f2fd687f414e51d0c7464922be7692d231b
# Parent  706902a9abddf0e5553fe48316027fc4ec4b7f99
Each datatype t now proves a theorem split_t_case_prem

  P(t_case f1 ... fn x) =
     (~((? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
        ...
        (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
     ) )

diff -r 706902a9abdd -r 23a09f2fd687 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Thu Nov 06 16:44:35 1997 +0100
+++ b/src/HOL/datatype.ML	Fri Nov 07 08:25:02 1997 +0100
@@ -435,16 +435,19 @@
       local
       val fs = map (fn i => "f"^(string_of_int i)) (1 upto num_of_cons);
 
-      fun split1case ((_,name,_,vns,_),fi) =
+      fun split1case concl ((_,name,_,vns,_),fi) =
         let val svns = " " ^ (space_implode " " vns);
-            val all = if null vns then "" else "!" ^ svns ^ ". "
-        in "("^all^tname^"0 = "^C_exp name vns^" --> P("^fi^svns^"))" end;
+            val quant = if concl then "!" else "?";
+            val impl = if concl then " --> " else " & ~";
+            val all = if null vns then "" else quant ^ svns ^ ". "
+        in "("^all^tname^"0 = "^C_exp name vns^impl^"P("^fi^svns^"))" end;
 
-      val rhss  = map split1case (cons_list ~~ fs);
-      val rhs = space_implode " & " rhss;
+      fun rhss concl = map (split1case concl) (cons_list ~~ fs);
+      fun rhs concl= space_implode(if concl then " & " else " | ")(rhss concl);
       val lhs = "P(" ^ t_case ^ " " ^ (space_implode " " fs) ^" "^ tname^"0)"
       in
-      val split_eqn = lhs ^ " = (" ^ rhs ^ ")"
+      val split_eqn = lhs ^ " = (" ^ rhs true ^ ")"
+      val split_eqn_prem = lhs ^ " = ( ~ (" ^ rhs false ^ "))"
       end;
 
 (* -------------------------------------------------------------------- *)
@@ -518,7 +521,8 @@
            |> Theory.add_arities arities
            |> Theory.add_consts consts
            |> Theory.add_trrules xrules
-           |> PureThy.add_store_axioms rules, add_primrec, size_eqns, split_eqn)
+           |> PureThy.add_store_axioms rules,
+       add_primrec, size_eqns, (split_eqn,split_eqn_prem))
     end
 
 (*Warn if the (induction) variable occurs Free among the premises, which
diff -r 706902a9abdd -r 23a09f2fd687 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Thu Nov 06 16:44:35 1997 +0100
+++ b/src/HOL/thy_syntax.ML	Fri Nov 07 08:25:02 1997 +0100
@@ -123,7 +123,7 @@
 
   (*generate string for calling add_datatype and build_record*)
   fun mk_params ((ts, tname), cons) =
-    "val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqn) =\n\
+    "val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqns) =\n\
     \    Datatype.add_datatype\n"
     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
     \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)\n\
@@ -161,7 +161,11 @@
     \val dummy = Addsimps(map (fn (_,eqn) =>\n\
     \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
                      "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
-    \val split_"^tname^"_case = prove_goal thy split_"^tname^"_eqn\n\
+    \val split_"^tname^"_case = prove_goal thy (#1(split_"^tname^"_eqns))\n\
+    \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
+      ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
+    \            ALLGOALS Asm_simp_tac]);\n\
+    \val split_"^tname^"_case_prem = prove_goal thy (#2(split_"^tname^"_eqns))\n\
     \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
       ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
     \            ALLGOALS Asm_simp_tac]);\n\