--- a/Nominal/Ex/SingleLet.thy	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Mon Jun 07 11:43:01 2010 +0200
@@ -4,15 +4,14 @@
 
 atom_decl name
 
-declare [[STEPS = 9]]
-
+declare [[STEPS = 10]]
 
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind_set x in t
 | Let a::"assg" t::"trm"  bind_set "bn a" in t
-| Foo x::"name" y::"name" t::"trm" bind_set x in y t
+| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
 and assg =
   As "name" "name" "trm" "name"
@@ -21,6 +20,145 @@
 where
   "bn (As x y t z) = {atom x}"
 
+thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros
+thm alpha_trm_raw.cases alpha_assg_raw.cases alpha_bn_raw.cases
+
+
+lemma [eqvt]:
+ "p \<bullet> alpha_trm_raw x1 y1  = alpha_trm_raw (p \<bullet> x1) (p \<bullet> y1)"
+ "p \<bullet> alpha_assg_raw x2 y2 = alpha_assg_raw (p \<bullet> x2) (p \<bullet> y2)"
+ "p \<bullet> alpha_bn_raw x3 y3   = alpha_bn_raw (p \<bullet> x3) (p \<bullet> y3)"
+sorry
+
+lemmas ii = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros
+lemmas cc = alpha_trm_raw.cases alpha_assg_raw.cases alpha_bn_raw.cases
+
+ML {*
+length @{thms cc}
+*}
+
+ML {*
+  val pp = ["SingleLet.alpha_trm_raw", "SingleLet.alpha_assg_raw", "SingleLet.alpha_bn_raw"]
+*}
+
+lemma exi_sum: "\<exists>(q :: perm). P q \<Longrightarrow> \<exists>q. Q q \<Longrightarrow> (\<And>p q. P p \<Longrightarrow> Q q \<Longrightarrow> R (p + q)) \<Longrightarrow> \<exists>r. R r"
+apply(erule exE)+
+apply(rule_tac x="q + qa" in exI)
+apply(simp)
+done
+
+lemma alpha_gen_compose_trans:
+  assumes b: "(as, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (bs, s)"
+  shows "(\<forall>x. R s x \<longrightarrow> R (pi \<bullet> t) x)"
+  using b
+  by (simp add: alphas)
+
+lemma test:
+  assumes b: "(as, t) \<approx>gen R f pi (bs, s)"
+  shows "R (pi \<bullet> t) s"
+  using b
+  by (simp add: alphas)
+
+lemma alpha_gen_trans_eqvt:
+  assumes a: "(bs, x) \<approx>gen R f p (cs, y)" and a1: "(cs, y) \<approx>gen R f q (ds, z)"
+  and b: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+  shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
+  sorry
+
+
+lemma
+ "alpha_trm_raw x1 y1  \<Longrightarrow> (\<And>z1. alpha_trm_raw y1 z1 \<Longrightarrow> alpha_trm_raw x1 z1)"
+ "alpha_assg_raw x2 y2 \<Longrightarrow> (\<And>z2. alpha_assg_raw y2 z2 \<Longrightarrow> alpha_assg_raw x2 z2)"
+ "alpha_bn_raw x3 y3   \<Longrightarrow> (\<And>z3. alpha_bn_raw y3 z3 \<Longrightarrow> alpha_bn_raw x3 z3)"
+apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
+(* 8 *)
+prefer 8
+thm alpha_bn_raw.cases
+apply(rotate_tac -1)
+apply(erule alpha_bn_raw.cases)
+apply(simp_all)[6]
+
+
+apply(rotate_tac -1)
+apply(erule cc)
+apply(simp_all)[6]
+apply(rule ii) 
+apply(simp)
+(* 1 *)
+apply(rotate_tac -1)
+apply(erule cc)
+apply(simp_all)[6]
+apply(rule ii) 
+apply(simp)
+apply(simp)
+(* 2 *)
+apply(rotate_tac -1)
+apply(erule cc)
+apply(simp_all)[6]
+apply(rule ii)
+apply(erule exE)+
+apply(rule_tac x="pa + p" in exI)
+apply(rule alpha_gen_trans_eqvt)
+prefer 2
+apply(assumption)
+apply(simp add: alphas)
+apply(metis)
+apply(drule test)
+apply(simp)
+(* 3 *)
+apply(rotate_tac -1)
+apply(erule cc)
+apply(simp_all)[6]
+apply(rule ii)
+apply(erule exE)+
+apply(rule_tac x="pa + p" in exI)
+apply(rule alpha_gen_trans_eqvt)
+prefer 2
+apply(assumption)
+apply(simp add: alphas)
+apply(metis)
+apply(drule alpha_gen_compose_trans)
+apply(simp)
+apply(simp)
+(* 4 *)
+apply(rotate_tac -1)
+apply(erule cc)
+apply(simp_all)[6]
+apply(rule ii)
+apply(erule exE)+
+apply(rule_tac x="pa + p" in exI)
+apply(rule alpha_gen_trans_eqvt)
+prefer 2
+apply(assumption)
+prefer 2
+apply(drule test)
+apply(simp add: prod_alpha_def)
+apply(simp add: alphas)
+
+apply(drule alpha_gen_compose_trans)
+apply(drule_tac x="(- pa \<bullet> trm_rawaa)" in spec)
+apply(simp)
+apply(simp)
+(* 4 *)
+apply(assumption) 
+apply(simp)
+apply(simp)
+
+(* 3 *)
+
+(* 4 *)
+
+(* 5 *)
+
+(* 6 *)
+
+(* 7 *)
+
+(* 8 *)
+
+(* 9 *)
+done
+
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv
 thm trm_assg.supp