src/HOL/Tools/split_rule.ML
author haftmann
Tue Nov 24 17:28:25 2009 +0100 (2009-11-24)
changeset 33955 fff6f11b1f09
parent 33368 b1cf34f1855c
child 33957 e9afca2118d4
permissions -rw-r--r--
curried take/drop
     1 (*  Title:      HOL/Tools/split_rule.ML
     2     Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
     3 
     4 Some tools for managing tupled arguments and abstractions in rules.
     5 *)
     6 
     7 signature BASIC_SPLIT_RULE =
     8 sig
     9   val split_rule: thm -> thm
    10   val complete_split_rule: thm -> thm
    11 end;
    12 
    13 signature SPLIT_RULE =
    14 sig
    15   include BASIC_SPLIT_RULE
    16   val split_rule_var: term -> thm -> thm
    17   val split_rule_goal: Proof.context -> string list list -> thm -> thm
    18   val setup: theory -> theory
    19 end;
    20 
    21 structure SplitRule: SPLIT_RULE =
    22 struct
    23 
    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.flatten_tupleT 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.flatten_tupleT T1 ---> T2;
    60           val newt = ap_split T1 T2 (Var (v, T'));
    61           val cterm = Thm.cterm_of (Thm.theory_of_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 (maps HOLogic.flatten_tupleT 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 (Thm.theory_of_thm rl)
    76         val (Us', U') = strip_type T;
    77         val Us = (uncurry take) (length ts, Us');
    78         val U = (uncurry drop) (length ts, Us') ---> U';
    79         val T' = maps HOLogic.flatten_tupleT Us ---> U;
    80         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
    81               let
    82                 val Ts = HOLogic.flatten_tupleT T;
    83                 val ys = Name.variant_list xs (replicate (length Ts) a);
    84               in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) 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 (Thm.theory_of_thm rl);
    90         val (vs', insts) = fold mk_tuple ts (vs, []);
    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 (Abs (_, _, t)) = collect_vars t
    97   | collect_vars t =
    98       (case strip_comb t of
    99         (v as Var _, ts) => cons (v, ts)
   100       | (t, ts) => fold collect_vars ts);
   101 
   102 
   103 val split_rule_var = (Drule.standard o remove_internal_split) oo split_rule_var';
   104 
   105 (*curries ALL function variables occurring in a rule's conclusion*)
   106 fun split_rule rl =
   107   fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
   108   |> remove_internal_split
   109   |> Drule.standard;
   110 
   111 (*curries ALL function variables*)
   112 fun complete_split_rule rl =
   113   let
   114     val prop = Thm.prop_of rl;
   115     val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
   116     val vars = collect_vars prop [];
   117   in
   118     fst (fold_rev complete_split_rule_var vars (rl, xs))
   119     |> remove_internal_split
   120     |> Drule.standard
   121     |> Rule_Cases.save rl
   122   end;
   123 
   124 
   125 fun pair_tac ctxt s =
   126   res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
   127   THEN' hyp_subst_tac
   128   THEN' K prune_params_tac;
   129 
   130 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
   131 
   132 fun split_rule_goal ctxt xss rl =
   133   let
   134     fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
   135     fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
   136   in
   137     rl
   138     |> fold_index one_goal xss
   139     |> Simplifier.full_simplify split_rule_ss
   140     |> Drule.standard
   141     |> Rule_Cases.save rl
   142   end;
   143 
   144 
   145 (* attribute syntax *)
   146 
   147 (* FIXME dynamically scoped due to Args.name_source/pair_tac *)
   148 
   149 val setup =
   150   Attrib.setup @{binding split_format}
   151     (Scan.lift
   152      (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
   153       OuterParse.and_list1 (Scan.repeat Args.name_source)
   154         >> (fn xss => Thm.rule_attribute (fn context =>
   155             split_rule_goal (Context.proof_of context) xss))))
   156     "split pair-typed subterms in premises, or function arguments" #>
   157   Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
   158     "curries ALL function variables occurring in a rule's conclusion";
   159 
   160 end;
   161 
   162 structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule;
   163 open BasicSplitRule;