# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267087274 -3600
# Node ID a6eeca90fd4e6669e23ced0223c2b7ec03760534
# Parent  2f020819ada933678438ec3b1e57bc5655a6f9da
Use eqvt infrastructure.

diff -r 2f020819ada9 -r a6eeca90fd4e Nominal/Terms.thy
--- a/Nominal/Terms.thy	Thu Feb 25 09:22:29 2010 +0100
+++ b/Nominal/Terms.thy	Thu Feb 25 09:41:14 2010 +0100
@@ -65,7 +65,7 @@
 ML {*
 fun build_eqvts funs perms simps induct ctxt =
 let
-  val pi = Free ("pi", @{typ perm});
+  val pi = Free ("p", @{typ perm});
   val types = map (domain_type o fastype_of) funs;
   val fv_indnames = Datatype_Prop.make_tnames (map body_type types);
   val args = map Free (fv_indnames ~~ types);
@@ -76,30 +76,21 @@
   fun tac _ = (indtac induct fv_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" :: fv_indnames) [] gl tac
+  val thms = HOLogic.conj_elims thm
 in
-  Goal.prove ctxt ("pi" :: fv_indnames) [] gl tac
+  Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt
 end
 *}
 
-ML {*
-build_eqvts [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)} @{context}
+local_setup {*
+snd o (build_eqvts [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)})
 *}
-lemma bv1_eqvt[eqvt]:
-  shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
-  apply (induct x)
-  apply (simp_all add: eqvts atom_eqvt)
-  done
 
-ML {*
-build_eqvts [@{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} @{context}
+local_setup {*
+snd o build_eqvts [@{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 fv_rtrm1_eqvt[eqvt]:
-    "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
-    "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
-  apply (induct t and b)
-  apply (simp_all add: eqvts atom_eqvt)
-  done
-
+thm eqvts
 lemma alpha1_eqvt:
   "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
   "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)"