[isabelle-dev] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

[Tobias Nipkow]

The name "sorted_wrt" came from Manuel and I would like to keep it. For 
transtive predicates it is the same as sorted (I will add that lemma to List).

I looked into your theory but did not find any further generic lemmas about 
"linked". Let me know if I missed any that should go into List.

Tobias

On 16/08/2017 10:44, Christian Sternagel wrote:
> Dear Tobias,
> 
> I think your "sorted_wrt" is almost (modulo "fun" vs. "inductive") my
> "linked" from the AFP (Efficient_Mergesort).
> 
> 
> https://www.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Sort.html
> 
> Maybe we could unify the constants/names somehow?
> 
> At the moment I somewhat prefer "linked" (or maybe "linked_by") since
> sortedness implies that "P" is some kind of order, which it doesn't have
> to be.
> 
> kind regards,
> 
> chris
> 
> 
> -------- Forwarded Message --------
> Subject: 	added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
> Date: 	Tue, 15 Aug 2017 19:47:08 +0200
> From: 	nipkow <>
> 
> 
> 
> added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy added
> sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170816/b0f1802a/attachment.bin>