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