From ff1688e753b2b96b5b0d036e1fce334dd0910d5f Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Mon, 6 Jun 2022 11:31:25 +1000
Subject: [PATCH] lib: better automation of dom equality

Domain equality is nice to state and sometimes nice to prove, but it is
hard to use in automation (fastforce/auto). The new phrasing here is not
as nice to read, but useful in automation.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 lib/Lib.thy | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/lib/Lib.thy b/lib/Lib.thy
index 86e7ffc59..715e13ead 100644
--- a/lib/Lib.thy
+++ b/lib/Lib.thy
@@ -2012,6 +2012,11 @@ lemma dom_eqD:
   "\<lbrakk> f x = Some v; dom f = S \<rbrakk> \<Longrightarrow> x \<in> S"
   by clarsimp
 
+lemma dom_eq_All:
+  "dom f = dom f' \<Longrightarrow>
+   (\<forall>x. f x = None \<longrightarrow> f' x = None) \<and> (\<forall>x v. f x = Some v \<longrightarrow> (\<exists>v'. f' x = Some v'))"
+  by auto
+
 lemma exception_set_finite1:
   "finite {x. P x} \<Longrightarrow> finite {x. (x = y \<longrightarrow> Q x) \<and> P x}"
   by (simp add: Collect_conj_eq)