--- a/Quot/Nominal/Fv.thy	Mon Feb 22 15:41:30 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 16:16:04 2010 +0100
@@ -276,5 +276,49 @@
 end
 *}
 
+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}))
+*}
+
+ML {*
+fun symp_tac induct inj eqvt =
+  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' eresolve_tac eqvt)
+*}
+
+ML {*
+fun transp_tac induct alpha_inj term_inj distinct cases eqvt =
+  rtac induct THEN_ALL_NEW
+  (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN'
+  eresolve_tac cases) THEN_ALL_NEW
+  (
+    asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN'
+    TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
+    (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt])
+  )
+*}
+
+ML {*
+fun build_equivps alphas induct alpha_inj term_inj distinct cases eqvt ctxt =
+let
+  val (reflg, (symg, transg)) = build_alpha_refl_gl alphas
+  fun reflp_tac' _ = reflp_tac induct term_inj 1;
+  fun symp_tac' _ = symp_tac induct alpha_inj eqvt 1;
+  fun transp_tac' _ = transp_tac induct alpha_inj term_inj distinct cases eqvt 1;
+  val reflt = Goal.prove ctxt ["x"] [] reflg reflp_tac';
+  val symt = Goal.prove ctxt ["x","y"] [] symg symp_tac';
+  val transt = Goal.prove ctxt ["x","y","z"] [] transg transp_tac';
+in
+  (reflt, symt, transt)
+end
+*}
 
 end