author | haftmann |
Fri, 01 Nov 2013 18:51:14 +0100 | |
changeset 54230 | b1d955791529 |
parent 51717 | 9e7d1c139569 |
child 55990 | 41c6b99c5fb7 |
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 *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
84 |
fun DEBUG_tac (msg,tac) = |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
85 |
CHANGED (EVERY [print_tac ("before "^msg), tac, print_tac ("after "^msg)]); |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
86 |
fun NO_DEBUG_tac (_,tac) = CHANGED tac; |
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 |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
100 |
(Const ("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) *) |
19494 | 106 |
(Const("Nominal.perm", |
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset
|
107 |
Type("fun",[Type("List.list",[Type(@{type_name Product_Type.prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
108 |
(if (applicable_app f) then |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
109 |
let |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
110 |
val name = Long_Name.base_name n |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
111 |
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
|
112 |
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
|
113 |
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
|
114 |
else NONE) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
115 |
| _ => NONE |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
116 |
end |
19139 | 117 |
|
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
|
118 |
val perm_simproc_app = Simplifier.simproc_global @{theory} "perm_simproc_app" |
25997 | 119 |
["Nominal.perm pi x"] perm_simproc_app'; |
120 |
||
24519 | 121 |
(* 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
|
122 |
fun perm_simproc_fun' ctxt redex = |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
123 |
let |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
124 |
fun applicable_fun t = |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
125 |
(case (strip_comb t) of |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
126 |
(Abs _ ,[]) => true |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
127 |
| (Const ("Nominal.perm",_),_) => false |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
128 |
| (Const _, _) => true |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
129 |
| _ => false) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
130 |
in |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
131 |
case redex of |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
132 |
(* case pi o f == (%x. pi o (f ((rev pi)o x))) *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
133 |
(Const("Nominal.perm",_) $ pi $ f) => |
44830 | 134 |
(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
|
135 |
| _ => NONE |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
136 |
end |
19139 | 137 |
|
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
|
138 |
val perm_simproc_fun = Simplifier.simproc_global @{theory} "perm_simproc_fun" |
25997 | 139 |
["Nominal.perm pi x"] perm_simproc_fun'; |
140 |
||
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
141 |
(* function for simplyfying permutations *) |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
142 |
(* 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
|
143 |
(* applied (see (no_asm) options below *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
144 |
fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i = |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
145 |
("general simplification of permutations", fn st => |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
146 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
147 |
val ctxt' = ctxt |
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset
|
148 |
addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms) |
25997 | 149 |
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
|
150 |
|> 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
|
151 |
|> fold Simplifier.add_cong strong_congs |
19477 | 152 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
153 |
stac ctxt' i st |
19987
b97607d4d9a5
- put declarations inside a structure (NominalPermeq)
berghofe
parents:
19858
diff
changeset
|
154 |
end); |
19477 | 155 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
156 |
(* 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
|
157 |
fun perm_simp stac ctxt = |
22610 | 158 |
let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"] |
159 |
in |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
160 |
perm_simp_gen stac simps [] ctxt |
22610 | 161 |
end; |
162 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
163 |
fun eqvt_simp stac ctxt = |
22610 | 164 |
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
|
165 |
val eqvts_thms = NominalThmDecls.get_eqvt_thms ctxt; |
22610 | 166 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
167 |
perm_simp_gen stac simps eqvts_thms ctxt |
22610 | 168 |
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
|
169 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
170 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
171 |
(* main simplification tactics for permutations *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
172 |
fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical (perm_simp stac ctxt i)); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
173 |
fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical (eqvt_simp stac ctxt i)); |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
174 |
|
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
175 |
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
|
176 |
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
|
177 |
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
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
|
19477 | 182 |
(* applies the perm_compose rule such that *) |
183 |
(* pi o (pi' o lhs) = rhs *) |
|
184 |
(* is transformed to *) |
|
185 |
(* (pi o pi') o (pi' o lhs) = rhs *) |
|
186 |
(* *) |
|
187 |
(* this rule would loop in the simplifier, so some trick is used with *) |
|
188 |
(* generating perm_aux'es for the outermost permutation and then un- *) |
|
189 |
(* folding the definition *) |
|
25997 | 190 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
191 |
fun perm_compose_simproc' ctxt redex = |
25997 | 192 |
(case redex of |
193 |
(Const ("Nominal.perm", Type ("fun", [Type ("List.list", |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset
|
194 |
[Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", |
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37391
diff
changeset
|
195 |
Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ |
25997 | 196 |
pi2 $ t)) => |
19477 | 197 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
198 |
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
|
199 |
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
|
200 |
val uname' = Long_Name.base_name uname |
25997 | 201 |
in |
202 |
if pi1 <> pi2 then (* only apply the composition rule in this case *) |
|
203 |
if T = U then |
|
204 |
SOME (Drule.instantiate' |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
205 |
[SOME (ctyp_of thy (fastype_of t))] |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
206 |
[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
|
207 |
(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
|
208 |
Global_Theory.get_thm thy ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux))) |
25997 | 209 |
else |
210 |
SOME (Drule.instantiate' |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
211 |
[SOME (ctyp_of thy (fastype_of t))] |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
212 |
[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
|
213 |
(mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS |
25997 | 214 |
cp1_aux))) |
215 |
else NONE |
|
216 |
end |
|
217 |
| _ => NONE); |
|
19477 | 218 |
|
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
|
219 |
val perm_compose_simproc = Simplifier.simproc_global @{theory} "perm_compose" |
25997 | 220 |
["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc'; |
19477 | 221 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
222 |
fun perm_compose_tac ctxt i = |
25997 | 223 |
("analysing permutation compositions on the lhs", |
224 |
fn st => EVERY |
|
225 |
[rtac trans i, |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
226 |
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
|
227 |
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st); |
18012 | 228 |
|
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
|
229 |
fun apply_cong_tac i = ("application of congruence", cong_tac i); |
17870 | 230 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
231 |
|
19477 | 232 |
(* unfolds the definition of permutations *) |
233 |
(* applied to functions such that *) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
234 |
(* pi o f = rhs *) |
19477 | 235 |
(* is transformed to *) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
236 |
(* %x. pi o (f ((rev pi) o x)) = rhs *) |
24519 | 237 |
fun unfold_perm_fun_def_tac i = |
238 |
("unfolding of permutations on functions", |
|
239 |
rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i) |
|
17870 | 240 |
|
19477 | 241 |
(* applies the ext-rule such that *) |
242 |
(* *) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
243 |
(* f = g goes to /\x. f x = g x *) |
19477 | 244 |
fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i); |
17870 | 245 |
|
246 |
||
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
247 |
(* perm_extend_simp_tac_i is perm_simp plus additional tactics *) |
19477 | 248 |
(* to decide equation that come from support problems *) |
249 |
(* since it contains looping rules the "recursion" - depth is set *) |
|
250 |
(* 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
|
251 |
fun perm_extend_simp_tac_i tactical ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
252 |
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
|
253 |
if n=0 then K all_tac |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
254 |
else DETERM o |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
255 |
(FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i), |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
256 |
fn i => tactical (perm_simp asm_full_simp_tac ctxt i), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
257 |
fn i => tactical (perm_compose_tac ctxt i), |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32733
diff
changeset
|
258 |
fn i => tactical (apply_cong_tac i), |
19477 | 259 |
fn i => tactical (unfold_perm_fun_def_tac i), |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
260 |
fn i => tactical (ext_fun_tac i)] |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
261 |
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
|
262 |
in perm_extend_simp_tac_aux tactical ctxt 10 end; |
19151 | 263 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
264 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
265 |
(* 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
|
266 |
(* 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
|
267 |
(* intros, then applies eqvt_simp_tac *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
268 |
fun supports_tac_i tactical ctxt i = |
18012 | 269 |
let |
36945 | 270 |
val simps = [supports_def, Thm.symmetric fresh_def, fresh_prod] |
17870 | 271 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
272 |
EVERY [tactical ("unfolding of supports ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i), |
19477 | 273 |
tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)), |
274 |
tactical ("geting rid of the imps ", rtac impI i), |
|
275 |
tactical ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)), |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
276 |
tactical ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )] |
17870 | 277 |
end; |
278 |
||
19151 | 279 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
280 |
(* 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
|
281 |
(* 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
|
282 |
(* 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
|
283 |
(* the goal *) |
20854 | 284 |
fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j - i)) vs |
285 |
| collect_vars i (v as Free _) vs = insert (op =) v vs |
|
286 |
| collect_vars i (v as Var _) vs = insert (op =) v vs |
|
19151 | 287 |
| collect_vars i (Const _) vs = vs |
288 |
| collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs |
|
289 |
| collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs); |
|
290 |
||
43278 | 291 |
(* 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
|
292 |
fun finite_guess_tac_i tactical ctxt i st = |
42364 | 293 |
let val goal = nth (cprems_of st) (i - 1) |
19151 | 294 |
in |
26806 | 295 |
case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of |
22274 | 296 |
_ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) => |
19151 | 297 |
let |
22578 | 298 |
val cert = Thm.cterm_of (Thm.theory_of_thm st); |
19151 | 299 |
val ps = Logic.strip_params (term_of goal); |
300 |
val Ts = rev (map snd ps); |
|
301 |
val vs = collect_vars 0 x []; |
|
33244 | 302 |
val s = fold_rev (fn v => fn s => |
19151 | 303 |
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) |
33244 | 304 |
vs HOLogic.unit; |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset
|
305 |
val s' = fold_rev Term.abs ps |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset
|
306 |
(Const ("Nominal.supp", fastype_of1 (Ts, s) --> |
44692
ccfc7c193d2b
modify nominal packages to better respect set/pred distinction
huffman
parents:
43278
diff
changeset
|
307 |
Term.range_type T) $ s); |
19151 | 308 |
val supports_rule' = Thm.lift_rule goal supports_rule; |
309 |
val _ $ (_ $ S $ _) = |
|
310 |
Logic.strip_assums_concl (hd (prems_of supports_rule')); |
|
311 |
val supports_rule'' = Drule.cterm_instantiate |
|
312 |
[(cert (head_of S), cert s')] supports_rule' |
|
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset
|
313 |
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
|
314 |
val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp |
19151 | 315 |
in |
316 |
(tactical ("guessing of the right supports-set", |
|
317 |
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
|
318 |
asm_full_simp_tac ctxt' (i+1), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
319 |
supports_tac_i tactical ctxt i])) st |
19151 | 320 |
end |
321 |
| _ => Seq.empty |
|
322 |
end |
|
43278 | 323 |
handle General.Subscript => Seq.empty |
324 |
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) |
|
19151 | 325 |
|
22595
293934e41dfd
make fresh_guess fail if it does not solve the subgoal
narboux
parents:
22578
diff
changeset
|
326 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
327 |
(* 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
|
328 |
(* 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
|
329 |
(* support of these free variables (op supports) the goal *) |
43278 | 330 |
(* 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
|
331 |
fun fresh_guess_tac_i tactical ctxt i st = |
19857 | 332 |
let |
42364 | 333 |
val goal = nth (cprems_of st) (i - 1) |
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset
|
334 |
val fin_supp = dynamic_thms st ("fin_supp") |
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26338
diff
changeset
|
335 |
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
|
336 |
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
|
337 |
val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp |
19857 | 338 |
in |
339 |
case Logic.strip_assums_concl (term_of goal) of |
|
340 |
_ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => |
|
341 |
let |
|
22578 | 342 |
val cert = Thm.cterm_of (Thm.theory_of_thm st); |
19857 | 343 |
val ps = Logic.strip_params (term_of goal); |
344 |
val Ts = rev (map snd ps); |
|
345 |
val vs = collect_vars 0 t []; |
|
33244 | 346 |
val s = fold_rev (fn v => fn s => |
19857 | 347 |
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) |
33244 | 348 |
vs HOLogic.unit; |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset
|
349 |
val s' = |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset
|
350 |
fold_rev Term.abs ps |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45620
diff
changeset
|
351 |
(Const ("Nominal.supp", fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s); |
19857 | 352 |
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule; |
353 |
val _ $ (_ $ S $ _) = |
|
354 |
Logic.strip_assums_concl (hd (prems_of supports_fresh_rule')); |
|
355 |
val supports_fresh_rule'' = Drule.cterm_instantiate |
|
356 |
[(cert (head_of S), cert s')] supports_fresh_rule' |
|
357 |
in |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
358 |
(tactical ("guessing of the right set that supports the goal", |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
359 |
(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
|
360 |
asm_full_simp_tac ctxt1 (i+2), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
361 |
asm_full_simp_tac ctxt2 (i+1), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
362 |
supports_tac_i tactical ctxt i]))) st |
19857 | 363 |
end |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
364 |
(* 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
|
365 |
(* in nominal_primrecs to try whether the goal can be solved by an hammer *) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
366 |
| _ => (tactical ("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
|
367 |
(asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps [fresh_prod]@fresh_atm) i))) st |
19857 | 368 |
end |
43278 | 369 |
handle General.Subscript => Seq.empty; |
370 |
(* 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
|
371 |
|
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
372 |
val eqvt_simp_tac = eqvt_asm_full_simp_tac_i NO_DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
373 |
|
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
374 |
val perm_simp_tac = perm_asm_full_simp_tac_i NO_DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
375 |
val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
376 |
val supports_tac = supports_tac_i NO_DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
377 |
val finite_guess_tac = finite_guess_tac_i NO_DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
378 |
val fresh_guess_tac = fresh_guess_tac_i NO_DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
379 |
|
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
380 |
val dperm_simp_tac = perm_asm_full_simp_tac_i DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
381 |
val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
382 |
val dsupports_tac = supports_tac_i DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
383 |
val dfinite_guess_tac = finite_guess_tac_i DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
384 |
val dfresh_guess_tac = fresh_guess_tac_i DEBUG_tac; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
385 |
|
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
386 |
(* 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
|
387 |
(* 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
|
388 |
(* options like (no_asm) etc. *) |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
389 |
val no_asmN = "no_asm"; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
390 |
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
|
391 |
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
|
392 |
val asm_lrN = "asm_lr"; |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
393 |
|
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
394 |
val perm_simp_options = |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
395 |
(Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG_tac) || |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
396 |
Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG_tac) || |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
397 |
Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG_tac) || |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
398 |
Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) || |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
399 |
Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac)); |
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
400 |
|
30549 | 401 |
val perm_simp_meth = |
33554 | 402 |
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
|
403 |
(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
|
404 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22274
diff
changeset
|
405 |
(* 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
|
406 |
fun local_simp_meth_setup tac = |
30549 | 407 |
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
|
408 |
(K (SIMPLE_METHOD' o tac)); |
17870 | 409 |
|
22595
293934e41dfd
make fresh_guess fail if it does not solve the subgoal
narboux
parents:
22578
diff
changeset
|
410 |
(* 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
|
411 |
|
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
|
412 |
fun basic_simp_meth_setup debug tac = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46219
diff
changeset
|
413 |
Scan.depend (fn context => Scan.succeed (Simplifier.map_ss (put_simpset HOL_basic_ss) context, ())) -- |
30549 | 414 |
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
|
415 |
(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
|
416 |
|
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
417 |
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
|
418 |
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
|
419 |
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
|
420 |
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
|
421 |
val supports_meth_debug = local_simp_meth_setup dsupports_tac; |
24571 | 422 |
|
28322
6f4cf302c798
made the perm_simp tactic to understand options such as (no_asm)
urbanc
parents:
28262
diff
changeset
|
423 |
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
|
424 |
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
|
425 |
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
|
426 |
val fresh_guess_meth_debug = basic_simp_meth_setup true dfresh_guess_tac; |
17870 | 427 |
|
20289 | 428 |
end |