src/HOL/Datatype_Examples/Derivation_Trees/Parallel_Composition.thy
changeset 65574 10f4a17e5928
parent 63167 0909deb8059b
child 67399 eab6ce8368fa
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Datatype_Examples/Derivation_Trees/Parallel_Composition.thy	Mon Apr 24 13:58:38 2017 +0200
     1.3 @@ -0,0 +1,147 @@
     1.4 +(*  Title:      HOL/Datatype_Examples/Derivation_Trees/Parallel_Composition.thy
     1.5 +    Author:     Andrei Popescu, TU Muenchen
     1.6 +    Copyright   2012
     1.7 +
     1.8 +Parallel composition.
     1.9 +*)
    1.10 +
    1.11 +section \<open>Parallel Composition\<close>
    1.12 +
    1.13 +theory Parallel_Composition
    1.14 +imports DTree
    1.15 +begin
    1.16 +
    1.17 +no_notation plus_class.plus (infixl "+" 65)
    1.18 +
    1.19 +consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60)
    1.20 +
    1.21 +axiomatization where
    1.22 +    Nplus_comm: "(a::N) + b = b + (a::N)"
    1.23 +and Nplus_assoc: "((a::N) + b) + c = a + (b + c)"
    1.24 +
    1.25 +subsection\<open>Corecursive Definition of Parallel Composition\<close>
    1.26 +
    1.27 +fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2"
    1.28 +fun par_c where
    1.29 +"par_c (tr1,tr2) =
    1.30 + Inl ` (Inl -` (cont tr1 \<union> cont tr2)) \<union>
    1.31 + Inr ` (Inr -` cont tr1 \<times> Inr -` cont tr2)"
    1.32 +
    1.33 +declare par_r.simps[simp del]  declare par_c.simps[simp del]
    1.34 +
    1.35 +definition par :: "dtree \<times> dtree \<Rightarrow> dtree" where
    1.36 +"par \<equiv> unfold par_r par_c"
    1.37 +
    1.38 +abbreviation par_abbr (infixr "\<parallel>" 80) where "tr1 \<parallel> tr2 \<equiv> par (tr1, tr2)"
    1.39 +
    1.40 +lemma finite_par_c: "finite (par_c (tr1, tr2))"
    1.41 +unfolding par_c.simps apply(rule finite_UnI)
    1.42 +  apply (metis finite_Un finite_cont finite_imageI finite_vimageI inj_Inl)
    1.43 +  apply(intro finite_imageI finite_cartesian_product finite_vimageI)
    1.44 +  using finite_cont by auto
    1.45 +
    1.46 +lemma root_par: "root (tr1 \<parallel> tr2) = root tr1 + root tr2"
    1.47 +using unfold(1)[of par_r par_c "(tr1,tr2)"] unfolding par_def par_r.simps by simp
    1.48 +
    1.49 +lemma cont_par:
    1.50 +"cont (tr1 \<parallel> tr2) = (id \<oplus> par) ` par_c (tr1,tr2)"
    1.51 +using unfold(2)[of par_c "(tr1,tr2)" par_r, OF finite_par_c]
    1.52 +unfolding par_def ..
    1.53 +
    1.54 +lemma Inl_cont_par[simp]:
    1.55 +"Inl -` (cont (tr1 \<parallel> tr2)) = Inl -` (cont tr1 \<union> cont tr2)"
    1.56 +unfolding cont_par par_c.simps by auto
    1.57 +
    1.58 +lemma Inr_cont_par[simp]:
    1.59 +"Inr -` (cont (tr1 \<parallel> tr2)) = par ` (Inr -` cont tr1 \<times> Inr -` cont tr2)"
    1.60 +unfolding cont_par par_c.simps by auto
    1.61 +
    1.62 +lemma Inl_in_cont_par:
    1.63 +"Inl t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (Inl t \<in> cont tr1 \<or> Inl t \<in> cont tr2)"
    1.64 +using Inl_cont_par[of tr1 tr2] unfolding vimage_def by auto
    1.65 +
    1.66 +lemma Inr_in_cont_par:
    1.67 +"Inr t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (t \<in> par ` (Inr -` cont tr1 \<times> Inr -` cont tr2))"
    1.68 +using Inr_cont_par[of tr1 tr2] unfolding vimage_def by auto
    1.69 +
    1.70 +
    1.71 +subsection\<open>Structural Coinduction Proofs\<close>
    1.72 +
    1.73 +lemma rel_set_rel_sum_eq[simp]:
    1.74 +"rel_set (rel_sum (op =) \<phi>) A1 A2 \<longleftrightarrow>
    1.75 + Inl -` A1 = Inl -` A2 \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
    1.76 +unfolding rel_set_rel_sum rel_set_eq ..
    1.77 +
    1.78 +(* Detailed proofs of commutativity and associativity: *)
    1.79 +theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1"
    1.80 +proof-
    1.81 +  let ?\<theta> = "\<lambda> trA trB. \<exists> tr1 tr2. trA = tr1 \<parallel> tr2 \<and> trB = tr2 \<parallel> tr1"
    1.82 +  {fix trA trB
    1.83 +   assume "?\<theta> trA trB" hence "trA = trB"
    1.84 +   apply (induct rule: dtree_coinduct)
    1.85 +   unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe
    1.86 +     fix tr1 tr2  show "root (tr1 \<parallel> tr2) = root (tr2 \<parallel> tr1)"
    1.87 +     unfolding root_par by (rule Nplus_comm)
    1.88 +   next
    1.89 +     fix n tr1 tr2 assume "Inl n \<in> cont (tr1 \<parallel> tr2)" thus "n \<in> Inl -` (cont (tr2 \<parallel> tr1))"
    1.90 +     unfolding Inl_in_cont_par by auto
    1.91 +   next
    1.92 +     fix n tr1 tr2 assume "Inl n \<in> cont (tr2 \<parallel> tr1)" thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2))"
    1.93 +     unfolding Inl_in_cont_par by auto
    1.94 +   next
    1.95 +     fix tr1 tr2 trA' assume "Inr trA' \<in> cont (tr1 \<parallel> tr2)"
    1.96 +     then obtain tr1' tr2' where "trA' = tr1' \<parallel> tr2'"
    1.97 +     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
    1.98 +     unfolding Inr_in_cont_par by auto
    1.99 +     thus "\<exists> trB' \<in> Inr -` (cont (tr2 \<parallel> tr1)). ?\<theta> trA' trB'"
   1.100 +     apply(intro bexI[of _ "tr2' \<parallel> tr1'"]) unfolding Inr_in_cont_par by auto
   1.101 +   next
   1.102 +     fix tr1 tr2 trB' assume "Inr trB' \<in> cont (tr2 \<parallel> tr1)"
   1.103 +     then obtain tr1' tr2' where "trB' = tr2' \<parallel> tr1'"
   1.104 +     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
   1.105 +     unfolding Inr_in_cont_par by auto
   1.106 +     thus "\<exists> trA' \<in> Inr -` (cont (tr1 \<parallel> tr2)). ?\<theta> trA' trB'"
   1.107 +     apply(intro bexI[of _ "tr1' \<parallel> tr2'"]) unfolding Inr_in_cont_par by auto
   1.108 +   qed
   1.109 +  }
   1.110 +  thus ?thesis by blast
   1.111 +qed
   1.112 +
   1.113 +lemma par_assoc: "(tr1 \<parallel> tr2) \<parallel> tr3 = tr1 \<parallel> (tr2 \<parallel> tr3)"
   1.114 +proof-
   1.115 +  let ?\<theta> =
   1.116 +  "\<lambda> trA trB. \<exists> tr1 tr2 tr3. trA = (tr1 \<parallel> tr2) \<parallel> tr3 \<and> trB = tr1 \<parallel> (tr2 \<parallel> tr3)"
   1.117 +  {fix trA trB
   1.118 +   assume "?\<theta> trA trB" hence "trA = trB"
   1.119 +   apply (induct rule: dtree_coinduct)
   1.120 +   unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe
   1.121 +     fix tr1 tr2 tr3  show "root ((tr1 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))"
   1.122 +     unfolding root_par by (rule Nplus_assoc)
   1.123 +   next
   1.124 +     fix n tr1 tr2 tr3 assume "Inl n \<in> (cont ((tr1 \<parallel> tr2) \<parallel> tr3))"
   1.125 +     thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2 \<parallel> tr3))" unfolding Inl_in_cont_par by simp
   1.126 +   next
   1.127 +     fix n tr1 tr2 tr3 assume "Inl n \<in> (cont (tr1 \<parallel> tr2 \<parallel> tr3))"
   1.128 +     thus "n \<in> Inl -` (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" unfolding Inl_in_cont_par by simp
   1.129 +   next
   1.130 +     fix trA' tr1 tr2 tr3 assume "Inr trA' \<in> cont ((tr1 \<parallel> tr2) \<parallel> tr3)"
   1.131 +     then obtain tr1' tr2' tr3' where "trA' = (tr1' \<parallel> tr2') \<parallel> tr3'"
   1.132 +     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
   1.133 +     and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto
   1.134 +     thus "\<exists> trB' \<in> Inr -` (cont (tr1 \<parallel> tr2 \<parallel> tr3)). ?\<theta> trA' trB'"
   1.135 +     apply(intro bexI[of _ "tr1' \<parallel> tr2' \<parallel> tr3'"])
   1.136 +     unfolding Inr_in_cont_par by auto
   1.137 +   next
   1.138 +     fix trB' tr1 tr2 tr3 assume "Inr trB' \<in> cont (tr1 \<parallel> tr2 \<parallel> tr3)"
   1.139 +     then obtain tr1' tr2' tr3' where "trB' = tr1' \<parallel> (tr2' \<parallel> tr3')"
   1.140 +     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
   1.141 +     and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto
   1.142 +     thus "\<exists> trA' \<in> Inr -` cont ((tr1 \<parallel> tr2) \<parallel> tr3). ?\<theta> trA' trB'"
   1.143 +     apply(intro bexI[of _ "(tr1' \<parallel> tr2') \<parallel> tr3'"])
   1.144 +     unfolding Inr_in_cont_par by auto
   1.145 +   qed
   1.146 +  }
   1.147 +  thus ?thesis by blast
   1.148 +qed
   1.149 +
   1.150 +end