proper induction rule for arbitrarily branching datatype;
authorwenzelm
Tue Jan 16 00:33:40 2001 +0100 (2001-01-16)
changeset 10911eb5721204b38
parent 10910 058775a575db
child 10912 3cf3bb8ee324
proper induction rule for arbitrarily branching datatype;
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jan 16 00:32:38 2001 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jan 16 00:33:40 2001 +0100
     1.3 @@ -238,7 +238,8 @@
     1.4          val induct' = cterm_instantiate ((map cert induct_Ps) ~~
     1.5            (map cert insts)) induct;
     1.6          val (tac, _) = foldl mk_unique_tac
     1.7 -          ((rtac induct' 1, rec_intrs), descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
     1.8 +          (((rtac induct' THEN_ALL_NEW atomize_strip_tac) 1, rec_intrs),
     1.9 +            descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
    1.10  
    1.11        in split_conj_thm (prove_goalw_cterm []
    1.12          (cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac]))
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jan 16 00:32:38 2001 +0100
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 16 00:33:40 2001 +0100
     2.3 @@ -532,7 +532,8 @@
     2.4      val (thy3, (([induct], [rec_thms]), inject)) =
     2.5        thy2 |>
     2.6        Theory.add_path (space_implode "_" new_type_names) |>
     2.7 -      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [case_names_induct])] |>>>
     2.8 +      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
     2.9 +        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>>
    2.10        PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
    2.11        (if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
    2.12        Theory.parent_path |>>>
     3.1 --- a/src/HOL/Tools/datatype_prop.ML	Tue Jan 16 00:32:38 2001 +0100
     3.2 +++ b/src/HOL/Tools/datatype_prop.ML	Tue Jan 16 00:33:40 2001 +0100
     3.3 @@ -113,8 +113,9 @@
     3.4          fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
     3.5                (make_pred k T $ Free (s, T))
     3.6            | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
     3.7 -              HOLogic.mk_Trueprop (HOLogic.all_const T $
     3.8 -                Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0)));
     3.9 +              (Const (InductivePackage.inductive_forall_name,
    3.10 +                  [T --> HOLogic.boolT] ---> HOLogic.boolT) $
    3.11 +                Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0))) |> HOLogic.mk_Trueprop;
    3.12  
    3.13          val recs = filter is_rec_type cargs;
    3.14          val Ts = map (typ_of_dtyp descr' sorts) cargs;
     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jan 16 00:32:38 2001 +0100
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jan 16 00:33:40 2001 +0100
     4.3 @@ -626,7 +626,7 @@
     4.4        map (Free o apfst fst o dest_Var) Ps;
     4.5      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
     4.6  
     4.7 -    val dt_induct = prove_goalw_cterm [] (cert
     4.8 +    val dt_induct = prove_goalw_cterm [InductivePackage.inductive_forall_def] (cert
     4.9        (DatatypeProp.make_ind descr sorts)) (fn prems =>
    4.10          [rtac indrule_lemma' 1, indtac rep_induct 1,
    4.11           EVERY (map (fn (prem, r) => (EVERY
    4.12 @@ -638,7 +638,8 @@
    4.13  
    4.14      val (thy7, [dt_induct']) = thy6 |>
    4.15        Theory.add_path big_name |>
    4.16 -      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    4.17 +      PureThy.add_thms [(("induct", dt_induct),
    4.18 +        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>
    4.19        Theory.parent_path;
    4.20  
    4.21    in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')