--- a/Nominal/nominal_dt_alpha.ML	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Mon Jun 07 11:43:01 2010 +0200
@@ -15,6 +15,9 @@
     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
+
+  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
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -288,6 +291,7 @@
 
 (** 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 =
@@ -323,5 +327,123 @@
   |> map mk_simp_rule
 end
 
+
+
+(** symmetry proof for the alphas **)
+
+val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p"
+  by (erule exE, rule_tac x="-p" in exI, auto)}
+
+(* for premises that contain binders *)
+fun prem_bound_tac pred_names ctxt = 
+let
+  fun trans_prem_tac pred_names ctxt = 
+    SUBPROOF (fn {prems, context, ...} => 
+    let
+      val prems' = map (transform_prem1 context pred_names) prems
+    in
+      resolve_tac prems' 1
+    end) ctxt
+  val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas}
+in
+  EVERY' 
+    [ etac exi_neg,
+      resolve_tac @{thms alpha_gen_sym_eqvt},
+      asm_full_simp_tac (HOL_ss addsimps prod_simps),
+      Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
+      trans_prem_tac pred_names ctxt ] 
+end
+
+fun prove_sym_tac pred_names intros induct ctxt =
+let
+  val prem_eq_tac = rtac @{thm sym} THEN' atac   
+  val prem_unbound_tac = atac
+
+  val prem_cases_tacs = FIRST' 
+    [prem_eq_tac, prem_unbound_tac, prem_bound_tac pred_names ctxt]
+in
+  HEADGOAL (rtac induct THEN_ALL_NEW 
+    (resolve_tac intros THEN_ALL_NEW prem_cases_tacs))
+end
+
+fun prep_sym_goal alpha_trm (arg1, arg2) =
+let
+  val lhs = alpha_trm $ arg1 $ arg2
+  val rhs = alpha_trm $ arg2 $ arg1
+in
+  HOLogic.mk_imp (lhs, rhs)  
+end
+
+fun raw_prove_sym alpha_trms 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_names1, (arg_names2, ctxt')) =
+    ctxt
+    |> Variable.variant_fixes (replicate (length arg_tys) "x") 
+    ||> Variable.variant_fixes (replicate (length arg_tys) "y")   
+  val args1 = map Free (arg_names1 ~~ arg_tys) 
+  val args2 = map Free (arg_names2 ~~ arg_tys)
+  val goal = HOLogic.mk_Trueprop 
+    (foldr1 HOLogic.mk_conj (map2 prep_sym_goal alpha_trms (args1 ~~ args2)))	      
+in
+  Goal.prove ctxt' [] [] goal 
+    (fn {context,...} =>  prove_sym_tac alpha_names alpha_intros alpha_induct context)
+    |> singleton (ProofContext.export ctxt' ctxt)
+    |> Datatype_Aux.split_conj_thm 
+    |> map (fn th => zero_var_indexes (th RS mp))
+end
+
+
+(** transitivity proof for alphas **)
+
+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
+in
+  HEADGOAL (rtac induct THEN_ALL_NEW tac)
+end
+
+fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
+let
+  val lhs = alpha_trm $ arg1 $ arg2
+  val mid = alpha_trm $ arg2 $ (Bound 0)
+  val rhs = alpha_trm $ arg1 $ (Bound 0) 
+in
+  HOLogic.mk_imp (lhs, 
+    HOLogic.all_const arg_ty $ Abs ("z", arg_ty, 
+      HOLogic.mk_imp (mid, rhs)))
+end
+
+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
+  val arg_tys = 
+    alpha_trms
+    |> 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 args1 = map Free (arg_names1 ~~ arg_tys) 
+  val args2 = map Free (arg_names2 ~~ arg_tys)
+  val goal = HOLogic.mk_Trueprop 
+    (foldr1 HOLogic.mk_conj (map2 prep_trans_goal alpha_trms (args1 ~~ args2 ~~ arg_tys))) 
+in
+  Goal.prove ctxt' [] [] goal 
+    (fn {context,...} =>  
+       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 
+end
+
 end (* structure *)