author | urbanc |
Thu, 06 Apr 2006 17:29:40 +0200 | |
changeset 19350 | 2e1c7ca05ee0 |
parent 19169 | 20a73345dd6e |
child 19477 | a95176d0f0dd |
permissions | -rw-r--r-- |
17870 | 1 |
(* $Id$ *) |
2 |
||
3 |
(* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *) |
|
4 |
||
5 |
local |
|
6 |
||
18012 | 7 |
(* pulls out dynamically a thm via the simpset *) |
18434
a31e52a3e6ef
fixed a bug that occured when more than one atom-type
urbanc
parents:
18279
diff
changeset
|
8 |
fun dynamic_thms ss name = |
a31e52a3e6ef
fixed a bug that occured when more than one atom-type
urbanc
parents:
18279
diff
changeset
|
9 |
ProofContext.get_thms (Simplifier.the_context ss) (Name name); |
19139 | 10 |
fun dynamic_thm ss name = |
11 |
ProofContext.get_thm (Simplifier.the_context ss) (Name name); |
|
18012 | 12 |
|
13 |
(* initial simplification step in the tactic *) |
|
19139 | 14 |
fun perm_eval_tac ss i = |
18012 | 15 |
let |
19139 | 16 |
fun perm_eval_simproc sg ss redex = |
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
17 |
let |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
18 |
|
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
19 |
(* the "application" case below is only applicable when the head *) |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
20 |
(* of f is not a constant or when it is a permuattion with two or *) |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
21 |
(* more arguments *) |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
22 |
fun applicable t = |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
23 |
(case (strip_comb t) of |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
24 |
(Const ("nominal.perm",_),ts) => (length ts) >= 2 |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
25 |
| (Const _,_) => false |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
26 |
| _ => true) |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
27 |
|
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
28 |
in |
19139 | 29 |
(case redex of |
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
30 |
(* case pi o (f x) == (pi o f) (pi o x) *) |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
31 |
(* special treatment according to the head of f *) |
19144 | 32 |
(Const("nominal.perm", |
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
33 |
Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
34 |
(case (applicable f) of |
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
35 |
false => NONE |
19163 | 36 |
| _ => |
37 |
let |
|
38 |
val name = Sign.base_name n |
|
39 |
val at_inst = dynamic_thm ss ("at_"^name^"_inst") |
|
40 |
val pt_inst = dynamic_thm ss ("pt_"^name^"_inst") |
|
41 |
val perm_eq_app = thm "nominal.pt_fun_app_eq" |
|
42 |
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end) |
|
19139 | 43 |
|
44 |
(* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *) |
|
19144 | 45 |
| (Const("nominal.perm",_) $ pi $ (Abs _)) => |
46 |
let |
|
19163 | 47 |
val perm_fun_def = thm "nominal.perm_fun_def" |
19139 | 48 |
in SOME (perm_fun_def) end |
49 |
||
50 |
(* no redex otherwise *) |
|
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
51 |
| _ => NONE) end |
19139 | 52 |
|
53 |
val perm_eval = |
|
54 |
Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" |
|
55 |
["nominal.perm pi x"] perm_eval_simproc; |
|
56 |
||
19350 | 57 |
(* applies the pt_perm_compose lemma *) |
58 |
(* *) |
|
59 |
(* pi1 o (pi2 o x) = (pi1 o pi2) o (pi1 o x) *) |
|
60 |
(* *) |
|
61 |
(* in the restricted case where pi1 is a swapping *) |
|
62 |
(* (a b) coming from a "supports problem"; in *) |
|
63 |
(* this rule would cause loops in the simplifier *) |
|
64 |
val pt_perm_compose = thm "pt_perm_compose"; |
|
65 |
||
66 |
fun perm_compose_simproc i sg ss redex = |
|
67 |
(case redex of |
|
68 |
(Const ("nominal.perm", _) $ (pi1 as Const ("List.list.Cons", _) $ |
|
69 |
(Const ("Pair", _) $ Free (a as (_, T as Type (tname, _))) $ Free b) $ |
|
70 |
Const ("List.list.Nil", _)) $ (Const ("nominal.perm", |
|
71 |
Type ("fun", [Type ("List.list", [Type ("*", [U, _])]), _])) $ pi2 $ t)) => |
|
72 |
let |
|
73 |
val ({bounds = (_, xs), ...}, _) = rep_ss ss |
|
74 |
val ai = find_index (fn (x, _) => x = a) xs |
|
75 |
val bi = find_index (fn (x, _) => x = b) xs |
|
76 |
val tname' = Sign.base_name tname |
|
77 |
in |
|
78 |
if ai = length xs - i - 1 andalso |
|
79 |
bi = length xs - i - 2 andalso |
|
80 |
T = U andalso pi1 <> pi2 then |
|
81 |
SOME (Drule.instantiate' |
|
82 |
[SOME (ctyp_of sg (fastype_of t))] |
|
83 |
[SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)] |
|
84 |
(mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")), |
|
85 |
PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose))) |
|
86 |
else NONE |
|
87 |
end |
|
88 |
| _ => NONE); |
|
89 |
||
90 |
fun perm_compose i = |
|
91 |
Simplifier.simproc (the_context()) "perm_compose" |
|
92 |
["nominal.perm [(a, b)] (nominal.perm pi t)"] (perm_compose_simproc i); |
|
93 |
||
94 |
(* these lemmas are created dynamically according to the atom types *) |
|
95 |
val perm_swap = dynamic_thms ss "perm_swap" |
|
96 |
val perm_fresh = dynamic_thms ss "perm_fresh_fresh" |
|
97 |
val perm_bij = dynamic_thms ss "perm_bij" |
|
98 |
val perm_pi_simp = dynamic_thms ss "perm_pi_simp" |
|
99 |
val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp) |
|
18012 | 100 |
in |
19163 | 101 |
("general simplification step", |
19350 | 102 |
FIRST [rtac conjI i, |
103 |
SUBGOAL (fn (g, i) => asm_full_simp_tac |
|
104 |
(ss' addsimprocs [perm_eval,perm_compose (length (Logic.strip_params g)-2)]) i) i]) |
|
18012 | 105 |
end; |
17870 | 106 |
|
18434
a31e52a3e6ef
fixed a bug that occured when more than one atom-type
urbanc
parents:
18279
diff
changeset
|
107 |
(* applies the perm_compose rule - this rule would loop in the simplifier *) |
a31e52a3e6ef
fixed a bug that occured when more than one atom-type
urbanc
parents:
18279
diff
changeset
|
108 |
(* in case there are more atom-types we have to check every possible instance *) |
19139 | 109 |
(* of perm_compose *) |
18012 | 110 |
fun apply_perm_compose_tac ss i = |
111 |
let |
|
18434
a31e52a3e6ef
fixed a bug that occured when more than one atom-type
urbanc
parents:
18279
diff
changeset
|
112 |
val perm_compose = dynamic_thms ss "perm_compose"; |
a31e52a3e6ef
fixed a bug that occured when more than one atom-type
urbanc
parents:
18279
diff
changeset
|
113 |
val tacs = map (fn thm => (rtac (thm RS trans) i)) perm_compose |
18012 | 114 |
in |
18434
a31e52a3e6ef
fixed a bug that occured when more than one atom-type
urbanc
parents:
18279
diff
changeset
|
115 |
("analysing permutation compositions on the lhs",FIRST (tacs)) |
18012 | 116 |
end |
117 |
||
118 |
(* applying Stefan's smart congruence tac *) |
|
119 |
fun apply_cong_tac i = |
|
120 |
("application of congruence", |
|
121 |
(fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st)); |
|
17870 | 122 |
|
123 |
(* unfolds the definition of permutations applied to functions *) |
|
18012 | 124 |
fun unfold_perm_fun_def_tac i = |
125 |
let |
|
126 |
val perm_fun_def = thm "nominal.perm_fun_def" |
|
127 |
in |
|
128 |
("unfolding of permutations on functions", |
|
129 |
simp_tac (HOL_basic_ss addsimps [perm_fun_def]) i) |
|
17870 | 130 |
end |
131 |
||
18012 | 132 |
(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *) |
133 |
fun expand_fun_eq_tac i = |
|
134 |
("extensionality expansion of functions", |
|
135 |
EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) i, REPEAT_DETERM (rtac allI i)]); |
|
17870 | 136 |
|
137 |
(* debugging *) |
|
138 |
fun DEBUG_tac (msg,tac) = |
|
19169
20a73345dd6e
fixed a problem where a permutation is not analysed
urbanc
parents:
19163
diff
changeset
|
139 |
CHANGED (EVERY [tac, print_tac ("after "^msg)]); |
17870 | 140 |
fun NO_DEBUG_tac (_,tac) = CHANGED tac; |
141 |
||
142 |
(* Main Tactic *) |
|
18012 | 143 |
|
144 |
fun perm_simp_tac tactical ss i = |
|
19139 | 145 |
DETERM (tactical (perm_eval_tac ss i)); |
146 |
||
19151 | 147 |
|
148 |
(* perm_simp_tac plus additional tactics to decide *) |
|
149 |
(* support problems *) |
|
19163 | 150 |
(* the "recursion"-depth is set to 10 - this seems sufficient *) |
19151 | 151 |
fun perm_supports_tac tactical ss n = |
152 |
if n=0 then K all_tac |
|
153 |
else DETERM o |
|
154 |
(FIRST'[fn i => tactical (perm_eval_tac ss i), |
|
19350 | 155 |
(*fn i => tactical (apply_perm_compose_tac ss i),*) |
19163 | 156 |
fn i => tactical (apply_cong_tac i), |
157 |
fn i => tactical (unfold_perm_fun_def_tac i), |
|
158 |
fn i => tactical (expand_fun_eq_tac i)] |
|
19151 | 159 |
THEN_ALL_NEW (TRY o (perm_supports_tac tactical ss (n-1)))); |
17870 | 160 |
|
19139 | 161 |
(* tactic that first unfolds the support definition *) |
162 |
(* and strips off the intros, then applies perm_supports_tac *) |
|
18012 | 163 |
fun supports_tac tactical ss i = |
164 |
let |
|
165 |
val supports_def = thm "nominal.op supports_def"; |
|
166 |
val fresh_def = thm "nominal.fresh_def"; |
|
167 |
val fresh_prod = thm "nominal.fresh_prod"; |
|
168 |
val simps = [supports_def,symmetric fresh_def,fresh_prod] |
|
17870 | 169 |
in |
19151 | 170 |
EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i), |
171 |
tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)), |
|
172 |
tactical ("geting rid of the imps", rtac impI i), |
|
173 |
tactical ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)), |
|
174 |
tactical ("applying perm_simp ", perm_supports_tac tactical ss 10 i)] |
|
17870 | 175 |
end; |
176 |
||
19151 | 177 |
|
178 |
(* tactic that guesses the finite-support of a goal *) |
|
179 |
||
180 |
fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs |
|
181 |
| collect_vars i (v as Free _) vs = v ins vs |
|
182 |
| collect_vars i (v as Var _) vs = v ins vs |
|
183 |
| collect_vars i (Const _) vs = vs |
|
184 |
| collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs |
|
185 |
| collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs); |
|
186 |
||
187 |
val supports_rule = thm "supports_finite"; |
|
188 |
||
189 |
fun finite_guess_tac tactical ss i st = |
|
190 |
let val goal = List.nth(cprems_of st, i-1) |
|
191 |
in |
|
192 |
case Logic.strip_assums_concl (term_of goal) of |
|
193 |
_ $ (Const ("op :", _) $ (Const ("nominal.supp", T) $ x) $ |
|
194 |
Const ("Finite_Set.Finites", _)) => |
|
195 |
let |
|
196 |
val cert = Thm.cterm_of (sign_of_thm st); |
|
197 |
val ps = Logic.strip_params (term_of goal); |
|
198 |
val Ts = rev (map snd ps); |
|
199 |
val vs = collect_vars 0 x []; |
|
200 |
val s = foldr (fn (v, s) => |
|
201 |
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) |
|
202 |
HOLogic.unit vs; |
|
203 |
val s' = list_abs (ps, |
|
204 |
Const ("nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s); |
|
205 |
val supports_rule' = Thm.lift_rule goal supports_rule; |
|
206 |
val _ $ (_ $ S $ _) = |
|
207 |
Logic.strip_assums_concl (hd (prems_of supports_rule')); |
|
208 |
val supports_rule'' = Drule.cterm_instantiate |
|
209 |
[(cert (head_of S), cert s')] supports_rule' |
|
210 |
in |
|
211 |
(tactical ("guessing of the right supports-set", |
|
212 |
EVERY [compose_tac (false, supports_rule'', 2) i, |
|
213 |
asm_full_simp_tac ss (i+1), |
|
214 |
supports_tac tactical ss i])) st |
|
215 |
end |
|
216 |
| _ => Seq.empty |
|
217 |
end |
|
218 |
handle Subscript => Seq.empty |
|
219 |
||
17870 | 220 |
in |
221 |
||
222 |
||
18012 | 223 |
fun simp_meth_setup tac = |
18046
b7389981170b
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
urbanc
parents:
18012
diff
changeset
|
224 |
Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers) |
18012 | 225 |
(Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of); |
17870 | 226 |
|
19151 | 227 |
val perm_eq_meth = simp_meth_setup (perm_simp_tac NO_DEBUG_tac); |
228 |
val perm_eq_meth_debug = simp_meth_setup (perm_simp_tac DEBUG_tac); |
|
229 |
val supports_meth = simp_meth_setup (supports_tac NO_DEBUG_tac); |
|
230 |
val supports_meth_debug = simp_meth_setup (supports_tac DEBUG_tac); |
|
231 |
val finite_gs_meth = simp_meth_setup (finite_guess_tac NO_DEBUG_tac); |
|
232 |
val finite_gs_meth_debug = simp_meth_setup (finite_guess_tac DEBUG_tac); |
|
17870 | 233 |
|
234 |
end |
|
235 |
||
236 |
||
237 |