--- a/Nominal/Ex/CoreHaskell.thy	Wed Jun 09 15:14:16 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy	Thu Jun 10 14:53:28 2010 +0200
@@ -85,105 +85,6 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
-lemma alpha_gen_sym_test:
-  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" 
-  and     b: "p \<bullet> R = R"
-  shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
-  and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
-  and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
-  unfolding alphas fresh_star_def
-  apply(auto simp add:  fresh_minus_perm)
-  apply(rule_tac p="p" in permute_boolE)
-  apply(perm_simp add: permute_minus_cancel b)
-  apply(simp add: a)
-  apply(rule_tac p="p" in permute_boolE)
-  apply(perm_simp add: permute_minus_cancel b)
-  apply(simp add: a)
-  apply(rule_tac p="p" in permute_boolE)
-  apply(perm_simp add: permute_minus_cancel b)
-  apply(simp add: a)
-  done  
-
-ML {*
-(* for equalities *)
-val tac1 = rtac @{thm sym} THEN' atac 
-
-(* for "unbound" premises *)
-val tac2 = atac
-
-fun trans_prem_tac pred_names ctxt = 
-  SUBPROOF (fn {prems, context as ctxt, ...} =>
-    let
-      val prems' = map (transform_prem1 ctxt pred_names) prems
-      val _ = tracing ("prems'\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) prems'))
-    in
-      print_tac "goal" THEN resolve_tac prems' 1
-    end) ctxt
-
-(* for "bound" premises *) 
-fun tac3 pred_names ctxt = 
-  EVERY' [etac @{thm exi_neg},
-          resolve_tac @{thms alpha_gen_sym_test},
-          asm_full_simp_tac (HOL_ss addsimps @{thms split_conv permute_prod.simps 
-                prod_alpha_def prod_rel.simps alphas}),
-          Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
-          trans_prem_tac pred_names ctxt] 
-
-fun tac intro pred_names ctxt = 
-  resolve_tac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3 pred_names ctxt]
-*}
-
-lemma [eqvt]:
-shows "p \<bullet> alpha_tkind_raw = alpha_tkind_raw" 
-and   "p \<bullet> alpha_ckind_raw = alpha_ckind_raw" 
-and   "p \<bullet> alpha_ty_raw = alpha_ty_raw" 
-and   "p \<bullet> alpha_ty_lst_raw = alpha_ty_lst_raw" 
-and   "p \<bullet> alpha_co_raw = alpha_co_raw" 
-and   "p \<bullet> alpha_co_lst_raw = alpha_co_lst_raw"
-and   "p \<bullet> alpha_trm_raw = alpha_trm_raw"
-and   "p \<bullet> alpha_assoc_lst_raw = alpha_assoc_lst_raw"
-and   "p \<bullet> alpha_pat_raw = alpha_pat_raw"
-and   "p \<bullet> alpha_vars_raw = alpha_vars_raw"
-and   "p \<bullet> alpha_tvars_raw = alpha_tvars_raw"
-and   "p \<bullet> alpha_cvars_raw = alpha_cvars_raw"
-and   "p \<bullet> alpha_bv_raw = alpha_bv_raw"
-and   "p \<bullet> alpha_bv_vs_raw = alpha_bv_vs_raw"
-and   "p \<bullet> alpha_bv_tvs_raw = alpha_bv_tvs_raw"
-and   "p \<bullet> alpha_bv_cvs_raw = alpha_bv_cvs_raw"
-sorry
-
-lemmas ii = alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts
-
-lemmas ij = alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros
-
-ML {*
-val pp = ["CoreHaskel.alpha_tkind_raw", "CoreHaskell.alpha_ckind_raw", "CoreHaskell.alpha_ty_raw", "CoreHaskell.alpha_ty_lst_raw", "CoreHaskell.alpha_co_raw", "CoreHaskell.alpha_co_lst_raw", "CoreHaskell.alpha_trm_raw", "CoreHaskell.alpha_assoc_lst_raw", "CoreHaskell.alpha_pat_raw", "CoreHaskell.alpha_vars_raw", "CoreHaskell.alpha_tvars_raw", "CoreHaskell.alpha_cvars_raw", "CoreHaskell.alpha_bv_raw", "CoreHaskell.alpha_bv_vs_raw", "CoreHaskell.alpha_bv_tvs_raw", "CoreHaskell.alpha_bv_cvs_raw"]
-*}
-
-lemma
-shows "alpha_tkind_raw x1 y1 ==> alpha_tkind_raw y1 x1" 
-and   "alpha_ckind_raw x2 y2 ==> alpha_ckind_raw y2 x2" 
-and   "alpha_ty_raw x3 y3 ==> alpha_ty_raw y3 x3" 
-and   "alpha_ty_lst_raw x4 y4 ==> alpha_ty_lst_raw y4 x4" 
-and   "alpha_co_raw x5 y5 ==> alpha_co_raw y5 x5" 
-and   "alpha_co_lst_raw x6 y6 ==> alpha_co_lst_raw y6 x6"
-and   "alpha_trm_raw x7 y7 ==> alpha_trm_raw y7 x7"
-and   "alpha_assoc_lst_raw x8 y8 ==> alpha_assoc_lst_raw y8 x8"
-and   "alpha_pat_raw x9 y9 ==> alpha_pat_raw y9 x9"
-and   "alpha_vars_raw xa ya ==> alpha_vars_raw ya xa"
-and   "alpha_tvars_raw xb yb ==> alpha_tvars_raw yb xb"
-and   "alpha_cvars_raw xc yc ==> alpha_cvars_raw yc xc"
-and   "alpha_bv_raw xd yd ==> alpha_bv_raw yd xd"
-and   "alpha_bv_vs_raw xe ye ==> alpha_bv_vs_raw ye xe"
-and   "alpha_bv_tvs_raw xf yf ==> alpha_bv_tvs_raw yf xf"
-and   "alpha_bv_cvs_raw xg yg ==> alpha_bv_cvs_raw yg xg"
-apply(induct rule: ii)
-apply(tactic {* tac @{thms ij} pp @{context} 1 *})+
-done
-
-
-lemma
-alpha_tkind_raw, alpha_ckind_raw, alpha_ty_raw, alpha_ty_lst_raw, alpha_co_raw, alpha_co_lst_raw, alpha_trm_raw, alpha_assoc_lst_raw, alpha_pat_raw, alpha_vars_raw, alpha_tvars_raw, alpha_cvars_raw, alpha_bv_raw, alpha_bv_vs_raw, alpha_bv_tvs_raw, alpha_bv_cvs_raw
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm

