author | wenzelm |
Tue, 29 Sep 2009 22:48:24 +0200 | |
changeset 32765 | 3032c0308019 |
parent 32603 | e08fdd615333 |
child 33961 | 03f2ab6a4ea6 |
permissions | -rw-r--r-- |
31775 | 1 |
(* Title: HOL/Tools/Function/sum_tree.ML |
25555 | 2 |
Author: Alexander Krauss, TU Muenchen |
3 |
||
4 |
Some common tools for working with sum types in balanced tree form. |
|
5 |
*) |
|
6 |
||
7 |
structure SumTree = |
|
8 |
struct |
|
9 |
||
10 |
(* Theory dependencies *) |
|
29183
f1648e009dc1
removed duplicate sum_case used only by function package;
krauss
parents:
25555
diff
changeset
|
11 |
val proj_in_rules = [@{thm "Datatype.Projl_Inl"}, @{thm "Datatype.Projr_Inr"}] |
f1648e009dc1
removed duplicate sum_case used only by function package;
krauss
parents:
25555
diff
changeset
|
12 |
val sumcase_split_ss = HOL_basic_ss addsimps (@{thm "Product_Type.split"} :: @{thms "sum.cases"}) |
25555 | 13 |
|
14 |
(* top-down access in balanced tree *) |
|
15 |
fun access_top_down {left, right, init} len i = |
|
32765 | 16 |
Balanced_Tree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init |
25555 | 17 |
|
18 |
(* Sum types *) |
|
19 |
fun mk_sumT LT RT = Type ("+", [LT, RT]) |
|
32603 | 20 |
fun mk_sumcase TL TR T l r = Const (@{const_name sum.sum_case}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r |
25555 | 21 |
|
22 |
val App = curry op $ |
|
23 |
||
24 |
fun mk_inj ST n i = |
|
25 |
access_top_down |
|
26 |
{ init = (ST, I : term -> term), |
|
32603 | 27 |
left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name Inl}, LT --> T)))), |
28 |
right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i |
|
25555 | 29 |
|> snd |
30 |
||
31 |
fun mk_proj ST n i = |
|
32 |
access_top_down |
|
33 |
{ init = (ST, I : term -> term), |
|
32603 | 34 |
left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Datatype.Projl}, T --> LT)) o proj)), |
35 |
right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Datatype.Projr}, T --> RT)) o proj))} n i |
|
25555 | 36 |
|> snd |
37 |
||
38 |
fun mk_sumcases T fs = |
|
32765 | 39 |
Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) |
25555 | 40 |
(map (fn f => (f, domain_type (fastype_of f))) fs) |
41 |
|> fst |
|
42 |
||
43 |
end |