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