1Kind name,action,proc type.
2
3Import "ccs_bisim_context".
4Import "ccs_ctx".
5Import "ccs_bisim_examples_helper".
6
7Theorem bisim_context_reflexive_ : forall P,
8  bisim_up_to bisim_context_t P P.
9coinduction. intros. unfold.
10  intros.
11  witness P1. split. search.
12    witness P1. witness P1. split.
13      unfold. witness P1. witness P1. split.
14        unfold.
15          backchain bisim_reflexive_.
16          backchain bisim_reflexive_.
17        search.
18      backchain CH.
19  intros.
20  witness Q1. split. search.
21    witness Q1. witness Q1. split.
22      unfold. witness Q1. witness Q1. split.
23        unfold.
24          backchain bisim_reflexive_.
25          backchain bisim_reflexive_.
26        search.
27      backchain CH.
28
29Theorem bisim_repl_absorb : forall P,
30  bisim_up_to refl_t (par (repl P) P) (repl P).
31Sound : apply bisim_context_sound. Sound : case Sound.
32intros. backchain Sound. clear Sound.
33coinduction. intros. unfold.
34  intros. case H1.
35    case H2.
36      witness (par (repl P) Q). split. search.
37      witness (par (repl P) P).
38      witness (repl P). split. unfold.
39      witness (par (par (repl P) P) Q).
40      witness (par (repl P) Q). split. unfold.
41      backchain bisim_par_assoc_left.
42      backchain bisim_reflexive_.
43      search.
44      backchain CH.
45      witness (par (repl P) (par Q R)). split. search.
46      witness (par (repl P) P).
47      witness (repl P). split. unfold.
48      witness (par (par (repl P) P) (par Q R)).
49      witness (par (repl P) (par Q R)). split. unfold.
50      backchain bisim_par_assoc_left.
51      backchain bisim_reflexive_.
52      search.
53      backchain CH.
54      witness (par (repl P) Q1). split. search.
55      witness (par (repl P) Q1).
56      witness (par (repl P) Q1). split. unfold.
57      witness (par (repl P) Q1).
58      witness (par (repl P) Q1). split. unfold.
59      backchain bisim_reflexive_.
60      backchain bisim_reflexive_.
61      search.
62      backchain bisim_context_reflexive_.
63    case H2.
64      witness (par (repl P) (par Q Q1)). split. search.
65      witness (par (repl P) (par Q Q1)).
66      witness (par (repl P) (par Q Q1)). split. unfold.
67      witness (par (repl P) (par Q Q1)).
68      witness (par (repl P) (par Q Q1)). split. unfold.
69      backchain bisim_par_assoc.
70      backchain bisim_reflexive_.
71      search.
72      backchain bisim_context_reflexive_.
73    case H2.
74      witness (par (repl P) (par Q1 Q)). split. search.
75      witness (par (repl P) (par Q1 Q)).
76      witness (par (repl P) (par Q1 Q)). split. unfold.
77      witness (par (repl P) (par Q1 Q)).
78      witness (par (repl P) (par Q1 Q)). split. unfold.
79      apply bisim_par_comm with P = Q, Q = Q1.
80      apply bisim_par_subst_2 to H5 with R = (repl P).
81      apply bisim_par_assoc with P = (repl P), Q = Q, R = Q1.
82      backchain bisim_transitive_.
83      backchain bisim_reflexive_.
84      search.
85      backchain bisim_context_reflexive_.
86  intros. case H1.
87      witness (par (par (repl P) Q) P). split. search.
88      witness (par (repl P) P).
89      witness (repl P). split. unfold.
90      witness (par (par (repl P) P) Q).
91      witness (par (repl P) Q). split. unfold.
92      backchain bisim_par_assoc_left.
93      backchain bisim_reflexive_.
94      search.
95      backchain CH.
96      witness (par (par (repl P) (par Q R)) P). split. search.
97      witness (par (repl P) P).
98      witness (repl P). split. unfold.
99      witness (par (par (repl P) P) (par Q R)).
100      witness (par (repl P) (par Q R)). split. unfold.
101      backchain bisim_par_assoc_left.
102      backchain bisim_reflexive_.
103      search.
104      backchain CH.
105
106
107%%% !(a.P + b.Q) ~ (!a.P | !b.Q)
108
109Theorem ex_bang_plus_ctx : forall P,
110  bisim (repl (plus (act (dn a) P) (act (dn b) P)))
111        (par (repl (act (dn a) P)) (repl (act (dn b) P))).
112Sound : apply bisim_context_sound. Sound : case Sound.
113intros. unfold. backchain Sound. clear Sound.
114coinduction. intros. unfold.
115  intros. case H1.
116    case H2.
117      case H3.
118      witness (par (par (repl (act (dn a) P)) P) (repl (act (dn b) P))). split. search.
119        witness (repl (plus (act (dn a) P) (act (dn b) P))).
120        witness (par (repl (act (dn a) P)) (repl (act (dn b) P))). split. unfold.
121        witness (par (repl (plus (act (dn a) P) (act (dn b) P))) P).
122        witness (par (par (repl (act (dn a) P)) (repl (act (dn b) P))) P). split. unfold.
123        backchain bisim_reflexive_.
124        apply bisim_par_comm with P = P, Q = (repl (act (dn b) Q)).
125        apply bisim_par_subst_2 to H4 with R = (repl (act (dn a) Q)).
126        apply bisim_par_assoc with P = (repl (act (dn a) Q)), Q = P, R = (repl (act (dn b) Q)).
127        apply bisim_par_assoc with P = (repl (act (dn a) Q)), Q = (repl (act (dn b) Q)), R = P.
128        apply bisim_transitive_ to H6 H5.
129        apply bisim_symmetric_ to H7.
130        apply bisim_transitive_ to H8 H9.
131        search.
132        search.
133        backchain CH.
134      case H3.
135      witness (par (repl (act (dn a) P)) (par (repl (act (dn b) P)) P)). split. search.
136        witness (repl (plus (act (dn a) P) (act (dn b) P))).
137        witness (par (repl (act (dn a) P)) (repl (act (dn b) P))). split. unfold.
138        witness (par (repl (plus (act (dn a) P) (act (dn b) P))) P).
139        witness (par (par (repl (act (dn a) P)) (repl (act (dn b) P))) P). split. unfold.
140        backchain bisim_reflexive_.
141        apply bisim_par_assoc with P = (repl (act (dn a) Q)), Q = (repl (act (dn b) Q)), R = Q.
142        backchain bisim_symmetric_.
143        search.
144        backchain CH.
145    case H2.
146      case H4.
147      case H4.
148  intros. case H1.
149    case H2.
150      case H3.
151      witness (par (repl (plus (act (dn a) P) (act (dn b) P))) P). split. search.
152        witness (repl (plus (act (dn a) P) (act (dn b) P))).
153        witness (par (repl (act (dn a) P)) (repl (act (dn b) P))). split. unfold.
154        witness (par (repl (plus (act (dn a) P) (act (dn b) P))) P).
155        witness (par (par (repl (act (dn a) P)) (repl (act (dn b) P))) P). split. unfold.
156        backchain bisim_reflexive_.
157        apply bisim_par_comm with P = Q, Q = (repl (act (dn b) Q)).
158        apply bisim_par_subst_2 to H4 with R = (repl (act (dn a) Q)).
159        apply bisim_par_assoc with P = (repl (act (dn a) Q)), Q = Q, R = (repl (act (dn b) Q)).
160        apply bisim_par_assoc with P = (repl (act (dn a) Q)), Q = (repl (act (dn b) Q)), R = Q.
161        apply bisim_transitive_ to H6 H5.
162        apply bisim_symmetric_ to H7.
163        apply bisim_transitive_ to H8 H9.
164        search.
165        search.
166        backchain CH.
167      case H3.
168    case H2.
169      case H3.
170      witness (par (repl (plus (act (dn a) P) (act (dn b) P))) P). split. search.
171        witness (repl (plus (act (dn a) P) (act (dn b) P))).
172        witness (par (repl (act (dn a) P)) (repl (act (dn b) P))). split. unfold.
173        witness par (repl (plus (act (dn a) P) (act (dn b) P))) Q.
174        witness par (par (repl (act (dn a) P)) (repl (act (dn b) P))) Q. split. unfold.
175        backchain bisim_reflexive_.
176        apply bisim_par_assoc with P = (repl (act (dn a) P)), Q = (repl (act (dn b) P)), R = Q.
177        backchain bisim_symmetric_.
178        search.
179        backchain CH.
180      case H3.
181    case H2.
182      case H4.
183    case H3.
184      case H4.
185
186
187%%% !!a.P ~ !a.P
188
189Theorem ex_bang_bang_ctx : forall P,
190  bisim (repl (repl (act (dn a) P)))
191        (repl (act (dn a) P)).
192Sound : apply bisim_context_sound. Sound : case Sound. intros.
193unfold. backchain Sound. clear Sound.
194coinduction. intros. unfold.
195  intros. case H1.
196    case H2.
197      case H3.
198      witness (par (repl (act (dn a) P)) P). split. search.
199      witness (repl (repl (act (dn a) P))).
200      witness (repl (act (dn a) P)). split. unfold.
201      witness (par (repl (repl (act (dn a) P))) P).
202      witness (par (repl (act (dn a) P)) P). split. unfold.
203      apply bisim_repl_absorb with P = (repl (act (dn a) P)).
204      apply bisim_par_subst_1 to H4 with R = P.
205      apply bisim_par_assoc with P = (repl (repl (act (dn a) P))), Q = (repl (act (dn a) P)), R = P.
206      apply bisim_symmetric_ to H6.
207      apply bisim_transitive_ to H7 H5.
208      search.
209      backchain bisim_reflexive_.
210      search.
211      backchain CH.
212      case H3.
213    case H2.
214      case H4.
215
216  intros. case H1.
217    case H2.
218      witness (par (repl (repl (act (dn a) P))) (par (repl (act (dn a) P)) P)). split. search.
219      witness (repl (repl (act (dn a) P))).
220      witness (repl (act (dn a) P)). split. unfold.
221      witness (par (repl (repl (act (dn a) P))) P).
222      witness (par (repl (act (dn a) P)) P). split. unfold.
223      apply bisim_repl_absorb with P = (repl (act (dn a) P)).
224      apply bisim_par_subst_1 to H3 with R = P.
225      apply bisim_par_assoc with P = (repl (repl (act (dn a) P))), Q = (repl (act (dn a) P)), R = P.
226      apply bisim_symmetric_ to H5.
227      apply bisim_transitive_ to H6 H4.
228      search.
229      backchain bisim_reflexive_.
230      search.
231      backchain CH.
232    case H2.
233