mathlib3 documentation

tactic.omega.term

@[protected, instance]

def omega.term.inhabited :

inhabited omega.term

def omega.term :

Shadow syntax of normalized terms. The first element represents the constant term and the list represents the coefficients.

Equations

omega.term = (ℤ × list ℤ)

Instances for omega.term

@[protected, instance]

meta def omega.term.has_reflect :

has_reflect omega.term

@[simp]

def omega.term.val (v : ℕ → ℤ) :

omega.term → ℤ

Evaluate a term using the valuation v.

Equations

omega.term.val v (b, as) = b + omega.coeffs.val v as

@[simp]

def omega.term.neg :

omega.term → omega.term

Equations

omega.term.neg (b, as) = (-b, list.func.neg as)

@[simp]

def omega.term.add :

omega.term → omega.term → omega.term

Equations

omega.term.add (c1, cfs1) (c2, cfs2) = (c1 + c2, list.func.add cfs1 cfs2)

@[simp]

def omega.term.sub :

omega.term → omega.term → omega.term

Equations

omega.term.sub (c1, cfs1) (c2, cfs2) = (c1 - c2, list.func.sub cfs1 cfs2)

@[simp]

def omega.term.mul (i : ℤ) :

omega.term → omega.term

Equations

omega.term.mul i (b, as) = (i * b, list.map (has_mul.mul i) as)

@[simp]

def omega.term.div (i : ℤ) :

omega.term → omega.term

Equations

omega.term.div i (b, as) = (b / i, list.map (λ (x : ℤ), x / i) as)

theorem omega.term.val_neg {v : ℕ → ℤ} {t : omega.term} :

omega.term.val v t.neg = -omega.term.val v t

@[simp]

theorem omega.term.val_sub {v : ℕ → ℤ} {t1 t2 : omega.term} :

omega.term.val v (t1.sub t2) = omega.term.val v t1 - omega.term.val v t2

@[simp]

theorem omega.term.val_add {v : ℕ → ℤ} {t1 t2 : omega.term} :

omega.term.val v (t1.add t2) = omega.term.val v t1 + omega.term.val v t2

@[simp]

theorem omega.term.val_mul {v : ℕ → ℤ} {i : ℤ} {t : omega.term} :

omega.term.val v (omega.term.mul i t) = i * omega.term.val v t

theorem omega.term.val_div {v : ℕ → ℤ} {i b : ℤ} {as : list ℤ} :

i ∣ b → (∀ (x : ℤ), x ∈ as → i ∣ x) → omega.term.val v (omega.term.div i (b, as)) = omega.term.val v (b, as) / i

def omega.term.fresh_index (t : omega.term) :

Fresh de Brujin index not used by any variable ocurring in the term

Equations

t.fresh_index = t.snd.length

def omega.term.to_string (t : omega.term) :

Equations

t.to_string = list.foldr (λ (_x : ℕ × ℤ), omega.term.to_string._match_1 _x) (to_string t.fst) t.snd.enum
omega.term.to_string._match_1 (i, n) = λ (r : string), to_string n ++ " * x" ++ to_string i ++ " + " ++ r

@[protected, instance]

def omega.term.has_to_string :

has_to_string omega.term

Equations

omega.term.has_to_string = {to_string := omega.term.to_string}

def omega.terms.fresh_index :

list omega.term → ℕ

Fresh de Brujin index not used by any variable ocurring in the list of terms

Equations

omega.terms.fresh_index (t :: ts) = linear_order.max t.fresh_index (omega.terms.fresh_index ts)
omega.terms.fresh_index list.nil = 0