added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
--- a/src/HOL/Nominal/Examples/Crary.thy Fri Feb 02 15:47:58 2007 +0100
+++ b/src/HOL/Nominal/Examples/Crary.thy Fri Feb 02 17:16:16 2007 +0100
@@ -102,7 +102,7 @@
v_nil[intro]: "valid []"
| v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
-lemma valid_eqvt:
+lemma valid_eqvt[eqvt]:
fixes pi:: "name prm"
assumes a: "valid \<Gamma>"
shows "valid (pi\<bullet>\<Gamma>)"
@@ -129,10 +129,10 @@
using assms
by (induct) (auto)
-lemma typing_eqvt :
+lemma typing_eqvt[eqvt]:
fixes pi::"name prm"
assumes "\<Gamma> \<turnstile> t : T"
- shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : T"
+ shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : (pi\<bullet>T)"
using assms
apply(induct)
apply(auto simp add: fresh_bij set_eqvt valid_eqvt)
@@ -163,29 +163,28 @@
and x :: "'a::fs_name"
assumes a: "\<Gamma> \<turnstile> e : T"
and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
- and a2: "\<And>\<Gamma> e1 T1 T2 e2 c.
- \<lbrakk>\<Gamma> \<turnstile> e1 : T1\<rightarrow>T2 ; \<And>c. P c \<Gamma> e1 (T1\<rightarrow>T2); \<Gamma> \<turnstile> e2 : T1 ; \<And>c. P c \<Gamma> e2 T1\<rbrakk>
+ and a2: "\<And>\<Gamma> e1 T1 T2 e2 c. \<lbrakk>\<And>c. P c \<Gamma> e1 (T1\<rightarrow>T2); \<And>c. P c \<Gamma> e2 T1\<rbrakk>
\<Longrightarrow> P c \<Gamma> (App e1 e2) T2"
- and a3: "\<And>x \<Gamma> T1 t T2 c.
- \<lbrakk>x\<sharp>(\<Gamma>,c); (x,T1)#\<Gamma> \<turnstile> t : T2 ; \<And>c. P c ((x,T1)#\<Gamma>) t T2\<rbrakk>
+ and a3: "\<And>x \<Gamma> T1 t T2 c.\<lbrakk>x\<sharp>(\<Gamma>,c); \<And>c. P c ((x,T1)#\<Gamma>) t T2\<rbrakk>
\<Longrightarrow> P c \<Gamma> (Lam [x].t) (T1\<rightarrow>T2)"
and a4: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> (Const n) TBase"
and a5: "\<And>\<Gamma> c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> Unit TUnit"
shows "P c \<Gamma> e T"
proof -
- from a have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>e) T"
+ from a have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>e) (pi\<bullet>T)"
proof (induct)
case (t_Var \<Gamma> x T pi c)
have "valid \<Gamma>" by fact
- then have "valid (pi\<bullet>\<Gamma>)" by (simp only: valid_eqvt)
+ then have "valid (pi\<bullet>\<Gamma>)" by (simp only: eqvt)
moreover
have "(x,T)\<in>set \<Gamma>" by fact
then have "pi\<bullet>(x,T)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])
then have "(pi\<bullet>x,T)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: set_eqvt)
- ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Var x)) T" using a1 by simp
+ ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Var x)) (pi\<bullet>T)" using a1 by simp
next
case (t_App \<Gamma> e1 T1 T2 e2 pi c)
- thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(App e1 e2)) T2" using a2 by (simp, blast intro: typing_eqvt)
+ thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(App e1 e2)) (pi\<bullet>T2)" using a2
+ by (simp only: eqvt) (blast)
next
case (t_Lam x \<Gamma> T1 t T2 pi c)
obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>\<Gamma>,pi\<bullet>t,c)" by (erule exists_fresh[OF fs_name1])
@@ -194,11 +193,8 @@
have f0: "x\<sharp>\<Gamma>" by fact
have f1: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f0 by (simp add: fresh_bij)
have f2: "y\<sharp>?pi'\<bullet>\<Gamma>" by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp)
- have pr1: "(x,T1)#\<Gamma> \<turnstile> t : T2" by fact
- then have "(?pi'\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>t) : T2" by (simp only: typing_eqvt)
- moreover
- have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>t) T2" by fact
- ultimately have "P c (?pi'\<bullet>\<Gamma>) (Lam [y].(?pi'\<bullet>t)) (T1\<rightarrow>T2)" using fs f2 a3
+ have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>T2)" by fact
+ then have "P c (?pi'\<bullet>\<Gamma>) (Lam [y].(?pi'\<bullet>t)) (T1\<rightarrow>T2)" using fs f2 a3
by (simp add: calc_atm)
then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) (T1\<rightarrow>T2)"
by (simp del: append_Cons add: calc_atm pt_name2)
@@ -206,18 +202,17 @@
by (rule perm_fresh_fresh) (simp_all add: fs f1)
moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) = Lam [(pi\<bullet>x)].(pi\<bullet>t)"
by (rule perm_fresh_fresh) (simp_all add: fs f1 fresh_atm abs_fresh)
- ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [x].t)) (T1\<rightarrow>T2)"
- by simp
+ ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [x].t)) (pi\<bullet>T1\<rightarrow>T2)" by simp
next
case (t_Const \<Gamma> n pi c)
- thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Const n)) (TBase)" using a4 by (simp, blast intro: valid_eqvt)
+ thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Const n)) (pi\<bullet>TBase)" using a4 by (simp, blast intro: valid_eqvt)
next
case (t_Unit \<Gamma> pi c)
- thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Unit) (TUnit)" using a5 by (simp, blast intro: valid_eqvt)
+ thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Unit) (pi\<bullet>TUnit)" using a5 by (simp, blast intro: valid_eqvt)
qed
- then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>e) T" by blast
+ then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>e) (([]::name prm)\<bullet>T)" by blast
then show "P c \<Gamma> e T" by simp
-qed
+qed
text {* capture-avoiding substitution *}
@@ -279,7 +274,7 @@
and "Unit [y::=t'] = Unit"
by (simp_all add: fresh_list_cons fresh_list_nil)
-lemma subst_eqvt:
+lemma subst_eqvt[eqvt]:
fixes pi::"name prm"
and t::"trm"
shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]"
@@ -371,13 +366,13 @@
shows "valid \<Gamma>"
using assms by (induct,auto elim:typing_valid)
-lemma equiv_def_eqvt:
+lemma equiv_def_eqvt[eqvt]:
fixes pi::"name prm"
assumes a: "\<Gamma> \<turnstile> s == t : T"
- shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) == (pi\<bullet>t) : T"
+ shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) == (pi\<bullet>t) : (pi\<bullet>T)"
using a
apply(induct)
-apply(auto intro: typing_eqvt valid_eqvt simp add: fresh_bij subst_eqvt)
+apply(auto intro: typing_eqvt valid_eqvt simp add: fresh_bij subst_eqvt simp del: perm_ty)
apply(rule_tac x="pi\<bullet>x" in Q_Ext)
apply(simp add: fresh_bij)+
done
@@ -387,46 +382,39 @@
fixes c::"'a::fs_name"
assumes a0: "\<Gamma> \<turnstile> s == t : T"
and a1: "\<And>\<Gamma> t T c. \<Gamma> \<turnstile> t : T \<Longrightarrow> P c \<Gamma> t t T"
- and a2: "\<And>\<Gamma> t s T c. \<lbrakk>\<Gamma> \<turnstile> t == s : T; \<And>d. P d \<Gamma> t s T\<rbrakk> \<Longrightarrow> P c \<Gamma> s t T"
- and a3: "\<And>\<Gamma> s t T u c.
- \<lbrakk>\<Gamma> \<turnstile> s == t : T; \<And>d. P d \<Gamma> s t T; \<Gamma> \<turnstile> t == u : T; \<And>d. P d \<Gamma> t u T\<rbrakk>
+ and a2: "\<And>\<Gamma> t s T c. \<lbrakk>\<And>d. P d \<Gamma> t s T\<rbrakk> \<Longrightarrow> P c \<Gamma> s t T"
+ and a3: "\<And>\<Gamma> s t T u c. \<lbrakk>\<And>d. P d \<Gamma> s t T; \<And>d. P d \<Gamma> t u T\<rbrakk>
\<Longrightarrow> P c \<Gamma> s u T"
- and a4: "\<And>x \<Gamma> T1 s2 t2 T2 c. \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>c; (x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2; \<And>d. P d ((x,T1)#\<Gamma>) s2 t2 T2\<rbrakk>
+ and a4: "\<And>x \<Gamma> T1 s2 t2 T2 c. \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>c; \<And>d. P d ((x,T1)#\<Gamma>) s2 t2 T2\<rbrakk>
\<Longrightarrow> P c \<Gamma> (Lam [x].s2) (Lam [x].t2) (T1\<rightarrow>T2)"
- and a5: "\<And>\<Gamma> s1 t1 T1 T2 s2 t2 c.
- \<lbrakk>\<Gamma> \<turnstile> s1 == t1 : T1\<rightarrow>T2; \<And>d. P d \<Gamma> s1 t1 (T1\<rightarrow>T2);
- \<Gamma> \<turnstile> s2 == t2 : T1; \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> \<Longrightarrow> P c \<Gamma> (App s1 s2) (App t1 t2) T2"
+ and a5: "\<And>\<Gamma> s1 t1 T1 T2 s2 t2 c. \<lbrakk>\<And>d. P d \<Gamma> s1 t1 (T1\<rightarrow>T2); \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk>
+ \<Longrightarrow> P c \<Gamma> (App s1 s2) (App t1 t2) T2"
and a6: "\<And>x \<Gamma> T1 s12 t12 T2 s2 t2 c.
- \<lbrakk>x\<sharp>(\<Gamma>,s2,t2); x\<sharp>c; (x,T1)#\<Gamma> \<turnstile> s12 == t12 : T2; \<And>d. P d ((x,T1)#\<Gamma>) s12 t12 T2;
- \<Gamma> \<turnstile> s2 == t2 : T1; \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk>
+ \<lbrakk>x\<sharp>(\<Gamma>,s2,t2); x\<sharp>c; \<And>d. P d ((x,T1)#\<Gamma>) s12 t12 T2; \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk>
\<Longrightarrow> P c \<Gamma> (App (Lam [x].s12) s2) (t12[x::=t2]) T2"
and a7: "\<And>x \<Gamma> s t T1 T2 c.
- \<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T1)#\<Gamma> \<turnstile> App s (Var x) == App t (Var x) : T2;
- \<And>d. P d ((x,T1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T2\<rbrakk>
+ \<lbrakk>x\<sharp>(\<Gamma>,s,t); \<And>d. P d ((x,T1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T2\<rbrakk>
\<Longrightarrow> P c \<Gamma> s t (T1\<rightarrow>T2)"
shows "P c \<Gamma> s t T"
proof -
- from a0 have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) T"
+ from a0 have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)"
proof(induct)
case (Q_Refl \<Gamma> t T pi c)
- then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>t) T" using a1 by (simp add: typing_eqvt)
+ then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>t) (pi\<bullet>T)" using a1 by (simp only: eqvt)
next
case (Q_Symm \<Gamma> t s T pi c)
- then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) T" using a2 by (simp only: equiv_def_eqvt)
+ then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" using a2 by (simp only: equiv_def_eqvt)
next
case (Q_Trans \<Gamma> s t T u pi c)
- then show " P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>u) T" using a3 by (blast intro: equiv_def_eqvt)
+ then show " P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>u) (pi\<bullet>T)" using a3 by (blast intro: equiv_def_eqvt)
next
case (Q_App \<Gamma> s1 t1 T1 T2 s2 t2 pi c)
- then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App s1 s2) (pi\<bullet>App t1 t2) T2" using a5
- by (simp, blast intro: equiv_def_eqvt)
+ then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App s1 s2) (pi\<bullet>App t1 t2) (pi\<bullet>T2)" using a5
+ by (simp only: eqvt) (blast)
next
case (Q_Ext x \<Gamma> s t T1 T2 pi c)
- then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (T1\<rightarrow>T2)"
- apply(auto intro!: a7 simp add: fresh_bij)
- apply(drule equiv_def_eqvt)
- apply(simp)
- done
+ then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T1\<rightarrow>T2)"
+ by (auto intro!: a7 simp add: fresh_bij)
next
case (Q_Abs x \<Gamma> T1 s2 t2 T2 pi c)
obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s2,pi\<bullet>t2,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1])
@@ -435,13 +423,9 @@
have f1: "x\<sharp>\<Gamma>" by fact
have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij)
have f3: "y\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp)
- have pr1: "(x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2" by fact
- then have "?pi'\<bullet>((x,T1)#\<Gamma>) \<turnstile> (?pi'\<bullet>s2) == (?pi'\<bullet>t2) : T2" by (rule equiv_def_eqvt)
- then have "((y,T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>s2) == (?pi'\<bullet>t2) : T2" by (simp add: calc_atm)
- moreover
- have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T2" by fact
+ have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) (?pi'\<bullet>T2)" by fact
then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T2" by (simp add: calc_atm)
- ultimately have "P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>Lam [x].s2) (?pi'\<bullet>Lam [x].t2) (T1\<rightarrow>T2)" using a4 f3 fs
+ then have "P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>Lam [x].s2) (?pi'\<bullet>Lam [x].t2) (T1\<rightarrow>T2)" using a4 f3 fs
by (simp add: calc_atm)
then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>s2)) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>t2)) (T1\<rightarrow>T2)"
by (simp del: append_Cons add: calc_atm pt_name2)
@@ -452,7 +436,7 @@
moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t2))) = Lam [(pi\<bullet>x)].(pi\<bullet>t2)"
by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh)
ultimately have "P c (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>x)].(pi\<bullet>s2)) (Lam [(pi\<bullet>x)].(pi\<bullet>t2)) (T1\<rightarrow>T2)" by simp
- then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Lam [x].s2) (pi\<bullet>Lam [x].t2) (T1\<rightarrow>T2)" by simp
+ then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Lam [x].s2) (pi\<bullet>Lam [x].t2) (pi\<bullet>T1\<rightarrow>T2)" by simp
next
case (Q_Beta x \<Gamma> s2 t2 T1 s12 t12 T2 pi c)
obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s12,pi\<bullet>t12,pi\<bullet>s2,pi\<bullet>t2,pi\<bullet>\<Gamma>,c)"
@@ -463,19 +447,12 @@
have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s2,t2))" using f1 by (simp add: fresh_bij)
have f3: "y\<sharp>(?pi'\<bullet>(\<Gamma>,s2,t2))" using f1
by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp fresh_prod)
- have pr1: "(x,T1)#\<Gamma> \<turnstile> s12 == t12 : T2" by fact
- then have "?pi'\<bullet>((x,T1)#\<Gamma>) \<turnstile> (?pi'\<bullet>s12) == (?pi'\<bullet>t12) : T2" by (rule equiv_def_eqvt)
- then have "((y,T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>s12) == (?pi'\<bullet>t12) : T2" by (simp add: calc_atm)
- moreover
- have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) T2" by fact
- then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) T2" by (simp add: calc_atm)
+ have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) (?pi'\<bullet>T2)" by fact
+ then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) (?pi'\<bullet>T2)" by (simp add: calc_atm)
moreover
- have pr2: "\<Gamma> \<turnstile> s2 == t2 : T1" by fact
- then have "(?pi'\<bullet>\<Gamma>) \<turnstile> (?pi'\<bullet>s2) == (?pi'\<bullet>t2) : T1" by (rule equiv_def_eqvt)
- moreover
- have ih2: "\<And>c. P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T1" by fact
- ultimately have "P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>(App (Lam [x].s12) s2)) (?pi'\<bullet>(t12[x::=t2])) T2"
- using a6 f3 fs by (simp add: subst_eqvt calc_atm)
+ have ih2: "\<And>c. P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s2) (?pi'\<bullet>t2) (?pi'\<bullet>T1)" by fact
+ ultimately have "P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>(App (Lam [x].s12) s2)) (?pi'\<bullet>(t12[x::=t2])) (?pi'\<bullet>T2)"
+ using a6 f3 fs by (force simp add: subst_eqvt calc_atm del: perm_ty)
then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2)))
(?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])) T2"
by (simp del: append_Cons add: calc_atm pt_name2 subst_eqvt)
@@ -488,9 +465,9 @@
(simp_all add: fs[simplified] f2[simplified] fresh_subst fresh_subst'')
ultimately have "P c (pi\<bullet>\<Gamma>) (App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2)) ((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)]) T2"
by simp
- then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App (Lam [x].s12) s2) (pi\<bullet>t12[x::=t2]) T2" by (simp add: subst_eqvt)
+ then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App (Lam [x].s12) s2) (pi\<bullet>t12[x::=t2]) (pi\<bullet>T2)" by (simp add: subst_eqvt)
qed
- then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) T" by blast
+ then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>T)" by blast
then show "P c \<Gamma> s t T" by simp
qed
@@ -538,7 +515,7 @@
using a
by (induct) (auto simp add: subst_eqvt fresh_bij)
-lemma whn_eqvt:
+lemma whn_eqvt[eqvt]:
fixes pi::"name prm"
assumes a: "t \<Down> t'"
shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')"
@@ -568,10 +545,10 @@
| QAP_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T1 \<rightarrow> T2; \<Gamma> \<turnstile> s <=> t : T1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T2"
| QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase"
-lemma alg_equiv_alg_path_equiv_eqvt:
+lemma alg_equiv_alg_path_equiv_eqvt[eqvt]:
fixes pi::"name prm"
- shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : T"
- and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>p) \<leftrightarrow> (pi\<bullet>q) : T"
+ shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : (pi\<bullet>T)"
+ and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>p) \<leftrightarrow> (pi\<bullet>q) : (pi\<bullet>T)"
apply(induct rule: alg_equiv_alg_path_equiv.inducts)
apply(auto intro: whn_eqvt simp add: fresh_bij valid_eqvt)
apply(rule_tac x="pi\<bullet>x" in QAT_Arrow)
@@ -606,7 +583,7 @@
then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TBase"
apply(auto)
apply(rule_tac p="pi\<bullet>q" and q="pi\<bullet>p" in a1)
- apply(simp_all add: whn_eqvt alg_equiv_alg_path_equiv_eqvt)
+ apply(simp_all add: whn_eqvt alg_equiv_alg_path_equiv_eqvt[simplified])
done
next
case (QAT_Arrow x \<Gamma> s t T1 T2)
@@ -623,8 +600,8 @@
by (simp only: pt_name2 fresh_left, auto simp add: perm_pi_simp calc_atm)
then have f3': "y\<sharp>?pi'\<bullet>\<Gamma>" "y\<sharp>?pi'\<bullet>s" "y\<sharp>?pi'\<bullet>t" by (auto simp add: fresh_prod)
have pr1: "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact
- then have "(?pi'\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>(App s (Var x))) <=> (?pi'\<bullet>(App t (Var x))) : T2"
- by (simp only: alg_equiv_alg_path_equiv_eqvt)
+ then have "(?pi'\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>(App s (Var x))) <=> (?pi'\<bullet>(App t (Var x))) : (?pi'\<bullet>T2)"
+ by (rule alg_equiv_alg_path_equiv_eqvt)
then have "(y,T1)#(?pi'\<bullet>\<Gamma>) \<turnstile> (App (?pi'\<bullet>s) (Var y)) <=> (App (?pi'\<bullet>t) (Var y)) : T2"
by (simp add: calc_atm)
moreover
@@ -659,7 +636,7 @@
next
case (QAP_App \<Gamma> p q T1 T2 s t)
then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>App p s) (pi\<bullet>App q t) T2"
- by (auto intro!: a5 simp add: alg_equiv_alg_path_equiv_eqvt)
+ by (auto intro!: a5 simp add: alg_equiv_alg_path_equiv_eqvt[simplified])
next
case (QAP_Const \<Gamma> n)
then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>Const n) (pi\<bullet>Const n) TBase"
@@ -724,7 +701,6 @@
proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv_strong_inducts)
case (QAT_Arrow x \<Gamma> s t T1 T2 \<Gamma>')
have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
- have h1:"(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact
have h2:"\<Gamma>\<lless>\<Gamma>'" by fact
have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T1)#\<Gamma> \<lless> \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact
have "x\<sharp>\<Gamma>'" by fact
@@ -984,7 +960,8 @@
have "(pi\<bullet>((x,T1)#\<Gamma>)) \<turnstile> pi \<bullet> (App s (Var x)) <=> pi \<bullet> (App t (Var x)) : T2" by fact
then have "(pi\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" by auto
moreover have "pi\<bullet>((x,T1)#\<Gamma>) = (pi\<bullet>x,pi\<bullet>T1)#(pi\<bullet>\<Gamma>)" by auto
- ultimately have "((pi\<bullet>x,T1)#(pi\<bullet>\<Gamma>)) \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" using perm_ty by auto
+ ultimately have "((pi\<bullet>x,T1)#(pi\<bullet>\<Gamma>)) \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2"
+ using perm_ty by auto
then show ?case using h by auto
qed (auto elim:whn_eqvt valid_eqvt)
@@ -1271,7 +1248,6 @@
case (Q_Abs x \<Gamma> T1 s2 t2 T2 \<Gamma>' \<gamma> \<theta>)
have fs:"x\<sharp>\<Gamma>" by fact
have fs2: "x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact
- have h1:"(x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2" by fact
have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T2" by fact
{
--- a/src/HOL/Nominal/Examples/Weakening.thy Fri Feb 02 15:47:58 2007 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy Fri Feb 02 17:16:16 2007 +0100
@@ -32,7 +32,7 @@
v1[intro]: "valid []"
| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
-lemma eqvt_valid:
+lemma eqvt_valid[eqvt]:
fixes pi:: "name prm"
assumes a: "valid \<Gamma>"
shows "valid (pi\<bullet>\<Gamma>)"
@@ -40,6 +40,8 @@
by (induct)
(auto simp add: fresh_bij)
+thm eqvt
+
text{* typing judgements *}
inductive2
typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
@@ -48,22 +50,22 @@
| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
| t_Lam[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
-lemma eqvt_typing:
+lemma eqvt_typing[eqvt]:
fixes pi:: "name prm"
assumes a: "\<Gamma> \<turnstile> t : \<tau>"
- shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
+ shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : (pi\<bullet>\<tau>)"
using a
proof (induct)
case (t_Var \<Gamma> a \<tau>)
have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid)
moreover
have "(pi\<bullet>(a,\<tau>))\<in>(pi\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
- ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Var a) : \<tau>"
+ ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Var a) : (pi\<bullet>\<tau>)"
using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
next
case (t_Lam a \<Gamma> \<tau> t \<sigma>)
moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
- ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force
+ ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :(pi\<bullet>\<tau>\<rightarrow>\<sigma>)" by force
qed (auto)
text {* the strong induction principle needs to be derived manually *}
@@ -76,26 +78,26 @@
and x :: "'a::fs_name"
assumes a: "\<Gamma> \<turnstile> t : \<tau>"
and a1: "\<And>\<Gamma> a \<tau> x. \<lbrakk>valid \<Gamma>; (a,\<tau>) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>"
- and a2: "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x.
- \<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; (\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>)); \<Gamma> \<turnstile> t2 : \<tau>; (\<And>z. P z \<Gamma> t2 \<tau>)\<rbrakk>
+ and a2: "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. \<lbrakk>\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>); \<And>z. P z \<Gamma> t2 \<tau>\<rbrakk>
\<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>"
- and a3: "\<And>a \<Gamma> \<tau> \<sigma> t x. \<lbrakk>a\<sharp>x; a\<sharp>\<Gamma>; ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>; (\<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>)\<rbrakk>
+ and a3: "\<And>a \<Gamma> \<tau> \<sigma> t x. \<lbrakk>a\<sharp>x; a\<sharp>\<Gamma>; \<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>\<rbrakk>
\<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)"
shows "P x \<Gamma> t \<tau>"
proof -
- from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>"
+ from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>\<tau>)"
proof (induct)
case (t_Var \<Gamma> a \<tau>)
have "valid \<Gamma>" by fact
- then have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid)
+ then have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt)
moreover
have "(a,\<tau>)\<in>set \<Gamma>" by fact
then have "pi\<bullet>(a,\<tau>)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])
then have "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])
- ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 by simp
+ ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) (pi\<bullet>\<tau>)" using a1 by simp
next
case (t_App \<Gamma> t1 \<tau> \<sigma> t2)
- thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(App t1 t2)) \<sigma>" using a2 by (simp, blast intro: eqvt_typing)
+ thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(App t1 t2)) (pi\<bullet>\<sigma>)" using a2
+ by (simp only: eqvt) (blast)
next
case (t_Lam a \<Gamma> \<tau> t \<sigma>)
obtain c::"name" where fs: "c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" by (rule exists_fresh[OF fs_name1])
@@ -104,22 +106,18 @@
have f1: "a\<sharp>\<Gamma>" by fact
have f2: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij)
have f3: "c\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp)
- have pr1: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
- then have "(?pi'\<bullet>((a,\<tau>)#\<Gamma>)) \<turnstile> (?pi'\<bullet>t) : \<sigma>" by (rule eqvt_typing)
- then have "((c,\<tau>)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>t) : \<sigma>" by (simp add: calc_atm)
- moreover
- have ih1: "\<And>x. P x (?pi'\<bullet>((a,\<tau>)#\<Gamma>)) (?pi'\<bullet>t) \<sigma>" by fact
- then have "\<And>x. P x ((c,\<tau>)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>t) \<sigma>" by (simp add: calc_atm)
- ultimately have "P x (?pi'\<bullet>\<Gamma>) (Lam [c].(?pi'\<bullet>t)) (\<tau> \<rightarrow> \<sigma>)" using a3 f3 fs by simp
- then have "P x (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) (\<tau> \<rightarrow> \<sigma>)"
+ have ih1: "\<And>x. P x (?pi'\<bullet>((a,\<tau>)#\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>\<sigma>)" by fact
+ then have "\<And>x. P x ((c,\<tau>)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>\<sigma>)" by (simp add: calc_atm)
+ then have "P x (?pi'\<bullet>\<Gamma>) (Lam [c].(?pi'\<bullet>t)) (\<tau>\<rightarrow>\<sigma>)" using a3 f3 fs by simp
+ then have "P x (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) (\<tau>\<rightarrow>\<sigma>)"
by (simp del: append_Cons add: calc_atm pt_name2)
moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)"
by (rule perm_fresh_fresh) (simp_all add: fs f2)
moreover have "(?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) = Lam [(pi\<bullet>a)].(pi\<bullet>t)"
by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh)
- ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (\<tau> \<rightarrow> \<sigma>)" by (simp only: , simp)
+ ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (pi\<bullet>\<tau>\<rightarrow>\<sigma>)" by (simp)
qed
- hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) \<tau>" by blast
+ hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>\<tau>)" by blast
thus "P x \<Gamma> t \<tau>" by simp
qed
--- a/src/HOL/Nominal/Nominal.thy Fri Feb 02 15:47:58 2007 +0100
+++ b/src/HOL/Nominal/Nominal.thy Fri Feb 02 17:16:16 2007 +0100
@@ -4,6 +4,7 @@
imports Main Infinite_Set
uses
("nominal_atoms.ML")
+ ("nominal_tags.ML")
("nominal_package.ML")
("nominal_induct.ML")
("nominal_permeq.ML")
@@ -3006,22 +3007,19 @@
(* setup for the individial atom-kinds *)
(* and nominal datatypes *)
use "nominal_atoms.ML"
+setup "NominalAtoms.setup"
+
+(******************************************)
+(* Setup of the tags: eqvt, fresh and bij *)
+
+use "nominal_tags.ML"
+setup "EqvtRules.setup"
+setup "FreshRules.setup"
+setup "BijRules.setup"
+
+(*******************************)
(* permutation equality tactic *)
use "nominal_permeq.ML";
-use "nominal_package.ML"
-setup "NominalAtoms.setup"
-setup "NominalPackage.setup"
-
-(** primitive recursive functions on nominal datatypes **)
-use "nominal_primrec.ML"
-
-(*****************************************)
-(* setup for induction principles method *)
-
-use "nominal_induct.ML";
-method_setup nominal_induct =
- {* NominalInduct.nominal_induct_method *}
- {* nominal induction *}
method_setup perm_simp =
{* NominalPermeq.perm_eq_meth *}
@@ -3063,4 +3061,22 @@
{* NominalPermeq.fresh_gs_meth_debug *}
{* tactic for deciding whether an atom is fresh for something including debugging facilities *}
+(*********************************)
+(* nominal datatype construction *)
+use "nominal_package.ML"
+setup "NominalPackage.setup"
+
+(******************************************************)
+(* primitive recursive functions on nominal datatypes *)
+use "nominal_primrec.ML"
+
+(*****************************************)
+(* setup for induction principles method *)
+
+use "nominal_induct.ML";
+method_setup nominal_induct =
+ {* NominalInduct.nominal_induct_method *}
+ {* nominal induction *}
+
+
end
--- a/src/HOL/Nominal/nominal_package.ML Fri Feb 02 15:47:58 2007 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Fri Feb 02 17:16:16 2007 +0100
@@ -1104,6 +1104,7 @@
end) atoms;
val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];
+ val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add, EqvtRules.eqvt_add];
val (_, thy9) = thy8 |>
Theory.add_path big_name |>
@@ -1112,7 +1113,7 @@
Theory.parent_path ||>>
DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
- DatatypeAux.store_thmss_atts "perm" new_type_names simp_atts perm_simps' ||>>
+ DatatypeAux.store_thmss_atts "perm" new_type_names simp_eqvt_atts perm_simps' ||>>
DatatypeAux.store_thmss "inject" new_type_names inject_thms ||>>
DatatypeAux.store_thmss "supp" new_type_names supp_thms ||>>
DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/nominal_tags.ML Fri Feb 02 17:16:16 2007 +0100
@@ -0,0 +1,267 @@
+(* ID: "$Id$"
+ Authors: Julien Narboux and Christian Urban
+
+ This file introduces the infrastructure for the lemma
+ declaration "eqvt" "bij" and "fresh".
+
+ By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
+ in a data-slot in the theory context. Possible modifiers
+ are [tag add] and [tag del] for adding and deleting,
+ respectively the lemma from the data-slot.
+*)
+
+signature EQVT_RULES =
+sig
+ val print_eqvtset: Proof.context -> unit
+ val eqvt_add: attribute
+ val eqvt_del: attribute
+ val setup: theory -> theory
+
+ val EQVT_DEBUG : bool ref
+end;
+
+structure EqvtRules: EQVT_RULES =
+struct
+
+structure Data = GenericDataFun
+(
+ val name = "HOL/Nominal/eqvt";
+ type T = thm list;
+ val empty = [];
+ val extend = I;
+ fun merge _ = Drule.merge_rules;
+ fun print context rules =
+ Pretty.writeln (Pretty.big_list "Equivariance lemmas:"
+ (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
+);
+
+(* Exception for when a theorem does not conform with form of an equivariance lemma. *)
+(* There are two forms: one is an implication (for relations) and the other is an *)
+(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal *)
+(* to P except that every free variable of Q, say x, is replaced by pi o x. In the *)
+(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *)
+(* be equal to t except that every free variable, say x, is replaced by pi o x. In *)
+(* the implicational case it is also checked that the variables and permutation fit *)
+(* together, i.e. are of the right "pt_class", so that a stronger version of the *)
+(* eqality-lemma can be derived. *)
+exception EQVT_FORM;
+
+val print_eqvtset = Data.print o Context.Proof;
+
+(* FIXME: should be a function in a library *)
+fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
+
+val perm_bool = thm "perm_bool";
+
+val EQVT_DEBUG = ref false;
+
+fun tactic (msg,tac) =
+ if !EQVT_DEBUG
+ then (EVERY [tac, print_tac ("after "^msg)])
+ else tac
+
+fun tactic_eqvt ctx orig_thm pi typi =
+ let
+ val mypi = Thm.cterm_of ctx (Var (pi,typi))
+ val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
+ val perm_pi_simp = PureThy.get_thms ctx (Name "perm_pi_simp")
+ in
+ EVERY [tactic ("iffI applied",rtac iffI 1),
+ tactic ("simplifies with orig_thm and perm_bool",
+ asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1),
+ tactic ("applies orig_thm instantiated with rev pi",
+ dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
+ tactic ("getting rid of all remaining perms",
+ full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)]
+ end;
+
+fun get_derived_thm thy hyp concl orig_thm pi typi =
+ let
+ val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
+ val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
+ val _ = Display.print_cterm (cterm_of thy goal_term)
+ in
+ Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
+ end
+
+(* FIXME: something naughty here, but as long as there is no infrastructure to expose *)
+(* the eqvt_thm_list to the user, we have to manually update the context and the *)
+(* thm-list eqvt *)
+fun update_context flag thms context =
+ let
+ val context' = fold (fn thm => Data.map (flag thm)) thms context
+ in
+ Context.mapping (snd o PureThy.add_thmss [(("eqvt",Data.get context'),[])]) I context'
+ end;
+
+(* replaces every variable, say x, in t with pi o x *)
+fun apply_pi trm (pi,typi) =
+ let
+ fun only_vars t =
+ (case t of
+ Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty)))
+ | _ => t)
+ in
+ map_aterms only_vars trm
+ end;
+
+(* returns *the* pi which is in front of all variables, provided there *)
+(* exists such a pi; otherwise raises EQVT_FORM *)
+fun get_pi t thy =
+ let fun get_pi_aux s =
+ (case s of
+ (Const ("Nominal.perm",typrm) $
+ (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
+ (Var (n,ty))) =>
+ let
+ (* FIXME: this should be an operation the library *)
+ val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
+ in
+ if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
+ then [(pi,typi)]
+ else raise EQVT_FORM
+ end
+ | Abs (_,_,t1) => get_pi_aux t1
+ | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
+ | _ => [])
+ in
+ (* collect first all pi's in front of variables in t and then use distinct *)
+ (* to ensure that all pi's must have been the same, i.e. distinct returns *)
+ (* a singleton-list *)
+ (case (distinct (op =) (get_pi_aux t)) of
+ [(pi,typi)] => (pi,typi)
+ | _ => raise EQVT_FORM)
+ end;
+
+(* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *)
+(* lemma list depending on flag. To be added the lemma has to satisfy a *)
+(* certain form. *)
+fun eqvt_add_del_aux flag orig_thm context =
+ let
+ val thy = Context.theory_of context
+ val thms_to_be_added = (case (prop_of orig_thm) of
+ (* case: eqvt-lemma is of the implicational form *)
+ (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
+ let
+ val (pi,typi) = get_pi concl thy
+ in
+ if (apply_pi hyp (pi,typi) = concl)
+ then
+ (warning ("equivariance lemma of the relational form");
+ [orig_thm, get_derived_thm thy hyp concl orig_thm pi typi])
+ else raise EQVT_FORM
+ end
+ (* case: eqvt-lemma is of the equational form *)
+ | (Const ("Trueprop", _) $ (Const ("op =", _) $
+ (Const ("Nominal.perm",_) $ Var (pi,typi) $ lhs) $ rhs)) =>
+ (if (apply_pi lhs (pi,typi)) = rhs
+ then [orig_thm]
+ else raise EQVT_FORM)
+ | _ => raise EQVT_FORM)
+ in
+ update_context flag thms_to_be_added context
+ end
+ handle EQVT_FORM =>
+ error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma.")
+
+val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux Drule.add_rule);
+val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux Drule.del_rule);
+
+val setup =
+ Data.init #>
+ Attrib.add_attributes [("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance rules")];
+
+end;
+
+
+
+signature BIJ_RULES =
+sig
+ val print_bijset: Proof.context -> unit
+ val bij_add: attribute
+ val bij_del: attribute
+ val setup: theory -> theory
+end;
+
+structure BijRules: BIJ_RULES =
+struct
+
+structure Data = GenericDataFun
+(
+ val name = "HOL/Nominal/bij";
+ type T = thm list;
+ val empty = [];
+ val extend = I;
+ fun merge _ = Drule.merge_rules;
+ fun print context rules =
+ Pretty.writeln (Pretty.big_list "Bijection lemmas:"
+ (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
+);
+
+val print_bijset = Data.print o Context.Proof;
+
+fun bij_add_del_aux f = fn th => fn context =>
+ let val new_context = Data.map (f th) context
+ in
+ Context.mapping (snd o PureThy.add_thmss [(("bij",Data.get new_context),[])]) I new_context
+ end
+
+val bij_add = Thm.declaration_attribute (bij_add_del_aux Drule.add_rule);
+val bij_del = Thm.declaration_attribute (bij_add_del_aux Drule.del_rule);
+
+val setup =
+ Data.init #>
+ Attrib.add_attributes [("bij", Attrib.add_del_args bij_add bij_del, "bijection rules")];
+
+end;
+
+
+signature FRESH_RULES =
+sig
+ val print_freshset: Proof.context -> unit
+ val fresh_add: attribute
+ val fresh_del: attribute
+ val setup: theory -> theory
+end;
+
+structure FreshRules: FRESH_RULES =
+struct
+
+structure Data = GenericDataFun
+(
+ val name = "HOL/Nominal/fresh";
+ type T = thm list;
+ val empty = [];
+ val extend = I;
+ fun merge _ = Drule.merge_rules;
+ fun print context rules =
+ Pretty.writeln (Pretty.big_list "Freshness lemmas:"
+ (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
+);
+
+val print_freshset = Data.print o Context.Proof;
+
+fun fresh_add_del_aux f = fn th => fn context =>
+ let val new_context = Data.map (f th) context
+ in
+ Context.mapping (snd o PureThy.add_thmss [(("fresh",Data.get new_context),[])]) I new_context
+ end
+
+val fresh_add = Thm.declaration_attribute (fresh_add_del_aux Drule.add_rule);
+val fresh_del = Thm.declaration_attribute (fresh_add_del_aux Drule.del_rule);
+
+val setup =
+ Data.init #>
+ Attrib.add_attributes [("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness rules")];
+
+end;
+
+(* Thm.declaration_attribute is of type (thm -> Context.generic -> Context.generic) -> attribute *)
+
+(* Thm.declaration_attribute has type (thm -> Context.generic -> Context.generic) -> attribute *)
+
+(* Drule.add_rule has type thm -> thm list -> thm list *)
+
+(* Data.map has type thm list -> thm list -> Context.generic -> Context.generic *)
+
+(* add_del_args is of type attribute -> attribute -> src -> attribute *)
\ No newline at end of file