# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266847428 -3600
# Node ID 10a0e3578507b32414785aa7bb1927793ddcce8a
# Parent  7b1a3df239cd2772bc851c4cf14a8148c6d5397f
Generalize atom_trans and atom_sym.

diff -r 7b1a3df239cd -r 10a0e3578507 Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Mon Feb 22 14:50:53 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Mon Feb 22 15:03:48 2010 +0100
@@ -74,11 +74,11 @@
   apply(clarsimp)
   done
 
-(* introduced for examples *)
-lemma alpha_gen_atom_sym:
-  assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi ({atom b}, s) \<Longrightarrow>
-        \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)"
+lemma alpha_gen_compose_sym:
+  assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+  shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)"
+  using b apply -
   apply(erule exE)
   apply(rule_tac x="- pi" in exI)
   apply(simp add: alpha_gen.simps)
@@ -91,11 +91,12 @@
   apply assumption
   done
 
-lemma alpha_gen_atom_trans:
-  assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi ({atom aa}, ta);
-        \<exists>pi\<Colon>perm. ({atom aa}, ta) \<approx>gen R f pi ({atom ba}, sa)\<rbrakk>
-    \<Longrightarrow> \<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen R f pi ({atom ba}, sa)"
+lemma alpha_gen_compose_trans:
+  assumes b: "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
+  and c: "\<exists>pi\<Colon>perm. (ab, ta) \<approx>gen R f pi (ac, sa)"
+  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+  shows "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen R f pi (ac, sa)"
+  using b c apply -
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
   apply(erule exE)+
diff -r 7b1a3df239cd -r 10a0e3578507 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Mon Feb 22 14:50:53 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Mon Feb 22 15:03:48 2010 +0100
@@ -185,15 +185,12 @@
   apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts)
   apply(simp_all add: akind_aty_atrm.intros)
   apply (simp_all add: akind_aty_atrm_inj)
-  apply(rule alpha_gen_atom_sym)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
-  apply(rule alpha_gen_atom_sym)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
-  apply(rule alpha_gen_atom_sym)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
+  apply(erule alpha_gen_compose_sym)
+  apply(erule alpha_eqvt)
+  apply(erule alpha_gen_compose_sym)
+  apply(erule alpha_eqvt)
+  apply(erule alpha_gen_compose_sym)
+  apply(erule alpha_eqvt)
   done
 
 lemma al_trans:
@@ -206,9 +203,9 @@
   apply(erule akind.cases)
   apply(simp_all add: akind_aty_atrm.intros)
   apply(simp add: akind_aty_atrm_inj)
-  apply(rule alpha_gen_atom_trans)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
+  apply(erule alpha_gen_compose_trans)
+  apply(assumption)
+  apply(erule alpha_eqvt)
   apply(rotate_tac 4)
   apply(erule aty.cases)
   apply(simp_all add: akind_aty_atrm.intros)
@@ -216,9 +213,9 @@
   apply(erule aty.cases)
   apply(simp_all add: akind_aty_atrm.intros)
   apply(simp add: akind_aty_atrm_inj)
-  apply(rule alpha_gen_atom_trans)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
+  apply(erule alpha_gen_compose_trans)
+  apply(assumption)
+  apply(erule alpha_eqvt)
   apply(rotate_tac 4)
   apply(erule atrm.cases)
   apply(simp_all add: akind_aty_atrm.intros)
@@ -226,9 +223,9 @@
   apply(erule atrm.cases)
   apply(simp_all add: akind_aty_atrm.intros)
   apply(simp add: akind_aty_atrm_inj)
-  apply(rule alpha_gen_atom_trans)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
+  apply(erule alpha_gen_compose_trans)
+  apply(assumption)
+  apply(erule alpha_eqvt)
   done
 
 lemma alpha_equivps:
diff -r 7b1a3df239cd -r 10a0e3578507 Quot/Nominal/LamEx2.thy
--- a/Quot/Nominal/LamEx2.thy	Mon Feb 22 14:50:53 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Mon Feb 22 15:03:48 2010 +0100
@@ -137,9 +137,8 @@
   apply(simp add: a1)
   apply(simp add: a2)
   apply(rule a3)
-  apply(rule alpha_gen_atom_sym)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
+  apply(erule alpha_gen_compose_sym)
+  apply(erule alpha_eqvt)
   done
 
 lemma alpha_trans:
@@ -152,9 +151,9 @@
 apply(erule alpha.cases)
 apply(simp_all)
 apply(rule a3)
-apply(rule alpha_gen_atom_trans)
-apply(rule alpha_eqvt)
-apply(assumption)+
+apply(erule alpha_gen_compose_trans)
+apply(assumption)
+apply(erule alpha_eqvt)
 done
 
 lemma alpha_equivp:
diff -r 7b1a3df239cd -r 10a0e3578507 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Mon Feb 22 14:50:53 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 15:03:48 2010 +0100
@@ -116,23 +116,6 @@
   apply(simp add: permute_eqvt[symmetric])
   done
 
-lemma alpha_gen_atom_sym:
-  assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)"
-  using b apply -
-  apply(erule exE)
-  apply(rule_tac x="- pi" in exI)
-  apply(simp add: alpha_gen.simps)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
-  apply simp
-  apply(rule a)
-  apply assumption
-  done
-
 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
 by (tactic {*
 
@@ -148,7 +131,7 @@
  (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW
   TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
- (etac @{thm alpha_gen_atom_sym} THEN'
+ (etac @{thm alpha_gen_compose_sym} THEN'
   asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt})
  )) 1 *})
 
@@ -163,7 +146,7 @@
 apply (rotate_tac 2)
 apply (erule alpha_rtrm1.cases)
 apply (simp_all add: alpha1_inj)
-thm alpha_gen_atom_trans
+apply (erule alpha_gen_compose_trans)
 (*apply (tactic {*
  (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj})) 1 *})*)