# HG changeset patch # User blanchet # Date 1482430498 -3600 # Node ID a15785625f7c7f303fb91f429e95e750bb851aa4 # Parent a42dbe9d2c1f3baa2e0f571ec8e426a33a347607 export ML functions (towards nonuniform codatatypes) + signature tuning diff -r a42dbe9d2c1f -r a15785625f7c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Dec 22 17:36:28 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Dec 22 19:14:58 2016 +0100 @@ -168,6 +168,9 @@ term list * ((term * (term * term)) list * (int * term)) list * term val finish_induct_prem: Proof.context -> int -> term list -> term list * ((term * (term * term)) list * (int * term)) list * term -> term + val mk_coinduct_prem: Proof.context -> typ list -> typ list -> term list -> term -> term -> + term -> int -> term list -> term list list -> term list -> term list list -> typ list list -> + term val mk_induct_attrs: term list list -> Token.src list val mk_coinduct_attrs: typ list -> term list list -> term list list -> int list list -> Token.src list * Token.src list @@ -176,18 +179,18 @@ BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list -> term list -> thm list -> Proof.context -> lfp_sugar_thms - val derive_coinduct_thms_for_types: bool -> (term -> term) -> BNF_Def.bnf list -> thm -> - thm list -> BNF_Def.bnf list -> typ list -> typ list -> typ list list list -> int list -> + val derive_coinduct_thms_for_types: Proof.context -> bool -> (term -> term) -> BNF_Def.bnf list -> + thm -> thm list -> BNF_Def.bnf list -> typ list -> typ list -> typ list list list -> int list -> thm list -> thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> - Proof.context -> (thm list * thm) list - val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list -> + (thm list * thm) list + val derive_coinduct_corecs_thms_for_types: Proof.context -> BNF_Def.bnf list -> string * term list * term list list * (((term list list * term list list * term list list list list * term list list list list) * term list list list) * typ list) -> thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> typ list list list -> int list list -> int list list -> int list -> thm list -> thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list -> - thm list -> Proof.context -> gfp_sugar_thms + thm list -> gfp_sugar_thms val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list -> binding list -> binding list list -> binding list -> (string * sort) list -> @@ -1623,7 +1626,7 @@ @{map 5} mk_preds_getterss_join cs cpss f_absTs abss cqgsss))) end; -fun mk_induct_raw_prem_prems names_lthy Xss setss_fp_nesting (x as Free (s, Type (T_name, Ts0))) +fun mk_induct_raw_prem_prems names_ctxt Xss setss_fp_nesting (x as Free (s, Type (T_name, Ts0))) (Type (_, Xs_Ts0)) = (case AList.lookup (op =) setss_fp_nesting T_name of NONE => [] @@ -1633,9 +1636,9 @@ filter (exists_subtype_in (flat Xss) o fst) (Xs_Ts0 ~~ (Ts0 ~~ raw_sets0)) |> split_list ||> split_list; val sets = map (mk_set Ts0) raw_sets; - val (ys, names_lthy') = names_lthy |> mk_Frees s Ts; + val (ys, names_ctxt') = names_ctxt |> mk_Frees s Ts; val xysets = map (pair x) (ys ~~ sets); - val ppremss = map2 (mk_induct_raw_prem_prems names_lthy' Xss setss_fp_nesting) ys Xs_Ts; + val ppremss = map2 (mk_induct_raw_prem_prems names_ctxt' Xss setss_fp_nesting) ys Xs_Ts; in flat (map2 (map o apfst o cons) xysets ppremss) end) @@ -1643,29 +1646,56 @@ [([], (find_index (fn Xs => member (op =) Xs X) Xss + 1, x))] | mk_induct_raw_prem_prems _ _ _ _ _ = []; -fun mk_induct_raw_prem modify_x names_lthy Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts = +fun mk_induct_raw_prem modify_x names_ctxt Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts = let - val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts; + val (xs, names_ctxt') = names_ctxt |> mk_Frees "x" ctr_Ts; val pprems = - flat (map2 (mk_induct_raw_prem_prems names_lthy' Xss setss_fp_nesting) xs ctrXs_Ts); + flat (map2 (mk_induct_raw_prem_prems names_ctxt' Xss setss_fp_nesting) xs ctrXs_Ts); val y = Term.list_comb (ctr, map modify_x xs); - val p' = enforce_type names_lthy domain_type (fastype_of y) p; + val p' = enforce_type names_ctxt domain_type (fastype_of y) p; in (xs, pprems, HOLogic.mk_Trueprop (p' $ y)) end; fun close_induct_prem_prem nn ps xs t = fold_rev Logic.all (map Free (drop (nn + length xs) (rev (Term.add_frees t (map dest_Free xs @ map_filter (try dest_Free) ps))))) t; -fun finish_induct_prem_prem lthy nn ps xs (xysets, (j, x)) = - let val p' = enforce_type lthy domain_type (fastype_of x) (nth ps (j - 1)) in +fun finish_induct_prem_prem ctxt nn ps xs (xysets, (j, x)) = + let val p' = enforce_type ctxt domain_type (fastype_of x) (nth ps (j - 1)) in close_induct_prem_prem nn ps xs (Logic.list_implies (map (fn (x', (y, set)) => mk_Trueprop_mem (y, set $ x')) xysets, HOLogic.mk_Trueprop (p' $ x))) end; -fun finish_induct_prem lthy nn ps (xs, raw_pprems, concl) = +fun finish_induct_prem ctxt nn ps (xs, raw_pprems, concl) = fold_rev Logic.all xs (Logic.list_implies - (map (finish_induct_prem_prem lthy nn ps xs) raw_pprems, concl)); + (map (finish_induct_prem_prem ctxt nn ps xs) raw_pprems, concl)); + +fun mk_coinduct_prem_ctr_concls ctxt Xs fpTs rs' n k udisc usels vdisc vsels ctrXs_Ts = + let + fun build_the_rel rs' T Xs_T = + build_rel [] ctxt [] [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) + |> Term.subst_atomic_types (Xs ~~ fpTs); + fun build_rel_app rs' usel vsel Xs_T = + fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T); + in + (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @ + (if null usels then + [] + else + [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], + Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]) + end; + +fun mk_coinduct_prem_concl ctxt Xs fpTs rs' n udiscs uselss vdiscs vselss ctrXs_Tss = + @{map 6} (mk_coinduct_prem_ctr_concls ctxt Xs fpTs rs' n) + (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss + |> flat |> Library.foldr1 HOLogic.mk_conj + handle List.Empty => @{term True}; + +fun mk_coinduct_prem ctxt Xs fpTs rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = + fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, + HOLogic.mk_Trueprop (mk_coinduct_prem_concl ctxt Xs fpTs rs' n udiscs uselss vdiscs vselss + ctrXs_Tss))); fun postproc_co_induct ctxt nn prop prop_conj = Drule.zero_var_indexes @@ -1679,7 +1709,7 @@ let val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss); in [Attrib.case_names induct_cases] end; -fun derive_rel_induct_thms_for_types lthy nn fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct +fun derive_rel_induct_thms_for_types ctxt nn fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs = let val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); @@ -1689,7 +1719,7 @@ val ctrBs_Tsss = map (map (map B_ify_T)) ctrAs_Tsss; val ctrBss = map (map B_ify) ctrAss; - val ((((Rs, IRs), ctrAsss), ctrBsss), names_lthy) = lthy + val ((((Rs, IRs), ctrAsss), ctrBsss), names_ctxt) = ctxt |> mk_Frees "R" (map2 mk_pred2T As Bs) ||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts) ||>> mk_Freesss "a" ctrAs_Tsss @@ -1699,30 +1729,30 @@ let fun mk_prem ctrA ctrB argAs argBs = fold_rev Logic.all (argAs @ argBs) (fold_rev (curry Logic.mk_implies) - (map2 (HOLogic.mk_Trueprop oo build_rel_app names_lthy (Rs @ IRs) fpA_Ts) argAs argBs) - (HOLogic.mk_Trueprop (build_rel_app names_lthy (Rs @ IRs) fpA_Ts + (map2 (HOLogic.mk_Trueprop oo build_rel_app names_ctxt (Rs @ IRs) fpA_Ts) argAs argBs) + (HOLogic.mk_Trueprop (build_rel_app names_ctxt (Rs @ IRs) fpA_Ts (Term.list_comb (ctrA, argAs)) (Term.list_comb (ctrB, argBs))))); in flat (@{map 4} (@{map 4} mk_prem) ctrAss ctrBss ctrAsss ctrBsss) end; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq - (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs)); - val vars = Variable.add_free_names lthy goal []; + (map2 (build_the_rel ctxt (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs)); + val vars = Variable.add_free_names ctxt goal []; val rel_induct0_thm = - Goal.prove_sorry lthy vars prems goal (fn {context = ctxt, prems} => + Goal.prove_sorry ctxt vars prems goal (fn {context = ctxt, prems} => mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs) |> Thm.close_derivation; in - (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm, + (postproc_co_induct ctxt nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm, mk_induct_attrs ctrAss) end; fun derive_induct_recs_thms_for_types plugins pre_bnfs rec_args_typess ctor_induct ctor_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss pre_abs_inverses pre_type_definitions - abs_inverses ctrss ctr_defss recs rec_defs lthy = + abs_inverses ctrss ctr_defss recs rec_defs ctxt = let val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; @@ -1738,7 +1768,7 @@ val fp_b_names = map base_name_of_typ fpTs; - val (((ps, xsss), us'), names_lthy) = lthy + val (((ps, xsss), us'), names_ctxt) = ctxt |> mk_Frees "P" (map mk_pred1T fpTs) ||>> mk_Freesss "x" ctr_Tsss ||>> Variable.variant_fixes fp_b_names; @@ -1750,20 +1780,20 @@ val (induct_thms, induct_thm) = let val raw_premss = @{map 4} (@{map 3} - o mk_induct_raw_prem I names_lthy (map single Xs) setss_fp_nesting) + o mk_induct_raw_prem I names_ctxt (map single Xs) setss_fp_nesting) ps ctrss ctr_Tsss ctrXs_Tsss; val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us)); val goal = - Library.foldr (Logic.list_implies o apfst (map (finish_induct_prem lthy nn ps))) + Library.foldr (Logic.list_implies o apfst (map (finish_induct_prem ctxt nn ps))) (raw_premss, concl); - val vars = Variable.add_free_names lthy goal []; + val vars = Variable.add_free_names ctxt goal []; val kksss = map (map (map (fst o snd) o #2)) raw_premss; val ctor_induct' = ctor_induct OF (map2 mk_absumprodE pre_type_definitions mss); val thm = - Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => + Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} => mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' pre_abs_inverses abs_inverses fp_nesting_set_maps pre_set_defss) |> Thm.close_derivation; @@ -1796,7 +1826,7 @@ indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk)); in - build_map lthy [] [] build_simple (T, U) $ x + build_map ctxt [] [] build_simple (T, U) $ x end; val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss; @@ -1807,7 +1837,7 @@ ctor_rec_thms pre_abs_inverses abs_inverses ctr_defss; fun prove goal tac = - Goal.prove_sorry lthy [] [] goal (tac o #context) + Goal.prove_sorry ctxt [] [] goal (tac o #context) |> Thm.close_derivation; in map2 (map2 prove) goalss tacss @@ -1852,7 +1882,7 @@ (coinduct_attrs, common_coinduct_attrs) end; -fun derive_rel_coinduct_thms_for_types lthy nn fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list) +fun derive_rel_coinduct_thms_for_types ctxt nn fpA_Ts ns As Bs mss (ctr_sugars : ctr_sugar list) abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct live_nesting_rel_eqs = let @@ -1862,14 +1892,14 @@ val (Rs, IRs, fpAs, fpBs, _) = let val fp_names = map base_name_of_typ fpA_Ts; - val ((((Rs, IRs), fpAs_names), fpBs_names), names_lthy) = lthy + val ((((Rs, IRs), fpAs_names), fpBs_names), names_ctxt) = ctxt |> mk_Frees "R" (map2 mk_pred2T As Bs) ||>> mk_Frees "IR" (map2 mk_pred2T fpA_Ts fpB_Ts) ||>> Variable.variant_fixes fp_names ||>> Variable.variant_fixes (map (suffix "'") fp_names); in (Rs, IRs, map2 (curry Free) fpAs_names fpA_Ts, map2 (curry Free) fpBs_names fpB_Ts, - names_lthy) + names_ctxt) end; val ((discA_tss, selA_tsss), (discB_tss, selB_tsss)) = @@ -1895,7 +1925,7 @@ [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [discA_t, discB_t], Library.foldr1 HOLogic.mk_conj - (map2 (build_rel_app lthy (Rs @ IRs) fpA_Ts) selA_ts selB_ts))]); + (map2 (build_rel_app ctxt (Rs @ IRs) fpA_Ts) selA_ts selB_ts))]); fun mk_prem_concl n discA_ts selA_tss discB_ts selB_tss = Library.foldr1 HOLogic.mk_conj (flat (@{map 5} (mk_prem_ctr_concls n) @@ -1910,22 +1940,22 @@ end; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq - IRs (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts))); - val vars = Variable.add_free_names lthy goal []; + IRs (map2 (build_the_rel ctxt (Rs @ IRs) []) fpA_Ts fpB_Ts))); + val vars = Variable.add_free_names ctxt goal []; val rel_coinduct0_thm = - Goal.prove_sorry lthy vars prems goal (fn {context = ctxt, prems} => + Goal.prove_sorry ctxt vars prems goal (fn {context = ctxt, prems} => mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (Thm.cterm_of ctxt) IRs) prems (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars) (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses live_nesting_rel_eqs) |> Thm.close_derivation; in - (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm, + (postproc_co_induct ctxt nn @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm, mk_coinduct_attrs fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss) end; -fun derive_set_induct_thms_for_types lthy nn fpTs ctrss setss dtor_set_inducts exhausts set_pre_defs +fun derive_set_induct_thms_for_types ctxt nn fpTs ctrss setss dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses = let fun mk_prems A Ps ctr_args t ctxt = @@ -1994,9 +2024,9 @@ |>> apfst (apsnd (Library.foldr1 HOLogic.mk_conj)) |>> apsnd flat; - val vars = fold (Variable.add_free_names lthy) (concl :: prems) []; + val vars = fold (Variable.add_free_names ctxt) (concl :: prems) []; val thm = - Goal.prove_sorry lthy vars prems (HOLogic.mk_Trueprop concl) + Goal.prove_sorry ctxt vars prems (HOLogic.mk_Trueprop concl) (fn {context = ctxt, prems} => mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses) @@ -2009,7 +2039,7 @@ end val consumes_attr = Attrib.consumes 1; in - map (mk_thm lthy fpTs ctrss + map (mk_thm ctxt fpTs ctrss #> nn = 1 ? map_prod (fn thm => rotate_prems ~1 (thm RS bspec)) (cons consumes_attr)) (transpose setss) end; @@ -2033,9 +2063,9 @@ |> unfold_thms ctxt unfolds end; -fun derive_coinduct_thms_for_types strong alter_r pre_bnfs dtor_coinduct dtor_ctors +fun derive_coinduct_thms_for_types ctxt strong alter_r pre_bnfs dtor_coinduct dtor_ctors live_nesting_bnfs fpTs Xs ctrXs_Tsss ns pre_abs_inverses abs_inverses mk_vimage2p ctr_defss - (ctr_sugars : ctr_sugar list) ctxt = + (ctr_sugars : ctr_sugar list) = let val nn = length pre_bnfs; @@ -2069,38 +2099,15 @@ @{map 4} (fn u => fn v => fn uvr => fn uv_eq => fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; - fun build_the_rel rs' T Xs_T = - build_rel [] ctxt [] [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) - |> Term.subst_atomic_types (Xs ~~ fpTs); - - fun build_rel_app rs' usel vsel Xs_T = - fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T); - - fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels ctrXs_Ts = - (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @ - (if null usels then - [] - else - [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], - Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]); - - fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss = - flat (@{map 6} (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss) - |> Library.foldr1 HOLogic.mk_conj - handle List.Empty => @{term True}; - - fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = - fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, - HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss))); - val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (@{map 3} (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) - uvrs us vs)); + uvrs us vs)) fun mk_goal rs0' = - Logic.list_implies (@{map 9} (mk_prem (map alter_r rs0')) uvrs us vs ns udiscss uselsss - vdiscss vselsss ctrXs_Tsss, concl); + Logic.list_implies (@{map 9} (mk_coinduct_prem ctxt Xs fpTs (map alter_r rs0')) + uvrs us vs ns udiscss uselsss vdiscss vselsss ctrXs_Tsss, + concl); val goals = map mk_goal ([rs] @ (if strong then [strong_rs] else [])); @@ -2122,10 +2129,10 @@ dtor_coinducts goals end; -fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _)) - dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss - kss mss ns pre_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) - corecs corec_defs ctxt = +fun derive_coinduct_corecs_thms_for_types ctxt pre_bnfs + (x, cs, cpss, (((pgss, _, _, _), cqgsss), _)) dtor_coinduct dtor_injects dtor_ctors + dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns pre_abs_inverses abs_inverses + mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list) corecs corec_defs = let fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec = iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]]; @@ -2145,9 +2152,9 @@ val discIss = map #discIs ctr_sugars; val sel_thmsss = map #sel_thmss ctr_sugars; - val coinduct_thms_pairs = derive_coinduct_thms_for_types true I pre_bnfs dtor_coinduct + val coinduct_thms_pairs = derive_coinduct_thms_for_types ctxt true I pre_bnfs dtor_coinduct dtor_ctors live_nesting_bnfs fpTs Xs ctrXs_Tsss ns pre_abs_inverses abs_inverses mk_vimage2p - ctr_defss ctr_sugars ctxt; + ctr_defss ctr_sugars; fun mk_maybe_not pos = not pos ? HOLogic.mk_not; @@ -2786,9 +2793,9 @@ (coinduct_attrs, common_coinduct_attrs)), corec_thmss, corec_disc_thmss, (corec_disc_iff_thmss, corec_disc_iff_attrs), (corec_sel_thmsss, corec_sel_attrs)) = - derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct + derive_coinduct_corecs_thms_for_types lthy pre_bnfs (the corecs_args_types) xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss - ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs lthy; + ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs; fun distinct_prems ctxt thm = Goal.prove (*no sorry*) ctxt [] [] diff -r a42dbe9d2c1f -r a15785625f7c src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Dec 22 17:36:28 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Dec 22 19:14:58 2016 +0100 @@ -283,10 +283,10 @@ ([induct], [inducts], rec_thmss, replicate nn [], replicate nn [])) ||> (fn info => (SOME info, NONE)) else - derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) + derive_coinduct_corecs_thms_for_types lthy pre_bnfs (the corecs_args_types) xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses - (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs lthy + (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _, (corec_sel_thmsss, _)) => (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss, diff -r a42dbe9d2c1f -r a15785625f7c src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu Dec 22 17:36:28 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu Dec 22 19:14:58 2016 +0100 @@ -685,9 +685,9 @@ fun mk_applied_cong arg = enforce_type ctxt domain_type (fastype_of arg) cong0 $ arg; - val thm = derive_coinduct_thms_for_types false mk_applied_cong [pre_bnf] dtor_coinduct + val thm = derive_coinduct_thms_for_types ctxt false mk_applied_cong [pre_bnf] dtor_coinduct dtor_ctors live_nesting_bnfs [fpT] [substXAT X] [map (map substXAT) ctrXs_Tss] [n] - [abs_inverse] [abs_inverse] I [ctr_defs] [morph_ctr_sugar phi ctr_sugar0] ctxt + [abs_inverse] [abs_inverse] I [ctr_defs] [morph_ctr_sugar phi ctr_sugar0] |> map snd |> the_single; val (attrs, _) = mk_coinduct_attrs [fpT] [ctrs0] [discs0] [ms]; in