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