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

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>
This commit is contained in:
Gerwin Klein 2022-06-06 11:31:25 +10:00 committed by Gerwin Klein
parent 53e724808f
commit ff1688e753
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
lib/Lib.thy
View File

@ -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)