# HG changeset patch # User Christian Urban # Date 1281800003 -28800 # Node ID 1e616069054666e5440c76919f4fe9da8fc000e5 # Parent c670a849af65c174d821cb47db518b9ab332258b improved code diff -r c670a849af65 -r 1e6160690546 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Sat Aug 14 16:54:41 2010 +0800 +++ b/Nominal-General/nominal_library.ML Sat Aug 14 23:33:23 2010 +0800 @@ -58,6 +58,7 @@ (* transformation into the object logic *) val atomize: thm -> thm + end @@ -262,7 +263,6 @@ (* transformes a theorem into one of the object logic *) val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars - end (* structure *) open Nominal_Library; \ No newline at end of file diff -r c670a849af65 -r 1e6160690546 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Sat Aug 14 16:54:41 2010 +0800 +++ b/Nominal/Ex/CoreHaskell.thy Sat Aug 14 23:33:23 2010 +0800 @@ -8,7 +8,7 @@ atom_decl cvar atom_decl tvar -declare [[STEPS = 17]] +declare [[STEPS = 18]] nominal_datatype tkind = KStar diff -r c670a849af65 -r 1e6160690546 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sat Aug 14 16:54:41 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Sat Aug 14 23:33:23 2010 +0800 @@ -4,7 +4,7 @@ atom_decl name -declare [[STEPS = 17]] +declare [[STEPS = 18]] nominal_datatype trm = Var "name" @@ -25,37 +25,13 @@ thm distinct thm trm_raw_assg_raw.inducts thm fv_defs - - -(* cannot lift yet *) -thm eq_iff -thm eq_iff_simps thm perm_simps thm perm_laws thm trm_raw_assg_raw.size(9 - 16) -(* rsp lemmas *) -thm size_rsp -thm funs_rsp -thm constrs_rsp -thm permute_rsp - -declare constrs_rsp[quot_respect] -declare funs_rsp[quot_respect] -declare size_rsp[quot_respect] -declare permute_rsp[quot_respect] - -ML {* - val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} -*} - -ML {* - val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts} -*} - -ML {* - val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} -*} +(* cannot lift yet *) +thm eq_iff +thm eq_iff_simps instantiation trm and assg :: size begin @@ -72,12 +48,6 @@ end -ML {* - val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} -*} - - - instantiation trm and assg :: pt begin @@ -101,13 +71,36 @@ end +ML {* + val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} +*} -(* -lemma [quot_respect]: - "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw" -apply(simp) -sorry -*) +ML {* + val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts} +*} + +ML {* + val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} +*} + +ML {* + val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} +*} + +ML {* + val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps} +*} + +ML {* + val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} +*} + + + + + +section {* NOT *} + ML {* val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas prod_fv.simps prod_rel.simps prod_alpha_def]} @@ -134,21 +127,6 @@ section {* NOT *} - -ML {* - val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} -*} - - -ML {* - val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)} -*} - -ML {* - val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} -*} - - ML {* val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)} *} diff -r c670a849af65 -r 1e6160690546 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sat Aug 14 16:54:41 2010 +0800 +++ b/Nominal/NewParser.thy Sat Aug 14 23:33:23 2010 +0800 @@ -13,6 +13,13 @@ section{* Interface for nominal_datatype *} +ML {* +(* attributes *) +val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) +val rsp_attrib = Attrib.internal (K Quotient_Info.rsp_rules_add) + +*} + ML {* (* nominal datatype parser *) @@ -305,11 +312,11 @@ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo - val all_raw_tys = all_dtyps descr sorts - val all_raw_ty_names = map (fn (_, (n, _, _)) => n) descr val all_raw_constrs = flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts)) - + val all_raw_tys = all_dtyps descr sorts + val all_raw_ty_names = map (fst o dest_Type) all_raw_tys + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names val inject_thms = flat (map #inject dtinfos); val distinct_thms = flat (map #distinct dtinfos); @@ -329,20 +336,16 @@ val _ = warning "Definition of raw permutations"; val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = if get_STEPS lthy0 > 1 - then Local_Theory.theory_result (define_raw_perms descr sorts raw_induct_thm (length dts)) lthy0 + then Local_Theory.theory_result + (define_raw_perms all_raw_ty_names all_raw_tys all_raw_constrs raw_induct_thm) lthy0 else raise TEST lthy0 + val lthy2a = Named_Target.reinit lthy2 lthy2 (* noting the raw permutations as eqvt theorems *) - val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) - val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2 - - val thy = Local_Theory.exit_global lthy2a; - val thy_name = Context.theory_name thy + val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a (* definition of raw fv_functions *) val _ = warning "Definition of raw fv-functions"; - val lthy3 = Named_Target.init NONE thy; - val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = if get_STEPS lthy3 > 2 then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 @@ -382,8 +385,7 @@ else raise TEST lthy4 (* noting the bn_eqvt lemmas in a temprorary theory *) - val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) - val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4) + val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), bn_eqvt) lthy4) val fv_eqvt = if get_STEPS lthy > 7 @@ -399,7 +401,7 @@ |> map (fn thm => thm RS @{thm sym}) else raise TEST lthy4 - val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) + val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), fv_eqvt) lthy_tmp) val (alpha_eqvt, lthy6) = if get_STEPS lthy > 9 @@ -452,17 +454,23 @@ val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt + (* noting the quot_respects lemmas *) + val (_, lthy6a) = + if get_STEPS lthy > 15 + then Local_Theory.note ((Binding.empty, [rsp_attrib]), + raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp) lthy6 + else raise TEST lthy6 + (* defining the quotient type *) val _ = warning "Declaring the quotient types" val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts val qty_binds = map (fn (_, bind, _, _) => bind) dts val qty_names = map Name.of_binding qty_binds; - val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *) val (qty_infos, lthy7) = - if get_STEPS lthy > 15 - then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 - else raise TEST lthy6 + if get_STEPS lthy > 16 + then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a + else raise TEST lthy6a val qtys = map #qtyp qty_infos @@ -479,13 +487,16 @@ map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs val qfv_bns_descr = - map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns + map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns val qalpha_bns_descr = map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms + val qperm_descr = + map2 (fn n => fn t => ("permute_" ^ n, t, NoSyn)) qty_names raw_perm_funs + val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = - if get_STEPS lthy > 16 + if get_STEPS lthy > 17 then lthy7 |> qconst_defs qtys qconstrs_descr @@ -495,12 +506,17 @@ ||>> qconst_defs qtys qalpha_bns_descr else raise TEST lthy7 + (*val _ = Local_Theory.theory_result + (qperm_defs qtys qty_full_names qperm_descr raw_perm_laws) lthy8*) + + val qconstrs = map #qconst qconstrs_info val qbns = map #qconst qbns_info val qfvs = map #qconst qfvs_info val qfv_bns = map #qconst qfv_bns_info val qalpha_bns = map #qconst qalpha_bns_info + (* temporary theorem bindings *) val (_, lthy8') = lthy8 @@ -511,17 +527,17 @@ ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) - ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) - ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp) - ||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp) - ||>> Local_Theory.note ((@{binding "permute_rsp"}, []), alpha_permute_rsp) val _ = - if get_STEPS lthy > 17 + if get_STEPS lthy > 18 then true else raise TEST lthy8' (* old stuff *) + val thy = ProofContext.theory_of lthy8' + val thy_name = Context.theory_name thy + val qty_full_names = map (Long_Name.qualify thy_name) qty_names + val _ = warning "Proving respects"; val bn_nos = map (fn (_, i, _) => i) raw_bn_info; @@ -578,7 +594,7 @@ val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs (* use Local_Theory.theory_result *) val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy; - val lthy13 = Named_Target.init NONE thy'; + val lthy13 = Named_Target.init "" thy'; val q_name = space_implode "_" qty_names; fun suffix_bind s = Binding.qualify true q_name (Binding.name s); diff -r c670a849af65 -r 1e6160690546 Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Sat Aug 14 16:54:41 2010 +0800 +++ b/Nominal/nominal_dt_quot.ML Sat Aug 14 23:33:23 2010 +0800 @@ -42,18 +42,21 @@ (* defines the quotient permutations *) -fun qperm_defs qtys full_tnames name_term_pairs thms thy = +fun qperm_defs qtys full_tnames perm_specs thms thy = let val lthy = Class.instantiation (full_tnames, [], @{sort pt}) thy; - val (_, lthy') = qconst_defs qtys name_term_pairs lthy; + + val (_, lthy') = qconst_defs qtys perm_specs lthy; + val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; + fun tac _ = Class.intro_classes_tac [] THEN - (ALLGOALS (resolve_tac lifted_thms)) - val lthy'' = Class.prove_instantiation_instance tac lthy' + (ALLGOALS (resolve_tac lifted_thms)) in - Local_Theory.exit_global lthy'' + lthy' + |> Class.prove_instantiation_exit tac end diff -r c670a849af65 -r 1e6160690546 Nominal/nominal_dt_rawperm.ML --- a/Nominal/nominal_dt_rawperm.ML Sat Aug 14 16:54:41 2010 +0800 +++ b/Nominal/nominal_dt_rawperm.ML Sat Aug 14 23:33:23 2010 +0800 @@ -9,7 +9,7 @@ signature NOMINAL_DT_RAWPERM = sig - val define_raw_perms: Datatype.descr -> (string * sort) list -> thm -> int -> theory -> + val define_raw_perms: string list -> typ list -> term list -> thm -> theory -> (term list * thm list * thm list) * theory end @@ -18,39 +18,6 @@ struct -(* permutation function for one argument - - - in case the argument is recursive it returns - - permute_fn p arg - - - in case the argument is non-recursive it will return - - p o arg -*) -fun perm_arg permute_fn_frees p (arg_dty, arg) = - if Datatype_Aux.is_rec_type arg_dty - then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg - else mk_perm p arg - - -(* generates the equation for the permutation function for one constructor; - i is the index of the corresponding datatype *) -fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) = -let - val p = Free ("p", @{typ perm}) - val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts - val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) - val args = map Free (arg_names ~~ arg_tys) - val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i)) - val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args) - val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args)) - val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) -in - (Attrib.empty_binding, eq) -end - - (** proves the two pt-type class properties **) fun prove_permute_zero lthy induct perm_defs perm_fns = @@ -99,49 +66,62 @@ end -(* user_dt_nos refers to the number of "un-unfolded" datatypes - given by the user -*) -fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy = +fun mk_perm_eq ty_perm_assoc cnstr = let - val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; - val user_full_tnames = List.take (all_full_tnames, user_dt_nos); + fun lookup_perm p (ty, arg) = + case (AList.lookup (op=) ty_perm_assoc ty) of + SOME perm => perm $ p $ arg + | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg + + val p = Free ("p", @{typ perm}) + val (arg_tys, ty) = + fastype_of cnstr + |> strip_type + + val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) + val args = map Free (arg_names ~~ arg_tys) - val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" - val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr - val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) + val lhs = lookup_perm p (ty, list_comb (cnstr, args)) + val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) + + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) +in + (Attrib.empty_binding, eq) +end + - fun perm_eq (i, (_, _, constrs)) = - map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; +fun define_raw_perms full_ty_names tys constrs induct_thm thy = +let + val perm_fn_names = full_ty_names + |> map Long_Name.base_name + |> map (prefix "permute_") - val perm_eqs = maps perm_eq dt_descr; + val perm_fn_types = map perm_ty tys + val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) + val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names + + val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs val lthy = - Class.instantiation (user_full_tnames, [], @{sort pt}) thy; + Class.instantiation (full_ty_names, [], @{sort pt}) thy val ((perm_funs, perm_eq_thms), lthy') = - Primrec.add_primrec - (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; + Primrec.add_primrec perm_fn_binds perm_eqs lthy; val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs - val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); - val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) - val perms_name = space_implode "_" perm_fn_names - val perms_zero_bind = Binding.name (perms_name ^ "_zero") - val perms_plus_bind = Binding.name (perms_name ^ "_plus") fun tac _ (_, _, simps) = Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) fun morphism phi (fvs, dfs, simps) = - (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); + (map (Morphism.term phi) fvs, + map (Morphism.thm phi) dfs, + map (Morphism.thm phi) simps); in lthy' - |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) - |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |> Class.prove_instantiation_exit_result morphism tac - (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') + (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) end