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

lib: make some elimination rules safer 

Elimination against the pattern "P v", where both "P" and "v" are free,
can loop, if the rule is marked as a safe elimination rule. In the rules
modified in this commit, variable "v" provides no real benefit, so we
replace the pattern with "P".
This commit is contained in:
Matthew Brecknell 2017-11-22 10:36:59 +11:00
parent 70de40bcdd
commit 0570943ee8
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
lib/Monad_WP/OptionMonad.thy
View File

@ -159,7 +159,7 @@ lemma in_oreturn [simp]:
by (auto simp: oreturn_def K_def)
lemma oreturnE:
"\<lbrakk>oreturn x s = Some v; v = x \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P v"
"\<lbrakk>oreturn x s = Some v; v = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by simp
lemma in_ofail [simp]:
@ -192,7 +192,7 @@ lemma in_othrow_eq [simp]:
by (auto simp: othrow_def K_def)
lemma othrowE:
"\<lbrakk>othrow e s = Some v; v = Inl e \<Longrightarrow> P (Inl e)\<rbrakk> \<Longrightarrow> P v"
"\<lbrakk>othrow e s = Some v; v = Inl e \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by simp
lemma in_oreturnOk_eq [simp]:
@ -200,7 +200,7 @@ lemma in_oreturnOk_eq [simp]:
by (auto simp: oreturnOk_def K_def)
lemma oreturnOkE:
"\<lbrakk>oreturnOk x s = Some v; v = Inr x \<Longrightarrow> P (Inr x)\<rbrakk> \<Longrightarrow> P v"
"\<lbrakk>oreturnOk x s = Some v; v = Inr x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by simp
lemmas omonadE [elim!] =