--- a/Nominal/Ex/SingleLet.thy	Mon Jun 07 11:46:26 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Wed Jun 09 15:14:16 2010 +0200
@@ -2,9 +2,10 @@
 imports "../NewParser"
 begin
 
+
 atom_decl name
 
-declare [[STEPS = 10]]
+declare [[STEPS = 11]]
 
 nominal_datatype trm =
   Var "name"
@@ -20,146 +21,7 @@
 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
 thm trm_assg.eq_iff