47 |
47 |
48 fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); |
48 fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); |
49 fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs; |
49 fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs; |
50 fun mk_uncurried2_fun f xss = |
50 fun mk_uncurried2_fun f xss = |
51 mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss); |
51 mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss); |
52 |
|
53 val mk_sumTN_balanced = Balanced_Tree.make mk_sumT; |
|
54 val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT; |
|
55 |
|
56 fun mk_InN_balanced sum_T n t k = |
|
57 let |
|
58 fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t |
|
59 | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t |
|
60 | repair_types _ t = t |
|
61 and repair_inj_types T s get t = |
|
62 let val T' = get (dest_sumT T) in |
|
63 Const (s, T' --> T) $ repair_types T' t |
|
64 end; |
|
65 in |
|
66 Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k |
|
67 |> repair_types sum_T |
|
68 end; |
|
69 |
|
70 val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case; |
|
71 |
|
72 fun mk_sumEN_balanced 1 = @{thm one_pointE} |
|
73 | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*) |
|
74 | mk_sumEN_balanced n = |
|
75 Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f}))) |
|
76 (replicate n asm_rl) OF (replicate n (impI RS allI)) RS @{thm obj_one_pointE}; |
|
77 |
52 |
78 fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v)); |
53 fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v)); |
79 |
54 |
80 fun tack z_name (c, v) f = |
55 fun tack z_name (c, v) f = |
81 let val z = Free (z_name, mk_sumT (fastype_of v, fastype_of c)) in |
56 let val z = Free (z_name, mk_sumT (fastype_of v, fastype_of c)) in |