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

lib+crefine: zipWith lemma [simp] consolidation 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-01-24 16:04:56 +11:00
parent 40dc7eaa01
commit 6bf7c92d22
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
6 changed files with 2 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Monad_Lists.thy
View File

@ -208,7 +208,7 @@ lemma zipWithM_One:
"zipWithM f (x#xs) [a] = (do z \<leftarrow> f x a; return [z] od)"
by (simp add: zipWithM_def zipWith_def sequence_def)
lemma zipWithM_x_Nil:
lemma zipWithM_x_Nil[simp]:
"zipWithM_x f xs [] = return ()"
by (simp add: zipWithM_x_def zipWith_def sequence_x_def)
@ -333,8 +333,6 @@ lemma mapM_map_simp:
apply (simp add: mapM_Cons)
done
lemmas zipWithM_x_Nil2 = zipWithM_x_Nil (* FIXME lib: eliminate, make the original [simp] *)
lemma filterM_voodoo:
"\<forall>ys. P ys (do zs \<leftarrow> filterM m xs; return (ys @ zs) od)
\<Longrightarrow> P [] (filterM m xs)"

2
lib/Monads/Monad_Lib.thy
View File

@ -46,7 +46,7 @@ definition
zipWith :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
"zipWith f xs ys \<equiv> map (case_prod f) (zip xs ys)"
lemma zipWith_Nil2 :
lemma zipWith_Nil[simp]:
"zipWith f xs [] = []"
unfolding zipWith_def by simp

4
proof/crefine/ARM/Ipc_C.thy
View File

@ -1204,10 +1204,6 @@ shows
apply (auto split: if_split)
done
declare zipWith_Nil2[simp]
declare zipWithM_x_Nil2[simp]
lemma asUser_tcbFault_obj_at:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> asUser t' m
\<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"

4
proof/crefine/ARM_HYP/Ipc_C.thy
View File

@ -1421,10 +1421,6 @@ shows
apply (auto split: if_split)
done
declare zipWith_Nil2[simp]
declare zipWithM_x_Nil2[simp]
lemma getRestartPC_ccorres [corres]:
"ccorres (=) ret__unsigned_long_' \<top>
(UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs

4
proof/crefine/RISCV64/Ipc_C.thy
View File

@ -1345,10 +1345,6 @@ shows
apply (auto split: if_split)
done
declare zipWith_Nil2[simp]
declare zipWithM_x_Nil2[simp]
lemma getRestartPC_ccorres [corres]:
"ccorres (=) ret__unsigned_long_' \<top>
(UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs

4
proof/crefine/X64/Ipc_C.thy
View File

@ -1353,10 +1353,6 @@ shows
apply (auto split: if_split)
done
declare zipWith_Nil2[simp]
declare zipWithM_x_Nil2[simp]
lemma getRestartPC_ccorres [corres]:
"ccorres (=) ret__unsigned_long_' \<top>
(UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs