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

lib: remove eq_restrict_map_None from the simp set 

Hotfix for a7ed68e75d, which moved some lemmas from X64 Move_C.thy into
Lib. `eq_restrict_map_None` being in the simp set caused several
breakages across other arches.

Signed-off-by: Victor Phan <Victor.Phan@data61.csiro.au>
This commit is contained in:
Victor Phan 2020-04-23 11:40:38 +10:00
parent 306fe017c3
commit 51ff27cce6
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Lib.thy
View File

@ -1784,12 +1784,12 @@ lemma the_the_inv_mapI:
"inj_on m (dom m) \<Longrightarrow> m x = Some y \<Longrightarrow> the (the_inv_map m y) = x"
by (auto simp: the_inv_map_def ran_def inj_on_def dom_def)
lemma eq_restrict_map_None[simp]:
lemma eq_restrict_map_None:
"restrict_map m A x = None \<longleftrightarrow> x ~: (A \<inter> dom m)"
by (auto simp: restrict_map_def split: if_split_asm)
lemma eq_the_inv_map_None[simp]: "the_inv_map m x = None \<longleftrightarrow> x\<notin>ran m"
by (simp add: the_inv_map_def2)
by (simp add: the_inv_map_def2 eq_restrict_map_None)
lemma is_inv_unique:
"is_inv f g \<Longrightarrow> is_inv f h \<Longrightarrow> g=h"