src/HOL/Sum.ML
changeset 2922 580647a879cf
parent 2891 d8f254ad1ab9
child 3091 9366415b93ad
equal deleted inserted replaced
2921:aee40b88a0ad 2922:580647a879cf
   183 goalw Sum.thy [Part_def] "Part A h <= A";
   183 goalw Sum.thy [Part_def] "Part A h <= A";
   184 by (rtac Int_lower1 1);
   184 by (rtac Int_lower1 1);
   185 qed "Part_subset";
   185 qed "Part_subset";
   186 
   186 
   187 goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
   187 goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
   188 by (Fast_tac 1);
   188 by (Blast_tac 1);
   189 qed "Part_mono";
   189 qed "Part_mono";
   190 
   190 
   191 val basic_monos = basic_monos @ [Part_mono];
   191 val basic_monos = basic_monos @ [Part_mono];
   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";
   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 (Fast_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 (Fast_tac 1);
   207 by (Blast_tac 1);
   208 qed "Part_Collect";
   208 qed "Part_Collect";