1(* Title: HOL/Tools/Function/sum_tree.ML 2 Author: Alexander Krauss, TU Muenchen 3 4Some common tools for working with sum types in balanced tree form. 5*) 6 7signature SUM_TREE = 8sig 9 val sumcase_split_ss: simpset 10 val access_top_down: {init: 'a, left: 'a -> 'a, right: 'a -> 'a} -> int -> int -> 'a 11 val mk_sumT: typ -> typ -> typ 12 val mk_sumcase: typ -> typ -> typ -> term -> term -> term 13 val App: term -> term -> term 14 val mk_inj: typ -> int -> int -> term -> term 15 val mk_proj: typ -> int -> int -> term -> term 16 val mk_sumcases: typ -> term list -> term 17end 18 19structure Sum_Tree: SUM_TREE = 20struct 21 22(* Theory dependencies *) 23val sumcase_split_ss = 24 simpset_of (put_simpset HOL_basic_ss @{context} 25 addsimps (@{thm Product_Type.split} :: @{thms sum.case})) 26 27(* top-down access in balanced tree *) 28fun access_top_down {left, right, init} len i = 29 Balanced_Tree.access 30 {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init 31 32(* Sum types *) 33fun mk_sumT LT RT = Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]) 34fun mk_sumcase TL TR T l r = 35 Const (\<^const_name>\<open>sum.case_sum\<close>, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r 36 37val App = curry op $ 38 39fun mk_inj ST n i = 40 access_top_down 41 { init = (ST, I : term -> term), 42 left = (fn (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]), inj) => 43 (LT, inj o App (Const (\<^const_name>\<open>Inl\<close>, LT --> T)))), 44 right =(fn (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]), inj) => 45 (RT, inj o App (Const (\<^const_name>\<open>Inr\<close>, RT --> T))))} n i 46 |> snd 47 48fun mk_proj ST n i = 49 access_top_down 50 { init = (ST, I : term -> term), 51 left = (fn (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]), proj) => 52 (LT, App (Const (\<^const_name>\<open>Sum_Type.projl\<close>, T --> LT)) o proj)), 53 right =(fn (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]), proj) => 54 (RT, App (Const (\<^const_name>\<open>Sum_Type.projr\<close>, T --> RT)) o proj))} n i 55 |> snd 56 57fun mk_sumcases T fs = 58 Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 59 (map (fn f => (f, domain_type (fastype_of f))) fs) 60 |> fst 61 62end 63