Documentation

Flypitch.Examples.Abel

inductive Flypitch.abel.Functions :

zero : Functions 0
plus : Functions 2

Instances For

def Flypitch.abel.LAbel :

Equations

Flypitch.abel.LAbel = { functions := Flypitch.abel.Functions, relations := fun (x : ℕ) => PEmpty.{1} }

Instances For

def Flypitch.abel.zeroTerm :

Equations

Flypitch.abel.zeroTerm = Flypitch.fol.preterm.func Flypitch.abel.Functions.zero

Instances For

def Flypitch.abel.addTerm (t₁ t₂ : fol.term LAbel) :

Equations

Flypitch.abel.addTerm t₁ t₂ = Flypitch.fol.apps (Flypitch.fol.preterm.func Flypitch.abel.Functions.plus) (Flypitch.dvector.cons t₁ (Flypitch.dvector.cons t₂ Flypitch.dvector.nil))

Instances For

def Flypitch.abel.aAssoc :

fol.formula LAbel

Equations

Flypitch.abel.aAssoc = ∀' ∀' ∀' (Flypitch.abel.addTerm (Flypitch.abel.addTerm &2 &1) &0 ≃ Flypitch.abel.addTerm (&2) (Flypitch.abel.addTerm &1 &0))

Instances For

def Flypitch.abel.aZeroRight :

fol.formula LAbel

Equations

Flypitch.abel.aZeroRight = ∀' (Flypitch.abel.addTerm (&0) Flypitch.abel.zeroTerm ≃ &0)

Instances For

def Flypitch.abel.aZeroLeft :

fol.formula LAbel

Equations

Flypitch.abel.aZeroLeft = ∀' (Flypitch.abel.addTerm Flypitch.abel.zeroTerm &0 ≃ &0)

Instances For

def Flypitch.abel.aInv :

fol.formula LAbel

Equations

Flypitch.abel.aInv = ∀' Flypitch.fol.ex (Flypitch.fol.and (Flypitch.abel.addTerm &1 &0 ≃ Flypitch.abel.zeroTerm) (Flypitch.abel.addTerm &0 &1 ≃ Flypitch.abel.zeroTerm))

Instances For

def Flypitch.abel.aComm :

fol.formula LAbel

Equations

Flypitch.abel.aComm = ∀' ∀' (Flypitch.abel.addTerm &1 &0 ≃ Flypitch.abel.addTerm &0 &1)

Instances For

def Flypitch.abel.TAb :

Set (fol.formula LAbel)

Equations

Flypitch.abel.TAb = insert Flypitch.abel.aAssoc (insert Flypitch.abel.aZeroRight (insert Flypitch.abel.aZeroLeft (insert Flypitch.abel.aInv (insert Flypitch.abel.aComm ∅))))

Instances For

def Flypitch.abel.intStructure :

fol.Structure LAbel

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible]

instance Flypitch.abel.instAddCommGroupCarrierIntStructure :

AddCommGroup intStructure.carrier

Equations

One or more equations did not get rendered due to their size.

@[reducible]

instance Flypitch.abel.instOfNatCarrierIntStructureOfNatNat :

OfNat intStructure.carrier 0

Equations

Flypitch.abel.instOfNatCarrierIntStructureOfNatNat = { ofNat := Flypitch.abel.instOfNatCarrierIntStructureOfNatNat._aux_1 }

@[simp]

theorem Flypitch.abel.realize_zeroTerm (v : ℕ → intStructure.carrier) :

fol.realize_term v zeroTerm dvector.nil = 0

@[simp]

theorem Flypitch.abel.intStructure_plus (x y : intStructure.carrier) :

intStructure.fun_map Functions.plus (dvector.cons x (dvector.cons y dvector.nil)) = x + y

@[simp]

theorem Flypitch.abel.realize_addTerm (v : ℕ → intStructure.carrier) (t₁ t₂ : fol.term LAbel) :

fol.realize_term v (addTerm t₁ t₂) dvector.nil = fol.realize_term v t₁ dvector.nil + fol.realize_term v t₂ dvector.nil

theorem Flypitch.abel.int_satisfies_assoc :

fol.satisfied_in intStructure aAssoc

theorem Flypitch.abel.int_satisfies_zeroRight :

fol.satisfied_in intStructure aZeroRight

theorem Flypitch.abel.int_satisfies_zeroLeft :

fol.satisfied_in intStructure aZeroLeft

theorem Flypitch.abel.int_satisfies_inv :

fol.satisfied_in intStructure aInv

theorem Flypitch.abel.int_satisfies_comm :

fol.satisfied_in intStructure aComm

theorem Flypitch.abel.int_satisfies_TAb :

fol.all_satisfied_in intStructure TAb

theorem Flypitch.abel.int_satisfies_of_prf {f : fol.formula LAbel} (h : TAb ⊢ f) :

fol.satisfied_in intStructure f