src/HOL/Tools/split_rule.ML
author bulwahn
Fri, 03 Dec 2010 08:40:47 +0100
changeset 40905 647142607448
parent 40388 cb9fd7dd641c
child 43333 2bdec7f430d3
permissions -rw-r--r--
only handle TimeOut exception if used interactively
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 22278
diff changeset
     1
(*  Title:      HOL/Tools/split_rule.ML
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
     2
    Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
     3
15661
9ef583b08647 reverted renaming of Some/None in comments and strings;
wenzelm
parents: 15574
diff changeset
     4
Some tools for managing tupled arguments and abstractions in rules.
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
     5
*)
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
     6
35365
2fcd08c62495 modernized structure Split_Rule;
wenzelm
parents: 35021
diff changeset
     7
signature SPLIT_RULE =
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
     8
sig
35365
2fcd08c62495 modernized structure Split_Rule;
wenzelm
parents: 35021
diff changeset
     9
  val split_rule_var: term -> thm -> thm
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    10
  val split_rule: thm -> thm
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    11
  val complete_split_rule: thm -> thm
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18629
diff changeset
    12
  val setup: theory -> theory
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    13
end;
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    14
35365
2fcd08c62495 modernized structure Split_Rule;
wenzelm
parents: 35021
diff changeset
    15
structure Split_Rule: SPLIT_RULE =
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    16
struct
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    17
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    18
(** split rules **)
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    19
35365
2fcd08c62495 modernized structure Split_Rule;
wenzelm
parents: 35021
diff changeset
    20
fun internal_split_const (Ta, Tb, Tc) =
2fcd08c62495 modernized structure Split_Rule;
wenzelm
parents: 35021
diff changeset
    21
  Const (@{const_name Product_Type.internal_split},
2fcd08c62495 modernized structure Split_Rule;
wenzelm
parents: 35021
diff changeset
    22
    [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
2fcd08c62495 modernized structure Split_Rule;
wenzelm
parents: 35021
diff changeset
    23
2fcd08c62495 modernized structure Split_Rule;
wenzelm
parents: 35021
diff changeset
    24
val eval_internal_split =
2fcd08c62495 modernized structure Split_Rule;
wenzelm
parents: 35021
diff changeset
    25
  hol_simplify [@{thm internal_split_def}] o hol_simplify [@{thm internal_split_conv}];
2fcd08c62495 modernized structure Split_Rule;
wenzelm
parents: 35021
diff changeset
    26
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    27
val remove_internal_split = eval_internal_split o split_all;
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    28
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    29
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    30
(*In ap_split S T u, term u expects separate arguments for the factors of S,
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    31
  with result type T.  The call creates a new term expecting one argument
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    32
  of type S.*)
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37167
diff changeset
    33
fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u =
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    34
      internal_split_const (T1, T2, T3) $
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    35
      Abs ("v", T1,
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    36
          ap_split T2 T3
32287
65d5c5b30747 cleaned up abstract tuple operations and named them consistently
haftmann
parents: 30722
diff changeset
    37
             ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    38
              Bound 0))
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    39
  | ap_split T T3 u = u;
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    40
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    41
(*Curries any Var of function type in the rule*)
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    42
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
32287
65d5c5b30747 cleaned up abstract tuple operations and named them consistently
haftmann
parents: 30722
diff changeset
    43
      let val T' = HOLogic.flatten_tupleT T1 ---> T2;
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    44
          val newt = ap_split T1 T2 (Var (v, T'));
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    45
          val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    46
      in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    47
  | split_rule_var' t rl = rl;
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    48
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    49
40388
cb9fd7dd641c abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
krauss
parents: 37678
diff changeset
    50
(* complete splitting of partially split rules *)
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    51
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    52
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
32288
168f31155c5e cleaned up abstract tuple operations and named them consistently
haftmann
parents: 32287
diff changeset
    53
      (ap_split T (maps HOLogic.flatten_tupleT Ts ---> U)
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    54
        (incr_boundvars 1 u) $ Bound 0))
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    55
  | ap_split' _ _ u = u;
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    56
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    57
fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    58
      let
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    59
        val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    60
        val (Us', U') = strip_type T;
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
    61
        val Us = take (length ts) Us';
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
    62
        val U = drop (length ts) Us' ---> U';
32288
168f31155c5e cleaned up abstract tuple operations and named them consistently
haftmann
parents: 32287
diff changeset
    63
        val T' = maps HOLogic.flatten_tupleT Us ---> U;
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    64
        fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    65
              let
32287
65d5c5b30747 cleaned up abstract tuple operations and named them consistently
haftmann
parents: 30722
diff changeset
    66
                val Ts = HOLogic.flatten_tupleT T;
20071
8f3e1ddb50e6 replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents: 19735
diff changeset
    67
                val ys = Name.variant_list xs (replicate (length Ts) a);
32342
3fabf5b5fc83 path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
haftmann
parents: 32288
diff changeset
    68
              in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    69
                (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    70
              end
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    71
          | mk_tuple _ x = x;
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    72
        val newt = ap_split' Us U (Var (v, T'));
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    73
        val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    74
        val (vs', insts) = fold mk_tuple ts (vs, []);
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    75
      in
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    76
        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    77
      end
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    78
  | complete_split_rule_var _ x = x;
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    79
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    80
fun collect_vars (Abs (_, _, t)) = collect_vars t
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    81
  | collect_vars t =
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    82
      (case strip_comb t of
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    83
        (v as Var _, ts) => cons (v, ts)
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    84
      | (t, ts) => fold collect_vars ts);
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    85
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    86
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 33957
diff changeset
    87
val split_rule_var = (Drule.export_without_context o remove_internal_split) oo split_rule_var';
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    88
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    89
(*curries ALL function variables occurring in a rule's conclusion*)
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    90
fun split_rule rl =
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 27882
diff changeset
    91
  fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    92
  |> remove_internal_split
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 33957
diff changeset
    93
  |> Drule.export_without_context;
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    94
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    95
(*curries ALL function variables*)
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    96
fun complete_split_rule rl =
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    97
  let
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    98
    val prop = Thm.prop_of rl;
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    99
    val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   100
    val vars = collect_vars prop [];
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   101
  in
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   102
    fst (fold_rev complete_split_rule_var vars (rl, xs))
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   103
    |> remove_internal_split
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 33957
diff changeset
   104
    |> Drule.export_without_context
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 32342
diff changeset
   105
    |> Rule_Cases.save rl
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   106
  end;
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   107
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   108
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   109
(* attribute syntax *)
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   110
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   111
val setup =
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30528
diff changeset
   112
  Attrib.setup @{binding split_format}
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30528
diff changeset
   113
    (Scan.lift
40388
cb9fd7dd641c abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
krauss
parents: 37678
diff changeset
   114
     (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule))))
30528
7173bf123335 simplified attribute setup;
wenzelm
parents: 29265
diff changeset
   115
    "split pair-typed subterms in premises, or function arguments" #>
7173bf123335 simplified attribute setup;
wenzelm
parents: 29265
diff changeset
   116
  Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
7173bf123335 simplified attribute setup;
wenzelm
parents: 29265
diff changeset
   117
    "curries ALL function variables occurring in a rule's conclusion";
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
   118
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
   119
end;
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
   120