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