Added functions arities_of, params_of, partition_rules, and
authorberghofe
Wed Apr 25 15:24:15 2007 +0200 (2007-04-25)
changeset 227894d03dc1cad04
parent 22788 3038bd211582
child 22790 e1cff9268177
Added functions arities_of, params_of, partition_rules, and
infer_intro_vars (from inductive_realizer.ML).
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Apr 25 15:22:57 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Apr 25 15:24:15 2007 +0200
     1.3 @@ -49,6 +49,11 @@
     1.4    val add_inductive_global: bool -> bstring -> bool -> bool -> bool ->
     1.5      (string * typ option * mixfix) list -> (string * typ option) list ->
     1.6      ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
     1.7 +  val arities_of: thm -> (string * int) list
     1.8 +  val params_of: thm -> term list
     1.9 +  val partition_rules: thm -> thm list -> (string * thm list) list
    1.10 +  val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
    1.11 +  val infer_intro_vars: thm -> int -> thm list -> term list list
    1.12    val setup: theory -> theory
    1.13  end;
    1.14  
    1.15 @@ -827,6 +832,59 @@
    1.16      ProofContext.theory_of (LocalTheory.exit lthy)));
    1.17  
    1.18  
    1.19 +(* read off arities of inductive predicates from raw induction rule *)
    1.20 +fun arities_of induct =
    1.21 +  map (fn (_ $ t $ u) =>
    1.22 +      (fst (dest_Const (head_of t)), length (snd (strip_comb u))))
    1.23 +    (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.24 +
    1.25 +(* read off parameters of inductive predicate from raw induction rule *)
    1.26 +fun params_of induct =
    1.27 +  let
    1.28 +    val (_ $ t $ u :: _) =
    1.29 +      HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
    1.30 +    val (_, ts) = strip_comb t;
    1.31 +    val (_, us) = strip_comb u
    1.32 +  in
    1.33 +    List.take (ts, length ts - length us)
    1.34 +  end;
    1.35 +
    1.36 +val pname_of_intr =
    1.37 +  concl_of #> HOLogic.dest_Trueprop #> head_of #> dest_Const #> fst;
    1.38 +
    1.39 +(* partition introduction rules according to predicate name *)
    1.40 +fun partition_rules induct intros =
    1.41 +  fold_rev (fn r => AList.map_entry op = (pname_of_intr r) (cons r)) intros
    1.42 +    (map (rpair [] o fst) (arities_of induct));
    1.43 +
    1.44 +fun unpartition_rules intros xs =
    1.45 +  fold_map (fn r => AList.map_entry_yield op = (pname_of_intr r)
    1.46 +    (fn x :: xs => (x, xs)) #>> the) intros xs |> fst;
    1.47 +
    1.48 +(* infer order of variables in intro rules from order of quantifiers in elim rule *)
    1.49 +fun infer_intro_vars elim arity intros =
    1.50 +  let
    1.51 +    val thy = theory_of_thm elim;
    1.52 +    val _ :: cases = prems_of elim;
    1.53 +    val used = map (fst o fst) (Term.add_vars (prop_of elim) []);
    1.54 +    fun mtch (t, u) =
    1.55 +      let
    1.56 +        val params = Logic.strip_params t;
    1.57 +        val vars = map (Var o apfst (rpair 0))
    1.58 +          (Name.variant_list used (map fst params) ~~ map snd params);
    1.59 +        val ts = map (curry subst_bounds (rev vars))
    1.60 +          (List.drop (Logic.strip_assums_hyp t, arity));
    1.61 +        val us = Logic.strip_imp_prems u;
    1.62 +        val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
    1.63 +          (Vartab.empty, Vartab.empty);
    1.64 +      in
    1.65 +        map (Envir.subst_vars tab) vars
    1.66 +      end
    1.67 +  in
    1.68 +    map (mtch o apsnd prop_of) (cases ~~ intros)
    1.69 +  end;
    1.70 +
    1.71 +
    1.72  (** package setup **)
    1.73  
    1.74  (* setup theory *)