src/HOL/Lifting_Set.thy
changeset 57599 7ef939f89776
parent 57129 7edb7550663e
child 58104 c5316f843f72
     1.1 --- a/src/HOL/Lifting_Set.thy	Mon Jul 21 17:51:11 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Mon Jul 21 17:51:29 2014 +0200
     1.3 @@ -266,6 +266,12 @@
     1.4    shows "((A ===> B) ===> rel_set B ===> rel_set A) vimage vimage"
     1.5    unfolding vimage_def[abs_def] by transfer_prover
     1.6  
     1.7 +lemma Image_parametric [transfer_rule]:
     1.8 +  assumes "bi_unique A"
     1.9 +  shows "(rel_set (rel_prod A B) ===> rel_set A ===> rel_set B) op `` op ``"
    1.10 +by(intro rel_funI rel_setI)
    1.11 +  (force dest: rel_setD1 bi_uniqueDr[OF assms], force dest: rel_setD2 bi_uniqueDl[OF assms])
    1.12 +
    1.13  end
    1.14  
    1.15  lemma (in comm_monoid_set) F_parametric [transfer_rule]: