registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
authorhaftmann
Sun Sep 27 09:52:23 2009 +0200 (2009-09-27)
changeset 32712ec5976f4d3d8
parent 32706 b68f3afdc137
child 32713 b8381161adb1
registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/Function/fundef_datatype.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/old_primrec.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Sep 25 10:20:03 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 09:52:23 2009 +0200
     1.3 @@ -189,13 +189,11 @@
     1.4  
     1.5  (* add_cases_induct *)
     1.6  
     1.7 -fun add_cases_induct infos induction thy =
     1.8 +fun add_cases_induct infos inducts thy =
     1.9    let
    1.10 -    val inducts = Project_Rule.projections (ProofContext.init thy) induction;
    1.11 -
    1.12 -    fun named_rules (name, {index, exhaustion, ...}: info) =
    1.13 +    fun named_rules (name, {index, exhaust, ...}: info) =
    1.14        [((Binding.empty, nth inducts index), [Induct.induct_type name]),
    1.15 -       ((Binding.empty, exhaustion), [Induct.cases_type name])];
    1.16 +       ((Binding.empty, exhaust), [Induct.cases_type name])];
    1.17      fun unnamed_rule i =
    1.18        ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
    1.19    in
    1.20 @@ -307,9 +305,9 @@
    1.21  
    1.22  (**** make datatype info ****)
    1.23  
    1.24 -fun make_dt_info alt_names descr sorts induct reccomb_names rec_thms
    1.25 -    (((((((((i, (_, (tname, _, _))), case_name), case_thms),
    1.26 -      exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) =
    1.27 +fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms
    1.28 +    ((((((((((i, (_, (tname, _, _))), case_name), case_thms),
    1.29 +      exhaust_thm), distinct_thm), inject), splits), nchotomy), case_cong), weak_case_cong) =
    1.30    (tname,
    1.31     {index = i,
    1.32      alt_names = alt_names,
    1.33 @@ -319,10 +317,11 @@
    1.34      rec_rewrites = rec_thms,
    1.35      case_name = case_name,
    1.36      case_rewrites = case_thms,
    1.37 -    induction = induct,
    1.38 -    exhaustion = exhaustion_thm,
    1.39 +    inducts = inducts,
    1.40 +    exhaust = exhaust_thm,
    1.41      distinct = distinct_thm,
    1.42      inject = inject,
    1.43 +    splits = splits,
    1.44      nchotomy = nchotomy,
    1.45      case_cong = case_cong,
    1.46      weak_case_cong = weak_case_cong});
    1.47 @@ -342,6 +341,7 @@
    1.48      val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
    1.49        DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
    1.50          types_syntax constr_syntax case_names_induct;
    1.51 +    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
    1.52  
    1.53      val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
    1.54        sorts induct case_names_exhausts thy2;
    1.55 @@ -360,9 +360,9 @@
    1.56        descr sorts thy9;
    1.57  
    1.58      val dt_infos = map
    1.59 -      (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
    1.60 +      (make_dt_info (SOME new_type_names) (flat descr) sorts (inducts, induct) reccomb_names rec_thms)
    1.61        ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
    1.62 -        casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.63 +        casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.64  
    1.65      val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
    1.66      val dt_names = map fst dt_infos;
    1.67 @@ -374,7 +374,7 @@
    1.68        |> add_rules simps case_thms rec_thms inject distinct
    1.69            weak_case_congs (Simplifier.attrib (op addcongs))
    1.70        |> put_dt_infos dt_infos
    1.71 -      |> add_cases_induct dt_infos induct
    1.72 +      |> add_cases_induct dt_infos inducts
    1.73        |> Sign.parent_path
    1.74        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    1.75        |> DatatypeInterpretation.data (config, map fst dt_infos);
    1.76 @@ -427,10 +427,11 @@
    1.77        ||>> store_thmss "distinct" new_type_names distinct
    1.78        ||> Sign.add_path (space_implode "_" new_type_names)
    1.79        ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
    1.80 +    val inducts = Project_Rule.projections (ProofContext.init thy10) induct';
    1.81  
    1.82 -    val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms)
    1.83 +    val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct') reccomb_names rec_thms)
    1.84        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
    1.85 -        map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.86 +        map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.87  
    1.88      val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
    1.89      val dt_names = map fst dt_infos;
    1.90 @@ -441,7 +442,7 @@
    1.91        |> add_rules simps case_thms rec_thms inject distinct
    1.92             weak_case_congs (Simplifier.attrib (op addcongs))
    1.93        |> put_dt_infos dt_infos
    1.94 -      |> add_cases_induct dt_infos induct'
    1.95 +      |> add_cases_induct dt_infos inducts
    1.96        |> Sign.parent_path
    1.97        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.98        |> snd
     2.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Sep 25 10:20:03 2009 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Sep 27 09:52:23 2009 +0200
     2.3 @@ -195,10 +195,11 @@
     2.4     rec_rewrites : thm list,
     2.5     case_name : string,
     2.6     case_rewrites : thm list,
     2.7 -   induction : thm,
     2.8 -   exhaustion : thm,
     2.9 +   inducts : thm list * thm,
    2.10 +   exhaust : thm,
    2.11     distinct : simproc_dist,
    2.12     inject : thm list,
    2.13 +   splits : thm * thm,
    2.14     nchotomy : thm,
    2.15     case_cong : thm,
    2.16     weak_case_cong : thm};
     3.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Fri Sep 25 10:20:03 2009 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Sep 27 09:52:23 2009 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4  
     3.5  fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
     3.6  
     3.7 -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy =
     3.8 +fun make_ind sorts ({descr, rec_names, rec_rewrites, inducts = (_, induct), ...} : info) is thy =
     3.9    let
    3.10      val recTs = get_rec_types descr sorts;
    3.11      val pnames = if length descr = 1 then ["P"]
    3.12 @@ -113,18 +113,18 @@
    3.13            (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
    3.14      val cert = cterm_of thy;
    3.15      val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
    3.16 -      (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
    3.17 +      (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
    3.18  
    3.19      val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
    3.20        (fn prems =>
    3.21           [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
    3.22 -          rtac (cterm_instantiate inst induction) 1,
    3.23 +          rtac (cterm_instantiate inst induct) 1,
    3.24            ALLGOALS ObjectLogic.atomize_prems_tac,
    3.25            rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
    3.26            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
    3.27              REPEAT (etac allE i) THEN atac i)) 1)]);
    3.28  
    3.29 -    val ind_name = Thm.get_name induction;
    3.30 +    val ind_name = Thm.get_name induct;
    3.31      val vs = map (fn i => List.nth (pnames, i)) is;
    3.32      val (thm', thy') = thy
    3.33        |> Sign.root_path
    3.34 @@ -157,7 +157,7 @@
    3.35    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    3.36  
    3.37  
    3.38 -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy =
    3.39 +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaust, ...} : info) thy =
    3.40    let
    3.41      val cert = cterm_of thy;
    3.42      val rT = TFree ("'P", HOLogic.typeS);
    3.43 @@ -187,12 +187,12 @@
    3.44        HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
    3.45          list_comb (r, rs @ [y'])))))
    3.46        (fn prems =>
    3.47 -         [rtac (cterm_instantiate [(cert y, cert y')] exhaustion) 1,
    3.48 +         [rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
    3.49            ALLGOALS (EVERY'
    3.50              [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
    3.51               resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
    3.52  
    3.53 -    val exh_name = Thm.get_name exhaustion;
    3.54 +    val exh_name = Thm.get_name exhaust;
    3.55      val (thm', thy') = thy
    3.56        |> Sign.root_path
    3.57        |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
    3.58 @@ -210,7 +210,7 @@
    3.59  
    3.60    in Extraction.add_realizers_i
    3.61      [(exh_name, (["P"], r', prf)),
    3.62 -     (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
    3.63 +     (exh_name, ([], Extraction.nullt, prf_of exhaust))] thy'
    3.64    end;
    3.65  
    3.66  fun add_dt_realizers config names thy =
     4.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Sep 25 10:20:03 2009 +0200
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sun Sep 27 09:52:23 2009 +0200
     4.3 @@ -38,7 +38,7 @@
     4.4  (** theory context references **)
     4.5  
     4.6  fun exh_thm_of (dt_info : info Symtab.table) tname =
     4.7 -  #exhaustion (the (Symtab.lookup dt_info tname));
     4.8 +  #exhaust (the (Symtab.lookup dt_info tname));
     4.9  
    4.10  (******************************************************************************)
    4.11  
    4.12 @@ -389,7 +389,7 @@
    4.13      fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
    4.14        let
    4.15          val (_, (tname, _, _)) = hd ds;
    4.16 -        val {induction, ...} = the (Symtab.lookup dt_info tname);
    4.17 +        val induct = (snd o #inducts o the o Symtab.lookup dt_info) tname;
    4.18  
    4.19          fun mk_ind_concl (i, _) =
    4.20            let
    4.21 @@ -410,7 +410,7 @@
    4.22  
    4.23          val inj_thm = SkipProof.prove_global thy5 [] []
    4.24            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    4.25 -            [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    4.26 +            [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    4.27               REPEAT (EVERY
    4.28                 [rtac allI 1, rtac impI 1,
    4.29                  exh_tac (exh_thm_of dt_info) 1,
    4.30 @@ -436,7 +436,7 @@
    4.31          val elem_thm = 
    4.32              SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    4.33                (fn _ =>
    4.34 -               EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    4.35 +               EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    4.36                  rewrite_goals_tac rewrites,
    4.37                  REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
    4.38                    ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
     5.1 --- a/src/HOL/Tools/Function/fundef_datatype.ML	Fri Sep 25 10:20:03 2009 +0200
     5.2 +++ b/src/HOL/Tools/Function/fundef_datatype.ML	Sun Sep 27 09:52:23 2009 +0200
     5.3 @@ -145,7 +145,7 @@
     5.4           let
     5.5               val T = fastype_of v
     5.6               val (tname, _) = dest_Type T
     5.7 -             val {exhaustion=case_thm, ...} = Datatype.the_info thy tname
     5.8 +             val {exhaust=case_thm, ...} = Datatype.the_info thy tname
     5.9               val constrs = inst_constrs_of thy T
    5.10               val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
    5.11           in
     6.1 --- a/src/HOL/Tools/Function/size.ML	Fri Sep 25 10:20:03 2009 +0200
     6.2 +++ b/src/HOL/Tools/Function/size.ML	Sun Sep 27 09:52:23 2009 +0200
     6.3 @@ -59,7 +59,7 @@
     6.4  
     6.5  fun prove_size_thms (info : info) new_type_names thy =
     6.6    let
     6.7 -    val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
     6.8 +    val {descr, alt_names, sorts, rec_names, rec_rewrites, inducts = (_, induct), ...} = info;
     6.9      val l = length new_type_names;
    6.10      val alt_names' = (case alt_names of
    6.11        NONE => replicate l NONE | SOME names => map SOME names);
    6.12 @@ -169,7 +169,7 @@
    6.13             map (mk_unfolded_size_eq (AList.lookup op =
    6.14                 (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
    6.15               (xs ~~ recTs2 ~~ rec_combs2))))
    6.16 -        (fn _ => (indtac induction xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
    6.17 +        (fn _ => (indtac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
    6.18  
    6.19      val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
    6.20      val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';
     7.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Fri Sep 25 10:20:03 2009 +0200
     7.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Sun Sep 27 09:52:23 2009 +0200
     7.3 @@ -96,7 +96,7 @@
     7.4                     | TVar((s,i),_) => error ("Free variable: " ^ s)
     7.5        val dt = Datatype.the_info thy ty_str
     7.6      in
     7.7 -      cases_thm_of_induct_thm (#induction dt)
     7.8 +      cases_thm_of_induct_thm (snd (#inducts dt))
     7.9      end;
    7.10  
    7.11  (*
     8.1 --- a/src/HOL/Tools/old_primrec.ML	Fri Sep 25 10:20:03 2009 +0200
     8.2 +++ b/src/HOL/Tools/old_primrec.ML	Sun Sep 27 09:52:23 2009 +0200
     8.3 @@ -230,15 +230,15 @@
     8.4                (tname, dt)::(find_dts dt_info tnames' tnames)
     8.5              else find_dts dt_info tnames' tnames);
     8.6  
     8.7 -fun prepare_induct ({descr, induction, ...}: info) rec_eqns =
     8.8 +fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns =
     8.9    let
    8.10      fun constrs_of (_, (_, _, cs)) =
    8.11        map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
    8.12 -    val params_of = these o AList.lookup (op =) (List.concat (map constrs_of rec_eqns));
    8.13 +    val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
    8.14    in
    8.15 -    induction
    8.16 -    |> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr)))
    8.17 -    |> RuleCases.save induction
    8.18 +    induct
    8.19 +    |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
    8.20 +    |> RuleCases.save induct
    8.21    end;
    8.22  
    8.23  local