--- 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');
--- 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;
--- 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;
--- 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;