1 (* Theory be Kirstin Peters *) |
|
2 |
|
3 theory Pi |
|
4 imports "../Nominal2" |
|
5 begin |
|
6 |
|
7 atom_decl name |
|
8 |
|
9 subsection {* Capture-Avoiding Substitution of Names *} |
|
10 |
|
11 definition |
|
12 subst_name :: "name \<Rightarrow> name \<Rightarrow> name \<Rightarrow> name" ("_[_:::=_]" [110, 110, 110] 110) |
|
13 where |
|
14 "a[b:::=c] \<equiv> if (a = b) then c else a" |
|
15 |
|
16 declare subst_name_def[simp] |
|
17 |
|
18 lemma subst_name_mix_eqvt[eqvt]: |
|
19 fixes p :: perm |
|
20 and a :: name |
|
21 and b :: name |
|
22 and c :: name |
|
23 |
|
24 shows "p \<bullet> (a[b:::=c]) = (p \<bullet> a)[(p \<bullet> b):::=(p \<bullet> c)]" |
|
25 proof - |
|
26 show ?thesis |
|
27 by(auto) |
|
28 qed |
|
29 |
|
30 nominal_primrec |
|
31 subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name" |
|
32 where |
|
33 "subst_name_list a [] = a" |
|
34 | "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))" |
|
35 apply(simp add: eqvt_def subst_name_list_graph_aux_def) |
|
36 apply(simp) |
|
37 apply(auto) |
|
38 apply(rule_tac y="b" in list.exhaust) |
|
39 by(auto) |
|
40 |
|
41 termination (eqvt) |
|
42 by (lexicographic_order) |
|
43 |
|
44 |
|
45 section {* The Synchronous Pi-Calculus *} |
|
46 |
|
47 subsection {* Syntax: Synchronous, Monadic Pi-Calculus with n-ary, Mixed Choice *} |
|
48 |
|
49 nominal_datatype |
|
50 guardedTerm_mix = Output name name piMix ("_!<_>\<onesuperior>._" [120, 120, 110] 110) |
|
51 | Input name b::name P::piMix binds b in P ("_?<_>\<onesuperior>._" [120, 120, 110] 110) |
|
52 | Tau piMix ("<\<tau>\<onesuperior>>._" [110] 110) |
|
53 and sumList_mix = SumNil ("\<zero>\<onesuperior>") |
|
54 | AddSummand guardedTerm_mix sumList_mix (infixr "\<oplus>\<onesuperior>" 65) |
|
55 and piMix = Res a::name P::piMix binds a in P ("<\<nu>_>\<onesuperior>_" [100, 100] 100) |
|
56 | Par piMix piMix (infixr "\<parallel>\<onesuperior>" 85) |
|
57 | Match name name piMix ("[_\<frown>\<onesuperior>_]_" [120, 120, 110] 110) |
|
58 | Sum sumList_mix ("\<oplus>\<onesuperior>{_}" 90) |
|
59 | Rep name b::name P::piMix binds b in P ("\<infinity>_?<_>\<onesuperior>._" [120, 120, 110] 110) |
|
60 | Succ ("succ\<onesuperior>") |
|
61 |
|
62 lemmas piMix_strong_induct = guardedTerm_mix_sumList_mix_piMix.strong_induct |
|
63 lemmas piMix_fresh = guardedTerm_mix_sumList_mix_piMix.fresh |
|
64 lemmas piMix_eq_iff = guardedTerm_mix_sumList_mix_piMix.eq_iff |
|
65 lemmas piMix_distinct = guardedTerm_mix_sumList_mix_piMix.distinct |
|
66 lemmas piMix_size = guardedTerm_mix_sumList_mix_piMix.size |
|
67 |
|
68 subsection {* Alpha-Conversion Lemmata *} |
|
69 |
|
70 lemma alphaRes_mix: |
|
71 fixes a :: name |
|
72 and P :: piMix |
|
73 and z :: name |
|
74 |
|
75 assumes "atom z \<sharp> P" |
|
76 |
|
77 shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>((atom a \<rightleftharpoons> atom z) \<bullet> P)" |
|
78 proof(cases "a = z") |
|
79 assume "a = z" |
|
80 thus ?thesis |
|
81 by(simp) |
|
82 next |
|
83 assume "a \<noteq> z" |
|
84 thus ?thesis |
|
85 using assms |
|
86 by (simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left) |
|
87 qed |
|
88 |
|
89 lemma alphaInput_mix: |
|
90 fixes a :: name |
|
91 and b :: name |
|
92 and P :: piMix |
|
93 and z :: name |
|
94 |
|
95 assumes "atom z \<sharp> P" |
|
96 |
|
97 shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)" |
|
98 proof(cases "b = z") |
|
99 assume "b = z" |
|
100 thus ?thesis |
|
101 by(simp) |
|
102 next |
|
103 assume "b \<noteq> z" |
|
104 thus ?thesis |
|
105 using assms |
|
106 by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left) |
|
107 qed |
|
108 |
|
109 lemma alphaRep_mix: |
|
110 fixes a :: name |
|
111 and b :: name |
|
112 and P :: piMix |
|
113 and z :: name |
|
114 |
|
115 assumes "atom z \<sharp> P" |
|
116 |
|
117 shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)" |
|
118 proof(cases "b = z") |
|
119 assume "b = z" |
|
120 thus ?thesis |
|
121 by(simp) |
|
122 next |
|
123 assume "b \<noteq> z" |
|
124 thus ?thesis |
|
125 using assms |
|
126 by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left) |
|
127 qed |
|
128 |
|
129 subsection {* Capture-Avoiding Substitution of Names *} |
|
130 |
|
131 lemma testl: |
|
132 assumes a: "\<exists>y. f = Inl y" |
|
133 shows "(p \<bullet> (Sum_Type.Projl f)) = Sum_Type.Projl (p \<bullet> f)" |
|
134 using a by auto |
|
135 |
|
136 lemma testrr: |
|
137 assumes a: "\<exists>y. f = Inr (Inr y)" |
|
138 shows "(p \<bullet> (Sum_Type.Projr (Sum_Type.Projr f))) = Sum_Type.Projr (Sum_Type.Projr (p \<bullet> f))" |
|
139 using a by auto |
|
140 |
|
141 lemma testlr: |
|
142 assumes a: "\<exists>y. f = Inr (Inl y)" |
|
143 shows "(p \<bullet> (Sum_Type.Projl (Sum_Type.Projr f))) = Sum_Type.Projl (Sum_Type.Projr (p \<bullet> f))" |
|
144 using a by auto |
|
145 |
|
146 nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (sum_case (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))") |
|
147 subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix" ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and |
|
148 subsList_mix :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix" ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and |
|
149 subs_mix :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix" ("_[_::=\<onesuperior>_]" [100, 100, 100] 100) |
|
150 where |
|
151 "(a!<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])!<(b[x:::=y])>\<onesuperior>.(P[x::=\<onesuperior>y])" |
|
152 | "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (a?<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])" |
|
153 | "(<\<tau>\<onesuperior>>.P)[x::=\<onesuperior>\<onesuperior>y] = <\<tau>\<onesuperior>>.(P[x::=\<onesuperior>y])" |
|
154 | "(\<zero>\<onesuperior>)[x::=\<onesuperior>\<twosuperior>y] = \<zero>\<onesuperior>" |
|
155 | "(g \<oplus>\<onesuperior> xg)[x::=\<onesuperior>\<twosuperior>y] = (g[x::=\<onesuperior>\<onesuperior>y]) \<oplus>\<onesuperior> (xg[x::=\<onesuperior>\<twosuperior>y])" |
|
156 | "\<lbrakk>atom a \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (<\<nu>a>\<onesuperior>P)[x::=\<onesuperior>y] = <\<nu>a>\<onesuperior>(P[x::=\<onesuperior>y])" |
|
157 | "(P \<parallel>\<onesuperior> Q)[x::=\<onesuperior>y] = (P[x::=\<onesuperior>y]) \<parallel>\<onesuperior> (Q[x::=\<onesuperior>y])" |
|
158 | "([a\<frown>\<onesuperior>b]P)[x::=\<onesuperior>y] = ([(a[x:::=y])\<frown>\<onesuperior>(b[x:::=y])](P[x::=\<onesuperior>y]))" |
|
159 | "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}" |
|
160 | "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])" |
|
161 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>" |
|
162 using [[simproc del: alpha_lst]] |
|
163 apply(auto simp add: piMix_distinct piMix_eq_iff) |
|
164 apply(simp add: eqvt_def subsGuard_mix_subsList_mix_subs_mix_graph_aux_def) |
|
165 --"Covered all cases" |
|
166 apply(case_tac x) |
|
167 apply(simp) |
|
168 apply(case_tac a) |
|
169 apply(simp) |
|
170 apply (rule_tac y="aa" and c="(b, c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(1)) |
|
171 apply(blast) |
|
172 apply(auto simp add: fresh_star_def)[1] |
|
173 apply(blast) |
|
174 apply(simp) |
|
175 apply(blast) |
|
176 apply(simp) |
|
177 apply(case_tac b) |
|
178 apply(simp) |
|
179 apply(case_tac a) |
|
180 apply(simp) |
|
181 apply (rule_tac ya="aa" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(2)) |
|
182 apply(blast) |
|
183 apply(blast) |
|
184 apply(simp) |
|
185 apply(case_tac ba) |
|
186 apply(simp) |
|
187 apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3)) |
|
188 using [[simproc del: alpha_lst]] |
|
189 apply(auto simp add: fresh_star_def)[1] |
|
190 apply(blast) |
|
191 apply(blast) |
|
192 apply(blast) |
|
193 using [[simproc del: alpha_lst]] |
|
194 apply(auto simp add: fresh_star_def)[1] |
|
195 apply(blast) |
|
196 apply(simp) |
|
197 apply(blast) |
|
198 --"compatibility" |
|
199 apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff]) |
|
200 apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)") |
|
201 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))") |
|
202 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))") |
|
203 prefer 2 |
|
204 apply (simp only: eqvt_at_def subs_mix_def) |
|
205 apply rule |
|
206 apply(simp (no_asm)) |
|
207 apply (subst testrr) |
|
208 apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def) |
|
209 apply (simp add: THE_default_def) |
|
210 apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))") |
|
211 apply simp_all[2] |
|
212 apply auto[1] |
|
213 apply (erule_tac x="x" in allE) |
|
214 apply simp |
|
215 apply (thin_tac "\<forall>p\<Colon>perm. |
|
216 p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) = |
|
217 (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
218 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
|
219 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
220 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
|
221 else Inr (Inr undefined))") |
|
222 apply (thin_tac "\<forall>p\<Colon>perm. |
|
223 p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
224 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
|
225 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
226 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
|
227 else Inr (Inr undefined)) = |
|
228 (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
229 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
|
230 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
231 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
|
232 else Inr (Inr undefined))") |
|
233 apply (thin_tac "atom b \<sharp> (xa, ya)") |
|
234 apply (thin_tac "atom ba \<sharp> (xa, ya)") |
|
235 apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa") |
|
236 apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
237 apply assumption |
|
238 apply (metis Inr_not_Inl) |
|
239 apply (metis Inr_not_Inl) |
|
240 apply (metis Inr_not_Inl) |
|
241 apply (metis Inr_inject Inr_not_Inl) |
|
242 apply (metis Inr_inject Inr_not_Inl) |
|
243 apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr |
|
244 (Sum_Type.Projr |
|
245 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
|
246 apply clarify |
|
247 apply (rule the1_equality) |
|
248 apply blast apply assumption |
|
249 apply (rule_tac x="Sum_Type.Projr |
|
250 (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior> |
|
251 Sum_Type.Projr |
|
252 (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) |
|
253 apply clarify |
|
254 apply (rule the1_equality) |
|
255 apply blast apply assumption |
|
256 apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr |
|
257 (Sum_Type.Projr |
|
258 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
|
259 apply clarify |
|
260 apply (rule the1_equality) |
|
261 apply blast apply assumption |
|
262 apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl |
|
263 (Sum_Type.Projr |
|
264 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI) |
|
265 apply clarify |
|
266 apply (rule the1_equality) |
|
267 apply blast apply assumption |
|
268 apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr |
|
269 (Sum_Type.Projr |
|
270 (subsGuard_mix_subsList_mix_subs_mix_sum |
|
271 (Inr (Inr (Pb, xb, y)))))" in exI) |
|
272 apply clarify |
|
273 apply (rule the1_equality) |
|
274 apply blast apply assumption |
|
275 apply (rule_tac x="succ\<onesuperior>" in exI) |
|
276 apply clarify |
|
277 apply (rule the1_equality) |
|
278 apply blast apply assumption |
|
279 apply simp |
|
280 (* Here the only real goal compatibility is left *) |
|
281 apply (erule Abs_lst1_fcb) |
|
282 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
|
283 apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)") |
|
284 apply simp |
|
285 apply (erule fresh_eqvt_at) |
|
286 apply(simp add: finite_supp) |
|
287 apply(simp) |
|
288 apply(simp add: eqvt_at_def) |
|
289 apply(drule_tac x="(b \<leftrightarrow> ba)" in spec) |
|
290 apply(simp) |
|
291 apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff]) |
|
292 apply(rename_tac b P ba xa ya Pa) |
|
293 apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)") |
|
294 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))") |
|
295 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))") |
|
296 prefer 2 |
|
297 apply (simp only: eqvt_at_def subs_mix_def) |
|
298 apply rule |
|
299 apply(simp (no_asm)) |
|
300 apply (subst testrr) |
|
301 apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def) |
|
302 apply (simp add: THE_default_def) |
|
303 apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))") |
|
304 apply simp_all[2] |
|
305 apply auto[1] |
|
306 apply (erule_tac x="x" in allE) |
|
307 apply simp |
|
308 apply (thin_tac "\<forall>p\<Colon>perm. |
|
309 p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) = |
|
310 (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
311 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
|
312 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
313 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
|
314 else Inr (Inr undefined))") |
|
315 apply (thin_tac "\<forall>p\<Colon>perm. |
|
316 p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
317 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
|
318 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
319 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
|
320 else Inr (Inr undefined)) = |
|
321 (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
322 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
|
323 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
324 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
|
325 else Inr (Inr undefined))") |
|
326 apply (thin_tac "atom b \<sharp> (xa, ya)") |
|
327 apply (thin_tac "atom ba \<sharp> (xa, ya)") |
|
328 apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa") |
|
329 apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
330 apply assumption |
|
331 apply (metis Inr_not_Inl) |
|
332 apply (metis Inr_not_Inl) |
|
333 apply (metis Inr_not_Inl) |
|
334 apply (metis Inr_inject Inr_not_Inl) |
|
335 apply (metis Inr_inject Inr_not_Inl) |
|
336 apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr |
|
337 (Sum_Type.Projr |
|
338 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
|
339 apply clarify |
|
340 apply (rule the1_equality) |
|
341 apply blast apply assumption |
|
342 apply (rule_tac x="Sum_Type.Projr |
|
343 (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior> |
|
344 Sum_Type.Projr |
|
345 (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) |
|
346 apply clarify |
|
347 apply (rule the1_equality) |
|
348 apply blast apply assumption |
|
349 apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr |
|
350 (Sum_Type.Projr |
|
351 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
|
352 apply clarify |
|
353 apply (rule the1_equality) |
|
354 apply blast apply assumption |
|
355 apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl |
|
356 (Sum_Type.Projr |
|
357 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI) |
|
358 apply clarify |
|
359 apply (rule the1_equality) |
|
360 apply blast apply assumption |
|
361 apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr |
|
362 (Sum_Type.Projr |
|
363 (subsGuard_mix_subsList_mix_subs_mix_sum |
|
364 (Inr (Inr (Pb, xb, y)))))" in exI) |
|
365 apply clarify |
|
366 apply (rule the1_equality) |
|
367 apply blast apply assumption |
|
368 apply (rule_tac x="succ\<onesuperior>" in exI) |
|
369 apply clarify |
|
370 apply (rule the1_equality) |
|
371 apply blast apply assumption |
|
372 apply simp |
|
373 (* Here the only real goal compatibility is left *) |
|
374 apply (erule Abs_lst1_fcb) |
|
375 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
|
376 apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)") |
|
377 apply simp |
|
378 apply (erule fresh_eqvt_at) |
|
379 apply(simp add: finite_supp) |
|
380 apply(simp) |
|
381 apply(simp add: eqvt_at_def) |
|
382 apply(drule_tac x="(b \<leftrightarrow> ba)" in spec) |
|
383 apply(simp) |
|
384 done |
|
385 |
|
386 termination (eqvt) |
|
387 by (lexicographic_order) |
|
388 |
|
389 lemma forget_mix: |
|
390 fixes g :: guardedTerm_mix |
|
391 and xg :: sumList_mix |
|
392 and P :: piMix |
|
393 and x :: name |
|
394 and y :: name |
|
395 |
|
396 shows "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g" |
|
397 and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg" |
|
398 and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P" |
|
399 proof - |
|
400 show "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g" |
|
401 and "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg" |
|
402 and "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P" |
|
403 using assms |
|
404 apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct) |
|
405 by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base) |
|
406 qed |
|
407 |
|
408 lemma fresh_fact_mix: |
|
409 fixes g :: guardedTerm_mix |
|
410 and xg :: sumList_mix |
|
411 and P :: piMix |
|
412 and x :: name |
|
413 and y :: name |
|
414 and z :: name |
|
415 |
|
416 assumes "atom z \<sharp> y" |
|
417 |
|
418 shows "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]" |
|
419 and "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]" |
|
420 and "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]" |
|
421 proof - |
|
422 show "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]" |
|
423 and "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]" |
|
424 and "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]" |
|
425 using assms |
|
426 apply(nominal_induct g and xg and P avoiding: x y z rule: piMix_strong_induct) |
|
427 by(auto simp add: piMix_fresh fresh_at_base) |
|
428 qed |
|
429 |
|
430 lemma substitution_lemma_mix: |
|
431 fixes g :: guardedTerm_mix |
|
432 and xg :: sumList_mix |
|
433 and P :: piMix |
|
434 and s :: name |
|
435 and u :: name |
|
436 and x :: name |
|
437 and y :: name |
|
438 |
|
439 assumes "x \<noteq> y" |
|
440 and "atom x \<sharp> u" |
|
441 |
|
442 shows "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]" |
|
443 and "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]" |
|
444 and "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]" |
|
445 proof - |
|
446 show "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]" |
|
447 and "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]" |
|
448 and "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]" |
|
449 using assms |
|
450 apply(nominal_induct g and xg and P avoiding: x y s u rule: piMix_strong_induct) |
|
451 apply(simp_all add: fresh_fact_mix forget_mix) |
|
452 by(auto simp add: fresh_at_base) |
|
453 qed |
|
454 |
|
455 lemma perm_eq_subst_mix: |
|
456 fixes g :: guardedTerm_mix |
|
457 and xg :: sumList_mix |
|
458 and P :: piMix |
|
459 and x :: name |
|
460 and y :: name |
|
461 |
|
462 shows "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]" |
|
463 and "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]" |
|
464 and "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]" |
|
465 proof - |
|
466 show "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]" |
|
467 and "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]" |
|
468 and "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]" |
|
469 apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct) |
|
470 by(auto simp add: piMix_fresh fresh_at_base) |
|
471 qed |
|
472 |
|
473 lemma subst_id_mix: |
|
474 fixes g :: guardedTerm_mix |
|
475 and xg :: sumList_mix |
|
476 and P :: piMix |
|
477 and x :: name |
|
478 |
|
479 shows "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P" |
|
480 proof - |
|
481 show "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P" |
|
482 apply(nominal_induct g and xg and P avoiding: x rule: piMix_strong_induct) |
|
483 by(auto) |
|
484 qed |
|
485 |
|
486 lemma alphaRes_subst_mix: |
|
487 fixes a :: name |
|
488 and P :: piMix |
|
489 and z :: name |
|
490 |
|
491 assumes "atom z \<sharp> P" |
|
492 |
|
493 shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>(P[a::=\<onesuperior>z])" |
|
494 proof(cases "a = z") |
|
495 assume "a = z" |
|
496 thus ?thesis |
|
497 by(simp add: subst_id_mix) |
|
498 next |
|
499 assume "a \<noteq> z" |
|
500 thus ?thesis |
|
501 using assms |
|
502 by(simp add: alphaRes_mix perm_eq_subst_mix) |
|
503 qed |
|
504 |
|
505 lemma alphaInput_subst_mix: |
|
506 fixes a :: name |
|
507 and b :: name |
|
508 and P :: piMix |
|
509 and z :: name |
|
510 |
|
511 assumes "atom z \<sharp> P" |
|
512 |
|
513 shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])" |
|
514 proof(cases "b = z") |
|
515 assume "b = z" |
|
516 thus ?thesis |
|
517 by(simp add: subst_id_mix) |
|
518 next |
|
519 assume "b \<noteq> z" |
|
520 thus ?thesis |
|
521 using assms |
|
522 by(simp add: alphaInput_mix perm_eq_subst_mix) |
|
523 qed |
|
524 |
|
525 lemma alphaRep_subst_mix: |
|
526 fixes a :: name |
|
527 and b :: name |
|
528 and P :: piMix |
|
529 and z :: name |
|
530 |
|
531 assumes "atom z \<sharp> P" |
|
532 |
|
533 shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])" |
|
534 proof(cases "b = z") |
|
535 assume "b = z" |
|
536 thus ?thesis |
|
537 by(simp add: subst_id_mix) |
|
538 next |
|
539 assume "b \<noteq> z" |
|
540 thus ?thesis |
|
541 using assms |
|
542 by(simp add: alphaRep_mix perm_eq_subst_mix) |
|
543 qed |
|
544 |
|
545 inductive |
|
546 fresh_list_guard_mix :: "name list \<Rightarrow> guardedTerm_mix \<Rightarrow> bool" |
|
547 where |
|
548 "fresh_list_guard_mix [] g" |
|
549 | "\<lbrakk>atom n \<sharp> g; fresh_list_guard_mix xn g\<rbrakk> \<Longrightarrow> fresh_list_guard_mix (n#xn) g" |
|
550 |
|
551 equivariance fresh_list_guard_mix |
|
552 nominal_inductive fresh_list_guard_mix |
|
553 done |
|
554 |
|
555 inductive |
|
556 fresh_list_sumList_mix :: "name list \<Rightarrow> sumList_mix \<Rightarrow> bool" |
|
557 where |
|
558 "fresh_list_sumList_mix [] xg" |
|
559 | "\<lbrakk>atom n \<sharp> xg; fresh_list_sumList_mix xn xg\<rbrakk> \<Longrightarrow> fresh_list_sumList_mix (n#xn) xg" |
|
560 |
|
561 equivariance fresh_list_sumList_mix |
|
562 nominal_inductive fresh_list_sumList_mix |
|
563 done |
|
564 |
|
565 inductive |
|
566 fresh_list_mix :: "name list \<Rightarrow> piMix \<Rightarrow> bool" |
|
567 where |
|
568 "fresh_list_mix [] P" |
|
569 | "\<lbrakk>atom n \<sharp> P; fresh_list_mix xn P\<rbrakk> \<Longrightarrow> fresh_list_mix (n#xn) P" |
|
570 |
|
571 equivariance fresh_list_mix |
|
572 nominal_inductive fresh_list_mix |
|
573 done |
|
574 |
|
575 end |
|