equal
deleted
inserted
replaced
192 |
192 |
193 goalw Sum.thy [Part_def] "!!a. a : Part A h ==> a : A"; |
193 goalw Sum.thy [Part_def] "!!a. a : Part A h ==> a : A"; |
194 by (etac IntD1 1); |
194 by (etac IntD1 1); |
195 qed "PartD1"; |
195 qed "PartD1"; |
196 |
196 |
197 goal Sum.thy "Part A (%x.x) = A"; |
197 goal Sum.thy "Part A (%x. x) = A"; |
198 by (Blast_tac 1); |
198 by (Blast_tac 1); |
199 qed "Part_id"; |
199 qed "Part_id"; |
200 |
200 |
201 goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)"; |
201 goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)"; |
202 by (Blast_tac 1); |
202 by (Blast_tac 1); |
203 qed "Part_Int"; |
203 qed "Part_Int"; |
204 |
204 |
205 (*For inductive definitions*) |
205 (*For inductive definitions*) |
206 goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}"; |
206 goal Sum.thy "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}"; |
207 by (Blast_tac 1); |
207 by (Blast_tac 1); |
208 qed "Part_Collect"; |
208 qed "Part_Collect"; |