src/HOL/Sum.ML
changeset 3842 b55686a7b22c
parent 3091 9366415b93ad
child 4089 96fba19bcbe2
equal deleted inserted replaced
3841:22bbc1676768 3842:b55686a7b22c
   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";