# HG changeset patch # User Christian Urban # Date 1281852028 -28800 # Node ID c6d30d5f5ba19dd9ecd69610f200dad0e3145689 # Parent 107c06267f33f5a69bb46a65e9c6e1ddf3571d82 defined qperms and qsizes diff -r 107c06267f33 -r c6d30d5f5ba1 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Sun Aug 15 11:03:13 2010 +0800 +++ b/Nominal/Ex/CoreHaskell.thy Sun Aug 15 14:00:28 2010 +0800 @@ -8,7 +8,7 @@ atom_decl cvar atom_decl tvar -declare [[STEPS = 18]] +declare [[STEPS = 20]] nominal_datatype tkind = KStar @@ -85,10 +85,50 @@ | "bv_cvs CvsNil = []" | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" - +(* can lift *) thm distinct +thm fv_defs -term TvsNil +thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts +thm perm_simps +thm perm_laws +thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98) + +(* cannot lift yet *) +thm eq_iff +thm eq_iff_simps + +ML {* + val qtys = [@{typ tkind}, @{typ ckind}, @{typ ty}, @{typ ty_lst}, @{typ co}, + @{typ co_lst}, @{typ trm}, @{typ assoc_lst}, @{typ pat}, @{typ vars}, + @{typ tvars}, @{typ cvars}] +*} + +ML {* + val thms_d = map (lift_thm qtys @{context}) @{thms distinct} +*} + +ML {* + val thms_i = map (lift_thm qtys @{context}) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts} +*} + +ML {* + val thms_f = map (lift_thm qtys @{context}) @{thms fv_defs} +*} + +ML {* + val thms_i = map (lift_thm qtys @{context}) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)} +*} + +ML {* + val thms_p = map (lift_thm qtys @{context}) @{thms perm_simps} +*} + +ML {* + val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws} +*} + + lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) diff -r 107c06267f33 -r c6d30d5f5ba1 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Sun Aug 15 11:03:13 2010 +0800 +++ b/Nominal/Ex/SingleLet.thy Sun Aug 15 14:00:28 2010 +0800 @@ -4,7 +4,7 @@ atom_decl name -declare [[STEPS = 18]] +declare [[STEPS = 20]] nominal_datatype trm = Var "name" @@ -33,44 +33,6 @@ thm eq_iff thm eq_iff_simps -instantiation trm and assg :: size -begin - -quotient_definition - "size_trm :: trm \ nat" -is "size :: trm_raw \ nat" - -quotient_definition - "size_assg :: assg \ nat" -is "size :: assg_raw \ nat" - -instance .. - -end - -instantiation trm and assg :: pt -begin - -quotient_definition - "permute_trm :: perm => trm => trm" - is "permute :: perm \ trm_raw \ trm_raw" - -quotient_definition - "permute_assg :: perm => assg => assg" - is "permute :: perm \ assg_raw \ assg_raw" - -lemma qperm_laws: - fixes t::trm and a::assg - shows "permute 0 t = t" - and "permute 0 a = a" -sorry - -instance -apply(default) -sorry - -end - ML {* val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} *} diff -r 107c06267f33 -r c6d30d5f5ba1 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sun Aug 15 11:03:13 2010 +0800 +++ b/Nominal/NewParser.thy Sun Aug 15 14:00:28 2010 +0800 @@ -312,20 +312,19 @@ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) val {descr, sorts, ...} = dtinfo - val all_raw_constrs = + val 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 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)) all_raw_ty_names - val inject_thms = flat (map #inject dtinfos) - val distinct_thms = flat (map #distinct dtinfos) - val constr_thms = inject_thms @ distinct_thms - - val raw_induct_thm = #induct dtinfo; - val raw_induct_thms = #inducts dtinfo; - val exhaust_thms = map #exhaust dtinfos; - val raw_size_trms = map size_const all_raw_tys + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names + + val raw_inject_thms = flat (map #inject dtinfos) + val raw_distinct_thms = flat (map #distinct dtinfos) + val raw_induct_thm = #induct dtinfo + val raw_induct_thms = #inducts dtinfo + val raw_exhaust_thms = map #exhaust dtinfos + val raw_size_trms = map size_const raw_tys val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) |> `(fn thms => (length thms) div 2) |> uncurry drop @@ -335,7 +334,7 @@ val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = if get_STEPS lthy0 > 1 then Local_Theory.theory_result - (define_raw_perms all_raw_ty_names all_raw_tys all_raw_constrs raw_induct_thm) lthy0 + (define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm) lthy0 else raise TEST lthy0 val lthy2a = Named_Target.reinit lthy2 lthy2 @@ -346,12 +345,13 @@ val _ = warning "Definition of raw fv-functions"; 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 + then raw_bn_decls raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs + (raw_inject_thms @ raw_distinct_thms) lthy3 else raise TEST lthy3 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 constr_thms lthy3a + then define_raw_fvs descr sorts raw_bn_info raw_bclauses (raw_inject_thms @ raw_distinct_thms) lthy3a else raise TEST lthy3a (* definition of raw alphas *) @@ -365,14 +365,14 @@ (* definition of alpha-distinct lemmas *) val _ = warning "Distinct theorems"; val alpha_distincts = - mk_alpha_distincts lthy4 alpha_cases distinct_thms alpha_trms all_raw_tys + mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys (* definition of alpha_eq_iff lemmas *) (* they have a funny shape for the simplifier *) val _ = warning "Eq-iff theorems"; val (alpha_eq_iff_simps, alpha_eq_iff) = if get_STEPS lthy > 5 - then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases + then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases else raise TEST lthy4 (* proving equivariance lemmas for bns, fvs, size and alpha *) @@ -421,7 +421,7 @@ val alpha_trans_thms = if get_STEPS lthy > 12 - then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) + then raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_induct alpha_cases lthy6 else raise TEST lthy6 @@ -447,7 +447,7 @@ (raw_size_thms @ raw_size_eqvt) lthy6 |> map mk_funs_rsp - val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros + val raw_constrs_rsp = raw_constrs_rsp raw_constrs alpha_trms alpha_intros (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt @@ -462,21 +462,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_infos, lthy7) = if get_STEPS lthy > 16 - then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a + then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a else raise TEST lthy6a val qtys = map #qtyp qty_infos - + val qty_full_names = map (fst o dest_Type) qtys + val qty_names = map Long_Name.base_name qty_full_names + + (* defining of quotient term-constructors, binding functions, free vars functions *) val _ = warning "Defining the quotient constants" val qconstrs_descr = flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) - |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs + |> map2 (fn t => fn (b, mx) => (b, t, mx)) raw_constrs val qbns_descr = map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns @@ -493,20 +494,34 @@ val qperm_descr = map2 (fn n => fn t => ("permute_" ^ n, t, NoSyn)) qty_names raw_perm_funs + val qsize_descr = + map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms + val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = if get_STEPS lthy > 17 then lthy7 - |> qconst_defs qtys qconstrs_descr - ||>> qconst_defs qtys qbns_descr - ||>> qconst_defs qtys qfvs_descr - ||>> qconst_defs qtys qfv_bns_descr - ||>> qconst_defs qtys qalpha_bns_descr + |> define_qconsts qtys qconstrs_descr + ||>> define_qconsts qtys qbns_descr + ||>> define_qconsts qtys qfvs_descr + ||>> define_qconsts qtys qfv_bns_descr + ||>> define_qconsts 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*) + (* definition of the quotient permfunctions and pt-class *) + val lthy9 = + if get_STEPS lthy > 18 + then Local_Theory.theory + (define_qperms qtys qty_full_names qperm_descr raw_perm_laws) lthy8 + else raise TEST lthy8 + + val lthy9' = + if get_STEPS lthy > 19 + then Local_Theory.theory + (define_qsizes qtys qty_full_names qsize_descr) lthy9 + else raise TEST lthy9 + val lthy9a = Named_Target.reinit lthy9' lthy9' val qconstrs = map #qconst qconstrs_info val qbns = map #qconst qbns_info @@ -517,7 +532,7 @@ (* temporary theorem bindings *) - val (_, lthy8') = lthy8 + val (_, lthy9') = lthy9a |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) @@ -527,12 +542,12 @@ ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) val _ = - if get_STEPS lthy > 18 - then true else raise TEST lthy8' + if get_STEPS lthy > 20 + then true else raise TEST lthy9' (* old stuff *) - val thy = ProofContext.theory_of lthy8' + val thy = ProofContext.theory_of lthy9' val thy_name = Context.theory_name thy val qty_full_names = map (Long_Name.qualify thy_name) qty_names @@ -561,28 +576,28 @@ (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else - let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; + let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms raw_exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] alpha_bn_rsp_tac) alpha_bn_trms lthy11 fun const_rsp_tac _ = let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] - const_rsp_tac) all_raw_constrs lthy11a + const_rsp_tac) raw_constrs lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns) - val (qfv_info, lthy12a) = qconst_defs qtys dd lthy12; + val (qfv_info, lthy12a) = define_qconsts qtys dd lthy12; val qfv_ts = map #qconst qfv_info val qfv_defs = map #def qfv_info 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 dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bns - val (qbn_info, lthy12b) = qconst_defs qtys dd lthy12a; + val (qbn_info, lthy12b) = define_qconsts qtys dd lthy12a; val qbn_ts = map #qconst qbn_info val qbn_defs = map #def qbn_info val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms - val (qalpha_info, lthy12c) = qconst_defs qtys dd lthy12b; + val (qalpha_info, lthy12c) = define_qconsts qtys dd lthy12b; val qalpha_bn_trms = map #qconst qalpha_info val qalphabn_defs = map #def qalpha_info @@ -591,7 +606,7 @@ val perm_names = map (fn x => "permute_" ^ x) qty_names 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 thy' = define_qperms qtys qty_full_names dd raw_perm_laws thy; val lthy13 = Named_Target.init "" thy'; val q_name = space_implode "_" qty_names; diff -r 107c06267f33 -r c6d30d5f5ba1 Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Sun Aug 15 11:03:13 2010 +0800 +++ b/Nominal/nominal_dt_quot.ML Sun Aug 15 14:00:28 2010 +0800 @@ -7,21 +7,24 @@ signature NOMINAL_DT_QUOT = sig - val qtype_defs: (string list * binding * mixfix) list -> typ list -> term list -> + val define_qtypes: (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 -> + val define_qconsts: typ list -> (string * term * mixfix) list -> local_theory -> Quotient_Info.qconsts_info list * local_theory - val qperm_defs: typ list -> string list -> (string * term * mixfix) list -> + val define_qperms: typ list -> string list -> (string * term * mixfix) list -> thm list -> theory -> theory + + val define_qsizes: typ list -> string list -> (string * term * mixfix) list -> + theory -> 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 = +fun define_qtypes 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 @@ -31,7 +34,7 @@ (* defines quotient constants *) -fun qconst_defs qtys consts_specs lthy = +fun define_qconsts qtys consts_specs lthy = let val (qconst_infos, lthy') = fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy @@ -41,24 +44,36 @@ end -(* defines the quotient permutations *) -fun qperm_defs qtys full_tnames perm_specs thms thy = +(* defines the quotient permutations and proves pt-class *) +fun define_qperms qtys qfull_ty_names perm_specs raw_perm_laws thy = let - val lthy = - Class.instantiation (full_tnames, [], @{sort pt}) thy; + val lthy = Class.instantiation (qfull_ty_names, [], @{sort pt}) thy - val (_, lthy') = qconst_defs qtys perm_specs lthy; + val (_, lthy') = define_qconsts qtys perm_specs lthy - val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; + val lifted_perm_laws = map (Quotient_Tacs.lifted qtys lthy') raw_perm_laws fun tac _ = Class.intro_classes_tac [] THEN - (ALLGOALS (resolve_tac lifted_thms)) + (ALLGOALS (resolve_tac lifted_perm_laws)) in lthy' |> Class.prove_instantiation_exit tac end +(* defines the size functions and proves size-class *) +fun define_qsizes qtys qfull_ty_names size_specs thy = +let + val lthy = Class.instantiation (qfull_ty_names, [], @{sort size}) thy + + val (_, lthy') = define_qconsts qtys size_specs lthy + + fun tac _ = Class.intro_classes_tac [] +in + lthy' + |> Class.prove_instantiation_exit tac +end + end (* structure *)