# HG changeset patch # User blanchet # Date 1367931781 -7200 # Node ID 9a27c870ee21b9b13493384d64d2d26a6d75b887 # Parent 1cf1fe22145d670f5453b845c06d58c59c619417 refactoring diff -r 1cf1fe22145d -r 9a27c870ee21 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue May 07 14:27:39 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue May 07 15:03:01 2013 +0200 @@ -35,7 +35,17 @@ int list list -> term list -> term list -> term list * term list val mk_unfolds_corecs: Proof.context -> typ list -> typ list -> typ list -> int list -> int list list -> term list -> term list -> term list * term list - + val define_fold_rec: term list list * typ list list * term list list list -> + term list list * typ list list * term list list list -> (string -> binding) -> typ list -> + typ list -> typ list -> term -> term -> Proof.context -> + (term * term * thm * thm) * local_theory + val define_unfold_corec: term list -> int list -> term list list -> + (term list list * term list list list list * term list list list list) + * (typ list * typ list list list * typ list list) -> + (term list list * term list list list list * term list list list list) + * (typ list * typ list list list * typ list list) -> + (string -> binding) -> typ list -> typ list -> typ list -> term -> term -> Proof.context -> + (term * term * thm * thm) * local_theory val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> term list list -> thm list list -> term list -> term list -> thm list -> thm list -> @@ -459,6 +469,75 @@ map2 mk_terms dtor_unfolds dtor_corecs |> split_list end; +fun define_fold_rec fold_only rec_only mk_binding fpTs As Cs ctor_fold ctor_rec no_defs_lthy = + let + val kk = find_index (curry (op =) (body_type (fastype_of ctor_fold))) Cs; + val fpT = nth fpTs kk; (* ### can use dummyT? or steal it from ctor_fold etc? *) + val C = nth Cs kk; + + fun generate_iter (suf, ctor_iter, (fss, f_Tss, xsss)) = + let + val res_T = fold_rev (curry (op --->)) f_Tss (fpT --> C); + val binding = mk_binding suf; + val spec = + mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)), + mk_iter_body no_defs_lthy fpTs ctor_iter fss xsss); + in (binding, spec) end; + + val binding_specs = + map generate_iter [(foldN, ctor_fold, fold_only), (recN, ctor_rec, rec_only)]; + + val ((csts, defs), (lthy', lthy)) = no_defs_lthy + |> apfst split_list o fold_map (fn (b, spec) => + Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) + #>> apsnd snd) binding_specs + ||> `Local_Theory.restore; + + val phi = Proof_Context.export_morphism lthy lthy'; + + val [fold_def, rec_def] = map (Morphism.thm phi) defs; + + val [foldx, recx] = map (mk_co_iter true As Cs o Morphism.term phi) csts; + in + ((foldx, recx, fold_def, rec_def), lthy') + end; + +fun define_unfold_corec cs ns cpss unfold_only corec_only mk_binding fpTs As Cs dtor_unfold + dtor_corec no_defs_lthy = + let + val kk = find_index (curry (op =) (body_type (fastype_of dtor_unfold))) fpTs; + val fpT = nth fpTs kk; (* ### can use dummyT? or steal it from ctor_fold etc? *) + val C = nth Cs kk; + + fun generate_coiter (suf, dtor_coiter, ((pfss, cqssss, cfssss), + (f_sum_prod_Ts, f_Tsss, pf_Tss))) = + let + val res_T = fold_rev (curry (op --->)) pf_Tss (C --> fpT); + val binding = mk_binding suf; + val spec = + mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)), + mk_coiter_body no_defs_lthy cs ns cpss f_sum_prod_Ts f_Tsss cqssss cfssss + dtor_coiter); + in (binding, spec) end; + + val binding_specs = + map generate_coiter [(unfoldN, dtor_unfold, unfold_only), (corecN, dtor_corec, corec_only)]; + + val ((csts, defs), (lthy', lthy)) = no_defs_lthy + |> apfst split_list o fold_map (fn (b, spec) => + Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) + #>> apsnd snd) binding_specs + ||> `Local_Theory.restore; + + val phi = Proof_Context.export_morphism lthy lthy'; + + val [unfold_def, corec_def] = map (Morphism.thm phi) defs; + + val [unfold, corec] = map (mk_co_iter false As Cs o Morphism.term phi) csts; + in + ((unfold, corec, unfold_def, corec_def), lthy') + end; + fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_folds0 ctor_recs0 ctor_induct ctor_fold_thms ctor_rec_thms nesting_bnfs nested_bnfs fpTs Cs As ctrss ctr_defss folds recs fold_defs rec_defs lthy = @@ -772,7 +851,6 @@ val crgsss = map2 (map2 (map2 (intr_coiters gunfolds))) crssss cgssss; val cshsss = map2 (map2 (map2 (intr_coiters hcorecs))) csssss chssss; -val _ = tracing ("*** cshsss1: " ^ PolyML.makestring cshsss) (*###*) val unfold_goalss = map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss; val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss; @@ -1115,7 +1193,7 @@ val ctrs = map (mk_ctr As) ctrs0; - fun wrap lthy = + fun wrap_ctrs lthy = let fun exhaust_tac {context = ctxt, prems = _} = let @@ -1245,72 +1323,16 @@ lthy |> Local_Theory.notes notes |> snd) end; - fun define_fold_rec no_defs_lthy = - let - fun generate_iter (suf, ctor_iter, (fss, f_Tss, xsss)) = - let - val res_T = fold_rev (curry (op --->)) f_Tss (fpT --> C); - val binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b); - val spec = - mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)), - mk_iter_body no_defs_lthy fpTs ctor_iter fss xsss); - in (binding, spec) end; - - val binding_specs = - map generate_iter [(foldN, fp_fold, fold_only), (recN, fp_rec, rec_only)]; - - val ((csts, defs), (lthy', lthy)) = no_defs_lthy - |> apfst split_list o fold_map (fn (b, spec) => - Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) - #>> apsnd snd) binding_specs - ||> `Local_Theory.restore; - - val phi = Proof_Context.export_morphism lthy lthy'; - - val [fold_def, rec_def] = map (Morphism.thm phi) defs; - - val [foldx, recx] = map (mk_co_iter lfp As Cs o Morphism.term phi) csts; - in - ((foldx, recx, fold_def, rec_def), lthy') - end; - - fun define_unfold_corec no_defs_lthy = - let - fun generate_coiter (suf, dtor_coiter, ((pfss, cqssss, cfssss), - (f_sum_prod_Ts, f_Tsss, pf_Tss))) = - let - val res_T = fold_rev (curry (op --->)) pf_Tss (C --> fpT); - val binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b); - val spec = - mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)), - mk_coiter_body no_defs_lthy cs ns cpss f_sum_prod_Ts f_Tsss cqssss cfssss - dtor_coiter); - in (binding, spec) end; - - val binding_specs = - map generate_coiter [(unfoldN, fp_fold, unfold_only), (corecN, fp_rec, corec_only)]; - - val ((csts, defs), (lthy', lthy)) = no_defs_lthy - |> apfst split_list o fold_map (fn (b, spec) => - Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) - #>> apsnd snd) binding_specs - ||> `Local_Theory.restore; - - val phi = Proof_Context.export_morphism lthy lthy'; - - val [unfold_def, corec_def] = map (Morphism.thm phi) defs; - - val [unfold, corec] = map (mk_co_iter lfp As Cs o Morphism.term phi) csts; - in - ((unfold, corec, unfold_def, corec_def), lthy') - end; + fun mk_binding suf = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b); fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) = (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy); in - (wrap + (wrap_ctrs #> derive_maps_sets_rels - ##>> (if lfp then define_fold_rec else define_unfold_corec) + ##>> (if lfp then define_fold_rec fold_only rec_only + else define_unfold_corec cs ns cpss unfold_only corec_only) + mk_binding fpTs As Cs fp_fold fp_rec #> massage_res, lthy') end;