# HG changeset patch
# User urbanc
# Date 1180615640 -7200
# Node ID 749b6870b1a1dfc1f3a935b5ef161db1dc71b4a2
# Parent  340586b2305cd6595b4c844d74af4c2faebddcb2
introduced symmetric variants of the lemmas for alpha-equivalence

diff -r 340586b2305c -r 749b6870b1a1 src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Thu May 31 14:34:09 2007 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Thu May 31 14:47:20 2007 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory Class
-imports "Nominal" 
+imports "../Nominal" 
 begin
 
 section {* Term-Calculus from Urban's PhD *}
@@ -4084,7 +4084,7 @@
   assumes a: "[a].M = [b].N" "c\<sharp>(a,b,M,N)"
   shows "M = [(a,c)]\<bullet>[(b,c)]\<bullet>N"
 using a
-apply(auto simp add: alpha' fresh_prod fresh_atm)
+apply(auto simp add: alpha_fresh fresh_prod fresh_atm)
 apply(drule sym)
 apply(perm_simp)
 done 
@@ -4095,7 +4095,7 @@
   assumes a: "[x].M = [y].N" "z\<sharp>(x,y,M,N)"
   shows "M = [(x,z)]\<bullet>[(y,z)]\<bullet>N"
 using a
-apply(auto simp add: alpha' fresh_prod fresh_atm)
+apply(auto simp add: alpha_fresh fresh_prod fresh_atm)
 apply(drule sym)
 apply(perm_simp)
 done 
@@ -4107,7 +4107,8 @@
   assumes a: "[x].[b].M = [y].[c].N" "z\<sharp>(x,y,M,N)" "a\<sharp>(b,c,M,N)"
   shows "M = [(x,z)]\<bullet>[(b,a)]\<bullet>[(c,a)]\<bullet>[(y,z)]\<bullet>N"
 using a
-apply(auto simp add: alpha' fresh_prod fresh_atm abs_supp fin_supp abs_fresh abs_perm fresh_left calc_atm)
+apply(auto simp add: alpha_fresh fresh_prod fresh_atm 
+                     abs_supp fin_supp abs_fresh abs_perm fresh_left calc_atm)
 apply(drule sym)
 apply(simp)
 apply(perm_simp)
diff -r 340586b2305c -r 749b6870b1a1 src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Thu May 31 14:34:09 2007 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Thu May 31 14:47:20 2007 +0200
@@ -5,9 +5,9 @@
 Various examples involving nominal datatypes.
 *)
 
+(*use_thy "Class";*)  
 use_thy "CR";
 use_thy "CR_Takahashi";
-(*use_thy "Class";*)
 use_thy "Compile";
 use_thy "Fsub";
 use_thy "Height";
diff -r 340586b2305c -r 749b6870b1a1 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Thu May 31 14:34:09 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Thu May 31 14:47:20 2007 +0200
@@ -15,7 +15,7 @@
   imports "../Nominal"
 begin
 
-atom_decl name 
+atom_decl name
 
 nominal_datatype data = 
     DNat
@@ -314,7 +314,7 @@
     by auto
   obtain c::"name" where "c\<sharp>(\<Gamma>,x,x',t,t')" by (erule exists_fresh[OF fs_name1])
   then have fs: "c\<sharp>\<Gamma>" "c\<noteq>x" "c\<noteq>x'" "c\<sharp>t" "c\<sharp>t'" by (simp_all add: fresh_atm[symmetric]) 
-  then have b5: "[(x',c)]\<bullet>t'=[(x,c)]\<bullet>t" using b3 fs by (simp add: alpha')
+  then have b5: "[(x',c)]\<bullet>t'=[(x,c)]\<bullet>t" using b3 fs by (simp add: alpha_fresh)
   have "([(x,c)]\<bullet>[(x',c)]\<bullet>((x',T\<^isub>1)#\<Gamma>)) \<turnstile> ([(x,c)]\<bullet>[(x',c)]\<bullet>t') : T\<^isub>2" using b2
     by (simp only: typing_eqvt')
   then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2" using fs b1 a2 b5 by (perm_simp add: calc_atm)
@@ -336,7 +336,7 @@
     e1:"[x\<^isub>1].e\<^isub>1=[x\<^isub>1'].e\<^isub>1'" and e2:"[x\<^isub>2].e\<^isub>2=[x\<^isub>2'].e\<^isub>2'"
     by auto
   obtain c::name where f':"c \<sharp> (x\<^isub>1,x\<^isub>1',e\<^isub>1,e\<^isub>1',\<Gamma>)" by (erule exists_fresh[OF fs_name1])
-  have e1':"[(x\<^isub>1,c)]\<bullet>e\<^isub>1 = [(x\<^isub>1',c)]\<bullet>e\<^isub>1'" using e1 f' by (auto simp add: alpha' fresh_prod fresh_atm)
+  have e1':"[(x\<^isub>1,c)]\<bullet>e\<^isub>1 = [(x\<^isub>1',c)]\<bullet>e\<^isub>1'" using e1 f' by (auto simp add: alpha_fresh fresh_prod fresh_atm)
   have "[(x\<^isub>1',c)]\<bullet>((x\<^isub>1',Data \<sigma>\<^isub>1)# \<Gamma>) \<turnstile> [(x\<^isub>1',c)]\<bullet>e\<^isub>1' : T" using h1 typing_eqvt' by blast
   then have x:"(c,Data \<sigma>\<^isub>1)#( [(x\<^isub>1',c)]\<bullet>\<Gamma>) \<turnstile> [(x\<^isub>1',c)]\<bullet>e\<^isub>1': T" using f' 
     by (auto simp add: fresh_atm calc_atm)
@@ -349,7 +349,7 @@
   then have g1:"(x\<^isub>1, Data \<sigma>\<^isub>1)#\<Gamma> \<turnstile> e\<^isub>1 : T"  using f' by (auto simp add: fresh_atm calc_atm fresh_prod)
     (* The second part of the proof is the same *)
   obtain c::name where f':"c \<sharp> (x\<^isub>2,x\<^isub>2',e\<^isub>2,e\<^isub>2',\<Gamma>)" by (erule exists_fresh[OF fs_name1])
-  have e2':"[(x\<^isub>2,c)]\<bullet>e\<^isub>2 = [(x\<^isub>2',c)]\<bullet>e\<^isub>2'" using e2 f' by (auto simp add: alpha' fresh_prod fresh_atm)
+  have e2':"[(x\<^isub>2,c)]\<bullet>e\<^isub>2 = [(x\<^isub>2',c)]\<bullet>e\<^isub>2'" using e2 f' by (auto simp add: alpha_fresh fresh_prod fresh_atm)
   have "[(x\<^isub>2',c)]\<bullet>((x\<^isub>2',Data \<sigma>\<^isub>2)# \<Gamma>) \<turnstile> [(x\<^isub>2',c)]\<bullet>e\<^isub>2' : T" using h2 typing_eqvt' by blast
   then have x:"(c,Data \<sigma>\<^isub>2)#([(x\<^isub>2',c)]\<bullet>\<Gamma>) \<turnstile> [(x\<^isub>2',c)]\<bullet>e\<^isub>2': T" using f' 
     by (auto simp add: fresh_atm calc_atm)
