--- a/Nominal/nominal_dt_alpha.ML	Mon Jun 07 11:46:26 2010 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Wed Jun 09 15:14:16 2010 +0200
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk
     Author:     Christian Urban
 
-  Definitions of the alpha relations.
+  Definitions and proofs for the alpha-relations.
 *)
 
 signature NOMINAL_DT_ALPHA =
@@ -398,20 +398,56 @@
 end
 
 
+
 (** transitivity proof for alphas **)
 
+fun ecases_tac cases = 
+  Subgoal.FOCUS (fn {prems, ...} =>
+    HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
+
+fun aatac pred_names = 
+  SUBPROOF (fn {prems, context, ...} =>
+    HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
+  
+val perm_inst_tac =
+  Subgoal.FOCUS (fn {params, ...} => 
+    let
+      val (p, q) = pairself snd (last2 params)
+      val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q]
+      val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
+    in
+      HEADGOAL (rtac exi_inst)
+    end)
+
+fun non_trivial_cases_tac pred_names intros ctxt = 
+let
+  val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
+in
+  resolve_tac intros
+  THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' 
+    TRY o EVERY' 
+      [ etac @{thm exE},
+        etac @{thm exE},
+        perm_inst_tac ctxt, 
+        resolve_tac @{thms alpha_trans_eqvt}, 
+        atac,
+        aatac pred_names ctxt, 
+        Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
+        asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
+end
+			  
 fun prove_trans_tac pred_names raw_dt_thms intros induct cases ctxt =
 let
-  val _ = ("induct\n" ^ Syntax.string_of_term ctxt (prop_of induct))
-
-  val tac1 = asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms)
-  fun tac i = (EVERY' [rtac @{thm allI}, rtac @{thm impI}, rotate_tac ~1, 
-    etac (nth cases i) THEN_ALL_NEW tac1]) i
+  fun all_cases ctxt = 
+    asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) 
+    THEN' TRY o non_trivial_cases_tac pred_names intros ctxt
 in
-  HEADGOAL (rtac induct THEN_ALL_NEW tac)
+  HEADGOAL (rtac induct THEN_ALL_NEW  
+    EVERY' [ rtac @{thm allI}, rtac @{thm impI}, 
+             ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ])
 end
 
-fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
+xfun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
 let
   val lhs = alpha_trm $ arg1 $ arg2
   val mid = alpha_trm $ arg2 $ (Bound 0)
@@ -422,6 +458,8 @@
       HOLogic.mk_imp (mid, rhs)))
 end
 
+val norm = @{lemma "A --> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp}
+
 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt =
 let
   val alpha_names =  map (fst o dest_Const) alpha_trms
@@ -443,6 +481,7 @@
        prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_induct alpha_cases context)
     |> singleton (ProofContext.export ctxt' ctxt)
     |> Datatype_Aux.split_conj_thm 
+    |> map (fn th => zero_var_indexes (th RS norm))
 end
 
 end (* structure *)