--- a/Nominal/nominal_dt_alpha.ML	Mon Jun 21 15:41:59 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Tue Jun 22 13:05:00 2010 +0100
@@ -19,11 +19,15 @@
   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_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
 struct
 
+fun lookup xs x = the (AList.lookup (op=) xs x)
+fun group xs = AList.group (op=) xs
+
 (** definition of the inductive rules for alpha and alpha_bn **)
 
 (* construct the compound terms for prod_fv and prod_alpha *)
@@ -89,7 +93,7 @@
     (NONE, _) => []
   | (SOME bn, i) =>
      if member (op=) bodies i then [] 
-     else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)]
+     else [lookup alpha_bn_map bn $ nth args i $ nth args' i]
 
 (* generat the premises for an alpha rule; mk_frees is used
    if no binders are present *)
@@ -102,7 +106,7 @@
       val ty = fastype_of arg
     in
       if nth is_rec i
-      then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg'
+      then fst (lookup alpha_map ty) $ arg $ arg'
       else HOLogic.mk_eq (arg, arg')
     end
 
@@ -141,7 +145,7 @@
   val arg_names' = Name.variant_list arg_names arg_names
   val args = map Free (arg_names ~~ arg_tys)
   val args' = map Free (arg_names' ~~ arg_tys)
-  val alpha = fst (the (AList.lookup (op=) alpha_map ty))
+  val alpha = fst (lookup alpha_map ty)
   val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))
   val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses
 in
@@ -169,7 +173,7 @@
                  NONE =>  [HOLogic.mk_eq (arg, arg')]
                | SOME (alpha, _) => [alpha $ arg $ arg'])
     | SOME (NONE) => []
-    | SOME (SOME bn) => [the (AList.lookup (op=) alpha_bn_map bn) $ arg $ arg']
+    | SOME (SOME bn) => [lookup alpha_bn_map bn $ arg $ arg']
   end  
 in
   case bclause of
@@ -185,7 +189,7 @@
   val arg_names' = Name.variant_list arg_names arg_names
   val args = map Free (arg_names ~~ arg_tys)
   val args' = map Free (arg_names' ~~ arg_tys)
-  val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm)
+  val alpha_bn = lookup alpha_bn_map bn_trm
   val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))
   val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses
 in
@@ -361,11 +365,11 @@
     |> 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 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 = 
-    AList.group (op=) ((arg_bns ~~ alpha_bns) @ (args ~~ alpha_trms))
+    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
@@ -538,5 +542,77 @@
     |> map (fn th => zero_var_indexes (th RS norm))
 end
 
+
+(* proves that alpha_raw implies alpha_bn *)
+
+fun is_true @{term "Trueprop True"} = true
+  | is_true _ = false 
+
+fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = 
+  Subgoal.FOCUS (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 ])
+    end) ctxt
+
+fun raw_prove_bn_imp alpha_trms alpha_bns alpha_intros alpha_induct ctxt =
+let
+  val alpha_names =  map (fst o dest_Const) alpha_trms
+
+  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_names1, (arg_names2, ctxt')) =
+    ctxt
+    |> Variable.variant_fixes (replicate (length arg_tys) "x") 
+    ||> Variable.variant_fixes (replicate (length arg_tys) "y")
+  val arg_bn_names1 = map (lookup (arg_tys ~~ arg_names1)) arg_bn_tys
+  val arg_bn_names2 = map (lookup (arg_tys ~~ arg_names2)) arg_bn_tys
+  val args1 = map Free (arg_names1 ~~ arg_tys)
+  val args2 = map Free (arg_names2 ~~ arg_tys)
+  val arg_bns1 = map Free (arg_bn_names1 ~~ arg_bn_tys)
+  val arg_bns2 = map Free (arg_bn_names2 ~~ arg_bn_tys)
+
+  val alpha_bn_trms = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_bns (arg_bns1 ~~ arg_bns2)
+  val true_trms = map (K @{term True}) arg_tys
+
+  val goal_rhs = 
+    group ((arg_bn_tys ~~ alpha_bn_trms) @ (arg_tys ~~ true_trms))
+    |> map snd 
+    |> map (foldr1 HOLogic.mk_conj)
+
+  val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_trms (args1 ~~ args2)
+  val goal_rest = map (fn t => HOLogic.mk_imp (t, @{term "True"})) alpha_bn_trms  
+
+  val goal =
+    (map2 (curry HOLogic.mk_imp) goal_lhs goal_rhs) @ goal_rest
+    |> foldr1 HOLogic.mk_conj
+    |> HOLogic.mk_Trueprop
+in
+  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)) 
+  |> singleton (ProofContext.export ctxt' ctxt)
+  |> Datatype_Aux.split_conj_thm 
+  |> map (fn th => zero_var_indexes (th RS mp))
+  |> map Datatype_Aux.split_conj_thm 
+  |> flat
+  |> filter_out (is_true o concl_of)
+end
+
+
 end (* structure *)