src/HOL/Tools/split_rule.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 29265 5b4247055bd7
child 30528 7173bf123335
permissions -rw-r--r--
use long names for old-style fold combinators;
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
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
     7
signature BASIC_SPLIT_RULE =
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
     8
sig
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
     9
  val split_rule: thm -> thm
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    10
  val complete_split_rule: thm -> thm
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    11
end;
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    12
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    13
signature SPLIT_RULE =
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    14
sig
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    15
  include BASIC_SPLIT_RULE
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    16
  val split_rule_var: term -> thm -> thm
27208
5fe899199f85 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 26352
diff changeset
    17
  val split_rule_goal: Proof.context -> string list list -> thm -> thm
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18629
diff changeset
    18
  val setup: theory -> theory
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    19
end;
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    20
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    21
structure SplitRule: SPLIT_RULE =
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    22
struct
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    23
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    24
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    25
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    26
(** theory context references **)
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    27
11838
02d75712061d got rid of ML proof scripts for Product_Type;
wenzelm
parents: 11045
diff changeset
    28
val split_conv = thm "split_conv";
02d75712061d got rid of ML proof scripts for Product_Type;
wenzelm
parents: 11045
diff changeset
    29
val fst_conv = thm "fst_conv";
02d75712061d got rid of ML proof scripts for Product_Type;
wenzelm
parents: 11045
diff changeset
    30
