src/HOL/Tools/inductive_realizer.ML
changeset 22790 e1cff9268177
parent 22606 962f824c2df9
child 23577 c5b93c69afd3
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Apr 25 15:24:15 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Apr 25 15:25:22 2007 +0200
     1.3 @@ -21,46 +21,6 @@
     1.4       [(name, _)] => name
     1.5     | _ => error ("name_of_thm: bad proof of theorem\n" ^ string_of_thm thm));
     1.6  
     1.7 -(* infer order of variables in intro rules from order of quantifiers in elim rule *)
     1.8 -fun infer_intro_vars elim arity intros =
     1.9 -  let
    1.10 -    val thy = theory_of_thm elim;
    1.11 -    val _ :: cases = prems_of elim;
    1.12 -    val used = map (fst o fst) (Term.add_vars (prop_of elim) []);
    1.13 -    fun mtch (t, u) =
    1.14 -      let
    1.15 -        val params = Logic.strip_params t;
    1.16 -        val vars = map (Var o apfst (rpair 0))
    1.17 -          (Name.variant_list used (map fst params) ~~ map snd params);
    1.18 -        val ts = map (curry subst_bounds (rev vars))
    1.19 -          (List.drop (Logic.strip_assums_hyp t, arity));
    1.20 -        val us = Logic.strip_imp_prems u;
    1.21 -        val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
    1.22 -          (Vartab.empty, Vartab.empty);
    1.23 -      in
    1.24 -        map (Envir.subst_vars tab) vars
    1.25 -      end
    1.26 -  in
    1.27 -    map (mtch o apsnd prop_of) (cases ~~ intros)
    1.28 -  end;
    1.29 -
    1.30 -(* read off arities of inductive predicates from raw induction rule *)
    1.31 -fun arities_of induct =
    1.32 -  map (fn (_ $ t $ u) =>
    1.33 -      (fst (dest_Const (head_of t)), length (snd (strip_comb u))))
    1.34 -    (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.35 -
    1.36 -(* read off parameters of inductive predicate from raw induction rule *)
    1.37 -fun params_of induct =
    1.38 -  let
    1.39 -    val (_ $ t $ u :: _) =
    1.40 -      HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
    1.41 -    val (_, ts) = strip_comb t;
    1.42 -    val (_, us) = strip_comb u
    1.43 -  in
    1.44 -    List.take (ts, length ts - length us)
    1.45 -  end;
    1.46 -
    1.47  val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
    1.48  
    1.49  fun prf_of thm =
    1.50 @@ -311,16 +271,6 @@
    1.51        (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
    1.52    end;
    1.53  
    1.54 -fun partition_rules induct intrs =
    1.55 -  let
    1.56 -    fun name_of t = fst (dest_Const (head_of t));
    1.57 -    val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
    1.58 -    val sets = map (name_of o fst o HOLogic.dest_imp) ts;
    1.59 -  in
    1.60 -    map (fn s => (s, filter
    1.61 -      (equal s o name_of o HOLogic.dest_Trueprop o concl_of) intrs)) sets
    1.62 -  end;
    1.63 -
    1.64  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
    1.65    let
    1.66      val qualifier = NameSpace.qualifier (name_of_thm induct);
    1.67 @@ -328,13 +278,14 @@
    1.68        (NameSpace.qualified qualifier "inducts"));
    1.69      val iTs = term_tvars (prop_of (hd intrs));
    1.70      val ar = length vs + length iTs;
    1.71 -    val params = params_of raw_induct;
    1.72 -    val arities = arities_of raw_induct;
    1.73 +    val params = InductivePackage.params_of raw_induct;
    1.74 +    val arities = InductivePackage.arities_of raw_induct;
    1.75      val nparms = length params;
    1.76      val params' = map dest_Var params;
    1.77 -    val rss = partition_rules raw_induct intrs;
    1.78 +    val rss = InductivePackage.partition_rules raw_induct intrs;
    1.79      val rss' = map (fn (((s, rs), (_, arity)), elim) =>
    1.80 -      (s, (infer_intro_vars elim arity rs ~~ rs))) (rss ~~ arities ~~ elims);
    1.81 +      (s, (InductivePackage.infer_intro_vars elim arity rs ~~ rs)))
    1.82 +        (rss ~~ arities ~~ elims);
    1.83      val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
    1.84      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
    1.85