author | berghofe |
Tue, 04 Jul 2006 15:26:56 +0200 | |
changeset 19987 | b97607d4d9a5 |
parent 19858 | d319e39a2e0e |
child 19993 | e0a5783d708f |
permissions | -rw-r--r-- |
19494 | 1 |
(* Title: HOL/Nominal/nominal_permeq.ML |
2 |
ID: $Id$ |
|
3 |
Author: Christian Urban, TU Muenchen |
|
17870 | 4 |
|
19494 | 5 |
Methods for simplifying permutations and |
6 |
for analysing equations involving permutations. |
|
7 |
*) |
|
17870 | 8 |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
9 |
signature NOMINAL_PERMEQ = |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
10 |
sig |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
11 |
val perm_simp_tac : simpset -> int -> tactic |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
12 |
val perm_full_simp_tac : simpset -> int -> tactic |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
13 |
val supports_tac : simpset -> int -> tactic |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
14 |
val finite_guess_tac : simpset -> int -> tactic |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
15 |
val fresh_guess_tac : simpset -> int -> tactic |
17870 | 16 |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
17 |
val perm_eq_meth : Method.src -> ProofContext.context -> Method.method |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
18 |
val perm_eq_meth_debug : Method.src -> ProofContext.context -> Method.method |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
19 |
val perm_full_eq_meth : Method.src -> ProofContext.context -> Method.method |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
20 |
val perm_full_eq_meth_debug : Method.src -> ProofContext.context -> Method.method |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
21 |
val supports_meth : Method.src -> ProofContext.context -> Method.method |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
22 |
val supports_meth_debug : Method.src -> ProofContext.context -> Method.method |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
23 |
val finite_gs_meth : Method.src -> ProofContext.context -> Method.method |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
24 |
val finite_gs_meth_debug : Method.src -> ProofContext.context -> Method.method |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
25 |
val fresh_gs_meth : Method.src -> ProofContext.context -> Method.method |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
26 |
val fresh_gs_meth_debug : Method.src -> ProofContext.context -> Method.method |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
27 |
end |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
28 |
|
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
29 |
structure NominalPermeq : NOMINAL_PERMEQ = |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
30 |
struct |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
31 |
|
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
32 |
(* pulls out dynamically a thm via the proof state *) |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
33 |
fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name); |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
34 |
fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) (Name name); |
18012 | 35 |
|
19477 | 36 |
(* a tactic simplyfying permutations *) |
19494 | 37 |
val perm_fun_def = thm "Nominal.perm_fun_def" |
38 |
val perm_eq_app = thm "Nominal.pt_fun_app_eq" |
|
19477 | 39 |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
40 |
fun perm_eval_tac ss i = ("general simplification step", fn st => |
18012 | 41 |
let |
19139 | 42 |
fun perm_eval_simproc sg ss redex = |
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
43 |
let |
19477 | 44 |
(* the "application" case below is only applicable when the head *) |
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
45 |
(* of f is not a constant or when it is a permuattion with two or *) |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
46 |
(* more arguments *) |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
47 |
fun applicable t = |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
48 |
(case (strip_comb t) of |
19494 | 49 |
(Const ("Nominal.perm",_),ts) => (length ts) >= 2 |
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
50 |
| (Const _,_) => false |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
51 |
| _ => true) |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
52 |
|
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
53 |
in |
19139 | 54 |
(case redex of |
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
55 |
(* case pi o (f x) == (pi o f) (pi o x) *) |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
56 |
(* special treatment according to the head of f *) |
19494 | 57 |
(Const("Nominal.perm", |
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
58 |
Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
59 |
(case (applicable f) of |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
60 |
false => NONE |
19163 | 61 |
| _ => |
62 |
let |
|
63 |
val name = Sign.base_name n |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
64 |
val at_inst = dynamic_thm st ("at_"^name^"_inst") |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
65 |
val pt_inst = dynamic_thm st ("pt_"^name^"_inst") |
19163 | 66 |
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end) |
19139 | 67 |
|
68 |
(* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *) |
|
19494 | 69 |
| (Const("Nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def) |
19139 | 70 |
|
71 |
(* no redex otherwise *) |
|
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
72 |
| _ => NONE) end |
19139 | 73 |
|
74 |
val perm_eval = |
|
75 |
Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" |
|
19494 | 76 |
["Nominal.perm pi x"] perm_eval_simproc; |
19139 | 77 |
|
19477 | 78 |
(* these lemmas are created dynamically according to the atom types *) |
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
79 |
val perm_swap = dynamic_thms st "perm_swap" |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
80 |
val perm_fresh = dynamic_thms st "perm_fresh_fresh" |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
81 |
val perm_bij = dynamic_thms st "perm_bij" |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
82 |
val perm_pi_simp = dynamic_thms st "perm_pi_simp" |
19477 | 83 |
val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp) |
84 |
in |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
85 |
asm_full_simp_tac (ss' addsimprocs [perm_eval]) i st |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
86 |
end); |
19477 | 87 |
|
88 |
(* applies the perm_compose rule such that *) |
|
89 |
(* *) |
|
90 |
(* pi o (pi' o lhs) = rhs *) |
|
91 |
(* *) |
|
92 |
(* is transformed to *) |
|
93 |
(* *) |
|
94 |
(* (pi o pi') o (pi' o lhs) = rhs *) |
|
95 |
(* *) |
|
96 |
(* this rule would loop in the simplifier, so some trick is used with *) |
|
97 |
(* generating perm_aux'es for the outermost permutation and then un- *) |
|
98 |
(* folding the definition *) |
|
99 |
val pt_perm_compose_aux = thm "pt_perm_compose_aux"; |
|
100 |
val cp1_aux = thm "cp1_aux"; |
|
101 |
val perm_aux_fold = thm "perm_aux_fold"; |
|
102 |
||
103 |
fun perm_compose_tac ss i = |
|
104 |
let |
|
105 |
fun perm_compose_simproc sg ss redex = |
|
106 |
(case redex of |
|
19494 | 107 |
(Const ("Nominal.perm", Type ("fun", [Type ("List.list", |
108 |
[Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", |
|
19477 | 109 |
Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ |
110 |
pi2 $ t)) => |
|
19350 | 111 |
let |
112 |
val tname' = Sign.base_name tname |
|
19477 | 113 |
val uname' = Sign.base_name uname |
19350 | 114 |
in |
19477 | 115 |
if pi1 <> pi2 then (* only apply the composition rule in this case *) |
116 |
if T = U then |
|
19350 | 117 |
SOME (Drule.instantiate' |
118 |
[SOME (ctyp_of sg (fastype_of t))] |
|
119 |
[SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)] |
|
120 |
(mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")), |
|
19477 | 121 |
PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux))) |
122 |
else |
|
123 |
SOME (Drule.instantiate' |
|
124 |
[SOME (ctyp_of sg (fastype_of t))] |
|
125 |
[SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)] |
|
126 |
(mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS |
|
127 |
cp1_aux))) |
|
19350 | 128 |
else NONE |
129 |
end |
|
130 |
| _ => NONE); |
|
19477 | 131 |
|
132 |
val perm_compose = |
|
19350 | 133 |
Simplifier.simproc (the_context()) "perm_compose" |
19494 | 134 |
["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc; |
19477 | 135 |
|
136 |
val ss' = Simplifier.theory_context (the_context ()) empty_ss |
|
137 |
||
18012 | 138 |
in |
19477 | 139 |
("analysing permutation compositions on the lhs", |
140 |
EVERY [rtac trans i, |
|
141 |
asm_full_simp_tac (ss' addsimprocs [perm_compose]) i, |
|
142 |
asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i]) |
|
18012 | 143 |
end |
144 |
||
145 |
(* applying Stefan's smart congruence tac *) |
|
146 |
fun apply_cong_tac i = |
|
147 |
("application of congruence", |
|
19477 | 148 |
(fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st)); |
17870 | 149 |
|
19477 | 150 |
(* unfolds the definition of permutations *) |
151 |
(* applied to functions such that *) |
|
152 |
(* *) |
|
153 |
(* pi o f = rhs *) |
|
154 |
(* *) |
|
155 |
(* is transformed to *) |
|
156 |
(* *) |
|
157 |
(* %x. pi o (f ((rev pi) o x)) = rhs *) |
|
18012 | 158 |
fun unfold_perm_fun_def_tac i = |
159 |
let |
|
19494 | 160 |
val perm_fun_def = thm "Nominal.perm_fun_def" |
18012 | 161 |
in |
162 |
("unfolding of permutations on functions", |
|
19477 | 163 |
rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i) |
17870 | 164 |
end |
165 |
||
19477 | 166 |
(* applies the ext-rule such that *) |
167 |
(* *) |
|
168 |
(* f = g goes to /\x. f x = g x *) |
|
169 |
fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i); |
|
17870 | 170 |
|
19477 | 171 |
(* FIXME FIXME FIXME *) |
172 |
(* should be able to analyse pi o fresh_fun () = fresh_fun instances *) |
|
173 |
fun fresh_fun_eqvt_tac i = |
|
174 |
let |
|
19494 | 175 |
val fresh_fun_equiv = thm "Nominal.fresh_fun_equiv_ineq" |
19477 | 176 |
in |
177 |
("fresh_fun equivariance", rtac (fresh_fun_equiv RS trans) i) |
|
178 |
end |
|
179 |
||
17870 | 180 |
(* debugging *) |
181 |
fun DEBUG_tac (msg,tac) = |
|
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
182 |
CHANGED (EVERY [tac, print_tac ("after "^msg)]); |
17870 | 183 |
fun NO_DEBUG_tac (_,tac) = CHANGED tac; |
184 |
||
19477 | 185 |
(* Main Tactics *) |
18012 | 186 |
fun perm_simp_tac tactical ss i = |
19139 | 187 |
DETERM (tactical (perm_eval_tac ss i)); |
188 |
||
19477 | 189 |
(* perm_full_simp_tac is perm_simp_tac plus additional tactics *) |
190 |
(* to decide equation that come from support problems *) |
|
191 |
(* since it contains looping rules the "recursion" - depth is set *) |
|
192 |
(* to 10 - this seems to be sufficient in most cases *) |
|
193 |
fun perm_full_simp_tac tactical ss = |
|
194 |
let fun perm_full_simp_tac_aux tactical ss n = |
|
195 |
if n=0 then K all_tac |
|
196 |
else DETERM o |
|
197 |
(FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i), |
|
198 |
fn i => tactical (perm_eval_tac ss i), |
|
199 |
fn i => tactical (perm_compose_tac ss i), |
|
200 |
fn i => tactical (apply_cong_tac i), |
|
201 |
fn i => tactical (unfold_perm_fun_def_tac i), |
|
202 |
fn i => tactical (ext_fun_tac i), |
|
203 |
fn i => tactical (fresh_fun_eqvt_tac i)] |
|
204 |
THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n-1)))) |
|
205 |
in perm_full_simp_tac_aux tactical ss 10 end; |
|
19151 | 206 |
|
19477 | 207 |
(* tactic that first unfolds the support definition *) |
208 |
(* and strips off the intros, then applies perm_full_simp_tac *) |
|
18012 | 209 |
fun supports_tac tactical ss i = |
210 |
let |
|
19494 | 211 |
val supports_def = thm "Nominal.op supports_def"; |
212 |
val fresh_def = thm "Nominal.fresh_def"; |
|
213 |
val fresh_prod = thm "Nominal.fresh_prod"; |
|
18012 | 214 |
val simps = [supports_def,symmetric fresh_def,fresh_prod] |
17870 | 215 |
in |
19477 | 216 |
EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i), |
217 |
tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)), |
|
218 |
tactical ("geting rid of the imps ", rtac impI i), |
|
219 |
tactical ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)), |
|
220 |
tactical ("applying perm_full_simp ", perm_full_simp_tac tactical ss i |
|
221 |
(*perm_simp_tac tactical ss i*))] |
|
17870 | 222 |
end; |
223 |
||
19151 | 224 |
|
19477 | 225 |
(* tactic that guesses the finite-support of a goal *) |
226 |
(* it collects all free variables and tries to show *) |
|
227 |
(* that the support of these free variables (op supports) *) |
|
228 |
(* the goal *) |
|
19151 | 229 |
fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs |
230 |
| collect_vars i (v as Free _) vs = v ins vs |
|
231 |
| collect_vars i (v as Var _) vs = v ins vs |
|
232 |
| collect_vars i (Const _) vs = vs |
|
233 |
| collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs |
|
234 |
| collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs); |
|
235 |
||
236 |
val supports_rule = thm "supports_finite"; |
|
237 |
||
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
238 |
val supp_prod = thm "supp_prod"; |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
239 |
val supp_unit = thm "supp_unit"; |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
240 |
|
19151 | 241 |
fun finite_guess_tac tactical ss i st = |
242 |
let val goal = List.nth(cprems_of st, i-1) |
|
243 |
in |
|
244 |
case Logic.strip_assums_concl (term_of goal) of |
|
19494 | 245 |
_ $ (Const ("op :", _) $ (Const ("Nominal.supp", T) $ x) $ |
19151 | 246 |
Const ("Finite_Set.Finites", _)) => |
247 |
let |
|
248 |
val cert = Thm.cterm_of (sign_of_thm st); |
|
249 |
val ps = Logic.strip_params (term_of goal); |
|
250 |
val Ts = rev (map snd ps); |
|
251 |
val vs = collect_vars 0 x []; |
|
252 |
val s = foldr (fn (v, s) => |
|
253 |
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) |
|
254 |
HOLogic.unit vs; |
|
255 |
val s' = list_abs (ps, |
|
19494 | 256 |
Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s); |
19151 | 257 |
val supports_rule' = Thm.lift_rule goal supports_rule; |
258 |
val _ $ (_ $ S $ _) = |
|
259 |
Logic.strip_assums_concl (hd (prems_of supports_rule')); |
|
260 |
val supports_rule'' = Drule.cterm_instantiate |
|
261 |
[(cert (head_of S), cert s')] supports_rule' |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
262 |
val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites.emptyI] |
19151 | 263 |
in |
264 |
(tactical ("guessing of the right supports-set", |
|
265 |
EVERY [compose_tac (false, supports_rule'', 2) i, |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
266 |
asm_full_simp_tac ss' (i+1), |
19151 | 267 |
supports_tac tactical ss i])) st |
268 |
end |
|
269 |
| _ => Seq.empty |
|
270 |
end |
|
271 |
handle Subscript => Seq.empty |
|
272 |
||
19857 | 273 |
val supports_fresh_rule = thm "supports_fresh"; |
274 |
||
275 |
fun fresh_guess_tac tactical ss i st = |
|
276 |
let |
|
277 |
val goal = List.nth(cprems_of st, i-1) |
|
278 |
in |
|
279 |
case Logic.strip_assums_concl (term_of goal) of |
|
280 |
_ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => |
|
281 |
let |
|
282 |
val cert = Thm.cterm_of (sign_of_thm st); |
|
283 |
val ps = Logic.strip_params (term_of goal); |
|
284 |
val Ts = rev (map snd ps); |
|
285 |
val vs = collect_vars 0 t []; |
|
286 |
val s = foldr (fn (v, s) => |
|
287 |
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) |
|
288 |
HOLogic.unit vs; |
|
289 |
val s' = list_abs (ps, |
|
290 |
Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s); |
|
291 |
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule; |
|
292 |
val _ $ (_ $ S $ _) = |
|
293 |
Logic.strip_assums_concl (hd (prems_of supports_fresh_rule')); |
|
294 |
val supports_fresh_rule'' = Drule.cterm_instantiate |
|
295 |
[(cert (head_of S), cert s')] supports_fresh_rule' |
|
19858 | 296 |
val fresh_def = thm "Nominal.fresh_def"; |
297 |
val fresh_prod = thm "Nominal.fresh_prod"; |
|
298 |
val fresh_unit = thm "Nominal.fresh_unit"; |
|
299 |
val simps = [symmetric fresh_def,fresh_prod,fresh_unit] |
|
19857 | 300 |
in |
301 |
(tactical ("guessing of the right set that supports the goal", |
|
19858 | 302 |
EVERY [compose_tac (false, supports_fresh_rule'', 3) i, |
303 |
asm_full_simp_tac (ss addsimps simps) (i+2), |
|
304 |
asm_full_simp_tac ss (i+1), |
|
305 |
supports_tac tactical ss i])) st |
|
19857 | 306 |
end |
307 |
| _ => Seq.empty |
|
308 |
end |
|
309 |
handle Subscript => Seq.empty |
|
310 |
||
18012 | 311 |
fun simp_meth_setup tac = |
18046
b7389981170b
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
urbanc
parents:
18012
diff
changeset
|
312 |
Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers) |
18012 | 313 |
(Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of); |
17870 | 314 |
|
19477 | 315 |
val perm_eq_meth = simp_meth_setup (perm_simp_tac NO_DEBUG_tac); |
316 |
val perm_eq_meth_debug = simp_meth_setup (perm_simp_tac DEBUG_tac); |
|
317 |
val perm_full_eq_meth = simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac); |
|
318 |
val perm_full_eq_meth_debug = simp_meth_setup (perm_full_simp_tac DEBUG_tac); |
|
319 |
val supports_meth = simp_meth_setup (supports_tac NO_DEBUG_tac); |
|
320 |
val supports_meth_debug = simp_meth_setup (supports_tac DEBUG_tac); |
|
321 |
val finite_gs_meth = simp_meth_setup (finite_guess_tac NO_DEBUG_tac); |
|
322 |
val finite_gs_meth_debug = simp_meth_setup (finite_guess_tac DEBUG_tac); |
|
19857 | 323 |
val fresh_gs_meth = simp_meth_setup (fresh_guess_tac NO_DEBUG_tac); |
324 |
val fresh_gs_meth_debug = simp_meth_setup (fresh_guess_tac DEBUG_tac); |
|
17870 | 325 |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
326 |
(* FIXME: get rid of "debug" versions? *) |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
327 |
val perm_simp_tac = perm_simp_tac NO_DEBUG_tac; |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
328 |
val perm_full_simp_tac = perm_full_simp_tac NO_DEBUG_tac; |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
329 |
val supports_tac = supports_tac NO_DEBUG_tac; |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
330 |
val finite_guess_tac = finite_guess_tac NO_DEBUG_tac; |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
331 |
val fresh_guess_tac = fresh_guess_tac NO_DEBUG_tac; |
17870 | 332 |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
333 |
end |