# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266858584 -3600
# Node ID 06ace3a1eedd9658b76cb9ee23b4a3705597503e
# Parent  aec9576b39505da5c81ddea73931ac494e2edede
Fixed pseudo_injectivity for trm4

diff -r aec9576b3950 -r 06ace3a1eedd Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Mon Feb 22 17:19:28 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 18:09:44 2010 +0100
@@ -220,11 +220,11 @@
 ML {*
 fun alpha_inj_tac dist_inj intrs elims =
   SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
-  rtac @{thm iffI} THEN' RANGE [
+  (rtac @{thm iffI} THEN' RANGE [
      (eresolve_tac elims THEN_ALL_NEW
        asm_full_simp_tac (HOL_ss addsimps dist_inj)
      ),
-     (asm_full_simp_tac (HOL_ss addsimps intrs))]
+     asm_full_simp_tac (HOL_ss addsimps intrs)])
 *}
 
 ML {*
diff -r aec9576b3950 -r 06ace3a1eedd Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Mon Feb 22 17:19:28 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 18:09:44 2010 +0100
@@ -451,15 +451,23 @@
   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)) *} *)
+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 list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
+thm alpha4_inj
 
 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)) *}*)
+(*
+prove alpha4_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] ("x","y","z")) *}
+apply (tactic {* 
+transp_tac @{thm rtrm4.induct} @{thms alpha4_inj} @{thms rtrm4.inject list.inject} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha1_eqvt} 1 *})
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
+  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases list.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
+*)
+
+
 
 
 lemma alpha4_equivp: "equivp alpha_rtrm4" sorry