--- a/Nominal/nominal_dt_alpha.ML	Thu Jun 10 14:53:45 2010 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Fri Jun 11 03:02:42 2010 +0200
@@ -16,6 +16,7 @@
 
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list
 
+  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
 end
@@ -246,6 +247,7 @@
 end
 
 
+
 (** produces the distinctness theorems **)
 
 (* transforms the distinctness theorems of the constructors 
@@ -289,9 +291,9 @@
 end
 
 
+
 (** produces the alpha_eq_iff simplification rules **)
 
-
 (* in case a theorem is of the form (C.. = C..), it will be
    rewritten to ((C.. = C..) = True) *)
 fun mk_simp_rule thm =
@@ -329,6 +331,56 @@
 
 
 
+(** reflexivity proof for the alphas **)
+
+val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}
+
+fun cases_tac intros =
+let
+  val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
+
+  val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac  
+
+  val bound_tac = 
+    EVERY' [ rtac exi_zero, 
+             resolve_tac @{thms alpha_gen_refl}, 
+             asm_full_simp_tac (HOL_ss addsimps prod_simps) ]
+in
+  REPEAT o FIRST' [rtac @{thm conjI}, 
+    resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]]
+end
+
+fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt =
+let
+  val arg_tys = 
+    alpha_trms
+    |> map fastype_of
+    |> map domain_type
+  val arg_bn_tys = 
+    alpha_bns
+    |> map fastype_of
+    |> map domain_type
+  val arg_names = Datatype_Prop.make_tnames arg_tys
+  val arg_bn_names = map (fn ty => the (AList.lookup (op=) (arg_tys ~~ arg_names) ty)) arg_bn_tys
+  val args = map Free (arg_names ~~ arg_tys)
+  val arg_bns = map Free (arg_bn_names ~~ arg_bn_tys)
+  val goal = 
+    AList.group (op=) ((arg_bns ~~ alpha_bns) @ (args ~~ alpha_trms))
+    |> map (fn (ar, cnsts) => map (fn c => c $ ar $ ar) cnsts) 
+    |> map (foldr1 HOLogic.mk_conj)
+    |> foldr1 HOLogic.mk_conj
+    |> HOLogic.mk_Trueprop
+in
+  Goal.prove ctxt arg_names [] goal
+    (fn {context, ...} => 
+       HEADGOAL (DETERM o (rtac raw_dt_induct) THEN_ALL_NEW cases_tac alpha_intros)) 
+  |> Datatype_Aux.split_conj_thm 
+  |> map Datatype_Aux.split_conj_thm 
+  |> flat
+end
+
+
+
 (** symmetry proof for the alphas **)
 
 val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p"