1(*  Title:      HOL/Tools/split_rule.ML
2    Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
3
4Some tools for managing tupled arguments and abstractions in rules.
5*)
6
7signature SPLIT_RULE =
8sig
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
12end;
13
14structure Split_Rule: SPLIT_RULE =
15struct
16
17(** split rules **)
18
19fun internal_case_prod_const (Ta, Tb, Tc) =
20  Const (\<^const_name>\<open>Product_Type.internal_case_prod\<close>,
21    [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
22
23fun eval_internal_split ctxt =
24  hol_simplify ctxt @{thms internal_case_prod_def} o
25  hol_simplify ctxt @{thms internal_case_prod_conv};
26
27fun 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.*)
33fun ap_split (Type (\<^type_name>\<open>Product_Type.prod\<close>, [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*)
42fun 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
51fun 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
56fun 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
80fun 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
87fun 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*)
91fun 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*)
97fun 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
112val _ =
113  Theory.setup
114   (Attrib.setup \<^binding>\<open>split_format\<close>
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>\<open>split_rule\<close>
119      (Scan.succeed (Thm.rule_attribute [] (split_rule o Context.proof_of)))
120      "curries ALL function variables occurring in a rule's conclusion");
121
122end;
123
124