author | wenzelm |
Sat, 09 Aug 2008 22:43:46 +0200 | |
changeset 27809 | a1e409db516b |
parent 27239 | f2f42f9fa09d |
child 27882 | eaa9fef9f4c1 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: HOL/Tools/split_rule.ML |
11037 | 2 |
ID: $Id$ |
3 |
Author: Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen |
|
4 |
||
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15574
diff
changeset
|
5 |
Some tools for managing tupled arguments and abstractions in rules. |
11037 | 6 |
*) |
7 |
||
8 |
signature BASIC_SPLIT_RULE = |
|
9 |
sig |
|
10 |
val split_rule: thm -> thm |
|
11 |
val complete_split_rule: thm -> thm |
|
12 |
end; |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
13 |
|
11037 | 14 |
signature SPLIT_RULE = |
15 |
sig |
|
16 |
include BASIC_SPLIT_RULE |
|
19735 | 17 |
val split_rule_var: term -> thm -> thm |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
18 |
val split_rule_goal: Proof.context -> string list list -> thm -> thm |
18708 | 19 |
val setup: theory -> theory |
11037 | 20 |
end; |
21 |
||
22 |
structure SplitRule: SPLIT_RULE = |
|
23 |
struct |
|
24 |
||
25 |
||
19735 | 26 |
|
11037 | 27 |
(** theory context references **) |
28 |
||
11838 | 29 |
val split_conv = thm "split_conv"; |
30 |
val fst_conv = thm "fst_conv"; |
|
31 |
val snd_conv = thm "snd_conv"; |
|
32 |
||
11037 | 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 |
||
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
46 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
47 |
(*In ap_split S T u, term u expects separate arguments for the factors of S, |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
48 |
with result type T. The call creates a new term expecting one argument |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
49 |
of type S.*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
50 |
fun ap_split (Type ("*", [T1, T2])) T3 u = |
11037 | 51 |
internal_split_const (T1, T2, T3) $ |
52 |
Abs ("v", T1, |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
53 |
ap_split T2 T3 |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
54 |
((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
55 |
Bound 0)) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
56 |
| ap_split T T3 u = u; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
57 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
58 |
(*Curries any Var of function type in the rule*) |
19735 | 59 |
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl = |
11037 | 60 |
let val T' = HOLogic.prodT_factors T1 ---> T2; |
61 |
val newt = ap_split T1 T2 (Var (v, T')); |
|
19735 | 62 |
val cterm = Thm.cterm_of (Thm.theory_of_thm rl); |
11037 | 63 |
in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end |
19735 | 64 |
| split_rule_var' t rl = rl; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
65 |
|
11037 | 66 |
|
67 |
(* complete splitting of partially splitted rules *) |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
68 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
69 |
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U |
15570 | 70 |
(ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U) |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
71 |
(incr_boundvars 1 u) $ Bound 0)) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
72 |
| ap_split' _ _ u = u; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
73 |
|
19735 | 74 |
fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) = |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
75 |
let |
19735 | 76 |
val cterm = Thm.cterm_of (Thm.theory_of_thm rl) |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
77 |
val (Us', U') = strip_type T; |
15570 | 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; |
|
19735 | 81 |
fun mk_tuple (v as Var ((a, _), T)) (xs, insts) = |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
82 |
let |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
83 |
val Ts = HOLogic.prodT_factors T; |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19735
diff
changeset
|
84 |
val ys = Name.variant_list xs (replicate (length Ts) a); |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
85 |
in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
86 |
(map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
87 |
end |
19735 | 88 |
| mk_tuple _ x = x; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
89 |
val newt = ap_split' Us U (Var (v, T')); |
19735 | 90 |
val cterm = Thm.cterm_of (Thm.theory_of_thm rl); |
91 |
val (vs', insts) = fold mk_tuple ts (vs, []); |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
92 |
in |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
93 |
(instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs') |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
94 |
end |
19735 | 95 |
| complete_split_rule_var _ x = x; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
96 |
|
19735 | 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); |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
102 |
|
11037 | 103 |
|
19735 | 104 |
val split_rule_var = (Drule.standard o remove_internal_split) oo split_rule_var'; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
105 |
|
11037 | 106 |
(*curries ALL function variables occurring in a rule's conclusion*) |
107 |
fun split_rule rl = |
|
19735 | 108 |
fold_rev split_rule_var' (Term.term_vars (concl_of rl)) rl |
11037 | 109 |
|> remove_internal_split |
110 |
|> Drule.standard; |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
111 |
|
19735 | 112 |
(*curries ALL function variables*) |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
113 |
fun complete_split_rule rl = |
19735 | 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; |
|
11037 | 124 |
|
125 |
||
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
126 |
fun pair_tac ctxt s = |
27239 | 127 |
res_inst_tac ctxt [(("p", 0), s)] @{thm PairE} |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
128 |
THEN' hyp_subst_tac |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
129 |
THEN' K prune_params_tac; |
26352 | 130 |
|
11037 | 131 |
val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; |
132 |
||
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
133 |
fun split_rule_goal ctxt xss rl = |
11037 | 134 |
let |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
135 |
fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i); |
19735 | 136 |
fun one_goal (i, xs) = fold (one_split (i + 1)) xs; |
11037 | 137 |
in |
18050 | 138 |
rl |
19735 | 139 |
|> fold_index one_goal xss |
18050 | 140 |
|> Simplifier.full_simplify split_rule_ss |
19735 | 141 |
|> Drule.standard |
11037 | 142 |
|> RuleCases.save rl |
143 |
end; |
|
144 |
||
145 |
(* attribute syntax *) |
|
146 |
||
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15574
diff
changeset
|
147 |
(* FIXME dynamically scoped due to Args.name/pair_tac *) |
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15574
diff
changeset
|
148 |
|
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27239
diff
changeset
|
149 |
val split_format = Attrib.syntax (Scan.lift |
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27239
diff
changeset
|
150 |
(Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) || |
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27239
diff
changeset
|
151 |
OuterParse.and_list1 (Scan.repeat Args.name) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
152 |
>> (fn xss => Thm.rule_attribute (fn context => |
27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27239
diff
changeset
|
153 |
split_rule_goal (Context.proof_of context) xss)))); |
11037 | 154 |
|
155 |
val setup = |
|
18708 | 156 |
Attrib.add_attributes |
18728 | 157 |
[("split_format", split_format, |
22278 | 158 |
"split pair-typed subterms in premises, or function arguments"), |
159 |
("split_rule", Attrib.no_args (Thm.rule_attribute (K split_rule)), |
|
160 |
"curries ALL function variables occurring in a rule's conclusion")]; |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
161 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
162 |
end; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
163 |
|
11037 | 164 |
structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule; |
165 |
open BasicSplitRule; |