--- a/Nominal/Ex/Lambda.thy Tue Apr 12 15:46:35 2011 +0800
+++ b/Nominal/Ex/Lambda.thy Wed Apr 13 13:44:25 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 \<Rightarrow> nat \<Rightarrow> 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
--- a/Nominal/nominal_dt_alpha.ML Tue Apr 12 15:46:35 2011 +0800
+++ b/Nominal/nominal_dt_alpha.ML Wed Apr 13 13:44:25 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
--- a/Nominal/nominal_dt_quot.ML Tue Apr 12 15:46:35 2011 +0800
+++ b/Nominal/nominal_dt_quot.ML Wed Apr 13 13:44:25 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'
--- a/Nominal/nominal_dt_rawfuns.ML Tue Apr 12 15:46:35 2011 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML Wed Apr 13 13:44:25 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 =
--- a/Nominal/nominal_eqvt.ML Tue Apr 12 15:46:35 2011 +0800
+++ b/Nominal/nominal_eqvt.ML Wed Apr 13 13:44:25 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
--- a/Nominal/nominal_inductive.ML Tue Apr 12 15:46:35 2011 +0800
+++ b/Nominal/nominal_inductive.ML Wed Apr 13 13:44:25 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
--- a/Nominal/nominal_permeq.ML Tue Apr 12 15:46:35 2011 +0800
+++ b/Nominal/nominal_permeq.ML Wed Apr 13 13:44:25 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 *)