Added renaming function to prevent correctness proof for realizer
authorberghofe
Mon Aug 06 16:08:01 2007 +0200 (2007-08-06)
changeset 24157409cd6eaa7ea
parent 24156 99e4722eceb1
child 24158 ebecbe4f53ae
Added renaming function to prevent correctness proof for realizer
of induction rule to fail because of name clashes between parameters
and predicate variables.
src/HOL/Tools/inductive_realizer.ML
     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;