--- a/Nominal/Ex/CoreHaskell.thy	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy	Mon Jun 07 11:43:01 2010 +0200
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 9]]
+declare [[STEPS = 10]]
 
 nominal_datatype tkind =
   KStar
@@ -85,7 +85,105 @@
 | "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