author | wenzelm |
Fri, 19 Oct 2001 22:01:25 +0200 | |
changeset 11838 | 02d75712061d |
parent 11045 | 971a50fda146 |
child 14981 | e73f8140af78 |
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 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
||
6 |
Some tools for managing tupled arguments and abstractions in rules. |
|
7 |
*) |
|
8 |
||
9 |
signature BASIC_SPLIT_RULE = |
|
10 |
sig |
|
11 |
val split_rule: thm -> thm |
|
12 |
val complete_split_rule: thm -> thm |
|
13 |
end; |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
14 |
|
11037 | 15 |
signature SPLIT_RULE = |
16 |
sig |
|
17 |
include BASIC_SPLIT_RULE |
|
18 |
val split_rule_var: term * thm -> thm |
|
19 |
val split_rule_goal: string list list -> thm -> thm |
|
20 |
val setup: (theory -> theory) list |
|
21 |
end; |
|
22 |
||
23 |
structure SplitRule: SPLIT_RULE = |
|
24 |
struct |
|
25 |
||
26 |
||
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*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
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')); |
|
62 |
val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl)); |
|
63 |
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
|
64 |
| split_rule_var' (t, rl) = rl; |
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 |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
70 |
(ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U) |
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 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
74 |
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
|
75 |
let |
11037 | 76 |
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
|
77 |
val (Us', U') = strip_type T; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
78 |
val Us = take (length ts, Us'); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
79 |
val U = drop (length ts, Us') ---> U'; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
80 |
val T' = flat (map HOLogic.prodT_factors Us) ---> U; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
81 |
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
|
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; |
11037 | 84 |
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
|
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 |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
88 |
| mk_tuple (x, _) = x; |
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')); |
11037 | 90 |
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
|
91 |
val (vs', insts) = foldl mk_tuple ((vs, []), ts); |
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 |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
95 |
| complete_split_rule_var (_, x) = x; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
96 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
97 |
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
|
98 |
| 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
|
99 |
(v as Var _, ts) => (v, ts)::vs |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
100 |
| (t, ts) => foldl collect_vars (vs, ts)); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
101 |
|
11037 | 102 |
|
103 |
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
|
104 |
|
11037 | 105 |
(*curries ALL function variables occurring in a rule's conclusion*) |
106 |
fun split_rule rl = |
|
107 |
foldr split_rule_var' (Term.term_vars (concl_of rl), rl) |
|
108 |
|> remove_internal_split |
|
109 |
|> Drule.standard; |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
110 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
111 |
fun complete_split_rule rl = |
11037 | 112 |
fst (foldr complete_split_rule_var |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
113 |
(collect_vars ([], concl_of rl), |
11037 | 114 |
(rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl)))))) |
115 |
|> remove_internal_split |
|
116 |
|> Drule.standard |
|
117 |
|> RuleCases.save rl; |
|
118 |
||
119 |
||
120 |
val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; |
|
121 |
||
122 |
fun split_rule_goal xss rl = |
|
123 |
let |
|
124 |
fun one_split i (th, s) = Tactic.rule_by_tactic (pair_tac s i) th; |
|
125 |
fun one_goal (xs, i) th = foldl (one_split i) (th, xs); |
|
126 |
in |
|
127 |
Drule.standard (Simplifier.full_simplify split_rule_ss (Library.foldln one_goal xss rl)) |
|
128 |
|> RuleCases.save rl |
|
129 |
end; |
|
130 |
||
131 |
||
132 |
(* attribute syntax *) |
|
133 |
||
11040 | 134 |
fun split_format x = Attrib.syntax |
11045 | 135 |
(Scan.lift (Args.parens (Args.$$$ "complete")) |
136 |
>> K (Drule.rule_attribute (K complete_split_rule)) || |
|
137 |
Args.and_list1 (Scan.lift (Scan.repeat Args.name)) |
|
138 |
>> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x; |
|
11037 | 139 |
|
140 |
val setup = |
|
11040 | 141 |
[Attrib.add_attributes |
142 |
[("split_format", (split_format, split_format), |
|
143 |
"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
|
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 |
|
11037 | 147 |
structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule; |
148 |
open BasicSplitRule; |