For each datatype `t' there is now a theorem `split_t_case' of the form

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)))

The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x
to (..t.. & ..t..) --> P t
(and similarly for t=x).

--- a/src/HOL/List.ML	Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/List.ML	Thu Oct 30 09:45:03 1997 +0100
@@ -48,13 +48,7 @@
 
 (** list_case **)
 
-goal thy
- "P(list_case a f xs) = ((xs=[] --> P(a)) & \
-\                        (!y ys. xs=y#ys --> P(f y ys)))";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-qed "expand_list_case";
+val expand_list_case = split_list_case;
 
 val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
 by (induct_tac "xs" 1);

--- a/src/HOL/NatDef.ML	Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/NatDef.ML	Thu Oct 30 09:45:03 1997 +0100
@@ -722,7 +722,7 @@
 
 
 (* add function nat_add_primrec *) 
-val (_, nat_add_primrec, _) = Datatype.add_datatype
+val (_, nat_add_primrec, _, _) = Datatype.add_datatype
 ([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([],
 "nat")], NoSyn)]) (Theory.add_name "Arith" HOL.thy);
 (*pretend Arith is part of the basic theory to fool package*)

--- a/src/HOL/Option.ML	Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/Option.ML	Thu Oct 30 09:45:03 1997 +0100
@@ -6,11 +6,4 @@
 Derived rules
 *)
 
-open Option;
-
-goal Option.thy "P(case opt of None => a | Some(x) => b x) = \
-\                ((opt = None --> P a) & (!x. opt = Some x --> P(b x)))";
-by (option.induct_tac "opt" 1);
-by (Simp_tac 1);
-by (Asm_full_simp_tac 1);
-qed "expand_option_case";
+val expand_option_case = split_option_case;

--- a/src/HOL/datatype.ML	Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/datatype.ML	Thu Oct 30 09:45:03 1997 +0100
@@ -443,6 +443,25 @@
       val size_eqns  = map size_eqn cons_list;
 
 (* -------------------------------------------------------------------- *)
+(* The split equation                                                   *) 
+
+      local
+      val fs = map (fn i => "f"^(string_of_int i)) (1 upto num_of_cons);
+
+      fun split1case ((_,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 rhss  = map split1case (cons_list ~~ fs);
+      val rhs = space_implode " & " rhss;
+      val lhs = "P(" ^ t_case ^ " " ^ (space_implode " " fs) ^" "^ tname^"0)"
+      in
+      val split_eqn = lhs ^ " = (" ^ rhs ^ ")"
+      end;
+
+(* -------------------------------------------------------------------- *)
+
       val consts = 
         map const_type cons_list
         @ (if num_of_cons < dtK then []
@@ -512,7 +531,7 @@
            |> Theory.add_arities arities
            |> Theory.add_consts consts
            |> Theory.add_trrules xrules
-           |> Theory.add_axioms rules, add_primrec, size_eqns)
+           |> Theory.add_axioms rules, add_primrec, size_eqns, split_eqn)
     end
 
 (*Warn if the (induction) variable occurs Free among the premises, which

--- a/src/HOL/simpdata.ML	Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/simpdata.ML	Thu Oct 30 09:45:03 1997 +0100
@@ -145,10 +145,22 @@
                  "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
                  "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];
 
-(*** Simplification procedure for turning  ? x. ... & x = t & ...
-     into                                  ? x. x = t & ... & ...
-     where the latter can be rewritten via (? x. x = t & P(x)) = P(t)
- ***)
+(*** Simplification procedures for turning
+
+            ? x. ... & x = t & ...
+     into   ? x. x = t & ... & ...
+     where the `? x. x = t &' in the latter formula is eliminated
+           by ordinary simplification. 
+
+     and   ! x. (... & x = t & ...) --> P x
+     into  ! x. x = t --> (... & ...) --> P x
+     where the `!x. x=t -->' in the latter formula is eliminated
+           by ordinary simplification.
+
+NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"
+   "!x. x=t --> P(x)" and "!x. t=x --> P(x)"
+   must be taken care of by ordinary rewrite rules.
+***)
 
 local
 
@@ -171,25 +183,49 @@
                  | None => None))))
   | extract _ = None;
 
