renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
authorblanchet
Fri Feb 14 07:53:46 2014 +0100 (2014-02-14)
changeset 5546898b25c51e9e5
parent 55467 a5c9002bc54d
child 55469 b19dd108f0c2
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
src/Doc/Datatypes/Datatypes.thy
src/HOL/Ctr_Sugar.thy
src/HOL/Nat.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -119,7 +119,7 @@
     1.4  \item Section
     1.5  \ref{sec:deriving-destructors-and-theorems-for-free-constructors},
     1.6  ``Deriving Destructors and Theorems for Free Constructors,'' explains how to
     1.7 -use the command @{command wrap_free_constructors} to derive destructor constants
     1.8 +use the command @{command free_constructors} to derive destructor constants
     1.9  and theorems for freely generated types, as performed internally by @{command
    1.10  datatype_new} and @{command codatatype}.
    1.11  
    1.12 @@ -687,7 +687,7 @@
    1.13  
    1.14  \item The \emph{free constructor theorems} are properties about the constructors
    1.15  and destructors that can be derived for any freely generated type. Internally,
    1.16 -the derivation is performed by @{command wrap_free_constructors}.
    1.17 +the derivation is performed by @{command free_constructors}.
    1.18  
    1.19  \item The \emph{functorial theorems} are properties of datatypes related to
    1.20  their BNF nature.
    1.21 @@ -1016,8 +1016,8 @@
    1.22  with nested recursion through old-style datatypes, the old-style
    1.23  datatypes can be registered as a BNF
    1.24  (Section~\ref{sec:introducing-bounded-natural-functors}). If the goal is
    1.25 -to derive discriminators and selectors, this can be achieved using @{command
    1.26 -wrap_free_constructors}
    1.27 +to derive discriminators and selectors, this can be achieved using
    1.28 +@{command free_constructors}
    1.29  (Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
    1.30  *}
    1.31  
    1.32 @@ -2588,7 +2588,7 @@
    1.33  text {*
    1.34  The derivation of convenience theorems for types equipped with free constructors,
    1.35  as performed internally by @{command datatype_new} and @{command codatatype},
    1.36 -is available as a stand-alone command called @{command wrap_free_constructors}.
    1.37 +is available as a stand-alone command called @{command free_constructors}.
    1.38  
    1.39  %  * need for this is rare but may arise if you want e.g. to add destructors to
    1.40  %    a type not introduced by ...
    1.41 @@ -2596,7 +2596,7 @@
    1.42  %  * also useful for compatibility with old package, e.g. add destructors to
    1.43  %    old \keyw{datatype}
    1.44  %
    1.45 -%  * @{command wrap_free_constructors}
    1.46 +%  * @{command free_constructors}
    1.47  %    * @{text "no_discs_sels"}, @{text "no_code"}
    1.48  %    * hack to have both co and nonco view via locale (cf. ext nats)
    1.49  %  * code generator
    1.50 @@ -2619,11 +2619,11 @@
    1.51  
    1.52  text {*
    1.53  \begin{matharray}{rcl}
    1.54 -  @{command_def "wrap_free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
    1.55 +  @{command_def "free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
    1.56  \end{matharray}
    1.57  
    1.58  @{rail \<open>
    1.59 -  @@{command wrap_free_constructors} target? @{syntax dt_options} \<newline>
    1.60 +  @@{command free_constructors} target? @{syntax dt_options} \<newline>
    1.61      term_list name @{syntax wfc_discs_sels}?
    1.62    ;
    1.63    @{syntax_def wfc_discs_sels}: name_list (name_list_list name_term_list_list? )?
     2.1 --- a/src/HOL/Ctr_Sugar.thy	Fri Feb 14 07:53:46 2014 +0100
     2.2 +++ b/src/HOL/Ctr_Sugar.thy	Fri Feb 14 07:53:46 2014 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4  imports HOL
     2.5  keywords
     2.6    "print_case_translations" :: diag and
     2.7 -  "wrap_free_constructors" :: thy_goal
     2.8 +  "free_constructors" :: thy_goal
     2.9  begin
    2.10  
    2.11  consts
     3.1 --- a/src/HOL/Nat.thy	Fri Feb 14 07:53:46 2014 +0100
     3.2 +++ b/src/HOL/Nat.thy	Fri Feb 14 07:53:46 2014 +0100
     3.3 @@ -82,7 +82,7 @@
     3.4  apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
     3.5  done
     3.6  
     3.7 -wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
     3.8 +free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
     3.9    apply atomize_elim
    3.10    apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
    3.11   apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
    3.12 @@ -101,7 +101,7 @@
    3.13  
    3.14  setup {* Sign.parent_path *}
    3.15  
    3.16 --- {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
    3.17 +-- {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
    3.18  setup {* Sign.mandatory_path "nat" *}
    3.19  
    3.20  declare
     4.1 --- a/src/HOL/Product_Type.thy	Fri Feb 14 07:53:46 2014 +0100
     4.2 +++ b/src/HOL/Product_Type.thy	Fri Feb 14 07:53:46 2014 +0100
     4.3 @@ -12,7 +12,7 @@
     4.4  
     4.5  subsection {* @{typ bool} is a datatype *}
     4.6  
     4.7 -wrap_free_constructors [True, False] case_bool [=]
     4.8 +free_constructors [True, False] case_bool [=]
     4.9  by auto
    4.10  
    4.11  text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    4.12 @@ -23,7 +23,7 @@
    4.13  
    4.14  setup {* Sign.parent_path *}
    4.15  
    4.16 -text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
    4.17 +text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
    4.18  
    4.19  setup {* Sign.mandatory_path "bool" *}
    4.20  
    4.21 @@ -82,7 +82,7 @@
    4.22      else SOME (mk_meta_eq @{thm unit_eq})
    4.23  *}
    4.24  
    4.25 -wrap_free_constructors ["()"] case_unit
    4.26 +free_constructors ["()"] case_unit
    4.27  by auto
    4.28  
    4.29  text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    4.30 @@ -93,7 +93,7 @@
    4.31  
    4.32  setup {* Sign.parent_path *}
    4.33  
    4.34 -text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
    4.35 +text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
    4.36  
    4.37  setup {* Sign.mandatory_path "unit" *}
    4.38  
    4.39 @@ -184,7 +184,7 @@
    4.40  lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
    4.41    by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
    4.42  
    4.43 -wrap_free_constructors [Pair] case_prod [] [[fst, snd]]
    4.44 +free_constructors [Pair] case_prod [] [[fst, snd]]
    4.45  proof -
    4.46    fix P :: bool and p :: "'a \<times> 'b"
    4.47    show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P"
    4.48 @@ -208,7 +208,7 @@
    4.49  
    4.50  setup {* Sign.parent_path *}
    4.51  
    4.52 -text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
    4.53 +text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
    4.54  
    4.55  setup {* Sign.mandatory_path "prod" *}
    4.56  
     5.1 --- a/src/HOL/Sum_Type.thy	Fri Feb 14 07:53:46 2014 +0100
     5.2 +++ b/src/HOL/Sum_Type.thy	Fri Feb 14 07:53:46 2014 +0100
     5.3 @@ -85,7 +85,7 @@
     5.4    with assms show P by (auto simp add: sum_def Inl_def Inr_def)
     5.5  qed
     5.6  
     5.7 -wrap_free_constructors [Inl, Inr] case_sum [isl] [[projl], [projr]]
     5.8 +free_constructors [Inl, Inr] case_sum [isl] [[projl], [projr]]
     5.9  by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
    5.10  
    5.11  text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    5.12 @@ -102,7 +102,7 @@
    5.13  
    5.14  setup {* Sign.parent_path *}
    5.15  
    5.16 -text {* But erase the prefix for properties that are not generated by @{text wrap_free_constructors}. *}
    5.17 +text {* But erase the prefix for properties that are not generated by @{text free_constructors}. *}
    5.18  
    5.19  setup {* Sign.mandatory_path "sum" *}
    5.20  
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     6.3 @@ -1250,7 +1250,7 @@
     6.4  
     6.5              val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
     6.6            in
     6.7 -            wrap_free_constructors tacss (((wrap_opts, ctrs0), standard_binding), (disc_bindings,
     6.8 +            free_constructors tacss (((wrap_opts, ctrs0), standard_binding), (disc_bindings,
     6.9                (sel_bindingss, sel_defaultss))) lthy
    6.10            end;
    6.11  
    6.12 @@ -1527,7 +1527,7 @@
    6.13    parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
    6.14    Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
    6.15  
    6.16 -val parse_co_datatype = parse_wrap_free_constructors_options -- Parse.and_list1 parse_spec;
    6.17 +val parse_co_datatype = parse_free_constructors_options -- Parse.and_list1 parse_spec;
    6.18  
    6.19  fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
    6.20  
     7.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     7.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     7.3 @@ -53,11 +53,11 @@
     7.4    val dest_case: Proof.context -> string -> typ list -> term ->
     7.5      (ctr_sugar * term list * term list) option
     7.6  
     7.7 -  val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     7.8 +  val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     7.9      (((bool * bool) * term list) * binding) *
    7.10        (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    7.11      ctr_sugar * local_theory
    7.12 -  val parse_wrap_free_constructors_options: (bool * bool) parser
    7.13 +  val parse_free_constructors_options: (bool * bool) parser
    7.14    val parse_bound_term: (binding * string) parser
    7.15  end;
    7.16  
    7.17 @@ -278,8 +278,8 @@
    7.18  
    7.19  fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    7.20  
    7.21 -fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs),
    7.22 -    raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    7.23 +fun prepare_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs), raw_case_binding),
    7.24 +    (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    7.25    let
    7.26      (* TODO: sanity checks on arguments *)
    7.27  
    7.28 @@ -946,13 +946,13 @@
    7.29      (goalss, after_qed, lthy')
    7.30    end;
    7.31  
    7.32 -fun wrap_free_constructors tacss = (fn (goalss, after_qed, lthy) =>
    7.33 +fun free_constructors tacss = (fn (goalss, after_qed, lthy) =>
    7.34    map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
    7.35 -  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_free_constructors (K I);
    7.36 +  |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I);
    7.37  
    7.38 -val wrap_free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
    7.39 +val free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
    7.40    Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
    7.41 -  prepare_wrap_free_constructors Syntax.read_term;
    7.42 +  prepare_free_constructors Syntax.read_term;
    7.43  
    7.44  fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
    7.45  
    7.46 @@ -963,7 +963,7 @@
    7.47  val parse_bound_terms = parse_bracket_list parse_bound_term;
    7.48  val parse_bound_termss = parse_bracket_list parse_bound_terms;
    7.49  
    7.50 -val parse_wrap_free_constructors_options =
    7.51 +val parse_free_constructors_options =
    7.52    Scan.optional (@{keyword "("} |-- Parse.list1
    7.53          (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
    7.54        @{keyword ")"}
    7.55 @@ -971,12 +971,12 @@
    7.56      (false, false);
    7.57  
    7.58  val _ =
    7.59 -  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
    7.60 -    "wrap an existing freely generated type's constructors"
    7.61 -    ((parse_wrap_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
    7.62 +  Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
    7.63 +    "register an existing freely generated type's constructors"
    7.64 +    ((parse_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
    7.65          @{keyword "]"}) --
    7.66        parse_binding -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
    7.67          Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
    7.68 -     >> wrap_free_constructors_cmd);
    7.69 +     >> free_constructors_cmd);
    7.70  
    7.71  end;