author | haftmann |
Sat, 08 Nov 2014 16:53:26 +0100 | |
changeset 58952 | 5d82cdef6c1b |
parent 56492 | 29a1d14b944c |
child 58956 | a816aa3ff391 |
permissions | -rw-r--r-- |
19494 | 1 |
(* Title: HOL/Nominal/nominal_permeq.ML |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
2 |
Author: Christian Urban, TU Muenchen |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
3 |
Author: Julien Narboux, TU Muenchen |
17870 | 4 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
5 |
Methods for simplifying permutations and for analysing equations |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
6 |
involving permutations. |
19494 | 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 |
25997 | 30 |
val perm_simproc_fun : simproc |
31 |
val perm_simproc_app : simproc |
|
32 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
33 |
val perm_simp_tac : Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
34 |
val perm_extend_simp_tac : Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
35 |
val supports_tac : Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
36 |
val finite_guess_tac : Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
37 |
val fresh_guess_tac : Proof.context -> int -> tactic |
17870 | 38 |
|
30549 | 39 |
val perm_simp_meth : (Proof.context -> Proof.method) context_parser |
40 |
val perm_simp_meth_debug : (Proof.context -> Proof.method) context_parser |
|
41 |
val perm_extend_simp_meth : (Proof.context -> Proof.method) context_parser |
|
42 |
val perm_extend_simp_meth_debug : (Proof.context -> Proof.method) context_parser |
|
43 |
val supports_meth : (Proof.context -> Proof.method) context_parser |
|
44 |
val supports_meth_debug : (Proof.context -> Proof.method) context_parser |
|
45 |
val finite_guess_meth : (Proof.context -> Proof.method) context_parser |
|
46 |
val finite_guess_meth_debug : (Proof.context -> Proof.method) context_parser |
|
47 |
val fresh_guess_meth : (Proof.context -> Proof.method) context_parser |
|
48 |
val fresh_guess_meth_debug : (Proof.context -> Proof.method) context_parser |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
49 |
end |
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 |
structure NominalPermeq : NOMINAL_PERMEQ = |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
52 |
struct |
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
53 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
54 |
(* some lemmas needed below *) |
24519 | 55 |
val finite_emptyI = @{thm "finite.emptyI"}; |
56 |
val finite_Un = @{thm "finite_Un"}; |
|
57 |
val conj_absorb = @{thm "conj_absorb"}; |
|
58 |
val not_false = @{thm "not_False_eq_True"} |
|
44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
43278
diff
changeset
|
59 |
val perm_fun_def = Simpdata.mk_eq @{thm "Nominal.perm_fun_def"}; |
24519 | 60 |
val perm_eq_app = @{thm "Nominal.pt_fun_app_eq"}; |
44684
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
43278
diff
changeset
|
61 |
val supports_def = Simpdata.mk_eq @{thm "Nominal.supports_def"}; |
8dde3352d5c4
assert Pure equations for theorem references; tuned
haftmann
parents:
43278
diff
changeset
|
62 |
val fresh_def = Simpdata.mk_eq @{thm "Nominal.fresh_def"}; |
24519 | 63 |
val fresh_prod = @{thm "Nominal.fresh_prod"}; |
64 |
val fresh_unit = @{thm "Nominal.fresh_unit"}; |
|
65 |
val supports_rule = @{thm "supports_finite"}; |
|
66 |
val supp_prod = @{thm "supp_prod"}; |
|
67 |
val supp_unit = @{thm "supp_unit"}; |
|
68 |
val pt_perm_compose_aux = @{thm "pt_perm_compose_aux"}; |
|
69 |
val cp1_aux = @{thm "cp1_aux"}; |
|
70 |
val perm_aux_fold = @{thm "perm_aux_fold"}; |
|
71 |
val supports_fresh_rule = @{thm "supports_fresh"}; |
|
21669 | 72 |
|
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
73 |
(* pulls out dynamically a thm via the proof state *) |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38715
diff
changeset
|
74 |
fun dynamic_thms st name = Global_Theory.get_thms (theory_of_thm st) name; |
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38715
diff
changeset
|
75 |
fun dynamic_thm st name = Global_Theory.get_thm (theory_of_thm st) name; |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
76 |
|
18012 | 77 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
78 |
(* needed in the process of fully simplifying permutations *) |
24519 | 79 |
val strong_congs = [@{thm "if_cong"}] |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
80 |
(* needed to avoid warnings about overwritten congs *) |
24519 | 81 |
val weak_congs = [@{thm "if_weak_cong"}] |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
82 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
83 |
(* debugging *) |
56492 | 84 |
fun DEBUG ctxt (msg,tac) = |
56491 | 85 |
CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]); |
56492 | 86 |
fun NO_DEBUG _ (_,tac) = CHANGED tac; |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
87 |
|
19477 | 88 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
89 |
(* simproc that deals with instances of permutations in front *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
90 |
(* of applications; just adding this rule to the simplifier *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
91 |
(* would loop; it also needs careful tuning with the simproc *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
92 |
(* for functions to avoid further possibilities for looping *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
93 |
fun perm_simproc_app' ctxt redex = |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
94 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
95 |
val thy = Proof_Context.theory_of ctxt; |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
96 |
(* the "application" case is only applicable when the head of f is not a *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
97 |
(* constant or when (f x) is a permuation with two or more arguments *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
98 |
fun applicable_app t = |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
99 |
(case (strip_comb t) of |
56253 | 100 |
(Const (@{const_name Nominal.perm},_),ts) => (length ts) >= 2 |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
101 |
| (Const _,_) => false |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
102 |
| _ => true) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
103 |
in |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
104 |
case redex of |
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
105 |
(* case pi o (f x) == (pi o f) (pi o x) *) |
56253 | 106 |
(Const(@{const_name Nominal.perm}, |
107 |
Type(@{type_name fun}, |
|
108 |
[Type(@{type_name list}, [Type(@{type_name prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
109 |
(if (applicable_app f) then |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
110 |
let |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
111 |
val name = Long_Name.base_name n |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
112 |
val at_inst = Global_Theory.get_thm thy ("at_" ^ name ^ "_inst") |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
113 |
val pt_inst = Global_Theory.get_thm thy ("pt_" ^ name ^ "_inst") |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
114 |
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
115 |
else NONE) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
116 |
| _ => NONE |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
117 |
end |
19139 | 118 |
|
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
37678
diff
changeset
|
119 |
val perm_simproc_app = Simplifier.simproc_global @{theory} "perm_simproc_app" |
25997 | 120 |
["Nominal.perm pi x"] perm_simproc_app'; |
121 |
||
24519 | 122 |
(* a simproc that deals with permutation instances in front of functions *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
123 |
fun perm_simproc_fun' ctxt redex = |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
124 |
let |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
125 |
fun applicable_fun t = |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
126 |
(case (strip_comb t) of |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
127 |
(Abs _ ,[]) => true |
56253 | 128 |
| (Const (@{const_name Nominal.perm},_),_) => false |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
129 |
| (Const _, _) => true |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
130 |
| _ => false) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
131 |
in |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
132 |
case redex of |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
133 |
(* case pi o f == (%x. pi o (f ((rev pi)o x))) *) |
56253 | 134 |
(Const(@{const_name Nominal.perm},_) $ pi $ f) => |
44830 | 135 |
(if applicable_fun f then SOME perm_fun_def else NONE) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
136 |
| _ => NONE |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
137 |
end |
19139 | 138 |
|
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
37678
diff
changeset
|
139 |
val perm_simproc_fun = Simplifier.simproc_global @{theory} "perm_simproc_fun" |
25997 | 140 |
["Nominal.perm pi x"] perm_simproc_fun'; |
141 |
||
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
142 |
(* function for simplyfying permutations *) |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
143 |
(* stac contains the simplifiation tactic that is *) |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
144 |
(* applied (see (no_asm) options below *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
145 |
fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i = |
56230 | 146 |
("general simplification of permutations", fn st => SUBGOAL (fn _ => |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
147 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
148 |
val ctxt' = ctxt |
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset
|
149 |
addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms) |
25997 | 150 |
addsimprocs [perm_simproc_fun, perm_simproc_app] |
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
44830
diff
changeset
|
151 |
|> fold Simplifier.del_cong weak_congs |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
44830
diff
changeset
|
152 |
|> fold Simplifier.add_cong strong_congs |
19477 | 153 |
in |
56230 | 154 |
stac ctxt' i |
155 |
end) i st); |
|
19477 | 156 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
157 |
(* general simplification of permutations and permutation that arose from eqvt-problems *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
158 |
fun perm_simp stac ctxt = |
22610 | 159 |
let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"] |
160 |
in |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
161 |
perm_simp_gen stac simps [] ctxt |
22610 | 162 |
end; |
163 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
164 |
fun eqvt_simp stac ctxt = |
22610 | 165 |
let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"] |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
166 |
val eqvts_thms = NominalThmDecls.get_eqvt_thms ctxt; |
22610 | 167 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
168 |
perm_simp_gen stac simps eqvts_thms ctxt |
22610 | 169 |
end; |
22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
170 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
171 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
172 |
(* main simplification tactics for permutations *) |
56491 | 173 |
fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (perm_simp stac ctxt i)); |
174 |
fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i)); |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
175 |
|
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
176 |
val perm_simp_tac_i = perm_simp_tac_gen_i simp_tac |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
177 |
val perm_asm_simp_tac_i = perm_simp_tac_gen_i asm_simp_tac |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
178 |
val perm_full_simp_tac_i = perm_simp_tac_gen_i full_simp_tac |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
179 |
val perm_asm_lr_simp_tac_i = perm_simp_tac_gen_i asm_lr_simp_tac |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
180 |
val perm_asm_full_simp_tac_i = perm_simp_tac_gen_i asm_full_simp_tac |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
181 |
val eqvt_asm_full_simp_tac_i = eqvt_simp_tac_gen_i asm_full_simp_tac |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
182 |
|
19477 | 183 |
(* applies the perm_compose rule such that *) |
184 |
(* pi o (pi' o lhs) = rhs *) |
|
185 |
(* is transformed to *) |
|
186 |
(* (pi o pi') o (pi' o lhs) = rhs *) |
|
187 |
(* *) |
|
188 |
(* this rule would loop in the simplifier, so some trick is used with *) |
|
189 |
(* generating perm_aux'es for the outermost permutation and then un- *) |
|
190 |
(* folding the definition *) |
|
25997 | 191 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
192 |
fun perm_compose_simproc' ctxt redex = |
25997 | 193 |
(case redex of |
56253 | 194 |
(Const (@{const_name Nominal.perm}, Type (@{type_name fun}, [Type (@{type_name list}, |
195 |
[Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (@{const_name Nominal.perm}, |
|
196 |
Type (@{type_name fun}, [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ |
|
25997 | 197 |
pi2 $ t)) => |
19477 | 198 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
199 |
val thy = Proof_Context.theory_of ctxt |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
200 |
val tname' = Long_Name.base_name tname |
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
201 |
val uname' = Long_Name.base_name uname |
25997 | 202 |
in |
203 |
if pi1 <> pi2 then (* only apply the composition rule in this case *) |
|
204 |
if T = U then |
|
205 |
SOME (Drule.instantiate' |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
206 |
[SOME (ctyp_of thy (fastype_of t))] |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
207 |
[SOME (cterm_of thy pi1), SOME (cterm_of thy pi2), SOME (cterm_of thy t)] |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
208 |
(mk_meta_eq ([Global_Theory.get_thm thy ("pt_"^tname'^"_inst"), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
209 |
Global_Theory.get_thm thy ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux))) |
25997 | 210 |
else |
211 |
SOME (Drule.instantiate' |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
212 |
[SOME (ctyp_of thy (fastype_of t))] |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
213 |
[SOME (cterm_of thy pi1), SOME (cterm_of thy pi2), SOME (cterm_of thy t)] |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
214 |
(mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS |
25997 | 215 |
cp1_aux))) |
216 |
else NONE |
|
217 |
end |
|
218 |
| _ => NONE); |
|
19477 | 219 |
|
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
37678
diff
changeset
|
220 |
val perm_compose_simproc = Simplifier.simproc_global @{theory} "perm_compose" |
25997 | 221 |
["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc'; |
19477 | 222 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
223 |
fun perm_compose_tac ctxt i = |
25997 | 224 |
("analysing permutation compositions on the lhs", |
225 |
fn st => EVERY |
|
226 |
[rtac trans i, |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
227 |
asm_full_simp_tac (empty_simpset ctxt addsimprocs [perm_compose_simproc]) i, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
228 |
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st); |
18012 | 229 |
|
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32149
diff
changeset
|
230 |
fun apply_cong_tac i = ("application of congruence", cong_tac i); |
17870 | 231 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
232 |
|
19477 | 233 |
(* unfolds the definition of permutations *) |
234 |
(* applied to functions such that *) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
235 |
(* pi o f = rhs *) |
19477 | 236 |
(* is transformed to *) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
237 |
(* %x. pi o (f ((rev pi) o x)) = rhs *) |
24519 | 238 |
fun unfold_perm_fun_def_tac i = |
239 |
("unfolding of permutations on functions", |
|
240 |
rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i) |
|
17870 | 241 |
|
19477 | 242 |
(* applies the ext-rule such that *) |
243 |
(* *) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
244 |
(* f = g goes to /\x. f x = g x *) |
55990 | 245 |
fun ext_fun_tac i = ("extensionality expansion of functions", rtac @{thm ext} i); |
17870 | 246 |
|
247 |
||
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
248 |
(* perm_extend_simp_tac_i is perm_simp plus additional tactics *) |
19477 | 249 |
(* to decide equation that come from support problems *) |
250 |
(* since it contains looping rules the "recursion" - depth is set *) |
|
251 |
(* to 10 - this seems to be sufficient in most cases *) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
252 |
fun perm_extend_simp_tac_i tactical ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
253 |
let fun perm_extend_simp_tac_aux tactical ctxt n = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
254 |
if n=0 then K all_tac |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
255 |
else DETERM o |
56491 | 256 |
(FIRST'[fn i => tactical ctxt ("splitting conjunctions on the rhs", rtac conjI i), |
257 |
fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i), |
|
258 |
fn i => tactical ctxt (perm_compose_tac ctxt i), |
|
259 |
fn i => tactical ctxt (apply_cong_tac i), |
|
260 |
fn i => tactical ctxt (unfold_perm_fun_def_tac i), |
|
261 |
fn i => tactical ctxt (ext_fun_tac i)] |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
262 |
THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1)))) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
263 |
in perm_extend_simp_tac_aux tactical ctxt 10 end; |
19151 | 264 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
265 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
266 |
(* tactic that tries to solve "supports"-goals; first it *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
267 |
(* unfolds the support definition and strips off the *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
268 |
(* intros, then applies eqvt_simp_tac *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
269 |
fun supports_tac_i tactical ctxt i = |
18012 | 270 |
let |
36945 | 271 |
val simps = [supports_def, Thm.symmetric fresh_def, fresh_prod] |
17870 | 272 |
in |
56491 | 273 |
EVERY [tactical ctxt ("unfolding of supports ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i), |
274 |
tactical ctxt ("stripping of foralls ", REPEAT_DETERM (rtac allI i)), |
|
275 |
tactical ctxt ("geting rid of the imps ", rtac impI i), |
|
276 |
tactical ctxt ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)), |
|
277 |
tactical ctxt ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )] |
|
17870 | 278 |
end; |
279 |
||
19151 | 280 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
281 |
(* tactic that guesses the finite-support of a goal *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
282 |
(* it first collects all free variables and tries to show *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
283 |
(* that the support of these free variables (op supports) *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
284 |
(* the goal *) |
20854 | 285 |
fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j - i)) vs |
286 |
| collect_vars i (v as Free _) vs = insert (op =) v vs |
|
287 |
| collect_vars i (v as Var _) vs = insert (op =) v vs |
|
19151 | 288 |
| collect_vars i (Const _) vs = vs |
289 |
| collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs |
|
290 |
| collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs); |
|
291 |
||
43278 | 292 |
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
293 |
fun finite_guess_tac_i tactical ctxt i st = |
42364 | 294 |
let val goal = nth (cprems_of st) (i - 1) |
19151 | 295 |
in |
26806 | 296 |
case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of |
56253 | 297 |
_ $ (Const (@{const_name finite}, _) $ (Const (@{const_name Nominal.supp}, T) $ x)) => |
19151 | 298 |
let |
22578 | 299 |
val cert = Thm.cterm_of (Thm.theory_of_thm st); |
19151 | 300 |
val ps = Logic.strip_params (term_of goal); |
301 |
val Ts = rev (map snd ps); |
|
302 |
val vs = collect_vars 0 x []; |
|
33244 | 303 |
val s = fold_rev (fn v => fn s => |
19151 | 304 |
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) |
33244 | 305 |
vs HOLogic.unit; |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset
|
306 |
val s' = fold_rev Term.abs ps |
56253 | 307 |
(Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) --> |
44692
ccfc7c193d2b
modify nominal packages to better respect set/pred distinction
huffman
parents:
43278
diff
changeset
|
308 |
Term.range_type T) $ s); |
19151 | 309 |
val supports_rule' = Thm.lift_rule goal supports_rule; |
310 |
val _ $ (_ $ S $ _) = |
|
311 |
Logic.strip_assums_concl (hd (prems_of supports_rule')); |
|
312 |
val supports_rule'' = Drule.cterm_instantiate |
|
313 |
[(cert (head_of S), cert s')] supports_rule' |
|
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset
|
314 |
val fin_supp = dynamic_thms st ("fin_supp") |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
315 |
val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp |
19151 | 316 |
in |
56491 | 317 |
(tactical ctxt ("guessing of the right supports-set", |
19151 | 318 |
EVERY [compose_tac (false, supports_rule'', 2) i, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
319 |
asm_full_simp_tac ctxt' (i+1), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
320 |
supports_tac_i tactical ctxt i])) st |
19151 | 321 |
end |
322 |
| _ => Seq.empty |
|
323 |
end |
|
43278 | 324 |
handle General.Subscript => Seq.empty |
325 |
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
|
19151 | 326 |
|
22595
293934e41dfd
make fresh_guess fail if it does not solve the subgoal
narboux
parents:
22578
diff
changeset
|
327 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
328 |
(* tactic that guesses whether an atom is fresh for an expression *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
329 |
(* it first collects all free variables and tries to show that the *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
330 |
(* support of these free variables (op supports) the goal *) |
43278 | 331 |
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
332 |
fun fresh_guess_tac_i tactical ctxt i st = |
19857 | 333 |
let |
42364 | 334 |
val goal = nth (cprems_of st) (i - 1) |
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset
|
335 |
val fin_supp = dynamic_thms st ("fin_supp") |
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset
|
336 |
val fresh_atm = dynamic_thms st ("fresh_atm") |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
337 |
val ctxt1 = ctxt addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
338 |
val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp |
19857 | 339 |
in |
340 |
case Logic.strip_assums_concl (term_of goal) of |
|
56253 | 341 |
_ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) => |
19857 | 342 |
let |
22578 | 343 |
val cert = Thm.cterm_of (Thm.theory_of_thm st); |
19857 | 344 |
val ps = Logic.strip_params (term_of goal); |
345 |
val Ts = rev (map snd ps); |
|
346 |
val vs = collect_vars 0 t []; |
|
33244 | 347 |
val s = fold_rev (fn v => fn s => |
19857 | 348 |
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) |
33244 | 349 |
vs HOLogic.unit; |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset
|
350 |
val s' = |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset
|
351 |
fold_rev Term.abs ps |
56253 | 352 |
(Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s); |
19857 | 353 |
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule; |
354 |
val _ $ (_ $ S $ _) = |
|
355 |
Logic.strip_assums_concl (hd (prems_of supports_fresh_rule')); |
|
356 |
val supports_fresh_rule'' = Drule.cterm_instantiate |
|
357 |
[(cert (head_of S), cert s')] supports_fresh_rule' |
|
358 |
in |
|
56491 | 359 |
(tactical ctxt ("guessing of the right set that supports the goal", |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
360 |
(EVERY [compose_tac (false, supports_fresh_rule'', 3) i, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
361 |
asm_full_simp_tac ctxt1 (i+2), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
362 |
asm_full_simp_tac ctxt2 (i+1), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
363 |
supports_tac_i tactical ctxt i]))) st |
19857 | 364 |
end |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
365 |
(* when a term-constructor contains more than one binder, it is useful *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
366 |
(* in nominal_primrecs to try whether the goal can be solved by an hammer *) |
56491 | 367 |
| _ => (tactical ctxt ("if it is not of the form _\<sharp>_, then try the simplifier", |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
368 |
(asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps [fresh_prod]@fresh_atm) i))) st |
19857 | 369 |
end |
43278 | 370 |
handle General.Subscript => Seq.empty; |
371 |
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
372 |
|
56492 | 373 |
val eqvt_simp_tac = eqvt_asm_full_simp_tac_i NO_DEBUG; |
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
374 |
|
56492 | 375 |
val perm_simp_tac = perm_asm_full_simp_tac_i NO_DEBUG; |
376 |
val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG; |
|
377 |
val supports_tac = supports_tac_i NO_DEBUG; |
|
378 |
val finite_guess_tac = finite_guess_tac_i NO_DEBUG; |
|
379 |
val fresh_guess_tac = fresh_guess_tac_i NO_DEBUG; |
|
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
380 |
|
56492 | 381 |
val dperm_simp_tac = perm_asm_full_simp_tac_i DEBUG; |
382 |
val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG; |
|
383 |
val dsupports_tac = supports_tac_i DEBUG; |
|
384 |
val dfinite_guess_tac = finite_guess_tac_i DEBUG; |
|
385 |
val dfresh_guess_tac = fresh_guess_tac_i DEBUG; |
|
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
386 |
|
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
387 |
(* Code opied from the Simplifer for setting up the perm_simp method *) |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
388 |
(* behaves nearly identical to the simp-method, for example can handle *) |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
389 |
(* options like (no_asm) etc. *) |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
390 |
val no_asmN = "no_asm"; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
391 |
val no_asm_useN = "no_asm_use"; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
392 |
val no_asm_simpN = "no_asm_simp"; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
393 |
val asm_lrN = "asm_lr"; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
394 |
|
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
395 |
val perm_simp_options = |
56492 | 396 |
(Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG) || |
397 |
Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG) || |
|
398 |
Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG) || |
|
399 |
Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG) || |
|
400 |
Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG)); |
|
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
401 |
|
30549 | 402 |
val perm_simp_meth = |
33554 | 403 |
Scan.lift perm_simp_options --| Method.sections (Simplifier.simp_modifiers') >> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
404 |
(fn tac => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o tac ctxt)); |
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
405 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
406 |
(* setup so that the simpset is used which is active at the moment when the tactic is called *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
407 |
fun local_simp_meth_setup tac = |
30549 | 408 |
Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
409 |
(K (SIMPLE_METHOD' o tac)); |
17870 | 410 |
|
22595
293934e41dfd
make fresh_guess fail if it does not solve the subgoal
narboux
parents:
22578
diff
changeset
|
411 |
(* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *) |
293934e41dfd
make fresh_guess fail if it does not solve the subgoal
narboux
parents:
22578
diff
changeset
|
412 |
|
22656
13302b2d0948
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
narboux
parents:
22610
diff
changeset
|
413 |
fun basic_simp_meth_setup debug tac = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
414 |
Scan.depend (fn context => Scan.succeed (Simplifier.map_ss (put_simpset HOL_basic_ss) context, ())) -- |
30549 | 415 |
Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
416 |
(K (SIMPLE_METHOD' o (if debug then tac else SOLVED' o tac))); |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
417 |
|
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
418 |
val perm_simp_meth_debug = local_simp_meth_setup dperm_simp_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
419 |
val perm_extend_simp_meth = local_simp_meth_setup perm_extend_simp_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
420 |
val perm_extend_simp_meth_debug = local_simp_meth_setup dperm_extend_simp_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
421 |
val supports_meth = local_simp_meth_setup supports_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
422 |
val supports_meth_debug = local_simp_meth_setup dsupports_tac; |
24571 | 423 |
|
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
424 |
val finite_guess_meth = basic_simp_meth_setup false finite_guess_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
425 |
val finite_guess_meth_debug = basic_simp_meth_setup true dfinite_guess_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
426 |
val fresh_guess_meth = basic_simp_meth_setup false fresh_guess_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
427 |
val fresh_guess_meth_debug = basic_simp_meth_setup true dfresh_guess_tac; |
17870 | 428 |
|
20289 | 429 |
end |