diff -r 4049a2651dd9 -r 01ff621599bc Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Wed Jul 06 15:59:11 2011 +0200 +++ b/Nominal/nominal_dt_rawfuns.ML Thu Jul 07 16:16:42 2011 +0200 @@ -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 *)