diff -r 1dedc0b76f32 -r d1999540d23a Nominal/Terms.thy
--- a/Nominal/Terms.thy	Thu Feb 25 12:15:11 2010 +0100
+++ b/Nominal/Terms.thy	Thu Feb 25 12:30:50 2010 +0100
@@ -46,43 +46,6 @@
 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)) *}
 thm alpha1_inj
 
-lemma alpha_bp_refl: "alpha_bp a a"
-apply induct
-apply (simp_all  add: alpha1_inj)
-done
-
-lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"
-apply rule
-apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2))
-apply (simp_all add: alpha_bp_refl)
-done
-
-lemma alpha_bp_eq: "alpha_bp = (op =)"
-apply (rule ext)+
-apply (rule alpha_bp_eq_eq)
-done
-
-ML {*
-fun build_eqvts bind funs perms simps induct ctxt =
-let
-  val pi = Free ("p", @{typ perm});
-  val types = map (domain_type o fastype_of) funs;
-  val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types));
-  val args = map Free (indnames ~~ types);
-  val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
-  fun eqvtc (fnctn, (arg, perm)) =
-    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
-  fun tac _ = (indtac induct indnames THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps 
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1
-  val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac
-  val thms = HOLogic.conj_elims thm
-in
-  Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt
-end
-*}
-
 local_setup {*
 snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)})
 *}
@@ -91,32 +54,6 @@
 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}
 *}
 
-ML {*
-fun build_alpha_eqvts funs perms simps induct ctxt =
-let
-  val pi = Free ("p", @{typ perm});
-  val types = map (domain_type o fastype_of) funs;
-  val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types));
-  val indnames2 = Name.variant_list ("pi" :: indnames) (Datatype_Prop.make_tnames (map body_type types));
-  val args = map Free (indnames ~~ types);
-  val args2 = map Free (indnames2 ~~ types);
-  fun eqvtc ((alpha, perm), (arg, arg2)) =
-    HOLogic.mk_imp (alpha $ arg $ arg2,
-      (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
-  fun tac _ = (rtac induct THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps 
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-    THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
-      (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps 
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
-) 1
-  val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
-in
-  map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
-end
-*}
 
 local_setup {*
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),
@@ -222,6 +159,17 @@
 apply auto
 done
 
+lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"
+apply rule
+apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2))
+apply (simp_all add: equivp_reflp[OF alpha1_equivp(2)])
+done
+
+lemma alpha_bp_eq: "alpha_bp = (op =)"
+apply (rule ext)+
+apply (rule alpha_bp_eq_eq)
+done
+
 lemma supp_fv:
   "supp t = fv_trm1 t"
   "supp b = fv_bp b"
@@ -670,9 +618,18 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *}
 thm alpha6_inj
 
-lemma alpha6_eqvt:
-  "xa \<approx>6 y \<Longrightarrow> (x \<bullet> xa) \<approx>6 (x \<bullet> y)"
-sorry
+local_setup {*
+snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct})
+*}
+
+local_setup {*
+snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}
+*}
+
+local_setup {*
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []),
+  build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt))
+*}
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []),
   (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *}