src/HOL/Tools/Function/sum_tree.ML
author krauss
Sat Jan 02 23:18:58 2010 +0100 (2010-01-02)
changeset 34232 36a2a3029fd3
parent 33961 03f2ab6a4ea6
child 36773 acb789f3936b
permissions -rw-r--r--
new year's resolution: reindented code in function package
haftmann@31775
     1
(*  Title:      HOL/Tools/Function/sum_tree.ML
krauss@25555
     2
    Author:     Alexander Krauss, TU Muenchen
krauss@25555
     3
krauss@25555
     4
Some common tools for working with sum types in balanced tree form.
krauss@25555
     5
*)
krauss@25555
     6
krauss@25555
     7
structure SumTree =
krauss@25555
     8
struct
krauss@25555
     9
krauss@25555
    10
(* Theory dependencies *)
haftmann@33961
    11
val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}]
krauss@34232
    12
val sumcase_split_ss =
krauss@34232
    13
  HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})
krauss@25555
    14
krauss@25555
    15
(* top-down access in balanced tree *)
krauss@25555
    16
fun access_top_down {left, right, init} len i =
krauss@34232
    17
  Balanced_Tree.access
krauss@34232
    18
    {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
krauss@25555
    19
krauss@25555
    20
(* Sum types *)
krauss@25555
    21
fun mk_sumT LT RT = Type ("+", [LT, RT])
krauss@34232
    22
fun mk_sumcase TL TR T l r =
krauss@34232
    23
  Const (@{const_name sum.sum_case},
krauss@34232
    24
    (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
krauss@25555
    25
krauss@25555
    26
val App = curry op $
krauss@25555
    27
krauss@34232
    28
fun mk_inj ST n i =
krauss@34232
    29
  access_top_down
krauss@34232
    30
  { init = (ST, I : term -> term),
krauss@34232
    31
    left = (fn (T as Type ("+", [LT, RT]), inj) =>
krauss@34232
    32
      (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
krauss@34232
    33
    right =(fn (T as Type ("+", [LT, RT]), inj) =>
krauss@34232
    34
      (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
krauss@34232
    35
  |> snd
krauss@25555
    36
krauss@34232
    37
fun mk_proj ST n i =
krauss@34232
    38
  access_top_down
krauss@34232
    39
  { init = (ST, I : term -> term),
krauss@34232
    40
    left = (fn (T as Type ("+", [LT, RT]), proj) =>
krauss@34232
    41
      (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
krauss@34232
    42
    right =(fn (T as Type ("+", [LT, RT]), proj) =>
krauss@34232
    43
      (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
krauss@34232
    44
  |> snd
krauss@25555
    45
krauss@25555
    46
fun mk_sumcases T fs =
krauss@34232
    47
  Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
krauss@34232
    48
    (map (fn f => (f, domain_type (fastype_of f))) fs)
krauss@34232
    49
  |> fst
krauss@25555
    50
krauss@25555
    51
end