# HG changeset patch # User urbanc # Date 1140989045 -3600 # Node ID af69e41eab5d5a6bb66bca60c867bb442579fa03 # Parent 42ff710d432f49176641d0fb8fb0e16ebdc374fd improved the decision-procedure for permutations; now uses a simproc FIXME: the simproc still needs to be adapted for arbitrary atom types diff -r 42ff710d432f -r af69e41eab5d src/HOL/Nominal/nominal_atoms.ML --- 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),[])] diff -r 42ff710d432f -r af69e41eab5d src/HOL/Nominal/nominal_permeq.ML --- 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