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