# HG changeset patch # User Christian Urban # Date 1302698512 -3600 # Node ID 7ac5e5c86c7db65f469fe5a06ec01a2512e515a1 # Parent d3ad5dc11ab39db12fedb57f3b6b802d5ba7adca introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Mon Apr 11 02:25:25 2011 +0100 +++ b/Nominal/Ex/Lambda.thy Wed Apr 13 13:41:52 2011 +0100 @@ -2,6 +2,7 @@ imports "../Nominal2" begin + atom_decl name nominal_datatype lam = @@ -9,6 +10,17 @@ | App "lam" "lam" | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) +inductive + triv :: "lam \ nat \ bool" +where + Var: "triv (Var x) n" + +equivariance triv +nominal_inductive triv avoids Var : "{}::name set" +apply(auto simp add: fresh_star_def) +done + + text {* height function *} nominal_primrec @@ -494,7 +506,6 @@ - end diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Mon Apr 11 02:25:25 2011 +0100 +++ b/Nominal/nominal_dt_alpha.ML Wed Apr 13 13:41:52 2011 +0100 @@ -47,6 +47,8 @@ structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = struct +open Nominal_Permeq + fun lookup xs x = the (AList.lookup (op=) xs x) fun group xs = AList.group (op=) xs @@ -505,7 +507,7 @@ [ etac exi_neg, resolve_tac @{thms alpha_sym_eqvt}, asm_full_simp_tac (HOL_ss addsimps prod_simps), - Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, + eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl}, trans_prem_tac pred_names ctxt ] end @@ -560,7 +562,7 @@ resolve_tac @{thms alpha_trans_eqvt}, atac, aatac pred_names ctxt, - Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, + eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl}, asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) end diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Mon Apr 11 02:25:25 2011 +0100 +++ b/Nominal/nominal_dt_quot.ML Wed Apr 13 13:41:52 2011 +0100 @@ -49,6 +49,8 @@ structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = struct +open Nominal_Permeq + fun lookup xs x = the (AList.lookup (op=) xs x) @@ -172,7 +174,7 @@ val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} in EVERY' [ simp_tac ss1, - Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], + eqvt_tac ctxt (eqvt_strict_config addpres perm_simps), simp_tac ss2 ] end @@ -299,11 +301,12 @@ case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) | NONE => mk_bn_supp_abs_tac fv_fun + val eqvt_rconfig = eqvt_relaxed_config addpres (perm_simps @ fv_bn_eqvts) in EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), TRY o supp_abs_tac, TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), - TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], + TRY o eqvt_tac ctxt eqvt_rconfig, TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), TRY o asm_full_simp_tac (add_ss thms3), TRY o simp_tac (add_ss thms2), @@ -373,7 +376,7 @@ val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs val ss_tac = EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss), - TRY o Nominal_Permeq.eqvt_strict_tac ctxt' qbn_eqvts [], + TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts), TRY o asm_full_simp_tac HOL_basic_ss] in induct_prove qtys props qinduct (K ss_tac) ctxt' @@ -519,8 +522,8 @@ in [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) |> (if rec_flag - then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] - else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ] + then eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt) + else eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) ] end @@ -556,8 +559,8 @@ val (abs_eqs, peqs) = split_filter is_abs_eq eqs val fprops' = - map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops - @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops + map (eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) fprops + @ map (eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)) fprops (* for freshness conditions *) val tac1 = SOLVED' (EVERY' diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Mon Apr 11 02:25:25 2011 +0100 +++ b/Nominal/nominal_dt_rawfuns.ML Wed Apr 13 13:41:52 2011 +0100 @@ -40,6 +40,8 @@ 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 @@ -361,7 +363,7 @@ SUBPROOF (fn {prems, context, ...} => HEADGOAL (simp_tac (HOL_basic_ss addsimps simps) - THEN' Nominal_Permeq.eqvt_tac context [] const_names + 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 = diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_eqvt.ML --- a/Nominal/nominal_eqvt.ML Mon Apr 11 02:25:25 2011 +0100 +++ b/Nominal/nominal_eqvt.ML Wed Apr 13 13:41:52 2011 +0100 @@ -5,6 +5,7 @@ Automatic proofs for equivariance of inductive predicates. *) + signature NOMINAL_EQVT = sig val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic @@ -32,7 +33,6 @@ (** equivariance tactics **) val perm_boolE = @{thm permute_boolE} -val perm_cancel = @{thms permute_minus_cancel(2)} fun eqvt_rel_single_case_tac ctxt pred_names pi intro = let @@ -41,16 +41,18 @@ val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} + val eqvt_sconfig = + eqvt_strict_config addpres @{thms permute_minus_cancel(2)} addexcls pred_names in - eqvt_strict_tac ctxt [] pred_names THEN' + eqvt_tac ctxt (eqvt_strict_config addexcls pred_names) THEN' SUBPROOF (fn {prems, context as ctxt, ...} => let val prems' = map (transform_prem2 ctxt pred_names) prems val tac1 = resolve_tac prems' val tac2 = EVERY' [ rtac pi_intro_rule, - eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] + eqvt_tac ctxt eqvt_sconfig, resolve_tac prems' ] val tac3 = EVERY' [ rtac pi_intro_rule, - eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, + eqvt_tac ctxt eqvt_sconfig, simp_tac simps1, simp_tac simps2, resolve_tac prems'] in (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_inductive.ML --- a/Nominal/nominal_inductive.ML Mon Apr 11 02:25:25 2011 +0100 +++ b/Nominal/nominal_inductive.ML Wed Apr 13 13:41:52 2011 +0100 @@ -133,8 +133,18 @@ f x y z u v r s :: map7 f xs ys zs us vs rs ss (* local abbreviations *) -fun eqvt_stac ctxt = Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel} [] -fun eqvt_srule ctxt = Nominal_Permeq.eqvt_strict_rule ctxt @{thms permute_minus_cancel} [] + +local + open Nominal_Permeq +in +(* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) + +val eqvt_sconfig = (delposts eqvt_strict_config) addpres @{thms permute_minus_cancel} + +fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig +fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig + +end val all_elims = let diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_permeq.ML --- a/Nominal/nominal_permeq.ML Mon Apr 11 02:25:25 2011 +0100 +++ b/Nominal/nominal_permeq.ML Wed Apr 13 13:41:52 2011 +0100 @@ -3,14 +3,24 @@ Author: Brian Huffman *) +infix 4 addpres addposts addexcls + signature NOMINAL_PERMEQ = sig - val eqvt_rule: Proof.context -> thm list -> string list -> thm -> thm - val eqvt_strict_rule: Proof.context -> thm list -> string list -> thm -> thm + datatype eqvt_config = + Eqvt_Config of {strict_mode: bool, pre_thms: thm list, post_thms: thm list, excluded: string list} - val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic - val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic - + val eqvt_relaxed_config: eqvt_config + val eqvt_strict_config: eqvt_config + val addpres : (eqvt_config * thm list) -> eqvt_config + val addposts : (eqvt_config * thm list) -> eqvt_config + val addexcls : (eqvt_config * string list) -> eqvt_config + val delpres : eqvt_config -> eqvt_config + val delposts : eqvt_config -> eqvt_config + + val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm + val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic + val perm_simp_meth: thm list * string list -> Proof.context -> Method.method val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method val args_parser: (thm list * string list) context_parser @@ -21,10 +31,10 @@ (* -- eqvt_tac and eqvt_strict_tac take a list of theorems - which are first tried to simplify permutations +- eqvt_tac and eqvt_rule take a list of theorems which + are first tried to simplify permutations - the string list contains constants that should not be +- the string list contains constants that should not be analysed (for example there is no raw eqvt-lemma for the constant The); therefore it should not be analysed @@ -38,6 +48,52 @@ open Nominal_ThmDecls; +datatype eqvt_config = Eqvt_Config of + {strict_mode: bool, pre_thms: thm list, post_thms: thm list, excluded: string list} + +fun (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) addpres thms = + Eqvt_Config { strict_mode = strict_mode, + pre_thms = thms @ pre_thms, + post_thms = post_thms, + excluded = excluded } + +fun (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) addposts thms = + Eqvt_Config { strict_mode = strict_mode, + pre_thms = pre_thms, + post_thms = thms @ post_thms, + excluded = excluded } + +fun (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) addexcls excls = + Eqvt_Config { strict_mode = strict_mode, + pre_thms = pre_thms, + post_thms = post_thms, + excluded = excls @ excluded } + +fun delpres (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) = + Eqvt_Config { strict_mode = strict_mode, + pre_thms = [], + post_thms = post_thms, + excluded = excluded } + +fun delposts (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) = + Eqvt_Config { strict_mode = strict_mode, + pre_thms = pre_thms, + post_thms = [], + excluded = excluded } + +val eqvt_relaxed_config = + Eqvt_Config { strict_mode = false, + pre_thms = @{thms eqvt_bound}, + post_thms = @{thms permute_pure}, + excluded = [] } + +val eqvt_strict_config = + Eqvt_Config { strict_mode = true, + pre_thms = @{thms eqvt_bound}, + post_thms = @{thms permute_pure}, + excluded = [] } + + (* tracing infrastructure *) val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); @@ -119,53 +175,41 @@ end (* main conversion *) -fun main_eqvt_conv ctxt strict_flag user_thms excluded ctrm = +fun main_eqvt_conv ctxt config ctrm = let + val Eqvt_Config {strict_mode, pre_thms, post_thms, excluded} = config + val first_conv_wrapper = if trace_enabled ctxt then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) else Conv.first_conv - val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt - val post_thms = map safe_mk_equiv @{thms permute_pure} + val all_pre_thms = map safe_mk_equiv (pre_thms @ get_eqvts_raw_thms ctxt) + val all_post_thms = map safe_mk_equiv post_thms in first_conv_wrapper - [ Conv.rewrs_conv pre_thms, + [ Conv.rewrs_conv all_pre_thms, eqvt_apply_conv, eqvt_lambda_conv, - Conv.rewrs_conv post_thms, - progress_info_conv ctxt strict_flag excluded + Conv.rewrs_conv all_post_thms, + progress_info_conv ctxt strict_mode excluded ] ctrm end -(* the eqvt-tactics first eta-normalise goals in + +(* the eqvt-conversion first eta-normalises goals in order to avoid problems with inductions in the equivariance command. *) - -(* raises an error if some permutations cannot be eliminated *) -fun eqvt_strict_conv ctxt user_thms excluded = - Conv.top_conv - (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt true user_thms excluded)) ctxt - -(* prints a warning message if some permutations cannot be eliminated *) -fun eqvt_conv ctxt user_thms excluded = - Conv.top_conv - (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt false user_thms excluded)) ctxt - +fun eqvt_conv ctxt config = + Conv.top_conv (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt config)) ctxt -(* thms rewriters *) -fun eqvt_strict_rule ctxt user_thms excluded = - Conv.fconv_rule (eqvt_strict_conv ctxt user_thms excluded) - -fun eqvt_rule ctxt user_thms excluded = - Conv.fconv_rule (eqvt_conv ctxt user_thms excluded) +(* thms rewriter *) +fun eqvt_rule ctxt config = + Conv.fconv_rule (eqvt_conv ctxt config) -(* tactics *) -fun eqvt_strict_tac ctxt user_thms excluded = - CONVERSION (eqvt_strict_conv ctxt user_thms excluded) - -fun eqvt_tac ctxt user_thms excluded = - CONVERSION (eqvt_conv ctxt user_thms excluded) +(* tactic *) +fun eqvt_tac ctxt config = + CONVERSION (eqvt_conv ctxt config) (* setup of the configuration value *) val setup = @@ -183,10 +227,10 @@ val args_parser = add_thms_parser -- exclude_consts_parser -fun perm_simp_meth (thms, consts) ctxt = - SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) +fun perm_simp_meth (thms, consts) ctxt = + SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_relaxed_config addpres thms addexcls consts))) fun perm_strict_simp_meth (thms, consts) ctxt = - SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts)) + SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_strict_config addpres thms addexcls consts))) end; (* structure *)