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 |
|
2387
|
17 |
val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list ->
|
|
18 |
thm list -> (thm list * thm list)
|
2311
|
19 |
|
2389
|
20 |
val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm ->
|
|
21 |
(Proof.context -> int -> tactic) -> Proof.context -> thm list
|
|
22 |
|
2316
|
23 |
val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
|
2311
|
24 |
val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list
|
|
25 |
val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
|
2322
|
26 |
val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list
|
2320
|
27 |
val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
|
2387
|
28 |
val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list ->
|
|
29 |
term list -> thm -> thm list -> Proof.context -> thm list
|
2392
|
30 |
val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
|
2395
|
31 |
val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
|
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
val resolve_fun_rel: thm -> thm
|
2297
|
34 |
end
|
|
35 |
|
|
36 |
structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
|
|
37 |
struct
|
|
38 |
|
2320
|
39 |
fun lookup xs x = the (AList.lookup (op=) xs x)
|
|
40 |
fun group xs = AList.group (op=) xs
|
|
41 |
|
2300
|
42 |
(** definition of the inductive rules for alpha and alpha_bn **)
|
|
43 |
|
2297
|
44 |
(* construct the compound terms for prod_fv and prod_alpha *)
|
|
45 |
fun mk_prod_fv (t1, t2) =
|
|
46 |
let
|
|
47 |
val ty1 = fastype_of t1
|
|
48 |
val ty2 = fastype_of t2
|
|
49 |
val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}
|
|
50 |
in
|
|
51 |
Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2
|
|
52 |
end
|
|
53 |
|
|
54 |
fun mk_prod_alpha (t1, t2) =
|
|
55 |
let
|
|
56 |
val ty1 = fastype_of t1
|
|
57 |
val ty2 = fastype_of t2
|
|
58 |
val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)
|
|
59 |
val resT = [prodT, prodT] ---> @{typ "bool"}
|
|
60 |
in
|
|
61 |
Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2
|
|
62 |
end
|
|
63 |
|
|
64 |
(* generates the compound binder terms *)
|
|
65 |
fun mk_binders lthy bmode args bodies =
|
|
66 |
let
|
|
67 |
fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
|
|
68 |
| bind_set _ args (SOME bn, i) = bn $ (nth args i)
|
|
69 |
fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)
|
|
70 |
| bind_lst _ args (SOME bn, i) = bn $ (nth args i)
|
|
71 |
|
|
72 |
val (combine_fn, bind_fn) =
|
|
73 |
case bmode of
|
|
74 |
Lst => (mk_append, bind_lst)
|
|
75 |
| Set => (mk_union, bind_set)
|
|
76 |
| Res => (mk_union, bind_set)
|
|
77 |
in
|
2375
|
78 |
bodies
|
|
79 |
|> map (bind_fn lthy args)
|
|
80 |
|> foldl1 combine_fn
|
2297
|
81 |
end
|
|
82 |
|
|
83 |
(* produces the term for an alpha with abstraction *)
|
|
84 |
fun mk_alpha_term bmode fv alpha args args' binders binders' =
|
|
85 |
let
|
|
86 |
val (alpha_name, binder_ty) =
|
|
87 |
case bmode of
|
|
88 |
Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
|
|
89 |
| Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
|
|
90 |
| Res => (@{const_name "alpha_res"}, @{typ "atom set"})
|
|
91 |
val ty = fastype_of args
|
|
92 |
val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
|
|
93 |
val alpha_ty = [ty, ty] ---> @{typ "bool"}
|
|
94 |
val fv_ty = ty --> @{typ "atom set"}
|
|
95 |
val pair_lhs = HOLogic.mk_prod (binders, args)
|
|
96 |
val pair_rhs = HOLogic.mk_prod (binders', args')
|
|
97 |
in
|
|
98 |
HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},
|
|
99 |
Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool})
|
|
100 |
$ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs)
|
|
101 |
end
|
|
102 |
|
|
103 |
(* for non-recursive binders we have to produce alpha_bn premises *)
|
|
104 |
fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder =
|
|
105 |
case binder of
|
|
106 |
(NONE, _) => []
|
|
107 |
| (SOME bn, i) =>
|
|
108 |
if member (op=) bodies i then []
|
2320
|
109 |
else [lookup alpha_bn_map bn $ nth args i $ nth args' i]
|
2297
|
110 |
|
|
111 |
(* generat the premises for an alpha rule; mk_frees is used
|
|
112 |
if no binders are present *)
|
|
113 |
fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
|
|
114 |
let
|
|
115 |
fun mk_frees i =
|
|
116 |
let
|
|
117 |
val arg = nth args i
|
|
118 |
val arg' = nth args' i
|
|
119 |
val ty = fastype_of arg
|
|
120 |
in
|
|
121 |
if nth is_rec i
|
2320
|
122 |
then fst (lookup alpha_map ty) $ arg $ arg'
|
2297
|
123 |
else HOLogic.mk_eq (arg, arg')
|
|
124 |
end
|
|
125 |
|
|
126 |
fun mk_alpha_fv i =
|
|
127 |
let
|
|
128 |
val ty = fastype_of (nth args i)
|
|
129 |
in
|
|
130 |
case AList.lookup (op=) alpha_map ty of
|
|
131 |
NONE => (HOLogic.eq_const ty, supp_const ty)
|
|
132 |
| SOME (alpha, fv) => (alpha, fv)
|
|
133 |
end
|
|
134 |
in
|
|
135 |
case bclause of
|
|
136 |
BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies
|
|
137 |
| BC (bmode, binders, bodies) =>
|
|
138 |
let
|
|
139 |
val (alphas, fvs) = split_list (map mk_alpha_fv bodies)
|
|
140 |
val comp_fv = foldl1 mk_prod_fv fvs
|
|
141 |
val comp_alpha = foldl1 mk_prod_alpha alphas
|
|
142 |
val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
|
|
143 |
val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
|
|
144 |
val comp_binders = mk_binders lthy bmode args binders
|
|
145 |
val comp_binders' = mk_binders lthy bmode args' binders
|
|
146 |
val alpha_prem =
|
|
147 |
mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
|
|
148 |
val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)
|
|
149 |
in
|
|
150 |
map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)
|
|
151 |
end
|
|
152 |
end
|
|
153 |
|
|
154 |
(* produces the introduction rule for an alpha rule *)
|
|
155 |
fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses =
|
|
156 |
let
|
|
157 |
val arg_names = Datatype_Prop.make_tnames arg_tys
|
|
158 |
val arg_names' = Name.variant_list arg_names arg_names
|
|
159 |
val args = map Free (arg_names ~~ arg_tys)
|
|
160 |
val args' = map Free (arg_names' ~~ arg_tys)
|
2320
|
161 |
val alpha = fst (lookup alpha_map ty)
|
2297
|
162 |
val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
|
|
163 |
val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses
|
|
164 |
in
|
|
165 |
Library.foldr Logic.mk_implies (flat prems, concl)
|
|
166 |
end
|
|
167 |
|
|
168 |
(* produces the premise of an alpha-bn rule; we only need to
|
|
169 |
treat the case special where the binding clause is empty;
|
|
170 |
|
|
171 |
- if the body is not included in the bn_info, then we either
|
|
172 |
produce an equation or an alpha-premise
|
|
173 |
|
|
174 |
- if the body is included in the bn_info, then we create
|
|
175 |
either a recursive call to alpha-bn, or no premise *)
|
|
176 |
fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =
|
|
177 |
let
|
|
178 |
fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i =
|
|
179 |
let
|
|
180 |
val arg = nth args i
|
|
181 |
val arg' = nth args' i
|
|
182 |
val ty = fastype_of arg
|
|
183 |
in
|
|
184 |
case AList.lookup (op=) bn_args i of
|
|
185 |
NONE => (case (AList.lookup (op=) alpha_map ty) of
|
|
186 |
NONE => [HOLogic.mk_eq (arg, arg')]
|
|
187 |
| SOME (alpha, _) => [alpha $ arg $ arg'])
|
|
188 |
| SOME (NONE) => []
|
2320
|
189 |
| SOME (SOME bn) => [lookup alpha_bn_map bn $ arg $ arg']
|
2297
|
190 |
end
|
|
191 |
in
|
|
192 |
case bclause of
|
|
193 |
BC (_, [], bodies) =>
|
|
194 |
map HOLogic.mk_Trueprop
|
|
195 |
(flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies))
|
|
196 |
| _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
|
|
197 |
end
|
|
198 |
|
|
199 |
fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
|
|
200 |
let
|
|
201 |
val arg_names = Datatype_Prop.make_tnames arg_tys
|
|
202 |
val arg_names' = Name.variant_list arg_names arg_names
|
|
203 |
val args = map Free (arg_names ~~ arg_tys)
|
|
204 |
val args' = map Free (arg_names' ~~ arg_tys)
|
2320
|
205 |
val alpha_bn = lookup alpha_bn_map bn_trm
|
2297
|
206 |
val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
|
|
207 |
val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses
|
|
208 |
in
|
|
209 |
Library.foldr Logic.mk_implies (flat prems, concl)
|
|
210 |
end
|
|
211 |
|
|
212 |
fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) =
|
|
213 |
let
|
|
214 |
val nth_constrs_info = nth constrs_info bn_n
|
|
215 |
val nth_bclausess = nth bclausesss bn_n
|
|
216 |
in
|
|
217 |
map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
|
|
218 |
end
|
|
219 |
|
|
220 |
fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy =
|
|
221 |
let
|
|
222 |
val alpha_names = prefix_dt_names descr sorts "alpha_"
|
|
223 |
val alpha_arg_tys = all_dtyps descr sorts
|
|
224 |
val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys
|
|
225 |
val alpha_frees = map Free (alpha_names ~~ alpha_tys)
|
|
226 |
val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs)
|
|
227 |
|
|
228 |
val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
|
|
229 |
val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
|
|
230 |
val alpha_bn_names = map (prefix "alpha_") bn_names
|
|
231 |
val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
|
|
232 |
val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys
|
|
233 |
val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
|
|
234 |
val alpha_bn_map = bns ~~ alpha_bn_frees
|
|
235 |
|
|
236 |
val constrs_info = all_dtyp_constrs_types descr sorts
|
|
237 |
|
|
238 |
val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss
|
|
239 |
val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info
|
|
240 |
|
2299
|
241 |
val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
|
|
242 |
(alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
|
2297
|
243 |
val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
|
|
244 |
|
|
245 |
val (alphas, lthy') = Inductive.add_inductive_i
|
|
246 |
{quiet_mode = true, verbose = false, alt_name = Binding.empty,
|
2300
|
247 |
coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
|
2297
|
248 |
all_alpha_names [] all_alpha_intros [] lthy
|
|
249 |
|
2298
|
250 |
val all_alpha_trms_loc = #preds alphas;
|
2297
|
251 |
val alpha_induct_loc = #raw_induct alphas;
|
|
252 |
val alpha_intros_loc = #intrs alphas;
|
|
253 |
val alpha_cases_loc = #elims alphas;
|
|
254 |
val phi = ProofContext.export_morphism lthy' lthy;
|
|
255 |
|
2298
|
256 |
val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc;
|
2297
|
257 |
val alpha_induct = Morphism.thm phi alpha_induct_loc;
|
|
258 |
val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
|
|
259 |
val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
|
2298
|
260 |
|
|
261 |
val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms
|
2297
|
262 |
in
|
2298
|
263 |
(alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
|
2297
|
264 |
end
|
|
265 |
|
2300
|
266 |
|
2316
|
267 |
|
2300
|
268 |
(** produces the distinctness theorems **)
|
|
269 |
|
|
270 |
(* transforms the distinctness theorems of the constructors
|
|
271 |
to "not-alphas" of the constructors *)
|
|
272 |
fun mk_alpha_distinct_goal alpha neq =
|
|
273 |
let
|
|
274 |
val (lhs, rhs) =
|
|
275 |
neq
|
|
276 |
|> HOLogic.dest_Trueprop
|
|
277 |
|> HOLogic.dest_not
|
|
278 |
|> HOLogic.dest_eq
|
|
279 |
in
|
|
280 |
alpha $ lhs $ rhs
|
|
281 |
|> HOLogic.mk_not
|
|
282 |
|> HOLogic.mk_Trueprop
|
|
283 |
end
|
|
284 |
|
|
285 |
fun distinct_tac cases distinct_thms =
|
|
286 |
rtac notI THEN' eresolve_tac cases
|
|
287 |
THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
|
|
288 |
|
|
289 |
fun mk_alpha_distinct ctxt cases_thms (distinct_thm, alpha) =
|
|
290 |
let
|
|
291 |
val ((_, thms), ctxt') = Variable.import false distinct_thm ctxt
|
|
292 |
val goals = map (mk_alpha_distinct_goal alpha o prop_of) thms
|
|
293 |
val nrels = map (fn t => Goal.prove ctxt' [] [] t (K (distinct_tac cases_thms distinct_thm 1))) goals
|
|
294 |
in
|
|
295 |
Variable.export ctxt' ctxt nrels
|
|
296 |
end
|
|
297 |
|
|
298 |
fun mk_alpha_distincts ctxt alpha_cases constrs_distinct_thms alpha_trms alpha_bn_trms bn_infos =
|
|
299 |
let
|
|
300 |
val alpha_distincts =
|
|
301 |
map (mk_alpha_distinct ctxt alpha_cases) (constrs_distinct_thms ~~ alpha_trms)
|
|
302 |
val distinc_thms = map
|
|
303 |
val alpha_bn_distincts_aux = map (fn (_, i, _) => nth constrs_distinct_thms i) bn_infos
|
|
304 |
val alpha_bn_distincts =
|
|
305 |
map (mk_alpha_distinct ctxt alpha_cases) (alpha_bn_distincts_aux ~~ alpha_bn_trms)
|
|
306 |
in
|
|
307 |
(flat alpha_distincts, flat alpha_bn_distincts)
|
|
308 |
end
|
|
309 |
|
|
310 |
|
2316
|
311 |
|
2300
|
312 |
(** produces the alpha_eq_iff simplification rules **)
|
|
313 |
|
|
314 |
(* in case a theorem is of the form (C.. = C..), it will be
|
|
315 |
rewritten to ((C.. = C..) = True) *)
|
|
316 |
fun mk_simp_rule thm =
|
|
317 |
case (prop_of thm) of
|
|
318 |
@{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm]
|
|
319 |
| _ => thm
|
|
320 |
|
|
321 |
fun alpha_eq_iff_tac dist_inj intros elims =
|
|
322 |
SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE'
|
|
323 |
(rtac @{thm iffI} THEN'
|
|
324 |
RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj),
|
|
325 |
asm_full_simp_tac (HOL_ss addsimps intros)])
|
|
326 |
|
|
327 |
fun mk_alpha_eq_iff_goal thm =
|
|
328 |
let
|
|
329 |
val prop = prop_of thm;
|
|
330 |
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
|
|
331 |
val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
|
|
332 |
fun list_conj l = foldr1 HOLogic.mk_conj l;
|
|
333 |
in
|
|
334 |
if hyps = [] then HOLogic.mk_Trueprop concl
|
|
335 |
else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
|
|
336 |
end;
|
|
337 |
|
|
338 |
fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims =
|
|
339 |
let
|
|
340 |
val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
|
|
341 |
val goals = map mk_alpha_eq_iff_goal thms_imp;
|
|
342 |
val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1;
|
|
343 |
val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
|
|
344 |
in
|
|
345 |
Variable.export ctxt' ctxt thms
|
2387
|
346 |
|> `(map mk_simp_rule)
|
2300
|
347 |
end
|
|
348 |
|
2311
|
349 |
|
2389
|
350 |
(** proof by induction over the alpha-definitions **)
|
|
351 |
|
|
352 |
fun is_true @{term "Trueprop True"} = true
|
|
353 |
| is_true _ = false
|
|
354 |
|
|
355 |
fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
|
|
356 |
let
|
|
357 |
val arg_tys = map (domain_type o fastype_of) alphas
|
|
358 |
|
|
359 |
val ((arg_names1, arg_names2), ctxt') =
|
|
360 |
ctxt
|
|
361 |
|> Variable.variant_fixes (replicate (length alphas) "x")
|
|
362 |
||>> Variable.variant_fixes (replicate (length alphas) "y")
|
|
363 |
|
|
364 |
val args1 = map2 (curry Free) arg_names1 arg_tys
|
|
365 |
val args2 = map2 (curry Free) arg_names2 arg_tys
|
|
366 |
|
|
367 |
val true_trms = replicate (length alphas) (K @{term True})
|
|
368 |
|
|
369 |
fun apply_all x fs = map (fn f => f x) fs
|
2391
|
370 |
val goals_rhs =
|
2389
|
371 |
group (props @ (alphas ~~ true_trms))
|
|
372 |
|> map snd
|
|
373 |
|> map2 apply_all (args1 ~~ args2)
|
|
374 |
|> map fold_conj
|
|
375 |
|
|
376 |
fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2
|
2391
|
377 |
val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)
|
2389
|
378 |
|
2391
|
379 |
val goals =
|
|
380 |
(map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs)
|
2389
|
381 |
|> foldr1 HOLogic.mk_conj
|
|
382 |
|> HOLogic.mk_Trueprop
|
2391
|
383 |
|
|
384 |
fun tac ctxt =
|
|
385 |
HEADGOAL
|
|
386 |
(DETERM o (rtac alpha_induct_thm)
|
|
387 |
THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
|
2389
|
388 |
in
|
2391
|
389 |
Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
|
2389
|
390 |
|> singleton (ProofContext.export ctxt' ctxt)
|
2390
|
391 |
|> Datatype_Aux.split_conj_thm
|
|
392 |
|> map (fn th => th RS mp)
|
2389
|
393 |
|> map Datatype_Aux.split_conj_thm
|
|
394 |
|> flat
|
|
395 |
|> map zero_var_indexes
|
|
396 |
|> filter_out (is_true o concl_of)
|
|
397 |
end
|
|
398 |
|
2311
|
399 |
|
2316
|
400 |
(** reflexivity proof for the alphas **)
|
|
401 |
|
|
402 |
val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}
|
|
403 |
|
|
404 |
fun cases_tac intros =
|
|
405 |
let
|
|
406 |
val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
|
|
407 |
|
|
408 |
val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac
|
|
409 |
|
|
410 |
val bound_tac =
|
|
411 |
EVERY' [ rtac exi_zero,
|
2385
|
412 |
resolve_tac @{thms alpha_refl},
|
2316
|
413 |
asm_full_simp_tac (HOL_ss addsimps prod_simps) ]
|
|
414 |
in
|
|
415 |
REPEAT o FIRST' [rtac @{thm conjI},
|
|
416 |
resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]]
|
|
417 |
end
|
|
418 |
|
|
419 |
fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt =
|
|
420 |
let
|
|
421 |
val arg_tys =
|
|
422 |
alpha_trms
|
|
423 |
|> map fastype_of
|
|
424 |
|> map domain_type
|
|
425 |
val arg_bn_tys =
|
|
426 |
alpha_bns
|
|
427 |
|> map fastype_of
|
|
428 |
|> map domain_type
|
|
429 |
val arg_names = Datatype_Prop.make_tnames arg_tys
|
2320
|
430 |
val arg_bn_names = map (lookup (arg_tys ~~ arg_names)) arg_bn_tys
|
2316
|
431 |
val args = map Free (arg_names ~~ arg_tys)
|
|
432 |
val arg_bns = map Free (arg_bn_names ~~ arg_bn_tys)
|
|
433 |
val goal =
|
2320
|
434 |
group ((arg_bns ~~ alpha_bns) @ (args ~~ alpha_trms))
|
2316
|
435 |
|> map (fn (ar, cnsts) => map (fn c => c $ ar $ ar) cnsts)
|
|
436 |
|> map (foldr1 HOLogic.mk_conj)
|
|
437 |
|> foldr1 HOLogic.mk_conj
|
|
438 |
|> HOLogic.mk_Trueprop
|
|
439 |
in
|
|
440 |
Goal.prove ctxt arg_names [] goal
|
|
441 |
(fn {context, ...} =>
|
|
442 |
HEADGOAL (DETERM o (rtac raw_dt_induct) THEN_ALL_NEW cases_tac alpha_intros))
|
|
443 |
|> Datatype_Aux.split_conj_thm
|
|
444 |
|> map Datatype_Aux.split_conj_thm
|
|
445 |
|> flat
|
|
446 |
end
|
|
447 |
|
|
448 |
|
|
449 |
|
2311
|
450 |
(** symmetry proof for the alphas **)
|
|
451 |
|
|
452 |
val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p"
|
|
453 |
by (erule exE, rule_tac x="-p" in exI, auto)}
|
|
454 |
|
|
455 |
(* for premises that contain binders *)
|
|
456 |
fun prem_bound_tac pred_names ctxt =
|
|
457 |
let
|
|
458 |
fun trans_prem_tac pred_names ctxt =
|
|
459 |
SUBPROOF (fn {prems, context, ...} =>
|
|
460 |
let
|
|
461 |
val prems' = map (transform_prem1 context pred_names) prems
|
|
462 |
in
|
|
463 |
resolve_tac prems' 1
|
|
464 |
end) ctxt
|
|
465 |
val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas}
|
|
466 |
in
|
|
467 |
EVERY'
|
|
468 |
[ etac exi_neg,
|
2385
|
469 |
resolve_tac @{thms alpha_sym_eqvt},
|
2311
|
470 |
asm_full_simp_tac (HOL_ss addsimps prod_simps),
|
|
471 |
Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
|
|
472 |
trans_prem_tac pred_names ctxt ]
|
|
473 |
end
|
|
474 |
|
|
475 |
fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt =
|
|
476 |
let
|
2389
|
477 |
val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
|
|
478 |
|
|
479 |
fun tac ctxt =
|
|
480 |
let
|
|
481 |
val alpha_names = map (fst o dest_Const) alpha_trms
|
|
482 |
in
|
|
483 |
resolve_tac alpha_intros THEN_ALL_NEW
|
|
484 |
FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names ctxt]
|
|
485 |
end
|
2311
|
486 |
in
|
2389
|
487 |
alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt
|
2311
|
488 |
end
|
|
489 |
|
|
490 |
|
|
491 |
(** transitivity proof for alphas **)
|
|
492 |
|
2314
|
493 |
(* applies cases rules and resolves them with the last premise *)
|
2313
|
494 |
fun ecases_tac cases =
|
|
495 |
Subgoal.FOCUS (fn {prems, ...} =>
|
|
496 |
HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
|
|
497 |
|
|
498 |
fun aatac pred_names =
|
|
499 |
SUBPROOF (fn {prems, context, ...} =>
|
|
500 |
HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
|
|
501 |
|
2314
|
502 |
(* instantiates exI with the permutation p + q *)
|
2313
|
503 |
val perm_inst_tac =
|
|
504 |
Subgoal.FOCUS (fn {params, ...} =>
|
|
505 |
let
|
|
506 |
val (p, q) = pairself snd (last2 params)
|
|
507 |
val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q]
|
|
508 |
val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
|
|
509 |
in
|
|
510 |
HEADGOAL (rtac exi_inst)
|
|
511 |
end)
|
|
512 |
|
|
513 |
fun non_trivial_cases_tac pred_names intros ctxt =
|
|
514 |
let
|
|
515 |
val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
|
|
516 |
in
|
|
517 |
resolve_tac intros
|
|
518 |
THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN'
|
2314
|
519 |
TRY o EVERY' (* if binders are present *)
|
2313
|
520 |
[ etac @{thm exE},
|
|
521 |
etac @{thm exE},
|
|
522 |
perm_inst_tac ctxt,
|
|
523 |
resolve_tac @{thms alpha_trans_eqvt},
|
|
524 |
atac,
|
|
525 |
aatac pred_names ctxt,
|
|
526 |
Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
|
|
527 |
asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
|
|
528 |
end
|
|
529 |
|
2389
|
530 |
fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt =
|
2311
|
531 |
let
|
2313
|
532 |
fun all_cases ctxt =
|
|
533 |
asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms)
|
|
534 |
THEN' TRY o non_trivial_cases_tac pred_names intros ctxt
|
2311
|
535 |
in
|
2389
|
536 |
EVERY' [ rtac @{thm allI}, rtac @{thm impI},
|
|
537 |
ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]
|
2311
|
538 |
end
|
|
539 |
|
2389
|
540 |
fun prep_trans_goal alpha_trm (arg1, arg2) =
|
2311
|
541 |
let
|
2389
|
542 |
val arg_ty = fastype_of arg1
|
2311
|
543 |
val mid = alpha_trm $ arg2 $ (Bound 0)
|
|
544 |
val rhs = alpha_trm $ arg1 $ (Bound 0)
|
|
545 |
in
|
2389
|
546 |
HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs))
|
2311
|
547 |
end
|
|
548 |
|
|
549 |
fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt =
|
|
550 |
let
|
2389
|
551 |
val alpha_names = map (fst o dest_Const) alpha_trms
|
|
552 |
val props = map prep_trans_goal alpha_trms
|
|
553 |
val norm = @{lemma "A ==> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp}
|
2311
|
554 |
in
|
2389
|
555 |
alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct
|
|
556 |
(prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt
|
2311
|
557 |
end
|
|
558 |
|
2390
|
559 |
|
|
560 |
(** proves the equivp predicate for all alphas **)
|
2322
|
561 |
|
|
562 |
val equivp_intro =
|
2389
|
563 |
@{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y. R x y --> (!z. R y z --> R x z)|] ==> equivp R"
|
2322
|
564 |
by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)}
|
|
565 |
|
|
566 |
fun raw_prove_equivp alphas refl symm trans ctxt =
|
|
567 |
let
|
|
568 |
val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
|
|
569 |
val refl' = map atomize refl
|
|
570 |
val symm' = map atomize symm
|
|
571 |
val trans' = map atomize trans
|
|
572 |
fun prep_goal t =
|
|
573 |
HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t)
|
|
574 |
in
|
|
575 |
Goal.prove_multi ctxt [] [] (map prep_goal alphas)
|
|
576 |
(K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac equivp_intro THEN'
|
|
577 |
RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
|
|
578 |
end
|
|
579 |
|
2320
|
580 |
|
|
581 |
(* proves that alpha_raw implies alpha_bn *)
|
|
582 |
|
|
583 |
fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt =
|
2322
|
584 |
SUBPROOF (fn {prems, context, ...} =>
|
2320
|
585 |
let
|
|
586 |
val prems' = flat (map Datatype_Aux.split_conj_thm prems)
|
|
587 |
val prems'' = map (transform_prem1 context pred_names) prems'
|
|
588 |
in
|
2322
|
589 |
HEADGOAL
|
|
590 |
(REPEAT_ALL_NEW
|
|
591 |
(FIRST' [ rtac @{thm TrueI},
|
|
592 |
rtac @{thm conjI},
|
|
593 |
resolve_tac prems',
|
|
594 |
resolve_tac prems'',
|
|
595 |
resolve_tac alpha_intros ]))
|
2320
|
596 |
end) ctxt
|
|
597 |
|
2390
|
598 |
fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt =
|
2320
|
599 |
let
|
2390
|
600 |
val arg_ty = domain_type o fastype_of
|
2320
|
601 |
val alpha_names = map (fst o dest_Const) alpha_trms
|
2390
|
602 |
val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
|
|
603 |
val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms
|
2320
|
604 |
in
|
2390
|
605 |
alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct
|
|
606 |
(raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt
|
2320
|
607 |
end
|
|
608 |
|
2387
|
609 |
|
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
610 |
(* respectfulness for fv_raw / bn_raw *)
|
2387
|
611 |
|
|
612 |
fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
|
|
613 |
let
|
2390
|
614 |
val arg_ty = domain_type o fastype_of
|
|
615 |
val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
|
2387
|
616 |
|
2390
|
617 |
val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) fvs
|
|
618 |
val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) bns
|
|
619 |
val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => HOLogic.mk_eq (t2 $ x, t2 $ y))) alpha_bn_trms fv_bns
|
2387
|
620 |
|
|
621 |
val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps}
|
|
622 |
@ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left})
|
|
623 |
in
|
2390
|
624 |
alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct
|
|
625 |
(K (asm_full_simp_tac ss)) ctxt
|
2387
|
626 |
end
|
|
627 |
|
2395
|
628 |
|
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
629 |
(* respectfulness for size *)
|
2392
|
630 |
|
|
631 |
fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
|
|
632 |
let
|
|
633 |
val arg_tys = map (domain_type o fastype_of) all_alpha_trms
|
|
634 |
|
|
635 |
fun mk_prop ty (x, y) = HOLogic.mk_eq
|
|
636 |
(HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)
|
|
637 |
|
|
638 |
val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys
|
|
639 |
|
|
640 |
val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel.simps
|
|
641 |
permute_prod_def prod.cases prod.recs})
|
|
642 |
|
|
643 |
val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
|
|
644 |
in
|
|
645 |
alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt
|
|
646 |
end
|
|
647 |
|
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
648 |
|
2395
|
649 |
(* respectfulness for constructors *)
|
|
650 |
|
|
651 |
fun raw_constr_rsp_tac alpha_intros simps =
|
|
652 |
let
|
|
653 |
val pre_ss = HOL_ss addsimps @{thms fun_rel_def}
|
|
654 |
val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel.simps
|
|
655 |
prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps
|
|
656 |
(* funs_rsp alpha_bn_simps *)
|
|
657 |
in
|
|
658 |
asm_full_simp_tac pre_ss
|
|
659 |
THEN' REPEAT o (resolve_tac @{thms allI impI})
|
|
660 |
THEN' resolve_tac alpha_intros
|
|
661 |
THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
|
|
662 |
end
|
|
663 |
|
|
664 |
|
|
665 |
fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =
|
|
666 |
let
|
|
667 |
val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms
|
|
668 |
|
|
669 |
fun lookup ty =
|
|
670 |
case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of
|
|
671 |
NONE => HOLogic.eq_const ty
|
|
672 |
| SOME alpha => alpha
|
|
673 |
|
|
674 |
fun fun_rel_app t1 t2 =
|
|
675 |
Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2
|
|
676 |
|
|
677 |
fun prep_goal trm =
|
|
678 |
trm
|
|
679 |
|> strip_type o fastype_of
|
|
680 |
|>> map lookup
|
|
681 |
||> lookup
|
|
682 |
|> uncurry (fold_rev fun_rel_app)
|
|
683 |
|> (fn t => t $ trm $ trm)
|
|
684 |
|> Syntax.check_term ctxt
|
|
685 |
|> HOLogic.mk_Trueprop
|
|
686 |
in
|
|
687 |
Goal.prove_multi ctxt [] [] (map prep_goal constrs)
|
|
688 |
(K (HEADGOAL
|
|
689 |
(Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))
|
|
690 |
end
|
|
691 |
|
|
692 |
|
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
693 |
(* resolve with @{thm fun_relI} *)
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
694 |
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
695 |
fun resolve_fun_rel thm =
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
696 |
let
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
697 |
val fun_rel = @{thm fun_relI}
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
698 |
val thm' = forall_intr_vars thm
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
699 |
val cinsts = Thm.match (cprem_of fun_rel 1, cprop_of thm')
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
700 |
val fun_rel' = Thm.instantiate cinsts fun_rel
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
701 |
in
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
702 |
thm' COMP fun_rel'
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
703 |
end
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
704 |
|
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
705 |
|
2297
|
706 |
end (* structure *)
|
|
707 |
|