--- a/Quot/Nominal/Fv.thy	Mon Feb 22 16:44:58 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 17:19:28 2010 +0100
@@ -288,7 +288,7 @@
 
 ML {*
 fun symp_tac induct inj eqvt =
-  rtac induct THEN_ALL_NEW
+  ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
   TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
   (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt)
@@ -296,7 +296,7 @@
 
 ML {*
 fun transp_tac induct alpha_inj term_inj distinct cases eqvt =
-  rtac induct THEN_ALL_NEW
+  ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
   (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN'
   eresolve_tac cases) THEN_ALL_NEW
   (
@@ -306,6 +306,21 @@
   )
 *}
 
+lemma transp_aux:
+  "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
+  unfolding transp_def
+  by blast
+
+ML {*
+fun equivp_tac reflps symps transps =
+  simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'
+  resolve_tac reflps THEN'
+  rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
+  resolve_tac symps THEN'
+  rtac @{thm transp_aux} THEN' resolve_tac transps
+*}
+
 ML {*
 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
 let
@@ -318,12 +333,19 @@
   val symt = Goal.prove ctxt' [] [] symg symp_tac';
   val transt = Goal.prove ctxt' [] [] transg transp_tac';
   val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt]
+  val reflts = HOLogic.conj_elims refltg
+  val symts = HOLogic.conj_elims symtg
+  val transts = HOLogic.conj_elims transtg
   fun equivp alpha =
     let
-      val goal = @{term Trueprop} $ (@{term equivp} $ alpha)
-      val tac = 
+      val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
+      val goal = @{term Trueprop} $ (equivp $ alpha)
+      fun tac _ = equivp_tac reflts symts transts 1
+    in
+      Goal.prove ctxt [] [] goal tac
+    end
 in
-  (refltg, symtg, transtg)
+  map equivp alphas
 end
 *}
 

--- a/Quot/Nominal/Terms.thy	Mon Feb 22 16:44:58 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 17:19:28 2010 +0100
@@ -116,12 +116,11 @@
   apply(simp add: permute_eqvt[symmetric])
   done
 
-ML {*
-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} @{context}
-*}
-ML Variable.export
+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)) *}
+thm alpha1_equivp
 
-prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+(*prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})
 
 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
@@ -130,11 +129,6 @@
 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
 by (tactic {* transp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})
 
-lemma transp_aux:
-  "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
-  unfolding transp_def
-  by blast
-
 lemma alpha1_equivp:
   "equivp alpha_rtrm1"
   "equivp alpha_bp"
@@ -147,7 +141,7 @@
   THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})
 )
 1 *})
-done
+done*)
 
 quotient_type trm1 = rtrm1 / alpha_rtrm1
   by (rule alpha1_equivp(1))
@@ -345,17 +339,21 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *}
 thm alpha2_inj
 
+lemma alpha2_eqvt:
+  "t \<approx>2 s \<Longrightarrow> (pi \<bullet> t) \<approx>2 (pi \<bullet> s)"
+  "a \<approx>2b b \<Longrightarrow> (pi \<bullet> a) \<approx>2b (pi \<bullet> b)"
+sorry
 
-lemma alpha2_equivp:
-  "equivp alpha_rtrm2"
-  "equivp alpha_rassign"
-  sorry
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []),
+  (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *}
+thm alpha2_equivp
+
 
 quotient_type
   trm2 = rtrm2 / alpha_rtrm2
 and
   assign = rassign / alpha_rassign
-  by (auto intro: alpha2_equivp)
+  by (rule alpha2_equivp(1)) (rule alpha2_equivp(2))
 
 local_setup {*
 (fn ctxt => ctxt
@@ -400,16 +398,23 @@
   alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)
 thm alpha_rtrm3_alpha_rassigns.intros
 
-lemma alpha3_equivp:
-  "equivp alpha_rtrm3"
-  "equivp alpha_rassigns"
-  sorry
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *}
+thm alpha3_inj
+
+lemma alpha3_eqvt:
+  "t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)"
+  "a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)"
+sorry
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []),
+  (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *}
+thm alpha3_equivp
 
 quotient_type
   trm3 = rtrm3 / alpha_rtrm3
 and
   assigns = rassigns / alpha_rassigns
-  by (auto intro: alpha3_equivp)
+  by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))
 
 
 section {*** lam with indirect list recursion ***}
@@ -418,6 +423,7 @@
   rVr4 "name"
 | rAp4 "rtrm4" "rtrm4 list"
 | rLm4 "name" "rtrm4"  --"bind (name) in (trm)"
+print_theorems
 
 thm rtrm4.recs
 
@@ -445,6 +451,17 @@
   alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
 thm alpha_rtrm4_alpha_rtrm4_list.intros
 
+(*local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} *)
+
+lemma alpha4_eqvt:
+  "t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)"
+  "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)"
+sorry
+
+(*local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
+  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rassigns}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject rassigns.inject} @{thms alpha4_inj} @{thms rtrm4.distinct rassigns.distinct} @{thms alpha_rtrm4.cases alpha_rassigns.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}*)
+
+
 lemma alpha4_equivp: "equivp alpha_rtrm4" sorry
 lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry
 
@@ -530,36 +547,15 @@
   apply (simp)
   done
 
-prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *}
-by (tactic {* reflp_tac @{thm rtrm5_rlts.induct} @{thms alpha5_inj} 1 *})
-
-prove alpha5_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *}
-by (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} 1 *})
-
-prove alpha5_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *}
-by (tactic {* transp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms rtrm5.inject rlts.inject} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} 1 *})
-
-lemma alpha5_equivps:
-  shows "equivp alpha_rtrm5"
-  and   "equivp alpha_rlts"
-ML_prf Goal.prove
-unfolding equivp_reflp_symp_transp reflp_def
-apply (simp_all add: alpha5_reflp_aux)
-unfolding symp_def
-apply (simp_all add: alpha5_symp_aux)
-unfolding transp_def
-apply (simp_all only: helper)
-apply (rule allI)+
-apply (rule conjunct1[OF alpha5_transp_aux])
-apply (rule allI)+
-apply (rule conjunct2[OF alpha5_transp_aux])
-done
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),
+  (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *}
+thm alpha5_equivp
 
 quotient_type
   trm5 = rtrm5 / alpha_rtrm5
 and
   lts = rlts / alpha_rlts
-  by (auto intro: alpha5_equivps)
+  by (auto intro: alpha5_equivp)
 
 local_setup {*
 (fn ctxt => ctxt
@@ -730,13 +726,17 @@
 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_equivps:
-  shows "equivp alpha6"
+lemma alpha6_eqvt:
+  "xa \<approx>6 y \<Longrightarrow> (x \<bullet> xa) \<approx>6 (x \<bullet> y)"
 sorry
 
+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)) *}
+thm alpha6_equivp
+
 quotient_type
   trm6 = rtrm6 / alpha_rtrm6
-  by (auto intro: alpha6_equivps)
+  by (auto intro: alpha6_equivp)
 
 local_setup {*
 (fn ctxt => ctxt
@@ -750,8 +750,7 @@
 
 lemma [quot_respect]:
   "(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute"
-apply auto (* will work with eqvt *)
-sorry
+by (auto simp add: alpha6_eqvt)
 
 (* Definitely not true , see lemma below *)
 lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6"