Isabelle对二元谓词表示关系的算子支持问题咨询

1. What support does Isabelle provide for relations represented as binary predicates? #

First off, Isabelle/HOL’s core logic has you covered here since binary predicates are just terms of type 'a ⇒ 'b ⇒ bool—a fundamental type in HOL. Here’s what you get out of the box:

• Basic logical operations: You can directly use HOL’s standard connectives to manipulate these relations:
  • Intersection: λx y. R x y ∧ S x y (both relations hold)
  • Union: λx y. R x y ∨ S x y (either relation holds)
  • Complement: λx y. ¬R x y (the relation does not hold)
• Property expression: Key relational properties can be written directly with quantifiers and implications, no extra imports needed:
  • Reflexivity: ∀x. R x x
  • Symmetry: ∀x y. R x y ⟶ R y x
  • Transitivity: ∀x y z. R x y ∧ R y z ⟶ R x z
• Conversion utilities: The Relation theory includes functions to switch between binary predicate and set-based relation representations:
  • set_of_rel: Converts a binary predicate 'a ⇒ 'b ⇒ bool to a set of pairs ('a × 'b) set
  • rel_of_set: Converts a set-based relation back to a binary predicate

2. How to get operators for composition, converse, etc., for binary predicate relations? #

You’re right that the standard library prioritizes set-based relations (since they align nicely with relational algebra and have more pre-defined utilities). But building these operators for binary predicates is straightforward—you have two main options:

Option 1: Define the operators directly using logical formulas #

This is the most direct approach, as these operations have clear logical definitions:

(* Converse (inverse) of a binary predicate relation *)
definition rel_converse :: "('a ⇒ 'b ⇒ bool) ⇒ 'b ⇒ 'a ⇒ bool" where
  "rel_converse R y x ≡ R x y"

(* Composition of two binary predicate relations *)
definition rel_comp :: "('a ⇒ 'b ⇒ bool) ⇒ ('b ⇒ 'c ⇒ bool) ⇒ 'a ⇒ 'c ⇒ bool" where
  "rel_comp R S x z ≡ ∃y. R x y ∧ S y z"

(* Identity relation for binary predicates *)
definition rel_id :: "'a ⇒ 'a ⇒ bool" where
  "rel_id x y ≡ x = y"

Once defined, you can prove standard properties for these operators using Isabelle’s HOL proof tools. For example:

lemma rel_converse_involutive: "rel_converse (rel_converse R) = R"
  by (auto simp: rel_converse_def)

lemma rel_comp_assoc: "rel_comp R (rel_comp S T) = rel_comp (rel_comp R S) T"
  by (auto simp: rel_comp_def)

Option 2: Reuse set-based operators with conversion functions #

If you want to leverage the pre-defined operators from the Relation theory (like converse, O for composition), you can convert your binary predicate to a set-based relation, apply the operator, then convert back:

(* Converse using set-based utility *)
definition rel_converse' :: "('a ⇒ 'b ⇒ bool) ⇒ 'b ⇒ 'a ⇒ bool" where
  "rel_converse' R = rel_of_set (converse (set_of_rel R))"

(* Composition using set-based utility *)
definition rel_comp' :: "('a ⇒ 'b ⇒ bool) ⇒ ('b ⇒ 'c ⇒ bool) ⇒ 'a ⇒ 'c ⇒ bool" where
  "rel_comp' R S = rel_of_set (set_of_rel R O set_of_rel S)"

This works because the conversion functions preserve all relational properties—so the behavior is identical to defining the operators directly.

A quick note: The standard library favors set-based relations because they’re often easier to reason about with Isabelle’s set theory tools, but binary predicates are fully supported via the core logic and these straightforward extensions.

内容的提问来源于stack exchange，提问作者Wolfgang Jeltsch