src/HOL/Tools/split_rule.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 61853 fb7756087101
child 67149 e61557884799
permissions -rw-r--r--
tuned;
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@51717
     9
  val split_rule_var: Proof.context -> term -> thm -> thm
wenzelm@51717
    10
  val split_rule: Proof.context -> thm -> thm
wenzelm@51717
    11
  val complete_split_rule: Proof.context -> thm -> thm
wenzelm@11037
    12
end;
wenzelm@11037
    13
wenzelm@35365
    14
structure Split_Rule: SPLIT_RULE =
wenzelm@11037
    15
struct
wenzelm@11037
    16
wenzelm@11037
    17
(** split rules **)
wenzelm@11037
    18
haftmann@61424
    19
fun internal_case_prod_const (Ta, Tb, Tc) =
haftmann@61424
    20
  Const (@{const_name Product_Type.internal_case_prod},
wenzelm@35365
    21
    [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
wenzelm@35365
    22
wenzelm@51717
    23
fun eval_internal_split ctxt =
haftmann@61424
    24
  hol_simplify ctxt @{thms internal_case_prod_def} o
haftmann@61424
    25
  hol_simplify ctxt @{thms internal_case_prod_conv};
wenzelm@35365
    26
wenzelm@51717
    27
fun remove_internal_split ctxt = eval_internal_split ctxt o split_all ctxt;
wenzelm@11037
    28
oheimb@11025
    29
oheimb@11025
    30
(*In ap_split S T u, term u expects separate arguments for the factors of S,
oheimb@11025
    31
  with result type T.  The call creates a new term expecting one argument
oheimb@11025
    32
  of type S.*)
haftmann@37678
    33
fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u =
haftmann@61424
    34
      internal_case_prod_const (T1, T2, T3) $
wenzelm@11037
    35
      Abs ("v", T1,
oheimb@11025
    36
          ap_split T2 T3
haftmann@32287
    37
             ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $
oheimb@11025
    38
              Bound 0))
haftmann@58468
    39
  | ap_split _ T3 u = u;
oheimb@11025
    40
oheimb@11025
    41
(*Curries any Var of function type in the rule*)
wenzelm@60362
    42
fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl =
haftmann@32287
    43
      let val T' = HOLogic.flatten_tupleT T1 ---> T2;
wenzelm@11037
    44
          val newt = ap_split T1 T2 (Var (v, T'));
wenzelm@60642
    45
      in Thm.instantiate ([], [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end
wenzelm@60362
    46
  | split_rule_var' _ _ rl = rl;
oheimb@11025
    47
wenzelm@11037
    48
krauss@40388
    49
(* complete splitting of partially split rules *)
oheimb@11025
    50
oheimb@11025
    51
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
haftmann@32288
    52
      (ap_split T (maps HOLogic.flatten_tupleT Ts ---> U)
oheimb@11025
    53
        (incr_boundvars 1 u) $ Bound 0))
oheimb@11025
    54
  | ap_split' _ _ u = u;
oheimb@11025
    55
wenzelm@60363
    56
fun complete_split_rule_var ctxt (t as Var (v, T), ts) (rl, vs) =
oheimb@11025
    57
      let
oheimb@11025
    58
        val (Us', U') = strip_type T;
haftmann@33957
    59
        val Us = take (length ts) Us';
haftmann@33957
    60
        val U = drop (length ts) Us' ---> U';
haftmann@32288
    61
        val T' = maps HOLogic.flatten_tupleT Us ---> U;
wenzelm@19735
    62
        fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
oheimb@11025
    63
              let
haftmann@32287
    64
                val Ts = HOLogic.flatten_tupleT T;
wenzelm@20071
    65
                val ys = Name.variant_list xs (replicate (length Ts) a);
wenzelm@60363
    66
              in
wenzelm@60363
    67
                (xs @ ys,
wenzelm@60642
    68
                  (dest_Var v,
wenzelm@60642
    69
                    Thm.cterm_of ctxt (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
wenzelm@60642
    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 (vs', insts) = fold mk_tuple ts (vs, []);
oheimb@11025
    75
      in
wenzelm@60642
    76
        (Drule.instantiate_normalize ([], ((v, T), Thm.cterm_of ctxt newt) :: insts) rl, vs')
oheimb@11025
    77
      end
wenzelm@60363
    78
  | complete_split_rule_var _ _ x = x;
oheimb@11025
    79
wenzelm@19735
    80
fun collect_vars (Abs (_, _, t)) = collect_vars t
wenzelm@19735
    81
  | collect_vars t =
wenzelm@19735
    82
      (case strip_comb t of
wenzelm@19735
    83
        (v as Var _, ts) => cons (v, ts)
haftmann@58468
    84
      | (_, ts) => fold collect_vars ts);
oheimb@11025
    85
wenzelm@11037
    86
wenzelm@51717
    87
fun split_rule_var ctxt =
wenzelm@60362
    88
  (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var' ctxt;
oheimb@11025
    89
wenzelm@11037
    90
(*curries ALL function variables occurring in a rule's conclusion*)
wenzelm@51717
    91
fun split_rule ctxt rl =
wenzelm@60362
    92
  fold_rev (split_rule_var' ctxt) (Misc_Legacy.term_vars (Thm.concl_of rl)) rl
wenzelm@51717
    93
  |> remove_internal_split ctxt
wenzelm@35021
    94
  |> Drule.export_without_context;
oheimb@11025
    95
wenzelm@19735
    96
(*curries ALL function variables*)
wenzelm@51717
    97
fun complete_split_rule ctxt 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@60363
   103
    fst (fold_rev (complete_split_rule_var ctxt) vars (rl, xs))
wenzelm@51717
   104
    |> remove_internal_split ctxt
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@11037
   110
(* attribute syntax *)
wenzelm@11037
   111
wenzelm@58820
   112
val _ =
wenzelm@58820
   113
  Theory.setup
wenzelm@58820
   114
   (Attrib.setup @{binding split_format}
wenzelm@58820
   115
      (Scan.lift (Args.parens (Args.$$$ "complete")
wenzelm@61853
   116
        >> K (Thm.rule_attribute [] (complete_split_rule o Context.proof_of))))
wenzelm@58820
   117
      "split pair-typed subterms in premises, or function arguments" #>
wenzelm@58820
   118
    Attrib.setup @{binding split_rule}
wenzelm@61853
   119
      (Scan.succeed (Thm.rule_attribute [] (split_rule o Context.proof_of)))
wenzelm@58820
   120
      "curries ALL function variables occurring in a rule's conclusion");
oheimb@11025
   121
oheimb@11025
   122
end;
oheimb@11025
   123