equal
deleted
inserted
replaced
356 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
356 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
357 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
357 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
358 |
358 |
359 val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) |
359 val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) |
360 |
360 |
361 val tac = (Datatype_Aux.indtac induct perm_indnames |
361 val tac = (Datatype_Aux.ind_tac induct perm_indnames |
362 THEN_ALL_NEW asm_simp_tac simps) 1 |
362 THEN_ALL_NEW asm_simp_tac simps) 1 |
363 in |
363 in |
364 Goal.prove lthy perm_indnames [] goals (K tac) |
364 Goal.prove lthy perm_indnames [] goals (K tac) |
365 |> Datatype_Aux.split_conj_thm |
365 |> Datatype_Aux.split_conj_thm |
366 end |
366 end |
380 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
380 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
381 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
381 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
382 |
382 |
383 val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) |
383 val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) |
384 |
384 |
385 val tac = (Datatype_Aux.indtac induct perm_indnames |
385 val tac = (Datatype_Aux.ind_tac induct perm_indnames |
386 THEN_ALL_NEW asm_simp_tac simps) 1 |
386 THEN_ALL_NEW asm_simp_tac simps) 1 |
387 in |
387 in |
388 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
388 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
389 |> Datatype_Aux.split_conj_thm |
389 |> Datatype_Aux.split_conj_thm |
390 end |
390 end |