improved the decision-procedure for permutations;
now uses a simproc
FIXME:
the simproc still needs to be adapted for arbitrary
atom types
--- a/src/HOL/Nominal/nominal_atoms.ML Sat Feb 25 15:19:47 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Sun Feb 26 22:24:05 2006 +0100
@@ -658,7 +658,8 @@
val pt_fresh_fresh = thm "nominal.pt_fresh_fresh";
val pt_bij = thm "nominal.pt_bij";
val pt_perm_compose = thm "nominal.pt_perm_compose";
- val perm_eq_app = thm "nominal.perm_eq_app";
+ val pt_perm_compose' = thm "nominal.pt_perm_compose'";
+ val perm_app = thm "nominal.pt_fun_app_eq";
val at_fresh = thm "nominal.at_fresh";
val at_calc = thms "nominal.at_calc";
val at_supp = thm "nominal.at_supp";
@@ -667,6 +668,8 @@
val fresh_left = thm "nominal.pt_fresh_left";
val fresh_bij_ineq = thm "nominal.pt_fresh_bij_ineq";
val fresh_bij = thm "nominal.pt_fresh_bij";
+ val pt_pi_rev = thm "nominal.pt_pi_rev";
+ val pt_rev_pi = thm "nominal.pt_rev_pi";
(* Now we collect and instantiate some lemmas w.r.t. all atom *)
(* types; this allows for example to use abs_perm (which is a *)
@@ -732,13 +735,18 @@
thy32
|> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
+ ||>> PureThy.add_thmss
+ let val thms1 = inst_pt_at [pt_pi_rev];
+ val thms2 = inst_pt_at [pt_rev_pi];
+ in [(("perm_pi_simp",thms1 @ thms2),[])] end
||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [pt_perm_compose];
val thms2 = instR cp1 (Library.flat cps');
in [(("perm_compose",thms1 @ thms2),[])] end
- ||>> PureThy.add_thmss [(("perm_app_eq", inst_pt_at [perm_eq_app]),[])]
+ ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])]
+ ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])]
||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
||>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])]
||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])]
--- a/src/HOL/Nominal/nominal_permeq.ML Sat Feb 25 15:19:47 2006 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Sun Feb 26 22:24:05 2006 +0100
@@ -2,38 +2,72 @@
(* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
-(* tries until depth 40 the following (in that order): *)
-(* *)
-(* - simplification plus analysing perm_swaps, perm_fresh_fresh, perm_bij *)
-(* - permutation compositions (on the left hand side of =) *)
-(* - simplification of permutation on applications and abstractions *)
-(* - analysing congruences (from Stefan Berghofer's datatype pkg) *)
-(* - unfolding permutation on functions *)
-(* - expanding equalities of functions *)
-(* *)
-(* for supports - it first unfolds the definitions and strips of intros *)
-
local
(* pulls out dynamically a thm via the simpset *)
fun dynamic_thms ss name =
ProofContext.get_thms (Simplifier.the_context ss) (Name name);
+fun dynamic_thm ss name =
+ ProofContext.get_thm (Simplifier.the_context ss) (Name name);
+(* FIXME: make it usable for all atom-types *)
(* initial simplification step in the tactic *)
-fun initial_simp_tac ss i =
+fun perm_eval_tac ss i =
let
+ val perm_eq_app = thm "nominal.pt_fun_app_eq";
+ val at_inst = dynamic_thm ss "at_name_inst";
+ val pt_inst = dynamic_thm ss "pt_name_inst";
+
+ fun perm_eval_simproc sg ss redex =
+ (case redex of
+ (* case pi o (f x) == (pi o f) (pi o x) *)
+ (* special treatment in cases of constants *)
+ (Const("nominal.perm",Type("fun",[Type("List.list",[Type("*",[ty,_])]),_])) $ pi $ (f $ x))
+ => let
+ val _ = warning ("type: "^Sign.string_of_typ (sign_of (the_context())) ty)
+ in
+
+ (case f of
+ (* nothing to do on constants *)
+ (* FIXME: proper treatment of constants *)
+ Const(_,_) => NONE
+ | (Const(_,_) $ _) => NONE
+ | ((Const(_,_) $ _) $ _) => NONE
+ | (((Const(_,_) $ _) $ _) $ _) => NONE
+ | _ =>
+ (* FIXME: analyse type here or at "pty"*)
+ SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection))
+ end
+
+ (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
+ | (Const("nominal.perm",_) $ pi $ (Abs _))
+ => let
+ val perm_fun_def = thm "nominal.perm_fun_def"
+ in SOME (perm_fun_def) end
+
+ (* no redex otherwise *)
+ | _ => NONE);
+
+ val perm_eval =
+ Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval"
+ ["nominal.perm pi x"] perm_eval_simproc;
+
(* these lemmas are created dynamically according to the atom types *)
- val perm_swap = dynamic_thms ss "perm_swap";
- val perm_fresh = dynamic_thms ss "perm_fresh_fresh";
- val perm_bij = dynamic_thms ss "perm_bij";
- val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij)
+ val perm_swap = dynamic_thms ss "perm_swap";
+ val perm_fresh = dynamic_thms ss "perm_fresh_fresh";
+ val perm_bij = dynamic_thms ss "perm_bij";
+ val perm_compose' = dynamic_thms ss "perm_compose'";
+ val perm_pi_simp = dynamic_thms ss "perm_pi_simp";
+ val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_compose'@perm_pi_simp)
+ addsimprocs [perm_eval];
+
in
("general simplification step", FIRST [rtac conjI i, asm_full_simp_tac ss' i])
end;
(* applies the perm_compose rule - this rule would loop in the simplifier *)
(* in case there are more atom-types we have to check every possible instance *)
-(* of perm_compose *)
+(* of perm_compose *)
fun apply_perm_compose_tac ss i =
let
val perm_compose = dynamic_thms ss "perm_compose";
@@ -42,18 +76,6 @@
("analysing permutation compositions on the lhs",FIRST (tacs))
end
-(* applies the perm_eq_lam and perm_eq_app simplifications *)
-(* FIXME: it seems the order of perm_app_eq and perm_lam_eq is *)
-(* significant *)
-fun apply_app_lam_simp_tac ss i =
- let
- val perm_app_eq = dynamic_thms ss "perm_app_eq";
- val perm_lam_eq = thm "nominal.perm_eq_lam"
- in
- ("simplification of permutations on applications and lambdas",
- asm_full_simp_tac (HOL_basic_ss addsimps (perm_app_eq@[perm_lam_eq])) i)
- end
-
(* applying Stefan's smart congruence tac *)
fun apply_cong_tac i =
("application of congruence",
@@ -80,18 +102,22 @@
(* Main Tactic *)
-(* "repeating"-depth is set to 40 - this seems sufficient *)
fun perm_simp_tac tactical ss i =
+ DETERM (tactical (perm_eval_tac ss i));
+
+(* perm_simp_tac plus additional tactics to decide *)
+(* support problems *)
+(* the "repeating"-depth is set to 40 - this seems sufficient *)
+fun perm_supports_tac tactical ss i =
DETERM (REPEAT_DETERM_N 40
- (FIRST[tactical (initial_simp_tac ss i),
+ (FIRST[tactical (perm_eval_tac ss i),
tactical (apply_perm_compose_tac ss i),
- tactical (apply_app_lam_simp_tac ss i),
tactical (apply_cong_tac i),
tactical (unfold_perm_fun_def_tac i),
tactical (expand_fun_eq_tac i)]));
-(* tactic that first unfolds the support definition *)
-(* and strips of intros, then applies perm_simp_tac *)
+(* tactic that first unfolds the support definition *)
+(* and strips off the intros, then applies perm_supports_tac *)
fun supports_tac tactical ss i =
let
val supports_def = thm "nominal.op supports_def";
@@ -103,7 +129,7 @@
tactical ("stripping of foralls " ,REPEAT_DETERM (rtac allI i)),
tactical ("geting rid of the imps",rtac impI i),
tactical ("eliminating conjuncts ",REPEAT_DETERM (etac conjE i)),
- tactical ("applying perm_simp ",perm_simp_tac tactical ss i)]
+ tactical ("applying perm_simp ",perm_supports_tac tactical ss i)]
end;
in