  12namespace Strict
  13namespace Ordered
  14
  15def intCost (a b : ℤ) : Nat :=
  16  if a = b then 0 else 1
  17
  18@[simp] theorem intCost_self (a : ℤ) : intCost a a = 0 := by
  19  simp [intCost]
  20
  21theorem intCost_symm (a b : ℤ) : intCost a b = intCost b a := by
  22  by_cases h : a = b
  23  · subst h
  24    simp [intCost]
  25  · have h' : b ≠ a := by intro hb; exact h hb.symm
  26    simp [intCost, h, h']
  27
  28/-- Strict ordered integer realization. -/
  29def strictOrderedRealization : StrictLogicRealization where
  30  Carrier := ℤ
  31  Cost := Nat
  32  zeroCost := inferInstance
  33  compare := intCost
  34  compose := fun a b => a + b
  35  one := 0
  36  generator := 1
  37  identity_law := intCost_self
  38  non_contradiction_law := intCost_symm
  39  excluded_middle_law := True
  40  composition_law := True
  41  invariance_law := True
  42  nontrivial_law := by
  43    simp [intCost]
  44
  45def strictOrdered_arith_equiv_logicNat :

papers checked against this theorem

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