New function complete_split_rule for complete splitting of partially
authorberghofe
Mon Jan 29 13:28:15 2001 +0100 (2001-01-29)
changeset 1098987f8a7644f91
parent 10988 e0016a009c17
child 10990 e7ffc23a05f6
New function complete_split_rule for complete splitting of partially
splitted rules (as generated by inductive definition package).
src/HOL/Product_Type.ML
     1.1 --- a/src/HOL/Product_Type.ML	Mon Jan 29 13:26:04 2001 +0100
     1.2 +++ b/src/HOL/Product_Type.ML	Mon Jan 29 13:28:15 2001 +0100
     1.3 @@ -595,6 +595,41 @@
     1.4        end
     1.5    | split_rule_var' (t, rl) = rl;
     1.6  
     1.7 +(*** Complete splitting of partially splitted rules ***)
     1.8 +
     1.9 +fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
    1.10 +      (ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U)
    1.11 +        (incr_boundvars 1 u) $ Bound 0))
    1.12 +  | ap_split' _ _ u = u;
    1.13 +
    1.14 +fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
    1.15 +      let
    1.16 +        val cterm = Thm.cterm_of (#sign (rep_thm rl))
    1.17 +        val (Us', U') = strip_type T;
    1.18 +        val Us = take (length ts, Us');
    1.19 +        val U = drop (length ts, Us') ---> U';
    1.20 +        val T' = flat (map HOLogic.prodT_factors Us) ---> U;
    1.21 +        fun mk_tuple (xs, v as Var ((a, _), T)) =
    1.22 +          let
    1.23 +            val Ts = HOLogic.prodT_factors T;
    1.24 +            val ys = variantlist (replicate (length Ts) a, xs);
    1.25 +          in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
    1.26 +            (map (Var o apfst (rpair 0)) (ys ~~ Ts)))))
    1.27 +          end;
    1.28 +        val newt = ap_split' Us U (Var (v, T'));
    1.29 +        val cterm = Thm.cterm_of (#sign (rep_thm rl));
    1.30 +        val (vs', insts) = foldl_map mk_tuple (vs, ts);
    1.31 +      in
    1.32 +        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
    1.33 +      end
    1.34 +  | complete_split_rule_var (_, x) = x;
    1.35 +
    1.36 +fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t)
    1.37 +  | collect_vars (vs, t) = (case strip_comb t of
    1.38 +        (v as Var _, ts) =>
    1.39 +          (case filter is_Var ts of [] => vs | ts' => (v, ts')::vs)
    1.40 +      | (t, ts) => foldl collect_vars (vs, ts));
    1.41 +
    1.42  in
    1.43  
    1.44  val split_rule_var = standard o remove_split o split_rule_var';
    1.45 @@ -602,4 +637,9 @@
    1.46  (*Curries ALL function variables occurring in a rule's conclusion*)
    1.47  fun split_rule rl = standard (remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)));
    1.48  
    1.49 +fun complete_split_rule rl =
    1.50 +  standard (remove_split (fst (foldr complete_split_rule_var
    1.51 +    (collect_vars ([], concl_of rl),
    1.52 +     (rl, map (fst o fst o dest_Var) (term_vars (#prop (rep_thm rl))))))));
    1.53 +
    1.54  end;