src/HOL/Tools/inductive_realizer.ML
changeset 24157 409cd6eaa7ea
parent 23590 ad95084a5c63
child 24712 64ed05609568
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Aug 06 16:05:25 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Aug 06 16:08:01 2007 +0200
     1.3 @@ -271,6 +271,8 @@
     1.4        (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
     1.5    end;
     1.6  
     1.7 +fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
     1.8 +
     1.9  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
    1.10    let
    1.11      val qualifier = NameSpace.qualifier (name_of_thm induct);
    1.12 @@ -365,9 +367,12 @@
    1.13  
    1.14      fun add_ind_realizer (thy, Ps) =
    1.15        let
    1.16 +        val vs' = rename (map (pairself (fst o fst o dest_Var))
    1.17 +          (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop
    1.18 +            (hd (prems_of (hd inducts))))), nparms))) vs;
    1.19          val rs = indrule_realizer thy induct raw_induct rsets params'
    1.20 -          (vs @ Ps) rec_names rss' intrs dummies;
    1.21 -        val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs @ Ps) r
    1.22 +          (vs' @ Ps) rec_names rss' intrs dummies;
    1.23 +        val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
    1.24            (prop_of ind)) (rs ~~ inducts);
    1.25          val used = foldr add_term_free_names [] rlzs;
    1.26          val rnames = Name.variant_list used (replicate (length inducts) "r");
    1.27 @@ -391,22 +396,22 @@
    1.28               [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
    1.29                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
    1.30          val (thm', thy') = PureThy.store_thm ((space_implode "_"
    1.31 -          (NameSpace.qualified qualifier "induct" :: vs @ Ps @
    1.32 +          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @
    1.33               ["correctness"]), thm), []) thy;
    1.34          val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
    1.35            (DatatypeAux.split_conj_thm thm');
    1.36          val ([thms'], thy'') = PureThy.add_thmss
    1.37            [((space_implode "_"
    1.38 -             (NameSpace.qualified qualifier "inducts" :: vs @ Ps @
    1.39 +             (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
    1.40                 ["correctness"]), thms), [])] thy';
    1.41          val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
    1.42        in
    1.43          Extraction.add_realizers_i
    1.44            (map (fn (((ind, corr), rlz), r) =>
    1.45 -              mk_realizer thy' (vs @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
    1.46 +              mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
    1.47              realizers @ (case realizers of
    1.48               [(((ind, corr), rlz), r)] =>
    1.49 -               [mk_realizer thy' (vs @ Ps) (NameSpace.qualified qualifier "induct",
    1.50 +               [mk_realizer thy' (vs' @ Ps) (NameSpace.qualified qualifier "induct",
    1.51                    ind, corr, rlz, r)]
    1.52             | _ => [])) thy''
    1.53        end;