310 (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) |
310 (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) |
311 end |
311 end |
312 *} |
312 *} |
313 |
313 |
314 ML {* |
314 ML {* |
315 fun reflp_tac induct inj = |
315 fun reflp_tac induct inj ctxt = |
316 rtac induct THEN_ALL_NEW |
316 rtac induct THEN_ALL_NEW |
317 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
317 simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW |
318 (* TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW*) |
318 split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} |
319 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
319 THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps |
320 asm_full_simp_tac (HOL_ss addsimps |
320 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv |
321 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
321 add_0_left supp_zero_perm Int_empty_left}) |
322 *} |
322 *} |
|
323 |
323 |
324 |
324 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
325 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
325 apply (erule exE) |
326 apply (erule exE) |
326 apply (rule_tac x="-pi" in exI) |
327 apply (rule_tac x="-pi" in exI) |
327 by auto |
328 by auto |
398 ML {* |
399 ML {* |
399 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
400 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
400 let |
401 let |
401 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
402 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
402 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
403 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
403 fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1; |
404 fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1; |
404 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; |
405 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; |
405 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
406 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
406 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
407 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
407 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
408 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
408 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
409 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |