--- 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)
--- 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";
--- 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)
--- 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"
--- 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