301 |
301 |
302 ML {* |
302 ML {* |
303 fun reflp_tac induct inj = |
303 fun reflp_tac induct inj = |
304 rtac induct THEN_ALL_NEW |
304 rtac induct THEN_ALL_NEW |
305 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
305 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
306 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
306 (* TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW*) |
307 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
307 (rtac @{thm exI[of _ "0 :: perm"]} THEN' |
308 asm_full_simp_tac (HOL_ss addsimps |
308 asm_full_simp_tac (HOL_ss addsimps |
309 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
309 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
310 *} |
310 *} |
311 |
311 |
|
312 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi" |
|
313 apply (erule exE) |
|
314 apply (rule_tac x="-pi" in exI) |
|
315 by auto |
|
316 |
312 ML {* |
317 ML {* |
313 fun symp_tac induct inj eqvt = |
318 fun symp_tac induct inj eqvt = |
314 ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
319 (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
315 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
320 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
316 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
321 (etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN' |
317 (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) |
322 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
|
323 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
|
324 (etac @{thm alpha_gen_compose_sym} THEN' |
|
325 (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))))) |
318 *} |
326 *} |
319 |
327 |
320 ML {* |
328 ML {* |
321 fun imp_elim_tac case_rules = |
329 fun imp_elim_tac case_rules = |
322 Subgoal.FOCUS (fn {concl, context, ...} => |
330 Subgoal.FOCUS (fn {concl, context, ...} => |
338 end |
346 end |
339 | _ => no_tac |
347 | _ => no_tac |
340 ) |
348 ) |
341 *} |
349 *} |
342 |
350 |
|
351 |
|
352 lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi" |
|
353 apply (erule exE)+ |
|
354 apply (rule_tac x="pia + pi" in exI) |
|
355 by auto |
|
356 |
343 ML {* |
357 ML {* |
344 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
358 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = |
345 ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
359 ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
346 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
360 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
347 ( |
361 ( |
348 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' |
362 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) |
349 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
363 THEN_ALL_NEW (etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW |
350 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) |
364 (REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) |
|
365 THEN_ALL_NEW (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
|
366 (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW |
|
367 (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))) |
351 ) |
368 ) |
352 *} |
369 *} |
353 |
370 |
354 lemma transp_aux: |
371 lemma transp_aux: |
355 "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |
372 "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |