author | haftmann |
Mon, 06 Jun 2005 15:09:47 +0200 | |
changeset 16303 | fee0a02f61bb |
parent 15661 | 9ef583b08647 |
child 18050 | 652c95961a8b |
permissions | -rw-r--r-- |
11037 | 1 |
(* Title: Tools/split_rule.ML |
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 |
|
17 |
val split_rule_var: term * thm -> thm |
|
18 |
val split_rule_goal: string list list -> thm -> thm |
|
19 |
val setup: (theory -> theory) list |
|
20 |
end; |
|
21 |
||
22 |
structure SplitRule: SPLIT_RULE = |
|
23 |
struct |
|
24 |
||
25 |
||
26 |
(** theory context references **) |
|
27 |
||
11838 | 28 |
val split_conv = thm "split_conv"; |
29 |
val fst_conv = thm "fst_conv"; |
|
30 |
val snd_conv = thm "snd_conv"; |
|
31 |
||
11037 | 32 |
fun internal_split_const (Ta, Tb, Tc) = |
33 |
Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc); |
|
34 |
||
35 |
val internal_split_def = thm "internal_split_def"; |
|
36 |
val internal_split_conv = thm "internal_split_conv"; |
|
37 |
||
38 |
||
39 |
||
40 |
(** split rules **) |
|
41 |
||
42 |
val eval_internal_split = hol_simplify [internal_split_def] o hol_simplify [internal_split_conv]; |
|
43 |
val remove_internal_split = eval_internal_split o split_all; |
|
44 |
||
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
45 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
46 |
(*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
|
47 |
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
|
48 |
of type S.*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
49 |
fun ap_split (Type ("*", [T1, T2])) T3 u = |
11037 | 50 |
internal_split_const (T1, T2, T3) $ |
51 |
Abs ("v", T1, |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
52 |
ap_split T2 T3 |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
53 |
((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
|
54 |
Bound 0)) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
55 |
| ap_split T T3 u = u; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
56 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
57 |
(*Curries any Var of function type in the rule*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
58 |
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) = |
11037 | 59 |
let val T' = HOLogic.prodT_factors T1 ---> T2; |
60 |
val newt = ap_split T1 T2 (Var (v, T')); |
|
61 |
val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl)); |
|
62 |
in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
63 |
| split_rule_var' (t, rl) = rl; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
64 |
|
11037 | 65 |
|
66 |
(* complete splitting of partially splitted rules *) |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
67 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
68 |
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U |
15570 | 69 |
(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
|
70 |
(incr_boundvars 1 u) $ Bound 0)) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
71 |
| ap_split' _ _ u = u; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
72 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
73 |
fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) = |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
74 |
let |
11037 | 75 |
val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl)) |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
76 |
val (Us', U') = strip_type T; |
15570 | 77 |
val Us = Library.take (length ts, Us'); |
78 |
val U = Library.drop (length ts, Us') ---> U'; |
|
79 |
val T' = List.concat (map HOLogic.prodT_factors Us) ---> U; |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
80 |
fun mk_tuple ((xs, insts), v as Var ((a, _), T)) = |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
81 |
let |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
82 |
val Ts = HOLogic.prodT_factors T; |
11037 | 83 |
val ys = Term.variantlist (replicate (length Ts) a, xs); |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
84 |
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
|
85 |
(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
|
86 |
end |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
87 |
| mk_tuple (x, _) = x; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
88 |
val newt = ap_split' Us U (Var (v, T')); |
11037 | 89 |
val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl)); |
15570 | 90 |
val (vs', insts) = Library.foldl mk_tuple ((vs, []), ts); |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
91 |
in |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
92 |
(instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs') |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
93 |
end |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
94 |
| complete_split_rule_var (_, x) = x; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
95 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
96 |
fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
97 |
| collect_vars (vs, t) = (case strip_comb t of |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
98 |
(v as Var _, ts) => (v, ts)::vs |
15570 | 99 |
| (t, ts) => Library.foldl collect_vars (vs, ts)); |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
100 |
|
11037 | 101 |
|
102 |
val split_rule_var = Drule.standard o remove_internal_split o split_rule_var'; |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
103 |
|
11037 | 104 |
(*curries ALL function variables occurring in a rule's conclusion*) |
105 |
fun split_rule rl = |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
106 |
foldr split_rule_var' rl (Term.term_vars (concl_of rl)) |
11037 | 107 |
|> remove_internal_split |
108 |
|> Drule.standard; |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
109 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
110 |
fun complete_split_rule rl = |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
111 |
fst (foldr complete_split_rule_var |
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
112 |
(rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl)))) |
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
113 |
(collect_vars ([], concl_of rl))) |
11037 | 114 |
|> remove_internal_split |
115 |
|> Drule.standard |
|
116 |
|> RuleCases.save rl; |
|
117 |
||
118 |
||
119 |
val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; |
|
120 |
||
121 |
fun split_rule_goal xss rl = |
|
122 |
let |
|
123 |
fun one_split i (th, s) = Tactic.rule_by_tactic (pair_tac s i) th; |
|
15570 | 124 |
fun one_goal (xs, i) th = Library.foldl (one_split i) (th, xs); |
11037 | 125 |
in |
126 |
Drule.standard (Simplifier.full_simplify split_rule_ss (Library.foldln one_goal xss rl)) |
|
127 |
|> RuleCases.save rl |
|
128 |
end; |
|
129 |
||
130 |
||
131 |
(* attribute syntax *) |
|
132 |
||
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15574
diff
changeset
|
133 |
(* FIXME dynamically scoped due to Args.name/pair_tac *) |
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15574
diff
changeset
|
134 |
|
11040 | 135 |
fun split_format x = Attrib.syntax |
11045 | 136 |
(Scan.lift (Args.parens (Args.$$$ "complete")) |
137 |
>> K (Drule.rule_attribute (K complete_split_rule)) || |
|
138 |
Args.and_list1 (Scan.lift (Scan.repeat Args.name)) |
|
139 |
>> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x; |
|
11037 | 140 |
|
141 |
val setup = |
|
11040 | 142 |
[Attrib.add_attributes |
143 |
[("split_format", (split_format, split_format), |
|
144 |
"split pair-typed subterms in premises, or function arguments")]]; |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
145 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
146 |
end; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
147 |
|
11037 | 148 |
structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule; |
149 |
open BasicSplitRule; |