2297
|
1 |
(* Title: nominal_dt_alpha.ML
|
|
2 |
Author: Cezary Kaliszyk
|
|
3 |
Author: Christian Urban
|
|
4 |
|
2313
|
5 |
Definitions and proofs for the alpha-relations.
|
2297
|
6 |
*)
|
|
7 |
|
|
8 |
signature NOMINAL_DT_ALPHA =
|
|
9 |
sig
|
|
10 |
val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
|
|
11 |
bclause list list list -> term list -> Proof.context ->
|
2298
|
12 |
term list * term list * thm list * thm list * thm * local_theory
|
2300
|
13 |
|
|
14 |
val mk_alpha_distincts: Proof.context -> thm list -> thm list list ->
|
|
15 |
term list -> term list -> bn_info -> thm list * thm list
|
|
16 |
|
|
17 |
val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list
|
2311
|
18 |
|
|
19 |
val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list
|
|
20 |
val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
|
2297
|
21 |
end
|
|
22 |
|
|
23 |
structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
|
|
24 |
struct
|
|
25 |
|
2300
|
26 |
(** definition of the inductive rules for alpha and alpha_bn **)
|
|
27 |
|
2297
|
28 |
(* construct the compound terms for prod_fv and prod_alpha *)
|
|
29 |
fun mk_prod_fv (t1, t2) =
|
|
30 |
let
|
|
31 |
val ty1 = fastype_of t1
|
|
32 |
val ty2 = fastype_of t2
|
|
33 |
val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}
|
|
34 |
in
|
|
35 |
Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2
|
|
36 |
end
|
|
37 |
|
|
38 |
fun mk_prod_alpha (t1, t2) =
|
|
39 |
let
|
|
40 |
val ty1 = fastype_of t1
|
|
41 |
val ty2 = fastype_of t2
|
|
42 |
val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)
|
|
43 |
val resT = [prodT, prodT] ---> @{typ "bool"}
|
|
44 |
in
|
|
45 |
Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2
|
|
46 |
end
|
|
47 |
|
|
48 |
(* generates the compound binder terms *)
|
|
49 |
fun mk_binders lthy bmode args bodies =
|
|
50 |
let
|
|
51 |
fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
|
|
52 |
| bind_set _ args (SOME bn, i) = bn $ (nth args i)
|
|
53 |
fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)
|
|
54 |
| bind_lst _ args (SOME bn, i) = bn $ (nth args i)
|
|
55 |
|
|
56 |
val (combine_fn, bind_fn) =
|
|
57 |
case bmode of
|
|
58 |
Lst => (mk_append, bind_lst)
|
|
59 |
| Set => (mk_union, bind_set)
|
|
60 |
| Res => (mk_union, bind_set)
|
|
61 |
in
|
|
62 |
foldl1 combine_fn (map (bind_fn lthy args) bodies)
|
|
63 |
end
|
|
64 |
|
|
65 |
(* produces the term for an alpha with abstraction *)
|
|
66 |
fun mk_alpha_term bmode fv alpha args args' binders binders' =
|
|
67 |
let
|
|
68 |
val (alpha_name, binder_ty) =
|
|
69 |
case bmode of
|
|
70 |
Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
|
|
71 |
| Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
|
|
72 |
| Res => (@{const_name "alpha_res"}, @{typ "atom set"})
|
|
73 |
val ty = fastype_of args
|
|
74 |
val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
|
|
75 |
val alpha_ty = [ty, ty] ---> @{typ "bool"}
|
|
76 |
val fv_ty = ty --> @{typ "atom set"}
|
|
77 |
val pair_lhs = HOLogic.mk_prod (binders, args)
|
|
78 |
val pair_rhs = HOLogic.mk_prod (binders', args')
|
|
79 |
in
|
|
80 |
HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},
|
|
81 |
Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool})
|
|
82 |
$ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs)
|
|
83 |
end
|
|
84 |
|
|
85 |
(* for non-recursive binders we have to produce alpha_bn premises *)
|
|
86 |
fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder =
|
|
87 |
case binder of
|
|
88 |
(NONE, _) => []
|
|
89 |
| (SOME bn, i) =>
|
|
90 |
if member (op=) bodies i then []
|
|
91 |
else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)]
|
|
92 |
|
|
93 |
(* generat the premises for an alpha rule; mk_frees is used
|
|
94 |
if no binders are present *)
|
|
95 |
fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
|
|
96 |
let
|
|
97 |
fun mk_frees i =
|
|
98 |
let
|
|
99 |
val arg = nth args i
|
|
100 |
val arg' = nth args' i
|
|
101 |
val ty = fastype_of arg
|
|
102 |
in
|
|
103 |
if nth is_rec i
|
|
104 |
then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg'
|
|
105 |
else HOLogic.mk_eq (arg, arg')
|
|
106 |
end
|
|
107 |
|
|
108 |
fun mk_alpha_fv i =
|
|
109 |
let
|
|
110 |
val ty = fastype_of (nth args i)
|
|
111 |
in
|
|
112 |
case AList.lookup (op=) alpha_map ty of
|
|
113 |
NONE => (HOLogic.eq_const ty, supp_const ty)
|
|
114 |
| SOME (alpha, fv) => (alpha, fv)
|
|
115 |
end
|
|
116 |
in
|
|
117 |
case bclause of
|
|
118 |
BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies
|
|
119 |
| BC (bmode, binders, bodies) =>
|
|
120 |
let
|
|
121 |
val (alphas, fvs) = split_list (map mk_alpha_fv bodies)
|
|
122 |
val comp_fv = foldl1 mk_prod_fv fvs
|
|
123 |
val comp_alpha = foldl1 mk_prod_alpha alphas
|
|
124 |
val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
|
|
125 |
val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
|
|
126 |
val comp_binders = mk_binders lthy bmode args binders
|
|
127 |
val comp_binders' = mk_binders lthy bmode args' binders
|
|
128 |
val alpha_prem =
|
|
129 |
mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
|
|
130 |
val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)
|
|
131 |
in
|
|
132 |
map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)
|
|
133 |
end
|
|
134 |
end
|
|
135 |
|
|
136 |
(* produces the introduction rule for an alpha rule *)
|
|
137 |
fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses =
|
|
138 |
let
|
|
139 |
val arg_names = Datatype_Prop.make_tnames arg_tys
|
|
140 |
val arg_names' = Name.variant_list arg_names arg_names
|
|
141 |
val args = map Free (arg_names ~~ arg_tys)
|
|
142 |
val args' = map Free (arg_names' ~~ arg_tys)
|
|
143 |
val alpha = fst (the (AList.lookup (op=) alpha_map ty))
|
|
144 |
val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
|
|
145 |
val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses
|
|
146 |
in
|
|
147 |
Library.foldr Logic.mk_implies (flat prems, concl)
|
|
148 |
end
|
|
149 |
|
|
150 |
(* produces the premise of an alpha-bn rule; we only need to
|
|
151 |
treat the case special where the binding clause is empty;
|
|
152 |
|
|
153 |
- if the body is not included in the bn_info, then we either
|
|
154 |
produce an equation or an alpha-premise
|
|
155 |
|
|
156 |
- if the body is included in the bn_info, then we create
|
|
157 |
either a recursive call to alpha-bn, or no premise *)
|
|
158 |
fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =
|
|
159 |
let
|
|
160 |
fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i =
|
|
161 |
let
|
|
162 |
val arg = nth args i
|
|
163 |
val arg' = nth args' i
|
|
164 |
val ty = fastype_of arg
|
|
165 |
in
|
|
166 |
case AList.lookup (op=) bn_args i of
|
|
167 |
NONE => (case (AList.lookup (op=) alpha_map ty) of
|
|
168 |
NONE => [HOLogic.mk_eq (arg, arg')]
|
|
169 |
| SOME (alpha, _) => [alpha $ arg $ arg'])
|
|
170 |
| SOME (NONE) => []
|
|
171 |
| SOME (SOME bn) => [the (AList.lookup (op=) alpha_bn_map bn) $ arg $ arg']
|
|
172 |
end
|
|
173 |
in
|
|
174 |
case bclause of
|
|
175 |
BC (_, [], bodies) =>
|
|
176 |
map HOLogic.mk_Trueprop
|
|
177 |
(flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies))
|
|
178 |
| _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
|
|
179 |
end
|
|
180 |
|
|
181 |
fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
|
|
182 |
let
|
|
183 |
val arg_names = Datatype_Prop.make_tnames arg_tys
|
|
184 |
val arg_names' = Name.variant_list arg_names arg_names
|
|
185 |
val args = map Free (arg_names ~~ arg_tys)
|
|
186 |
val args' = map Free (arg_names' ~~ arg_tys)
|
|
187 |
val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm)
|
|
188 |
val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
|
|
189 |
val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses
|
|
190 |
in
|
|
191 |
Library.foldr Logic.mk_implies (flat prems, concl)
|
|
192 |
end
|
|
193 |
|
|
194 |
fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) =
|
|
195 |
let
|
|
196 |
val nth_constrs_info = nth constrs_info bn_n
|
|
197 |
val nth_bclausess = nth bclausesss bn_n
|
|
198 |
in
|
|
199 |
map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
|
|
200 |
end
|
|
201 |
|
|
202 |
fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy =
|
|
203 |
let
|
|
204 |
val alpha_names = prefix_dt_names descr sorts "alpha_"
|
|
205 |
val alpha_arg_tys = all_dtyps descr sorts
|
|
206 |
val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys
|
|
207 |
val alpha_frees = map Free (alpha_names ~~ alpha_tys)
|
|
208 |
val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs)
|
|
209 |
|
|
210 |
val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
|
|
211 |
val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
|
|
212 |
val alpha_bn_names = map (prefix "alpha_") bn_names
|
|
213 |
val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
|
|
214 |
val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys
|
|
215 |
val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
|
|
216 |
val alpha_bn_map = bns ~~ alpha_bn_frees
|
|
217 |
|
|
218 |
val constrs_info = all_dtyp_constrs_types descr sorts
|
|
219 |
|
|
220 |
val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss
|
|
221 |
val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info
|
|
222 |
|
2299
|
223 |
val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
|
|
224 |
(alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
|
2297
|
225 |
val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
|
|
226 |
|
|
227 |
val (alphas, lthy') = Inductive.add_inductive_i
|
|
228 |
{quiet_mode = true, verbose = false, alt_name = Binding.empty,
|
2300
|
229 |
coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
|
2297
|
230 |
all_alpha_names [] all_alpha_intros [] lthy
|
|
231 |
|
2298
|
232 |
val all_alpha_trms_loc = #preds alphas;
|
2297
|
233 |
val alpha_induct_loc = #raw_induct alphas;
|
|
234 |
val alpha_intros_loc = #intrs alphas;
|
|
235 |
val alpha_cases_loc = #elims alphas;
|
|
236 |
val phi = ProofContext.export_morphism lthy' lthy;
|
|
237 |
|
2298
|
238 |
val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc;
|
2297
|
239 |
val alpha_induct = Morphism.thm phi alpha_induct_loc;
|
|
240 |
val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
|
|
241 |
val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
|
2298
|
242 |
|
|
243 |
val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms
|
2297
|
244 |
in
|
2298
|
245 |
(alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
|
2297
|
246 |
end
|
|
247 |
|
2300
|
248 |
|
|
249 |
(** produces the distinctness theorems **)
|
|
250 |
|
|
251 |
(* transforms the distinctness theorems of the constructors
|
|
252 |
to "not-alphas" of the constructors *)
|
|
253 |
fun mk_alpha_distinct_goal alpha neq =
|
|
254 |
let
|
|
255 |
val (lhs, rhs) =
|
|
256 |
neq
|
|
257 |
|> HOLogic.dest_Trueprop
|
|
258 |
|> HOLogic.dest_not
|
|
259 |
|> HOLogic.dest_eq
|
|
260 |
in
|
|
261 |
alpha $ lhs $ rhs
|
|
262 |
|> HOLogic.mk_not
|
|
263 |
|> HOLogic.mk_Trueprop
|
|
264 |
end
|
|
265 |
|
|
266 |
fun distinct_tac cases distinct_thms =
|
|
267 |
rtac notI THEN' eresolve_tac cases
|
|
268 |
THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
|
|
269 |
|
|
270 |
fun mk_alpha_distinct ctxt cases_thms (distinct_thm, alpha) =
|
|
271 |
let
|
|
272 |
val ((_, thms), ctxt') = Variable.import false distinct_thm ctxt
|
|
273 |
val goals = map (mk_alpha_distinct_goal alpha o prop_of) thms
|
|
274 |
val nrels = map (fn t => Goal.prove ctxt' [] [] t (K (distinct_tac cases_thms distinct_thm 1))) goals
|
|
275 |
in
|
|
276 |
Variable.export ctxt' ctxt nrels
|
|
277 |
end
|
|
278 |
|
|
279 |
fun mk_alpha_distincts ctxt alpha_cases constrs_distinct_thms alpha_trms alpha_bn_trms bn_infos =
|
|
280 |
let
|
|
281 |
val alpha_distincts =
|
|
282 |
map (mk_alpha_distinct ctxt alpha_cases) (constrs_distinct_thms ~~ alpha_trms)
|
|
283 |
val distinc_thms = map
|
|
284 |
val alpha_bn_distincts_aux = map (fn (_, i, _) => nth constrs_distinct_thms i) bn_infos
|
|
285 |
val alpha_bn_distincts =
|
|
286 |
map (mk_alpha_distinct ctxt alpha_cases) (alpha_bn_distincts_aux ~~ alpha_bn_trms)
|
|
287 |
in
|
|
288 |
(flat alpha_distincts, flat alpha_bn_distincts)
|
|
289 |
end
|
|
290 |
|
|
291 |
|
|
292 |
(** produces the alpha_eq_iff simplification rules **)
|
|
293 |
|
2311
|
294 |
|
2300
|
295 |
(* in case a theorem is of the form (C.. = C..), it will be
|
|
296 |
rewritten to ((C.. = C..) = True) *)
|
|
297 |
fun mk_simp_rule thm =
|
|
298 |
case (prop_of thm) of
|
|
299 |
@{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm]
|
|
300 |
| _ => thm
|
|
301 |
|
|
302 |
fun alpha_eq_iff_tac dist_inj intros elims =
|
|
303 |
SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE'
|
|
304 |
(rtac @{thm iffI} THEN'
|
|
305 |
RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj),
|
|
306 |
asm_full_simp_tac (HOL_ss addsimps intros)])
|
|
307 |
|
|
308 |
fun mk_alpha_eq_iff_goal thm =
|
|
309 |
let
|
|
310 |
val prop = prop_of thm;
|
|
311 |
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
|
|
312 |
val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
|
|
313 |
fun list_conj l = foldr1 HOLogic.mk_conj l;
|
|
314 |
in
|
|
315 |
if hyps = [] then HOLogic.mk_Trueprop concl
|
|
316 |
else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
|
|
317 |
end;
|
|
318 |
|
|
319 |
fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims =
|
|
320 |
let
|
|
321 |
val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
|
|
322 |
val goals = map mk_alpha_eq_iff_goal thms_imp;
|
|
323 |
val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1;
|
|
324 |
val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
|
|
325 |
in
|
|
326 |
Variable.export ctxt' ctxt thms
|
|
327 |
|> map mk_simp_rule
|
|
328 |
end
|
|
329 |
|
2311
|
330 |
|
|
331 |
|
|
332 |
(** symmetry proof for the alphas **)
|
|
333 |
|
|
334 |
val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p"
|
|
335 |
by (erule exE, rule_tac x="-p" in exI, auto)}
|
|
336 |
|
|
337 |
(* for premises that contain binders *)
|
|
338 |
fun prem_bound_tac pred_names ctxt =
|
|
339 |
let
|
|
340 |
fun trans_prem_tac pred_names ctxt =
|
|
341 |
SUBPROOF (fn {prems, context, ...} =>
|
|
342 |
let
|
|
343 |
val prems' = map (transform_prem1 context pred_names) prems
|
|
344 |
in
|
|
345 |
resolve_tac prems' 1
|
|
346 |
end) ctxt
|
|
347 |
val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas}
|
|
348 |
in
|
|
349 |
EVERY'
|
|
350 |
[ etac exi_neg,
|
|
351 |
resolve_tac @{thms alpha_gen_sym_eqvt},
|
|
352 |
asm_full_simp_tac (HOL_ss addsimps prod_simps),
|
|
353 |
Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
|
|
354 |
trans_prem_tac pred_names ctxt ]
|
|
355 |
end
|
|
356 |
|
|
357 |
fun prove_sym_tac pred_names intros induct ctxt =
|
|
358 |
let
|
|
359 |
val prem_eq_tac = rtac @{thm sym} THEN' atac
|
|
360 |
val prem_unbound_tac = atac
|
|
361 |
|
|
362 |
val prem_cases_tacs = FIRST'
|
|
363 |
[prem_eq_tac, prem_unbound_tac, prem_bound_tac pred_names ctxt]
|
|
364 |
in
|
|
365 |
HEADGOAL (rtac induct THEN_ALL_NEW
|
|
366 |
(resolve_tac intros THEN_ALL_NEW prem_cases_tacs))
|
|
367 |
end
|
|
368 |
|
|
369 |
fun prep_sym_goal alpha_trm (arg1, arg2) =
|
|
370 |
let
|
|
371 |
val lhs = alpha_trm $ arg1 $ arg2
|
|
372 |
val rhs = alpha_trm $ arg2 $ arg1
|
|
373 |
in
|
|
374 |
HOLogic.mk_imp (lhs, rhs)
|
|
375 |
end
|
|
376 |
|
|
377 |
fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt =
|
|
378 |
let
|
|
379 |
val alpha_names = map (fst o dest_Const) alpha_trms
|
|
380 |
val arg_tys =
|
|
381 |
alpha_trms
|
|
382 |
|> map fastype_of
|
|
383 |
|> map domain_type
|
|
384 |
val (arg_names1, (arg_names2, ctxt')) =
|
|
385 |
ctxt
|
|
386 |
|> Variable.variant_fixes (replicate (length arg_tys) "x")
|
|
387 |
||> Variable.variant_fixes (replicate (length arg_tys) "y")
|
|
388 |
val args1 = map Free (arg_names1 ~~ arg_tys)
|
|
389 |
val args2 = map Free (arg_names2 ~~ arg_tys)
|
|
390 |
val goal = HOLogic.mk_Trueprop
|
|
391 |
(foldr1 HOLogic.mk_conj (map2 prep_sym_goal alpha_trms (args1 ~~ args2)))
|
|
392 |
in
|
|
393 |
Goal.prove ctxt' [] [] goal
|
|
394 |
(fn {context,...} => prove_sym_tac alpha_names alpha_intros alpha_induct context)
|
|
395 |
|> singleton (ProofContext.export ctxt' ctxt)
|
|
396 |
|> Datatype_Aux.split_conj_thm
|
|
397 |
|> map (fn th => zero_var_indexes (th RS mp))
|
|
398 |
end
|
|
399 |
|
|
400 |
|
2313
|
401 |
|
2311
|
402 |
(** transitivity proof for alphas **)
|
|
403 |
|
2313
|
404 |
fun ecases_tac cases =
|
|
405 |
Subgoal.FOCUS (fn {prems, ...} =>
|
|
406 |
HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
|
|
407 |
|
|
408 |
fun aatac pred_names =
|
|
409 |
SUBPROOF (fn {prems, context, ...} =>
|
|
410 |
HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
|
|
411 |
|
|
412 |
val perm_inst_tac =
|
|
413 |
Subgoal.FOCUS (fn {params, ...} =>
|
|
414 |
let
|
|
415 |
val (p, q) = pairself snd (last2 params)
|
|
416 |
val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q]
|
|
417 |
val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
|
|
418 |
in
|
|
419 |
HEADGOAL (rtac exi_inst)
|
|
420 |
end)
|
|
421 |
|
|
422 |
fun non_trivial_cases_tac pred_names intros ctxt =
|
|
423 |
let
|
|
424 |
val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
|
|
425 |
in
|
|
426 |
resolve_tac intros
|
|
427 |
THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN'
|
|
428 |
TRY o EVERY'
|
|
429 |
[ etac @{thm exE},
|
|
430 |
etac @{thm exE},
|
|
431 |
perm_inst_tac ctxt,
|
|
432 |
resolve_tac @{thms alpha_trans_eqvt},
|
|
433 |
atac,
|
|
434 |
aatac pred_names ctxt,
|
|
435 |
Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
|
|
436 |
asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
|
|
437 |
end
|
|
438 |
|
2311
|
439 |
fun prove_trans_tac pred_names raw_dt_thms intros induct cases ctxt =
|
|
440 |
let
|
2313
|
441 |
fun all_cases ctxt =
|
|
442 |
asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms)
|
|
443 |
THEN' TRY o non_trivial_cases_tac pred_names intros ctxt
|
2311
|
444 |
in
|
2313
|
445 |
HEADGOAL (rtac induct THEN_ALL_NEW
|
|
446 |
EVERY' [ rtac @{thm allI}, rtac @{thm impI},
|
|
447 |
ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ])
|
2311
|
448 |
end
|
|
449 |
|
2313
|
450 |
xfun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
|
2311
|
451 |
let
|
|
452 |
val lhs = alpha_trm $ arg1 $ arg2
|
|
453 |
val mid = alpha_trm $ arg2 $ (Bound 0)
|
|
454 |
val rhs = alpha_trm $ arg1 $ (Bound 0)
|
|
455 |
in
|
|
456 |
HOLogic.mk_imp (lhs,
|
|
457 |
HOLogic.all_const arg_ty $ Abs ("z", arg_ty,
|
|
458 |
HOLogic.mk_imp (mid, rhs)))
|
|
459 |
end
|
|
460 |
|
2313
|
461 |
val norm = @{lemma "A --> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp}
|
|
462 |
|
2311
|
463 |
fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt =
|
|
464 |
let
|
|
465 |
val alpha_names = map (fst o dest_Const) alpha_trms
|
|
466 |
val arg_tys =
|
|
467 |
alpha_trms
|
|
468 |
|> map fastype_of
|
|
469 |
|> map domain_type
|
|
470 |
val (arg_names1, (arg_names2, ctxt')) =
|
|
471 |
ctxt
|
|
472 |
|> Variable.variant_fixes (replicate (length arg_tys) "x")
|
|
473 |
||> Variable.variant_fixes (replicate (length arg_tys) "y")
|
|
474 |
val args1 = map Free (arg_names1 ~~ arg_tys)
|
|
475 |
val args2 = map Free (arg_names2 ~~ arg_tys)
|
|
476 |
val goal = HOLogic.mk_Trueprop
|
|
477 |
(foldr1 HOLogic.mk_conj (map2 prep_trans_goal alpha_trms (args1 ~~ args2 ~~ arg_tys)))
|
|
478 |
in
|
|
479 |
Goal.prove ctxt' [] [] goal
|
|
480 |
(fn {context,...} =>
|
|
481 |
prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_induct alpha_cases context)
|
|
482 |
|> singleton (ProofContext.export ctxt' ctxt)
|
|
483 |
|> Datatype_Aux.split_conj_thm
|
2313
|
484 |
|> map (fn th => zero_var_indexes (th RS norm))
|
2311
|
485 |
end
|
|
486 |
|
2297
|
487 |
end (* structure *)
|
|
488 |
|