# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266847793 -3600
# Node ID 05e5fcf9840bcd491d91ffe66ff4620cb79861f8
# Parent  10a0e3578507b32414785aa7bb1927793ddcce8a
export the reflp and symp tacs.

diff -r 10a0e3578507 -r 05e5fcf9840b Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Mon Feb 22 15:03:48 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 15:09:53 2010 +0100
@@ -116,24 +116,30 @@
   apply(simp add: permute_eqvt[symmetric])
   done
 
-prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
-by (tactic {*
-
- (indtac @{thm rtrm1_bp.induct} ["x", "x"] THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW
+ML {*
+fun reflp_tac induct inj =
+  rtac induct THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
   TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
   (rtac @{thm exI[of _ "0 :: perm"]} THEN'
-  asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
- ) 1 *})
+   asm_full_simp_tac (HOL_ss addsimps
+     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
+*}
+
+prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
+by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})
+
+ML {*
+fun symp_tac induct inj =
+  rtac induct THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
+  TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
+  (etac @{thm alpha_gen_compose_sym} THEN'
+   asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}))
+*}
 
 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
-by (tactic {*
- (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW
-  TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
- (etac @{thm alpha_gen_compose_sym} THEN'
-  asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt})
- )) 1 *})
+by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} 1 *})
 
 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
 apply (rule alpha_rtrm1_alpha_bp.induct)