14 val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> |
14 val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> |
15 term list -> term list -> bn_info -> thm list * thm list |
15 term list -> term list -> bn_info -> thm list * thm list |
16 |
16 |
17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list |
17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list |
18 |
18 |
|
19 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
19 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
20 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 |
21 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list |
21 end |
22 end |
22 |
23 |
23 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
24 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
244 in |
245 in |
245 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
246 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
246 end |
247 end |
247 |
248 |
248 |
249 |
|
250 |
249 (** produces the distinctness theorems **) |
251 (** produces the distinctness theorems **) |
250 |
252 |
251 (* transforms the distinctness theorems of the constructors |
253 (* transforms the distinctness theorems of the constructors |
252 to "not-alphas" of the constructors *) |
254 to "not-alphas" of the constructors *) |
253 fun mk_alpha_distinct_goal alpha neq = |
255 fun mk_alpha_distinct_goal alpha neq = |
287 in |
289 in |
288 (flat alpha_distincts, flat alpha_bn_distincts) |
290 (flat alpha_distincts, flat alpha_bn_distincts) |
289 end |
291 end |
290 |
292 |
291 |
293 |
|
294 |
292 (** produces the alpha_eq_iff simplification rules **) |
295 (** produces the alpha_eq_iff simplification rules **) |
293 |
|
294 |
296 |
295 (* in case a theorem is of the form (C.. = C..), it will be |
297 (* in case a theorem is of the form (C.. = C..), it will be |
296 rewritten to ((C.. = C..) = True) *) |
298 rewritten to ((C.. = C..) = True) *) |
297 fun mk_simp_rule thm = |
299 fun mk_simp_rule thm = |
298 case (prop_of thm) of |
300 case (prop_of thm) of |
323 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
325 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; |
326 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
325 in |
327 in |
326 Variable.export ctxt' ctxt thms |
328 Variable.export ctxt' ctxt thms |
327 |> map mk_simp_rule |
329 |> map mk_simp_rule |
|
330 end |
|
331 |
|
332 |
|
333 |
|
334 (** reflexivity proof for the alphas **) |
|
335 |
|
336 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto} |
|
337 |
|
338 fun cases_tac intros = |
|
339 let |
|
340 val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps} |
|
341 |
|
342 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac |
|
343 |
|
344 val bound_tac = |
|
345 EVERY' [ rtac exi_zero, |
|
346 resolve_tac @{thms alpha_gen_refl}, |
|
347 asm_full_simp_tac (HOL_ss addsimps prod_simps) ] |
|
348 in |
|
349 REPEAT o FIRST' [rtac @{thm conjI}, |
|
350 resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]] |
|
351 end |
|
352 |
|
353 fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt = |
|
354 let |
|
355 val arg_tys = |
|
356 alpha_trms |
|
357 |> map fastype_of |
|
358 |> map domain_type |
|
359 val arg_bn_tys = |
|
360 alpha_bns |
|
361 |> map fastype_of |
|
362 |> map domain_type |
|
363 val arg_names = Datatype_Prop.make_tnames arg_tys |
|
364 val arg_bn_names = map (fn ty => the (AList.lookup (op=) (arg_tys ~~ arg_names) ty)) arg_bn_tys |
|
365 val args = map Free (arg_names ~~ arg_tys) |
|
366 val arg_bns = map Free (arg_bn_names ~~ arg_bn_tys) |
|
367 val goal = |
|
368 AList.group (op=) ((arg_bns ~~ alpha_bns) @ (args ~~ alpha_trms)) |
|
369 |> map (fn (ar, cnsts) => map (fn c => c $ ar $ ar) cnsts) |
|
370 |> map (foldr1 HOLogic.mk_conj) |
|
371 |> foldr1 HOLogic.mk_conj |
|
372 |> HOLogic.mk_Trueprop |
|
373 in |
|
374 Goal.prove ctxt arg_names [] goal |
|
375 (fn {context, ...} => |
|
376 HEADGOAL (DETERM o (rtac raw_dt_induct) THEN_ALL_NEW cases_tac alpha_intros)) |
|
377 |> Datatype_Aux.split_conj_thm |
|
378 |> map Datatype_Aux.split_conj_thm |
|
379 |> flat |
328 end |
380 end |
329 |
381 |
330 |
382 |
331 |
383 |
332 (** symmetry proof for the alphas **) |
384 (** symmetry proof for the alphas **) |