author | haftmann |
Thu, 01 Jul 2010 16:54:44 +0200 | |
changeset 37678 | 0040bafffdef |
parent 37167 | 161cf39694df |
child 40388 | cb9fd7dd641c |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: HOL/Tools/split_rule.ML |
11037 | 2 |
Author: Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen |
3 |
||
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15574
diff
changeset
|
4 |
Some tools for managing tupled arguments and abstractions in rules. |
11037 | 5 |
*) |
6 |
||
35365 | 7 |
signature SPLIT_RULE = |
11037 | 8 |
sig |
35365 | 9 |
val split_rule_var: term -> thm -> thm |
10 |
val split_rule_goal: Proof.context -> string list list -> thm -> thm |
|
11037 | 11 |
val split_rule: thm -> thm |
12 |
val complete_split_rule: thm -> thm |
|
18708 | 13 |
val setup: theory -> theory |
11037 | 14 |
end; |
15 |
||
35365 | 16 |
structure Split_Rule: SPLIT_RULE = |
11037 | 17 |
struct |
18 |
||
19 |
(** split rules **) |
|
20 |
||
35365 | 21 |
fun internal_split_const (Ta, Tb, Tc) = |
22 |
Const (@{const_name Product_Type.internal_split}, |
|
23 |
[[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc); |
|
24 |
||
25 |
val eval_internal_split = |
|
26 |
hol_simplify [@{thm internal_split_def}] o hol_simplify [@{thm internal_split_conv}]; |
|
27 |
||
11037 | 28 |
val remove_internal_split = eval_internal_split o split_all; |
29 |
||
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
30 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
31 |
(*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
|
32 |
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
|
33 |
of type S.*) |
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37167
diff
changeset
|
34 |
fun ap_split (Type (@{type_name Product_Type.prod}, [T1, T2])) T3 u = |
11037 | 35 |
internal_split_const (T1, T2, T3) $ |
36 |
Abs ("v", T1, |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
37 |
ap_split T2 T3 |
32287
65d5c5b30747
cleaned up abstract tuple operations and named them consistently
haftmann
parents:
30722
diff
changeset
|
38 |
((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $ |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
39 |
Bound 0)) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
40 |
| ap_split T T3 u = u; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
41 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
42 |
(*Curries any Var of function type in the rule*) |
19735 | 43 |
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl = |
32287
65d5c5b30747
cleaned up abstract tuple operations and named them consistently
haftmann
parents:
30722
diff
changeset
|
44 |
let val T' = HOLogic.flatten_tupleT T1 ---> T2; |
11037 | 45 |
val newt = ap_split T1 T2 (Var (v, T')); |
19735 | 46 |
val cterm = Thm.cterm_of (Thm.theory_of_thm rl); |
11037 | 47 |
in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end |
19735 | 48 |
| split_rule_var' t rl = rl; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
49 |
|
11037 | 50 |
|
51 |
(* complete splitting of partially splitted rules *) |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
52 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
53 |
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U |
32288
168f31155c5e
cleaned up abstract tuple operations and named them consistently
haftmann
parents:
32287
diff
changeset
|
54 |
(ap_split T (maps HOLogic.flatten_tupleT Ts ---> U) |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
55 |
(incr_boundvars 1 u) $ Bound 0)) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
56 |
| ap_split' _ _ u = u; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
57 |
|
19735 | 58 |
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
|
59 |
let |
19735 | 60 |
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
|
61 |
val (Us', U') = strip_type T; |
33957 | 62 |
val Us = take (length ts) Us'; |
63 |
val U = drop (length ts) Us' ---> U'; |
|
32288
168f31155c5e
cleaned up abstract tuple operations and named them consistently
haftmann
parents:
32287
diff
changeset
|
64 |
val T' = maps HOLogic.flatten_tupleT Us ---> U; |
19735 | 65 |
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
|
66 |
let |
32287
65d5c5b30747
cleaned up abstract tuple operations and named them consistently
haftmann
parents:
30722
diff
changeset
|
67 |
val Ts = HOLogic.flatten_tupleT T; |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19735
diff
changeset
|
68 |
val ys = Name.variant_list xs (replicate (length Ts) a); |
32342
3fabf5b5fc83
path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
haftmann
parents:
32288
diff
changeset
|
69 |
in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
70 |
(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
|
71 |
end |
19735 | 72 |
| mk_tuple _ x = x; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
73 |
val newt = ap_split' Us U (Var (v, T')); |
19735 | 74 |
val cterm = Thm.cterm_of (Thm.theory_of_thm rl); |
75 |
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
|
76 |
in |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
77 |
(instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs') |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
78 |
end |
19735 | 79 |
| complete_split_rule_var _ x = x; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
80 |
|
19735 | 81 |
fun collect_vars (Abs (_, _, t)) = collect_vars t |
82 |
| collect_vars t = |
|
83 |
(case strip_comb t of |
|
84 |
(v as Var _, ts) => cons (v, ts) |
|
85 |
| (t, ts) => fold collect_vars ts); |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
86 |
|
11037 | 87 |
|
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33957
diff
changeset
|
88 |
val split_rule_var = (Drule.export_without_context 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
|
89 |
|
11037 | 90 |
(*curries ALL function variables occurring in a rule's conclusion*) |
91 |
fun split_rule rl = |
|
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
27882
diff
changeset
|
92 |
fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl |
11037 | 93 |
|> remove_internal_split |
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33957
diff
changeset
|
94 |
|> Drule.export_without_context; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
95 |
|
19735 | 96 |
(*curries ALL function variables*) |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
97 |
fun complete_split_rule rl = |
19735 | 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 vars (rl, xs)) |
|
104 |
|> remove_internal_split |
|
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33957
diff
changeset
|
105 |
|> Drule.export_without_context |
33368 | 106 |
|> Rule_Cases.save rl |
19735 | 107 |
end; |
11037 | 108 |
|
109 |
||
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
110 |
fun pair_tac ctxt s = |
37167 | 111 |
res_inst_tac ctxt [(("y", 0), s)] @{thm prod.exhaust} |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
112 |
THEN' hyp_subst_tac |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
113 |
THEN' K prune_params_tac; |
26352 | 114 |
|
35365 | 115 |
val split_rule_ss = HOL_basic_ss addsimps [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}]; |
11037 | 116 |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26352
diff
changeset
|
117 |
fun split_rule_goal ctxt xss rl = |
11037 | 118 |
let |
36546 | 119 |
fun one_split i s = Tactic.rule_by_tactic ctxt (pair_tac ctxt s i); |
19735 | 120 |
fun one_goal (i, xs) = fold (one_split (i + 1)) xs; |
11037 | 121 |
in |
18050 | 122 |
rl |
19735 | 123 |
|> fold_index one_goal xss |
18050 | 124 |
|> Simplifier.full_simplify split_rule_ss |
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33957
diff
changeset
|
125 |
|> Drule.export_without_context |
33368 | 126 |
|> Rule_Cases.save rl |
11037 | 127 |
end; |
128 |
||
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset
|
129 |
|
11037 | 130 |
(* attribute syntax *) |
131 |
||
27882
eaa9fef9f4c1
Args.name_source(_position) for proper position information;
wenzelm
parents:
27809
diff
changeset
|
132 |
(* FIXME dynamically scoped due to Args.name_source/pair_tac *) |
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15574
diff
changeset
|
133 |
|
11037 | 134 |
val setup = |
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset
|
135 |
Attrib.setup @{binding split_format} |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset
|
136 |
(Scan.lift |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset
|
137 |
(Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) || |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36546
diff
changeset
|
138 |
Parse.and_list1 (Scan.repeat Args.name_source) |
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset
|
139 |
>> (fn xss => Thm.rule_attribute (fn context => |
623d4831c8cf
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset
|
140 |
split_rule_goal (Context.proof_of context) xss)))) |
30528 | 141 |
"split pair-typed subterms in premises, or function arguments" #> |
142 |
Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule))) |
|
143 |
"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
|
144 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
145 |
end; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
146 |