equal
deleted
inserted
replaced
123 "((A ===> B) ===> rel_set A ===> rel_set B) image image" |
123 "((A ===> B) ===> rel_set A ===> rel_set B) image image" |
124 unfolding rel_fun_def rel_set_def by simp fast |
124 unfolding rel_fun_def rel_set_def by simp fast |
125 |
125 |
126 lemma UNION_transfer [transfer_rule]: |
126 lemma UNION_transfer [transfer_rule]: |
127 "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION" |
127 "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION" |
128 unfolding SUP_def [abs_def] by transfer_prover |
128 unfolding Union_image_eq [symmetric, abs_def] by transfer_prover |
129 |
129 |
130 lemma Ball_transfer [transfer_rule]: |
130 lemma Ball_transfer [transfer_rule]: |
131 "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball" |
131 "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball" |
132 unfolding rel_set_def rel_fun_def by fast |
132 unfolding rel_set_def rel_fun_def by fast |
133 |
133 |