-
Notifications
You must be signed in to change notification settings - Fork 0
/
Weak_Cong_Pres.thy
214 lines (190 loc) · 8.23 KB
/
Weak_Cong_Pres.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
(*
Title: Psi-calculi
Based on the AFP entry by Jesper Bengtson ([email protected]), 2012
*)
theory Weak_Cong_Pres
imports Weak_Psi_Congruence Weak_Cong_Sim_Pres Weak_Bisim_Pres
begin
context env begin
lemma weakPsiCongInputPres:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and M :: 'a
and xvec :: "name list"
and N :: 'a
assumes "\<And>Tvec. length xvec = length Tvec \<Longrightarrow> \<Psi> \<rhd> P[xvec::=Tvec] \<approx> Q[xvec::=Tvec]"
shows "\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q"
proof -
from assms have "\<forall>Tvec. length xvec = length Tvec \<longrightarrow> \<Psi> \<rhd> P[xvec::=Tvec] \<approx> Q[xvec::=Tvec]"
by simp
thus ?thesis
proof(induct rule: weakPsiCongSymI)
case(cSym P Q)
thus ?case by(auto dest: weakBisimE)
next
case(cSim P Q)
show ?case
by(induct rule: weakCongSimI) auto
next
case(cWeakBisim P Q)
thus ?case by(rule_tac weakBisimInputPres) auto
qed
qed
lemma weakPsiCongOutputPres:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and M :: 'a
and xvec :: "name list"
and N :: 'a
assumes "\<Psi> \<rhd> P \<doteq> Q"
shows "\<Psi> \<rhd> M\<langle>N\<rangle>.P \<doteq> M\<langle>N\<rangle>.Q"
using assms
proof(induct rule: weakPsiCongSymI)
case(cSym P Q)
thus ?case by(rule weakPsiCongSym)
next
case(cSim P Q)
show ?case by(induct rule: weakCongSimI) auto
next
case(cWeakBisim P Q)
thus ?case by(metis weakPsiCongE weakBisimOutputPres)
qed
lemma weakBisimCasePres:
fixes \<Psi> :: 'b
and CsP :: "('c \<times> ('a, 'b, 'c) psi) list"
and CsQ :: "('c \<times> ('a, 'b, 'c) psi) list"
assumes A: "\<And>\<phi> P. (\<phi>, P) mem CsP \<Longrightarrow> \<exists>Q. (\<phi>, Q) mem CsQ \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)"
and B: "\<And>\<phi> Q. (\<phi>, Q) mem CsQ \<Longrightarrow> \<exists>P. (\<phi>, P) mem CsP \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)"
shows "\<Psi> \<rhd> Cases CsP \<approx> Cases CsQ"
proof -
let ?X = "{(\<Psi>, Cases CsP, Cases CsQ) | \<Psi> CsP CsQ. (\<forall>\<phi> P. (\<phi>, P) mem CsP \<longrightarrow> (\<exists>Q. (\<phi>, Q) mem CsQ \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q))) \<and>
(\<forall>\<phi> Q. (\<phi>, Q) mem CsQ \<longrightarrow> (\<exists>P. (\<phi>, P) mem CsP \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)))}"
from assms have "(\<Psi>, Cases CsP, Cases CsQ) \<in> ?X" by auto
thus ?thesis
proof(coinduct rule: weakBisimCoinduct)
case(cStatImp \<Psi> CasesP CasesQ)
thus ?case
apply(auto simp add: weak_stat_imp_def)
by(rule_tac x="Cases CsQ" in exI, auto)
next
case(cSim \<Psi> CasesP CasesQ)
then obtain CsP CsQ where C1: "\<And>\<phi> Q. (\<phi>, Q) mem CsQ \<Longrightarrow> \<exists>P. (\<phi>, P) mem CsP \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)"
and A: "CasesP = Cases CsP" and B: "CasesQ = Cases CsQ"
by auto
note C1
moreover have "\<And>\<Psi> P Q. \<Psi> \<rhd> P \<approx> Q \<Longrightarrow> \<Psi> \<rhd> P \<leadsto><weakBisim> Q" by(rule weakBisimE)
moreover note weakPsiCongE(1) weakPsiCongE(2)
ultimately have "\<Psi> \<rhd> Cases CsP \<leadsto><weakBisim> Cases CsQ"
by(rule_tac caseWeakSimPres) (assumption | blast)+
hence "\<Psi> \<rhd> Cases CsP \<leadsto><(?X \<union> weakBisim)> Cases CsQ"
by(rule_tac weakSimMonotonic) auto
with A B show ?case by blast
next
case(cExt \<Psi> P Q \<Psi>')
thus ?case by auto
next
case(cSym \<Psi> P Q)
thus ?case by auto (metis weakPsiCongSym)+
qed
qed
lemma weakPsiCongCasePres:
fixes \<Psi> :: 'b
and CsP :: "('c \<times> ('a, 'b, 'c) psi) list"
and CsQ :: "('c \<times> ('a, 'b, 'c) psi) list"
assumes A: "\<And>\<phi> P. (\<phi>, P) mem CsP \<Longrightarrow> \<exists>Q. (\<phi>, Q) mem CsQ \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)"
and B: "\<And>\<phi> Q. (\<phi>, Q) mem CsQ \<Longrightarrow> \<exists>P. (\<phi>, P) mem CsP \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)"
shows "\<Psi> \<rhd> Cases CsP \<doteq> Cases CsQ"
proof -
let ?Prop = "\<lambda>CsP CsQ. \<forall>\<phi> P. (\<phi>, P) mem CsP \<longrightarrow> (\<exists>Q. (\<phi>, Q) mem CsQ \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q))"
from A B have "?Prop CsP CsQ \<and> ?Prop CsQ CsP" by(metis weakPsiCongSym)
thus ?thesis
proof(induct rule: weakPsiCongSymI[where C="\<lambda>P. Cases P"])
case(cSym P Q)
thus ?case by auto
next
case(cWeakBisim CsP CsQ)
thus ?case
by(rule_tac weakBisimCasePres) (metis weakPsiCongSym)+
next
case(cSim CsP CsQ)
thus ?case
apply auto
apply(rule_tac weakCongSimCasePres, auto)
by(blast dest: weakPsiCongE)
qed
qed
lemma weakPsiCongResPres:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and x :: name
assumes "\<Psi> \<rhd> P \<doteq> Q"
and "x \<sharp> \<Psi>"
shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<doteq> \<lparr>\<nu>x\<rparr>Q"
using `\<Psi> \<rhd> P \<doteq> Q`
proof(induct rule: weakPsiCongSymI)
case(cSym P Q)
thus ?case by(rule weakPsiCongSym)
next
case(cWeakBisim P Q)
thus ?case using `x \<sharp> \<Psi>` by(metis weakPsiCongE weakBisimResPres)
next
case(cSim P Q)
obtain y::name where "y \<sharp> \<Psi>" and "y \<sharp> P" and "y \<sharp> Q"
by(generate_fresh "name") auto
from `\<Psi> \<rhd> P \<doteq> Q` have "([(x, y)] \<bullet> \<Psi>) \<rhd> ([(x, y)] \<bullet> P) \<doteq> ([(x, y)] \<bullet> Q)" by(rule weakPsiCongClosed)
hence "([(x, y)] \<bullet> \<Psi>) \<rhd> ([(x, y)] \<bullet> P) \<leadsto>\<guillemotleft>weakBisim\<guillemotright> ([(x, y)] \<bullet> Q)" by(rule weakPsiCongE)
with `x \<sharp> \<Psi>` `y \<sharp> \<Psi>` have "\<Psi> \<rhd> ([(x, y)] \<bullet> P) \<leadsto>\<guillemotleft>weakBisim\<guillemotright> ([(x, y)] \<bullet> Q)" by simp
moreover have "eqvt weakBisim" by simp
moreover note `y \<sharp> \<Psi>`
moreover have "weakBisim \<subseteq> weakBisim" by auto
moreover note weakBisimResPres
ultimately have "\<Psi> \<rhd> \<lparr>\<nu>y\<rparr>([(x, y)] \<bullet> P) \<leadsto>\<guillemotleft>weakBisim\<guillemotright> \<lparr>\<nu>y\<rparr>([(x, y)] \<bullet> Q)" by(rule weakCongSimResPres)
with `y \<sharp> P` `y \<sharp> Q` show ?case by(simp add: alpha_res)
qed
lemma weakPsiCongResChainPres:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and xvec :: "name list"
assumes "\<Psi> \<rhd> P \<doteq> Q"
and "xvec \<sharp>* \<Psi>"
shows "\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<doteq> \<lparr>\<nu>*xvec\<rparr>Q"
using assms
by(induct xvec) (auto intro: weakPsiCongResPres)
lemma weakPsiCongParPres:
fixes \<Psi> :: 'b
and P :: "('a, 'b, 'c) psi"
and Q :: "('a, 'b, 'c) psi"
and R :: "('a, 'b, 'c) psi"
assumes "\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q"
shows "\<Psi> \<rhd> P \<parallel> R \<doteq> Q \<parallel> R"
using assms
proof(induct rule: weakPsiCongSymI[where C="\<lambda>P. P \<parallel> R"])
case(cSym P Q)
thus ?case by(blast dest: weakPsiCongSym)
next
case(cWeakBisim P Q)
thus ?case by(metis weakBisimParPres weakPsiCongE)
next
case(cSim P Q)
{
fix \<Psi>
from `\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q` have "\<Psi> \<rhd> P \<leadsto>\<guillemotleft>weakBisim\<guillemotright> Q" by(auto dest: weakPsiCongE)
}
moreover {
fix \<Psi>
from `\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q` have "\<Psi> \<rhd> P \<leadsto><weakBisim> Q" by(auto dest: weakPsiCongE weakBisimE)
}
moreover {
fix \<Psi>
from `\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q` have "\<Psi> \<rhd> P \<approx> Q" by(auto dest: weakPsiCongE)
hence "\<Psi> \<rhd> Q \<lessapprox><weakBisim> P" by(metis weakBisimE)
}
ultimately show ?case using weakBisimEqvt weakBisimEqvt weakBisimE(4) weakBisimE(3) weakBisimParPresAux weakBisimResChainPres statEqWeakBisim
by(rule_tac weakCongSimParPres)
qed
end
end