# HG changeset patch # User urbanc # Date 1130510626 -7200 # Node ID 23e6cfda8c4b8261f3c4848899e77f2e771f08bd # Parent 685d95c793ff18909490e1978d77af87e5ac9bd2 Added (optional) arguments to the tactics perm_eq_simp and supports_simp. They now follow the "simp"-way and use the syntax: apply(supports_simp simp add: thms) etc. diff -r 685d95c793ff -r 23e6cfda8c4b src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Fri Oct 28 16:35:40 2005 +0200 +++ b/src/HOL/Nominal/Nominal.thy Fri Oct 28 16:43:46 2005 +0200 @@ -2288,6 +2288,7 @@ (*******************************) (* permutation equality tactic *) use "nominal_permeq.ML"; + method_setup perm_simp = {* perm_eq_meth *} {* tactic for deciding equalities involving permutations *} diff -r 685d95c793ff -r 23e6cfda8c4b src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Fri Oct 28 16:35:40 2005 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Fri Oct 28 16:43:46 2005 +0200 @@ -2,106 +2,121 @@ (* 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 -(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *) -val Expand_Fun_Eq_tac = - ("extensionality on functions", - EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) 1, REPEAT_DETERM (rtac allI 1)]); +(* pulls out dynamically a thm via the simpset *) +fun dynamic_thm ss name = + ProofContext.get_thm (Simplifier.the_context ss) (Name name); + +(* initial simplification step in the tactic *) +fun initial_simp_tac ss i = + let + val perm_swap = dynamic_thm ss "perm_swap"; + val perm_fresh = dynamic_thm ss "perm_fresh_fresh"; + val perm_bij = dynamic_thm ss "perm_bij"; + val ss' = ss addsimps [perm_swap,perm_fresh,perm_bij] + 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 *) -fun Apply_Perm_Compose_tac ctxt = +fun apply_perm_compose_tac ss i = + let + val perm_compose = dynamic_thm ss "perm_compose"; + in + ("analysing permutation compositions on the lhs",rtac (perm_compose RS trans) i) + end + + +(* applies the perm_eq_lam and perm_eq_app simplifications *) +fun apply_app_lam_simp_tac ss i = let - val perm_compose = PureThy.get_thm (ProofContext.theory_of ctxt) (Name ("perm_compose")); - in ("analysing permutation compositions",rtac (perm_compose RS trans) 1) - end; + val perm_app_eq = dynamic_thm ss "perm_app_eq"; + val perm_lam_eq = dynamic_thm ss "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", + (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st)); (* unfolds the definition of permutations applied to functions *) -fun Unfold_Perm_Fun_Def_tac ctxt = - let - val perm_fun_def = PureThy.get_thm (ProofContext.theory_of ctxt) (Name ("nominal.perm_fun_def")) - in ("unfolding of perms on functions", simp_tac (HOL_basic_ss addsimps [perm_fun_def]) 1) +fun unfold_perm_fun_def_tac i = + let + val perm_fun_def = thm "nominal.perm_fun_def" + in + ("unfolding of permutations on functions", + simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i) end - -(* applies the perm_eq_lam and perm_eq_app simplifications *) -fun Apply_SimProc_tac ctxt = - let - val thy = ProofContext.theory_of ctxt; - val perm_app_eq = PureThy.get_thm thy (Name ("perm_app_eq")); - val perm_lam_eq = PureThy.get_thm thy (Name ("perm_eq_lam")); - in - ("simplification of permutation on applications and lambdas", - asm_full_simp_tac (HOL_basic_ss addsimps [perm_app_eq,perm_lam_eq]) 1) - end; -(* applying Stefan's smart congruence tac *) -val Apply_Cong_tac = ("application of congruence", - (fn st => DatatypeAux.cong_tac 1 st handle Subscript => no_tac st)); - -(* initial simplification step in the tactic *) -fun Initial_Simp_tac thms ctxt = - let - val thy = ProofContext.theory_of ctxt; - val perm_swap = PureThy.get_thm thy (Name ("perm_swap")); - val perm_fresh = PureThy.get_thm thy (Name ("perm_fresh_fresh")); - val perm_bij = PureThy.get_thm thy (Name ("perm_bij")); - val simps = (local_simpset_of ctxt) addsimps (thms @ [perm_swap,perm_fresh,perm_bij]) - in - ("general simplification step", FIRST [rtac conjI 1, asm_full_simp_tac simps 1]) - end; - +(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *) +fun expand_fun_eq_tac i = + ("extensionality expansion of functions", + EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]); (* debugging *) fun DEBUG_tac (msg,tac) = - EVERY [print_tac ("before application of "^msg), CHANGED tac, print_tac ("after "^msg)]; + EVERY [CHANGED tac, print_tac ("after "^msg)]; fun NO_DEBUG_tac (_,tac) = CHANGED tac; (* Main Tactic *) + (* "repeating"-depth is set to 40 - this seems sufficient *) -fun perm_simp_tac tactical thms ctxt = - REPEAT_DETERM_N 40 - (FIRST[tactical (Initial_Simp_tac thms ctxt), - tactical (Apply_Perm_Compose_tac ctxt), - tactical (Apply_SimProc_tac ctxt), - tactical Apply_Cong_tac, - tactical (Unfold_Perm_Fun_Def_tac ctxt), - tactical Expand_Fun_Eq_tac]); +fun perm_simp_tac tactical ss i = + DETERM (REPEAT_DETERM_N 40 + (FIRST[tactical (initial_simp_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 unfolds first the support definition *) -(* and then applies perm_simp *) -fun supports_tac tactical thms ctxt = - let - val thy = ProofContext.theory_of ctxt; - val supports_def = PureThy.get_thm thy (Name ("nominal.op supports_def")); - val fresh_def = PureThy.get_thm thy (Name ("nominal.fresh_def")); - val fresh_prod = PureThy.get_thm thy (Name ("nominal.fresh_prod")); - val simps = [supports_def,symmetric fresh_def,fresh_prod]; - +(* tactic that first unfolds the support definition *) +(* and strips of intros, then applies perm_simp_tac *) +fun supports_tac tactical ss i = + let + val supports_def = thm "nominal.op supports_def"; + val fresh_def = thm "nominal.fresh_def"; + val fresh_prod = thm "nominal.fresh_prod"; + val simps = [supports_def,symmetric fresh_def,fresh_prod] in - EVERY [tactical ("unfolding of supports",simp_tac (HOL_basic_ss addsimps simps) 1), - tactical ("stripping of foralls " ,REPEAT_DETERM (rtac allI 1)), - tactical ("geting rid of the imp",rtac impI 1), - tactical ("eliminating conjuncts",REPEAT_DETERM (etac conjE 1)), - tactical ("applying perm_simp ",perm_simp_tac tactical thms ctxt)] + EVERY [tactical ("unfolding of supports ",simp_tac (HOL_basic_ss addsimps simps) i), + 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)] end; in -val perm_eq_meth = - Method.thms_ctxt_args - (fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (perm_simp_tac NO_DEBUG_tac thms ctxt))); +(* FIXME simp_modifiers' -val perm_eq_meth_debug = - Method.thms_ctxt_args - (fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (perm_simp_tac DEBUG_tac thms ctxt))); +(Markus needs to commit this) +*) + -val supports_meth = - Method.thms_ctxt_args - (fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (supports_tac NO_DEBUG_tac thms ctxt))); +fun simp_meth_setup tac = + Method.only_sectioned_args (Simplifier.simp_modifiers @ Splitter.split_modifiers) + (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of); -val supports_meth_debug = - Method.thms_ctxt_args - (fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (supports_tac DEBUG_tac thms ctxt))); +val perm_eq_meth = simp_meth_setup (perm_simp_tac NO_DEBUG_tac); +val perm_eq_meth_debug = simp_meth_setup (perm_simp_tac DEBUG_tac); +val supports_meth = simp_meth_setup (supports_tac NO_DEBUG_tac); +val supports_meth_debug = simp_meth_setup (supports_tac DEBUG_tac); end