1.1 --- a/src/HOL/Nominal/Nominal.thy Mon Sep 22 15:26:14 2008 +0200
1.2 +++ b/src/HOL/Nominal/Nominal.thy Mon Sep 22 19:46:24 2008 +0200
1.3 @@ -3495,12 +3495,12 @@
1.4 {* NominalPermeq.perm_simp_meth_debug *}
1.5 {* simp rules and simprocs for analysing permutations including debugging facilities *}
1.6
1.7 -method_setup perm_full_simp =
1.8 - {* NominalPermeq.perm_full_simp_meth *}
1.9 +method_setup perm_extend_simp =
1.10 + {* NominalPermeq.perm_extend_simp_meth *}
1.11 {* tactic for deciding equalities involving permutations *}
1.12
1.13 -method_setup perm_full_simp_debug =
1.14 - {* NominalPermeq.perm_full_simp_meth_debug *}
1.15 +method_setup perm_extend_simp_debug =
1.16 + {* NominalPermeq.perm_extend_simp_meth_debug *}
1.17 {* tactic for deciding equalities involving permutations including debugging facilities *}
1.18
1.19 method_setup supports_simp =
2.1 --- a/src/HOL/Nominal/nominal_permeq.ML Mon Sep 22 15:26:14 2008 +0200
2.2 +++ b/src/HOL/Nominal/nominal_permeq.ML Mon Sep 22 19:46:24 2008 +0200
2.3 @@ -31,15 +31,15 @@
2.4 val perm_simproc_app : simproc
2.5
2.6 val perm_simp_tac : simpset -> int -> tactic
2.7 - val perm_full_simp_tac : simpset -> int -> tactic
2.8 + val perm_extend_simp_tac : simpset -> int -> tactic
2.9 val supports_tac : simpset -> int -> tactic
2.10 val finite_guess_tac : simpset -> int -> tactic
2.11 val fresh_guess_tac : simpset -> int -> tactic
2.12
2.13 val perm_simp_meth : Method.src -> Proof.context -> Proof.method
2.14 val perm_simp_meth_debug : Method.src -> Proof.context -> Proof.method
2.15 - val perm_full_simp_meth : Method.src -> Proof.context -> Proof.method
2.16 - val perm_full_simp_meth_debug : Method.src -> Proof.context -> Proof.method
2.17 + val perm_extend_simp_meth : Method.src -> Proof.context -> Proof.method
2.18 + val perm_extend_simp_meth_debug : Method.src -> Proof.context -> Proof.method
2.19 val supports_meth : Method.src -> Proof.context -> Proof.method
2.20 val supports_meth_debug : Method.src -> Proof.context -> Proof.method
2.21 val finite_guess_meth : Method.src -> Proof.context -> Proof.method
2.22 @@ -141,8 +141,10 @@
2.23 val perm_simproc_fun = Simplifier.simproc (the_context ()) "perm_simproc_fun"
2.24 ["Nominal.perm pi x"] perm_simproc_fun';
2.25
2.26 -(* function for simplyfying permutations *)
2.27 -fun perm_simp_gen dyn_thms eqvt_thms ss i =
2.28 +(* function for simplyfying permutations *)
2.29 +(* stac contains the simplifiation tactic that is *)
2.30 +(* applied (see (no_asm) options below *)
2.31 +fun perm_simp_gen stac dyn_thms eqvt_thms ss i =
2.32 ("general simplification of permutations", fn st =>
2.33 let
2.34 val ss' = Simplifier.theory_context (theory_of_thm st) ss
2.35 @@ -151,28 +153,34 @@
2.36 addcongs strong_congs
2.37 addsimprocs [perm_simproc_fun, perm_simproc_app]
2.38 in
2.39 - asm_full_simp_tac ss' i st
2.40 + stac ss' i st
2.41 end);
2.42
2.43 (* general simplification of permutations and permutation that arose from eqvt-problems *)
2.44 -fun perm_simp ss =
2.45 +fun perm_simp stac ss =
2.46 let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
2.47 in
2.48 - perm_simp_gen simps [] ss
2.49 + perm_simp_gen stac simps [] ss
2.50 end;
2.51
2.52 -fun eqvt_simp ss =
2.53 +fun eqvt_simp stac ss =
2.54 let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
2.55 val eqvts_thms = NominalThmDecls.get_eqvt_thms (Simplifier.the_context ss);
2.56 in
2.57 - perm_simp_gen simps eqvts_thms ss
2.58 + perm_simp_gen stac simps eqvts_thms ss
2.59 end;
2.60
2.61
2.62 (* main simplification tactics for permutations *)
2.63 -fun perm_simp_tac tactical ss i = DETERM (tactical (perm_simp ss i));
2.64 -fun eqvt_simp_tac tactical ss i = DETERM (tactical (eqvt_simp ss i));
2.65 +fun perm_simp_tac_gen_i stac tactical ss i = DETERM (tactical (perm_simp stac ss i));
2.66 +fun eqvt_simp_tac_gen_i stac tactical ss i = DETERM (tactical (eqvt_simp stac ss i));
2.67
2.68 +val perm_simp_tac_i = perm_simp_tac_gen_i simp_tac
2.69 +val perm_asm_simp_tac_i = perm_simp_tac_gen_i asm_simp_tac
2.70 +val perm_full_simp_tac_i = perm_simp_tac_gen_i full_simp_tac
2.71 +val perm_asm_lr_simp_tac_i = perm_simp_tac_gen_i asm_lr_simp_tac
2.72 +val perm_asm_full_simp_tac_i = perm_simp_tac_gen_i asm_full_simp_tac
2.73 +val eqvt_asm_full_simp_tac_i = eqvt_simp_tac_gen_i asm_full_simp_tac
2.74
2.75 (* applies the perm_compose rule such that *)
2.76 (* pi o (pi' o lhs) = rhs *)
2.77 @@ -243,28 +251,28 @@
2.78 fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
2.79
2.80
2.81 -(* perm_full_simp_tac is perm_simp plus additional tactics *)
2.82 +(* perm_extend_simp_tac_i is perm_simp plus additional tactics *)
2.83 (* to decide equation that come from support problems *)
2.84 (* since it contains looping rules the "recursion" - depth is set *)
2.85 (* to 10 - this seems to be sufficient in most cases *)
2.86 -fun perm_full_simp_tac tactical ss =
2.87 - let fun perm_full_simp_tac_aux tactical ss n =
2.88 +fun perm_extend_simp_tac_i tactical ss =
2.89 + let fun perm_extend_simp_tac_aux tactical ss n =
2.90 if n=0 then K all_tac
2.91 else DETERM o
2.92 (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
2.93 - fn i => tactical (perm_simp ss i),
2.94 + fn i => tactical (perm_simp asm_full_simp_tac ss i),
2.95 fn i => tactical (perm_compose_tac ss i),
2.96 fn i => tactical (apply_cong_tac i),
2.97 fn i => tactical (unfold_perm_fun_def_tac i),
2.98 fn i => tactical (ext_fun_tac i)]
2.99 - THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n-1))))
2.100 - in perm_full_simp_tac_aux tactical ss 10 end;
2.101 + THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ss (n-1))))
2.102 + in perm_extend_simp_tac_aux tactical ss 10 end;
2.103
2.104
2.105 (* tactic that tries to solve "supports"-goals; first it *)
2.106 (* unfolds the support definition and strips off the *)
2.107 (* intros, then applies eqvt_simp_tac *)
2.108 -fun supports_tac tactical ss i =
2.109 +fun supports_tac_i tactical ss i =
2.110 let
2.111 val simps = [supports_def,symmetric fresh_def,fresh_prod]
2.112 in
2.113 @@ -272,7 +280,7 @@
2.114 tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)),
2.115 tactical ("geting rid of the imps ", rtac impI i),
2.116 tactical ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)),
2.117 - tactical ("applying eqvt_simp ", eqvt_simp_tac tactical ss i )]
2.118 + tactical ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ss i )]
2.119 end;
2.120
2.121
2.122 @@ -287,7 +295,7 @@
2.123 | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
2.124 | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
2.125
2.126 -fun finite_guess_tac tactical ss i st =
2.127 +fun finite_guess_tac_i tactical ss i st =
2.128 let val goal = List.nth(cprems_of st, i-1)
2.129 in
2.130 case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of
2.131 @@ -314,7 +322,7 @@
2.132 (tactical ("guessing of the right supports-set",
2.133 EVERY [compose_tac (false, supports_rule'', 2) i,
2.134 asm_full_simp_tac ss' (i+1),
2.135 - supports_tac tactical ss i])) st
2.136 + supports_tac_i tactical ss i])) st
2.137 end
2.138 | _ => Seq.empty
2.139 end
2.140 @@ -324,7 +332,7 @@
2.141 (* tactic that guesses whether an atom is fresh for an expression *)
2.142 (* it first collects all free variables and tries to show that the *)
2.143 (* support of these free variables (op supports) the goal *)
2.144 -fun fresh_guess_tac tactical ss i st =
2.145 +fun fresh_guess_tac_i tactical ss i st =
2.146 let
2.147 val goal = List.nth(cprems_of st, i-1)
2.148 val fin_supp = dynamic_thms st ("fin_supp")
2.149 @@ -354,7 +362,7 @@
2.150 (EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
2.151 asm_full_simp_tac ss1 (i+2),
2.152 asm_full_simp_tac ss2 (i+1),
2.153 - supports_tac tactical ss i]))) st
2.154 + supports_tac_i tactical ss i]))) st
2.155 end
2.156 (* when a term-constructor contains more than one binder, it is useful *)
2.157 (* in nominal_primrecs to try whether the goal can be solved by an hammer *)
2.158 @@ -363,6 +371,43 @@
2.159 end
2.160 handle Subscript => Seq.empty;
2.161
2.162 +val eqvt_simp_tac = eqvt_asm_full_simp_tac_i NO_DEBUG_tac;
2.163 +
2.164 +val perm_simp_tac = perm_asm_full_simp_tac_i NO_DEBUG_tac;
2.165 +val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG_tac;
2.166 +val supports_tac = supports_tac_i NO_DEBUG_tac;
2.167 +val finite_guess_tac = finite_guess_tac_i NO_DEBUG_tac;
2.168 +val fresh_guess_tac = fresh_guess_tac_i NO_DEBUG_tac;
2.169 +
2.170 +val dperm_simp_tac = perm_asm_full_simp_tac_i DEBUG_tac;
2.171 +val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG_tac;
2.172 +val dsupports_tac = supports_tac_i DEBUG_tac;
2.173 +val dfinite_guess_tac = finite_guess_tac_i DEBUG_tac;
2.174 +val dfresh_guess_tac = fresh_guess_tac_i DEBUG_tac;
2.175 +
2.176 +(* Code opied from the Simplifer for setting up the perm_simp method *)
2.177 +(* behaves nearly identical to the simp-method, for example can handle *)
2.178 +(* options like (no_asm) etc. *)
2.179 +val no_asmN = "no_asm";
2.180 +val no_asm_useN = "no_asm_use";
2.181 +val no_asm_simpN = "no_asm_simp";
2.182 +val asm_lrN = "asm_lr";
2.183 +
2.184 +val perm_simp_options =
2.185 + (Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG_tac) ||
2.186 + Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG_tac) ||
2.187 + Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG_tac) ||
2.188 + Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) ||
2.189 + Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
2.190 +
2.191 +fun perm_simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
2.192 + HEADGOAL (Method.insert_tac (prems @ facts) THEN'
2.193 + ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
2.194 +
2.195 +val perm_simp_meth = Method.sectioned_args
2.196 + (Args.bang_facts -- Scan.lift perm_simp_options)
2.197 + (Simplifier.simp_modifiers') perm_simp_method
2.198 +
2.199 (* setup so that the simpset is used which is active at the moment when the tactic is called *)
2.200 fun local_simp_meth_setup tac =
2.201 Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
2.202 @@ -376,23 +421,15 @@
2.203 (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
2.204 (fn _ => Method.SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
2.205
2.206 +val perm_simp_meth_debug = local_simp_meth_setup dperm_simp_tac;
2.207 +val perm_extend_simp_meth = local_simp_meth_setup perm_extend_simp_tac;
2.208 +val perm_extend_simp_meth_debug = local_simp_meth_setup dperm_extend_simp_tac;
2.209 +val supports_meth = local_simp_meth_setup supports_tac;
2.210 +val supports_meth_debug = local_simp_meth_setup dsupports_tac;
2.211
2.212 -val perm_simp_meth = local_simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
2.213 -val perm_simp_meth_debug = local_simp_meth_setup (perm_simp_tac DEBUG_tac);
2.214 -val perm_full_simp_meth = local_simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac);
2.215 -val perm_full_simp_meth_debug = local_simp_meth_setup (perm_full_simp_tac DEBUG_tac);
2.216 -val supports_meth = local_simp_meth_setup (supports_tac NO_DEBUG_tac);
2.217 -val supports_meth_debug = local_simp_meth_setup (supports_tac DEBUG_tac);
2.218 -
2.219 -val finite_guess_meth = basic_simp_meth_setup false (finite_guess_tac NO_DEBUG_tac);
2.220 -val finite_guess_meth_debug = basic_simp_meth_setup true (finite_guess_tac DEBUG_tac);
2.221 -val fresh_guess_meth = basic_simp_meth_setup false (fresh_guess_tac NO_DEBUG_tac);
2.222 -val fresh_guess_meth_debug = basic_simp_meth_setup true (fresh_guess_tac DEBUG_tac);
2.223 -
2.224 -val perm_simp_tac = perm_simp_tac NO_DEBUG_tac;
2.225 -val perm_full_simp_tac = perm_full_simp_tac NO_DEBUG_tac;
2.226 -val supports_tac = supports_tac NO_DEBUG_tac;
2.227 -val finite_guess_tac = finite_guess_tac NO_DEBUG_tac;
2.228 -val fresh_guess_tac = fresh_guess_tac NO_DEBUG_tac;
2.229 +val finite_guess_meth = basic_simp_meth_setup false finite_guess_tac;
2.230 +val finite_guess_meth_debug = basic_simp_meth_setup true dfinite_guess_tac;
2.231 +val fresh_guess_meth = basic_simp_meth_setup false fresh_guess_tac;
2.232 +val fresh_guess_meth_debug = basic_simp_meth_setup true dfresh_guess_tac;
2.233
2.234 end