--- 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

--- a/Quot/Nominal/Terms.thy	Mon Feb 22 15:41:30 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 16:16:04 2010 +0100
@@ -116,43 +116,16 @@
   apply(simp add: permute_eqvt[symmetric])
   done
 
-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}))
-*}
+
 
 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'
-   eresolve_tac @{thms alpha1_eqvt})
-*}
-
 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
-by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} 1 *})
+by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *})
 
 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
-apply (tactic {*
- (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW 
-  (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN'
-  eresolve_tac @{thms alpha_rtrm1.cases alpha_bp.cases}) THEN_ALL_NEW
-  (
-    asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj rtrm1.distinct rtrm1.inject bp.distinct bp.inject}) 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 @{thms alpha1_eqvt}])
-  )
-) 1 *})
-done
+by (tactic {* transp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})
 
 lemma helper: "(\<forall>x y z. R x y \<and> R y z \<longrightarrow> R x z) = (\<forall>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z))"
 by meson
@@ -512,30 +485,6 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *}
 thm alpha5_inj
 
-lemma alpha5_equivps:
-  shows "equivp alpha_rtrm5"
-  and   "equivp alpha_rlts"
-sorry
-
-quotient_type
-  trm5 = rtrm5 / alpha_rtrm5
-and
-  lts = rlts / alpha_rlts
-  by (auto intro: alpha5_equivps)
-
-local_setup {*
-(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
- |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})))
-*}
-print_theorems
-
 lemma rbv5_eqvt:
   "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
 sorry
@@ -577,6 +526,50 @@
   apply (simp)
   done
 
+prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *}
+by (tactic {* reflp_tac @{thm rtrm5_rlts.induct} @{thms alpha5_inj} 1 *})
+
+prove alpha5_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *}
+by (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} 1 *})
+
+prove alpha5_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *}
+by (tactic {* transp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms rtrm5.inject rlts.inject} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} 1 *})
+
+lemma alpha5_equivps:
+  shows "equivp alpha_rtrm5"
+  and   "equivp alpha_rlts"
+ML_prf Goal.prove
+unfolding equivp_reflp_symp_transp reflp_def
+apply (simp_all add: alpha5_reflp_aux)
+unfolding symp_def
+apply (simp_all add: alpha5_symp_aux)
+unfolding transp_def
+apply (simp_all only: helper)
+apply (rule allI)+
+apply (rule conjunct1[OF alpha5_transp_aux])
+apply (rule allI)+
+apply (rule conjunct2[OF alpha5_transp_aux])
+done
+
+quotient_type
+  trm5 = rtrm5 / alpha_rtrm5
+and
+  lts = rlts / alpha_rlts
+  by (auto intro: alpha5_equivps)
+
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})))
+*}
+print_theorems
+
 lemma alpha5_rfv:
   "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
   "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"