# HG changeset patch # User panny # Date 1386035480 -3600 # Node ID a692901ecdc2ed2ff1b85e81b6af2acb48ec667e # Parent ce80d7cd7277c836f1107e19d8517ff8b311ae56# Parent 8dd1a354ee86e1582592de030731f66ee4859e03 merge diff -r ce80d7cd7277 -r a692901ecdc2 etc/isar-keywords.el --- 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" diff -r ce80d7cd7277 -r a692901ecdc2 src/Doc/Datatypes/Datatypes.thy --- 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. diff -r ce80d7cd7277 -r a692901ecdc2 src/HOL/BNF/Examples/Derivation_Trees/DTree.thy --- 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 diff -r ce80d7cd7277 -r a692901ecdc2 src/HOL/BNF/Tools/bnf_def.ML --- 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)), diff -r ce80d7cd7277 -r a692901ecdc2 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- 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 *) diff -r ce80d7cd7277 -r a692901ecdc2 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- 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; diff -r ce80d7cd7277 -r a692901ecdc2 src/HOL/Ctr_Sugar.thy --- 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 diff -r ce80d7cd7277 -r a692901ecdc2 src/HOL/Inductive.thy --- 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: *} diff -r ce80d7cd7277 -r a692901ecdc2 src/HOL/Tools/Datatype/datatype_codegen.ML --- 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; diff -r ce80d7cd7277 -r a692901ecdc2 src/HOL/Tools/ctr_sugar.ML --- 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"} diff -r ce80d7cd7277 -r a692901ecdc2 src/HOL/Tools/ctr_sugar_code.ML --- /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;