# HG changeset patch # User Christian Urban # Date 1282038745 -28800 # Node ID 49ab06c0ca6487df18c00dd122e0813603d366c9 # Parent 428d9cb9a24300cb6c95c6109c668e6779345e87 improved code diff -r 428d9cb9a243 -r 49ab06c0ca64 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Tue Aug 17 07:11:45 2010 +0800 +++ b/Nominal-General/nominal_library.ML Tue Aug 17 17:52:25 2010 +0800 @@ -41,12 +41,12 @@ val fold_conj: term list -> term (* datatype operations *) + type cns_info = (term * typ * typ list * bool list) list + val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ - val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> - (term * typ * typ list * bool list) list list - val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> - (term * typ * typ list * bool list) list + val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list + val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list (* tactics for function package *) @@ -130,6 +130,8 @@ (** datatypes **) +(* constructor infos *) +type cns_info = (term * typ * typ list * bool list) list (* returns the type of the nth datatype *) fun all_dtyps descr sorts = diff -r 428d9cb9a243 -r 49ab06c0ca64 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Tue Aug 17 07:11:45 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Tue Aug 17 17:52:25 2010 +0800 @@ -25,6 +25,8 @@ thm distinct thm trm_raw_assg_raw.inducts +thm trm_raw.exhaust +thm assg_raw.exhaust thm fv_defs thm perm_simps thm perm_laws @@ -37,8 +39,6 @@ thm size_eqvt -(* eqvt lemmas for fv / fv_bn / bn *) - ML {* val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} *} @@ -47,6 +47,14 @@ val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts} *} +ML {* + val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.exhaust} +*} + +ML {* + val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms assg_raw.exhaust} +*} + ML {* val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} *} diff -r 428d9cb9a243 -r 49ab06c0ca64 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Tue Aug 17 07:11:45 2010 +0800 +++ b/Nominal/NewParser.thy Tue Aug 17 17:52:25 2010 +0800 @@ -312,13 +312,15 @@ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo - val raw_constrs = - flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts)) + val raw_tys = all_dtyps descr sorts val raw_full_ty_names = map (fst o dest_Type) raw_tys val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names + val raw_cns_info = all_dtyp_constrs_types descr sorts + val raw_constrs = flat (map (map (fn (c, _, _, _) => c)) raw_cns_info) + val raw_inject_thms = flat (map #inject dtinfos) val raw_distinct_thms = flat (map #distinct dtinfos) val raw_induct_thm = #induct dtinfo @@ -349,14 +351,15 @@ val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = if get_STEPS lthy3a > 3 - then define_raw_fvs descr sorts raw_bn_info raw_bclauses (raw_inject_thms @ raw_distinct_thms) lthy3a + then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses + (raw_inject_thms @ raw_distinct_thms) lthy3a else raise TEST lthy3a (* definition of raw alphas *) val _ = warning "Definition of alphas"; val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = if get_STEPS lthy3b > 4 - then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b + then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3b else raise TEST lthy3b val alpha_tys = map (domain_type o fastype_of) alpha_trms diff -r 428d9cb9a243 -r 49ab06c0ca64 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Tue Aug 17 07:11:45 2010 +0800 +++ b/Nominal/nominal_dt_alpha.ML Tue Aug 17 17:52:25 2010 +0800 @@ -7,9 +7,8 @@ signature NOMINAL_DT_ALPHA = sig - val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info -> - bclause list list list -> term list -> Proof.context -> - term list * term list * thm list * thm list * thm * local_theory + val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> + term list -> Proof.context -> term list * term list * thm list * thm list * thm * local_theory val mk_alpha_distincts: Proof.context -> thm list -> thm list -> term list -> typ list -> thm list @@ -220,26 +219,23 @@ map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess end -fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy = +fun define_raw_alpha raw_full_ty_names raw_tys cns_info bn_info bclausesss fvs lthy = let - val alpha_names = prefix_dt_names descr sorts "alpha_" - val alpha_arg_tys = all_dtyps descr sorts - val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys + val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_full_ty_names + val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys val alpha_frees = map Free (alpha_names ~~ alpha_tys) - val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs) + val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs) val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val alpha_bn_names = map (prefix "alpha_") bn_names - val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys + val alpha_bn_arg_tys = map (nth raw_tys) bn_tys val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) val alpha_bn_map = bns ~~ alpha_bn_frees - val constrs_info = all_dtyp_constrs_types descr sorts - - val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss - val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info + val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) cns_info bclausesss + val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map cns_info bclausesss) bn_info val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) diff -r 428d9cb9a243 -r 49ab06c0ca64 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Tue Aug 17 07:11:45 2010 +0800 +++ b/Nominal/nominal_dt_rawfuns.ML Tue Aug 17 17:52:25 2010 +0800 @@ -24,9 +24,8 @@ val setify: Proof.context -> term -> term val listify: Proof.context -> term -> term - val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info -> - bclause list list list -> thm list -> Proof.context -> - term list * term list * thm list * thm list * local_theory + val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> + thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list end @@ -211,26 +210,23 @@ map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess end -fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy = +fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms lthy = let - val fv_names = prefix_dt_names descr sorts "fv_" - val fv_arg_tys = all_dtyps descr sorts - val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; + val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names + val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys val fv_frees = map Free (fv_names ~~ fv_tys); - val fv_map = fv_arg_tys ~~ fv_frees + val fv_map = raw_tys ~~ fv_frees val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val fv_bn_names = map (prefix "fv_") bn_names - val fv_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys + val fv_bn_arg_tys = map (nth raw_tys) bn_tys val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) val fv_bn_map = bns ~~ fv_bn_frees - val constrs_info = all_dtyp_constrs_types descr sorts - - val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss - val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info + val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss + val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)