361 val args2 = map2 (curry Free) arg_names2 arg_tys |
361 val args2 = map2 (curry Free) arg_names2 arg_tys |
362 |
362 |
363 val true_trms = replicate (length alphas) (K @{term True}) |
363 val true_trms = replicate (length alphas) (K @{term True}) |
364 |
364 |
365 fun apply_all x fs = map (fn f => f x) fs |
365 fun apply_all x fs = map (fn f => f x) fs |
366 val goal_rhs = |
366 val goals_rhs = |
367 group (props @ (alphas ~~ true_trms)) |
367 group (props @ (alphas ~~ true_trms)) |
368 |> map snd |
368 |> map snd |
369 |> map2 apply_all (args1 ~~ args2) |
369 |> map2 apply_all (args1 ~~ args2) |
370 |> map fold_conj |
370 |> map fold_conj |
371 |
371 |
372 fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2 |
372 fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2 |
373 val goal_lhs = map2 apply_trm_pair alphas (args1 ~~ args2) |
373 val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2) |
374 |
374 |
375 val goal = |
375 val goals = |
376 (map2 (curry HOLogic.mk_imp) goal_lhs goal_rhs) |
376 (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs) |
377 |> foldr1 HOLogic.mk_conj |
377 |> foldr1 HOLogic.mk_conj |
378 |> HOLogic.mk_Trueprop |
378 |> HOLogic.mk_Trueprop |
379 in |
379 |
380 Goal.prove ctxt' [] [] goal |
380 fun tac ctxt = |
381 (fn {context, ...} => HEADGOAL |
381 HEADGOAL |
382 (DETERM o (rtac alpha_induct_thm) THEN_ALL_NEW (rtac @{thm TrueI} ORELSE' cases_tac context))) |
382 (DETERM o (rtac alpha_induct_thm) |
|
383 THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt]) |
|
384 in |
|
385 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |
383 |> singleton (ProofContext.export ctxt' ctxt) |
386 |> singleton (ProofContext.export ctxt' ctxt) |
384 |> Datatype_Aux.split_conj_thm |
387 |> Datatype_Aux.split_conj_thm |
385 |> map (fn th => th RS mp) |
388 |> map (fn th => th RS mp) |
386 |> map Datatype_Aux.split_conj_thm |
389 |> map Datatype_Aux.split_conj_thm |
387 |> flat |
390 |> flat |
388 |> map zero_var_indexes |
391 |> map zero_var_indexes |
389 |
|
390 |> filter_out (is_true o concl_of) |
392 |> filter_out (is_true o concl_of) |
391 end |
393 end |
392 |
394 |
393 |
395 |
394 (** reflexivity proof for the alphas **) |
396 (** reflexivity proof for the alphas **) |