# HG changeset patch # User Christian Urban # Date 1310383424 -3600 # Node ID c2ce4797321a13964e2fbbdf8a57c112e9f72096 # Parent 248546bfeb169d1f4a966ff15134b21dec553f2a# Parent 9bd97ed202f71967a1bec4acda6f16692e22c4d1 merged diff -r 248546bfeb16 -r c2ce4797321a Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon Jul 11 12:23:24 2011 +0100 +++ b/Nominal/Nominal2.thy Mon Jul 11 12:23:44 2011 +0100 @@ -145,7 +145,7 @@ ML {* (* definition of the raw datatype *) -fun define_raw_dts dts bn_funs bn_eqs bclauses lthy = +fun define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy = let val thy = Local_Theory.exit_global lthy val thy_name = Context.theory_name thy @@ -155,8 +155,6 @@ val dt_full_names' = add_raws dt_full_names val dts_env = dt_full_names ~~ dt_full_names' - val cnstr_names = get_cnstr_strs dts - val cnstr_tys = get_typed_cnstrs dts val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names val cnstr_full_names' = map (fn (x, y) => Long_Name.qualify thy_name (Long_Name.qualify (add_raw x) (add_raw y))) cnstr_tys @@ -168,37 +166,25 @@ val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) (bn_fun_strs ~~ bn_fun_strs') - val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env + val (raw_full_dt_names, raw_dts) = rawify_dts dt_names dts dts_env val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses - val (raw_dt_full_names, thy1) = - Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy + val (raw_full_dt_names', thy1) = + Datatype.add_datatype Datatype.default_config raw_full_dt_names raw_dts thy val lthy1 = Named_Target.theory_init thy1 -in - (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy1) -end -*} - -ML {* -fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = -let - val _ = trace_msg (K "Defining raw datatypes...") - val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) = - define_raw_dts dts bn_funs bn_eqs bclauses lthy - - val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_dt_names + val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) raw_full_dt_names' val {descr, sorts, ...} = hd dtinfos val raw_tys = Datatype_Aux.get_rec_types descr sorts - val tvs = hd raw_tys + val raw_ty_args = hd raw_tys |> snd o dest_Type - |> map dest_TFree + |> map dest_TFree val raw_cns_info = all_dtyp_constrs_types descr sorts - val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info + val raw_all_cns = (map o map) (fn (c, _, _, _) => c) raw_cns_info val raw_inject_thms = flat (map #inject dtinfos) val raw_distinct_thms = flat (map #distinct dtinfos) @@ -206,41 +192,100 @@ val raw_induct_thms = #inducts (hd dtinfos) val raw_exhaust_thms = map #exhaust dtinfos val raw_size_trms = map HOLogic.size_const raw_tys - val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names) + val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy1) (hd raw_full_dt_names') |> `(fn thms => (length thms) div 2) |> uncurry drop + + val raw_result = RawDtInfo + {raw_dt_names = raw_full_dt_names', + raw_dts = raw_dts, + raw_tys = raw_tys, + raw_ty_args = raw_ty_args, + raw_cns_info = raw_cns_info, + raw_all_cns = raw_all_cns, + raw_inject_thms = raw_inject_thms, + raw_distinct_thms = raw_distinct_thms, + raw_induct_thm = raw_induct_thm, + raw_induct_thms = raw_induct_thms, + raw_exhaust_thms = raw_exhaust_thms, + raw_size_trms = raw_size_trms, + raw_size_thms = raw_size_thms} +in + (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_result, lthy1) +end +*} + +ML {* +infix 1 ||>>> |>>> + +fun (x |>>> f) = + let + val (x', y') = f x + in + ([x'], y') + end + +fun (([], y) ||>>> f) = ([], y) + | ((xs, y) ||>>> f) = + let + val (x', y') = f y + in + (xs @ [x'], y') + end; +(op ||>>) +*} + + + +ML {* +fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = +let + val cnstr_names = get_cnstr_strs dts + val cnstr_tys = get_typed_cnstrs dts + + val _ = trace_msg (K "Defining raw datatypes...") + val (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_dt_info, lthy0) = + define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy + + val RawDtInfo + {raw_dt_names, + raw_tys, + raw_ty_args, + raw_all_cns, + raw_inject_thms, + raw_distinct_thms, + raw_induct_thm, + raw_induct_thms, + raw_exhaust_thms, + raw_size_trms, + raw_size_thms, ...} = raw_dt_info val _ = trace_msg (K "Defining raw permutations...") - val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = - define_raw_perms raw_dt_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0 + val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = define_raw_perms raw_dt_info lthy0 (* noting the raw permutations as eqvt theorems *) - val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a + val lthy3 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a) val _ = trace_msg (K "Defining raw fv- and bn-functions...") val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_inducts, lthy3a) = - define_raw_bns raw_dt_names raw_dts raw_bn_funs raw_bn_eqs - (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3 + define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs lthy3 (* defining the permute_bn functions *) val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = - define_raw_bn_perms raw_tys raw_bn_info raw_cns_info - (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a + define_raw_bn_perms raw_dt_info raw_bn_info lthy3a val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = - define_raw_fvs raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses - (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b + define_raw_fvs raw_dt_info raw_bn_info raw_bclauses lthy3b val _ = trace_msg (K "Defining alpha relations...") val (alpha_result, lthy4) = - define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c + define_raw_alpha raw_dt_info raw_bn_info raw_bclauses raw_fvs lthy3c val _ = trace_msg (K "Proving distinct theorems...") - val alpha_distincts = - raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names + val alpha_distincts = raw_prove_alpha_distincts lthy4 alpha_result raw_dt_info val _ = trace_msg (K "Proving eq-iff theorems...") - val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_distinct_thms raw_inject_thms + val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_dt_info val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...") val raw_bn_eqvt = @@ -253,11 +298,15 @@ raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) (Local_Theory.restore lthy_tmp) - val raw_size_eqvt = - raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) - (Local_Theory.restore lthy_tmp) - |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) - |> map (fn thm => thm RS @{thm sym}) + val raw_size_eqvt = + let + val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info + in + raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) + (Local_Theory.restore lthy_tmp) + |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) + |> map (fn thm => thm RS @{thm sym}) + end val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) @@ -293,7 +342,7 @@ |> map mk_funs_rsp val raw_constrs_rsp = - raw_constrs_rsp lthy5 alpha_result (flat raw_constrs) (alpha_bn_imp_thms @ raw_funs_rsp_aux) + raw_constrs_rsp lthy5 alpha_result (flat raw_all_cns) (alpha_bn_imp_thms @ raw_funs_rsp_aux) val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt @@ -324,7 +373,7 @@ val _ = trace_msg (K "Defining the quotient constants...") val qconstrs_descrs = - (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_constrs + (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_all_cns val qbns_descr = map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) bn_funs raw_bns @@ -362,10 +411,10 @@ ||>> define_qconsts qtys qperm_bn_descr val lthy9 = - define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 + define_qperms qtys qty_full_names raw_ty_args qperm_descr raw_perm_laws lthy8 val lthy9a = - define_qsizes qtys qty_full_names tvs qsize_descr lthy9 + define_qsizes qtys qty_full_names raw_ty_args qsize_descr lthy9 val qtrms = (map o map) #qconst qconstrs_infos val qbns = map #qconst qbns_info @@ -378,37 +427,34 @@ val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def prod.cases} - val (((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), qbn_inducts), - lthyA) = + val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, + qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, + qalpha_refl_thms ], lthyB) = lthy9a - |> lift_thms qtys [] alpha_distincts - ||>> lift_thms qtys eq_iff_simps alpha_eq_iff - ||>> lift_thms qtys [] raw_fv_defs - ||>> lift_thms qtys [] raw_bn_defs - ||>> lift_thms qtys [] raw_perm_simps - ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) - ||>> lift_thms qtys [] raw_bn_inducts - - val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) = - lthyA - |> lift_thms qtys [] raw_size_eqvt - ||>> lift_thms qtys [] [raw_induct_thm] - ||>> lift_thms qtys [] raw_exhaust_thms - ||>> lift_thms qtys [] raw_size_thms - ||>> lift_thms qtys [] raw_perm_bn_simps - ||>> lift_thms qtys [] alpha_refl_thms + |>>> lift_thms qtys [] alpha_distincts + ||>>> lift_thms qtys eq_iff_simps alpha_eq_iff + ||>>> lift_thms qtys [] raw_fv_defs + ||>>> lift_thms qtys [] raw_bn_defs + ||>>> lift_thms qtys [] raw_perm_simps + ||>>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) + ||>>> lift_thms qtys [] raw_bn_inducts + ||>>> lift_thms qtys [] raw_size_eqvt + ||>>> lift_thms qtys [] [raw_induct_thm] + ||>>> lift_thms qtys [] raw_exhaust_thms + ||>>> lift_thms qtys [] raw_size_thms + ||>>> lift_thms qtys [] raw_perm_bn_simps + ||>>> lift_thms qtys [] alpha_refl_thms val qinducts = Project_Rule.projections lthyB qinduct val _ = trace_msg (K "Proving supp lemmas and fs-instances...") - val qsupports_thms = - prove_supports lthyB qperm_simps (flat qtrms) + val qsupports_thms = prove_supports lthyB qperm_simps (flat qtrms) (* finite supp lemmas *) val qfsupp_thms = prove_fsupp lthyB qtys qinduct qsupports_thms (* fs instances *) - val lthyC = fs_instance qtys qty_full_names tvs qfsupp_thms lthyB + val lthyC = fs_instance qtys qty_full_names raw_ty_args qfsupp_thms lthyB val _ = trace_msg (K "Proving equality between fv and supp...") val qfv_supp_thms = @@ -523,6 +569,7 @@ fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) = let + val (constrs', sorts') = fold prep_constr constrs ([], sorts) diff -r 248546bfeb16 -r c2ce4797321a Nominal/nominal_basics.ML --- a/Nominal/nominal_basics.ML Mon Jul 11 12:23:24 2011 +0100 +++ b/Nominal/nominal_basics.ML Mon Jul 11 12:23:44 2011 +0100 @@ -10,6 +10,7 @@ val trace_msg: (unit -> string) -> unit val last2: 'a list -> 'a * 'a + val split_triples: ('a * 'b * 'c) list -> ('a list * 'b list * 'c list) val split_last2: 'a list -> 'a list * 'a * 'a val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list @@ -68,6 +69,9 @@ then remove_dups eq xs else x :: remove_dups eq xs +fun split_triples xs = + fold (fn (a, b, c) => fn (axs, bxs, cxs) => (a :: axs, b :: bxs, c :: cxs)) xs ([], [], []) + fun last2 [] = raise Empty | last2 [_] = raise Empty | last2 [x, y] = (x, y) diff -r 248546bfeb16 -r c2ce4797321a Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Mon Jul 11 12:23:24 2011 +0100 +++ b/Nominal/nominal_dt_alpha.ML Mon Jul 11 12:23:44 2011 +0100 @@ -9,8 +9,8 @@ sig val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term - val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> - bclause list list list -> term list -> Proof.context -> alpha_result * local_theory + val define_raw_alpha: raw_dt_info -> bn_info list -> bclause list list list -> term list -> + Proof.context -> alpha_result * local_theory val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list @@ -18,8 +18,8 @@ val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list - val raw_prove_alpha_distincts: Proof.context -> alpha_result -> thm list -> string list -> thm list - val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> thm list -> thm list -> thm list + val raw_prove_alpha_distincts: Proof.context -> alpha_result -> raw_dt_info -> thm list + val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list @@ -224,9 +224,11 @@ 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 raw_full_ty_names raw_tys cns_info bn_info bclausesss fvs lthy = +fun define_raw_alpha raw_dt_info bn_info bclausesss fvs lthy = let - val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_full_ty_names + val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, ...} = raw_dt_info + + val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_dt_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 = raw_tys ~~ (alpha_frees ~~ fvs) @@ -239,8 +241,8 @@ val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) val alpha_bn_map = bns ~~ alpha_bn_frees - 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 alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss + val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_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) @@ -393,9 +395,10 @@ rtac notI THEN' eresolve_tac cases_thms THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) -fun raw_prove_alpha_distincts ctxt alpha_result raw_distinct_thms raw_dt_names = +fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = let val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result + val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info val ty_trm_assoc = raw_dt_names ~~ alpha_names @@ -439,9 +442,10 @@ else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) end; -fun raw_prove_alpha_eq_iff ctxt alpha_result raw_distinct_thms raw_inject_thms = +fun raw_prove_alpha_eq_iff ctxt alpha_result raw_dt_info = let val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result + val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; val goals = map mk_alpha_eq_iff_goal thms_imp; diff -r 248546bfeb16 -r c2ce4797321a Nominal/nominal_dt_data.ML --- a/Nominal/nominal_dt_data.ML Mon Jul 11 12:23:24 2011 +0100 +++ b/Nominal/nominal_dt_data.ML Mon Jul 11 12:23:44 2011 +0100 @@ -5,11 +5,21 @@ signature NOMINAL_DT_DATA = sig + (* info of raw datatypes *) + type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list + + (* info of raw binding functions *) + type bn_info = term * int * (int * term option) list list + + (* binding modes and binding clauses *) + datatype bmode = Lst | Res | Set + datatype bclause = BC of bmode * (term option * int) list * int list + type info = - {inject : thm list, - distinct : thm list, - strong_inducts : thm list, - strong_exhaust : thm list} + {inject : thm list, + distinct : thm list, + strong_inducts : thm list, + strong_exhaust : thm list} val get_all_info: Proof.context -> (string * info) list val get_info: Proof.context -> string -> info option @@ -17,6 +27,29 @@ val register_info: (string * info) -> Context.generic -> Context.generic val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list + datatype user_data = UserData of + {dts : dt_info, + cn_names : string list, + cn_tys : (string * string) list, + bn_funs : (binding * typ * mixfix) list, + bn_eqs : (Attrib.binding * term) list, + bclauses : bclause list list list} + + datatype raw_dt_info = RawDtInfo of + {raw_dt_names : string list, + raw_dts : dt_info, + raw_tys : typ list, + raw_ty_args : (string * sort) list, + raw_cns_info : cns_info list, + raw_all_cns : term list list, + raw_inject_thms : thm list, + raw_distinct_thms : thm list, + raw_induct_thm : thm, + raw_induct_thms : thm list, + raw_exhaust_thms : thm list, + raw_size_trms : term list, + raw_size_thms : thm list} + datatype alpha_result = AlphaResult of {alpha_names : string list, alpha_trms : term list, @@ -33,6 +66,24 @@ structure Nominal_Dt_Data: NOMINAL_DT_DATA = struct +(* string list - type variables of a datatype + binding - name of the datatype + mixfix - its mixfix + (binding * typ list * mixfix) list - datatype constructors of the type +*) +type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list + + +(* term - is constant of the bn-function + int - is datatype number over which the bn-function is defined + int * term option - is number of the corresponding argument with possibly + recursive call with bn-function term +*) +type bn_info = term * int * (int * term option) list list + +datatype bmode = Lst | Res | Set +datatype bclause = BC of bmode * (term option * int) list * int list + (* information generated by nominal_datatype *) type info = @@ -68,6 +119,30 @@ map aux ty_names end + +datatype user_data = UserData of + {dts : dt_info, + cn_names : string list, + cn_tys : (string * string) list, + bn_funs : (binding * typ * mixfix) list, + bn_eqs : (Attrib.binding * term) list, + bclauses : bclause list list list} + +datatype raw_dt_info = RawDtInfo of + {raw_dt_names : string list, + raw_dts : dt_info, + raw_tys : typ list, + raw_ty_args : (string * sort) list, + raw_cns_info : cns_info list, + raw_all_cns : term list list, + raw_inject_thms : thm list, + raw_distinct_thms : thm list, + raw_induct_thm : thm, + raw_induct_thms : thm list, + raw_exhaust_thms : thm list, + raw_size_trms : term list, + raw_size_thms : thm list} + datatype alpha_result = AlphaResult of {alpha_names : string list, alpha_trms : term list, @@ -79,5 +154,4 @@ alpha_cases : thm list, alpha_raw_induct : thm} - end \ No newline at end of file diff -r 248546bfeb16 -r c2ce4797321a Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Mon Jul 11 12:23:24 2011 +0100 +++ b/Nominal/nominal_dt_rawfuns.ML Mon Jul 11 12:23:44 2011 +0100 @@ -7,59 +7,30 @@ signature NOMINAL_DT_RAWFUNS = sig - (* info of raw datatypes *) - type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list - - (* info of raw binding functions *) - type bn_info = term * int * (int * term option) list list - - (* binding modes and binding clauses *) - datatype bmode = Lst | Res | Set - datatype bclause = BC of bmode * (term option * int) list * int list - val get_all_binders: bclause list -> (term option * int) list val is_recursive_binder: bclause -> bool - val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> - (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> + val define_raw_bns: raw_dt_info -> (binding * typ option * mixfix) list -> + (Attrib.binding * term) list -> local_theory -> (term list * thm list * bn_info list * thm list * local_theory) - val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> - thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory + val define_raw_fvs: raw_dt_info -> bn_info list -> bclause list list list -> + Proof.context -> term list * term list * thm list * thm list * local_theory - val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> - local_theory -> (term list * thm list * local_theory) + val define_raw_bn_perms: raw_dt_info -> bn_info list -> local_theory -> + (term list * thm list * local_theory) + + val define_raw_perms: raw_dt_info -> local_theory -> (term list * thm list * thm list) * local_theory val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list - val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm -> - local_theory -> (term list * thm list * thm list) * local_theory end structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = struct -open Nominal_Permeq - -(* string list - type variables of a datatype - binding - name of the datatype - mixfix - its mixfix - (binding * typ list * mixfix) list - datatype constructors of the type -*) -type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list - - -(* term - is constant of the bn-function - int - is datatype number over which the bn-function is defined - int * term option - is number of the corresponding argument with possibly - recursive call with bn-function term -*) -type bn_info = term * int * (int * term option) list list - - -datatype bmode = Lst | Res | Set -datatype bclause = BC of bmode * (term option * int) list * int list +open Nominal_Permeq fun get_all_binders bclauses = bclauses @@ -136,22 +107,25 @@ |> order (op=) bn_funs (* ordered according to bn_functions *) end -fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy = +fun define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs lthy = if null raw_bn_funs then ([], [], [], [], lthy) else let + val RawDtInfo + {raw_dt_names, raw_dts, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info + val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs - Function_Common.default_config (pat_completeness_simp constr_thms) lthy + Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy - val (info, lthy2) = prove_termination_fun size_thms (Local_Theory.restore lthy1) + val (info, lthy2) = prove_termination_fun raw_size_thms (Local_Theory.restore lthy1) val {fs, simps, inducts, ...} = info val raw_bn_induct = (the inducts) val raw_bn_eqs = the simps val raw_bn_info = - prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs) + prep_bn_info lthy raw_dt_names raw_dts fs (map prop_of raw_bn_eqs) in (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) end @@ -255,9 +229,13 @@ 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 raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms size_simps lthy = +fun define_raw_fvs raw_dt_info bn_info bclausesss lthy = let - val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names + val RawDtInfo + {raw_dt_names, raw_tys, raw_cns_info, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = + raw_dt_info + + val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_dt_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 = raw_tys ~~ fv_frees @@ -270,16 +248,16 @@ val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) val fv_bn_map = bns ~~ fv_bn_frees - 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 fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) raw_cns_info bclausesss + val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map raw_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) val (_, lthy') = Function.add_function all_fun_names all_fun_eqs - Function_Common.default_config (pat_completeness_simp constr_thms) lthy + Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) lthy - val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy') + val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') val {fs, simps, inducts, ...} = info; @@ -325,11 +303,14 @@ map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info end -fun define_raw_bn_perms raw_tys bn_info cns_info cns_thms size_thms lthy = +fun define_raw_bn_perms raw_dt_info bn_info lthy = if null bn_info then ([], [], lthy) else let + val RawDtInfo + {raw_tys, raw_cns_info, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info + 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 perm_bn_names = map (prefix "permute_") bn_names @@ -338,7 +319,7 @@ val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys) val perm_bn_map = bns ~~ perm_bn_frees - val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map cns_info) bn_info + val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map raw_cns_info) bn_info val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs) @@ -346,9 +327,10 @@ val prod_simps = @{thms prod.inject HOL.simp_thms} val (_, lthy') = Function.add_function all_fun_names all_fun_eqs - Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy + Function_Common.default_config + (pat_completeness_simp (prod_simps @ raw_inject_thms @ raw_distinct_thms)) lthy - val (info, lthy'') = prove_termination_fun size_thms (Local_Theory.restore lthy') + val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') val {fs, simps, ...} = info; @@ -358,57 +340,6 @@ (fs, simps_exp, lthy'') end - -(** equivarance proofs **) - -val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} - -fun subproof_tac const_names simps = - SUBPROOF (fn {prems, context, ...} => - HEADGOAL - (simp_tac (HOL_basic_ss addsimps simps) - THEN' eqvt_tac context (eqvt_relaxed_config addexcls const_names) - THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym])))) - -fun prove_eqvt_tac insts ind_thms const_names simps ctxt = - HEADGOAL - (Object_Logic.full_atomize_tac - THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) - THEN_ALL_NEW subproof_tac const_names simps ctxt) - -fun mk_eqvt_goal pi const arg = - let - val lhs = mk_perm pi (const $ arg) - val rhs = const $ (mk_perm pi arg) - in - HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) - end - - -fun raw_prove_eqvt consts ind_thms simps ctxt = - if null consts then [] - else - let - val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt - val p = Free (p, @{typ perm}) - val arg_tys = - consts - |> map fastype_of - |> map domain_type - val (arg_names, ctxt'') = - Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt' - val args = map Free (arg_names ~~ arg_tys) - val goals = map2 (mk_eqvt_goal p) consts args - val insts = map (single o SOME) arg_names - val const_names = map (fst o dest_Const) consts - in - Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => - prove_eqvt_tac insts ind_thms const_names simps context) - |> ProofContext.export ctxt'' ctxt - end - - - (*** raw permutation functions ***) (** proves the two pt-type class properties **) @@ -483,17 +414,20 @@ end -fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy = +fun define_raw_perms raw_dt_info lthy = let - val perm_fn_names = full_ty_names + val RawDtInfo + {raw_dt_names, raw_tys, raw_ty_args, raw_all_cns, raw_induct_thm, ...} = raw_dt_info + + val perm_fn_names = raw_dt_names |> map Long_Name.base_name |> map (prefix "permute_") - val perm_fn_types = map perm_ty tys + val perm_fn_types = map perm_ty raw_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 perm_eqs = map (mk_perm_eq (raw_tys ~~ perm_fn_frees)) (flat raw_all_cns) fun tac _ (_, _, simps) = Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) @@ -506,11 +440,11 @@ val ((perm_funs, perm_eq_thms), lthy') = lthy |> Local_Theory.exit_global - |> Class.instantiation (full_ty_names, tvs, @{sort pt}) + |> Class.instantiation (raw_dt_names, raw_ty_args, @{sort pt}) |> Primrec.add_primrec perm_fn_binds perm_eqs - val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' - val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' + val perm_zero_thms = prove_permute_zero raw_induct_thm perm_eq_thms perm_funs lthy' + val perm_plus_thms = prove_permute_plus raw_induct_thm perm_eq_thms perm_funs lthy' in lthy' |> Class.prove_instantiation_exit_result morphism tac @@ -519,5 +453,54 @@ end +(** equivarance proofs **) + +val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} + +fun subproof_tac const_names simps = + SUBPROOF (fn {prems, context, ...} => + HEADGOAL + (simp_tac (HOL_basic_ss addsimps simps) + THEN' eqvt_tac context (eqvt_relaxed_config addexcls const_names) + THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym])))) + +fun prove_eqvt_tac insts ind_thms const_names simps ctxt = + HEADGOAL + (Object_Logic.full_atomize_tac + THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) + THEN_ALL_NEW subproof_tac const_names simps ctxt) + +fun mk_eqvt_goal pi const arg = + let + val lhs = mk_perm pi (const $ arg) + val rhs = const $ (mk_perm pi arg) + in + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) + end + + +fun raw_prove_eqvt consts ind_thms simps ctxt = + if null consts then [] + else + let + val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt + val p = Free (p, @{typ perm}) + val arg_tys = + consts + |> map fastype_of + |> map domain_type + val (arg_names, ctxt'') = + Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt' + val args = map Free (arg_names ~~ arg_tys) + val goals = map2 (mk_eqvt_goal p) consts args + val insts = map (single o SOME) arg_names + val const_names = map (fst o dest_Const) consts + in + Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => + prove_eqvt_tac insts ind_thms const_names simps context) + |> ProofContext.export ctxt'' ctxt + end + + end (* structure *)