1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7theory MoreHOL
8imports Main
9begin
10
11(*
12 * Simplification of a common pattern that comes out of
13 * expansions of "corres_underlying".
14 *)
15lemma tuple_relation_to_function [simp]: "((a, b) \<in> {(s, s'). f s' = s}) = (a = f b)"
16  by auto
17
18end
19