From 4cc9a1fb1921557dae70fe9368118bdc7c4bc4d5 Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Date: Tue, 30 Jul 2019 15:39:19 +1000
Subject: [PATCH] lib: add option_Some_value_independent

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

diff --git a/lib/Lib.thy b/lib/Lib.thy
index 67edd869a..4c41723e4 100644
--- a/lib/Lib.thy
+++ b/lib/Lib.thy
@@ -2507,6 +2507,10 @@ lemma rsubst:
 lemma ex_impE: "((\<exists>x. P x) \<longrightarrow> Q) \<Longrightarrow> P x \<Longrightarrow> Q"
   by blast
 
+lemma option_Some_value_independent:
+  "\<lbrakk> f x = Some v; \<And>v'. f x = Some v' \<Longrightarrow> f y = Some v' \<rbrakk> \<Longrightarrow> f y = Some v"
+  by blast
+
 text \<open>Some int bitwise lemmas. Helpers for proofs about \<^file>\<open>NatBitwise.thy\<close>\<close>
 lemma int_2p_eq_shiftl:
   "(2::int)^x = 1 << x"