# HG changeset patch # User huffman # Date 1287109012 25200 # Node ID 05cda34d36e7cc842d867d1f423e95111cf28117 # Parent bf85fef3cce423738b57ee1b055c429ff6b4ca23 put constructor argument specs in constr_info type diff -r bf85fef3cce4 -r 05cda34d36e7 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Thu Oct 14 14:42:05 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Thu Oct 14 19:16:52 2010 -0700 @@ -10,7 +10,7 @@ type constr_info = { iso_info : Domain_Take_Proofs.iso_info, - con_consts : term list, + con_specs : (term * (bool * typ) list) list, con_betas : thm list, nchotomy : thm, exhaust : thm, @@ -46,7 +46,7 @@ type constr_info = { iso_info : Domain_Take_Proofs.iso_info, - con_consts : term list, + con_specs : (term * (bool * typ) list) list, con_betas : thm list, nchotomy : thm, exhaust : thm, @@ -858,6 +858,8 @@ val dname = Binding.name_of dbind; val _ = writeln ("Proving isomorphism properties of domain "^dname^" ..."); + val bindings = map #1 spec; + (* retrieve facts about rep/abs *) val lhsT = #absT iso_info; val {rep_const, abs_const, ...} = iso_info; @@ -885,16 +887,19 @@ val {con_consts, con_betas, nchotomy, exhaust, compacts, con_rews, inverts, injects, dist_les, dist_eqs} = con_result; - (* define case combinator *) - val ((case_const : typ -> term, cases : thm list), thy) = + (* prepare constructor spec *) + val con_specs : (term * (bool * typ) list) list = let fun prep_arg (lazy, sel, T) = (lazy, T); fun prep_con c (b, args, mx) = (c, map prep_arg args); - val case_spec = map2 prep_con con_consts spec; in - add_case_combinator case_spec lhsT dbind + map2 prep_con con_consts spec + end; + + (* define case combinator *) + val ((case_const : typ -> term, cases : thm list), thy) = + add_case_combinator con_specs lhsT dbind con_betas exhaust iso_locale rep_const thy - end; (* define and prove theorems for selector functions *) val (sel_thms : thm list, thy : theory) = @@ -908,27 +913,13 @@ (* define and prove theorems for discriminator functions *) val (dis_thms : thm list, thy : theory) = - let - val bindings = map #1 spec; - fun prep_arg (lazy, sel, T) = (lazy, T); - fun prep_con c (b, args, mx) = (c, map prep_arg args); - val dis_spec = map2 prep_con con_consts spec; - in - add_discriminators bindings dis_spec lhsT - exhaust case_const cases thy - end + add_discriminators bindings con_specs lhsT + exhaust case_const cases thy; (* define and prove theorems for match combinators *) val (match_thms : thm list, thy : theory) = - let - val bindings = map #1 spec; - fun prep_arg (lazy, sel, T) = (lazy, T); - fun prep_con c (b, args, mx) = (c, map prep_arg args); - val mat_spec = map2 prep_con con_consts spec; - in - add_match_combinators bindings mat_spec lhsT - exhaust case_const cases thy - end + add_match_combinators bindings con_specs lhsT + exhaust case_const cases thy; (* restore original signature path *) val thy = Sign.parent_path thy; @@ -962,7 +953,7 @@ val result = { iso_info = iso_info, - con_consts = con_consts, + con_specs = con_specs, con_betas = con_betas, nchotomy = nchotomy, exhaust = exhaust, diff -r bf85fef3cce4 -r 05cda34d36e7 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Thu Oct 14 14:42:05 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Thu Oct 14 19:16:52 2010 -0700 @@ -198,7 +198,7 @@ val (take_rews, theorems_thy) = thy |> Domain_Theorems.comp_theorems (comp_dbind, eqs) - (dbinds ~~ map snd eqs') take_info constr_infos; + dbinds take_info constr_infos; in theorems_thy end; diff -r bf85fef3cce4 -r 05cda34d36e7 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Oct 14 14:42:05 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Oct 14 19:16:52 2010 -0700 @@ -11,7 +11,7 @@ sig val comp_theorems : binding * Domain_Library.eq list -> - (binding * (binding * (bool * binding option * typ) list * mixfix) list) list -> + binding list -> Domain_Take_Proofs.take_induct_info -> Domain_Constructors.constr_info list -> theory -> thm list * theory @@ -97,7 +97,7 @@ (******************************************************************************) fun take_theorems - (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list) + (dbinds : binding list) (take_info : Domain_Take_Proofs.take_induct_info) (constr_infos : Domain_Constructors.constr_info list) (thy : theory) : thm list list * theory = @@ -122,13 +122,13 @@ end fun prove_take_apps - (((dbind, spec), take_const), constr_info) thy = + ((dbind, take_const), constr_info) thy = let - val {iso_info, con_consts, con_betas, ...} = constr_info; + val {iso_info, con_specs, con_betas, ...} = constr_info; val {abs_inverse, ...} = iso_info; - fun prove_take_app (con_const : term) (bind, args, mx) = + fun prove_take_app (con_const, args) = let - val Ts = map (fn (_, _, T) => T) args; + val Ts = map snd args; val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts); val vs = map Free (ns ~~ Ts); val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs)); @@ -141,7 +141,7 @@ in Goal.prove_global thy [] [] goal (K tac) end; - val take_apps = map2 prove_take_app con_consts spec; + val take_apps = map prove_take_app con_specs; in yield_singleton Global_Theory.add_thmss ((Binding.qualified true "take_rews" dbind, take_apps), @@ -149,7 +149,7 @@ end; in fold_map prove_take_apps - (specs ~~ take_consts ~~ constr_infos) thy + (dbinds ~~ take_consts ~~ constr_infos) thy end; (* ----- general proofs ----------------------------------------------------- *) @@ -508,7 +508,7 @@ fun comp_theorems (comp_dbind : binding, eqs : eq list) - (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list) + (dbinds : binding list) (take_info : Domain_Take_Proofs.take_induct_info) (constr_infos : Domain_Constructors.constr_info list) (thy : theory) = @@ -537,7 +537,7 @@ (* theorems about take *) val (take_rewss, thy) = - take_theorems specs take_info constr_infos thy; + take_theorems dbinds take_info constr_infos thy; val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;