# HG changeset patch
# User wenzelm
# Date 979601620 -3600
# Node ID eb5721204b389cde3a23517981604baba486818d
# Parent  058775a575dba1231c4ebb843ae8a3fa58dc23f5
proper induction rule for arbitrarily branching datatype;

diff -r 058775a575db -r eb5721204b38 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jan 16 00:32:38 2001 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jan 16 00:33:40 2001 +0100
@@ -238,7 +238,8 @@
         val induct' = cterm_instantiate ((map cert induct_Ps) ~~
           (map cert insts)) induct;
         val (tac, _) = foldl mk_unique_tac
-          ((rtac induct' 1, rec_intrs), descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
+          (((rtac induct' THEN_ALL_NEW atomize_strip_tac) 1, rec_intrs),
+            descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
 
       in split_conj_thm (prove_goalw_cterm []
         (cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac]))
diff -r 058775a575db -r eb5721204b38 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Jan 16 00:32:38 2001 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 16 00:33:40 2001 +0100
@@ -532,7 +532,8 @@
     val (thy3, (([induct], [rec_thms]), inject)) =
       thy2 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [case_names_induct])] |>>>
+      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
+        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>>
       PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
       (if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
       Theory.parent_path |>>>
diff -r 058775a575db -r eb5721204b38 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Tue Jan 16 00:32:38 2001 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Tue Jan 16 00:33:40 2001 +0100
@@ -113,8 +113,9 @@
         fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
               (make_pred k T $ Free (s, T))
           | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
-              HOLogic.mk_Trueprop (HOLogic.all_const T $
-                Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0)));
+              (Const (InductivePackage.inductive_forall_name,
+                  [T --> HOLogic.boolT] ---> HOLogic.boolT) $
+                Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0))) |> HOLogic.mk_Trueprop;
 
         val recs = filter is_rec_type cargs;
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
diff -r 058775a575db -r eb5721204b38 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jan 16 00:32:38 2001 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jan 16 00:33:40 2001 +0100
@@ -626,7 +626,7 @@
       map (Free o apfst fst o dest_Var) Ps;
     val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
 
-    val dt_induct = prove_goalw_cterm [] (cert
+    val dt_induct = prove_goalw_cterm [InductivePackage.inductive_forall_def] (cert
       (DatatypeProp.make_ind descr sorts)) (fn prems =>
         [rtac indrule_lemma' 1, indtac rep_induct 1,
          EVERY (map (fn (prem, r) => (EVERY
@@ -638,7 +638,8 @@
 
     val (thy7, [dt_induct']) = thy6 |>
       Theory.add_path big_name |>
-      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
+      PureThy.add_thms [(("induct", dt_induct),
+        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>
       Theory.parent_path;
 
   in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')