src/HOL/Relation.ML
changeset 7913 86be2946bb0b
parent 7822 09aabe6d04b8
child 8004 6273f58ea2c1
equal deleted inserted replaced
7912:0e42be14f136 7913:86be2946bb0b
   373 
   373 
   374 (*NOT suitable for rewriting*)
   374 (*NOT suitable for rewriting*)
   375 Goal "r^^B = (UN y: B. r^^{y})";
   375 Goal "r^^B = (UN y: B. r^^{y})";
   376 by (Blast_tac 1);
   376 by (Blast_tac 1);
   377 qed "Image_eq_UN";
   377 qed "Image_eq_UN";
       
   378 
       
   379 Goal "[| r'<=r; A'<=A |] ==> (r' ^^ A') <= (r ^^ A)";
       
   380 by (Blast_tac 1);
       
   381 qed "Image_mono";
       
   382 
       
   383 Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))";
       
   384 by (Blast_tac 1);
       
   385 qed "Image_UN";
       
   386 
       
   387 (*Converse inclusion fails*)
       
   388 Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))";
       
   389 by (Blast_tac 1);
       
   390 qed "Image_INT_subset";
   378 
   391 
   379 
   392 
   380 section "Univalent";
   393 section "Univalent";
   381 
   394 
   382 Goalw [Univalent_def]
   395 Goalw [Univalent_def]