src/HOL/Tools/Function/sum_tree.ML
changeset 32765 3032c0308019
parent 32603 e08fdd615333
child 33961 03f2ab6a4ea6
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
    11 val proj_in_rules = [@{thm "Datatype.Projl_Inl"}, @{thm "Datatype.Projr_Inr"}]
    11 val proj_in_rules = [@{thm "Datatype.Projl_Inl"}, @{thm "Datatype.Projr_Inr"}]
    12 val sumcase_split_ss = HOL_basic_ss addsimps (@{thm "Product_Type.split"} :: @{thms "sum.cases"})
    12 val sumcase_split_ss = HOL_basic_ss addsimps (@{thm "Product_Type.split"} :: @{thms "sum.cases"})
    13 
    13 
    14 (* top-down access in balanced tree *)
    14 (* top-down access in balanced tree *)
    15 fun access_top_down {left, right, init} len i =
    15 fun access_top_down {left, right, init} len i =
    16     BalancedTree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
    16     Balanced_Tree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
    17 
    17 
    18 (* Sum types *)
    18 (* Sum types *)
    19 fun mk_sumT LT RT = Type ("+", [LT, RT])
    19 fun mk_sumT LT RT = Type ("+", [LT, RT])
    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
    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
    21 
    21 
    34       left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Datatype.Projl}, T --> LT)) o proj)),
    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
    35       right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Datatype.Projr}, T --> RT)) o proj))} n i
    36     |> snd
    36     |> snd
    37 
    37 
    38 fun mk_sumcases T fs =
    38 fun mk_sumcases T fs =
    39       BalancedTree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
    39       Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
    40                         (map (fn f => (f, domain_type (fastype_of f))) fs)
    40                         (map (fn f => (f, domain_type (fastype_of f))) fs)
    41       |> fst
    41       |> fst
    42 
    42 
    43 end
    43 end