--- a/src/HOL/Tools/Function/sum_tree.ML Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/sum_tree.ML Sat Jan 02 23:18:58 2010 +0100
@@ -9,35 +9,43 @@
(* Theory dependencies *)
val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}]
-val sumcase_split_ss = HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})
+val sumcase_split_ss =
+ HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})
(* top-down access in balanced tree *)
fun access_top_down {left, right, init} len i =
- Balanced_Tree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
+ Balanced_Tree.access
+ {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
(* Sum types *)
fun mk_sumT LT RT = Type ("+", [LT, RT])
-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
+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
val App = curry op $
-fun mk_inj ST n i =
- access_top_down
- { init = (ST, I : term -> term),
- left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
- right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
- |> snd
+fun mk_inj ST n i =
+ access_top_down
+ { init = (ST, I : term -> term),
+ left = (fn (T as Type ("+", [LT, RT]), inj) =>
+ (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
+ right =(fn (T as Type ("+", [LT, RT]), inj) =>
+ (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
+ |> snd
-fun mk_proj ST n i =
- access_top_down
- { init = (ST, I : term -> term),
- left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
- right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
- |> snd
+fun mk_proj ST n i =
+ access_top_down
+ { init = (ST, I : term -> term),
+ left = (fn (T as Type ("+", [LT, RT]), proj) =>
+ (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
+ right =(fn (T as Type ("+", [LT, RT]), proj) =>
+ (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
+ |> snd
fun mk_sumcases T fs =
- Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT))
- (map (fn f => (f, domain_type (fastype_of f))) fs)
- |> fst
+ Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT))
+ (map (fn f => (f, domain_type (fastype_of f))) fs)
+ |> fst
end