Theory Parallel_Composition

(*  Title:      HOL/Datatype_Examples/Derivation_Trees/Parallel_Composition.thy
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Parallel composition.
*)

section ‹Parallel Composition›

theory Parallel_Composition
imports DTree
begin

no_notation plus_class.plus (infixl "+" 65)

consts Nplus :: "N ⇒ N ⇒ N" (infixl "+" 60)

axiomatization where
    Nplus_comm: "(a::N) + b = b + (a::N)"
and Nplus_assoc: "((a::N) + b) + c = a + (b + c)"

subsection‹Corecursive Definition of Parallel Composition›

fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2"
fun par_c where
"par_c (tr1,tr2) =
 Inl ` (Inl -` (cont tr1 ∪ cont tr2)) ∪
 Inr ` (Inr -` cont tr1 × Inr -` cont tr2)"

declare par_r.simps[simp del]  declare par_c.simps[simp del]

definition par :: "dtree × dtree ⇒ dtree" where
"par ≡ unfold par_r par_c"

abbreviation par_abbr (infixr "∥" 80) where "tr1 ∥ tr2 ≡ par (tr1, tr2)"

lemma finite_par_c: "finite (par_c (tr1, tr2))"
unfolding par_c.simps apply(rule finite_UnI)
  apply (metis finite_Un finite_cont finite_imageI finite_vimageI inj_Inl)
  apply(intro finite_imageI finite_cartesian_product finite_vimageI)
  using finite_cont by auto

lemma root_par: "root (tr1 ∥ tr2) = root tr1 + root tr2"
using unfold(1)[of par_r par_c "(tr1,tr2)"] unfolding par_def par_r.simps by simp

lemma cont_par:
"cont (tr1 ∥ tr2) = (id ⊕ par) ` par_c (tr1,tr2)"
using unfold(2)[of par_c "(tr1,tr2)" par_r, OF finite_par_c]
unfolding par_def ..

lemma Inl_cont_par[simp]:
"Inl -` (cont (tr1 ∥ tr2)) = Inl -` (cont tr1 ∪ cont tr2)"
unfolding cont_par par_c.simps by auto

lemma Inr_cont_par[simp]:
"Inr -` (cont (tr1 ∥ tr2)) = par ` (Inr -` cont tr1 × Inr -` cont tr2)"
unfolding cont_par par_c.simps by auto

lemma Inl_in_cont_par:
"Inl t ∈ cont (tr1 ∥ tr2) ⟷ (Inl t ∈ cont tr1 ∨ Inl t ∈ cont tr2)"
using Inl_cont_par[of tr1 tr2] unfolding vimage_def by auto

lemma Inr_in_cont_par:
"Inr t ∈ cont (tr1 ∥ tr2) ⟷ (t ∈ par ` (Inr -` cont tr1 × Inr -` cont tr2))"
using Inr_cont_par[of tr1 tr2] unfolding vimage_def by auto


subsection‹Structural Coinduction Proofs›

lemma rel_set_rel_sum_eq[simp]:
"rel_set (rel_sum (=) φ) A1 A2 ⟷
 Inl -` A1 = Inl -` A2 ∧ rel_set φ (Inr -` A1) (Inr -` A2)"
unfolding rel_set_rel_sum rel_set_eq ..