val snd_conv = thm "snd_conv";
02d75712061d got rid of ML proof scripts for Product_Type;
wenzelm
parents: 11045
diff changeset
    31
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    32
fun internal_split_const (Ta, Tb, Tc) =
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    33
  Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    34
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    35
val internal_split_def = thm "internal_split_def";
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    36
val internal_split_conv = thm "internal_split_conv";
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    37
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    38
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    39
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    40
(** split rules **)
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    41
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    42
val eval_internal_split = hol_simplify [internal_split_def] o hol_simplify [internal_split_conv];
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    43
val remove_internal_split = eval_internal_split o split_all;
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    44
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    45
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    46
(*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
    47
  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
    48
  of type S.*)
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    49
fun ap_split (Type ("*", [T1, T2])) T3 u =
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    50
      internal_split_const (T1, T2, T3) $
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    51
      Abs ("v", T1,
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    52
          ap_split T2 T3
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    53
             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    54
              Bound 0))
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    55
  | ap_split T T3 u = u;
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    56
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    57
(*Curries any Var of function type in the rule*)
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    58
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    59
      let val T' = HOLogic.prodT_factors T1 ---> T2;
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    60
          val newt = ap_split T1 T2 (Var (v, T'));
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    61
          val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    62
      in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    63
  | split_rule_var' t rl = rl;
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    64
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    65
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
    66
(* complete splitting of partially splitted rules *)
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    67
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    68
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    69
      (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U)
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    70
        (incr_boundvars 1 u) $ Bound 0))
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    71
  | ap_split' _ _ u = u;
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    72
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    73
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
    74
      let
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    75
        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
    76
        val (Us', U') = strip_type T;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    77
        val Us = Library.take (length ts, Us');
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    78
        val U = Library.drop (length ts, Us') ---> U';
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    79
        val T' = List.concat (map HOLogic.prodT_factors Us) ---> U;
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    80
        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
    81
              let
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    82
                val Ts = HOLogic.prodT_factors T;
20071
8f3e1ddb50e6 replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents: 19735
diff changeset
    83
                val ys = Name.variant_list xs (replicate (length Ts) a);
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    84
              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    85
                (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
    86
              end
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    87
          | mk_tuple _ x = x;
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    88
        val newt = ap_split' Us U (Var (v, T'));
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    89
        val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    90
        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
    91
      in
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    92
        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    93
      end
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    94
  | complete_split_rule_var _ x = x;
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
    95
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    96
fun collect_vars (Abs (_, _, t)) = collect_vars t
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    97
  | collect_vars t =
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    98
      (case strip_comb t of
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
    99
        (v as Var _, ts) => cons (v, ts)
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   100
      | (t, ts) => fold collect_vars ts);
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
   101
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   102
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   103
val split_rule_var = (Drule.standard 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
   104
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   105
(*curries ALL function variables occurring in a rule's conclusion*)
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   106
fun split_rule rl =
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 27882
diff changeset
   107
  fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   108
  |> remove_internal_split
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   109
  |> Drule.standard;
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
   110
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   111
(*curries ALL function variables*)
11025
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
   112
fun complete_split_rule rl =
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   113
  let
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   114
    val prop = Thm.prop_of rl;
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   115
    val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   116
    val vars = collect_vars prop [];
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   117
  in
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   118
    fst (fold_rev complete_split_rule_var vars (rl, xs))
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   119
    |> remove_internal_split
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   120
    |> Drule.standard
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   121
    |> RuleCases.save rl
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   122
  end;
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   123
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   124
27208
5fe899199f85 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 26352
diff changeset
   125
fun pair_tac ctxt s =
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27208
diff changeset
   126
  res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
27208
5fe899199f85 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 26352
diff changeset
   127
  THEN' hyp_subst_tac
5fe899199f85 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 26352
diff changeset
   128
  THEN' K prune_params_tac;
26352
haftmann
parents: 25979
diff changeset
   129
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   130
val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   131
27208
5fe899199f85 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 26352
diff changeset
   132
fun split_rule_goal ctxt xss rl =
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   133
  let
27208
5fe899199f85 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 26352
diff changeset
   134
    fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   135
    fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   136
  in
18050
652c95961a8b fold_index replacing foldln
haftmann
parents: 15661
diff changeset
   137
    rl
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   138
    |> fold_index one_goal xss
18050
652c95961a8b fold_index replacing foldln
haftmann
parents: 15661
diff changeset
   139
    |> Simplifier.full_simplify split_rule_ss
19735
ff13585fbdab complete_split_rule: all Vars;
wenzelm
parents: 18728
diff changeset
   140
    |> Drule.standard
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   141
    |> RuleCases.save rl
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   142
  end;
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   143
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   144
(* attribute syntax *)
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   145
27882
eaa9fef9f4c1 Args.name_source(_position) for proper position information;
wenzelm
parents: 27809
diff changeset
   146
(* FIXME dynamically scoped due to Args.name_source/pair_tac *)
15661
9ef583b08647 reverted renaming of Some/None in comments and strings;
wenzelm
parents: 15574
diff changeset
   147
27809
a1e409db516b unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27239
diff changeset
   148
val split_format = Attrib.syntax (Scan.lift
a1e409db516b unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27239
diff changeset
   149
 (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
27882
eaa9fef9f4c1 Args.name_source(_position) for proper position information;
wenzelm
parents: 27809
diff changeset
   150
  OuterParse.and_list1 (Scan.repeat Args.name_source)
27208
5fe899199f85 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 26352
diff changeset
   151
    >> (fn xss => Thm.rule_attribute (fn context =>
27809
a1e409db516b unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27239
diff changeset
   152
        split_rule_goal (Context.proof_of context) xss))));
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   153
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   154
val setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18629
diff changeset
   155
  Attrib.add_attributes
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   156
    [("split_format", split_format,
22278
70a7cd02fec1 Added split_rule attribute.
berghofe
parents: 20071
diff changeset
   157
      "split pair-typed subterms in premises, or function arguments"),
70a7cd02fec1 Added split_rule attribute.
berghofe
parents: 20071
diff changeset
   158
     ("split_rule", Attrib.no_args (Thm.rule_attribute (K split_rule)),
70a7cd02fec1 Added split_rule attribute.
berghofe
parents: 20071
diff changeset
   159
      "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
   160
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
   161
end;
a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff changeset
   162
11037
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   163
structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule;
37716a82a3d9 module setup;
wenzelm
parents: 11025
diff changeset
   164
open BasicSplitRule;