renamed "wrap_data" to "wrap_free_constructors"
authorblanchet
Thu Apr 25 18:27:26 2013 +0200 (2013-04-25)
changeset 517810504e286d66d
parent 51780 67e4ed510dfb
child 51782 84e7225f5ab6
renamed "wrap_data" to "wrap_free_constructors"
src/HOL/BNF/BNF_Wrap.thy
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_wrap.ML
     1.1 --- a/src/HOL/BNF/BNF_Wrap.thy	Thu Apr 25 18:14:04 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Wrap.thy	Thu Apr 25 18:27:26 2013 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  theory BNF_Wrap
     1.5  imports BNF_Util
     1.6  keywords
     1.7 -  "wrap_data" :: thy_goal and
     1.8 +  "wrap_free_constructors" :: thy_goal and
     1.9    "no_dests" and
    1.10    "rep_compat"
    1.11  begin
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 18:14:04 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 18:27:26 2013 +0200
     2.3 @@ -534,8 +534,8 @@
     2.4  
     2.5              val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
     2.6            in
     2.7 -            wrap_datatype tacss (((wrap_opts, ctrs0), casex0), (disc_bindings, (sel_bindingss,
     2.8 -              sel_defaultss))) lthy
     2.9 +            wrap_free_constructors tacss (((wrap_opts, ctrs0), casex0), (disc_bindings,
    2.10 +              (sel_bindingss, sel_defaultss))) lthy
    2.11            end;
    2.12  
    2.13          fun derive_maps_sets_rels (wrap_res, lthy) =
     3.1 --- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 25 18:14:04 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 25 18:27:26 2013 +0200
     3.3 @@ -18,7 +18,7 @@
     3.4    val name_of_ctr: term -> string
     3.5    val name_of_disc: term -> string
     3.6  
     3.7 -  val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     3.8 +  val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     3.9      (((bool * bool) * term list) * term) *
    3.10        (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    3.11      (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
    3.12 @@ -123,7 +123,7 @@
    3.13  
    3.14  fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    3.15  
    3.16 -fun prepare_wrap_datatype prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case),
    3.17 +fun prepare_wrap_free_constructors prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case),
    3.18      (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    3.19    let
    3.20      (* TODO: sanity checks on arguments *)
    3.21 @@ -673,13 +673,13 @@
    3.22      (goalss, after_qed, lthy')
    3.23    end;
    3.24  
    3.25 -fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) =>
    3.26 +fun wrap_free_constructors tacss = (fn (goalss, after_qed, lthy) =>
    3.27    map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
    3.28 -  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I);
    3.29 +  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_free_constructors (K I);
    3.30  
    3.31 -val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
    3.32 +val wrap_free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
    3.33    Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
    3.34 -  prepare_wrap_datatype Syntax.read_term;
    3.35 +  prepare_wrap_free_constructors Syntax.read_term;
    3.36  
    3.37  fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
    3.38  
    3.39 @@ -696,10 +696,11 @@
    3.40      >> (pairself (exists I) o split_list)) (false, false);
    3.41  
    3.42  val _ =
    3.43 -  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wrap an existing datatype"
    3.44 +  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
    3.45 +    "wrap an existing (co)datatype's constructors"
    3.46      ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
    3.47        Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
    3.48          Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
    3.49 -     >> wrap_datatype_cmd);
    3.50 +     >> wrap_free_constructors_cmd);
    3.51  
    3.52  end;