src/HOL/Tools/split_rule.ML
author paulson
Tue May 22 17:56:06 2007 +0200 (2007-05-22)
changeset 23075 69e30a7e8880
parent 22278 70a7cd02fec1
child 24584 01e83ffa6c54
permissions -rw-r--r--
Some hacks for SPASS format
     1 (*  Title:      Tools/split_rule.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
     4 
     5 Some tools for managing tupled arguments and abstractions in rules.
     6 *)
     7 
     8 signature BASIC_SPLIT_RULE =
     9 sig
    10   val split_rule: thm -> thm
    11   val complete_split_rule: thm -> thm
    12 end;
    13 
    14 signature SPLIT_RULE =
    15 sig
    16   include BASIC_SPLIT_RULE
    17   val split_rule_var: term -> thm -> thm
    18   val split_rule_goal: string list list -> thm -> thm
    19   val setup: theory -> theory
    20 end;
    21 
    22 structure SplitRule: SPLIT_RULE =
    23 struct
    24 
    25 
    26 
    27 (** theory context references **)
    28 
    29 val split_conv = thm "split_conv";
    30 val fst_conv = thm "fst_conv";
    31 val snd_conv = thm "snd_conv";
    32 
    33 fun internal_split_const (Ta, Tb, Tc) =
    34   Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
    35 
    36 val internal_split_def = thm "internal_split_def";
    37 val internal_split_conv = thm "internal_split_conv";
    38 
    39 
    40 
    41 (** split rules **)
    42 
    43 val eval_internal_split = hol_simplify [internal_split_def] o hol_simplify [internal_split_conv];
    44 val remove_internal_split = eval_internal_split o split_all;
    45 
    46 
    47 (*In ap_split S T u, term u expects separate arguments for the factors of S,
    48   with result type T.  The call creates a new term expecting one argument
    49   of type S.*)
    50 fun ap_split (Type ("*", [T1, T2])) T3 u =
    51       internal_split_const (T1, T2, T3) $
    52       Abs ("v", T1,
    53           ap_split T2 T3
    54              ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
    55               Bound 0))
    56   | ap_split T T3 u = u;
    57 
    58 (*Curries any Var of function type in the rule*)
    59 fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
    60       let val T' = HOLogic.prodT_factors T1 ---> T2;
    61           val newt = ap_split T1 T2 (Var (v, T'));
    62           val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
    63       in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
    64   | split_rule_var' t rl = rl;
    65 
    66 
    67 (* complete splitting of partially splitted rules *)
    68 
    69 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
    70       (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U)
    71         (incr_boundvars 1 u) $ Bound 0))
    72   | ap_split' _ _ u = u;
    73 
    74 fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
    75       let
    76         val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
    77         val (Us', U') = strip_type T;
    78         val Us = Library.take (length ts, Us');
    79         val U = Library.drop (length ts, Us') ---> U';
    80         val T' = List.concat (map HOLogic.prodT_factors Us) ---> U;
    81         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
    82               let
    83                 val Ts = HOLogic.prodT_factors T;
    84                 val ys = Name.variant_list xs (replicate (length Ts) a);
    85               in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
    86                 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
    87               end
    88           | mk_tuple _ x = x;
    89         val newt = ap_split' Us U (Var (v, T'));
    90         val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
    91         val (vs', insts) = fold mk_tuple ts (vs, []);
    92       in
    93         (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
    94       end
    95   | complete_split_rule_var _ x = x;
    96 
    97 fun collect_vars (Abs (_, _, t)) = collect_vars t
    98   | collect_vars t =
    99       (case strip_comb t of
   100         (v as Var _, ts) => cons (v, ts)
   101       | (t, ts) => fold collect_vars ts);
   102 
   103 
   104 val split_rule_var = (Drule.standard o remove_internal_split) oo split_rule_var';
   105 
   106 (*curries ALL function variables occurring in a rule's conclusion*)
   107 fun split_rule rl =
   108   fold_rev split_rule_var' (Term.term_vars (concl_of rl)) rl
   109   |> remove_internal_split
   110   |> Drule.standard;
   111 
   112 (*curries ALL function variables*)
   113 fun complete_split_rule rl =
   114   let
   115     val prop = Thm.prop_of rl;
   116     val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
   117     val vars = collect_vars prop [];
   118   in
   119     fst (fold_rev complete_split_rule_var vars (rl, xs))
   120     |> remove_internal_split
   121     |> Drule.standard
   122     |> RuleCases.save rl
   123   end;
   124 
   125 
   126 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
   127 
   128 fun split_rule_goal xss rl =
   129   let
   130     fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
   131     fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
   132   in
   133     rl
   134     |> fold_index one_goal xss
   135     |> Simplifier.full_simplify split_rule_ss
   136     |> Drule.standard
   137     |> RuleCases.save rl
   138   end;
   139 
   140 (* attribute syntax *)
   141 
   142 (* FIXME dynamically scoped due to Args.name/pair_tac *)
   143 
   144 fun split_format x = Attrib.syntax
   145   (Scan.lift (Args.parens (Args.$$$ "complete"))
   146     >> K (Thm.rule_attribute (K complete_split_rule)) ||
   147   Args.and_list1 (Scan.lift (Scan.repeat Args.name))
   148     >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss)))) x;
   149 
   150 val setup =
   151   Attrib.add_attributes
   152     [("split_format", split_format,
   153       "split pair-typed subterms in premises, or function arguments"),
   154      ("split_rule", Attrib.no_args (Thm.rule_attribute (K split_rule)),
   155       "curries ALL function variables occurring in a rule's conclusion")];
   156 
   157 end;
   158 
   159 structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule;
   160 open BasicSplitRule;