src/HOL/Univ.ML
changeset 8703 816d8f6513be
parent 8292 93e125b21220
child 8709 483a3eb96c7e
equal deleted inserted replaced
8702:78b7010db847 8703:816d8f6513be
   580 qed "dsum_mono";
   580 qed "dsum_mono";
   581 
   581 
   582 
   582 
   583 (*** Bounding theorems ***)
   583 (*** Bounding theorems ***)
   584 
   584 
   585 Goal "(dprod (A Times B) (C Times D)) <= (uprod A C) Times (uprod B D)";
   585 Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)";
   586 by (Blast_tac 1);
   586 by (Blast_tac 1);
   587 qed "dprod_Sigma";
   587 qed "dprod_Sigma";
   588 
   588 
   589 val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
   589 val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
   590 
   590 
   593 by Safe_tac;
   593 by Safe_tac;
   594 by (stac Split 1);
   594 by (stac Split 1);
   595 by (Blast_tac 1);
   595 by (Blast_tac 1);
   596 qed "dprod_subset_Sigma2";
   596 qed "dprod_subset_Sigma2";
   597 
   597 
   598 Goal "(dsum (A Times B) (C Times D)) <= (usum A C) Times (usum B D)";
   598 Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)";
   599 by (Blast_tac 1);
   599 by (Blast_tac 1);
   600 qed "dsum_Sigma";
   600 qed "dsum_Sigma";
   601 
   601 
   602 val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
   602 val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
   603 
   603