# HG changeset patch # User blanchet # Date 1346312866 -7200 # Node ID b2884253b421c1ecca2e44db4bbdbbc7c2e9a64d # Parent 66fc7fc2d49bcfce391e56f22ed1c702b01b08f7 renamed ML function for consistency diff -r 66fc7fc2d49b -r b2884253b421 src/HOL/Codatatype/Tools/bnf_comp.ML --- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Aug 30 09:47:46 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Aug 30 09:47:46 2012 +0200 @@ -261,7 +261,7 @@ (maps wit_thms_of_bnf inners); val (bnf', lthy') = - add_bnf const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) + bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) ((((b, comp_map), comp_sets), comp_bd), comp_wits) lthy; val outer_rel_Gr = rel_Gr_of_bnf outer RS sym; @@ -368,7 +368,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) + bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) ((((b, killN_map), killN_sets), Term.absdummy T killN_bd), killN_wits) lthy; val rel_Gr = rel_Gr_of_bnf bnf RS sym; @@ -473,7 +473,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) + bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) ((((b, liftN_map), liftN_sets), Term.absdummy T liftN_bd), liftN_wits) lthy; val liftN_rel_unfold_thm = @@ -561,7 +561,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) + bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) ((((b, permute_map), permute_sets), Term.absdummy T permute_bd), permute_wits) lthy; val permute_rel_unfold_thm = @@ -716,7 +716,7 @@ fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf)); - val (bnf', lthy') = add_bnf Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE + val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy; val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf'); diff -r 66fc7fc2d49b -r b2884253b421 src/HOL/Codatatype/Tools/bnf_def.ML --- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Aug 30 09:47:46 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Aug 30 09:47:46 2012 +0200 @@ -81,14 +81,14 @@ val user_policy: Proof.context -> fact_policy val print_bnfs: Proof.context -> unit - val add_bnf: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> + val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> ({prems: thm list, context: Proof.context} -> tactic) list -> ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> (((binding * term) * term list) * term) * term list -> local_theory -> BNF * local_theory val filter_refl: thm list -> thm list - val add_bnf_cmd: (((binding * string) * string list) * string) * string list -> local_theory -> + val bnf_def_cmd: (((binding * string) * string list) * string) * string list -> local_theory -> Proof.state end; @@ -708,8 +708,7 @@ val goal_map_id = let - val bnf_map_app_id = Term.list_comb - (bnf_map_AsAs, map HOLogic.id_const As'); + val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As'); in HOLogic.mk_Trueprop (HOLogic.mk_eq (bnf_map_app_id, HOLogic.id_const CA')) @@ -717,8 +716,7 @@ val goal_map_comp = let - val bnf_map_app_comp = Term.list_comb - (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs); + val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs); val comp_bnf_map_app = HOLogic.mk_comp (Term.list_comb (bnf_map_BsCs, gs), Term.list_comb (bnf_map_AsBs, fs)); @@ -1155,7 +1153,7 @@ (goals, wit_goalss, after_qed, lthy', one_step_defs) end; -fun add_bnf const_policy fact_policy qualify tacs wit_tac Ds = +fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds = (fn (goals, wit_goalss, after_qed, lthy, defs) => let val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' unfold_defs_tac lthy defs wit_tac; @@ -1172,7 +1170,7 @@ end) oo prepare_bnf const_policy fact_policy qualify (fn ctxt => singleton (Type_Infer_Context.infer_types ctxt)) Ds; -val add_bnf_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) => +val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) => Proof.unfolding ([[(defs, [])]]) (Proof.theorem NONE (snd oo after_qed) (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo @@ -1211,6 +1209,6 @@ Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type" (((Parse.binding --| Parse.$$$ "=") -- Parse.term -- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term -- - (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]")) >> add_bnf_cmd); + (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]")) >> bnf_def_cmd); end; diff -r 66fc7fc2d49b -r b2884253b421 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Aug 30 09:47:46 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Aug 30 09:47:46 2012 +0200 @@ -2630,7 +2630,7 @@ val (Jbnfs, lthy) = fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => - add_bnf Dont_Inline user_policy I tacs wit_tac (SOME deads) + bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads) ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits)) tacss bs fs_maps setss_by_bnf Ts fld_witss lthy; diff -r 66fc7fc2d49b -r b2884253b421 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Aug 30 09:47:46 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Aug 30 09:47:46 2012 +0200 @@ -1661,7 +1661,7 @@ val (Ibnfs, lthy) = fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => - add_bnf Dont_Inline user_policy I tacs wit_tac (SOME deads) + bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads) ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits)) tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;