-fun prove_eq(ceqt) =
+fun prove_ex_eq(ceqt) =
   let val tac = rtac eq_reflection 1 THEN rtac iffI 1 THEN
                 ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
                  rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)])
   in rule_by_tactic tac (trivial ceqt) end;
 
-fun rearrange sg _ (F as ex $ Abs(x,T,P)) =
+fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
      (case extract P of
         None => None
       | Some(eq,Q) =>
           let val ceqt = cterm_of sg
                        (Logic.mk_equals(F,ex $ Abs(x,T,HOLogic.conj$eq$Q)))
-          in Some(prove_eq ceqt) end)
-  | rearrange _ _ _ = None;
+          in Some(prove_ex_eq ceqt) end)
+  | rearrange_ex _ _ _ = None;
+
+val ex_pattern =
+  read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
 
-val pattern = read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
+fun prove_all_eq(ceqt) =
+  let fun tac _ = [EVERY1[rtac eq_reflection, rtac iffI,
+                       rtac allI, etac allE, rtac impI, rtac impI, etac mp,
+                          REPEAT o (etac conjE),
+                          REPEAT o (ares_tac [conjI] ORELSE' etac sym),
+                       rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
+                          etac impE, atac ORELSE' etac sym, etac mp,
+                          REPEAT o (ares_tac [conjI])]]
+  in prove_goalw_cterm [] ceqt tac end;
+
+fun rearrange_all sg _ (F as all $ Abs(x,T,Const("op -->",_)$P$Q)) =
+     (case extract P of
+        None => None
+      | Some(eq,P') =>
+          let val R = HOLogic.imp $ eq $ (HOLogic.imp $ P' $ Q)
+              val ceqt = cterm_of sg (Logic.mk_equals(F,all$Abs(x,T,R)))
+          in Some(prove_all_eq ceqt) end)
+  | rearrange_all _ _ _ = None;
+
+val all_pattern =
+  read_cterm (sign_of HOL.thy) ("! x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
 
 in
-val defEX_regroup = mk_simproc "defined EX" [pattern] rearrange;
+val defEX_regroup = mk_simproc "defined EX" [ex_pattern] rearrange_ex;
+val defALL_regroup = mk_simproc "defined ALL" [all_pattern] rearrange_all;
 end;
 
 
@@ -386,7 +422,7 @@
        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
        not_all, not_ex, cases_simp]
      @ ex_simps @ all_simps @ simp_thms)
-     addsimprocs [defEX_regroup]
+     addsimprocs [defALL_regroup,defEX_regroup]
      addcongs [imp_cong];
 
 qed_goal "if_distrib" HOL.thy

--- a/src/HOL/thy_syntax.ML	Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/thy_syntax.ML	Thu Oct 30 09:45:03 1997 +0100
@@ -126,9 +126,10 @@
 
   (*generate string for calling add_datatype and build_record*)
   fun mk_params ((ts, tname), cons) =
-   ("val (thy," ^ tname ^ "_add_primrec," ^ tname ^ "_size_eqns) = Datatype.add_datatype\n"
+   ("val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqn) =\n\
+    \    Datatype.add_datatype\n"
     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
-    \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
+    \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)"
     ,
     "val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
     \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
@@ -161,9 +162,19 @@
       tname ^ ".distinct;\n\
     \val dummy = Addsimps(map (fn (_,eqn) =>\n\
     \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
-                     "] eqn (fn _ => [Simp_tac 1]))\n" ^
-    tname^"_size_eqns)\n"
+                     "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
+    \val split_"^tname^"_case = prove_goal thy split_"^tname^"_eqn\n\
+    \  (fn _ => [#exhaust_tac(snd(hd(!datatypes))) \""^tname^"0\" 1,\n\
+    \            ALLGOALS Asm_simp_tac])"
    );
+(*
+The #exhaust_tac(snd(hd(!datatypes))) in the proof of split_"^tname^"_case
+is a hack. Ideally I would just write exhaust_tac, but the latter extracts the
+specific exhaustion tactic from the theory associated with the proof
+state. However, the exhaustion tactic for the current datatype has only just
+been added to !datatypes (a few lines above) but is not yet associated with
+the theory. Hope this can be simplified in the future.
+*)
 
   (*parsers*)
   val tvars = type_args >> map (cat "dtVar");