--- a/Nominal/nominal_dt_alpha.ML	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Wed May 26 15:34:54 2010 +0200
@@ -10,11 +10,18 @@
   val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
     bclause list list list -> term list -> Proof.context -> 
     term list * term list * thm list * thm list * thm * local_theory
+
+  val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> 
+    term list -> term list -> bn_info -> thm list * thm list
+
+  val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
 struct
 
+(** definition of the inductive rules for alpha and alpha_bn **)
+
 (* construct the compound terms for prod_fv and prod_alpha *)
 fun mk_prod_fv (t1, t2) =
 let
@@ -216,7 +223,7 @@
   
   val (alphas, lthy') = Inductive.add_inductive_i
      {quiet_mode = true, verbose = false, alt_name = Binding.empty,
-      coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
+      coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
      all_alpha_names [] all_alpha_intros [] lthy
 
   val all_alpha_trms_loc = #preds alphas;
@@ -235,5 +242,86 @@
   (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
 end
 
+
+(** produces the distinctness theorems **)
+
+(* transforms the distinctness theorems of the constructors 
+   to "not-alphas" of the constructors *)
+fun mk_alpha_distinct_goal alpha neq =
+let
+  val (lhs, rhs) = 
+    neq
+    |> HOLogic.dest_Trueprop
+    |> HOLogic.dest_not
+    |> HOLogic.dest_eq
+in
+  alpha $ lhs $ rhs
+  |> HOLogic.mk_not
+  |> HOLogic.mk_Trueprop
+end
+
+fun distinct_tac cases distinct_thms =
+  rtac notI THEN' eresolve_tac cases 
+  THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
+
+fun mk_alpha_distinct ctxt cases_thms (distinct_thm, alpha) =
+let
+  val ((_, thms), ctxt') = Variable.import false distinct_thm ctxt
+  val goals = map (mk_alpha_distinct_goal alpha o prop_of) thms
+  val nrels = map (fn t => Goal.prove ctxt' [] [] t (K (distinct_tac cases_thms distinct_thm 1))) goals
+in
+  Variable.export ctxt' ctxt nrels
+end
+
+fun mk_alpha_distincts ctxt alpha_cases constrs_distinct_thms alpha_trms alpha_bn_trms bn_infos =
+let
+  val alpha_distincts = 
+    map (mk_alpha_distinct ctxt alpha_cases) (constrs_distinct_thms ~~ alpha_trms)
+  val distinc_thms = map 
+  val alpha_bn_distincts_aux = map (fn (_, i, _) => nth constrs_distinct_thms i) bn_infos
+  val alpha_bn_distincts =  
+    map (mk_alpha_distinct ctxt alpha_cases) (alpha_bn_distincts_aux ~~ alpha_bn_trms)
+in
+  (flat alpha_distincts, flat alpha_bn_distincts)
+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 =
+  case (prop_of thm) of
+    @{term "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) => @{thm eqTrueI} OF [thm]
+  | _ => thm
+
+fun alpha_eq_iff_tac dist_inj intros elims =
+  SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE'
+  (rtac @{thm iffI} THEN' 
+    RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj),
+           asm_full_simp_tac (HOL_ss addsimps intros)])
+
+fun mk_alpha_eq_iff_goal thm =
+  let
+    val prop = prop_of thm;
+    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
+    val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
+    fun list_conj l = foldr1 HOLogic.mk_conj l;
+  in
+    if hyps = [] then HOLogic.mk_Trueprop concl
+    else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
+  end;
+
+fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims =
+let
+  val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
+  val goals = map mk_alpha_eq_iff_goal thms_imp;
+  val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1;
+  val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
+in
+  Variable.export ctxt' ctxt thms
+  |> map mk_simp_rule
+end
+
 end (* structure *)