equal
deleted
inserted
replaced
162 lemma sndOp_in: "ac \<in> Collect (case_prod (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (case_prod Q)" |
162 lemma sndOp_in: "ac \<in> Collect (case_prod (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (case_prod Q)" |
163 unfolding sndOp_def mem_Collect_eq |
163 unfolding sndOp_def mem_Collect_eq |
164 by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2]) |
164 by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2]) |
165 |
165 |
166 lemma csquare_fstOp_sndOp: |
166 lemma csquare_fstOp_sndOp: |
167 "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" |
167 "csquare (Collect (f (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" |
168 unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp |
168 unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp |
169 |
169 |
170 lemma snd_fst_flip: "snd xy = (fst \<circ> (%(x, y). (y, x))) xy" |
170 lemma snd_fst_flip: "snd xy = (fst \<circ> (%(x, y). (y, x))) xy" |
171 by (simp split: prod.split) |
171 by (simp split: prod.split) |
172 |
172 |