FunctionFreeFacts

A FunctionFreeFact is a GeneralizedAtom with constants.

@[reducible, inline]

abbrev FunctionFreeFact (sig : Signature) [DecidableEq sig.P] : Type (max u_3 u_1)

Equations

• FunctionFreeFact sig = GeneralizedAtom sig sig.C

def FunctionFreeFact.toFact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : FunctionFreeFact sig) : Fact sig

A FunctionFreeFact can always be converted to a Fact.

Equations

• f.toFact = { predicate := f.predicate, terms := List.map GroundTerm.const f.terms, arity_ok := ⋯ }

theorem FunctionFreeFact.toFact_isFunctionFree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : FunctionFreeFact sig) : f.toFact.isFunctionFree

A Fact obtained from a FunctionFreeFact isFunctionFree.

def Fact.toFunctionFreeFact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : Fact sig) (isFunctionFree : f.isFunctionFree) : FunctionFreeFact sig

If a Fact.isFunctionFree, then we can convert it to a FunctionFreeFact.

Equations

• f.toFunctionFreeFact isFunctionFree = { predicate := f.predicate, terms := List.map (fun (t : { x : GroundTerm sig // x ∈ f.terms }) => t.val.toConst ⋯) f.terms.attach, arity_ok := ⋯ }

@[simp]

theorem Fact.toFact_after_toFunctionFreeFact_is_id {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : Fact sig) (isFunctionFree : f.isFunctionFree) : (f.toFunctionFreeFact isFunctionFree).toFact = f

Converting a Fact to a FunctionFreeFact and back yields the initial Fact.

@[simp]

theorem FunctionFreeFact.toFunctionFreeFact_after_toFact_is_id {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : FunctionFreeFact sig) : f.toFact.toFunctionFreeFact ⋯ = f

Converting a FunctionFreeFact to a Fact and back yields the initial FunctionFreeFact.