src/HOL/Prod.ML
changeset 8255 38f96394c099
parent 8157 b1a458416c92
child 8261 e4726ac0863a
equal deleted inserted replaced
8254:84a5fe44520f 8255:38f96394c099
   464 
   464 
   465 Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
   465 Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
   466 by (Blast_tac 1);
   466 by (Blast_tac 1);
   467 qed "Sigma_Union";
   467 qed "Sigma_Union";
   468 
   468 
       
   469 (*Non-dependent versions are needed to avoid the need for higher-order
       
   470   matching, especially when the rules are re-oriented*)
       
   471 Goal "(A Un B) Times C = (A Times C) Un (B Times C)";
       
   472 by (Blast_tac 1);
       
   473 qed "Times_Un_distrib1"; 
       
   474 
       
   475 Goal "(A Int B) Times C = (A Times C) Int (B Times C)";
       
   476 by (Blast_tac 1);
       
   477 qed "Times_Int_distrib1"; 
       
   478 
       
   479 Goal "(A - B) Times C = (A Times C) - (B Times C)";
       
   480 by (Blast_tac 1);
       
   481 qed "Times_Diff_distrib1"; 
   469 
   482 
   470 (** Exhaustion rule for unit -- a degenerate form of induction **)
   483 (** Exhaustion rule for unit -- a degenerate form of induction **)
   471 
   484 
   472 Goalw [Unity_def]
   485 Goalw [Unity_def]
   473     "u = ()";
   486     "u = ()";