# HG changeset patch
# User wenzelm
# Date 1493035118 -7200
# Node ID 10f4a17e5928b117654045afcba51782878adf5f
# Parent  0f3fdf689bf9f55fe4e5efeb406a10c70a67f3d4
clarified parent session images, to avoid duplicate loading of theories;
avoid name conflict with loaded theory src/HOL/Library/Parallel.thy;

diff -r 0f3fdf689bf9 -r 10f4a17e5928 src/HOL/Datatype_Examples/Derivation_Trees/Parallel.thy
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Parallel.thy	Mon Apr 24 11:52:51 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-(*  Title:      HOL/Datatype_Examples/Derivation_Trees/Parallel.thy
-    Author:     Andrei Popescu, TU Muenchen
-    Copyright   2012
-
-Parallel composition.
-*)
-
-section \<open>Parallel Composition\<close>
-
-theory Parallel
-imports DTree
-begin
-
-no_notation plus_class.plus (infixl "+" 65)
-
-consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60)
-
-axiomatization where
-    Nplus_comm: "(a::N) + b = b + (a::N)"
-and Nplus_assoc: "((a::N) + b) + c = a + (b + c)"
-
-subsection\<open>Corecursive Definition of Parallel Composition\<close>
-
-fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2"
-fun par_c where
-"par_c (tr1,tr2) =
- Inl ` (Inl -` (cont tr1 \<union> cont tr2)) \<union>
- Inr ` (Inr -` cont tr1 \<times> Inr -` cont tr2)"
-
-declare par_r.simps[simp del]  declare par_c.simps[simp del]
-
-definition par :: "dtree \<times> dtree \<Rightarrow> dtree" where
-"par \<equiv> unfold par_r par_c"
-
-abbreviation par_abbr (infixr "\<parallel>" 80) where "tr1 \<parallel> tr2 \<equiv> 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 \<parallel> 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 \<parallel> tr2) = (id \<oplus> 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 \<parallel> tr2)) = Inl -` (cont tr1 \<union> cont tr2)"
-unfolding cont_par par_c.simps by auto
-
-lemma Inr_cont_par[simp]:
-"Inr -` (cont (tr1 \<parallel> tr2)) = par ` (Inr -` cont tr1 \<times> Inr -` cont tr2)"
-unfolding cont_par par_c.simps by auto
-
-lemma Inl_in_cont_par:
-"Inl t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (Inl t \<in> cont tr1 \<or> Inl t \<in> cont tr2)"
-using Inl_cont_par[of tr1 tr2] unfolding vimage_def by auto
-
-lemma Inr_in_cont_par:
-"Inr t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (t \<in> par ` (Inr -` cont tr1 \<times> Inr -` cont tr2))"
-using Inr_cont_par[of tr1 tr2] unfolding vimage_def by auto
-
-
-subsection\<open>Structural Coinduction Proofs\<close>
-
-lemma rel_set_rel_sum_eq[simp]:
-"rel_set (rel_sum (op =) \<phi>) A1 A2 \<longleftrightarrow>
- Inl -` A1 = Inl -` A2 \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
-unfolding rel_set_rel_sum rel_set_eq ..
-
-(* Detailed proofs of commutativity and associativity: *)
-theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1"
-proof-
-  let ?\<theta> = "\<lambda> trA trB. \<exists> tr1 tr2. trA = tr1 \<parallel> tr2 \<and> trB = tr2 \<parallel> tr1"
-  {fix trA trB
-   assume "?\<theta> 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 \<parallel> tr2) = root (tr2 \<parallel> tr1)"
-     unfolding root_par by (rule Nplus_comm)
-   next
-     fix n tr1 tr2 assume "Inl n \<in> cont (tr1 \<parallel> tr2)" thus "n \<in> Inl -` (cont (tr2 \<parallel> tr1))"
-     unfolding Inl_in_cont_par by auto
-   next
-     fix n tr1 tr2 assume "Inl n \<in> cont (tr2 \<parallel> tr1)" thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2))"
-     unfolding Inl_in_cont_par by auto
-   next
-     fix tr1 tr2 trA' assume "Inr trA' \<in> cont (tr1 \<parallel> tr2)"
-     then obtain tr1' tr2' where "trA' = tr1' \<parallel> tr2'"
-     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
-     unfolding Inr_in_cont_par by auto
-     thus "\<exists> trB' \<in> Inr -` (cont (tr2 \<parallel> tr1)). ?\<theta> trA' trB'"
-     apply(intro bexI[of _ "tr2' \<parallel> tr1'"]) unfolding Inr_in_cont_par by auto
-   next
-     fix tr1 tr2 trB' assume "Inr trB' \<in> cont (tr2 \<parallel> tr1)"
-     then obtain tr1' tr2' where "trB' = tr2' \<parallel> tr1'"
-     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
-     unfolding Inr_in_cont_par by auto
-     thus "\<exists> trA' \<in> Inr -` (cont (tr1 \<parallel> tr2)). ?\<theta> trA' trB'"
-     apply(intro bexI[of _ "tr1' \<parallel> tr2'"]) unfolding Inr_in_cont_par by auto
-   qed
-  }
-  thus ?thesis by blast
-qed
-
-lemma par_assoc: "(tr1 \<parallel> tr2) \<parallel> tr3 = tr1 \<parallel> (tr2 \<parallel> tr3)"
-proof-
-  let ?\<theta> =
-  "\<lambda> trA trB. \<exists> tr1 tr2 tr3. trA = (tr1 \<parallel> tr2) \<parallel> tr3 \<and> trB = tr1 \<parallel> (tr2 \<parallel> tr3)"
-  {fix trA trB
-   assume "?\<theta> 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 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))"
-     unfolding root_par by (rule Nplus_assoc)
-   next
-     fix n tr1 tr2 tr3 assume "Inl n \<in> (cont ((tr1 \<parallel> tr2) \<parallel> tr3))"
-     thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2 \<parallel> tr3))" unfolding Inl_in_cont_par by simp
-   next
-     fix n tr1 tr2 tr3 assume "Inl n \<in> (cont (tr1 \<parallel> tr2 \<parallel> tr3))"
-     thus "n \<in> Inl -` (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" unfolding Inl_in_cont_par by simp
-   next
-     fix trA' tr1 tr2 tr3 assume "Inr trA' \<in> cont ((tr1 \<parallel> tr2) \<parallel> tr3)"
-     then obtain tr1' tr2' tr3' where "trA' = (tr1' \<parallel> tr2') \<parallel> tr3'"
-     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
-     and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto
-     thus "\<exists> trB' \<in> Inr -` (cont (tr1 \<parallel> tr2 \<parallel> tr3)). ?\<theta> trA' trB'"
-     apply(intro bexI[of _ "tr1' \<parallel> tr2' \<parallel> tr3'"])
-     unfolding Inr_in_cont_par by auto
-   next
-     fix trB' tr1 tr2 tr3 assume "Inr trB' \<in> cont (tr1 \<parallel> tr2 \<parallel> tr3)"
-     then obtain tr1' tr2' tr3' where "trB' = tr1' \<parallel> (tr2' \<parallel> tr3')"
-     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
-     and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto
-     thus "\<exists> trA' \<in> Inr -` cont ((tr1 \<parallel> tr2) \<parallel> tr3). ?\<theta> trA' trB'"
-     apply(intro bexI[of _ "(tr1' \<parallel> tr2') \<parallel> tr3'"])
-     unfolding Inr_in_cont_par by auto
-   qed
-  }
-  thus ?thesis by blast
-qed
-
-end
diff -r 0f3fdf689bf9 -r 10f4a17e5928 src/HOL/Datatype_Examples/Derivation_Trees/Parallel_Composition.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Parallel_Composition.thy	Mon Apr 24 13:58:38 2017 +0200
@@ -0,0 +1,147 @@
+(*  Title:      HOL/Datatype_Examples/Derivation_Trees/Parallel_Composition.thy
+    Author:     Andrei Popescu, TU Muenchen
+    Copyright   2012
+
+Parallel composition.
+*)
+
+section \<open>Parallel Composition\<close>
+
+theory Parallel_Composition
+imports DTree
+begin
+
+no_notation plus_class.plus (infixl "+" 65)
+
+consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60)
+
+axiomatization where
+    Nplus_comm: "(a::N) + b = b + (a::N)"
+and Nplus_assoc: "((a::N) + b) + c = a + (b + c)"
+
+subsection\<open>Corecursive Definition of Parallel Composition\<close>
+
+fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2"
+fun par_c where
+"par_c (tr1,tr2) =
+ Inl ` (Inl -` (cont tr1 \<union> cont tr2)) \<union>
+ Inr ` (Inr -` cont tr1 \<times> Inr -` cont tr2)"
+
+declare par_r.simps[simp del]  declare par_c.simps[simp del]
+
+definition par :: "dtree \<times> dtree \<Rightarrow> dtree" where
+"par \<equiv> unfold par_r par_c"
+
+abbreviation par_abbr (infixr "\<parallel>" 80) where "tr1 \<parallel> tr2 \<equiv> 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 \<parallel> 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 \<parallel> tr2) = (id \<oplus> 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 \<parallel> tr2)) = Inl -` (cont tr1 \<union> cont tr2)"
+unfolding cont_par par_c.simps by auto
+
+lemma Inr_cont_par[simp]:
+"Inr -` (cont (tr1 \<parallel> tr2)) = par ` (Inr -` cont tr1 \<times> Inr -` cont tr2)"
+unfolding cont_par par_c.simps by auto
+
+lemma Inl_in_cont_par:
+"Inl t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (Inl t \<in> cont tr1 \<or> Inl t \<in> cont tr2)"
+using Inl_cont_par[of tr1 tr2] unfolding vimage_def by auto
+
+lemma Inr_in_cont_par:
+"Inr t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (t \<in> par ` (Inr -` cont tr1 \<times> Inr -` cont tr2))"
+using Inr_cont_par[of tr1 tr2] unfolding vimage_def by auto
+
+
+subsection\<open>Structural Coinduction Proofs\<close>
+
+lemma rel_set_rel_sum_eq[simp]:
+"rel_set (rel_sum (op =) \<phi>) A1 A2 \<longleftrightarrow>
+ Inl -` A1 = Inl -` A2 \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
+unfolding rel_set_rel_sum rel_set_eq ..
+
+(* Detailed proofs of commutativity and associativity: *)
+theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1"
+proof-
+  let ?\<theta> = "\<lambda> trA trB. \<exists> tr1 tr2. trA = tr1 \<parallel> tr2 \<and> trB = tr2 \<parallel> tr1"
+  {fix trA trB
+   assume "?\<theta> 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 \<parallel> tr2) = root (tr2 \<parallel> tr1)"
+     unfolding root_par by (rule Nplus_comm)
+   next
+     fix n tr1 tr2 assume "Inl n \<in> cont (tr1 \<parallel> tr2)" thus "n \<in> Inl -` (cont (tr2 \<parallel> tr1))"
+     unfolding Inl_in_cont_par by auto
+   next
+     fix n tr1 tr2 assume "Inl n \<in> cont (tr2 \<parallel> tr1)" thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2))"
+     unfolding Inl_in_cont_par by auto
+   next
+     fix tr1 tr2 trA' assume "Inr trA' \<in> cont (tr1 \<parallel> tr2)"
+     then obtain tr1' tr2' where "trA' = tr1' \<parallel> tr2'"
+     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
+     unfolding Inr_in_cont_par by auto
+     thus "\<exists> trB' \<in> Inr -` (cont (tr2 \<parallel> tr1)). ?\<theta> trA' trB'"
+     apply(intro bexI[of _ "tr2' \<parallel> tr1'"]) unfolding Inr_in_cont_par by auto
+   next
+     fix tr1 tr2 trB' assume "Inr trB' \<in> cont (tr2 \<parallel> tr1)"
+     then obtain tr1' tr2' where "trB' = tr2' \<parallel> tr1'"
+     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
+     unfolding Inr_in_cont_par by auto
+     thus "\<exists> trA' \<in> Inr -` (cont (tr1 \<parallel> tr2)). ?\<theta> trA' trB'"
+     apply(intro bexI[of _ "tr1' \<parallel> tr2'"]) unfolding Inr_in_cont_par by auto
+   qed
+  }
+  thus ?thesis by blast
+qed
+
+lemma par_assoc: "(tr1 \<parallel> tr2) \<parallel> tr3 = tr1 \<parallel> (tr2 \<parallel> tr3)"
+proof-
+  let ?\<theta> =
+  "\<lambda> trA trB. \<exists> tr1 tr2 tr3. trA = (tr1 \<parallel> tr2) \<parallel> tr3 \<and> trB = tr1 \<parallel> (tr2 \<parallel> tr3)"
+  {fix trA trB
+   assume "?\<theta> 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 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))"
+     unfolding root_par by (rule Nplus_assoc)
+   next
+     fix n tr1 tr2 tr3 assume "Inl n \<in> (cont ((tr1 \<parallel> tr2) \<parallel> tr3))"
+     thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2 \<parallel> tr3))" unfolding Inl_in_cont_par by simp
+   next
+     fix n tr1 tr2 tr3 assume "Inl n \<in> (cont (tr1 \<parallel> tr2 \<parallel> tr3))"
+     thus "n \<in> Inl -` (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" unfolding Inl_in_cont_par by simp
+   next
+     fix trA' tr1 tr2 tr3 assume "Inr trA' \<in> cont ((tr1 \<parallel> tr2) \<parallel> tr3)"
+     then obtain tr1' tr2' tr3' where "trA' = (tr1' \<parallel> tr2') \<parallel> tr3'"
+     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
+     and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto
+     thus "\<exists> trB' \<in> Inr -` (cont (tr1 \<parallel> tr2 \<parallel> tr3)). ?\<theta> trA' trB'"
+     apply(intro bexI[of _ "tr1' \<parallel> tr2' \<parallel> tr3'"])
+     unfolding Inr_in_cont_par by auto
+   next
+     fix trB' tr1 tr2 tr3 assume "Inr trB' \<in> cont (tr1 \<parallel> tr2 \<parallel> tr3)"
+     then obtain tr1' tr2' tr3' where "trB' = tr1' \<parallel> (tr2' \<parallel> tr3')"
+     and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
+     and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto
+     thus "\<exists> trA' \<in> Inr -` cont ((tr1 \<parallel> tr2) \<parallel> tr3). ?\<theta> trA' trB'"
+     apply(intro bexI[of _ "(tr1' \<parallel> tr2') \<parallel> tr3'"])
+     unfolding Inr_in_cont_par by auto
+   qed
+  }
+  thus ?thesis by blast
+qed
+
+end
diff -r 0f3fdf689bf9 -r 10f4a17e5928 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Apr 24 11:52:51 2017 +0200
+++ b/src/HOL/ROOT	Mon Apr 24 13:58:38 2017 +0200
@@ -812,20 +812,18 @@
     "root.tex"
     "root.bib"
 
-session "HOL-Datatype_Examples" (timing) in Datatype_Examples = HOL +
+session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
   description {*
     (Co)datatype Examples.
   *}
   options [document = false]
-  sessions
-    "HOL-Library"
   theories
     Compat
     Lambda_Term
     Process
     TreeFsetI
     "Derivation_Trees/Gram_Lang"
-    "Derivation_Trees/Parallel"
+    "Derivation_Trees/Parallel_Composition"
     Koenig
     Lift_BNF
     Milner_Tofte