equal
deleted
inserted
replaced
350 fun basic_corec_specs_of ctxt res_T = |
350 fun basic_corec_specs_of ctxt res_T = |
351 (case res_T of |
351 (case res_T of |
352 Type (T_name, _) => |
352 Type (T_name, _) => |
353 (case Ctr_Sugar.ctr_sugar_of ctxt T_name of |
353 (case Ctr_Sugar.ctr_sugar_of ctxt T_name of |
354 NONE => not_codatatype ctxt res_T |
354 NONE => not_codatatype ctxt res_T |
355 | SOME {ctrs, discs, selss, ...} => |
355 | SOME {T = fpT, ctrs, discs, selss, ...} => |
356 let |
356 let |
357 val thy = Proof_Context.theory_of ctxt; |
357 val thy = Proof_Context.theory_of ctxt; |
358 |
358 |
359 val gfpT = body_type (fastype_of (hd ctrs)); |
359 val As_rho = tvar_subst thy [fpT] [res_T]; |
360 val As_rho = tvar_subst thy [gfpT] [res_T]; |
|
361 val substA = Term.subst_TVars As_rho; |
360 val substA = Term.subst_TVars As_rho; |
362 |
361 |
363 fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels}; |
362 fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels}; |
364 in |
363 in |
365 map3 mk_spec ctrs discs selss |
364 map3 mk_spec ctrs discs selss |
382 val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars; |
381 val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars; |
383 |
382 |
384 val indices = map #fp_res_index fp_sugars; |
383 val indices = map #fp_res_index fp_sugars; |
385 val perm_indices = map #fp_res_index perm_fp_sugars; |
384 val perm_indices = map #fp_res_index perm_fp_sugars; |
386 |
385 |
387 val perm_gfpTs = map #T perm_fp_sugars; |
386 val perm_fpTs = map #T perm_fp_sugars; |
388 val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars; |
387 val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars; |
389 |
388 |
390 val nn0 = length res_Ts; |
389 val nn0 = length res_Ts; |
391 val nn = length perm_gfpTs; |
390 val nn = length perm_fpTs; |
392 val kks = 0 upto nn - 1; |
391 val kks = 0 upto nn - 1; |
393 val perm_ns' = map length perm_ctrXs_Tsss'; |
392 val perm_ns' = map length perm_ctrXs_Tsss'; |
394 |
393 |
395 val perm_Ts = map #T perm_fp_sugars; |
394 val perm_Ts = map #T perm_fp_sugars; |
396 val perm_Xs = map #X perm_fp_sugars; |
395 val perm_Xs = map #X perm_fp_sugars; |
424 val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss); |
423 val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss); |
425 val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss); |
424 val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss); |
426 val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss); |
425 val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss); |
427 |
426 |
428 val f_Tssss = unpermute perm_f_Tssss; |
427 val f_Tssss = unpermute perm_f_Tssss; |
429 val gfpTs = unpermute perm_gfpTs; |
428 val fpTs = unpermute perm_fpTs; |
430 val Cs = unpermute perm_Cs; |
429 val Cs = unpermute perm_Cs; |
431 |
430 |
432 val As_rho = tvar_subst thy (take nn0 gfpTs) res_Ts; |
431 val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts; |
433 val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts; |
432 val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts; |
434 |
433 |
435 val substA = Term.subst_TVars As_rho; |
434 val substA = Term.subst_TVars As_rho; |
436 val substAT = Term.typ_subst_TVars As_rho; |
435 val substAT = Term.typ_subst_TVars As_rho; |
437 val substCT = Term.typ_subst_TVars Cs_rho; |
436 val substCT = Term.typ_subst_TVars Cs_rho; |