equal
deleted
inserted
replaced
86 |
86 |
87 fun mk_to_nat_checked T = |
87 fun mk_to_nat_checked T = |
88 Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT); |
88 Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT); |
89 |
89 |
90 val nn = length ns; |
90 val nn = length ns; |
91 val recs as rec1 :: _ = |
91 val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (replicate nn HOLogic.natT)) fpTs recs0; |
92 map2 (fn fpT => mk_co_rec thy Least_FP fpT (replicate nn HOLogic.natT)) fpTs recs0; |
|
93 val arg_Ts = binder_fun_types (fastype_of rec1); |
92 val arg_Ts = binder_fun_types (fastype_of rec1); |
94 val arg_Tss = Library.unflat ctrss0 arg_Ts; |
93 val arg_Tss = Library.unflat ctrss0 arg_Ts; |
95 |
94 |
96 fun mk_U (Type (@{type_name prod}, [T1, T2])) = |
95 fun mk_U (Type (@{type_name prod}, [T1, T2])) = |
97 if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2) |
96 if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2) |