14 term list -> typ list -> thm list |
14 term list -> typ list -> thm list |
15 |
15 |
16 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
16 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
17 thm list -> thm list |
17 thm list -> thm list |
18 |
18 |
|
19 val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> |
|
20 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
|
21 |
19 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
22 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
20 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
23 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
21 |
24 |
22 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
25 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
23 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
26 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
349 Variable.export ctxt' ctxt thms |
352 Variable.export ctxt' ctxt thms |
350 |> map mk_simp_rule |
353 |> map mk_simp_rule |
351 end |
354 end |
352 |
355 |
353 |
356 |
|
357 (** proof by induction over types **) |
|
358 |
|
359 fun induct_prove tys props induct_thm cases_tac ctxt = |
|
360 let |
|
361 val (arg_names, ctxt') = |
|
362 Variable.variant_fixes (replicate (length tys) "x") ctxt |
|
363 |
|
364 val args = map2 (curry Free) arg_names tys |
|
365 |
|
366 val true_trms = replicate (length tys) (K @{term True}) |
|
367 |
|
368 fun apply_all x fs = map (fn f => f x) fs |
|
369 |
|
370 val goals = |
|
371 group (props @ (tys ~~ true_trms)) |
|
372 |> map snd |
|
373 |> map2 apply_all args |
|
374 |> map fold_conj |
|
375 |> foldr1 HOLogic.mk_conj |
|
376 |> HOLogic.mk_Trueprop |
|
377 |
|
378 fun tac ctxt = |
|
379 HEADGOAL |
|
380 (DETERM o (rtac induct_thm) |
|
381 THEN_ALL_NEW |
|
382 (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt]))) |
|
383 in |
|
384 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |
|
385 |> singleton (ProofContext.export ctxt' ctxt) |
|
386 |> Datatype_Aux.split_conj_thm |
|
387 |> map Datatype_Aux.split_conj_thm |
|
388 |> flat |
|
389 |> filter_out (is_true o concl_of) |
|
390 |> map zero_var_indexes |
|
391 end |
|
392 |
|
393 |
354 (** proof by induction over the alpha-definitions **) |
394 (** proof by induction over the alpha-definitions **) |
355 |
|
356 fun is_true @{term "Trueprop True"} = true |
|
357 | is_true _ = false |
|
358 |
395 |
359 fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt = |
396 fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt = |
360 let |
397 let |
361 val arg_tys = map (domain_type o fastype_of) alphas |
398 val arg_tys = map (domain_type o fastype_of) alphas |
362 |
399 |
395 |> singleton (ProofContext.export ctxt' ctxt) |
432 |> singleton (ProofContext.export ctxt' ctxt) |
396 |> Datatype_Aux.split_conj_thm |
433 |> Datatype_Aux.split_conj_thm |
397 |> map (fn th => th RS mp) |
434 |> map (fn th => th RS mp) |
398 |> map Datatype_Aux.split_conj_thm |
435 |> map Datatype_Aux.split_conj_thm |
399 |> flat |
436 |> flat |
|
437 |> filter_out (is_true o concl_of) |
400 |> map zero_var_indexes |
438 |> map zero_var_indexes |
401 |> filter_out (is_true o concl_of) |
|
402 end |
439 end |
403 |
440 |
404 |
441 |
405 (** reflexivity proof for the alphas **) |
442 (** reflexivity proof for the alphas **) |
406 |
443 |
407 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto} |
444 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto} |
408 |
445 |
409 fun cases_tac intros = |
446 fun cases_tac intros ctxt = |
410 let |
447 let |
411 val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps} |
448 val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps} |
412 |
449 |
413 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac |
450 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac |
414 |
451 |
415 val bound_tac = |
452 val bound_tac = |
416 EVERY' [ rtac exi_zero, |
453 EVERY' [ rtac exi_zero, |
417 resolve_tac @{thms alpha_refl}, |
454 resolve_tac @{thms alpha_refl}, |
418 asm_full_simp_tac (HOL_ss addsimps prod_simps) ] |
455 asm_full_simp_tac (HOL_ss addsimps prod_simps) ] |
419 in |
456 in |
420 REPEAT o FIRST' [rtac @{thm conjI}, |
457 resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac] |
421 resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]] |
|
422 end |
458 end |
423 |
459 |
424 fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt = |
460 fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt = |
425 let |
461 let |
426 val arg_tys = |
462 val arg_tys = |
427 alpha_trms |
463 alpha_trms |
428 |> map fastype_of |
464 |> map fastype_of |
429 |> map domain_type |
465 |> map domain_type |
|
466 |
430 val arg_bn_tys = |
467 val arg_bn_tys = |
431 alpha_bns |
468 alpha_bns |
432 |> map fastype_of |
469 |> map fastype_of |
433 |> map domain_type |
470 |> map domain_type |
434 val arg_names = Datatype_Prop.make_tnames arg_tys |
471 |
435 val arg_bn_names = map (lookup (arg_tys ~~ arg_names)) arg_bn_tys |
472 val props = |
436 val args = map Free (arg_names ~~ arg_tys) |
473 map (fn (ty, c) => (ty, fn x => c $ x $ x)) |
437 val arg_bns = map Free (arg_bn_names ~~ arg_bn_tys) |
474 ((arg_tys ~~ alpha_trms) @ (arg_bn_tys ~~ alpha_bns)) |
438 val goal = |
475 in |
439 group ((arg_bns ~~ alpha_bns) @ (args ~~ alpha_trms)) |
476 induct_prove arg_tys props raw_dt_induct (cases_tac alpha_intros) ctxt |
440 |> map (fn (ar, cnsts) => map (fn c => c $ ar $ ar) cnsts) |
|
441 |> map (foldr1 HOLogic.mk_conj) |
|
442 |> foldr1 HOLogic.mk_conj |
|
443 |> HOLogic.mk_Trueprop |
|
444 in |
|
445 Goal.prove ctxt arg_names [] goal |
|
446 (fn {context, ...} => |
|
447 HEADGOAL (DETERM o (rtac raw_dt_induct) THEN_ALL_NEW cases_tac alpha_intros)) |
|
448 |> Datatype_Aux.split_conj_thm |
|
449 |> map Datatype_Aux.split_conj_thm |
|
450 |> flat |
|
451 end |
477 end |
452 |
478 |
453 |
479 |
454 |
480 |
455 (** symmetry proof for the alphas **) |
481 (** symmetry proof for the alphas **) |