diff -r 40e1646ff934 -r 10eca65a8d03 Nominal/Term1.thy
--- a/Nominal/Term1.thy	Wed Mar 10 14:47:04 2010 +0100
+++ b/Nominal/Term1.thy	Wed Mar 10 15:32:51 2010 +0100
@@ -32,16 +32,16 @@
 
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1")
-  [[[], [], [(NONE, 0, 1)], [(SOME @{term bv1}, 0, 2)]],
-  [[], [], []]] *}
+  [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]],
+  [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
 
 notation
   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
   alpha_bp ("_ \<approx>1b _" [100, 100] 100)
-thm alpha_rtrm1_alpha_bp.intros
+thm alpha_rtrm1_alpha_bp_alpha_bv1.intros
 thm fv_rtrm1_fv_bp.simps[no_vars]
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp_alpha_bv1.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases alpha_bv1.cases} ctxt)) ctxt)) *}
 thm alpha1_inj
 
 local_setup {*
@@ -52,9 +52,26 @@
 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct}
 *}
 
+lemma alpha1_eqvt: "(rtrm1 \<approx>1 rtrm1a \<longrightarrow> (p \<bullet> rtrm1) \<approx>1 (p \<bullet> rtrm1a)) \<and> (bp \<approx>1b bpa \<longrightarrow> (p \<bullet> bp) \<approx>1b (p \<bullet> bpa))
+  \<and> (alpha_bv1 a b c \<longrightarrow> alpha_bv1 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))"
+apply (rule alpha_rtrm1_alpha_bp_alpha_bv1.induct)
+apply (simp_all add: fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps alpha1_inj)
+apply (erule exE)
+apply (rule_tac x="p \<bullet> pi" in exI)
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: eqvts)
+apply (erule exE)
+apply (rule_tac x="p \<bullet> pi" in exI)
+apply (rule conjI)
+apply (erule conjE)+
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: eqvts permute_eqvt[symmetric])
+apply (simp add: eqvts[symmetric])
+done
+(*
 local_setup {*
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),
-build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) *}
+build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} ctxt) ctxt)) *}*)
 
 lemma alpha1_eqvt_proper[eqvt]:
   "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"
@@ -74,7 +91,7 @@
 thm eqvts_raw(1)
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
-  (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}
+  (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}
 thm alpha1_equivp
 
 local_setup  {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]