src/ZF/QPair.ML
changeset 790 4c10e8532d43
parent 782 200a16083201
child 1096 6c177c4c2127
equal deleted inserted replaced
789:30bdc59198ff 790:4c10e8532d43
   123     (assume_tac 1) ]);
   123     (assume_tac 1) ]);
   124 
   124 
   125 val qconverse_cs = qpair_cs addSIs [qconverseI] 
   125 val qconverse_cs = qpair_cs addSIs [qconverseI] 
   126 			    addSEs [qconverseD,qconverseE];
   126 			    addSEs [qconverseD,qconverseE];
   127 
   127 
   128 qed_goal "qconverse_of_qconverse" QPair.thy
   128 qed_goal "qconverse_qconverse" QPair.thy
   129     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
   129     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
   130  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   130  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   131 
   131 
   132 qed_goal "qconverse_type" QPair.thy
   132 qed_goal "qconverse_type" QPair.thy
   133     "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
   133     "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
   134  (fn _ => [ (fast_tac qconverse_cs 1) ]);
   134  (fn _ => [ (fast_tac qconverse_cs 1) ]);
   135 
   135 
   136 qed_goal "qconverse_of_prod" QPair.thy "qconverse(A <*> B) = B <*> A"
   136 qed_goal "qconverse_prod" QPair.thy "qconverse(A <*> B) = B <*> A"
   137  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   137  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   138 
   138 
   139 qed_goal "qconverse_empty" QPair.thy "qconverse(0) = 0"
   139 qed_goal "qconverse_empty" QPair.thy "qconverse(0) = 0"
   140  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   140  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   141 
   141