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