author | krauss |
Wed, 02 Aug 2006 18:33:46 +0200 | |
changeset 20285 | 23f5cd23c1e1 |
parent 19770 | be5c23ebe1eb |
child 20523 | 36a59e5d0039 |
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 |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
20 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
21 |
val mk_proj: sum_tree -> sum_path -> term -> term |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
22 |
val mk_inj: sum_tree -> sum_path -> term -> term |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
23 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
24 |
val mk_sumcases: sum_tree -> typ -> term list -> term |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
25 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
26 |
|
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 |
structure SumTools: SUM_TOOLS = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
29 |
struct |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
30 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
31 |
val inlN = "Sum_Type.Inl" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
32 |
val inrN = "Sum_Type.Inr" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
33 |
val sumcaseN = "Datatype.sum.sum_case" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
34 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
35 |
val projlN = "FunDef.lproj" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
36 |
val projrN = "FunDef.rproj" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
37 |
val projl_inl = thm "FunDef.lproj_inl" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
38 |
val projr_inr = thm "FunDef.rproj_inr" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
39 |
|
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 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
42 |
fun mk_sumT LT RT = Type ("+", [LT, RT]) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
43 |
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
|
44 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
45 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
46 |
datatype sum_tree |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
47 |
= Leaf of typ |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
48 |
| Branch of (typ * (typ * sum_tree) * (typ * sum_tree)) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
49 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
50 |
type sum_path = bool list (* true: left, false: right *) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
51 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
52 |
fun sum_type_of (Leaf T) = T |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
53 |
| sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
54 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
55 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
56 |
fun mk_tree Ts = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
57 |
let |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
58 |
fun mk_tree' 1 [T] = (T, Leaf T, [[]]) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
59 |
| mk_tree' n Ts = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
60 |
let |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
61 |
val n2 = n div 2 |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
62 |
val (lTs, rTs) = chop n2 Ts |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
63 |
val (TL, ltree, lpaths) = mk_tree' n2 lTs |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
64 |
val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
65 |
val T = mk_sumT TL TR |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
66 |
val pths = map (cons true) lpaths @ map (cons false) rpaths |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
67 |
in |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
68 |
(T, Branch (T, (TL, ltree), (TR, rtree)), pths) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
69 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
70 |
in |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
71 |
mk_tree' (length Ts) Ts |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
72 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
73 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
74 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
75 |
fun mk_inj (Leaf _) [] t = t |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
76 |
| mk_inj (Branch (ST, (LT, tr), _)) (true::pth) t = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
77 |
Const (inlN, LT --> ST) $ mk_inj tr pth t |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
78 |
| mk_inj (Branch (ST, _, (RT, tr))) (false::pth) t = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
79 |
Const (inrN, RT --> ST) $ mk_inj tr pth t |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
80 |
| mk_inj _ _ _ = sys_error "mk_inj" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
81 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
82 |
fun mk_proj (Leaf _) [] t = t |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
83 |
| mk_proj (Branch (ST, (LT, tr), _)) (true::pth) t = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
84 |
mk_proj tr pth (Const (projlN, ST --> LT) $ t) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
85 |
| mk_proj (Branch (ST, _, (RT, tr))) (false::pth) t = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
86 |
mk_proj tr pth (Const (projrN, ST --> RT) $ t) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
87 |
| mk_proj _ _ _ = sys_error "mk_proj" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
88 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
89 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
90 |
fun mk_sumcases tree T ts = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
91 |
let |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
92 |
fun mk_sumcases' (Leaf _) (t::ts) = (t,ts) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
93 |
| mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts = |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
94 |
let |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
95 |
val (lcase, ts') = mk_sumcases' ltr ts |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
96 |
val (rcase, ts'') = mk_sumcases' rtr ts' |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
97 |
in |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
98 |
(mk_sumcase LT RT T lcase rcase, ts'') |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
99 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
100 |
| mk_sumcases' _ [] = sys_error "mk_sumcases" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
101 |
in |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
102 |
fst (mk_sumcases' tree ts) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
103 |
end |
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 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
106 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
107 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
108 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
109 |