  17open ArithmeticFromLogic
  18
  19/-- Equality cost on integers. -/
  20def intCost (a b : ℤ) : Nat :=
  21  if a = b then 0 else 1
  22
  23@[simp] theorem intCost_self (a : ℤ) : intCost a a = 0 := by
  24  simp [intCost]
  25
  26theorem intCost_symm (a b : ℤ) : intCost a b = intCost b a := by
  27  by_cases h : a = b
  28  · subst h; simp [intCost]
  29  · have h' : b ≠ a := by intro hb; exact h hb.symm
  30    simp [intCost, h, h']
  31
  32/-- Interpret `LogicNat` as nonnegative integers. -/
  33def intOrbitInterpret (n : LogicNat) : ℤ :=
  34  (LogicNat.toNat n : ℤ)
  35
  36/-- Ordered integer realization with unit step. -/
  37def orderRealization : LogicRealization where
  38  Carrier := ℤ
  39  Cost := Nat
  40  zeroCost := inferInstance
  41  compare := intCost
  42  zero := 0
  43  step := fun z => z + 1
  44  Orbit := LogicNat
  45  orbitZero := LogicNat.zero
  46  orbitStep := LogicNat.succ
  47  interpret := intOrbitInterpret
  48  interpret_zero := by simp [intOrbitInterpret]
  49  interpret_step := by
  50    intro n

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.