|
1 (* Title: HOL/Datatype_Examples/Derivation_Trees/Parallel.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Parallel composition. |
|
6 *) |
|
7 |
|
8 header {* Parallel Composition *} |
|
9 |
|
10 theory Parallel |
|
11 imports DTree |
|
12 begin |
|
13 |
|
14 no_notation plus_class.plus (infixl "+" 65) |
|
15 |
|
16 consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60) |
|
17 |
|
18 axiomatization where |
|
19 Nplus_comm: "(a::N) + b = b + (a::N)" |
|
20 and Nplus_assoc: "((a::N) + b) + c = a + (b + c)" |
|
21 |
|
22 subsection{* Corecursive Definition of Parallel Composition *} |
|
23 |
|
24 fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2" |
|
25 fun par_c where |
|
26 "par_c (tr1,tr2) = |
|
27 Inl ` (Inl -` (cont tr1 \<union> cont tr2)) \<union> |
|
28 Inr ` (Inr -` cont tr1 \<times> Inr -` cont tr2)" |
|
29 |
|
30 declare par_r.simps[simp del] declare par_c.simps[simp del] |
|
31 |
|
32 definition par :: "dtree \<times> dtree \<Rightarrow> dtree" where |
|
33 "par \<equiv> unfold par_r par_c" |
|
34 |
|
35 abbreviation par_abbr (infixr "\<parallel>" 80) where "tr1 \<parallel> tr2 \<equiv> par (tr1, tr2)" |
|
36 |
|
37 lemma finite_par_c: "finite (par_c (tr1, tr2))" |
|
38 unfolding par_c.simps apply(rule finite_UnI) |
|
39 apply (metis finite_Un finite_cont finite_imageI finite_vimageI inj_Inl) |
|
40 apply(intro finite_imageI finite_cartesian_product finite_vimageI) |
|
41 using finite_cont by auto |
|
42 |
|
43 lemma root_par: "root (tr1 \<parallel> tr2) = root tr1 + root tr2" |
|
44 using unfold(1)[of par_r par_c "(tr1,tr2)"] unfolding par_def par_r.simps by simp |
|
45 |
|
46 lemma cont_par: |
|
47 "cont (tr1 \<parallel> tr2) = (id \<oplus> par) ` par_c (tr1,tr2)" |
|
48 using unfold(2)[of par_c "(tr1,tr2)" par_r, OF finite_par_c] |
|
49 unfolding par_def .. |
|
50 |
|
51 lemma Inl_cont_par[simp]: |
|
52 "Inl -` (cont (tr1 \<parallel> tr2)) = Inl -` (cont tr1 \<union> cont tr2)" |
|
53 unfolding cont_par par_c.simps by auto |
|
54 |
|
55 lemma Inr_cont_par[simp]: |
|
56 "Inr -` (cont (tr1 \<parallel> tr2)) = par ` (Inr -` cont tr1 \<times> Inr -` cont tr2)" |
|
57 unfolding cont_par par_c.simps by auto |
|
58 |
|
59 lemma Inl_in_cont_par: |
|
60 "Inl t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (Inl t \<in> cont tr1 \<or> Inl t \<in> cont tr2)" |
|
61 using Inl_cont_par[of tr1 tr2] unfolding vimage_def by auto |
|
62 |
|
63 lemma Inr_in_cont_par: |
|
64 "Inr t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (t \<in> par ` (Inr -` cont tr1 \<times> Inr -` cont tr2))" |
|
65 using Inr_cont_par[of tr1 tr2] unfolding vimage_def by auto |
|
66 |
|
67 |
|
68 subsection{* Structural Coinduction Proofs *} |
|
69 |
|
70 lemma rel_set_rel_sum_eq[simp]: |
|
71 "rel_set (rel_sum (op =) \<phi>) A1 A2 \<longleftrightarrow> |
|
72 Inl -` A1 = Inl -` A2 \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)" |
|
73 unfolding rel_set_rel_sum rel_set_eq .. |
|
74 |
|
75 (* Detailed proofs of commutativity and associativity: *) |
|
76 theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1" |
|
77 proof- |
|
78 let ?\<theta> = "\<lambda> trA trB. \<exists> tr1 tr2. trA = tr1 \<parallel> tr2 \<and> trB = tr2 \<parallel> tr1" |
|
79 {fix trA trB |
|
80 assume "?\<theta> trA trB" hence "trA = trB" |
|
81 apply (induct rule: dtree_coinduct) |
|
82 unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe |
|
83 fix tr1 tr2 show "root (tr1 \<parallel> tr2) = root (tr2 \<parallel> tr1)" |
|
84 unfolding root_par by (rule Nplus_comm) |
|
85 next |
|
86 fix n tr1 tr2 assume "Inl n \<in> cont (tr1 \<parallel> tr2)" thus "n \<in> Inl -` (cont (tr2 \<parallel> tr1))" |
|
87 unfolding Inl_in_cont_par by auto |
|
88 next |
|
89 fix n tr1 tr2 assume "Inl n \<in> cont (tr2 \<parallel> tr1)" thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2))" |
|
90 unfolding Inl_in_cont_par by auto |
|
91 next |
|
92 fix tr1 tr2 trA' assume "Inr trA' \<in> cont (tr1 \<parallel> tr2)" |
|
93 then obtain tr1' tr2' where "trA' = tr1' \<parallel> tr2'" |
|
94 and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2" |
|
95 unfolding Inr_in_cont_par by auto |
|
96 thus "\<exists> trB' \<in> Inr -` (cont (tr2 \<parallel> tr1)). ?\<theta> trA' trB'" |
|
97 apply(intro bexI[of _ "tr2' \<parallel> tr1'"]) unfolding Inr_in_cont_par by auto |
|
98 next |
|
99 fix tr1 tr2 trB' assume "Inr trB' \<in> cont (tr2 \<parallel> tr1)" |
|
100 then obtain tr1' tr2' where "trB' = tr2' \<parallel> tr1'" |
|
101 and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2" |
|
102 unfolding Inr_in_cont_par by auto |
|
103 thus "\<exists> trA' \<in> Inr -` (cont (tr1 \<parallel> tr2)). ?\<theta> trA' trB'" |
|
104 apply(intro bexI[of _ "tr1' \<parallel> tr2'"]) unfolding Inr_in_cont_par by auto |
|
105 qed |
|
106 } |
|
107 thus ?thesis by blast |
|
108 qed |
|
109 |
|
110 lemma par_assoc: "(tr1 \<parallel> tr2) \<parallel> tr3 = tr1 \<parallel> (tr2 \<parallel> tr3)" |
|
111 proof- |
|
112 let ?\<theta> = |
|
113 "\<lambda> trA trB. \<exists> tr1 tr2 tr3. trA = (tr1 \<parallel> tr2) \<parallel> tr3 \<and> trB = tr1 \<parallel> (tr2 \<parallel> tr3)" |
|
114 {fix trA trB |
|
115 assume "?\<theta> trA trB" hence "trA = trB" |
|
116 apply (induct rule: dtree_coinduct) |
|
117 unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe |
|
118 fix tr1 tr2 tr3 show "root ((tr1 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))" |
|
119 unfolding root_par by (rule Nplus_assoc) |
|
120 next |
|
121 fix n tr1 tr2 tr3 assume "Inl n \<in> (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" |
|
122 thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2 \<parallel> tr3))" unfolding Inl_in_cont_par by simp |
|
123 next |
|
124 fix n tr1 tr2 tr3 assume "Inl n \<in> (cont (tr1 \<parallel> tr2 \<parallel> tr3))" |
|
125 thus "n \<in> Inl -` (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" unfolding Inl_in_cont_par by simp |
|
126 next |
|
127 fix trA' tr1 tr2 tr3 assume "Inr trA' \<in> cont ((tr1 \<parallel> tr2) \<parallel> tr3)" |
|
128 then obtain tr1' tr2' tr3' where "trA' = (tr1' \<parallel> tr2') \<parallel> tr3'" |
|
129 and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2" |
|
130 and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto |
|
131 thus "\<exists> trB' \<in> Inr -` (cont (tr1 \<parallel> tr2 \<parallel> tr3)). ?\<theta> trA' trB'" |
|
132 apply(intro bexI[of _ "tr1' \<parallel> tr2' \<parallel> tr3'"]) |
|
133 unfolding Inr_in_cont_par by auto |
|
134 next |
|
135 fix trB' tr1 tr2 tr3 assume "Inr trB' \<in> cont (tr1 \<parallel> tr2 \<parallel> tr3)" |
|
136 then obtain tr1' tr2' tr3' where "trB' = tr1' \<parallel> (tr2' \<parallel> tr3')" |
|
137 and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2" |
|
138 and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto |
|
139 thus "\<exists> trA' \<in> Inr -` cont ((tr1 \<parallel> tr2) \<parallel> tr3). ?\<theta> trA' trB'" |
|
140 apply(intro bexI[of _ "(tr1' \<parallel> tr2') \<parallel> tr3'"]) |
|
141 unfolding Inr_in_cont_par by auto |
|
142 qed |
|
143 } |
|
144 thus ?thesis by blast |
|
145 qed |
|
146 |
|
147 end |