Added exhaustion thm and exhaust_tac for each datatype.

--- a/src/HOL/NatDef.ML	Wed May 21 17:31:12 1997 +0200
+++ b/src/HOL/NatDef.ML	Thu May 22 09:20:28 1997 +0200
@@ -46,13 +46,6 @@
           COND (Datatype.occs_in_prems a (i+1)) all_tac
                (rename_last_tac a [""] (i+1))];
 
-(*Install 'automatic' induction tactic, pretending nat is a datatype *)
-(*except for induct_tac, everything is dummy*)
-datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
-  constructors = [], induct_tac = nat_ind_tac,
-  nchotomy = flexpair_def, case_cong = flexpair_def})];
-
-
 (*A special form of induction for reasoning about m<n and m-n*)
 val prems = goal thy
     "[| !!x. P x 0;  \
@@ -76,6 +69,14 @@
 by (Blast_tac 1);
 qed "natE";
 
+(*Install 'automatic' induction tactic, pretending nat is a datatype *)
+(*except for induct_tac, everything is dummy*)
+datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
+  constructors = [], induct_tac = nat_ind_tac,
+  exhaustion = natE, exhaust_tac = fn v => res_inst_tac [("n",v)] natE,
+  nchotomy = flexpair_def, case_cong = flexpair_def})];
+
+
 (*** Isomorphisms: Abs_Nat and Rep_Nat ***)
 
 (*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat),

--- a/src/HOL/datatype.ML	Wed May 21 17:31:12 1997 +0200
+++ b/src/HOL/datatype.ML	Thu May 22 09:20:28 1997 +0200
@@ -798,6 +798,21 @@
  end
  handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"};
 
+(*---------------------------------------------------------------------------
+ * Turn nchotomy into exhaustion:
+ *    [| !!y1..yi. v = C1 y1..yi ==> P; ...; !!y1..yj. v = Cn y1..yj ==> P |]
+ *    ==> P
+ *---------------------------------------------------------------------------*)
+fun mk_exhaust nchotomy =
+  let val tac = rtac impI 1 THEN
+                REPEAT(SOMEGOAL(eresolve_tac [disjE,exE]))
+  in standard(rule_by_tactic tac (nchotomy RS spec RS rev_mp)) end;
+
+(* find name of v in exhaustion: *)
+fun exhaust_var thm =
+  let val _ $ ( _ $ Var((x,_),_) $ _ ) =
+        hd(Logic.strip_assums_hyp(hd(prems_of thm)))
+  in x end;
 
 (*---------------------------------------------------------------------------
  * Brings the preceeding functions together.
@@ -841,6 +856,9 @@
      fun const s = Const(s, the(Sign.const_type sign s))
      val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
      val {nchotomy,case_cong} = case_thms sign case_rewrites itac
+     val exhaustion = mk_exhaust nchotomy
+     val exh_var = exhaust_var exhaustion;
+     fun exhaust_tac a = res_inst_tac [(exh_var,a)] exhaustion;
      fun induct_tac a i =
            STATE(fn st =>
              (if Datatype.occs_in_prems a i st
@@ -853,6 +871,8 @@
         case_rewrites = map mk_rw case_rewrites,
         induct_tac = induct_tac,
         nchotomy = nchotomy,
+        exhaustion = exhaustion,
+        exhaust_tac = exhaust_tac,
         case_cong = case_cong})
  end
 end;

--- a/src/HOL/simpdata.ML	Wed May 21 17:31:12 1997 +0200
+++ b/src/HOL/simpdata.ML	Thu May 22 09:20:28 1997 +0200
@@ -351,7 +351,9 @@
                    case_rewrites:thm list,
                    constructors:term list,
                    induct_tac: string -> int -> tactic,
-                   nchotomy:thm,
+                   nchotomy: thm,
+                   exhaustion: thm,
+                   exhaust_tac: string -> int -> tactic,
                    case_cong:thm};
 
 exception DT_DATA of (string * dtype_info) list;

--- a/src/HOL/thy_data.ML	Wed May 21 17:31:12 1997 +0200
+++ b/src/HOL/thy_data.ML	Thu May 22 09:20:28 1997 +0200
@@ -49,27 +49,48 @@
               in (map #case_cong info, flat (map #case_rewrites info)) end;
   in {case_congs = congs, case_rewrites = rewrites} end;
 
+local
+
+fun find_tname var Bi =
+  let val frees = map dest_Free (term_frees Bi)
+      val params = Logic.strip_params Bi;
+  in case assoc (frees@params, var) of
+       None => error("No such variable in subgoal: " ^ quote var)
+     | Some(Type(tn,_)) => tn
+     | _ => error("Cannot induct on type of " ^ quote var)
+  end;
+
+fun get_dt_info sign tn =
+      case get_thydata (thyname_of_sign sign) "datatypes" of
+        None => error ("No such datatype: " ^ quote tn)
+      | Some (DT_DATA ds) =>
+          case assoc (ds, tn) of
+            Some info => info
+          | None => error ("Not a datatype: " ^ quote tn)
+
+in
+
 (* generic induction tactic for datatypes *)
 fun induct_tac var i =
-  let fun find_tname Bi =
-        let val frees = map dest_Free (term_frees Bi)
-            val params = Logic.strip_params Bi;
-        in case assoc (frees@params, var) of
-             None => error("No such variable in subgoal: " ^ quote var)
-           | Some(Type(tn,_)) => tn
-           | _ => error("Cannot induct on type of " ^ quote var)
-        end;
-      fun get_ind_tac sign tn =
-        (case get_thydata (thyname_of_sign sign) "datatypes" of
-           None => error ("No such datatype: " ^ quote tn)
-         | Some (DT_DATA ds) =>
-             (case assoc (ds, tn) of
-                Some {induct_tac, ...} => induct_tac
-              | None => error ("Not a datatype: " ^ quote tn)));
-      fun induct state =
+  let fun induct state =
+        let val (_, _, Bi, _) = dest_state (state, i)
+            val sign = #sign(rep_thm state)
+            val tn = find_tname var Bi
+            val ind_tac = #induct_tac(get_dt_info sign tn)
+        in ind_tac var i end
+  in STATE induct end;
+
+(* generic exhaustion tactic for datatypes *)
+fun exhaust_tac var i =
+  let fun exhaust state =
         let val (_, _, Bi, _) = dest_state (state, i) 
-        in get_ind_tac (#sign(rep_thm state)) (find_tname Bi) var i end
-  in STATE induct end;
+            val sign = #sign(rep_thm state)
+            val tn = find_tname var Bi
+            val exh_tac = #exhaust_tac(get_dt_info sign tn)
+        in exh_tac var i end
+  in STATE exhaust end;
+
+end;
 
 (*Must be redefined in order to refer to the new instance of bind_thm
   created by init_thy_reader.*)