如何在Isabelle定理证明助手中形式化公理？——Pure框架下集合遍历类公理的编写方法咨询

Alright, let's walk through how to craft those set-traversal axioms—including the ones with conjunctive (and-like) conditions—in Isabelle/Pure, since you mentioned you've already got other axioms set up with axiomatization.

First: Pure's Take on Sets #

Isabelle/Pure is a minimal logical framework, so it doesn't have a built-in set type like HOL does. Instead, we typically model sets using predicates: a set S is represented as a predicate S :: 'a ⇒ prop, where S x means "x belongs to S".

Handling Traversal + Conjunctive Conditions #

When you need to express "for all elements in a set, both condition A and condition B hold", Pure's universal quantifier ⋀ (written as \And in Isabelle's input mode) is your go-to tool. It lets you "traverse" all elements, and you can pair it with implication (⟹) to restrict to elements in your set, plus conjunctions (∧) for your "and" conditions.

Example 1: Basic Conjunctive Traversal #

Suppose you want an axiom stating every element in set S satisfies both P and Q. Here's how to write that alongside your existing axiomatized symbols:

axiomatization
  --"Your existing symbols go here"
  S :: "'a ⇒ prop" and
  P :: "'a ⇒ prop" and
  Q :: "'a ⇒ prop"
where
  --"Your existing axioms go here"
  conj_set_axiom: "⋀x. S x ⟹ P x ∧ Q x"

Breakdown:

• ⋀x : Traverses all elements x in the type 'a
• S x ⟹ : Restricts our attention to elements that are in S (via the predicate model)
• P x ∧ Q x : Enforces that both conditions hold for those elements

Example 2: Cross-Set Traversal with Conjunctions #

If your axiom involves two sets and a combined condition—like for every x in S and y in T, both R(x,y) and (S x ∧ T y) hold—you can extend the pattern:

axiomatization
  S :: "'a ⇒ prop" and
  T :: "'b ⇒ prop" and
  R :: "'a ⇒ 'b ⇒ prop"
where
  cross_set_axiom: "⋀x y. S x ⟹ T y ⟹ R x y ∧ (S x ∧ T y)"

Here, ⋀x y traverses all pairs of elements from 'a and 'b, and the two ⟹ clauses restrict us to pairs where x is in S and y is in T.

Quick Tips for Your Workflow #

• Keep related axioms and symbols in the same axiomatization block for readability, but you can also use separate blocks if needed.
• Remember that in Pure, all logical statements are of type prop—this is different from HOL's bool, so don't mix up ⋀ (Pure universal quantifier) with HOL's ∀.
• If you ever miss HOL's x ∈ S syntax, just map it to S x in your Pure predicate model.

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