src/HOL/Tools/split_rule.ML
author oheimb
Thu Feb 01 20:51:48 2001 +0100 (2001-02-01)
changeset 11025 a70b796d9af8
child 11037 37716a82a3d9
permissions -rw-r--r--
converted to Isar therory, adding attributes complete_split and split_format
oheimb@11025
     1
(*Attempts to remove occurrences of split, and pair-valued parameters*)
oheimb@11025
     2
val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all;
oheimb@11025
     3
oheimb@11025
     4
local
oheimb@11025
     5
oheimb@11025
     6
(*In ap_split S T u, term u expects separate arguments for the factors of S,
oheimb@11025
     7
  with result type T.  The call creates a new term expecting one argument
oheimb@11025
     8
  of type S.*)
oheimb@11025
     9
fun ap_split (Type ("*", [T1, T2])) T3 u =
oheimb@11025
    10
      HOLogic.split_const (T1, T2, T3) $
oheimb@11025
    11
      Abs("v", T1,
oheimb@11025
    12
          ap_split T2 T3
oheimb@11025
    13
             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
oheimb@11025
    14
              Bound 0))
oheimb@11025
    15
  | ap_split T T3 u = u;
oheimb@11025
    16
oheimb@11025
    17
(*Curries any Var of function type in the rule*)
oheimb@11025
    18
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
oheimb@11025
    19
      let val T' = HOLogic.prodT_factors T1 ---> T2
oheimb@11025
    20
          val newt = ap_split T1 T2 (Var (v, T'))
oheimb@11025
    21
          val cterm = Thm.cterm_of (#sign (rep_thm rl))
oheimb@11025
    22
      in
oheimb@11025
    23
          instantiate ([], [(cterm t, cterm newt)]) rl
oheimb@11025
    24
      end
oheimb@11025
    25
  | split_rule_var' (t, rl) = rl;
oheimb@11025
    26
oheimb@11025
    27
(*** Complete splitting of partially splitted rules ***)
oheimb@11025
    28
oheimb@11025
    29
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
oheimb@11025
    30
      (ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U)
oheimb@11025
    31
        (incr_boundvars 1 u) $ Bound 0))
oheimb@11025
    32
  | ap_split' _ _ u = u;
oheimb@11025
    33
oheimb@11025
    34
fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
oheimb@11025
    35
      let
oheimb@11025
    36
        val cterm = Thm.cterm_of (#sign (rep_thm rl))
oheimb@11025
    37
        val (Us', U') = strip_type T;
oheimb@11025
    38
        val Us = take (length ts, Us');
oheimb@11025
    39
        val U = drop (length ts, Us') ---> U';
oheimb@11025
    40
        val T' = flat (map HOLogic.prodT_factors Us) ---> U;
oheimb@11025
    41
        fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
oheimb@11025
    42
              let
oheimb@11025
    43
                val Ts = HOLogic.prodT_factors T;
oheimb@11025
    44
                val ys = variantlist (replicate (length Ts) a, xs);
oheimb@11025
    45
              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
oheimb@11025
    46
                (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
oheimb@11025
    47
              end
oheimb@11025
    48
          | mk_tuple (x, _) = x;
oheimb@11025
    49
        val newt = ap_split' Us U (Var (v, T'));
oheimb@11025
    50
        val cterm = Thm.cterm_of (#sign (rep_thm rl));
oheimb@11025
    51
        val (vs', insts) = foldl mk_tuple ((vs, []), ts);
oheimb@11025
    52
      in
oheimb@11025
    53
        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
oheimb@11025
    54
      end
oheimb@11025
    55
  | complete_split_rule_var (_, x) = x;
oheimb@11025
    56
oheimb@11025
    57
fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t)
oheimb@11025
    58
  | collect_vars (vs, t) = (case strip_comb t of
oheimb@11025
    59
        (v as Var _, ts) => (v, ts)::vs
oheimb@11025
    60
      | (t, ts) => foldl collect_vars (vs, ts));
oheimb@11025
    61
oheimb@11025
    62
in
oheimb@11025
    63
oheimb@11025
    64
val split_rule_var = standard o remove_split o split_rule_var';
oheimb@11025
    65
oheimb@11025
    66
(*Curries ALL function variables occurring in a rule's conclusion*)
oheimb@11025
    67
fun split_rule rl = standard (remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)));
oheimb@11025
    68
oheimb@11025
    69
fun complete_split_rule rl =
oheimb@11025
    70
  standard (remove_split (fst (foldr complete_split_rule_var
oheimb@11025
    71
    (collect_vars ([], concl_of rl),
oheimb@11025
    72
     (rl, map (fst o fst o dest_Var) (term_vars (#prop (rep_thm rl))))))))
oheimb@11025
    73
	|> RuleCases.save rl;
oheimb@11025
    74
oheimb@11025
    75
end;
oheimb@11025
    76
fun complete_split x = 
oheimb@11025
    77
	Attrib.no_args (Drule.rule_attribute (K complete_split_rule)) x;
oheimb@11025
    78
oheimb@11025
    79
fun split_rule_goal xss rl = let 
oheimb@11025
    80
	val ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; 
oheimb@11025
    81
	fun one_split i (th,s) = rule_by_tactic (pair_tac s i) th;
oheimb@11025
    82
	fun one_goal (xs,i) th = foldl (one_split i) (th,xs);
oheimb@11025
    83
        in standard (Simplifier.full_simplify ss (foldln one_goal xss rl))
oheimb@11025
    84
	   |> RuleCases.save rl
oheimb@11025
    85
        end;
oheimb@11025
    86
fun split_format x = 
oheimb@11025
    87
	Attrib.syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) 
oheimb@11025
    88
	>> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
oheimb@11025
    89
oheimb@11025
    90
val split_attributes = [Attrib.add_attributes 
oheimb@11025
    91
	[("complete_split", (complete_split, complete_split), 
oheimb@11025
    92
          "recursively split all pair-typed function arguments"),
oheimb@11025
    93
	 ("split_format", (split_format, split_format), 
oheimb@11025
    94
          "split given pair-typed subterms in premises")]];
oheimb@11025
    95