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