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);