Skip to content

Commit 2be7142

Browse files
jvanbrueggejvanbruegge
committed
Adjust substitution functions
1 parent 688181d commit 2be7142

File tree

2 files changed

+186
-36
lines changed

2 files changed

+186
-36
lines changed

‎Defs.thy‎

Lines changed: 170 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -35,9 +35,10 @@ nominal_function head_ctor :: "term \<Rightarrow> bool" where
3535
| "head_ctor (TApp e _) = head_ctor e"
3636
| "head_ctor (Ctor _) = True"
3737
| "head_ctor (Let _ _ _ _) = False"
38+
| "head_ctor (Case _ _) = False"
3839
proof goal_cases
3940
case (3 P x)
40-
then show ?case by (cases x rule: term.exhaust)
41+
then show ?case by (cases x rule: term_alt_list_alt.exhaust(1))
4142
qed (auto simp: eqvt_def head_ctor_graph_aux_def)
4243
nominal_termination (eqvt) by lexicographic_order
4344

@@ -49,44 +50,111 @@ nominal_function is_value :: "term => bool" where
4950
| "is_value (TApp e \<tau>) = head_ctor e"
5051
| "is_value (Ctor _) = True"
5152
| "is_value (Let x \<tau> e1 e2) = False"
53+
| "is_value (Case _ _) = False"
5254
proof goal_cases
5355
case (3 P x)
54-
then show ?case by (cases x rule: term.exhaust)
56+
then show ?case by (cases x rule: term_alt_list_alt.exhaust(1))
5557
next
56-
case (17 a k e a' k' e')
58+
case (19 a k e a' k' e')
5759
obtain c::tyvar where c: "atom c \<sharp> (a, e, a', e')" by (rule obtain_fresh)
5860
have 1: "is_value_sumC e' = (a' \<leftrightarrow> c) \<bullet> is_value_sumC e'" using permute_boolE permute_boolI by blast
5961
have 2: "is_value_sumC e = (a \<leftrightarrow> c) \<bullet> is_value_sumC e" using permute_boolE permute_boolI by blast
60-
from c have "(a \<leftrightarrow> c) \<bullet> e = (a' \<leftrightarrow> c) \<bullet> e'" using 17(5) by simp
61-
then show ?case using 1 2 17(1,2) eqvt_at_def by metis
62+
from c have "(a \<leftrightarrow> c) \<bullet> e = (a' \<leftrightarrow> c) \<bullet> e'" using 19(5) by simp
63+
then show ?case using 1 2 19(1,2) eqvt_at_def by metis
6264
qed (auto simp: eqvt_def is_value_graph_aux_def)
6365
nominal_termination (eqvt) by lexicographic_order
6466

65-
nominal_function subst_term :: "term => term \<Rightarrow> var => term" where
67+
nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
68+
subst_term :: "term => term \<Rightarrow> var => term" and
69+
subst_alt_list :: "alt_list \<Rightarrow> term \<Rightarrow> var \<Rightarrow> alt_list" and
70+
subst_alt :: "alt \<Rightarrow> term \<Rightarrow> var \<Rightarrow> alt" where
71+
6672
"subst_term (Var y) e x = (if x = y then e else Var y)"
6773
| "subst_term (App e1 e2) e x = App (subst_term e1 e x) (subst_term e2 e x)"
6874
| "subst_term (TApp e1 \<tau>) e x = TApp (subst_term e1 e x) \<tau>"
6975
| "subst_term (Ctor D) _ _ = Ctor D"
76+
| "subst_term (Case t alts) e x = Case (subst_term t e x) (subst_alt_list alts e x)"
7077
| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (\<lambda> y:\<tau>. e2) e x = (\<lambda> y:\<tau>. subst_term e2 e x)"
7178
| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (\<Lambda> y:k. e2) e x = (\<Lambda> y:k. subst_term e2 e x)"
7279
| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (Let y \<tau> e1 e2) e x = Let y \<tau> (subst_term e1 e x) (subst_term e2 e x)"
80+
81+
| "subst_alt_list ANil _ _ = ANil"
82+
| "subst_alt_list (ACons alt alts) e x = ACons (subst_alt alt e x) (subst_alt_list alts e x)"
83+
84+
| "atom y \<sharp> (e, x) \<Longrightarrow> subst_alt (MatchVar y t) e x = MatchVar y (subst_term t e x)"
85+
| "set (map atom tys @ map atom vals) \<sharp>* (e, x) \<Longrightarrow> subst_alt (MatchCtor D tys vals t) e x = MatchCtor D tys vals (subst_term t e x)"
7386
proof (goal_cases)
74-
case (3 P x)
75-
then obtain t e y where P: "x = (t, e, y)" by (metis prod.exhaust)
87+
88+
(* this is adapted and simplified from here: https://www.joachim-breitner.de/thesis/isa/Substitution.thy *)
89+
have eqvt_at_term: "\<And>e y z . eqvt_at subst_term_subst_alt_list_subst_alt_sumC (Inl (e, y, z)) \<Longrightarrow> eqvt_at (\<lambda>(a, b, c). subst_term a b c) (e, y, z)"
90+
apply (simp add: eqvt_at_def subst_term_def)
91+
apply rule
92+
apply (subst Projl_permute)
93+
apply (simp add: subst_term_subst_alt_list_subst_alt_sumC_def)
94+
apply (simp add: THE_default_def)
95+
apply (case_tac "Ex1 (subst_term_subst_alt_list_subst_alt_graph (Inl (e, y, z)))")
96+
apply(auto)[2]
97+
apply (erule_tac x="x" in allE)
98+
apply simp
99+
apply(cases rule: subst_term_subst_alt_list_subst_alt_graph.cases)
100+
apply(assumption)
101+
apply blast+
102+
apply simp
103+
done
104+
105+
{ case (3 P x)
76106
then show ?case
77-
apply (cases t rule: term.strong_exhaust[of _ _ "(e, y)"])
78-
apply (auto simp: 3)
79-
using 3(5-7) P fresh_star_def by blast+
107+
proof (cases x)
108+
case (Inl a)
109+
then obtain t e y where P: "a = (t, e, y)" by (metis prod.exhaust)
110+
then show ?thesis using 3(1-5) Inl
111+
proof (cases t rule: term_alt_list_alt.strong_exhaust(1)[of _ _ "(e, y)"])
112+
case Lam
113+
then show ?thesis using 3(6) Inl P fresh_star_insert by blast
114+
next
115+
case TyLam
116+
then show ?thesis using 3(7) Inl P fresh_star_insert by blast
117+
next
118+
case Let
119+
then show ?thesis using 3(8) Inl P fresh_star_insert by blast
120+
qed auto
121+
next
122+
case outer: (Inr b)
123+
then show ?thesis
124+
proof (cases b)
125+
case (Inl a)
126+
then obtain xs e y where "a = (xs, e, y)" by (metis prod.exhaust)
127+
then show ?thesis using 3(9,10) Inl outer by (cases xs rule: term_alt_list_alt.exhaust(2)) auto
128+
next
129+
case (Inr c)
130+
then obtain m e y where "c = (m, e, y)" by (metis prod.exhaust)
131+
then show ?thesis using 3(11,12) Inr outer fresh_star_insert
132+
apply (cases m rule: term_alt_list_alt.strong_exhaust(3)[of "(e, y)"])
133+
apply auto
134+
by blast
135+
qed
136+
qed
80137
next
81-
case (26 y e x \<tau> e2 y' e' x' \<tau>' e2')
82-
then show ?case using Abs_sumC[OF 26(5,6,1,2)] by fastforce
138+
case (54 y e x \<tau> e2 y' e' x' \<tau>' e2')
139+
have "(\<lambda> y : \<tau> . subst_term e2 e x) = (\<lambda> y' : \<tau>' . subst_term e2' e' x')" using Abs_sumC[OF 54(5,6) eqvt_at_term[OF 54(1)] eqvt_at_term[OF 54(2)]] 54(7) by fastforce
140+
then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
83141
next
84-
case (29 y e x k e2 y' e' x' k' e2')
85-
then show ?case using Abs_sumC[OF 29(5,6,1,2)] by fastforce
142+
case (61 y e x k e2 y' e' x' k' e2')
143+
have "(\<Lambda> y : k . subst_term e2 e x) = (\<Lambda> y' : k' . subst_term e2' e' x')" using Abs_sumC[OF 61(5,6) eqvt_at_term[OF 61(1)] eqvt_at_term[OF 61(2)]] 61(7) by fastforce
144+
then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
86145
next
87-
case (31 y e x \<tau> e1 e2 y' e' x' \<tau>' e1' e2')
88-
then show ?case using Abs_sumC[OF 31(9,10,2,4)] by fastforce
89-
qed (auto simp: eqvt_def subst_term_graph_aux_def)
146+
case (67 y e x \<tau> e1 e2 y' e' x' \<tau>' e1' e2')
147+
have "Let y \<tau> (subst_term e1 e x) (subst_term e2 e x) = Let y' \<tau>' (subst_term e1' e' x') (subst_term e2' e' x')" using Abs_sumC[OF 67(9,10) eqvt_at_term[OF 67(2)] eqvt_at_term[OF 67(4)]] 67(11) by fastforce
148+
then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
149+
next
150+
case (79 y e x t y' e' x' t')
151+
have "MatchVar y (subst_term t e x) = MatchVar y' (subst_term t' e' x')" using Abs_sumC[OF 79(5,6) eqvt_at_term[OF 79(1)] eqvt_at_term[OF 79(2)]] 79(7) by fastforce
152+
then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
153+
next
154+
case (81 tys vals e x D t tys' vals' e' x' D' t')
155+
have "MatchCtor D tys vals (subst_term t e x) = MatchCtor D' tys' vals' (subst_term t' e' x')" using Abs_sumC_star[OF 81(5,6) eqvt_at_term[OF 81(1)] eqvt_at_term[OF 81(2)]] 81(7) by fastforce
156+
then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
157+
} qed (auto simp: eqvt_def subst_term_subst_alt_list_subst_alt_graph_aux_def)
90158
nominal_termination (eqvt) by lexicographic_order
91159

92160
nominal_function subst_type :: "\<tau> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<tau>" where
@@ -98,41 +166,107 @@ nominal_function subst_type :: "\<tau> \<Rightarrow> \<tau> \<Rightarrow> tyvar
98166
proof goal_cases
99167
case (3 P x)
100168
then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
101-
then show ?case
102-
apply (cases t rule: \<tau>.strong_exhaust[of _ _ "(\<tau>, a)"])
103-
apply (auto simp: 3)
104-
using 3(5) P fresh_star_def by blast
169+
then show ?case proof(cases t rule: \<tau>.strong_exhaust[of _ _ "(\<tau>, a)"])
170+
case (TyForall x51 x52 x53)
171+
then show ?thesis using 3(5) P fresh_star_def by blast
172+
qed (auto simp: 3)
105173
next
106174
case (18 b \<tau> a k \<sigma> b' \<tau>' a' k' \<sigma>')
107175
then show ?case using Abs_sumC[OF 18(5,6,1,2)] by fastforce
108176
qed (auto simp: eqvt_def subst_type_graph_aux_def)
109177
nominal_termination (eqvt) by lexicographic_order
110178

111-
nominal_function subst_term_type :: "term \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> term" where
179+
nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
180+
subst_term_type :: "term \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> term" and
181+
subst_alt_list_type :: "alt_list \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> alt_list" and
182+
subst_alt_type :: "alt \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> alt" where
183+
112184
"subst_term_type (Var x) _ _ = Var x"
113185
| "subst_term_type (Ctor D) _ _ = Ctor D"
114186
| "subst_term_type (App e1 e2) \<tau> a = App (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a)"
115187
| "subst_term_type (TApp e \<tau>2) \<tau> a = TApp (subst_term_type e \<tau> a) (subst_type \<tau>2 \<tau> a)"
188+
| "subst_term_type (Case e alts) \<tau> a = Case (subst_term_type e \<tau> a) (subst_alt_list_type alts \<tau> a)"
116189
| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<lambda> y:\<tau>'. e2) \<tau> a = (\<lambda> y:(subst_type \<tau>' \<tau> a). subst_term_type e2 \<tau> a)"
117190
| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<Lambda> b:k. e2) \<tau> a = (\<Lambda> b:k. subst_term_type e2 \<tau> a)"
118191
| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (Let y \<tau>' e1 e2) \<tau> a = Let y (subst_type \<tau>' \<tau> a) (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a)"
192+
193+
| "subst_alt_list_type ANil _ _ = ANil"
194+
| "subst_alt_list_type (ACons alt alts) \<tau> a = ACons (subst_alt_type alt \<tau> a) (subst_alt_list_type alts \<tau> a)"
195+
196+
| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_alt_type (MatchVar y e) \<tau> a = MatchVar y (subst_term_type e \<tau> a)"
197+
| "set (map atom tys @ map atom vals) \<sharp>* (\<tau>, a) \<Longrightarrow> subst_alt_type (MatchCtor D tys vals e) \<tau> a = MatchCtor D tys vals (subst_term_type e \<tau> a)"
119198
proof goal_cases
120-
case (3 P x)
121-
then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
199+
200+
(* this is adapted and simplified from here: https://www.joachim-breitner.de/thesis/isa/Substitution.thy *)
201+
have eqvt_at_term: "\<And>e y z . eqvt_at subst_term_type_subst_alt_list_type_subst_alt_type_sumC (Inl (e, y, z)) \<Longrightarrow> eqvt_at (\<lambda>(a, b, c). subst_term_type a b c) (e, y, z)"
202+
apply (simp add: eqvt_at_def subst_term_type_def)
203+
apply rule
204+
apply (subst Projl_permute)
205+
apply (simp add: subst_term_type_subst_alt_list_type_subst_alt_type_sumC_def)
206+
apply (simp add: THE_default_def)
207+
apply (case_tac "Ex1 (subst_term_type_subst_alt_list_type_subst_alt_type_graph (Inl (e, y, z)))")
208+
apply(auto)[2]
209+
apply (erule_tac x="x" in allE)
210+
apply simp
211+
apply(cases rule: subst_term_type_subst_alt_list_type_subst_alt_type_graph.cases)
212+
apply(assumption)
213+
apply blast+
214+
apply simp
215+
done
216+
217+
{ case (3 P x)
122218
then show ?case
123-
apply (cases t rule: term.strong_exhaust[of _ _ "(\<tau>, a)"])
124-
using 3 P apply auto[4]
125-
using 3(5,6,7) P fresh_star_def by blast+
219+
proof (cases x)
220+
case (Inl a)
221+
then obtain t e y where P: "a = (t, e, y)" by (metis prod.exhaust)
222+
then show ?thesis using 3(1-5) Inl
223+
proof (cases t rule: term_alt_list_alt.strong_exhaust(1)[of _ _ "(e, y)"])
224+
case Lam
225+
then show ?thesis using 3(6) Inl P fresh_star_insert by blast
226+
next
227+
case TyLam
228+
then show ?thesis using 3(7) Inl P fresh_star_insert by blast
229+
next
230+
case Let
231+
then show ?thesis using 3(8) Inl P fresh_star_insert by blast
232+
qed auto
233+
next
234+
case outer: (Inr b)
235+
then show ?thesis
236+
proof (cases b)
237+
case (Inl a)
238+
then obtain xs e y where "a = (xs, e, y)" by (metis prod.exhaust)
239+
then show ?thesis using 3(9,10) Inl outer by (cases xs rule: term_alt_list_alt.exhaust(2)) auto
240+
next
241+
case (Inr c)
242+
then obtain m e y where P: "c = (m, e, y)" by (metis prod.exhaust)
243+
then show ?thesis using Inr outer 3(11,12)
244+
apply (cases m rule: term_alt_list_alt.strong_exhaust(3)[of "(e, y)"]) apply simp
245+
using fresh_star_insert by blast
246+
qed
247+
qed
248+
next
249+
case (54 y \<tau> a \<tau>2 e2 y' \<tau>' a' \<tau>2' e2')
250+
have "(\<lambda> y : subst_type \<tau>2 \<tau> a . subst_term_type e2 \<tau> a) = (\<lambda> y' : subst_type \<tau>2' \<tau>' a' . subst_term_type e2' \<tau>' a')" using Abs_sumC[OF 54(5,6) eqvt_at_term[OF 54(1)] eqvt_at_term[OF 54(2)]] 54(7) by fastforce
251+
then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
252+
next
253+
case (61 b \<tau> a k e2 b' \<tau>' a' k' e2')
254+
have "(\<Lambda> b : k . subst_term_type e2 \<tau> a) = (\<Lambda> b' : k' . subst_term_type e2' \<tau>' a')" using Abs_sumC[OF 61(5,6) eqvt_at_term[OF 61(1)] eqvt_at_term[OF 61(2)]] 61(7) by fastforce
255+
then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
126256
next
127-
case (26 y \<tau> a \<tau>1 e2 y' \<tau>' a' \<tau>1' e2')
128-
then show ?case using Abs_sumC[OF 26(5,6,1,2)] by fastforce
257+
case (67 y \<tau> a \<tau>2 e1 e2 y' \<tau>' a' \<tau>2' e1' e2')
258+
have "Let y (subst_type \<tau>2 \<tau> a) (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a) = Let y' (subst_type \<tau>2' \<tau>' a') (subst_term_type e1' \<tau>' a') (subst_term_type e2' \<tau>' a')"
259+
using Abs_sumC[OF 67(9,10) eqvt_at_term[OF 67(2)] eqvt_at_term[OF 67(4)]] 67(11) by fastforce
260+
then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
129261
next
130-
case (29 b \<tau> a k e2 b' \<tau>' a' k' e2')
131-
then show ?case using Abs_sumC[OF 29(5,6,1,2)] by fastforce
262+
case (79 y \<tau> a e y' \<tau>' a' e')
263+
have "MatchVar y (subst_term_type e \<tau> a) = MatchVar y' (subst_term_type e' \<tau>' a')" using Abs_sumC[OF 79(5,6) eqvt_at_term[OF 79(1)] eqvt_at_term[OF 79(2)]] 79(7) by fastforce
264+
then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
132265
next
133-
case (31 y \<tau> a \<tau>1 e1 e2 y' \<tau>' a' \<tau>1' e1' e2')
134-
then show ?case using Abs_sumC[OF 31(9,10,2,4)] by fastforce
135-
qed (auto simp: eqvt_def subst_term_type_graph_aux_def)
266+
case (81 tys vals \<tau> a D e tys' vals' \<tau>' a' D' e')
267+
have "MatchCtor D tys vals (subst_term_type e \<tau> a) = MatchCtor D' tys' vals' (subst_term_type e' \<tau>' a')" using Abs_sumC_star[OF 81(5,6) eqvt_at_term[OF 81(1)] eqvt_at_term[OF 81(2)]] 81(7) by fastforce
268+
then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
269+
} qed (auto simp: eqvt_def subst_term_type_subst_alt_list_type_subst_alt_type_graph_aux_def)
136270
nominal_termination (eqvt) by lexicographic_order
137271

138272
nominal_function subst_context :: "\<Gamma> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<Gamma>" where
@@ -154,6 +288,6 @@ no_notation inverse_divide (infixl "'/" 70)
154288
consts subst :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" ("_[_'/_]" [1000,0,0] 1000)
155289

156290
adhoc_overloading
157-
subst subst_term subst_type subst_term_type subst_context
291+
subst subst_term subst_alt_list subst_alt subst_type subst_term_type subst_alt_list_type subst_alt_type subst_context
158292

159293
end

‎Nominal2_Lemmas.thy‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,19 @@ proof -
6262
show ?thesis using 1 2 3 equal by argo
6363
qed
6464

65+
lemma Abs_sumC_star:
66+
fixes ys ys'::"atom list" and x x'::"'a::fs" and e e'::"'b::fs" and e2 e2'::"'c::fs" and f::"'c * 'b * 'a \<Rightarrow> 'd::fs"
67+
assumes fresh: "set ys \<sharp>* (e, x)" "set ys' \<sharp>* (e', x')"
68+
and eqvt_at: "eqvt_at f (e2, e, x)" "eqvt_at f (e2', e', x')"
69+
and equal: "[ys]lst. e2 = [ys']lst. e2'" "x = x'" "e = e'"
70+
shows "[ys]lst. f (e2, e, x) = [ys']lst. f (e2', e', x')"
71+
proof -
72+
have 1: "set ys \<sharp>* ([ys]lst. f (e2, e, x))" by (simp add: Abs_fresh_star(3))
73+
have 2: "\<And>p. supp p \<sharp>* (e, x) \<Longrightarrow> p \<bullet> ([ys]lst. f (e2, e, x)) = [p \<bullet> ys]lst. f (p \<bullet> e2, e, x)" using eqvt_at(1) by (simp add: eqvt_at_def, simp add: fresh_star_Pair perm_supp_eq)
74+
have 3: "\<And>p. supp p \<sharp>* (e, x) \<Longrightarrow> p \<bullet> ([ys']lst. f (e2', e, x)) = [p \<bullet> ys']lst. f (p \<bullet> e2', e, x)" using eqvt_at(2) equal(2,3) by (simp add: eqvt_at_def, simp add: fresh_star_Pair perm_supp_eq)
75+
show ?thesis using Abs_lst_fcb2[where f="\<lambda>a b c. [a]lst. f (b, e, x)", OF equal(1) 1 fresh(1) _ 2 3] fresh(2) equal(2,3) by simp
76+
qed
77+
6578
lemma Abs_fresh_var:
6679
fixes y::"'a::at" and e ::"'b::fs"
6780
obtains c::"'a" and e'::"'b" where "([[atom y]]lst. e = [[atom c]]lst. e') \<and> atom y \<sharp> [[atom c]]lst. e'"
@@ -79,4 +92,7 @@ lemma Abs_rename_body:
7992
shows "(a \<leftrightarrow> b) \<bullet> e1 = e2"
8093
by (metis Abs1_eq_iff'(3) Nominal2_Base.swap_self assms flip_commute flip_def fresh_star_zero supp_perm_eq_test)
8194

95+
lemma Projl_permute: "\<exists>y. f = Inl y \<Longrightarrow> p \<bullet> projl f = projl (p \<bullet> f)" by auto
96+
lemma Projr_permute: "\<exists>y. f = Inr y \<Longrightarrow> p \<bullet> projr f = projr (p \<bullet> f)" by auto
97+
8298
end

0 commit comments

Comments
 (0)