src/HOL/Tools/split_rule.ML
author wenzelm
Thu Aug 03 17:30:36 2006 +0200 (2006-08-03)
changeset 20328 5b240a4216b0
parent 20071 8f3e1ddb50e6
child 22278 70a7cd02fec1
permissions -rw-r--r--
RuleInsts.bires_inst_tac;
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
wenzelm@15661
     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@19735
    17
  val split_rule_var: term -> thm -> thm
wenzelm@11037
    18
  val split_rule_goal: string list list -> thm -> thm
wenzelm@18708
    19
  val setup: theory -> theory
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@19735
    26
wenzelm@11037
    27
(** theory context references **)
wenzelm@11037
    28
wenzelm@11838
    29
val split_conv = thm "split_conv";
wenzelm@11838
    30
val fst_conv = thm "fst_conv";
wenzelm@11838
    31
val snd_conv = thm "snd_conv";
wenzelm@11838
    32
wenzelm@11037
    33
fun internal_split_const (Ta, Tb, Tc) =
wenzelm@11037
    34
  Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
wenzelm@11037
    35
wenzelm@11037
    36
val internal_split_def = thm "internal_split_def";
wenzelm@11037
    37
val internal_split_conv = thm "internal_split_conv";
wenzelm@11037
    38
wenzelm@11037
    39
wenzelm@11037
    40
wenzelm@11037
    41
(** split rules **)
wenzelm@11037
    42
wenzelm@11037
    43
val eval_internal_split = hol_simplify [internal_split_def] o hol_simplify [internal_split_conv];
wenzelm@11037
    44
val remove_internal_split = eval_internal_split o split_all;
wenzelm@11037
    45
oheimb@11025
    46
oheimb@11025
    47
(*In ap_split S T u, term u expects separate arguments for the factors of S,
oheimb@11025
    48
  with result type T.  The call creates a new term expecting one argument
oheimb@11025
    49
  of type S.*)
oheimb@11025
    50
fun ap_split (Type ("*", [T1, T2])) T3 u =
wenzelm@11037
    51
      internal_split_const (T1, T2, T3) $
wenzelm@11037
    52
      Abs ("v", T1,
oheimb@11025
    53
          ap_split T2 T3
oheimb@11025
    54
             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
oheimb@11025
    55
              Bound 0))
oheimb@11025
    56
  | ap_split T T3 u = u;
oheimb@11025
    57
oheimb@11025
    58
(*Curries any Var of function type in the rule*)
wenzelm@19735
    59
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
wenzelm@11037
    60
      let val T' = HOLogic.prodT_factors T1 ---> T2;
wenzelm@11037
    61
          val newt = ap_split T1 T2 (Var (v, T'));
wenzelm@19735
    62
          val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
wenzelm@11037
    63
      in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
wenzelm@19735
    64
  | split_rule_var' t rl = rl;
oheimb@11025
    65
wenzelm@11037
    66
wenzelm@11037
    67
(* complete splitting of partially splitted rules *)
oheimb@11025
    68
oheimb@11025
    69
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
skalberg@15570
    70
      (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U)
oheimb@11025
    71
        (incr_boundvars 1 u) $ Bound 0))
oheimb@11025
    72
  | ap_split' _ _ u = u;
oheimb@11025
    73
wenzelm@19735
    74
fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
oheimb@11025
    75
      let
wenzelm@19735
    76
        val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
oheimb@11025
    77
        val (Us', U') = strip_type T;
