--- 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