adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: additional is_inv lemmas 

Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-07-25 18:17:54 +10:00 committed by Gerwin Klein
parent 773f7d52f1
commit 3faced9815
1 changed files with 19 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
lib/Lib.thy
View File

@ -1783,6 +1783,25 @@ lemma is_inv_inj2:
"is_inv f g \<Longrightarrow> inj_on g (dom g)"
using is_inv_com is_inv_inj by blast
lemma is_inv_eq:
"is_inv f g = (\<forall>x y. (f x = Some y) = (g y = Some x))"
proof
assume "\<forall>x y. (f x = Some y) = (g y = Some x)"
thus "is_inv f g" by (auto simp: is_inv_def ran_def)
next
assume "is_inv f g"
moreover
from this have "is_inv g f" by (rule is_inv_com)
ultimately
show "\<forall>x y. (f x = Some y) = (g y = Some x)"
unfolding is_inv_def by blast
qed
lemma is_inv_Some_upd:
"\<lbrakk> is_inv f g; f x = None; g y = None \<rbrakk> \<Longrightarrow> is_inv (f(x \<mapsto> y)) (g(y \<mapsto> x))"
unfolding is_inv_def
by clarsimp
text \<open>Map inversion (implicitly assuming injectivity).\<close>
definition
"the_inv_map m = (\<lambda>s. if s\<in>ran m then Some (THE x. m x = Some s) else None)"