src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy
 changeset 55938 f20d1db5aa3c parent 55075 b3d0a02a756d child 55943 5c2df04e97d1
```     1.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy	Thu Mar 06 14:25:55 2014 +0100
1.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy	Thu Mar 06 14:57:14 2014 +0100
1.3 @@ -67,10 +67,10 @@
1.4
1.5  subsection{* Structural Coinduction Proofs *}
1.6
1.7 -lemma set_rel_sum_rel_eq[simp]:
1.8 -"set_rel (sum_rel (op =) \<phi>) A1 A2 \<longleftrightarrow>
1.9 - Inl -` A1 = Inl -` A2 \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
1.10 -unfolding set_rel_sum_rel set_rel_eq ..
1.11 +lemma rel_set_sum_rel_eq[simp]:
1.12 +"rel_set (sum_rel (op =) \<phi>) A1 A2 \<longleftrightarrow>
1.13 + Inl -` A1 = Inl -` A2 \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
1.14 +unfolding rel_set_sum_rel rel_set_eq ..
1.15
1.16  (* Detailed proofs of commutativity and associativity: *)
1.17  theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1"
1.18 @@ -79,7 +79,7 @@
1.19    {fix trA trB
1.20     assume "?\<theta> trA trB" hence "trA = trB"
1.21     apply (induct rule: dtree_coinduct)
1.22 -   unfolding set_rel_sum_rel set_rel_eq unfolding set_rel_def proof safe
1.23 +   unfolding rel_set_sum_rel rel_set_eq unfolding rel_set_def proof safe
1.24       fix tr1 tr2  show "root (tr1 \<parallel> tr2) = root (tr2 \<parallel> tr1)"
1.25       unfolding root_par by (rule Nplus_comm)
1.26     next
1.27 @@ -114,7 +114,7 @@
1.28    {fix trA trB
1.29     assume "?\<theta> trA trB" hence "trA = trB"
1.30     apply (induct rule: dtree_coinduct)
1.31 -   unfolding set_rel_sum_rel set_rel_eq unfolding set_rel_def proof safe
1.32 +   unfolding rel_set_sum_rel rel_set_eq unfolding rel_set_def proof safe
1.33       fix tr1 tr2 tr3  show "root ((tr1 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))"
1.34       unfolding root_par by (rule Nplus_assoc)
1.35     next
```