src/HOL/Tools/split_rule.ML
author haftmann
Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424 c3658c18b7bc
parent 60642 48dd1cefb4ae
child 61853 fb7756087101
permissions -rw-r--r--
prod_case as canonical name for product type eliminator
     1 (*  Title:      HOL/Tools/split_rule.ML
     2     Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
     3 
     4 Some tools for managing tupled arguments and abstractions in rules.
     5 *)
     6 
     7 signature SPLIT_RULE =
     8 sig
     9   val split_rule_var: Proof.context -> term -> thm -> thm
    10   val split_rule: Proof.context -> thm -> thm
    11   val complete_split_rule: Proof.context -> thm -> thm
    12 end;
    13 
    14 structure Split_Rule: SPLIT_RULE =
    15 struct
    16 
    17 (** split rules **)
    18 
    19 fun internal_case_prod_const (Ta, Tb, Tc) =
    20   Const (@{const_name Product_Type.internal_case_prod},
    21     [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
    22 
    23 fun eval_internal_split ctxt =
    24   hol_simplify ctxt @{thms internal_case_prod_def} o
    25   hol_simplify ctxt @{thms internal_case_prod_conv};
    26 
    27 fun remove_internal_split ctxt = eval_internal_split ctxt o split_all ctxt;
    28 
    29 
    30 (*In ap_split S T u, term u expects separate arguments for the factors of S,
    31   with result type T.  The call creates a new term expecting one argument
    32   of type S.*)
    33 fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u =
    34       internal_case_prod_const (T1, T2, T3) $
    35       Abs ("v", T1,
    36           ap_split T2 T3
    37              ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $
    38               Bound 0))
    39   | ap_split _ T3 u = u;
    40 
    41 (*Curries any Var of function type in the rule*)
    42 fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl =
    43       let val T' = HOLogic.flatten_tupleT T1 ---> T2;
    44           val newt = ap_split T1 T2 (Var (v, T'));
    45       in Thm.instantiate ([], [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end
    46   | split_rule_var' _ _ rl = rl;
    47 
    48 
    49 (* complete splitting of partially split rules *)
    50 
    51 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
    52       (ap_split T (maps HOLogic.flatten_tupleT Ts ---> U)
    53         (incr_boundvars 1 u) $ Bound 0))
    54   | ap_split' _ _ u = u;
    55 
    56 fun complete_split_rule_var ctxt (t as Var (v, T), ts) (rl, vs) =
    57       let
    58         val (Us', U') = strip_type T;
    59         val Us = take (length ts) Us';
    60         val U = drop (length ts) Us' ---> U';
    61         val T' = maps HOLogic.flatten_tupleT Us ---> U;
    62         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
    63               let
    64                 val Ts = HOLogic.flatten_tupleT T;
    65                 val ys = Name.variant_list xs (replicate (length Ts) a);
    66               in
    67                 (xs @ ys,
    68                   (dest_Var v,
    69                     Thm.cterm_of ctxt (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
    70                       (map (Var o apfst (rpair 0)) (ys ~~ Ts)))) :: insts)
    71               end
    72           | mk_tuple _ x = x;
    73         val newt = ap_split' Us U (Var (v, T'));
    74         val (vs', insts) = fold mk_tuple ts (vs, []);
    75       in
    76         (Drule.instantiate_normalize ([], ((v, T), Thm.cterm_of ctxt newt) :: insts) rl, vs')
    77       end
    78   | complete_split_rule_var _ _ x = x;
    79 
    80 fun collect_vars (Abs (_, _, t)) = collect_vars t
    81   | collect_vars t =
    82       (case strip_comb t of
    83         (v as Var _, ts) => cons (v, ts)
    84       | (_, ts) => fold collect_vars ts);
    85 
    86 
    87 fun split_rule_var ctxt =
    88   (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var' ctxt;
    89 
    90 (*curries ALL function variables occurring in a rule's conclusion*)
    91 fun split_rule ctxt rl =
    92   fold_rev (split_rule_var' ctxt) (Misc_Legacy.term_vars (Thm.concl_of rl)) rl
    93   |> remove_internal_split ctxt
    94   |> Drule.export_without_context;
    95 
    96 (*curries ALL function variables*)
    97 fun complete_split_rule ctxt rl =
    98   let
    99     val prop = Thm.prop_of rl;
   100     val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop [];
   101     val vars = collect_vars prop [];
   102   in
   103     fst (fold_rev (complete_split_rule_var ctxt) vars (rl, xs))
   104     |> remove_internal_split ctxt
   105     |> Drule.export_without_context
   106     |> Rule_Cases.save rl
   107   end;
   108 
   109 
   110 (* attribute syntax *)
   111 
   112 val _ =
   113   Theory.setup
   114    (Attrib.setup @{binding split_format}
   115       (Scan.lift (Args.parens (Args.$$$ "complete")
   116         >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
   117       "split pair-typed subterms in premises, or function arguments" #>
   118     Attrib.setup @{binding split_rule}
   119       (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
   120       "curries ALL function variables occurring in a rule's conclusion");
   121 
   122 end;
   123