equal
deleted
inserted
replaced
493 by blast |
493 by blast |
494 |
494 |
495 |
495 |
496 (*** Bounding theorems ***) |
496 (*** Bounding theorems ***) |
497 |
497 |
498 lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)" |
498 lemma dprod_Sigma: "(dprod (A \<times> B) (C \<times> D)) <= (uprod A C) \<times> (uprod B D)" |
499 by blast |
499 by blast |
500 |
500 |
501 lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma] |
501 lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma] |
502 |
502 |
503 (*Dependent version*) |
503 (*Dependent version*) |
504 lemma dprod_subset_Sigma2: |
504 lemma dprod_subset_Sigma2: |
505 "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))" |
505 "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))" |
506 by auto |
506 by auto |
507 |
507 |
508 lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)" |
508 lemma dsum_Sigma: "(dsum (A \<times> B) (C \<times> D)) <= (usum A C) \<times> (usum B D)" |
509 by blast |
509 by blast |
510 |
510 |
511 lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma] |
511 lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma] |
512 |
512 |
513 |
513 |