Some changes for Lib, December '24 edition
#845
Conversation
lib/Monad_Lists.thy
Outdated
| "\<lbrace>\<lambda>s. \<forall>vs. map (\<lambda>t. f t s) ts = map Some vs \<longrightarrow> P vs s\<rbrace> | ||
| mapM (gets_the \<circ> f) ts | ||
| \<lbrace>P\<rbrace>" | ||
| unfolding comp_def |
There was a problem hiding this comment.
@lsf37 edge case for indentation, where does this one go? it's a new one for me
There was a problem hiding this comment.
I was going to say this is correct as is, but it is true that we usually put unfolding on the same indent as apply. That would probably look weird here. What does the Isabelle auto indenter do?
There was a problem hiding this comment.
The auto indenter indents this by 2 spaces. Sigh. I'll cancel the tests that are running and push an update
There was a problem hiding this comment.
Feel free to ignore if you don't want to keep on fiddling with this, but I imagine that the unfold isn't needed in the Nil case, and if that's right you could just add comp_def to the simp in the Cons case and possibly avoid fighting with the indentation at all.
There was a problem hiding this comment.
It does seem necessary in both cases, and even adding it to the simp in wpsimp in both cases doesn't work. So I just went with the unfolding. If this is suspicious, I can look into it further
There was a problem hiding this comment.
Huh, that seems unexpected to me but not enough to be worth further investigation.
There was a problem hiding this comment.
Yeah. If you want to sweep it under the rug, you can put a unfold ..., before the induct in proof, otherwise yeah just do what auto-indenter does it this case, it's a really rare event it seems.
Done in order to avoid unwanted interactions with comp_apply Signed-off-by: Michael McInerney <[email protected]>
Done in order to avoid unwanted simplification of heaps which are defined via multiple uses of opt_map_Some Signed-off-by: Michael McInerney <[email protected]>
This rule is no longer needed, now that opt_map_Some is not defined in terms of comp Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
force-pushed
the
michaelm-rules_for_Lib_Dec24
branch
from
96a3752 to
62292f3
Compare
These are some changes that cropped up during my work for
sorted_ipc_queuesfor MCS.I would recommend reviewing commit-by-commit, so that unrelated changes appearing in the same file can be considered individually.