From e46f2d7af0bf74b1c70f661661ead2172c74c4a4 Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Date: Sun, 28 Apr 2019 00:32:29 +1000
Subject: [PATCH] lib: add graph_of_SomeD

---
 lib/Lib.thy | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/lib/Lib.thy b/lib/Lib.thy
index cb18c5d2d..83a10ce99 100644
--- a/lib/Lib.thy
+++ b/lib/Lib.thy
@@ -764,6 +764,11 @@ lemma graph_of_empty :
 lemma graph_of_in_ranD: "\<forall>y \<in> ran f. P y \<Longrightarrow> (x,y) \<in> graph_of f \<Longrightarrow> P y"
   by (auto simp: graph_of_def ran_def)
 
+lemma graph_of_SomeD:
+  "\<lbrakk> graph_of f \<subseteq> graph_of g; f x = Some y \<rbrakk> \<Longrightarrow> g x = Some y"
+  unfolding graph_of_def
+  by auto
+
 lemma in_set_zip_refl :
   "(x,y) \<in> set (zip xs xs) = (y = x \<and> x \<in> set xs)"
   by (induct xs) auto