--- a/Nominal/NewParser.thy	Wed Jun 09 15:14:16 2010 +0200
+++ b/Nominal/NewParser.thy	Thu Jun 10 14:53:28 2010 +0200
@@ -5,6 +5,11 @@
         "Perm" "Tacs" "Equivp" "Lift"
 begin
 
+(* TODO
+
+  we need to also export a cases-rule for nominal datatypes
+  size function
+*)
 
 section{* Interface for nominal_datatype *}
 

--- a/Nominal/nominal_dt_alpha.ML	Wed Jun 09 15:14:16 2010 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Thu Jun 10 14:53:28 2010 +0200
@@ -401,6 +401,7 @@
 
 (** transitivity proof for alphas **)
 
+(* applies cases rules and resolves them with the last premise *)
 fun ecases_tac cases = 
   Subgoal.FOCUS (fn {prems, ...} =>
     HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
@@ -409,6 +410,7 @@
   SUBPROOF (fn {prems, context, ...} =>
     HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
   
+(* instantiates exI with the permutation p + q *)
 val perm_inst_tac =
   Subgoal.FOCUS (fn {params, ...} => 
     let
@@ -425,7 +427,7 @@
 in
   resolve_tac intros
   THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' 
-    TRY o EVERY' 
+    TRY o EVERY'   (* if binders are present *)
       [ etac @{thm exE},
         etac @{thm exE},
         perm_inst_tac ctxt, 
@@ -447,7 +449,7 @@
              ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ])
 end
 
-xfun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
+fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
 let
   val lhs = alpha_trm $ arg1 $ arg2
   val mid = alpha_trm $ arg2 $ (Bound 0)