# HG changeset patch # User Christian Urban # Date 1335870964 -3600 # Node ID 51c475ceaf09c16d732ce2be1d2c7c764a5aa5c9 # Parent 31c64dd4c95a3f7a6ab6755c92062ecf4afab0fb# Parent 25c61cc06ae2d27699f7dc031a988f1f963e4cfa merged diff -r 31c64dd4c95a -r 51c475ceaf09 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon Apr 30 15:45:23 2012 +0100 +++ b/Nominal/Nominal2.thy Tue May 01 12:16:04 2012 +0100 @@ -53,7 +53,6 @@ ML {* val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) -val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) val simp_attr = Attrib.internal (K Simplifier.simp_add) val induct_attr = Attrib.internal (K Induct.induct_simp_add) *} @@ -313,15 +312,24 @@ val _ = trace_msg (K "Proving respectfulness...") val raw_funs_rsp_aux = raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) - - val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux + + val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp) raw_funs_rsp_aux + + fun match_const cnst th = + (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th = + fst (dest_Const cnst); + fun find_matching_rsp cnst = + hd (filter (fn th => match_const cnst th) raw_funs_rsp); + val raw_fv_rsp = map find_matching_rsp raw_fvs; + val raw_bn_rsp = map find_matching_rsp raw_bns; + val raw_fv_bn_rsp = map find_matching_rsp raw_fv_bns; val raw_size_rsp = raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |> map mk_funs_rsp val raw_constrs_rsp = - raw_constrs_rsp lthy5 alpha_result (flat raw_all_cns) (alpha_bn_imp_thms @ raw_funs_rsp_aux) + raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux) val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt @@ -330,59 +338,54 @@ val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps - (* noting the quot_respects lemmas *) - val (_, lthy6) = - Local_Theory.note ((Binding.empty, [rsp_attr]), - raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ - alpha_bn_rsp @ raw_perm_bn_rsp) lthy5 - val _ = trace_msg (K "Defining the quotient types...") val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts - - val (qty_infos, lthy7) = + + val (qty_infos, lthy7) = let val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result in - define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 + define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy5 end 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 + val qty_names = map Long_Name.base_name qty_full_names 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, @{thm TrueI})) - (get_cnstrs dts) raw_all_cns + (map2 o map2) (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) + (get_cnstrs dts) (map (op ~~) (raw_all_cns ~~ raw_constrs_rsp)) val qbns_descr = - map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns + map2 (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) bn_funs (raw_bns ~~ raw_bn_rsp) - val qfvs_descr = - map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_fvs + val qfvs_descr = + map2 (fn n => fn (t, th) => ("fv_" ^ n, t, NoSyn, th)) qty_names (raw_fvs ~~ raw_fv_rsp) - val qfv_bns_descr = - map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) - bn_funs raw_fv_bns + val qfv_bns_descr = + map2 (fn (b, _, _) => fn (t, th) => ("fv_" ^ Variable.check_name b, t, NoSyn, th)) + bn_funs (raw_fv_bns ~~ raw_fv_bn_rsp) val qalpha_bns_descr = let val AlphaResult {alpha_bn_trms, ...} = alpha_result in - map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) - bn_funs alpha_bn_trms + map2 (fn (b, _, _) => fn (t, th) => ("alpha_" ^ Variable.check_name b, t, NoSyn, th)) + bn_funs (alpha_bn_trms ~~ alpha_bn_rsp) end val qperm_descr = - map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, @{thm TrueI})) - qty_names raw_perm_funs + map2 (fn n => fn (t, th) => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, th)) + qty_names (raw_perm_funs ~~ (take (length raw_perm_funs) alpha_permute_rsp)) val qsize_descr = - map2 (fn n => fn t => ("size_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_size_trms + map2 (fn n => fn (t, th) => ("size_" ^ n, t, NoSyn, th)) qty_names + (raw_size_trms ~~ (take (length raw_size_trms) raw_size_rsp)) val qperm_bn_descr = - map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) - bn_funs raw_perm_bns + map2 (fn (b, _, _) => fn (t, th) => ("permute_" ^ Variable.check_name b, t, NoSyn, th)) + bn_funs (raw_perm_bns ~~ raw_perm_bn_rsp) val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8) = diff -r 31c64dd4c95a -r 51c475ceaf09 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Mon Apr 30 15:45:23 2012 +0100 +++ b/Nominal/nominal_dt_alpha.ML Tue May 01 12:16:04 2012 +0100 @@ -29,7 +29,7 @@ val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> thm list -> thm list val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list - val raw_constrs_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list + val raw_constrs_rsp: Proof.context -> alpha_result -> term list list -> thm list -> thm list list val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list @@ -749,9 +749,10 @@ |> Syntax.check_term ctxt |> HOLogic.mk_Trueprop in + map (fn constrs => Goal.prove_multi ctxt [] [] (map prep_goal constrs) (K (HEADGOAL - (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps))) + (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))) constrs end diff -r 31c64dd4c95a -r 51c475ceaf09 Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Mon Apr 30 15:45:23 2012 +0100 +++ b/Nominal/nominal_dt_quot.ML Tue May 01 12:16:04 2012 +0100 @@ -105,7 +105,7 @@ |> Local_Theory.exit_global |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) - val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 + val (_, lthy2) = define_qconsts qtys perm_specs lthy1 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2