(* Detailed proofs of commutativity and associativity: *)
theorem par_com: "tr1 ∥ tr2 = tr2 ∥ tr1"
proof-
  let ?θ = "λ trA trB. ∃ tr1 tr2. trA = tr1 ∥ tr2 ∧ trB = tr2 ∥ tr1"
  {fix trA trB
   assume "?θ trA trB" hence "trA = trB"
   apply (induct rule: dtree_coinduct)
   unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe
     fix tr1 tr2  show "root (tr1 ∥ tr2) = root (tr2 ∥ tr1)"
     unfolding root_par by (rule Nplus_comm)
   next
     fix n tr1 tr2 assume "Inl n ∈ cont (tr1 ∥ tr2)" thus "n ∈ Inl -` (cont (tr2 ∥ tr1))"
     unfolding Inl_in_cont_par by auto
   next
     fix n tr1 tr2 assume "Inl n ∈ cont (tr2 ∥ tr1)" thus "n ∈ Inl -` (cont (tr1 ∥ tr2))"
     unfolding Inl_in_cont_par by auto
   next
     fix tr1 tr2 trA' assume "Inr trA' ∈ cont (tr1 ∥ tr2)"
     then obtain tr1' tr2' where "trA' = tr1' ∥ tr2'"
     and "Inr tr1' ∈ cont tr1" and "Inr tr2' ∈ cont tr2"
     unfolding Inr_in_cont_par by auto
     thus "∃ trB' ∈ Inr -` (cont (tr2 ∥ tr1)). ?θ trA' trB'"
     apply(intro bexI[of _ "tr2' ∥ tr1'"]) unfolding Inr_in_cont_par by auto
   next
     fix tr1 tr2 trB' assume "Inr trB' ∈ cont (tr2 ∥ tr1)"
     then obtain tr1' tr2' where "trB' = tr2' ∥ tr1'"
     and "Inr tr1' ∈ cont tr1" and "Inr tr2' ∈ cont tr2"
     unfolding Inr_in_cont_par by auto
     thus "∃ trA' ∈ Inr -` (cont (tr1 ∥ tr2)). ?θ trA' trB'"
     apply(intro bexI[of _ "tr1' ∥ tr2'"]) unfolding Inr_in_cont_par by auto
   qed
  }
  thus ?thesis by blast
qed

lemma par_assoc: "(tr1 ∥ tr2) ∥ tr3 = tr1 ∥ (tr2 ∥ tr3)"
proof-
  let ?θ =
  "λ trA trB. ∃ tr1 tr2 tr3. trA = (tr1 ∥ tr2) ∥ tr3 ∧ trB = tr1 ∥ (tr2 ∥ tr3)"
  {fix trA trB
   assume "?θ trA trB" hence "trA = trB"
   apply (induct rule: dtree_coinduct)
   unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe
     fix tr1 tr2 tr3  show "root ((tr1 ∥ tr2) ∥ tr3) = root (tr1 ∥ (tr2 ∥ tr3))"
     unfolding root_par by (rule Nplus_assoc)
   next
     fix n tr1 tr2 tr3 assume "Inl n ∈ (cont ((tr1 ∥ tr2) ∥ tr3))"
     thus "n ∈ Inl -` (cont (tr1 ∥ tr2 ∥ tr3))" unfolding Inl_in_cont_par by simp
   next
     fix n tr1 tr2 tr3 assume "Inl n ∈ (cont (tr1 ∥ tr2 ∥ tr3))"
     thus "n ∈ Inl -` (cont ((tr1 ∥ tr2) ∥ tr3))" unfolding Inl_in_cont_par by simp
   next
     fix trA' tr1 tr2 tr3 assume "Inr trA' ∈ cont ((tr1 ∥ tr2) ∥ tr3)"
     then obtain tr1' tr2' tr3' where "trA' = (tr1' ∥ tr2') ∥ tr3'"
     and "Inr tr1' ∈ cont tr1" and "Inr tr2' ∈ cont tr2"
     and "Inr tr3' ∈ cont tr3" unfolding Inr_in_cont_par by auto
     thus "∃ trB' ∈ Inr -` (cont (tr1 ∥ tr2 ∥ tr3)). ?θ trA' trB'"
     apply(intro bexI[of _ "tr1' ∥ tr2' ∥ tr3'"])
     unfolding Inr_in_cont_par by auto
   next
     fix trB' tr1 tr2 tr3 assume "Inr trB' ∈ cont (tr1 ∥ tr2 ∥ tr3)"
     then obtain tr1' tr2' tr3' where "trB' = tr1' ∥ (tr2' ∥ tr3')"
     and "Inr tr1' ∈ cont tr1" and "Inr tr2' ∈ cont tr2"
     and "Inr tr3' ∈ cont tr3" unfolding Inr_in_cont_par by auto
     thus "∃ trA' ∈ Inr -` cont ((tr1 ∥ tr2) ∥ tr3). ?θ trA' trB'"
     apply(intro bexI[of _ "(tr1' ∥ tr2') ∥ tr3'"])
     unfolding Inr_in_cont_par by auto
   qed
  }
  thus ?thesis by blast
qed

end