# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265102454 -3600
# Node ID bacf3584640ee1c4760127b72f150a1314399d92
# Parent  89ccda903f4afd29d84881643af1a3df5ff61a41
General alpha_gen_trans for one-variable abstraction.

diff -r 89ccda903f4a -r bacf3584640e Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Tue Feb 02 09:51:39 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 02 10:20:54 2010 +0100
@@ -9,6 +9,20 @@
 apply(simp add: permute_bool_def) 
 done
 
+lemma fresh_plus:
+  fixes p q::perm
+  shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
+  unfolding fresh_def
+  using supp_plus_perm
+  by(auto)
+
+lemma fresh_star_plus:
+  fixes p q::perm
+  shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
+  unfolding fresh_star_def
+  by (simp add: fresh_plus)
+
+
 lemma fresh_star_permute_iff:
   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
 apply(simp add: fresh_star_def)
@@ -25,6 +39,12 @@
 apply(simp)
 done
 
+lemma fresh_minus_perm:
+  fixes p::perm
+  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
+  apply(simp add: fresh_def)
+  apply(simp only: supp_minus_perm)
+  done
 
 fun
   alpha_gen 
@@ -49,6 +69,22 @@
   shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
   using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
 
+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)"
+  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
+
 lemma alpha_gen_trans:
   assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
   and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"
@@ -59,6 +95,27 @@
   apply(blast)
   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)"
+  apply(simp add: alpha_gen.simps)
+  apply(erule conjE)+
+  apply(erule exE)+
+  apply(erule conjE)+
+  apply(rule_tac x="pia + pi" in exI)
+  apply(simp add: fresh_star_plus)
+  apply(drule_tac x="- pia \<bullet> sa" in spec)
+  apply(drule mp)
+  apply(rotate_tac 4)
+  apply(drule_tac pi="- pia" in a)
+  apply(simp)
+  apply(rotate_tac 6)
+  apply(drule_tac pi="pia" in a)
+  apply(simp)
+  done
+
 lemma alpha_gen_eqvt:
   assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
   and     b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
diff -r 89ccda903f4a -r bacf3584640e Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Tue Feb 02 09:51:39 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Tue Feb 02 10:20:54 2010 +0100
@@ -17,7 +17,6 @@
   | Var "name"
   | App "trm" "trm"
   | Lam "ty" "name" "trm"
-print_theorems
 
 primrec
     rfv_kind :: "kind \<Rightarrow> atom set"
@@ -33,7 +32,6 @@
 | "rfv_trm (Var x) = {atom x}"
 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
-print_theorems
 
 instantiation kind and ty and trm :: pt
 begin
diff -r 89ccda903f4a -r bacf3584640e Quot/Nominal/LamEx.thy
--- a/Quot/Nominal/LamEx.thy	Tue Feb 02 09:51:39 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Tue Feb 02 10:20:54 2010 +0100
@@ -2,52 +2,6 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
 begin
 
-
-(* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
-lemma in_permute_iff:
-  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
-apply(unfold mem_def permute_fun_def)[1]
-apply(simp add: permute_bool_def) 
-done
-
-lemma fresh_star_permute_iff:
-  shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
-apply(simp add: fresh_star_def)
-apply(auto)
-apply(drule_tac x="p \<bullet> xa" in bspec)
-apply(unfold mem_def permute_fun_def)[1] 
-apply(simp add: eqvts)
-apply(simp add: fresh_permute_iff)
-apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
-apply(simp)
-apply(drule_tac x="- p \<bullet> xa" in bspec)
-apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
-apply(simp)
-apply(simp)
-done
-
-lemma fresh_minus_perm:
-  fixes p::perm
-  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
-  apply(simp add: fresh_def)
-  apply(simp only: supp_minus_perm)
-  done
-
-lemma fresh_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
-unfolding fresh_def
-using supp_plus_perm
-apply(auto)
-done
-
-lemma fresh_star_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
-unfolding fresh_star_def
-by (simp add: fresh_plus)
-
-
 atom_decl name
 
 datatype rlam =
diff -r 89ccda903f4a -r bacf3584640e Quot/Nominal/LamEx2.thy
--- a/Quot/Nominal/LamEx2.thy	Tue Feb 02 09:51:39 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Tue Feb 02 10:20:54 2010 +0100
@@ -4,42 +4,6 @@
 
 
 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
-lemma in_permute_iff:
-  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
-apply(unfold mem_def permute_fun_def)[1]
-apply(simp add: permute_bool_def) 
-done
-
-lemma fresh_star_permute_iff:
-  shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
-apply(simp add: fresh_star_def)
-apply(auto)
-apply(drule_tac x="p \<bullet> xa" in bspec)
-apply(unfold mem_def permute_fun_def)[1] 
-apply(simp add: eqvts)
-apply(simp add: fresh_permute_iff)
-apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
-apply(simp)
-apply(drule_tac x="- p \<bullet> xa" in bspec)
-apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
-apply(simp)
-apply(simp)
-done
-
-lemma fresh_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
-unfolding fresh_def
-using supp_plus_perm
-apply(auto)
-done
-
-lemma fresh_star_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
-unfolding fresh_star_def
-by (simp add: fresh_plus)
-
 lemma supp_finite_set:
   fixes S::"atom set"
   assumes "finite S"
@@ -191,29 +155,6 @@
 apply(assumption)
 done
 
-lemma fresh_minus_perm:
-  fixes p::perm
-  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
-  apply(simp add: fresh_def)
-  apply(simp only: supp_minus_perm)
-  done
-
-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)"
-  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
-
 lemma alpha_sym:
   shows "t \<approx> s \<Longrightarrow> s \<approx> t"
   apply(induct rule: alpha.induct)
@@ -238,20 +179,9 @@
 apply(erule alpha.cases)
 apply(simp_all)
 apply(rule a3)
-apply(simp add: alpha_gen.simps)
-apply(erule conjE)+
-apply(erule exE)+
-apply(erule conjE)+
-apply(rule_tac x="pia + pi" in exI)
-apply(simp add: fresh_star_plus)
-apply(drule_tac x="- pia \<bullet> sa" in spec)
-apply(drule mp)
-apply(rotate_tac 7)
-apply(drule_tac pi="- pia" in alpha_eqvt)
-apply(simp)
-apply(rotate_tac 9)
-apply(drule_tac pi="pia" in alpha_eqvt)
-apply(simp)
+apply(rule alpha_gen_atom_trans)
+apply(rule alpha_eqvt)
+apply(assumption)+
 done
 
 lemma alpha_equivp: