--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy Wed May 02 01:42:23 2007 +0200
@@ -4,15 +4,19 @@
imports Lam_Funs
begin
-text {* The Church-Rosser proof from a paper by Masako Takahashi;
- our formalisation follows with some slight exceptions the one
- done by Randy Pollack and James McKinna from their 1993
- TLCA-paper; the proof is simpler by using an auxiliary
- reduction relation called complete development reduction.
-
- Authors: Mathilde Arnaud and Christian Urban
- *}
+text {* Authors: Mathilde Arnaud and Christian Urban
+
+ The Church-Rosser proof from a paper by Masako Takahashi.
+ This formalisation follows with some very slight exceptions
+ the one given by Randy Pollack in his paper:
+ Polishing Up the Tait-Martin Löf Proof of the
+ Church-Rosser Theorem (1995).
+
+ *}
+
+section {* Lemmas about Capture-Avoiding Substitution *}
+
lemma forget:
assumes asm: "x\<sharp>L"
shows "L[x::=P] = L"
@@ -43,6 +47,14 @@
by (nominal_induct M avoiding: x y N L rule: lam.induct)
(auto simp add: fresh_fact forget)
+lemma subst_rename:
+ assumes a: "c\<sharp>t1"
+ shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
+using a
+by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
+ (auto simp add: calc_atm fresh_atm abs_fresh)
+
+
section {* Beta Reduction *}
inductive2
@@ -58,10 +70,12 @@
nominal_inductive Beta
by (simp_all add: abs_fresh fresh_fact')
+section {* Transitive Closure of Beta *}
+
inductive2
"Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
where
- bs1[intro, simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
+ bs1[intro,simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
| bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^isub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
equivariance Beta_star
@@ -103,6 +117,8 @@
by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
(auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)
+section {* Transitive Closure of One *}
+
inductive2
"One_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
where
@@ -127,33 +143,22 @@
by (nominal_induct avoiding: a rule: One.strong_induct)
(auto simp add: abs_fresh fresh_atm fresh_fact)
-lemma subst_rename:
- assumes a: "c\<sharp>t1"
- shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
-using a
-by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
- (auto simp add: calc_atm fresh_atm abs_fresh)
+section {* Elimination Rules for One *}
lemma one_var:
assumes a: "Var x \<longrightarrow>\<^isub>1 t"
shows "t = Var x"
using a
-by - (ind_cases2 "Var x \<longrightarrow>\<^isub>1 t", simp)
+by (erule_tac One.cases) (simp_all)
lemma one_abs:
- fixes t :: "lam"
- and t':: "lam"
- and a :: "name"
assumes a: "(Lam [a].t)\<longrightarrow>\<^isub>1t'"
shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
- using a
- apply -
- apply(ind_cases2 "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
+using a
+ apply(erule_tac One.cases)
apply(auto simp add: lam.inject alpha)
apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
- apply(rule conjI)
- apply(perm_simp)
- apply(simp add: fresh_left calc_atm)
+ apply(perm_simp add: fresh_left calc_atm)
apply(simp add: One.eqvt)
apply(simp add: one_fresh_preserv)
done
@@ -163,8 +168,7 @@
shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or>
(\<exists>a s s1 s2. t1 = Lam [a].s \<and> a\<sharp>(t2,s2) \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)"
using a
- apply -
- apply(ind_cases2 "App t1 t2 \<longrightarrow>\<^isub>1 t'")
+ apply(erule_tac One.cases)
apply(auto simp add: lam.distinct lam.inject)
done
@@ -173,8 +177,7 @@
shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or>
(\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)"
using a
- apply -
- apply(ind_cases2 "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M")
+ apply(erule_tac One.cases)
apply(simp_all add: lam.inject)
apply(force)
apply(erule conjE)
@@ -201,7 +204,7 @@
apply(simp add: One.eqvt)
done
-text {* complete development reduction *}
+text {* Complete Development Reduction *}
inductive2
cd1 :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ >c _" [80,80]80)
@@ -227,12 +230,9 @@
obtain c::"name" where fs: "c\<sharp>(a,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp,blast)
have eq1: "Lam [a].t1 = Lam [c].([(c,a)]\<bullet>t1)" using fs
by (rule_tac sym, auto simp add: lam.inject alpha fresh_prod fresh_atm)
- have "App (Lam [a].t1) s1 = App (Lam [c].([(c,a)]\<bullet>t1)) s1"
- using eq1 by simp
- also have "\<dots> >c ([(c,a)]\<bullet>t2)[c::=s2]" using fs a b
- by (rule_tac cd1r, simp_all add: cd1.eqvt)
- also have "\<dots> = t2[a::=s2]" using fs
- by (rule_tac subst_rename[symmetric], simp)
+ have "App (Lam [a].t1) s1 = App (Lam [c].([(c,a)]\<bullet>t1)) s1" using eq1 by simp
+ also have "\<dots> >c ([(c,a)]\<bullet>t2)[c::=s2]" using fs a b by (simp_all add: cd1.eqvt)
+ also have "\<dots> = t2[a::=s2]" using fs by (rule_tac subst_rename[symmetric], simp)
finally show "App (Lam [a].t1) s1 >c (t2[a::=s2])" by simp
qed
@@ -242,19 +242,15 @@
and b: "s1 >c s2"
shows "a\<sharp>s2"
using b a
-by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
-
+ by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
lemma cd1_lam:
- fixes c::"'a::fs_name"
assumes a: "Lam [a].t >c t'"
shows "\<exists>s. t'=Lam [a].s \<and> t >c s"
using a
apply -
apply(erule cd1.cases)
-apply(simp_all)
-apply(simp add: lam.inject)
-apply(simp add: alpha)
+apply(simp_all add: lam.inject alpha)
apply(auto)
apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
apply(perm_simp add: fresh_left cd1.eqvt cd1_fresh_preserve)
@@ -289,32 +285,19 @@
assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2"
shows "(Lam [a].t1)\<longrightarrow>\<^isub>\<beta>\<^sup>*(Lam [a].t2)"
using a
-proof induct
- case bs1 thus ?case by simp
-next
- case (bs2 y z)
- thus ?case by (blast dest: b3)
-qed
+by (induct) (blast)+
lemma one_app_congL:
assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2"
shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
using a
-proof induct
- case bs1 thus ?case by simp
-next
- case bs2 thus ?case by (blast dest: b1)
-qed
+by (induct) (blast)+
lemma one_app_congR:
assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2"
shows "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2"
using a
-proof induct
- case bs1 thus ?case by simp
-next
- case bs2 thus ?case by (blast dest: b2)
-qed
+by (induct) (blast)+
lemma one_app_cong:
assumes a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2"
@@ -324,7 +307,7 @@
have "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_app_congL)
moreover
have "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_app_congR)
- ultimately show ?thesis by (rule beta_star_trans)
+ ultimately show "App t1 s1\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" by (rule beta_star_trans)
qed
lemma one_beta_star:
--- a/src/HOL/Nominal/Examples/Compile.thy Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Compile.thy Wed May 02 01:42:23 2007 +0200
@@ -1,6 +1,6 @@
(* $Id$ *)
-(* A challenge suggested by Adam Chlipala *)
+(* The definitions for a challenge suggested by Adam Chlipala *)
theory Compile
imports "../Nominal"
@@ -8,51 +8,58 @@
atom_decl name
-nominal_datatype data = DNat
- | DProd "data" "data"
- | DSum "data" "data"
+nominal_datatype data =
+ DNat
+ | DProd "data" "data"
+ | DSum "data" "data"
-nominal_datatype ty = Data "data"
- | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
+nominal_datatype ty =
+ Data "data"
+ | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
-nominal_datatype trm = Var "name"
- | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
- | App "trm" "trm"
- | Const "nat"
- | Pr "trm" "trm"
- | Fst "trm"
- | Snd "trm"
- | InL "trm"
- | InR "trm"
- | Case "trm" "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"
- ("Case _ of inl _ \<rightarrow> _ | inr _ \<rightarrow> _" [100,100,100,100,100] 100)
+nominal_datatype trm =
+ Var "name"
+ | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
+ | App "trm" "trm"
+ | Const "nat"
+ | Pr "trm" "trm"
+ | Fst "trm"
+ | Snd "trm"
+ | InL "trm"
+ | InR "trm"
+ | Case "trm" "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"
+ ("Case _ of inl _ \<rightarrow> _ | inr _ \<rightarrow> _" [100,100,100,100,100] 100)
nominal_datatype dataI = OneI | NatI
-nominal_datatype tyI = DataI "dataI"
- | ArrowI "tyI" "tyI" ("_\<rightarrow>_" [100,100] 100)
+nominal_datatype tyI =
+ DataI "dataI"
+ | ArrowI "tyI" "tyI" ("_\<rightarrow>_" [100,100] 100)
-nominal_datatype trmI = IVar "name"
- | ILam "\<guillemotleft>name\<guillemotright>trmI" ("ILam [_]._" [100,100] 100)
- | IApp "trmI" "trmI"
- | IUnit
- | INat "nat"
- | ISucc "trmI"
- | IAss "trmI" "trmI" ("_\<mapsto>_" [100,100] 100)
- | IRef "trmI"
- | ISeq "trmI" "trmI" ("_;;_" [100,100] 100)
- | Iif "trmI" "trmI" "trmI"
+nominal_datatype trmI =
+ IVar "name"
+ | ILam "\<guillemotleft>name\<guillemotright>trmI" ("ILam [_]._" [100,100] 100)
+ | IApp "trmI" "trmI"
+ | IUnit
+ | INat "nat"
+ | ISucc "trmI"
+ | IAss "trmI" "trmI" ("_\<mapsto>_" [100,100] 100)
+ | IRef "trmI"
+ | ISeq "trmI" "trmI" ("_;;_" [100,100] 100)
+ | Iif "trmI" "trmI" "trmI"
text {* valid contexts *}
-inductive2 valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
+inductive2
+ valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
where
v1[intro]: "valid []"
| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *)
text {* typing judgements for trms *}
-inductive2 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
+inductive2
+ typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
where
t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>"
| t1[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> \<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : \<tau>2"
@@ -69,7 +76,8 @@
text {* typing judgements for Itrms *}
-inductive2 Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80)
+inductive2
+ Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80)
where
t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>"
| t1[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> I\<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IApp e1 e2 : \<tau>2"
@@ -159,7 +167,8 @@
text {* big-step evaluation for trms *}
-inductive2 big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
+inductive2
+ big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
where
b0[intro]: "Lam [x].e \<Down> Lam [x].e"
| b1[intro]: "\<lbrakk>e1\<Down>Lam [x].e; e2\<Down>e2'; e[x::=e2']\<Down>e'\<rbrakk> \<Longrightarrow> App e1 e2 \<Down> e'"
@@ -172,7 +181,8 @@
| b8[intro]: "\<lbrakk>e\<Down>InL e'; e1[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
| b9[intro]: "\<lbrakk>e\<Down>InR e'; e2[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
-inductive2 Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80)
+inductive2
+ Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80)
where
m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)"
| m1[intro]: "\<lbrakk>(m,e1)I\<Down>(m',ILam [x].e); (m',e2)I\<Down>(m'',e3); (m'',e[x::=e3])I\<Down>(m''',e4)\<rbrakk>
--- a/src/HOL/Nominal/Examples/Crary.thy Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy Wed May 02 01:42:23 2007 +0200
@@ -14,15 +14,17 @@
atom_decl name
-nominal_datatype ty = TBase
- | TUnit
- | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
+nominal_datatype ty =
+ TBase
+ | TUnit
+ | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
-nominal_datatype trm = Unit
- | Var "name"
- | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
- | App "trm" "trm"
- | Const "nat"
+nominal_datatype trm =
+ Unit
+ | Var "name"
+ | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
+ | App "trm" "trm"
+ | Const "nat"
types Ctxt = "(name\<times>ty) list"
types Subst = "(name\<times>trm) list"
--- a/src/HOL/Nominal/Examples/Height.thy Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy Wed May 02 01:42:23 2007 +0200
@@ -8,9 +8,10 @@
atom_decl name
-nominal_datatype lam = Var "name"
- | App "lam" "lam"
- | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+nominal_datatype lam =
+ Var "name"
+ | App "lam" "lam"
+ | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
text {* definition of the height-function on lambda-terms *}
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy Wed May 02 01:42:23 2007 +0200
@@ -6,9 +6,10 @@
atom_decl name
-nominal_datatype lam = Var "name"
- | App "lam" "lam"
- | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+nominal_datatype lam =
+ Var "name"
+ | App "lam" "lam"
+ | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
text {* depth of a lambda-term *}
--- a/src/HOL/Nominal/Examples/Lambda_mu.thy Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Lambda_mu.thy Wed May 02 01:42:23 2007 +0200
@@ -8,10 +8,11 @@
atom_decl var mvar
-nominal_datatype trm = Var "var"
- | Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
- | App "trm" "trm"
- | Pss "mvar" "trm"
- | Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100)
+nominal_datatype trm =
+ Var "var"
+ | Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
+ | App "trm" "trm"
+ | Pss "mvar" "trm"
+ | Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100)
end
--- a/src/HOL/Nominal/Nominal.thy Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Wed May 02 01:42:23 2007 +0200
@@ -31,7 +31,7 @@
(* permutation on sets *)
defs (unchecked overloaded)
- perm_set_def: "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"
+ perm_set_def: "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>x | x. x\<in>X}"
lemma empty_eqvt:
shows "pi\<bullet>{} = {}"
@@ -50,7 +50,7 @@
"pi\<bullet>() = ()"
primrec (unchecked perm_prod)
- "pi\<bullet>(a,b) = (pi\<bullet>a,pi\<bullet>b)"
+ "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
lemma fst_eqvt:
"pi\<bullet>(fst x) = fst (pi\<bullet>x)"
@@ -1171,7 +1171,7 @@
and y :: "'a"
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
- shows "pi \<bullet> (x=y) = (pi\<bullet>x = pi\<bullet>y)"
+ shows "pi\<bullet>(x=y) = (pi\<bullet>x = pi\<bullet>y)"
using assms
by (auto simp add: pt_bij perm_bool)
@@ -1309,9 +1309,18 @@
and pi::"'x prm"
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
- shows "pi \<bullet> (X - Y) = (pi \<bullet> X) - (pi \<bullet> Y)"
+ shows "pi\<bullet>(X - Y) = (pi\<bullet>X) - (pi\<bullet>Y)"
by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
+lemma pt_Collect_eqvt:
+ fixes pi::"'x prm"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
+apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at])
+apply(rule_tac x="(rev pi)\<bullet>x" in exI)
+apply(simp add: pt_pi_rev[OF pt, OF at])
+done
-- "some helper lemmas for the pt_perm_supp_ineq lemma"
lemma Collect_permI:
@@ -1596,15 +1605,15 @@
and x :: "'y"
assumes pt: "pt TYPE('y) TYPE('x)"
and at: "at TYPE('x)"
- and h1: "a \<sharp> pi"
- and h2: "a \<sharp> x"
- shows "a \<sharp> (pi \<bullet> x)"
+ and h1: "a\<sharp>pi"
+ and h2: "a\<sharp>x"
+ shows "a\<sharp>(pi\<bullet>x)"
using assms
proof -
- have "a \<sharp> rev pi"using h1 by (simp add: fresh_list_rev)
- then have "(rev pi) \<bullet> a = a" by (simp add: at_prm_fresh[OF at])
- then have "((rev pi) \<bullet> a) \<sharp> x" using h2 by simp
- thus "a \<sharp> (pi \<bullet> x)" by (simp add: pt_fresh_right[OF pt, OF at])
+ have "a\<sharp>(rev pi)"using h1 by (simp add: fresh_list_rev)
+ then have "(rev pi)\<bullet>a = a" by (simp add: at_prm_fresh[OF at])
+ then have "((rev pi)\<bullet>a)\<sharp>x" using h2 by simp
+ thus "a\<sharp>(pi\<bullet>x)" by (simp add: pt_fresh_right[OF pt, OF at])
qed
lemma pt_fresh_perm_app_ineq:
@@ -2127,11 +2136,11 @@
case goal1
show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
apply(auto simp add: perm_set_def)
- apply(rule_tac x="pi\<bullet>xa" in exI)
+ apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule conjI)
- apply(rule_tac x="xa" in exI)
+ apply(rule_tac x="xb" in exI)
apply(simp)
- apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xa) = pi\<bullet>(f xa)")(*A*)
+ apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xb) = pi\<bullet>(f xb)")(*A*)
apply(simp)
apply(rule pt_set_bij2[OF pt_x, OF at])
apply(assumption)
@@ -2146,7 +2155,7 @@
apply(rule_tac x="(rev pi)\<bullet>x" in exI)
apply(rule conjI)
apply(simp add: pt_pi_rev[OF pt_x, OF at])
- apply(rule_tac x="a" in bexI)
+ apply(rule_tac x="xb" in bexI)
apply(simp add: pt_set_bij1[OF pt_x, OF at])
apply(simp add: pt_fun_app_eq[OF pt, OF at])
apply(assumption)
@@ -2177,7 +2186,7 @@
apply(erule conjE)
apply(simp add: perm_set_def)
apply(auto)
- apply(subgoal_tac "[(a,b)]\<bullet>aa = aa")(*A*)
+ apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")(*A*)
apply(simp)
apply(rule pt_fresh_fresh[OF pt, OF at])
apply(force)
@@ -2351,7 +2360,7 @@
apply(simp add: cp_def)
apply(auto)
apply(auto simp add: perm_set_def)
-apply(rule_tac x="pi2\<bullet>aa" in exI)
+apply(rule_tac x="pi2\<bullet>xc" in exI)
apply(auto)
done