renamed ML function for consistency
authorblanchet
Thu Aug 30 09:47:46 2012 +0200 (2012-08-30)
changeset 49018b2884253b421
parent 49017 66fc7fc2d49b
child 49019 fc4decdba5ce
renamed ML function for consistency
src/HOL/Codatatype/Tools/bnf_comp.ML
src/HOL/Codatatype/Tools/bnf_def.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Aug 30 09:47:46 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Aug 30 09:47:46 2012 +0200
     1.3 @@ -261,7 +261,7 @@
     1.4          (maps wit_thms_of_bnf inners);
     1.5  
     1.6      val (bnf', lthy') =
     1.7 -      add_bnf const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
     1.8 +      bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
     1.9          ((((b, comp_map), comp_sets), comp_bd), comp_wits) lthy;
    1.10  
    1.11      val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
    1.12 @@ -368,7 +368,7 @@
    1.13      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.14  
    1.15      val (bnf', lthy') =
    1.16 -      add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
    1.17 +      bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
    1.18          ((((b, killN_map), killN_sets), Term.absdummy T killN_bd), killN_wits) lthy;
    1.19  
    1.20      val rel_Gr = rel_Gr_of_bnf bnf RS sym;
    1.21 @@ -473,7 +473,7 @@
    1.22      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.23  
    1.24      val (bnf', lthy') =
    1.25 -      add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
    1.26 +      bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
    1.27          ((((b, liftN_map), liftN_sets), Term.absdummy T liftN_bd), liftN_wits) lthy;
    1.28  
    1.29      val liftN_rel_unfold_thm =
    1.30 @@ -561,7 +561,7 @@
    1.31      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.32  
    1.33      val (bnf', lthy') =
    1.34 -      add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
    1.35 +      bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
    1.36          ((((b, permute_map), permute_sets), Term.absdummy T permute_bd), permute_wits) lthy;
    1.37  
    1.38      val permute_rel_unfold_thm =
    1.39 @@ -716,7 +716,7 @@
    1.40  
    1.41      fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
    1.42  
    1.43 -    val (bnf', lthy') = add_bnf Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE
    1.44 +    val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE
    1.45          ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
    1.46  
    1.47      val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Aug 30 09:47:46 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Aug 30 09:47:46 2012 +0200
     2.3 @@ -81,14 +81,14 @@
     2.4    val user_policy: Proof.context -> fact_policy
     2.5  
     2.6    val print_bnfs: Proof.context -> unit
     2.7 -  val add_bnf: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
     2.8 +  val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
     2.9      ({prems: thm list, context: Proof.context} -> tactic) list ->
    2.10      ({prems: thm list, context: Proof.context} -> tactic) -> typ list option ->
    2.11      (((binding * term) * term list) * term) * term list -> local_theory ->
    2.12      BNF * local_theory
    2.13  
    2.14    val filter_refl: thm list -> thm list
    2.15 -  val add_bnf_cmd: (((binding * string) * string list) * string) * string list -> local_theory ->
    2.16 +  val bnf_def_cmd: (((binding * string) * string list) * string) * string list -> local_theory ->
    2.17      Proof.state
    2.18  end;
    2.19  
    2.20 @@ -708,8 +708,7 @@
    2.21  
    2.22      val goal_map_id =
    2.23        let
    2.24 -        val bnf_map_app_id = Term.list_comb
    2.25 -          (bnf_map_AsAs, map HOLogic.id_const As');
    2.26 +        val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As');
    2.27        in
    2.28          HOLogic.mk_Trueprop
    2.29            (HOLogic.mk_eq (bnf_map_app_id, HOLogic.id_const CA'))
    2.30 @@ -717,8 +716,7 @@
    2.31  
    2.32      val goal_map_comp =
    2.33        let
    2.34 -        val bnf_map_app_comp = Term.list_comb
    2.35 -          (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs);
    2.36 +        val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs);
    2.37          val comp_bnf_map_app = HOLogic.mk_comp
    2.38            (Term.list_comb (bnf_map_BsCs, gs),
    2.39             Term.list_comb (bnf_map_AsBs, fs));
    2.40 @@ -1155,7 +1153,7 @@
    2.41      (goals, wit_goalss, after_qed, lthy', one_step_defs)
    2.42    end;
    2.43  
    2.44 -fun add_bnf const_policy fact_policy qualify tacs wit_tac Ds =
    2.45 +fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
    2.46    (fn (goals, wit_goalss, after_qed, lthy, defs) =>
    2.47    let
    2.48      val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' unfold_defs_tac lthy defs wit_tac;
    2.49 @@ -1172,7 +1170,7 @@
    2.50    end) oo prepare_bnf const_policy fact_policy qualify
    2.51    (fn ctxt => singleton (Type_Infer_Context.infer_types ctxt)) Ds;
    2.52  
    2.53 -val add_bnf_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
    2.54 +val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
    2.55    Proof.unfolding ([[(defs, [])]])
    2.56      (Proof.theorem NONE (snd oo after_qed)
    2.57        (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
    2.58 @@ -1211,6 +1209,6 @@
    2.59    Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
    2.60      (((Parse.binding --| Parse.$$$ "=") -- Parse.term --
    2.61         (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term --
    2.62 -       (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]")) >> add_bnf_cmd);
    2.63 +       (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]")) >> bnf_def_cmd);
    2.64  
    2.65  end;
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 09:47:46 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 09:47:46 2012 +0200
     3.3 @@ -2630,7 +2630,7 @@
     3.4  
     3.5          val (Jbnfs, lthy) =
     3.6            fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits =>
     3.7 -            add_bnf Dont_Inline user_policy I tacs wit_tac (SOME deads)
     3.8 +            bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads)
     3.9                ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits))
    3.10            tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;
    3.11  
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Aug 30 09:47:46 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Aug 30 09:47:46 2012 +0200
     4.3 @@ -1661,7 +1661,7 @@
     4.4  
     4.5          val (Ibnfs, lthy) =
     4.6            fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits =>
     4.7 -            add_bnf Dont_Inline user_policy I tacs wit_tac (SOME deads)
     4.8 +            bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads)
     4.9                ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits))
    4.10            tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;
    4.11