# HG changeset patch
# User berghofe
# Date 1026318934 -7200
# Node ID 9b0332344ae29a8cac50d614a8159eeb080a5414
# Parent  0f89104dd377d723d57e63e5173909b89d8b60b6
Simplified proof of induction rule for datatypes involving function types.

diff -r 0f89104dd377 -r 9b0332344ae2 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Jul 10 16:54:07 2002 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Jul 10 18:35:34 2002 +0200
@@ -548,7 +548,7 @@
       thy2 |>
       Theory.add_path (space_implode "_" new_type_names) |>
       PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
-        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>>
+        [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 0f89104dd377 -r 9b0332344ae2 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Wed Jul 10 16:54:07 2002 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Wed Jul 10 18:35:34 2002 +0200
@@ -113,9 +113,8 @@
         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])) =
-              (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;
+              all T $ Abs ("x", T, HOLogic.mk_Trueprop
+                (make_pred k U $ (Free (s, T') $ Bound 0)));
 
         val recs = filter is_rec_type cargs;
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
diff -r 0f89104dd377 -r 9b0332344ae2 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jul 10 16:54:07 2002 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jul 10 18:35:34 2002 +0200
@@ -639,20 +639,19 @@
       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 [InductivePackage.inductive_forall_def] (cert
+    val dt_induct = prove_goalw_cterm [] (cert
       (DatatypeProp.make_ind descr sorts)) (fn prems =>
         [rtac indrule_lemma' 1, indtac rep_induct 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
-              rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
+              dtac FunsD 1, etac CollectD 1]))]))
                 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
 
     val (thy7, [dt_induct']) = thy6 |>
       Theory.add_path big_name |>
-      PureThy.add_thms [(("induct", dt_induct),
-        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>
+      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
       Theory.parent_path;
 
   in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')