# HG changeset patch # User Christian Urban # Date 1277671281 -3600 # Node ID b151399bd2c37a1257c481909b956ec75a4bd509 # Parent f2d545b77b310414ee40a42fda802a2343a8af3d fixed according to changes in quotient diff -r f2d545b77b31 -r b151399bd2c3 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Thu Jun 24 21:35:11 2010 +0100 +++ b/Nominal/Ex/TypeSchemes.thy Sun Jun 27 21:41:21 2010 +0100 @@ -5,7 +5,8 @@ section {*** Type Schemes ***} atom_decl name -declare [[STEPS = 9]] + +declare [[STEPS = 15]] nominal_datatype ty = Var "name" @@ -17,10 +18,11 @@ Var2 "name" | Fun2 "ty2" "ty2" -(* PROBLEM: this only works once the type is defined +instance ty2 :: pt sorry + nominal_datatype tys2 = All2 xs::"name fset" ty::"ty2" bind_res xs in ty -*) + lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp] diff -r f2d545b77b31 -r b151399bd2c3 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Thu Jun 24 21:35:11 2010 +0100 +++ b/Nominal/NewParser.thy Sun Jun 27 21:41:21 2010 +0100 @@ -264,7 +264,7 @@ val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy in - (dt_full_names', raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) + (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) end *} @@ -313,17 +313,18 @@ let (* definition of the raw datatypes *) val _ = warning "Definition of raw datatypes"; - val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = + val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = if get_STEPS lthy > 0 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy else raise TEST lthy val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo - val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr - val all_full_tnames = map (fn (_, (n, _, _)) => n) descr - val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_full_tnames - + val all_raw_tys = map (fn (_, (n, _, _)) => n) descr + val all_raw_constrs = + flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts)) + + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_tys val inject_thms = flat (map #inject dtinfos); val distinct_thms = flat (map #distinct dtinfos); val constr_thms = inject_thms @ distinct_thms @@ -352,7 +353,7 @@ val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = if get_STEPS lthy3 > 2 - then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 + then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 else raise TEST lthy3 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = @@ -439,19 +440,22 @@ (* 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 + val qty_binds = map (fn (_, bind, _, _) => bind) dts (* not used *) + val qty_names = map Name.of_binding qty_binds; (* not used *) + val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *) - val qty_args' = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms - val qty_args = (qty_descr ~~ qty_args') ~~ alpha_equivp_thms - val (qty_infos, lthy7) = if get_STEPS lthy > 14 - then fold_map Quotient_Type.add_quotient_type qty_args lthy6 + then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 else raise TEST lthy6 val qtys = map #qtyp qty_infos + + val _ = tracing ("all_raw_tys: " ^ commas (map @{make_string} all_raw_tys)) + val _ = tracing ("constrs: " ^ commas (map @{make_string} all_raw_constrs)) + val _ = tracing ("qtys: " ^ commas (map @{make_string} qtys)) + + val _ = if get_STEPS lthy > 15 @@ -465,7 +469,8 @@ map (fn (cname, dts) => Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); - val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; + val dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts + val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys dd lthy7; val _ = warning "Proving respects"; val bn_nos = map (fn (_, i, _) => i) raw_bn_info; @@ -500,17 +505,20 @@ val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] const_rsp_tac) raw_consts lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) - val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12; + val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns) + val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12; val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs - val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; + val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bn_funs + val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys dd lthy12a; val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms - val (qalpha_bn_trms, qalphabn_defs, lthy12c) = - quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_trms) lthy12b; + val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms + val (qalpha_bn_trms, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys dd lthy12b; val _ = warning "Lifting permutations"; val thy = Local_Theory.exit_global lthy12c; val perm_names = map (fn x => "permute_" ^ x) qty_names - val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) raw_perm_simps thy; + val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs + val thy' = define_lifted_perms qtys qty_full_names dd raw_perm_simps thy; val lthy13 = Theory_Target.init NONE thy'; val q_name = space_implode "_" qty_names; fun suffix_bind s = Binding.qualify true q_name (Binding.name s); diff -r f2d545b77b31 -r b151399bd2c3 Nominal/Perm.thy --- a/Nominal/Perm.thy Thu Jun 24 21:35:11 2010 +0100 +++ b/Nominal/Perm.thy Sun Jun 27 21:41:21 2010 +0100 @@ -8,6 +8,7 @@ uses ("nominal_dt_rawperm.ML") ("nominal_dt_rawfuns.ML") ("nominal_dt_alpha.ML") + ("nominal_dt_quot.ML") begin use "nominal_dt_rawperm.ML" @@ -19,6 +20,10 @@ use "nominal_dt_alpha.ML" ML {* open Nominal_Dt_Alpha *} +use "nominal_dt_quot.ML" +ML {* open Nominal_Dt_Quot *} + + (* permutations for quotient types *) ML {* @@ -34,6 +39,8 @@ end *} + + ML {* fun define_lifted_perms qtys full_tnames name_term_pairs thms thy = let diff -r f2d545b77b31 -r b151399bd2c3 Nominal/nominal_dt_quot.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_dt_quot.ML Sun Jun 27 21:41:21 2010 +0100 @@ -0,0 +1,41 @@ +(* Title: nominal_dt_alpha.ML + Author: Christian Urban + Author: Cezary Kaliszyk + + Performing quotient constructions +*) + +signature NOMINAL_DT_QUOT = +sig + val qtype_defs: (string list * binding * mixfix) list -> typ list -> term list -> + thm list -> local_theory -> Quotient_Info.quotdata_info list * local_theory + + val qconst_defs: typ list -> (string * term * mixfix) list -> local_theory -> + Quotient_Info.qconsts_info list * local_theory +end + +structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = +struct + +(* defines the quotient types *) +fun qtype_defs qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = +let + val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms + val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms +in + fold_map Quotient_Type.add_quotient_type qty_args2 lthy +end + +(* defines quotient constants *) +fun qconst_defs qtys const_spec lthy = +let + val (qconst_infos, lthy') = fold_map (Quotient_Def.lift_raw_const qtys) const_spec lthy + val phi = ProofContext.export_morphism lthy' lthy +in + (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') +end + + + +end (* structure *) +