--- a/Nominal/nominal_dt_alpha.ML	Sat Sep 18 06:09:43 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Mon Sep 20 21:52:45 2010 +0800
@@ -16,6 +16,9 @@
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
     thm list -> thm list
 
+  val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> 
+    (Proof.context -> int -> tactic) -> Proof.context -> thm list
+  
   val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> 
     (Proof.context -> int -> tactic) -> Proof.context -> thm list
 
@@ -351,10 +354,44 @@
   end
 
 
-(** proof by induction over the alpha-definitions **)
+(** proof by induction over types **)
+
+fun induct_prove tys props induct_thm cases_tac ctxt =
+  let
+    val (arg_names, ctxt') =
+      Variable.variant_fixes (replicate (length tys) "x") ctxt
+
+    val args = map2 (curry Free) arg_names tys
 
-fun is_true @{term "Trueprop True"} = true
-  | is_true _ = false 
+    val true_trms = replicate (length tys) (K @{term True})
+  
+    fun apply_all x fs = map (fn f => f x) fs
+    
+    val goals = 
+        group (props @ (tys ~~ true_trms))
+        |> map snd 
+        |> map2 apply_all args
+        |> map fold_conj
+        |> foldr1 HOLogic.mk_conj
+        |> HOLogic.mk_Trueprop
+
+    fun tac ctxt =
+      HEADGOAL 
+        (DETERM o (rtac induct_thm) 
+         THEN_ALL_NEW 
+           (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))
+  in
+    Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
+    |> singleton (ProofContext.export ctxt' ctxt)
+    |> Datatype_Aux.split_conj_thm
+    |> map Datatype_Aux.split_conj_thm
+    |> flat
+    |> filter_out (is_true o concl_of)
+    |> map zero_var_indexes
+  end
+
+
+(** proof by induction over the alpha-definitions **)
 
 fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
   let
@@ -397,8 +434,8 @@
     |> map (fn th => th RS mp) 
     |> map Datatype_Aux.split_conj_thm
     |> flat
+    |> filter_out (is_true o concl_of)
     |> map zero_var_indexes
-    |> filter_out (is_true o concl_of)
   end
 
 
@@ -406,7 +443,7 @@
 
 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}
 
-fun cases_tac intros =
+fun cases_tac intros ctxt =
   let
     val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
 
@@ -417,8 +454,7 @@
                resolve_tac @{thms alpha_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]]
+    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 =
@@ -427,27 +463,17 @@
       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 (lookup (arg_tys ~~ arg_names)) arg_bn_tys
-    val args = map Free (arg_names ~~ arg_tys)
-    val arg_bns = map Free (arg_bn_names ~~ arg_bn_tys)
-    val goal = 
-      group ((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
+    
+    val props = 
+      map (fn (ty, c) => (ty, fn x => c $ x $ x)) 
+        ((arg_tys ~~ alpha_trms) @ (arg_bn_tys ~~ alpha_bns))
   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
+    induct_prove arg_tys props raw_dt_induct (cases_tac alpha_intros) ctxt 
   end