src/HOL/Tools/inductive_realizer.ML
changeset 13921 69c627b6b28d
parent 13725 12404b452034
child 13928 d572aeea3ff3
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Apr 23 13:33:55 2003 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Apr 23 18:09:48 2003 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4                  map fastype_of (rev args) ---> conclT), rev args))
     1.5            end
     1.6  
     1.7 -  in fun_of (rev args) [] args' used (Logic.strip_imp_prems rule') end;
     1.8 +  in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
     1.9  
    1.10  fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
    1.11    let
    1.12 @@ -383,20 +383,32 @@
    1.13      val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
    1.14        HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
    1.15  
    1.16 -    fun add_elim_realizer Ps ((((elim, elimR), case_thms), case_name), dummy) thy =
    1.17 +    fun add_elim_realizer Ps
    1.18 +      (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
    1.19        let
    1.20          val (prem :: prems) = prems_of elim;
    1.21 -        val p = Logic.list_implies (prems @ [prem], concl_of elim);
    1.22 +        fun reorder1 (p, intr) =
    1.23 +          foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
    1.24 +            (strip_all p, Term.add_vars ([], prop_of intr));
    1.25 +        fun reorder2 (intr, i) =
    1.26 +          let
    1.27 +            val fs1 = term_vars (prop_of intr);
    1.28 +            val fs2 = Term.add_vars ([], prop_of intr)
    1.29 +          in foldl (fn (t, x) => lambda (Var x) t)
    1.30 +            (list_comb (Bound (i + length fs1), fs1), fs2)
    1.31 +          end;
    1.32 +        val p = Logic.list_implies
    1.33 +          (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
    1.34          val T' = Extraction.etype_of thy (vs @ Ps) [] p;
    1.35          val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
    1.36 -        val Ts = filter_out (equal Extraction.nullT)
    1.37 -          (map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim));
    1.38 +        val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim);
    1.39          val r = if null Ps then Extraction.nullt
    1.40            else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
    1.41              (if dummy then
    1.42                 [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
    1.43               else []) @
    1.44 -            map Bound ((length prems - 1 downto 0) @ [length prems])));
    1.45 +            map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
    1.46 +            [Bound (length prems)]));
    1.47          val rlz = strip_all (Logic.unvarify
    1.48            (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
    1.49          val rews = map mk_meta_eq case_thms;
    1.50 @@ -424,11 +436,11 @@
    1.51           (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c,
    1.52              map Var (rev (Term.add_vars ([], prop_of rule)) \\ params')))) 
    1.53                (flat (map snd rss) ~~ rintr_thms ~~ flat constrss))) thy4;
    1.54 -    val elimps = mapfilter (fn (s, _) => if s mem rsets then
    1.55 -        find_first (fn (thm, _) => s mem term_consts (hd (prems_of thm)))
    1.56 -          (elims ~~ #elims ind_info)
    1.57 +    val elimps = mapfilter (fn (s, intrs) => if s mem rsets then
    1.58 +        apsome (rpair intrs) (find_first (fn (thm, _) =>
    1.59 +          s mem term_consts (hd (prems_of thm))) (elims ~~ #elims ind_info))
    1.60        else None) rss;
    1.61 -    val thy6 = foldl (fn (thy, p as ((((elim, _), _), _), _)) => thy |>
    1.62 +    val thy6 = foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
    1.63        add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
    1.64          (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
    1.65             elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)