diff -r 340586b2305c -r 749b6870b1a1 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu May 31 14:34:09 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu May 31 14:47:20 2007 +0200
@@ -2778,6 +2778,7 @@
   qed
 qed
 	
+(* alpha equivalence *)
 lemma abs_fun_eq: 
   fixes x  :: "'a"
   and   y  :: "'a"
@@ -2805,7 +2806,21 @@
   qed
 qed
 
+(* symmetric version of alpha-equivalence *)
 lemma abs_fun_eq': 
+  fixes x  :: "'a"
+  and   y  :: "'a"
+  and   a  :: "'x"
+  and   b  :: "'x"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+      and at: "at TYPE('x)"
+  shows "([a].x = [b].y) = ((a=b \<and> x=y)\<or>(a\<noteq>b \<and> [(a,b)]\<bullet>x=y \<and> b\<sharp>x))"
+by (auto simp add: abs_fun_eq[OF pt, OF at] pt_swap_bij[OF pt, OF at] 
+                   pt_fresh_left[OF pt, OF at] 
+                   at_calc[OF at])
+
+(* alpha_equivalence with a fresh name *)
+lemma abs_fun_fresh: 
   fixes x :: "'a"
   and   y :: "'a"
   and   c :: "'x"
@@ -2852,6 +2867,22 @@
   qed
 qed
 
+lemma abs_fun_fresh': 
+  fixes x :: "'a"
+  and   y :: "'a"
+  and   c :: "'x"
+  and   a :: "'x"
+  and   b :: "'x"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+      and at: "at TYPE('x)"
+      and as: "[a].x = [b].y"
+      and fr: "c\<noteq>a" "c\<noteq>b" "c\<sharp>x" "c\<sharp>y" 
+  shows "x = [(a,c)]\<bullet>[(b,c)]\<bullet>y"
+using as fr
+apply(drule_tac sym)
+apply(simp add: abs_fun_fresh[OF pt, OF at] pt_swap_bij[OF pt, OF at])
+done
+
 lemma abs_fun_supp_approx:
   fixes x :: "'a"
   and   a :: "'x"
diff -r 340586b2305c -r 749b6870b1a1 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Thu May 31 14:34:09 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Thu May 31 14:47:20 2007 +0200
@@ -671,6 +671,8 @@
        val abs_fun_pi_ineq     = thm "Nominal.abs_fun_pi_ineq";
        val abs_fun_eq          = thm "Nominal.abs_fun_eq";
        val abs_fun_eq'         = thm "Nominal.abs_fun_eq'";
+       val abs_fun_fresh       = thm "Nominal.abs_fun_fresh";
+       val abs_fun_fresh'      = thm "Nominal.abs_fun_fresh'";
        val dj_perm_forget      = thm "Nominal.dj_perm_forget";
        val dj_pp_forget        = thm "Nominal.dj_perm_perm_forget";
        val fresh_iff           = thm "Nominal.fresh_abs_fun_iff";
@@ -779,6 +781,8 @@
             thy32 
 	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
             ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
+            ||>> PureThy.add_thmss [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])]
+            ||>> PureThy.add_thmss [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])]
             ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
             ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])]	 
             ||>> PureThy.add_thmss