equal
deleted
inserted
replaced
57 typ list -> typ list list list -> term list list -> thm list list -> term list list -> |
57 typ list -> typ list list list -> term list list -> thm list list -> term list list -> |
58 thm list list -> local_theory -> |
58 thm list list -> local_theory -> |
59 (thm list * thm * Args.src list) * (thm list list * Args.src list) |
59 (thm list * thm * Args.src list) * (thm list list * Args.src list) |
60 * (thm list list * Args.src list) |
60 * (thm list list * Args.src list) |
61 val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list -> |
61 val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list -> |
62 string * term list * term list list * ((term list list * term list list list) * 'a) list -> |
62 string * term list * term list list * ((term list list * term list list list) |
|
63 * (typ list * typ list list list * typ list list)) list -> |
63 thm list -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> |
64 thm list -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> |
64 typ list -> typ list -> int list list -> int list list -> int list -> thm list list -> |
65 typ list -> typ list -> int list list -> int list list -> int list -> thm list list -> |
65 BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> local_theory -> |
66 BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> local_theory -> |
66 ((thm list * thm) list * Args.src list) |
67 ((thm list * thm) list * Args.src list) |
67 * (thm list list * thm list list * Args.src list) |
68 * (thm list list * thm list list * Args.src list) |
238 in |
239 in |
239 map (Term.subst_TVars rho) ts0 |
240 map (Term.subst_TVars rho) ts0 |
240 end; |
241 end; |
241 |
242 |
242 val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of; |
243 val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of; |
243 |
|
244 fun project_co_recT special_Tname Cs proj = |
|
245 let |
|
246 fun project (Type (s, Ts as [T, U])) = |
|
247 if s = special_Tname andalso member (op =) Cs U then proj (T, U) |
|
248 else Type (s, map project Ts) |
|
249 | project (Type (s, Ts)) = Type (s, map project Ts) |
|
250 | project T = T; |
|
251 in project end; |
|
252 |
|
253 val project_corecT = project_co_recT @{type_name sum}; |
|
254 |
244 |
255 fun unzip_recT Cs (T as Type (@{type_name prod}, Ts as [_, U])) = |
245 fun unzip_recT Cs (T as Type (@{type_name prod}, Ts as [_, U])) = |
256 if member (op =) Cs U then Ts else [T] |
246 if member (op =) Cs U then Ts else [T] |
257 | unzip_recT _ T = [T]; |
247 | unzip_recT _ T = [T]; |
258 |
248 |
456 let val n = length cqfss in |
446 let val n = length cqfss in |
457 Term.lambda c (mk_IfN sum_prod_T cps |
447 Term.lambda c (mk_IfN sum_prod_T cps |
458 (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n))) |
448 (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n))) |
459 end; |
449 end; |
460 |
450 |
461 fun mk_coiter_body lthy cs cpss f_sum_prod_Ts f_Tsss cqfsss dtor_coiter = |
451 fun mk_coiter_body cs cpss f_sum_prod_Ts cqfsss dtor_coiter = |
462 Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss); |
452 Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss); |
463 |
453 |
464 fun define_co_iters fp fpT Cs binding_specs lthy0 = |
454 fun define_co_iters fp fpT Cs binding_specs lthy0 = |
465 let |
455 let |
466 val thy = Proof_Context.theory_of lthy0; |
456 val thy = Proof_Context.theory_of lthy0; |
502 let |
492 let |
503 val nn = length fpTs; |
493 val nn = length fpTs; |
504 |
494 |
505 val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters))); |
495 val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters))); |
506 |
496 |
507 fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, f_Tsss, pf_Tss)) dtor_coiter = |
497 fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, _, pf_Tss)) dtor_coiter = |
508 let |
498 let |
509 val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT; |
499 val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT; |
510 val b = mk_binding suf; |
500 val b = mk_binding suf; |
511 val spec = |
501 val spec = |
512 mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)), |
502 mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)), |
513 mk_coiter_body lthy cs cpss f_sum_prod_Ts f_Tsss cqfsss dtor_coiter); |
503 mk_coiter_body cs cpss f_sum_prod_Ts cqfsss dtor_coiter); |
514 in (b, spec) end; |
504 in (b, spec) end; |
515 in |
505 in |
516 define_co_iters Greatest_FP fpT Cs |
506 define_co_iters Greatest_FP fpT Cs |
517 (map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy |
507 (map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy |
518 end; |
508 end; |
882 fun prove goal tac = |
872 fun prove goal tac = |
883 Goal.prove_sorry lthy [] [] goal (tac o #context) |
873 Goal.prove_sorry lthy [] [] goal (tac o #context) |
884 |> Thm.close_derivation; |
874 |> Thm.close_derivation; |
885 |
875 |
886 val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss; |
876 val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss; |
887 val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss; |
|
888 |
|
889 val corec_thmss = |
877 val corec_thmss = |
890 map2 (map2 prove) corec_goalss corec_tacss |
878 map2 (map2 prove) corec_goalss corec_tacss |
891 |> map (map (unfold_thms lthy @{thms sum_case_if})); |
879 |> map (map (unfold_thms lthy @{thms sum_case_if})); |
892 |
880 |
893 val unfold_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss; |
881 val unfold_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss; |