This holds for any type that supports the size function, in particular all datatypes (length is an abbreviation for size on lists). I'd also suggest a different name, maybe:

lemma wf_fst_size:
  "wf {((r :: 'b :: size, s :: 'a), (r', s')). size r < size r'}"
  apply (insert wf_inv_image[where r="{(m, n). m < n}" and f="λ(r :: 'b, s :: 'a). size r"])

This lemma was just moved from Refine, so I was hesitant to change the name, but I can do that and make it support size.

Right, the punishment for good deeds is swift sometimes :-). If it's old, then let's maybe go with a nice name for the lemma and a lemmas old_name = new_name statement afterwards with a FIXME for cleanup later. It will still be directly applicable to length, so nothing else should need to change.

You can supply a method to monadic_rewrite_symb_exec_l, in this case <wpsimp wp: get_object_wp set_object_wp> should work, which would save you the line later and the need for a + hopefully.

Adding newlines, while it looks other text bits don't have them (same after monadic_rewrite_noop) above. Might be that an argument to have sections instead makes sense, but I'm not sure if this file does that.

This does sort of have sections that are begun with text lines. I'm not sure whether that qualifies as something where we'd like the two newlines before a new section. I followed the same approach for the RCorres file, actually, so maybe we should decide

This rule seems unusual, can you say why the add_noop_lhs rules are not good enough here? Is it due to having to go forwards in some proof? But then why the equivalence? Also, the name doesn't fit with the other rules, all the other ones refer to adding "noop" for return, which is certainly a choice, but good to be consistent.

The noop_rhs rules will assume that the function to which we'd like to add the return will itself have unit as the return type. Here I'm wanting something more general. The fact that we have dc as the return relation means that we are free to disregard the value that's returned.

you can one-line this, or two-line this (assuming semicolon-unfriendliness here):

by (rule no_fail_pre)
   (fastforce intro: no_fail_grab_asm)+

I think you can combine these fastforces into one and semicolon it if you want to reduce size, but this is also ok

looking at this and the non-strong version, it takes a fair bit of cognitive power to figure out the difference, maybe a comment to point future readers to would help?

Sure, I can do that.

is there a non-prime version of this somewhere?

Yep, there is. I think it's currently unused (at least once the IPC queues work is merged), so I could remove it (maybe later).

I don't get it; the mapM_gets_the_wp with comp_def expanded only ends up having a different precondition. This means that either this precondition implies that one, or vice versa, or they're equivalent. So I'd expect one of these to become a one-liner weakening of the other, without a need for duplicating the induction proof.

Good point. I can get the original version as a one-line proof from this new version (the other way around doesn't work). Thanks

would it make any sense to make the in_inv_by_hoareD an instantiation of this one via lemmas? I'm ok keeping it like this in this case, as it's not much longer and shows the lemma

I did think about that, but wasn't sure whether I should mess with ancient rules like that one. I can try that out if people have a preference for the lemmas statement.

; fastforce intro: whileLoop_terminates.intros ?

That does work. The old proof is slightly more "informative" in that it tells you which of those rules is used for which case. I sort of like that for these Lib rules, but I can definitely go with this.

this name is strange... it's similar to the idea behind the rule context_conjI but under an exists... I'd suggest hoeare_ex_context_conj or something like that

wow, surprised this isn't in HOL

There's split_list, which is x ∈ set xs ⟹ ∃ys zs. xs = ys @ x # zs, but I wanted this version for some godforsaken reason I have now forgotten (but which I can investigate if you'd like).

I think it's fine, but maybe throw in a (* split_list uses x # *) or something

Damn, github won't let me type x space #

Did you guys already discuss naming of this? I've heard of queues before, and of doubly-linked lists, but have never heard of a "head end list". I think the comment is confusing me more than it helps; maybe it's just too contracted. We're defining a datatype here that only has two potential "pointers" in it, and then we're relating that concept to a queue, which is a kind of extraction of a list by following the pointers in memory? Is that right? If it is, then the name makes sense, but it's a lot to intuit.

Looking at list_queue_relation below, there's mappings of ('a ⇀ 'a), which I'm expecting are in practice projections on the heap that are heap pointers, so the key insight is that where normally we talk about lists with 'a as the member type of the list, here we're only really talking about indices that can be used for indexing something else to get an actual list? Did I interpret this correctly?

I'm getting the feeling a bit more documentation could help here. For example, checking if a head_end_list is empty only checks the head... which assumes we're always operating under an assumption of validity w.r.t. ... something? queue_end_valid takes another list, so that gets a bit confusing.

Any thoughts? I think the definitions are fine, but I think a little hand-holding for the reader would help. Especially if someone comes in from lists and is expecting the 'a to be the usual...

Gerwin and I discussed the naming of this on the work channel on Mattermost. This particular data structure where 'a is machine_word is used in the Haskell and C and called TcbQueue/tcb_queue_t. I'm no whizz with data structures (at least of the PLT/type theory/CS kind) so I'm not sure of the history of the name tcb_queue or whatever, but Gerwin insisted that a queue is something completely different and so we cannot use "queue" here. I thought that a "list" would be something different from this head/end thing, but that's the name Gerwin wanted. I mentioned that we use "queue" for the bound variables and in list_queue_relation itself, as well as in the datatypes in the Haskell and C, but Gerwin said that it would be too much of a pain to change all that now.

You have the right idea. We can extract the actual list we want from the heap of next pointers by starting at the head of this head_end_list and the end of this extracted list should be the end of the head_end_list. The use of the schematic type variable in the definition of list_queue_relation is to make it just as general as heap_ls, so that we can have a nice library for doubly-linked lists. I have some abbreviations in the skel file somewhere where the type variable is made to be machine_word and I call it TcbQueue.

I can definitely add some more comments. I'd have to think about exactly what they would be, especially since there's some confusion over the terminology used. As far as the headEndListEmpty definition, this mirrors the sorts of checks that are performed in the Haskell/C, although I think if we were writing something like this in Isabelle, checking whether it's equal to the emptyHeadEndList would be "nicer". We always do have list_queue_relation when we work with these head/end lists, and because this is always used for refinement, we always do have an abstract list from the abstract function or abstract state somewhere so that we can write things like list_queue_relation or queue_end_valid with that abstract list.