--- a/Nominal/nominal_dt_alpha.ML	Tue Jun 22 13:31:42 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Tue Jun 22 18:07:53 2010 +0100
@@ -19,6 +19,7 @@
   val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
   val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list
   val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
+  val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list
   val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
 end
 
@@ -542,6 +543,26 @@
     |> map (fn th => zero_var_indexes (th RS norm))
 end
 
+(* proves the equivp predicate for all alphas *)
+
+val equivp_intro = 
+  @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y z. R x y --> R y z --> R x z|] ==> equivp R"
+    by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)}
+
+fun raw_prove_equivp alphas refl symm trans ctxt = 
+let
+  val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
+  val refl' = map atomize refl
+  val symm' = map atomize symm
+  val trans' = map atomize trans
+  fun prep_goal t = 
+    HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) 
+in    
+  Goal.prove_multi ctxt [] [] (map prep_goal alphas)
+  (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac equivp_intro THEN' 
+     RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
+end
+
 
 (* proves that alpha_raw implies alpha_bn *)
 
@@ -549,17 +570,18 @@
   | is_true _ = false 
 
 fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = 
-  Subgoal.FOCUS (fn {prems, context, ...} => 
+  SUBPROOF (fn {prems, context, ...} => 
     let
       val prems' = flat (map Datatype_Aux.split_conj_thm prems)
       val prems'' = map (transform_prem1 context pred_names) prems'
     in
-      HEADGOAL (REPEAT o 
-        FIRST' [ rtac @{thm TrueI}, 
-                 rtac @{thm conjI}, 
-                 resolve_tac prems', 
-                 resolve_tac prems'',
-                 resolve_tac alpha_intros ])
+      HEADGOAL 
+        (REPEAT_ALL_NEW 
+           (FIRST' [ rtac @{thm TrueI}, 
+                     rtac @{thm conjI}, 
+                     resolve_tac prems', 
+                     resolve_tac prems'',
+                     resolve_tac alpha_intros ]))
     end) ctxt
 
 fun raw_prove_bn_imp alpha_trms alpha_bns alpha_intros alpha_induct ctxt =
@@ -604,7 +626,7 @@
   Goal.prove ctxt' [] [] goal
     (fn {context, ...} => 
        HEADGOAL (DETERM o (rtac alpha_induct) 
-         THEN_ALL_NEW raw_prove_bn_imp_tac alpha_names alpha_intros context)) 
+         THEN_ALL_NEW (raw_prove_bn_imp_tac alpha_names alpha_intros context)))
   |> singleton (ProofContext.export ctxt' ctxt)
   |> Datatype_Aux.split_conj_thm 
   |> map (fn th => zero_var_indexes (th RS mp))
@@ -613,6 +635,5 @@
   |> filter_out (is_true o concl_of)
 end
 
-
 end (* structure *)