ISAR.QuantityKernel

source

structure ISAR.Rational :

Type

Exact rational numbers represented as a pair of numerator and denominator.

num : ℤ
den : ℕ

Instances For

source

def ISAR.instDecidableEqRational.decEq (x✝ x✝¹ : Rational) :

Decidable (x✝ = x✝¹)

Equations

ISAR.instDecidableEqRational.decEq { num := a, den := a_1 } { num := b, den := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

source

@[implicit_reducible]

instance ISAR.instDecidableEqRational :

DecidableEq Rational

Equations

ISAR.instDecidableEqRational = ISAR.instDecidableEqRational.decEq

source

@[implicit_reducible]

instance ISAR.instReprRational :

Repr Rational

Equations

ISAR.instReprRational = { reprPrec := ISAR.instReprRational.repr }

source

def ISAR.instReprRational.repr :

Rational → ℕ → Std.Format

Equations

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

Instances For

source

def ISAR.Rational.mul (r1 r2 : Rational) :

Rational

Equations

r1.mul r2 = { num := r1.num * r2.num, den := r1.den * r2.den }

Instances For

source

def ISAR.Rational.add (r1 r2 : Rational) :

Rational

Equations

r1.add r2 = { num := r1.num * Int.ofNat r2.den + r2.num * Int.ofNat r1.den, den := r1.den * r2.den }

Instances For

source

inductive ISAR.DimBase :

Type

Base SI dimensions.

L : DimBase
T : DimBase
M : DimBase
I : DimBase
Θ : DimBase
N : DimBase
J : DimBase

Instances For

source

@[implicit_reducible]

instance ISAR.instDecidableEqDimBase :

DecidableEq DimBase

Equations

ISAR.instDecidableEqDimBase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[implicit_reducible]

instance ISAR.instReprDimBase :

Repr DimBase

Equations

ISAR.instReprDimBase = { reprPrec := ISAR.instReprDimBase.repr }

source

def ISAR.instReprDimBase.repr :

DimBase → ℕ → Std.Format

Equations

ISAR.instReprDimBase.repr ISAR.DimBase.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.DimBase.L")).group prec✝
ISAR.instReprDimBase.repr ISAR.DimBase.T prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.DimBase.T")).group prec✝
ISAR.instReprDimBase.repr ISAR.DimBase.M prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.DimBase.M")).group prec✝
ISAR.instReprDimBase.repr ISAR.DimBase.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.DimBase.I")).group prec✝
ISAR.instReprDimBase.repr ISAR.DimBase.Θ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.DimBase.Θ")).group prec✝
ISAR.instReprDimBase.repr ISAR.DimBase.N prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.DimBase.N")).group prec✝
ISAR.instReprDimBase.repr ISAR.DimBase.J prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.DimBase.J")).group prec✝

Instances For

source

inductive ISAR.DimExpr :

Type

Dimensional expressions forming a free abelian group.

DimUnit : DimExpr
DimBase : ISAR.DimBase → ℤ → DimExpr
DimMul : DimExpr → DimExpr → DimExpr
DimInv : DimExpr → DimExpr

Instances For

source

def ISAR.instDecidableEqDimExpr.decEq (x✝ x✝¹ : DimExpr) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
ISAR.instDecidableEqDimExpr.decEq ISAR.DimExpr.DimUnit ISAR.DimExpr.DimUnit = isTrue ⋯
ISAR.instDecidableEqDimExpr.decEq ISAR.DimExpr.DimUnit (ISAR.DimExpr.DimBase a a_1) = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq ISAR.DimExpr.DimUnit (a.DimMul a_1) = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq ISAR.DimExpr.DimUnit a.DimInv = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq (ISAR.DimExpr.DimBase a a_1) ISAR.DimExpr.DimUnit = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq (ISAR.DimExpr.DimBase a a_1) (ISAR.DimExpr.DimBase b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq (ISAR.DimExpr.DimBase a a_1) (a_2.DimMul a_3) = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq (ISAR.DimExpr.DimBase a a_1) a_2.DimInv = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq (a.DimMul a_1) ISAR.DimExpr.DimUnit = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq (a.DimMul a_1) (ISAR.DimExpr.DimBase a_2 a_3) = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq (a.DimMul a_1) a_2.DimInv = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq a.DimInv ISAR.DimExpr.DimUnit = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq a.DimInv (ISAR.DimExpr.DimBase a_1 a_2) = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq a.DimInv (a_1.DimMul a_2) = isFalse ⋯
ISAR.instDecidableEqDimExpr.decEq a.DimInv b.DimInv = if h : a = b then h ▸ have inst := ISAR.instDecidableEqDimExpr.decEq a a; isTrue ⋯ else isFalse ⋯

Instances For

source

@[implicit_reducible]

instance ISAR.instDecidableEqDimExpr :

DecidableEq DimExpr

Equations

ISAR.instDecidableEqDimExpr = ISAR.instDecidableEqDimExpr.decEq

source

@[implicit_reducible]

instance ISAR.instReprDimExpr :

Repr DimExpr

Equations

ISAR.instReprDimExpr = { reprPrec := ISAR.instReprDimExpr.repr }

source

def ISAR.instReprDimExpr.repr :

DimExpr → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
ISAR.instReprDimExpr.repr ISAR.DimExpr.DimUnit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.DimExpr.DimUnit")).group prec✝

Instances For

source

inductive ISAR.SymbolBase :

Type

Symbolic base constants and expressions.

Pi : SymbolBase
E : SymbolBase
Sqrt : Rational → SymbolBase
Symbolic : String → SymbolBase

Instances For

source

@[implicit_reducible]

instance ISAR.instDecidableEqSymbolBase :

DecidableEq SymbolBase

Equations

ISAR.instDecidableEqSymbolBase = ISAR.instDecidableEqSymbolBase.decEq

source

def ISAR.instDecidableEqSymbolBase.decEq (x✝ x✝¹ : SymbolBase) :

Decidable (x✝ = x✝¹)

Equations

ISAR.instDecidableEqSymbolBase.decEq ISAR.SymbolBase.Pi ISAR.SymbolBase.Pi = isTrue ⋯
ISAR.instDecidableEqSymbolBase.decEq ISAR.SymbolBase.Pi ISAR.SymbolBase.E = isFalse ISAR.instDecidableEqSymbolBase.decEq._proof_1
ISAR.instDecidableEqSymbolBase.decEq ISAR.SymbolBase.Pi (ISAR.SymbolBase.Sqrt a) = isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq ISAR.SymbolBase.Pi (ISAR.SymbolBase.Symbolic a) = isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq ISAR.SymbolBase.E ISAR.SymbolBase.Pi = isFalse ISAR.instDecidableEqSymbolBase.decEq._proof_4
ISAR.instDecidableEqSymbolBase.decEq ISAR.SymbolBase.E ISAR.SymbolBase.E = isTrue ⋯
ISAR.instDecidableEqSymbolBase.decEq ISAR.SymbolBase.E (ISAR.SymbolBase.Sqrt a) = isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq ISAR.SymbolBase.E (ISAR.SymbolBase.Symbolic a) = isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq (ISAR.SymbolBase.Sqrt a) ISAR.SymbolBase.Pi = isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq (ISAR.SymbolBase.Sqrt a) ISAR.SymbolBase.E = isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq (ISAR.SymbolBase.Sqrt a) (ISAR.SymbolBase.Sqrt b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq (ISAR.SymbolBase.Sqrt a) (ISAR.SymbolBase.Symbolic a_1) = isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq (ISAR.SymbolBase.Symbolic a) ISAR.SymbolBase.Pi = isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq (ISAR.SymbolBase.Symbolic a) ISAR.SymbolBase.E = isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq (ISAR.SymbolBase.Symbolic a) (ISAR.SymbolBase.Sqrt a_1) = isFalse ⋯
ISAR.instDecidableEqSymbolBase.decEq (ISAR.SymbolBase.Symbolic a) (ISAR.SymbolBase.Symbolic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

source

def ISAR.instReprSymbolBase.repr :

SymbolBase → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
ISAR.instReprSymbolBase.repr ISAR.SymbolBase.Pi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.SymbolBase.Pi")).group prec✝
ISAR.instReprSymbolBase.repr ISAR.SymbolBase.E prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ISAR.SymbolBase.E")).group prec✝

Instances For

source

@[implicit_reducible]

instance ISAR.instReprSymbolBase :

Repr SymbolBase

Equations

ISAR.instReprSymbolBase = { reprPrec := ISAR.instReprSymbolBase.repr }

source

inductive ISAR.SymbolExpr :

Type

Symbolic relational layer allowing exact algebraic manipulations.

Rational : ISAR.Rational → SymbolExpr
Add : SymbolExpr → SymbolExpr → SymbolExpr
Mul : SymbolExpr → SymbolExpr → SymbolExpr
Pow : SymbolExpr → SymbolExpr → SymbolExpr
Symbol : SymbolBase → SymbolExpr

Instances For

source

@[implicit_reducible]

instance ISAR.instDecidableEqSymbolExpr :

DecidableEq SymbolExpr

Equations

ISAR.instDecidableEqSymbolExpr = ISAR.instDecidableEqSymbolExpr.decEq

source

def ISAR.instDecidableEqSymbolExpr.decEq (x✝ x✝¹ : SymbolExpr) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
ISAR.instDecidableEqSymbolExpr.decEq (ISAR.SymbolExpr.Rational a) (ISAR.SymbolExpr.Rational b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (ISAR.SymbolExpr.Rational a) (a_1.Add a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (ISAR.SymbolExpr.Rational a) (a_1.Mul a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (ISAR.SymbolExpr.Rational a) (a_1.Pow a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (ISAR.SymbolExpr.Rational a) (ISAR.SymbolExpr.Symbol a_1) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Add a_1) (ISAR.SymbolExpr.Rational a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Add a_1) (a_2.Mul a_3) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Add a_1) (a_2.Pow a_3) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Add a_1) (ISAR.SymbolExpr.Symbol a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Mul a_1) (ISAR.SymbolExpr.Rational a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Mul a_1) (a_2.Add a_3) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Mul a_1) (a_2.Pow a_3) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Mul a_1) (ISAR.SymbolExpr.Symbol a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Pow a_1) (ISAR.SymbolExpr.Rational a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Pow a_1) (a_2.Add a_3) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Pow a_1) (a_2.Mul a_3) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (a.Pow a_1) (ISAR.SymbolExpr.Symbol a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (ISAR.SymbolExpr.Symbol a) (ISAR.SymbolExpr.Rational a_1) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (ISAR.SymbolExpr.Symbol a) (a_1.Add a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (ISAR.SymbolExpr.Symbol a) (a_1.Mul a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (ISAR.SymbolExpr.Symbol a) (a_1.Pow a_2) = isFalse ⋯
ISAR.instDecidableEqSymbolExpr.decEq (ISAR.SymbolExpr.Symbol a) (ISAR.SymbolExpr.Symbol b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

source

def ISAR.instReprSymbolExpr.repr :

SymbolExpr → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance ISAR.instReprSymbolExpr :

Repr SymbolExpr

Equations

ISAR.instReprSymbolExpr = { reprPrec := ISAR.instReprSymbolExpr.repr }

source

inductive ISAR.MetricExpr :

Type

Metric representation layer, mapping to numerical magnitude.

MetricExact : Rational → MetricExpr
MetricApprox : Float → MetricExpr
MetricSymbolic : SymbolExpr → MetricExpr

Instances For

source

@[implicit_reducible]

instance ISAR.instReprMetricExpr :

Repr MetricExpr

Equations

ISAR.instReprMetricExpr = { reprPrec := ISAR.instReprMetricExpr.repr }

source

def ISAR.instReprMetricExpr.repr :

MetricExpr → ℕ → Std.Format

Equations

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

Instances For

source

def ISAR.toSymbol :

MetricExpr → SymbolExpr

Map MetricExpr to SymbolExpr for symbolic propagation.

Equations

ISAR.toSymbol (ISAR.MetricExpr.MetricExact a) = ISAR.SymbolExpr.Rational a
ISAR.toSymbol (ISAR.MetricExpr.MetricApprox a) = ISAR.SymbolExpr.Symbol (ISAR.SymbolBase.Symbolic "approx_float")
ISAR.toSymbol (ISAR.MetricExpr.MetricSymbolic a) = a

Instances For

source

structure ISAR.Uncertainty :

Type

Uncertainty definition (mean and variance).

mean : MetricExpr
var : MetricExpr

Instances For

source

def ISAR.instReprUncertainty.repr :

Uncertainty → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance ISAR.instReprUncertainty :

Repr Uncertainty

Equations

ISAR.instReprUncertainty = { reprPrec := ISAR.instReprUncertainty.repr }

source

structure ISAR.Correlation :

Type

Covariance/correlation representation.

id1 : ℕ
id2 : ℕ
covar : MetricExpr

Instances For

source

def ISAR.instReprCorrelation.repr :

Correlation → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance ISAR.instReprCorrelation :

Repr Correlation

Equations

ISAR.instReprCorrelation = { reprPrec := ISAR.instReprCorrelation.repr }

source

structure ISAR.EpistemicExpr :

Type

Epistemic layer representing uncertainties and correlations.

uncertainties : List (ℕ × Uncertainty)
correlations : List Correlation

Instances For

source

def ISAR.instReprEpistemicExpr.repr :

EpistemicExpr → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance ISAR.instReprEpistemicExpr :

Repr EpistemicExpr

Equations

ISAR.instReprEpistemicExpr = { reprPrec := ISAR.instReprEpistemicExpr.repr }

source

structure ISAR.Quantity :

Type

The unified Quantity type, stacking structural, symbolic, metric, and epistemic.

dim : DimExpr
sym : SymbolExpr
mag : MetricExpr
epis : EpistemicExpr

Instances For

source

@[implicit_reducible]

instance ISAR.instReprQuantity :

Repr Quantity

Equations

ISAR.instReprQuantity = { reprPrec := ISAR.instReprQuantity.repr }

source

def ISAR.instReprQuantity.repr :

Quantity → ℕ → Std.Format

Equations

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

Instances For

source

def ISAR.propagateVarAdd (var1 var2 covar : MetricExpr) :

MetricExpr

Linearized variance propagation for addition: var(A + B) = var(A) + var(B) + 2 * covar(A,B).

Equations

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

Instances For

source

def ISAR.propagateVarMul (mean1 mean2 var1 var2 covar : MetricExpr) :

MetricExpr

Linearized variance propagation for multiplication: var(A * B) = B^2 * var(A) + A^2 * var(B) + 2 * A * B * covar(A,B).

Equations

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

Instances For

source

def ISAR.addQ (q1 q2 : Quantity) (_h_dim : q1.dim = q2.dim) :

Quantity

Dimension-compatible addition of two quantities.

Equations

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

Instances For

source

def ISAR.mulQ (q1 q2 : Quantity) :

Quantity

Multiplication of two quantities.

Equations

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

Instances For

source

axiom ISAR.quantityToNat :

Quantity → ℕ

Named modeling axioms: Quantity carries String and Float, which block a kernel Encodable instance. The countable bijection is not derived.

source

axiom ISAR.natQuantity :

ℕ → Quantity

source

axiom ISAR.quantityToNat_inverse (q : Quantity) :

natQuantity (quantityToNat q) = q

source

axiom ISAR.natQuantity_inverse (n : ℕ) :

quantityToNat (natQuantity n) = n

source

structure ISAR.QuantityCore :

Type

Exact core without SymbolBase.Symbolic (String) or MetricExpr.MetricApprox (Float). The four quantityToNat axioms on the full Quantity stay named.

dimCode : ℕ
num : ℤ
den : ℕ

Instances For

source

def ISAR.instDecidableEqQuantityCore.decEq (x✝ x✝¹ : QuantityCore) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[implicit_reducible]

instance ISAR.instDecidableEqQuantityCore :

DecidableEq QuantityCore

Equations

ISAR.instDecidableEqQuantityCore = ISAR.instDecidableEqQuantityCore.decEq

source

def ISAR.instReprQuantityCore.repr :

QuantityCore → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance ISAR.instReprQuantityCore :

Repr QuantityCore

Equations

ISAR.instReprQuantityCore = { reprPrec := ISAR.instReprQuantityCore.repr }

source

def ISAR.intToNat :

ℤ → ℕ

Equations

ISAR.intToNat (Int.ofNat k) = Nat.pair k 0
ISAR.intToNat (Int.negSucc k) = Nat.pair k 1

Instances For

source

def ISAR.natToInt (n : ℕ) :

ℤ

Equations

ISAR.natToInt n = if (Nat.unpair n).2 = 0 then Int.ofNat (Nat.unpair n).1 else Int.negSucc (Nat.unpair n).1

Instances For

source

theorem ISAR.natToInt_toNat (i : ℤ) :

natToInt (intToNat i) = i

source

def ISAR.quantityCoreToNat (q : QuantityCore) :

ℕ

Equations

ISAR.quantityCoreToNat q = Nat.pair q.dimCode (Nat.pair (ISAR.intToNat q.num) q.den)

Instances For

source

def ISAR.natToQuantityCore (n : ℕ) :

QuantityCore

Equations

ISAR.natToQuantityCore n = { dimCode := (Nat.unpair n).1, num := ISAR.natToInt (Nat.unpair (Nat.unpair n).2).1, den := (Nat.unpair (Nat.unpair n).2).2 }

Instances For

source

theorem ISAR.natToQuantityCore_toNat (q : QuantityCore) :

natToQuantityCore (quantityCoreToNat q) = q

Constructed left inverse: QuantityCore is encodable. Not a bijection on the full Quantity (those four axioms stay named).

source

noncomputable def ISAR.view_of (t : ISKSubtype) :

Quantity

Mapping from substrate to Quantity.

Equations

ISAR.view_of t = ISAR.natQuantity (ISAR.layerToNat ⟦t⟧)

Instances For

source

noncomputable def ISAR.decode (q : Quantity) :

ISKSubtype

Mapping from Quantity back to substrate.

Equations

ISAR.decode q = (ISAR.natToLayer (ISAR.quantityToNat q)).canonical_rep

Instances For

source

theorem ISAR.quantity_eq_equivalence :

Equivalence fun (x y : Quantity) => x = y

Equivalence on Quantity is standard equality.

source

theorem ISAR.sound (t u : ISKSubtype) (h : OperEq t u) :

view_of t = view_of u

source

theorem ISAR.decode_view (t : ISKSubtype) :

OperEq (decode (view_of t)) t

source

theorem ISAR.view_eq_decode (q : Quantity) :

view_of (decode q) = q

source

theorem ISAR.decode_eq (q1 q2 : Quantity) (h : q1 = q2) :

OperEq (decode q1) (decode q2)

source

@[reducible, inline]

noncomputable abbrev ISAR.QuantityKernel :

Kernel

QuantityKernel definition as an admissible semantic kernel.

Equations

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

Instances For

source

noncomputable def ISAR.InvariantLayer.add (q1 q2 : InvariantLayer) :

InvariantLayer

Stable addition on the Invariant Layer quotient class.

Equations

q1.add q2 = ISAR.natToLayer (ISAR.layerToNat q1 + ISAR.layerToNat q2)

Instances For

source

theorem ISAR.quantity_addition_invariant (q1 q2 : InvariantLayer) :

layerToNat (q1.add q2) = layerToNat q1 + layerToNat q2

Theorem proving that InvariantLayer.add is a stable invariant preserving arithmetic addition.