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