src/HOL/Tools/split_rule.ML
author boehmes
Sat Mar 27 02:10:00 2010 +0100 (2010-03-27)
changeset 35983 27e2fa7d4ce7
parent 35365 2fcd08c62495
child 36546 a9873318fe30
permissions -rw-r--r--
slightly more general simproc (avoids errors of linarith)
     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 SPLIT_RULE =
     8 sig
     9   val split_rule_var: term -> thm -> thm
    10   val split_rule_goal: Proof.context -> string list list -> thm -> thm
    11   val split_rule: thm -> thm
    12   val complete_split_rule: thm -> thm
    13   val setup: theory -> theory
    14 end;
    15 
    16 structure Split_Rule: SPLIT_RULE =
    17 struct
    18 
    19 (** split rules **)
    20 
    21 fun internal_split_const (Ta, Tb, Tc) =
    22   Const (@{const_name Product_Type.internal_split},
    23     [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
    24 
    25 val eval_internal_split =
    26   hol_simplify [@{thm internal_split_def}] o hol_simplify [@{thm internal_split_conv}];
    27 
    28 val remove_internal_split = eval_internal_split o split_all;
    29 
    30 
    31 (*In ap_split S T u, term u expects separate arguments for the factors of S,
    32   with result type T.  The call creates a new term expecting one argument
    33   of type S.*)
    34 fun ap_split (Type (@{type_name "*"}, [T1, T2])) T3 u =
    35       internal_split_const (T1, T2, T3) $
    36       Abs ("v", T1,
    37           ap_split T2 T3
    38              ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $
    39               Bound 0))
    40   | ap_split T T3 u = u;
    41 
    42 (*Curries any Var of function type in the rule*)
    43 fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
    44       let val T' = HOLogic.flatten_tupleT T1 ---> T2;
    45           val newt = ap_split T1 T2 (Var (v, T'));
    46           val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
    47       in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
    48   | split_rule_var' t rl = rl;
    49 
    50 
    51 (* complete splitting of partially splitted rules *)
    52 
    53 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
    54       (ap_split T (maps HOLogic.flatten_tupleT Ts ---> U)
    55         (incr_boundvars 1 u) $ Bound 0))
    56   | ap_split' _ _ u = u;
    57 
    58 fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
    59       let
    60         val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
    61         val (Us', U') = strip_type T;
    62         val Us = take (length ts) Us';
    63         val U = drop (length ts) Us' ---> U';
    64         val T' = maps HOLogic.flatten_tupleT Us ---> U;
    65         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
    66               let
    67                 val Ts = HOLogic.flatten_tupleT T;
    68                 val ys = Name.variant_list xs (replicate (length Ts) a);
    69               in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
    70                 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
    71               end
    72           | mk_tuple _ x = x;
    73         val newt = ap_split' Us U (Var (v, T'));
    74         val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
    75         val (vs', insts) = fold mk_tuple ts (vs, []);
    76       in
    77         (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
    78       end
    79   | complete_split_rule_var _ x = x;
    80 
    81 fun collect_vars (Abs (_, _, t)) = collect_vars t
    82   | collect_vars t =
    83       (case strip_comb t of
    84         (v as Var _, ts) => cons (v, ts)
    85       | (t, ts) => fold collect_vars ts);
    86 
    87 
    88 val split_rule_var = (Drule.export_without_context o remove_internal_split) oo split_rule_var';
    89 
    90 (*curries ALL function variables occurring in a rule's conclusion*)
    91 fun split_rule rl =
    92   fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
    93   |> remove_internal_split
    94   |> Drule.export_without_context;
    95 
    96 (*curries ALL function variables*)
    97 fun complete_split_rule rl =
    98   let
    99     val prop = Thm.prop_of rl;
   100     val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
   101     val vars = collect_vars prop [];
   102   in
   103     fst (fold_rev complete_split_rule_var vars (rl, xs))
   104     |> remove_internal_split
   105     |> Drule.export_without_context
   106     |> Rule_Cases.save rl
   107   end;
   108 
   109 
   110 fun pair_tac ctxt s =
   111   res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
   112   THEN' hyp_subst_tac
   113   THEN' K prune_params_tac;
   114 
   115 val split_rule_ss = HOL_basic_ss addsimps [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}];
   116 
   117 fun split_rule_goal ctxt xss rl =
   118   let
   119     fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
   120     fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
   121   in
   122     rl
   123     |> fold_index one_goal xss
   124     |> Simplifier.full_simplify split_rule_ss
   125     |> Drule.export_without_context
   126     |> Rule_Cases.save rl
   127   end;
   128 
   129 
   130 (* attribute syntax *)
   131 
   132 (* FIXME dynamically scoped due to Args.name_source/pair_tac *)
   133 
   134 val setup =
   135   Attrib.setup @{binding split_format}
   136     (Scan.lift
   137      (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
   138       OuterParse.and_list1 (Scan.repeat Args.name_source)
   139         >> (fn xss => Thm.rule_attribute (fn context =>
   140             split_rule_goal (Context.proof_of context) xss))))
   141     "split pair-typed subterms in premises, or function arguments" #>
   142   Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
   143     "curries ALL function variables occurring in a rule's conclusion";
   144 
   145 end;
   146