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