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