General

This site provides supporting material for the paper Certifying the Weighted Path Order by René Thiemann, Jonas Schöpf, Christian Sternagel and Akihisa Yamada.

Formalization

Our Isabelle formalization is part of IsaFoR/CeTA version 2.39 which compiles with Isabelle 2020 and a corresponding Archive of Formal Proofs. Below we provide links between Isabelle snippets of the paper and the actual formalization in IsaFoR.

Section 2

• The locale redpair S NS in the paper is actually locale redtriple S NS NS where several definitions of previous locales have been expanded.
• The locale redpair_order S NS in the paper is actually locale redtriple_order S NS NS, again with some definitions expanded.
• Similarly, locale ce_af_redpair_order in the paper correponds to locale ce_af_redtriple_order.

Section 3

• locale wpo_params
• theorem "redpair_order WPO_S WPO_NS" is actually named theorem wpo_redtriple_order.
• lemma wpo_af_compatible
• lemma wpo_ce_af_redtriple_order
• The generic_reduction_pair in the paper is actually the more generic and more complex locale generic_redtriple_impl.

Section 4

• datatype sig
• primrec I
• definition le_via_IA
• definition less_via_IA
• lemma le_via_IA
• lemma less_via_IA

Section 5

• partial_function (sum_bot) exp_parser
• partial_function (sum_bot) redtriple

Experimental Results