registering split rules and projected induction rules; ML identifiers more close to Isar theorem names

--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 09:52:23 2009 +0200
@@ -189,13 +189,11 @@
 
 (* add_cases_induct *)
 
-fun add_cases_induct infos induction thy =
+fun add_cases_induct infos inducts thy =
   let
-    val inducts = Project_Rule.projections (ProofContext.init thy) induction;
-
-    fun named_rules (name, {index, exhaustion, ...}: info) =
+    fun named_rules (name, {index, exhaust, ...}: info) =
       [((Binding.empty, nth inducts index), [Induct.induct_type name]),
-       ((Binding.empty, exhaustion), [Induct.cases_type name])];
+       ((Binding.empty, exhaust), [Induct.cases_type name])];
     fun unnamed_rule i =
       ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
   in
@@ -307,9 +305,9 @@
 
 (**** make datatype info ****)
 
-fun make_dt_info alt_names descr sorts induct reccomb_names rec_thms
-    (((((((((i, (_, (tname, _, _))), case_name), case_thms),
-      exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) =
+fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms
+    ((((((((((i, (_, (tname, _, _))), case_name), case_thms),
+      exhaust_thm), distinct_thm), inject), splits), nchotomy), case_cong), weak_case_cong) =
   (tname,
    {index = i,
     alt_names = alt_names,
@@ -319,10 +317,11 @@
     rec_rewrites = rec_thms,
     case_name = case_name,
     case_rewrites = case_thms,
-    induction = induct,
-    exhaustion = exhaustion_thm,
+    inducts = inducts,
+    exhaust = exhaust_thm,
     distinct = distinct_thm,
     inject = inject,
+    splits = splits,
     nchotomy = nchotomy,
     case_cong = case_cong,
     weak_case_cong = weak_case_cong});
@@ -342,6 +341,7 @@
     val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
       DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
         types_syntax constr_syntax case_names_induct;
+    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
 
     val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
       sorts induct case_names_exhausts thy2;
@@ -360,9 +360,9 @@
       descr sorts thy9;
 
     val dt_infos = map
-      (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
+      (make_dt_info (SOME new_type_names) (flat descr) sorts (inducts, induct) reccomb_names rec_thms)
       ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
-        casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
+        casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
     val dt_names = map fst dt_infos;
@@ -374,7 +374,7 @@
       |> add_rules simps case_thms rec_thms inject distinct
           weak_case_congs (Simplifier.attrib (op addcongs))
       |> put_dt_infos dt_infos
-      |> add_cases_induct dt_infos induct
+      |> add_cases_induct dt_infos inducts
       |> Sign.parent_path
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
       |> DatatypeInterpretation.data (config, map fst dt_infos);
@@ -427,10 +427,11 @@
       ||>> store_thmss "distinct" new_type_names distinct
       ||> Sign.add_path (space_implode "_" new_type_names)
       ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
+    val inducts = Project_Rule.projections (ProofContext.init thy10) induct';
 
-    val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms)
+    val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct') reccomb_names rec_thms)
       ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
-        map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
+        map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
     val dt_names = map fst dt_infos;
@@ -441,7 +442,7 @@
       |> add_rules simps case_thms rec_thms inject distinct
            weak_case_congs (Simplifier.attrib (op addcongs))
       |> put_dt_infos dt_infos
-      |> add_cases_induct dt_infos induct'
+      |> add_cases_induct dt_infos inducts
       |> Sign.parent_path
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
       |> snd

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Sep 27 09:52:23 2009 +0200
@@ -195,10 +195,11 @@
    rec_rewrites : thm list,
    case_name : string,
    case_rewrites : thm list,
-   induction : thm,
-   exhaustion : thm,
+   inducts : thm list * thm,
+   exhaust : thm,
    distinct : simproc_dist,
    inject : thm list,
+   splits : thm * thm,
    nchotomy : thm,
    case_cong : thm,
    weak_case_cong : thm};

--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Sep 27 09:52:23 2009 +0200
@@ -38,7 +38,7 @@
 
 fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
 
-fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy =
+fun make_ind sorts ({descr, rec_names, rec_rewrites, inducts = (_, induct), ...} : info) is thy =
   let
     val recTs = get_rec_types descr sorts;
     val pnames = if length descr = 1 then ["P"]
@@ -113,18 +113,18 @@
           (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
     val cert = cterm_of thy;
     val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
-      (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
+      (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
 
     val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
       (fn prems =>
          [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
-          rtac (cterm_instantiate inst induction) 1,
+          rtac (cterm_instantiate inst induct) 1,
           ALLGOALS ObjectLogic.atomize_prems_tac,
           rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
           REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
             REPEAT (etac allE i) THEN atac i)) 1)]);
 
-    val ind_name = Thm.get_name induction;
+    val ind_name = Thm.get_name induct;
     val vs = map (fn i => List.nth (pnames, i)) is;
     val (thm', thy') = thy
       |> Sign.root_path
@@ -157,7 +157,7 @@
   in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
 
 
-fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy =
+fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaust, ...} : info) thy =
   let
     val cert = cterm_of thy;
     val rT = TFree ("'P", HOLogic.typeS);
@@ -187,12 +187,12 @@
       HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
         list_comb (r, rs @ [y'])))))
       (fn prems =>
-         [rtac (cterm_instantiate [(cert y, cert y')] exhaustion) 1,
+         [rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
           ALLGOALS (EVERY'
             [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
              resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
 
-    val exh_name = Thm.get_name exhaustion;
+    val exh_name = Thm.get_name exhaust;
     val (thm', thy') = thy
       |> Sign.root_path
       |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
@@ -210,7 +210,7 @@
 
   in Extraction.add_realizers_i
     [(exh_name, (["P"], r', prf)),
-     (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
+     (exh_name, ([], Extraction.nullt, prf_of exhaust))] thy'
   end;
 
 fun add_dt_realizers config names thy =

--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sun Sep 27 09:52:23 2009 +0200
@@ -38,7 +38,7 @@
 (** theory context references **)
 
 fun exh_thm_of (dt_info : info Symtab.table) tname =
-  #exhaustion (the (Symtab.lookup dt_info tname));
+  #exhaust (the (Symtab.lookup dt_info tname));
 
 (******************************************************************************)
 
@@ -389,7 +389,7 @@
     fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
       let
         val (_, (tname, _, _)) = hd ds;
-        val {induction, ...} = the (Symtab.lookup dt_info tname);
+        val induct = (snd o #inducts o the o Symtab.lookup dt_info) tname;
 
         fun mk_ind_concl (i, _) =
           let
@@ -410,7 +410,7 @@
 
         val inj_thm = SkipProof.prove_global thy5 [] []
           (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
-            [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+            [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
              REPEAT (EVERY
                [rtac allI 1, rtac impI 1,
                 exh_tac (exh_thm_of dt_info) 1,
@@ -436,7 +436,7 @@
         val elem_thm = 
             SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
               (fn _ =>
-               EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+               EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
                 rewrite_goals_tac rewrites,
                 REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
                   ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);

--- a/src/HOL/Tools/Function/fundef_datatype.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML	Sun Sep 27 09:52:23 2009 +0200
@@ -145,7 +145,7 @@
          let
              val T = fastype_of v
              val (tname, _) = dest_Type T
-             val {exhaustion=case_thm, ...} = Datatype.the_info thy tname
+             val {exhaust=case_thm, ...} = Datatype.the_info thy tname
              val constrs = inst_constrs_of thy T
              val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
          in

--- a/src/HOL/Tools/Function/size.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML	Sun Sep 27 09:52:23 2009 +0200
@@ -59,7 +59,7 @@
 
 fun prove_size_thms (info : info) new_type_names thy =
   let
-    val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
+    val {descr, alt_names, sorts, rec_names, rec_rewrites, inducts = (_, induct), ...} = info;
     val l = length new_type_names;
     val alt_names' = (case alt_names of
       NONE => replicate l NONE | SOME names => map SOME names);
@@ -169,7 +169,7 @@
            map (mk_unfolded_size_eq (AList.lookup op =
                (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
              (xs ~~ recTs2 ~~ rec_combs2))))
-        (fn _ => (indtac induction xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
+        (fn _ => (indtac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
 
     val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
     val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';

--- a/src/HOL/Tools/TFL/casesplit.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Sun Sep 27 09:52:23 2009 +0200
@@ -96,7 +96,7 @@
                    | TVar((s,i),_) => error ("Free variable: " ^ s)
       val dt = Datatype.the_info thy ty_str
     in
-      cases_thm_of_induct_thm (#induction dt)
+      cases_thm_of_induct_thm (snd (#inducts dt))
     end;
 
 (*

--- a/src/HOL/Tools/old_primrec.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Sun Sep 27 09:52:23 2009 +0200
@@ -230,15 +230,15 @@
               (tname, dt)::(find_dts dt_info tnames' tnames)
             else find_dts dt_info tnames' tnames);
 
-fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
+fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns =
   let
     fun constrs_of (_, (_, _, cs)) =
       map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
-    val params_of = these o AList.lookup (op =) (List.concat (map constrs_of rec_eqns));
+    val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
   in
-    induction
-    |> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr)))
-    |> RuleCases.save induction
+    induct
+    |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
+    |> RuleCases.save induct
   end;
 
 local