Re: [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).

Tobias

On 16/08/2017 10:44, Christian Sternagel wrote:

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.

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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev