1 (* Title: HOL/BNF/Examples/Infinite_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 Tree |
|
12 begin |
|
13 |
|
14 no_notation plus_class.plus (infixl "+" 65) |
|
15 no_notation Sublist.parallel (infixl "\<parallel>" 50) |
|
16 |
|
17 consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60) |
|
18 |
|
19 axiomatization where |
|
20 Nplus_comm: "(a::N) + b = b + (a::N)" |
|
21 and Nplus_assoc: "((a::N) + b) + c = a + (b + c)" |
|
22 |
|
23 section{* Parallel composition *} |
|
24 |
|
25 fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2" |
|
26 fun par_c where |
|
27 "par_c (tr1,tr2) = |
|
28 Inl ` (Inl -` (cont tr1 \<union> cont tr2)) \<union> |
|
29 Inr ` (Inr -` cont tr1 \<times> Inr -` cont tr2)" |
|
30 |
|
31 declare par_r.simps[simp del] declare par_c.simps[simp del] |
|
32 |
|
33 definition par :: "Tree \<times> Tree \<Rightarrow> Tree" where |
|
34 "par \<equiv> unfold par_r par_c" |
|
35 |
|
36 abbreviation par_abbr (infixr "\<parallel>" 80) where "tr1 \<parallel> tr2 \<equiv> par (tr1, tr2)" |
|
37 |
|
38 lemma finite_par_c: "finite (par_c (tr1, tr2))" |
|
39 unfolding par_c.simps apply(rule finite_UnI) |
|
40 apply (metis finite_Un finite_cont finite_imageI finite_vimageI inj_Inl) |
|
41 apply(intro finite_imageI finite_cartesian_product finite_vimageI) |
|
42 using finite_cont by auto |
|
43 |
|
44 lemma root_par: "root (tr1 \<parallel> tr2) = root tr1 + root tr2" |
|
45 using unfold(1)[of par_r par_c "(tr1,tr2)"] unfolding par_def par_r.simps by simp |
|
46 |
|
47 lemma cont_par: |
|
48 "cont (tr1 \<parallel> tr2) = (id \<oplus> par) ` par_c (tr1,tr2)" |
|
49 using unfold(2)[of par_c "(tr1,tr2)" par_r, OF finite_par_c] |
|
50 unfolding par_def .. |
|
51 |
|
52 lemma Inl_cont_par[simp]: |
|
53 "Inl -` (cont (tr1 \<parallel> tr2)) = Inl -` (cont tr1 \<union> cont tr2)" |
|
54 unfolding cont_par par_c.simps by auto |
|
55 |
|
56 lemma Inr_cont_par[simp]: |
|
57 "Inr -` (cont (tr1 \<parallel> tr2)) = par ` (Inr -` cont tr1 \<times> Inr -` cont tr2)" |
|
58 unfolding cont_par par_c.simps by auto |
|
59 |
|
60 lemma Inl_in_cont_par: |
|
61 "Inl t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (Inl t \<in> cont tr1 \<or> Inl t \<in> cont tr2)" |
|
62 using Inl_cont_par[of tr1 tr2] unfolding vimage_def by auto |
|
63 |
|
64 lemma Inr_in_cont_par: |
|
65 "Inr t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (t \<in> par ` (Inr -` cont tr1 \<times> Inr -` cont tr2))" |
|
66 using Inr_cont_par[of tr1 tr2] unfolding vimage_def by auto |
|
67 |
|
68 |
|
69 section{* =-coinductive proofs *} |
|
70 |
|
71 (* Detailed proofs of commutativity and associativity: *) |
|
72 theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1" |
|
73 proof- |
|
74 let ?\<phi> = "\<lambda> trA trB. \<exists> tr1 tr2. trA = tr1 \<parallel> tr2 \<and> trB = tr2 \<parallel> tr1" |
|
75 {fix trA trB |
|
76 assume "?\<phi> trA trB" hence "trA = trB" |
|
77 proof (induct rule: Tree_coind, safe) |
|
78 fix tr1 tr2 |
|
79 show "root (tr1 \<parallel> tr2) = root (tr2 \<parallel> tr1)" |
|
80 unfolding root_par by (rule Nplus_comm) |
|
81 next |
|
82 fix tr1 tr2 :: Tree |
|
83 let ?trA = "tr1 \<parallel> tr2" let ?trB = "tr2 \<parallel> tr1" |
|
84 show "(?\<phi> ^#2) (cont ?trA) (cont ?trB)" |
|
85 unfolding lift2_def proof(intro conjI allI impI) |
|
86 fix n show "Inl n \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> Inl n \<in> cont (tr2 \<parallel> tr1)" |
|
87 unfolding Inl_in_cont_par by auto |
|
88 next |
|
89 fix trA' assume "Inr trA' \<in> cont ?trA" |
|
90 then obtain tr1' tr2' where "trA' = tr1' \<parallel> tr2'" |
|
91 and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2" |
|
92 unfolding Inr_in_cont_par by auto |
|
93 thus "\<exists> trB'. Inr trB' \<in> cont ?trB \<and> ?\<phi> trA' trB'" |
|
94 apply(intro exI[of _ "tr2' \<parallel> tr1'"]) unfolding Inr_in_cont_par by auto |
|
95 next |
|
96 fix trB' assume "Inr trB' \<in> cont ?trB" |
|
97 then obtain tr1' tr2' where "trB' = tr2' \<parallel> tr1'" |
|
98 and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2" |
|
99 unfolding Inr_in_cont_par by auto |
|
100 thus "\<exists> trA'. Inr trA' \<in> cont ?trA \<and> ?\<phi> trA' trB'" |
|
101 apply(intro exI[of _ "tr1' \<parallel> tr2'"]) unfolding Inr_in_cont_par by auto |
|
102 qed |
|
103 qed |
|
104 } |
|
105 thus ?thesis by blast |
|
106 qed |
|
107 |
|
108 theorem par_assoc: "(tr1 \<parallel> tr2) \<parallel> tr3 = tr1 \<parallel> (tr2 \<parallel> tr3)" |
|
109 proof- |
|
110 let ?\<phi> = |
|
111 "\<lambda> trA trB. \<exists> tr1 tr2 tr3. trA = (tr1 \<parallel> tr2) \<parallel> tr3 \<and> |
|
112 trB = tr1 \<parallel> (tr2 \<parallel> tr3)" |
|
113 {fix trA trB |
|
114 assume "?\<phi> trA trB" hence "trA = trB" |
|
115 proof (induct rule: Tree_coind, safe) |
|
116 fix tr1 tr2 tr3 |
|
117 show "root ((tr1 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))" |
|
118 unfolding root_par by (rule Nplus_assoc) |
|
119 next |
|
120 fix tr1 tr2 tr3 |
|
121 let ?trA = "(tr1 \<parallel> tr2) \<parallel> tr3" let ?trB = "tr1 \<parallel> (tr2 \<parallel> tr3)" |
|
122 show "(?\<phi> ^#2) (cont ?trA) (cont ?trB)" |
|
123 unfolding lift2_def proof(intro conjI allI impI) |
|
124 fix n show "Inl n \<in> (cont ?trA) \<longleftrightarrow> Inl n \<in> (cont ?trB)" |
|
125 unfolding Inl_in_cont_par by simp |
|
126 next |
|
127 fix trA' assume "Inr trA' \<in> cont ?trA" |
|
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'. Inr trB' \<in> cont ?trB \<and> ?\<phi> trA' trB'" |
|
132 apply(intro exI[of _ "tr1' \<parallel> (tr2' \<parallel> tr3')"]) |
|
133 unfolding Inr_in_cont_par by auto |
|
134 next |
|
135 fix trB' assume "Inr trB' \<in> cont ?trB" |
|
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'. Inr trA' \<in> cont ?trA \<and> ?\<phi> trA' trB'" |
|
140 apply(intro exI[of _ "(tr1' \<parallel> tr2') \<parallel> tr3'"]) |
|
141 unfolding Inr_in_cont_par by auto |
|
142 qed |
|
143 qed |
|
144 } |
|
145 thus ?thesis by blast |
|
146 qed |
|
147 |
|
148 |
|
149 |
|
150 |
|
151 |
|
152 end |
|