src/HOL/Tools/split_rule.ML
author haftmann
Fri Feb 10 09:09:07 2006 +0100 (2006-02-10)
changeset 19008 14c1b2f5dda4
parent 18728 6790126ab5f6
child 19735 ff13585fbdab
permissions -rw-r--r--
improved code generator devarification
     1 (*  Title:      Tools/split_rule.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
     4 
     5 Some tools for managing tupled arguments and abstractions in rules.
     6 *)
     7 
     8 signature BASIC_SPLIT_RULE =
     9 sig
    10   val split_rule: thm -> thm
    11   val complete_split_rule: thm -> thm
    12 end;
    13 
    14 signature SPLIT_RULE =
    15 sig
    16   include BASIC_SPLIT_RULE
    17   val split_rule_var: term * thm -> thm
    18   val split_rule_goal: string list list -> thm -> thm
    19   val setup: theory -> theory
    20 end;
    21 
    22 structure SplitRule: SPLIT_RULE =
    23 struct
    24 
    25 
    26 (** theory context references **)
    27 
    28 val split_conv = thm "split_conv";
    29 val fst_conv = thm "fst_conv";
    30 val snd_conv = thm "snd_conv";
    31 
    32 fun internal_split_const (Ta, Tb, Tc) =
    33   Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
    34 
    35 val internal_split_def = thm "internal_split_def";
    36 val internal_split_conv = thm "internal_split_conv";
    37 
    38 
    39 
    40 (** split rules **)
    41 
    42 val eval_internal_split = hol_simplify [internal_split_def] o hol_simplify [internal_split_conv];
    43 val remove_internal_split = eval_internal_split o split_all;
    44 
    45 
    46 (*In ap_split S T u, term u expects separate arguments for the factors of S,
    47   with result type T.  The call creates a new term expecting one argument
    48   of type S.*)
    49 fun ap_split (Type ("*", [T1, T2])) T3 u =
    50       internal_split_const (T1, T2, T3) $
    51       Abs ("v", T1,
    52           ap_split T2 T3
    53              ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
    54               Bound 0))
    55   | ap_split T T3 u = u;
    56 
    57 (*Curries any Var of function type in the rule*)
    58 fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
    59       let val T' = HOLogic.prodT_factors T1 ---> T2;
    60           val newt = ap_split T1 T2 (Var (v, T'));
    61           val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
    62       in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
    63   | split_rule_var' (t, rl) = rl;
    64 
    65 
    66 (* complete splitting of partially splitted rules *)
    67 
    68 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
    69       (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U)
    70         (incr_boundvars 1 u) $ Bound 0))
    71   | ap_split' _ _ u = u;
    72 
    73 fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
    74       let
    75         val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl))
    76         val (Us', U') = strip_type T;
    77         val Us = Library.take (length ts, Us');
    78         val U = Library.drop (length ts, Us') ---> U';
    79         val T' = List.concat (map HOLogic.prodT_factors Us) ---> U;
    80         fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
    81               let
    82                 val Ts = HOLogic.prodT_factors T;
    83                 val ys = Term.variantlist (replicate (length Ts) a, xs);
    84               in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
    85                 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
    86               end
    87           | mk_tuple (x, _) = x;
    88         val newt = ap_split' Us U (Var (v, T'));
    89         val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl));
    90         val (vs', insts) = Library.foldl mk_tuple ((vs, []), ts);
    91       in
    92         (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
    93       end
    94   | complete_split_rule_var (_, x) = x;
    95 
    96 fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t)
    97   | collect_vars (vs, t) = (case strip_comb t of
    98         (v as Var _, ts) => (v, ts)::vs
    99       | (t, ts) => Library.foldl collect_vars (vs, ts));
   100 
   101 
   102 val split_rule_var = Drule.standard o remove_internal_split o split_rule_var';
   103 
   104 (*curries ALL function variables occurring in a rule's conclusion*)
   105 fun split_rule rl =
   106   foldr split_rule_var' rl (Term.term_vars (concl_of rl))
   107   |> remove_internal_split
   108   |> Drule.standard;
   109 
   110 fun complete_split_rule rl =
   111   fst (foldr complete_split_rule_var
   112     (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl))))
   113     (collect_vars ([], concl_of rl)))
   114   |> remove_internal_split
   115   |> Drule.standard
   116   |> RuleCases.save rl;
   117 
   118 
   119 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
   120 
   121 fun split_rule_goal xss rl =
   122   let
   123     fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
   124     fun one_goal (i, xs) = fold (one_split (i+1)) xs;
   125   in
   126     rl
   127     |> Library.fold_index one_goal xss
   128     |> Simplifier.full_simplify split_rule_ss
   129     |> Drule.standard 
   130     |> RuleCases.save rl
   131   end;
   132 
   133 (* attribute syntax *)
   134 
   135 (* FIXME dynamically scoped due to Args.name/pair_tac *)
   136 
   137 fun split_format x = Attrib.syntax
   138   (Scan.lift (Args.parens (Args.$$$ "complete"))
   139     >> K (Thm.rule_attribute (K complete_split_rule)) ||
   140   Args.and_list1 (Scan.lift (Scan.repeat Args.name))
   141     >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss)))) x;
   142 
   143 val setup =
   144   Attrib.add_attributes
   145     [("split_format", split_format,
   146       "split pair-typed subterms in premises, or function arguments")];
   147 
   148 end;
   149 
   150 structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule;
   151 open BasicSplitRule;