skalberg@15570
    78
        val Us = Library.take (length ts, Us');
skalberg@15570
    79
        val U = Library.drop (length ts, Us') ---> U';
skalberg@15570
    80
        val T' = List.concat (map HOLogic.prodT_factors Us) ---> U;
wenzelm@19735
    81
        fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
oheimb@11025
    82
              let
oheimb@11025
    83
                val Ts = HOLogic.prodT_factors T;
wenzelm@20071
    84
                val ys = Name.variant_list xs (replicate (length Ts) a);
oheimb@11025
    85
              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
oheimb@11025
    86
                (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
oheimb@11025
    87
              end
wenzelm@19735
    88
          | mk_tuple _ x = x;
oheimb@11025
    89
        val newt = ap_split' Us U (Var (v, T'));
wenzelm@19735
    90
        val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
wenzelm@19735
    91
        val (vs', insts) = fold mk_tuple ts (vs, []);
oheimb@11025
    92
      in
oheimb@11025
    93
        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
oheimb@11025
    94
      end
wenzelm@19735
    95
  | complete_split_rule_var _ x = x;
oheimb@11025
    96
wenzelm@19735
    97
fun collect_vars (Abs (_, _, t)) = collect_vars t
wenzelm@19735
    98
  | collect_vars t =
wenzelm@19735
    99
      (case strip_comb t of
wenzelm@19735
   100
        (v as Var _, ts) => cons (v, ts)
wenzelm@19735
   101
      | (t, ts) => fold collect_vars ts);
oheimb@11025
   102
wenzelm@11037
   103
wenzelm@19735
   104
val split_rule_var = (Drule.standard o remove_internal_split) oo split_rule_var';
oheimb@11025
   105
wenzelm@11037
   106
(*curries ALL function variables occurring in a rule's conclusion*)
wenzelm@11037
   107
fun split_rule rl =
wenzelm@19735
   108
  fold_rev split_rule_var' (Term.term_vars (concl_of rl)) rl
wenzelm@11037
   109
  |> remove_internal_split
wenzelm@11037
   110
  |> Drule.standard;
oheimb@11025
   111
wenzelm@19735
   112
(*curries ALL function variables*)
oheimb@11025
   113
fun complete_split_rule rl =
wenzelm@19735
   114
  let
wenzelm@19735
   115
    val prop = Thm.prop_of rl;
wenzelm@19735
   116
    val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
wenzelm@19735
   117
    val vars = collect_vars prop [];
wenzelm@19735
   118
  in
wenzelm@19735
   119
    fst (fold_rev complete_split_rule_var vars (rl, xs))
wenzelm@19735
   120
    |> remove_internal_split
wenzelm@19735
   121
    |> Drule.standard
wenzelm@19735
   122
    |> RuleCases.save rl
wenzelm@19735
   123
  end;
wenzelm@11037
   124
wenzelm@11037
   125
wenzelm@11037
   126
val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
wenzelm@11037
   127
wenzelm@11037
   128
fun split_rule_goal xss rl =
wenzelm@11037
   129
  let
haftmann@18050
   130
    fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
wenzelm@19735
   131
    fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
wenzelm@11037
   132
  in
haftmann@18050
   133
    rl
wenzelm@19735
   134
    |> fold_index one_goal xss
haftmann@18050
   135
    |> Simplifier.full_simplify split_rule_ss
wenzelm@19735
   136
    |> Drule.standard
wenzelm@11037
   137
    |> RuleCases.save rl
wenzelm@11037
   138
  end;
wenzelm@11037
   139
wenzelm@11037
   140
(* attribute syntax *)
wenzelm@11037
   141
wenzelm@15661
   142
(* FIXME dynamically scoped due to Args.name/pair_tac *)
wenzelm@15661
   143
wenzelm@11040
   144
fun split_format x = Attrib.syntax
wenzelm@11045
   145
  (Scan.lift (Args.parens (Args.$$$ "complete"))
wenzelm@18728
   146
    >> K (Thm.rule_attribute (K complete_split_rule)) ||
wenzelm@11045
   147
  Args.and_list1 (Scan.lift (Scan.repeat Args.name))
wenzelm@18728
   148
    >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss)))) x;
wenzelm@11037
   149
wenzelm@11037
   150
val setup =
wenzelm@18708
   151
  Attrib.add_attributes
wenzelm@18728
   152
    [("split_format", split_format,
wenzelm@18708
   153
      "split pair-typed subterms in premises, or function arguments")];
oheimb@11025
   154
oheimb@11025
   155
end;
oheimb@11025
   156
wenzelm@11037
   157
structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule;
wenzelm@11037
   158
open BasicSplitRule;