author | krauss |
Tue, 07 Nov 2006 22:06:32 +0100 | |
changeset 21237 | b803f9870e97 |
parent 20523 | 36a59e5d0039 |
child 22622 | 25693088396b |
permissions | -rw-r--r-- |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/function_package/sum_tools.ML |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
2 |
ID: $Id$ |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
3 |
Author: Alexander Krauss, TU Muenchen |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
4 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
5 |
A package for general recursive function definitions. |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
6 |
Tools for mutual recursive definitions. This could actually be useful for other packages, too, but needs |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
7 |
some cleanup first... |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
8 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
9 |
*) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
10 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
11 |
signature SUM_TOOLS = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
12 |
sig |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
13 |
type sum_tree |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
14 |
type sum_path |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
15 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
16 |
val projl_inl: thm |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
17 |
val projr_inr: thm |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
18 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
19 |
val mk_tree : typ list -> typ * sum_tree * sum_path list |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
20 |
val mk_tree_distinct : typ list -> typ * sum_tree * sum_path list |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
21 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
22 |
val mk_proj: sum_tree -> sum_path -> term -> term |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
23 |
val mk_inj: sum_tree -> sum_path -> term -> term |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
24 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
25 |
val mk_sumcases: sum_tree -> typ -> term list -> term |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
26 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
27 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
28 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
29 |
structure SumTools: SUM_TOOLS = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
30 |
struct |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
31 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
32 |
val inlN = "Sum_Type.Inl" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
33 |
val inrN = "Sum_Type.Inr" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
34 |
val sumcaseN = "Datatype.sum.sum_case" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
35 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
36 |
val projlN = "FunDef.lproj" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
37 |
val projrN = "FunDef.rproj" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
38 |
val projl_inl = thm "FunDef.lproj_inl" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
39 |
val projr_inr = thm "FunDef.rproj_inr" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
40 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
41 |
fun mk_sumT LT RT = Type ("+", [LT, RT]) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
42 |
fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
43 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
44 |
datatype sum_tree |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
45 |
= Leaf of typ |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
46 |
| Branch of (typ * (typ * sum_tree) * (typ * sum_tree)) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
47 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
48 |
type sum_path = bool list (* true: left, false: right *) |
21237 | 49 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
50 |
fun sum_type_of (Leaf T) = T |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
51 |
| sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST |
21237 | 52 |
|
53 |
||
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
54 |
fun mk_tree Ts = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
55 |
let |
21237 | 56 |
fun mk_tree' 1 [T] = (T, Leaf T, [[]]) |
57 |
| mk_tree' n Ts = |
|
58 |
let |
|
59 |
val n2 = n div 2 |
|
60 |
val (lTs, rTs) = chop n2 Ts |
|
61 |
val (TL, ltree, lpaths) = mk_tree' n2 lTs |
|
62 |
val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs |
|
63 |
val T = mk_sumT TL TR |
|
64 |
val pths = map (cons true) lpaths @ map (cons false) rpaths |
|
65 |
in |
|
66 |
(T, Branch (T, (TL, ltree), (TR, rtree)), pths) |
|
67 |
end |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
68 |
in |
21237 | 69 |
mk_tree' (length Ts) Ts |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
70 |
end |
21237 | 71 |
|
72 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
73 |
fun mk_tree_distinct Ts = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
74 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
75 |
fun insert_once T Ts = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
76 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
77 |
val i = find_index_eq T Ts |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
78 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
79 |
if i = ~1 then (length Ts, Ts @ [T]) else (i, Ts) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
80 |
end |
21237 | 81 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
82 |
val (idxs, dist_Ts) = fold_map insert_once Ts [] |
21237 | 83 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
84 |
val (ST, tree, pths) = mk_tree dist_Ts |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
85 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
86 |
(ST, tree, map (nth pths) idxs) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
87 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
88 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19770
diff
changeset
|
89 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
90 |
fun mk_inj (Leaf _) [] t = t |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
91 |
| mk_inj (Branch (ST, (LT, tr), _)) (true::pth) t = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
92 |
Const (inlN, LT --> ST) $ mk_inj tr pth t |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
93 |
| mk_inj (Branch (ST, _, (RT, tr))) (false::pth) t = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
94 |
Const (inrN, RT --> ST) $ mk_inj tr pth t |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
95 |
| mk_inj _ _ _ = sys_error "mk_inj" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
96 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
97 |
fun mk_proj (Leaf _) [] t = t |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
98 |
| mk_proj (Branch (ST, (LT, tr), _)) (true::pth) t = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
99 |
mk_proj tr pth (Const (projlN, ST --> LT) $ t) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
100 |
| mk_proj (Branch (ST, _, (RT, tr))) (false::pth) t = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
101 |
mk_proj tr pth (Const (projrN, ST --> RT) $ t) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
102 |
| mk_proj _ _ _ = sys_error "mk_proj" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
103 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
104 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
105 |
fun mk_sumcases tree T ts = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
106 |
let |
21237 | 107 |
fun mk_sumcases' (Leaf _) (t::ts) = (t,ts) |
108 |
| mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts = |
|
109 |
let |
|
110 |
val (lcase, ts') = mk_sumcases' ltr ts |
|
111 |
val (rcase, ts'') = mk_sumcases' rtr ts' |
|
112 |
in |
|
113 |
(mk_sumcase LT RT T lcase rcase, ts'') |
|
114 |
end |
|
115 |
| mk_sumcases' _ [] = sys_error "mk_sumcases" |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
116 |
in |
21237 | 117 |
fst (mk_sumcases' tree ts) |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
118 |
end |
21237 | 119 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
120 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
121 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
122 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
123 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
124 |