# HG changeset patch # User blanchet # Date 1398241406 -7200 # Node ID 029997d3b5d88b62b152ef84e5582b924d26c1e7 # Parent 0a35354137a5e7abf48d2b111ecd6ae81a511110 reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec' diff -r 0a35354137a5 -r 029997d3b5d8 src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:26 2014 +0200 @@ -218,6 +218,9 @@ hide_fact (open) id_transfer +datatype_new 'a i = I 'a +thm i.size i.rec_o_map i.size_o_map + datatype_new ('a, 'b) j = J0 | J 'a "('a, 'b) j" thm j.size j.rec_o_map j.size_o_map @@ -249,11 +252,9 @@ thm w.size w.rec_o_map w.size_o_map (*TODO: -* deal with *unused* dead variables and other odd cases (e.g. recursion through fun) * what happens if recursion through arbitrary bnf, like 'fsize'? * by default * offer possibility to register size function and theorems -* non-recursive types use 'case' instead of 'rec', causes trouble (revert?) * compat with old size? * recursion of old through new (e.g. through list)? * recursion of new through old? diff -r 0a35354137a5 -r 029997d3b5d8 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:26 2014 +0200 @@ -75,7 +75,7 @@ typ list list * (typ list list list list * typ list list list * typ list list list list * typ list) val define_rec: - (typ list list * typ list list list list * term list list * term list list list list) option -> + typ list list * typ list list list list * term list list * term list list list list -> (string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context -> (term * thm) * Proof.context val define_corec: 'a * term list * term list list @@ -458,11 +458,8 @@ val ((recs_args_types, corecs_args_types), lthy') = if fp = Least_FP then - if nn = 1 andalso forall (forall (forall (not o exists_subtype_in fpTs))) ctr_Tsss then - ((NONE, NONE), lthy) - else - mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy - |>> (rpair NONE o SOME) + mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy + |>> (rpair NONE o SOME) else mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy |>> (pair NONE o SOME); @@ -497,20 +494,19 @@ ((cst', def'), lthy') end; -fun define_rec NONE _ _ _ _ _ = pair (Term.dummy, refl) - | define_rec (SOME (_, _, fss, xssss)) mk_binding fpTs Cs reps ctor_rec = - let - val nn = length fpTs; - val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec) - |>> map domain_type ||> domain_type; - in - define_co_rec Least_FP fpT Cs (mk_binding recN) - (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec, - map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss => - mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss) - (map flat_rec_arg_args xsss)) - ctor_rec_absTs reps fss xssss))) - end; +fun define_rec (_, _, fss, xssss) mk_binding fpTs Cs reps ctor_rec = + let + val nn = length fpTs; + val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec) + |>> map domain_type ||> domain_type; + in + define_co_rec Least_FP fpT Cs (mk_binding recN) + (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec, + map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss => + mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss) + (map flat_rec_arg_args xsss)) + ctor_rec_absTs reps fss xssss))) + end; fun define_corec (_, cs, cpss, ((pgss, cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec = let @@ -670,10 +666,7 @@ map2 (map2 prove) goalss tacss end; - val rec_thmss = - (case rec_args_typess of - SOME types => mk_rec_thmss types recs rec_defs ctor_rec_thms - | NONE => replicate nn []); + val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms; in ((induct_thms, induct_thm, [induct_case_names_attr]), (rec_thmss, code_nitpicksimp_attrs @ simp_attrs)) @@ -1312,7 +1305,7 @@ (wrap_ctrs #> derive_maps_sets_rels ##>> - (if fp = Least_FP then define_rec recs_args_types mk_binding fpTs Cs reps + (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec #> massage_res, lthy') end; @@ -1337,10 +1330,6 @@ val induct_type_attr = Attrib.internal o K o Induct.induct_type; - val (recs', rec_thmss') = - if is_some recs_args_types then (recs, rec_thmss) - else (map #casex ctr_sugars, map #case_thms ctr_sugars); - val simp_thmss = map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injects rel_distincts setss; @@ -1355,14 +1344,11 @@ |> massage_multi_notes; in lthy - |> (if is_some recs_args_types then - Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss) - else - I) + |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss) |> Local_Theory.notes (common_notes @ notes) |> snd |> register_as_fp_sugars Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res - ctrXs_Tsss ctr_defss ctr_sugars recs' mapss [induct_thm] (map single induct_thms) - rec_thmss' (replicate nn []) (replicate nn []) rel_injects + ctrXs_Tsss ctr_defss ctr_sugars recs mapss [induct_thm] (map single induct_thms) + rec_thmss (replicate nn []) (replicate nn []) rel_injects end; fun derive_note_coinduct_corecs_thms_for_types diff -r 0a35354137a5 -r 029997d3b5d8 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Apr 23 10:23:26 2014 +0200 @@ -247,7 +247,7 @@ val ((co_recs, co_rec_defs), lthy) = fold_map2 (fn b => - if fp = Least_FP then define_rec recs_args_types (mk_binding b) fpTs Cs reps + if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss) fp_bs xtor_co_recs lthy |>> split_list;