--- a/etc/isar-keywords.el Mon Dec 02 19:49:34 2013 +0100
+++ b/etc/isar-keywords.el Tue Dec 03 02:51:20 2013 +0100
@@ -344,7 +344,6 @@
"module_name"
"monos"
"morphisms"
- "no_discs_sels"
"notes"
"obtains"
"open"
@@ -353,7 +352,6 @@
"parametric"
"permissive"
"pervasive"
- "rep_compat"
"shows"
"structure"
"type_class"
--- a/src/Doc/Datatypes/Datatypes.thy Mon Dec 02 19:49:34 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Dec 03 02:51:20 2013 +0100
@@ -460,7 +460,7 @@
@@{command datatype_new} target? @{syntax dt_options}? \\
(@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
;
- @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
+ @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
"}
The syntactic entity \synt{target} can be used to specify a local
@@ -477,6 +477,10 @@
should be generated.
\item
+The @{text "no_code"} option indicates that the datatype should not be
+registered for code generation.
+
+\item
The @{text "rep_compat"} option indicates that the generated names should
contain optional (and normally not displayed) ``@{text "new."}'' components to
prevent clashes with a later call to \keyw{rep\_datatype}. See
@@ -704,8 +708,9 @@
(*>*)
text {*
-The first subgroup of properties is concerned with the constructors.
-They are listed below for @{typ "'a list"}:
+The free constructor theorems are partitioned in three subgroups. The first
+subgroup of properties is concerned with the constructors. They are listed below
+for @{typ "'a list"}:
\begin{indentblock}
\begin{description}
@@ -767,7 +772,7 @@
\end{indentblock}
\noindent
-The third and last subgroup revolves around discriminators and selectors:
+The third subgroup revolves around discriminators and selectors:
\begin{indentblock}
\begin{description}
@@ -826,7 +831,9 @@
\label{sssec:functorial-theorems} *}
text {*
-The BNF-related theorem are as follows:
+The functorial theorems are partitioned in two subgroups. The first subgroup
+consists of properties involving the constructors and either a set function, the
+map function, or the relator:
\begin{indentblock}
\begin{description}
@@ -853,6 +860,42 @@
\noindent
In addition, equational versions of @{text t.rel_inject} and @{text
rel_distinct} are registered with the @{text "[code]"} attribute.
+
+The second subgroup consists of more abstract properties of the set functions,
+the map function, and the relator:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\
+@{thm list.map_cong0[no_vars]}
+
+\item[@{text "t."}\hthm{map\_cong} @{text "[fundef_cong]"}\rm:] ~ \\
+@{thm list.map_cong[no_vars]}
+
+\item[@{text "t."}\hthm{map\_id}\rm:] ~ \\
+@{thm list.map_id[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_compp}\rm:] ~ \\
+@{thm list.rel_compp[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_conversep}\rm:] ~ \\
+@{thm list.rel_conversep[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_eq}\rm:] ~ \\
+@{thm list.rel_eq[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_flip}\rm:] ~ \\
+@{thm list.rel_flip[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_mono}\rm:] ~ \\
+@{thm list.rel_mono[no_vars]}
+
+\item[@{text "t."}\hthm{set\_map}\rm:] ~ \\
+@{thm list.set_map[no_vars]}
+
+\end{description}
+\end{indentblock}
*}
@@ -2348,8 +2391,10 @@
% old \keyw{datatype}
%
% * @{command wrap_free_constructors}
-% * @{text "no_discs_sels"}, @{text "rep_compat"}
+% * @{text "no_discs_sels"}, @{text "no_code"}, @{text "rep_compat"}
% * hack to have both co and nonco view via locale (cf. ext nats)
+% * code generator
+% * eq, refl, simps
*}
@@ -2382,9 +2427,7 @@
X_list: '[' (X + ',') ']'
"}
-% options: no_discs_sels rep_compat
-
-% X_list is as for BNF
+% options: no_discs_sels no_code rep_compat
\noindent
Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Mon Dec 02 19:49:34 2013 +0100
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Tue Dec 03 02:51:20 2013 +0100
@@ -11,8 +11,6 @@
imports Prelim
begin
-hide_fact (open) Lifting_Product.prod_rel_def
-
typedecl N
typedecl T
--- a/src/HOL/BNF/Tools/bnf_def.ML Mon Dec 02 19:49:34 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML Tue Dec 03 02:51:20 2013 +0100
@@ -125,7 +125,7 @@
open BNF_Tactics
open BNF_Def_Tactics
-val fundef_cong_attrs = @{attributes [fundef_cong]};
+val fundefcong_attrs = @{attributes [fundef_cong]};
type axioms = {
map_id0: thm,
@@ -579,8 +579,8 @@
val rel_conversepN = "rel_conversep";
val rel_monoN = "rel_mono"
val rel_mono_strongN = "rel_mono_strong"
-val rel_OON = "rel_compp";
-val rel_OO_GrpN = "rel_compp_Grp";
+val rel_comppN = "rel_compp";
+val rel_compp_GrpN = "rel_compp_Grp";
datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
@@ -636,16 +636,16 @@
val notes =
[(map_compN, [Lazy.force (#map_comp facts)], []),
(map_cong0N, [#map_cong0 axioms], []),
- (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs),
+ (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
(map_idN, [Lazy.force (#map_id facts)], []),
+ (rel_comppN, [Lazy.force (#rel_OO facts)], []),
+ (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
+ (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
(rel_eqN, [Lazy.force (#rel_eq facts)], []),
(rel_flipN, [Lazy.force (#rel_flip facts)], []),
- (set_mapN, map Lazy.force (#set_map facts), []),
- (rel_OO_GrpN, no_refl [#rel_OO_Grp axioms], []),
(rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
- (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
(rel_monoN, [Lazy.force (#rel_mono facts)], []),
- (rel_OON, [Lazy.force (#rel_OO facts)], [])]
+ (set_mapN, map Lazy.force (#set_map facts), [])]
|> filter_out (null o #2)
|> map (fn (thmN, thms, attrs) =>
((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)),
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Dec 02 19:49:34 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Dec 03 02:51:20 2013 +0100
@@ -95,8 +95,8 @@
val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
- (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
- ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
+ (bool * (bool * bool)) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
+ * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
mixfix) list) list ->
local_theory -> local_theory
val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
@@ -505,18 +505,12 @@
((xtor_co_iterss, iters_args_types, coiters_args_types), lthy')
end;
-fun mk_iter_body ctor_iter fss xssss =
- Term.list_comb (ctor_iter, map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss);
-
fun mk_preds_getterss_join c cps sum_prod_T cqfss =
let val n = length cqfss in
Term.lambda c (mk_IfN sum_prod_T cps
(map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)))
end;
-fun mk_coiter_body cs cpss f_sum_prod_Ts cqfsss dtor_coiter =
- Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss);
-
fun define_co_iters fp fpT Cs binding_specs lthy0 =
let
val thy = Proof_Context.theory_of lthy0;
@@ -525,8 +519,8 @@
#> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
val ((csts, defs), (lthy', lthy)) = lthy0
- |> apfst split_list o fold_map (fn (b, spec) =>
- Specification.definition (SOME (b, NONE, NoSyn), ((maybe_conceal_def_binding b, []), spec))
+ |> apfst split_list o fold_map (fn (b, rhs) =>
+ Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
#>> apsnd snd) binding_specs
||> `Local_Theory.restore;
@@ -544,14 +538,10 @@
val fpT_to_C as Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of (hd ctor_iters)));
- fun generate_iter pre (f_Tss, _, fss, xssss) ctor_iter =
- let
- val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
- val b = mk_binding pre;
- val spec =
- mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of b, res_T)),
- mk_iter_body ctor_iter fss xssss);
- in (b, spec) end;
+ fun generate_iter pre (_, _, fss, xssss) ctor_iter =
+ (mk_binding pre,
+ fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter,
+ map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss)));
in
define_co_iters Least_FP fpT Cs (map3 generate_iter iterNs iter_args_typess' ctor_iters) lthy
end;
@@ -564,13 +554,9 @@
val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
fun generate_coiter pre ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter =
- let
- val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
- val b = mk_binding pre;
- val spec =
- mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)),
- mk_coiter_body cs cpss f_sum_prod_Ts cqfsss dtor_coiter);
- in (b, spec) end;
+ (mk_binding pre,
+ fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_coiter,
+ map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss)));
in
define_co_iters Greatest_FP fpT Cs
(map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy
@@ -989,7 +975,7 @@
end;
fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
- (wrap_opts as (no_discs_sels, rep_compat), specs) no_defs_lthy0 =
+ (wrap_opts as (no_discs_sels, (_, rep_compat)), specs) no_defs_lthy0 =
let
(* TODO: sanity checks on arguments *)
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Dec 02 19:49:34 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Tue Dec 03 02:51:20 2013 +0100
@@ -28,7 +28,8 @@
structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
struct
-fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
+fun indexe _ h = (h, h + 1);
+fun indexed xs = fold_map indexe xs;
fun indexedd xss = fold_map indexed xss;
fun indexeddd xsss = fold_map indexedd xsss;
fun indexedddd xssss = fold_map indexeddd xssss;
--- a/src/HOL/Ctr_Sugar.thy Mon Dec 02 19:49:34 2013 +0100
+++ b/src/HOL/Ctr_Sugar.thy Tue Dec 03 02:51:20 2013 +0100
@@ -11,9 +11,7 @@
imports HOL
keywords
"print_case_translations" :: diag and
- "wrap_free_constructors" :: thy_goal and
- "no_discs_sels" and
- "rep_compat"
+ "wrap_free_constructors" :: thy_goal
begin
consts
@@ -40,6 +38,7 @@
ML_file "Tools/ctr_sugar_util.ML"
ML_file "Tools/ctr_sugar_tactics.ML"
+ML_file "Tools/ctr_sugar_code.ML"
ML_file "Tools/ctr_sugar.ML"
end
--- a/src/HOL/Inductive.thy Mon Dec 02 19:49:34 2013 +0100
+++ b/src/HOL/Inductive.thy Tue Dec 03 02:51:20 2013 +0100
@@ -274,7 +274,7 @@
ML_file "Tools/Datatype/datatype_prop.ML"
ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
ML_file "Tools/Datatype/rep_datatype.ML"
-ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
+ML_file "Tools/Datatype/datatype_codegen.ML"
ML_file "Tools/Datatype/primrec.ML"
text{* Lambda-abstractions with pattern matching: *}
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Dec 02 19:49:34 2013 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Dec 03 02:51:20 2013 +0100
@@ -6,152 +6,24 @@
signature DATATYPE_CODEGEN =
sig
- val setup: theory -> theory
end;
structure Datatype_Codegen : DATATYPE_CODEGEN =
struct
-(** generic code generator **)
-
-(* liberal addition of code data for datatypes *)
-
-fun mk_constr_consts thy vs tyco cos =
- let
- val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
- val cs' = map (fn c_ty as (_, ty) => (Axclass.unoverload_const thy c_ty, ty)) cs;
- in
- if is_some (try (Code.constrset_of_consts thy) cs')
- then SOME cs
- else NONE
- end;
-
-
-(* case certificates *)
-
-fun mk_case_cert thy tyco =
+fun add_code_for_datatype fcT_name thy =
let
- val raw_thms = #case_rewrites (Datatype_Data.the_info thy tyco);
- val thms as hd_thm :: _ = raw_thms
- |> Conjunction.intr_balanced
- |> Thm.unvarify_global
- |> Conjunction.elim_balanced (length raw_thms)
- |> map Simpdata.mk_meta_eq
- |> map Drule.zero_var_indexes;
- val params = fold_aterms (fn (Free (v, _)) => insert (op =) v | _ => I) (Thm.prop_of hd_thm) [];
- val rhs = hd_thm
- |> Thm.prop_of
- |> Logic.dest_equals
- |> fst
- |> Term.strip_comb
- |> apsnd (fst o split_last)
- |> list_comb;
- val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
- val asm = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs));
+ val (As', ctr_specs) = Datatype_Data.the_spec thy fcT_name;
+ val {inject = inject_thms, distinct = distinct_thms, case_rewrites = case_thms, ...} =
+ Datatype_Data.the_info thy fcT_name;
+
+ val As = map TFree As';
+ val fcT = Type (fcT_name, As);
+ val ctrs = map (fn (c, arg_Ts) => (c, arg_Ts ---> fcT)) ctr_specs;
in
- thms
- |> Conjunction.intr_balanced
- |> rewrite_rule [Thm.symmetric (Thm.assume asm)]
- |> Thm.implies_intr asm
- |> Thm.generalize ([], params) 0
- |> Axclass.unoverload thy
- |> Thm.varifyT_global
+ Ctr_Sugar_Code.add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy
end;
-
-(* equality *)
-
-fun mk_eq_eqns thy tyco =
- let
- val (vs, cos) = Datatype_Data.the_spec thy tyco;
- val {descr, index, inject = inject_thms, distinct = distinct_thms, ...} =
- Datatype_Data.the_info thy tyco;
- val ty = Type (tyco, map TFree vs);
- fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT) $ t1 $ t2;
- fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term True});
- fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term False});
- val triv_injects =
- map_filter
- (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
- | _ => NONE) cos;
- fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
- trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
- val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index);
- fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
- [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
- val distincts = maps prep_distinct (nth (Datatype_Prop.make_distincts [descr]) index);
- val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
- val simp_ctxt =
- Simplifier.global_context thy HOL_basic_ss
- addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms));
- fun prove prop =
- Goal.prove_sorry_global thy [] [] prop (K (ALLGOALS (simp_tac simp_ctxt)))
- |> Simpdata.mk_eq;
- in (map prove (triv_injects @ injects @ distincts), prove refl) end;
-
-fun add_equality vs tycos thy =
- let
- fun add_def tyco lthy =
- let
- val ty = Type (tyco, map TFree vs);
- fun mk_side const_name =
- Const (const_name, ty --> ty --> HOLogic.boolT) $ Free ("x", ty) $ Free ("y", ty);
- val def =
- HOLogic.mk_Trueprop (HOLogic.mk_eq
- (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq}));
- val def' = Syntax.check_term lthy def;
- val ((_, (_, thm)), lthy') =
- Specification.definition (NONE, (Attrib.empty_binding, def')) lthy;
- val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy);
- val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
- in (thm', lthy') end;
- fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
- fun prefix tyco =
- Binding.qualify true (Long_Name.base_name tyco) o Binding.qualify true "eq" o Binding.name;
- fun add_eq_thms tyco =
- `(fn thy => mk_eq_eqns thy tyco)
- #-> (fn (thms, thm) =>
- Global_Theory.note_thmss Thm.lemmaK
- [((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
- ((prefix tyco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
- #> snd;
- in
- thy
- |> Class.instantiation (tycos, vs, [HOLogic.class_equal])
- |> fold_map add_def tycos
- |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
- (fn _ => fn def_thms => tac def_thms) def_thms)
- |-> (fn def_thms => fold Code.del_eqn def_thms)
- |> fold add_eq_thms tycos
- end;
-
-
-(* register a datatype etc. *)
-
-fun add_all_code config tycos thy =
- let
- val (vs :: _, coss) = split_list (map (Datatype_Data.the_spec thy) tycos);
- val any_css = map2 (mk_constr_consts thy vs) tycos coss;
- val css = if exists is_none any_css then [] else map_filter I any_css;
- val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos;
- val certs = map (mk_case_cert thy) tycos;
- val tycos_eq =
- filter_out
- (fn tyco => Sorts.has_instance (Sign.classes_of thy) tyco [HOLogic.class_equal]) tycos;
- in
- if null css then thy
- else
- thy
- |> tap (fn _ => Datatype_Aux.message config "Registering datatype for code generator ...")
- |> fold Code.add_datatype css
- |> fold_rev Code.add_default_eqn case_rewrites
- |> fold Code.add_case certs
- |> not (null tycos_eq) ? add_equality vs tycos_eq
- end;
-
-
-(** theory setup **)
-
-val setup = Datatype_Data.interpretation add_all_code;
+val _ = Theory.setup (Datatype_Data.interpretation (K (fold add_code_for_datatype)));
end;
--- a/src/HOL/Tools/ctr_sugar.ML Mon Dec 02 19:49:34 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML Tue Dec 03 02:51:20 2013 +0100
@@ -54,10 +54,10 @@
val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
- (((bool * bool) * term list) * binding) *
+ (((bool * (bool * bool)) * term list) * binding) *
(binding list * (binding list list * (binding * term) list list)) -> local_theory ->
ctr_sugar * local_theory
- val parse_wrap_free_constructors_options: (bool * bool) parser
+ val parse_wrap_free_constructors_options: (bool * (bool * bool)) parser
val parse_bound_term: (binding * string) parser
end;
@@ -66,6 +66,7 @@
open Ctr_Sugar_Util
open Ctr_Sugar_Tactics
+open Ctr_Sugar_Code
type ctr_sugar =
{ctrs: term list,
@@ -285,7 +286,7 @@
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
-fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, rep_compat), raw_ctrs),
+fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, (no_code, rep_compat)), raw_ctrs),
raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
let
(* TODO: sanity checks on arguments *)
@@ -447,8 +448,6 @@
let
fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
- fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
-
fun alternate_disc k =
Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
@@ -461,7 +460,7 @@
| SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term lthy)
| SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
- fun sel_spec b proto_sels =
+ fun sel_rhs b proto_sels =
let
val _ =
(case duplicates (op =) (map fst proto_sels) of
@@ -476,8 +475,7 @@
quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. "
^ quote (Syntax.string_of_typ lthy T')));
in
- mk_Trueprop_eq (Free (Binding.name_of b, fcT --> T) $ u,
- Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
+ Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T)
end;
val sel_bindings = flat sel_bindingss;
@@ -500,18 +498,18 @@
val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
lthy
|> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b =>
- if Binding.is_empty b then
- if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
- else pair (alternate_disc k, alternate_disc_no_def)
- else if Binding.eq_name (b, equal_binding) then
- pair (Term.lambda u exist_xs_u_eq_ctr, refl)
- else
- Specification.definition (SOME (b, NONE, NoSyn),
- ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
- ks exist_xs_u_eq_ctrs disc_bindings
+ let val rhs = Term.lambda u exist_xs_u_eq_ctr in
+ if Binding.is_empty b then
+ if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
+ else pair (alternate_disc k, alternate_disc_no_def)
+ else if Binding.eq_name (b, equal_binding) then
+ pair (rhs, Thm.reflexive (certify lthy rhs))
+ else
+ Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) #>> apsnd snd
+ end) ks exist_xs_u_eq_ctrs disc_bindings
||>> apfst split_list o fold_map (fn (b, proto_sels) =>
- Specification.definition (SOME (b, NONE, NoSyn),
- ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
+ Local_Theory.define ((b, NoSyn),
+ ((Thm.def_binding b, []), sel_rhs b proto_sels)) #>> apsnd snd) sel_infos
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy lthy';
@@ -670,9 +668,11 @@
val vdiscs = map (rapp v) discs;
val vselss = map (map (rapp v)) selss;
+ fun massage_dest_def def = def RS meta_eq_to_obj_eq RS fun_cong;
+
fun make_sel_thm xs' case_thm sel_def =
zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
- (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
+ (Drule.forall_intr_vars (case_thm RS (massage_dest_def sel_def RS trans)))));
val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
@@ -706,7 +706,7 @@
nth exist_xs_u_eq_ctrs (k - 1));
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
+ mk_alternate_disc_def_tac ctxt k (massage_dest_def (nth disc_defs (2 - k)))
(nth distinct_thms (2 - k)) uexhaust_thm)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy)
@@ -719,7 +719,7 @@
map2 (fn k => fn def =>
if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def ()
else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k
- else def) ks disc_defs;
+ else massage_dest_def def) ks disc_defs;
val discD_thms = map (fn def => def RS iffD1) disc_defs';
val discI_thms =
@@ -926,11 +926,14 @@
(ctr_sugar,
lthy
|> not rep_compat ?
- (Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Case_Translation.register
- (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
+ Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Case_Translation.register
+ (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
|> Local_Theory.notes (anonymous_notes @ notes) |> snd
- |> register_ctr_sugar fcT_name ctr_sugar)
+ |> register_ctr_sugar fcT_name ctr_sugar
+ |> (not no_code andalso null (Thm.hyps_of (hd case_thms)))
+ ? Local_Theory.background_theory
+ (add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms case_thms))
end;
in
(goalss, after_qed, lthy')
@@ -954,9 +957,11 @@
val parse_bound_termss = parse_bracket_list parse_bound_terms;
val parse_wrap_free_constructors_options =
- Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_discs_sels"} >> K (true, false)) ||
- (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"}
- >> (pairself (exists I) o split_list)) (false, false);
+ Scan.optional (@{keyword "("} |-- Parse.list1
+ (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1 ||
+ Parse.reserved "rep_compat" >> K 2) --| @{keyword ")"}
+ >> (fn js => (member (op =) js 0, (member (op =) js 1, member (op =) js 2))))
+ (false, (false, false));
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ctr_sugar_code.ML Tue Dec 03 02:51:20 2013 +0100
@@ -0,0 +1,129 @@
+(* Title: HOL/Tools/ctr_sugar_code.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Dmitriy Traytel, TU Muenchen
+ Author: Stefan Berghofer, TU Muenchen
+ Author: Florian Haftmann, TU Muenchen
+ Copyright 2001-2013
+
+Code generation for freely generated types.
+*)
+
+signature CTR_SUGAR_CODE =
+sig
+ val add_ctr_code: string -> typ list -> (string * typ) list -> thm list -> thm list -> thm list ->
+ theory -> theory
+end;
+
+structure Ctr_Sugar_Code : CTR_SUGAR_CODE =
+struct
+
+open Ctr_Sugar_Util
+
+val eqN = "eq"
+val reflN = "refl"
+val simpsN = "simps"
+
+fun mk_case_certificate thy raw_thms =
+ let
+ val thms as thm1 :: _ = raw_thms
+ |> Conjunction.intr_balanced
+ |> Thm.unvarify_global
+ |> Conjunction.elim_balanced (length raw_thms)
+ |> map Simpdata.mk_meta_eq
+ |> map Drule.zero_var_indexes;
+ val params = Term.add_free_names (Thm.prop_of thm1) [];
+ val rhs = thm1
+ |> Thm.prop_of |> Logic.dest_equals |> fst |> Term.strip_comb
+ ||> fst o split_last |> list_comb;
+ val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
+ val assum = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs));
+ in
+ thms
+ |> Conjunction.intr_balanced
+ |> rewrite_rule [Thm.symmetric (Thm.assume assum)]
+ |> Thm.implies_intr assum
+ |> Thm.generalize ([], params) 0
+ |> Axclass.unoverload thy
+ |> Thm.varifyT_global
+ end;
+
+fun mk_free_ctr_equations fcT ctrs inject_thms distinct_thms thy =
+ let
+ fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u;
+ fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});
+ fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});
+
+ val monomorphic_prop_of = prop_of o Thm.unvarify_global o Drule.zero_var_indexes;
+
+ fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
+ fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];
+
+ val triv_inject_goals =
+ map_filter (fn c as (_, T) =>
+ if T = fcT then SOME (HOLogic.mk_Trueprop (true_eq (Const c, Const c))) else NONE)
+ ctrs;
+ val inject_goals = map (massage_inject o monomorphic_prop_of) inject_thms;
+ val distinct_goals = maps (massage_distinct o monomorphic_prop_of) distinct_thms;
+ val refl_goal = HOLogic.mk_Trueprop (true_eq (Free ("x", fcT), Free ("x", fcT)));
+
+ val simp_ctxt =
+ Simplifier.global_context thy HOL_basic_ss
+ addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms));
+
+ fun prove goal =
+ Goal.prove_sorry_global thy [] [] goal (K (ALLGOALS (simp_tac simp_ctxt)))
+ |> Simpdata.mk_eq;
+ in
+ (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
+ end;
+
+fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =
+ let
+ fun add_def lthy =
+ let
+ fun mk_side const_name =
+ Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT);
+ val spec =
+ mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
+ |> Syntax.check_term lthy;
+ val ((_, (_, raw_def)), lthy') =
+ Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
+ val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)
+ val def = singleton (Proof_Context.export lthy' ctxt_thy) raw_def;
+ in
+ (def, lthy')
+ end;
+
+ fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
+
+ val qualify =
+ Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;
+ in
+ Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
+ #> add_def
+ #-> Class.prove_instantiation_exit_result (map o Morphism.thm) (K tac) o single
+ #-> fold Code.del_eqn
+ #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
+ #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
+ [((qualify reflN, [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
+ ((qualify simpsN, [Code.add_default_eqn_attribute]), [(rev thms, [])])])
+ #> snd
+ end;
+
+fun add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy =
+ let
+ val fcT = Type (fcT_name, As);
+ val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs;
+ in
+ if can (Code.constrset_of_consts thy) unover_ctrs then
+ thy
+ |> Code.add_datatype ctrs
+ |> fold_rev Code.add_default_eqn case_thms
+ |> Code.add_case (mk_case_certificate thy case_thms)
+ |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
+ ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
+ else
+ thy
+ end;
+
+end;