--- a/Nominal/Ex/CoreHaskell.thy	Tue Jun 22 13:31:42 2010 +0100
+++ b/Nominal/Ex/CoreHaskell.thy	Tue Jun 22 18:07:53 2010 +0100
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 13]]
+declare [[STEPS = 14]]
 
 nominal_datatype tkind =
   KStar

--- a/Nominal/Ex/SingleLet.thy	Tue Jun 22 13:31:42 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Tue Jun 22 18:07:53 2010 +0100
@@ -4,7 +4,7 @@
 
 atom_decl name
 
-declare [[STEPS = 13]]
+declare [[STEPS = 14]]
 
 nominal_datatype trm =
   Var "name"
@@ -21,7 +21,6 @@
 where
   "bn (As x y t) = {atom x}"
 
-
 thm trm_assg.fv
 thm trm_assg.supp
 thm trm_assg.eq_iff

--- a/Nominal/NewParser.thy	Tue Jun 22 13:31:42 2010 +0100
+++ b/Nominal/NewParser.thy	Tue Jun 22 18:07:53 2010 +0100
@@ -436,44 +436,36 @@
            alpha_intros alpha_induct alpha_cases lthy_tmp'' 
     else raise TEST lthy4
 
+  val alpha_equivp_thms = 
+    if get_STEPS lthy > 12
+    then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy_tmp''
+    else raise TEST lthy4
+
   (* proving alpha implies alpha_bn *)
   val _ = warning "Proving alpha implies bn"
 
   val alpha_bn_imp_thms = 
-    if get_STEPS lthy > 12
+    if get_STEPS lthy > 13
     then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy_tmp'' 
     else raise TEST lthy4
-
-
+  
   val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms))
   val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms))
   val _ = tracing ("alpha_refl\n" ^ 
     cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms))
   val _ = tracing ("alpha_bn_imp\n" ^ 
     cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms))
+  val _ = tracing ("alpha_equivp\n" ^ 
+    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_equivp_thms))
 
   (* old stuff *)
   val _ = 
-    if get_STEPS lthy > 13
-    then true else raise TEST lthy4
-
-  val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
-  val bns = raw_bn_funs ~~ bn_nos;
-
-  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
-
-  val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4;
- 
-  val _ = tracing ("reflps\n" ^ 
-    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) reflps))
-  
-  val _ = 
-    if get_STEPS lthy > 13
+    if get_STEPS lthy > 14
     then true else raise TEST lthy4
 
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy4) alpha_trms
-    else build_equivps alpha_trms reflps alpha_induct
+    else build_equivps alpha_trms alpha_refl_thms alpha_induct
       inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4;
 
   val qty_binds = map (fn (_, b, _, _) => b) dts;
@@ -488,6 +480,10 @@
           Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
   val _ = warning "Proving respects";
+
+  val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
+  val bns = raw_bn_funs ~~ bn_nos;
+
   val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
@@ -496,6 +492,9 @@
 
   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
     else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1;
+
+  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
+
   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9;
   val (fv_rsp_pre, lthy10) = fold_map
     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
@@ -510,7 +509,7 @@
     alpha_bn_rsp_tac) alpha_bn_trms lthy11
   fun const_rsp_tac _ =
     let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a
-      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
+      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11a
     val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)

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