Stream: Beginner Questions

Topic: well-founded order

view this post on Zulip Maximilian Spitz (Aug 03 2023 at 17:29):

Hi everyone,
for a proof in Isabelle I need to assume, that I have a well-founded partial order r : B * B on a given set B, because I want to induct on (B, r). I have no experience with orders in Isabelle and the source files are confusing me a little bit. Could you help me to state "r is a well-founded partial order on B * B" in Isabelle the right way?

Also, to induct on (B, r) I think I will need the wf_induct rule, but I could not find any good examples of how to use it correctly. It would be great if you could point me to some theories which make use of wf_induct, so that I can get an idea by looking at examples.

Thanks a lot.

Last updated: Dec 21 2024 at 16:20 UTC