inductive ISAR.LTerm : Type

• var : Nat → LTerm
• abs : LTerm → LTerm
• app : LTerm → LTerm → LTerm

@[implicit_reducible]

instance ISAR.instDecidableEqLTerm : DecidableEq LTerm

Equations

• ISAR.instDecidableEqLTerm = ISAR.instDecidableEqLTerm.decEq

def ISAR.instDecidableEqLTerm.decEq (x✝ x✝¹ : LTerm) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• ISAR.instDecidableEqLTerm.decEq (ISAR.LTerm.var a) (ISAR.LTerm.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ISAR.instDecidableEqLTerm.decEq (ISAR.LTerm.var a) a_1.abs = isFalse ⋯
• ISAR.instDecidableEqLTerm.decEq (ISAR.LTerm.var a) (a_1.app a_2) = isFalse ⋯
• ISAR.instDecidableEqLTerm.decEq a.abs (ISAR.LTerm.var a_1) = isFalse ⋯
• ISAR.instDecidableEqLTerm.decEq a.abs b.abs = if h : a = b then h ▸ have inst := ISAR.instDecidableEqLTerm.decEq a a; isTrue ⋯ else isFalse ⋯
• ISAR.instDecidableEqLTerm.decEq a.abs (a_1.app a_2) = isFalse ⋯
• ISAR.instDecidableEqLTerm.decEq (a.app a_1) (ISAR.LTerm.var a_2) = isFalse ⋯
• ISAR.instDecidableEqLTerm.decEq (a.app a_1) a_2.abs = isFalse ⋯

@[implicit_reducible]

instance ISAR.instReprLTerm : Repr LTerm

Equations

• ISAR.instReprLTerm = { reprPrec := ISAR.instReprLTerm.repr }

def ISAR.instReprLTerm.repr : LTerm → Nat → Std.Format

Equations

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

def ISAR.shift (d c : Nat) : LTerm → LTerm

Equations

• ISAR.shift d c (ISAR.LTerm.var a) = if a < c then ISAR.LTerm.var a else ISAR.LTerm.var (a + d)
• ISAR.shift d c a.abs = (ISAR.shift d (c + 1) a).abs
• ISAR.shift d c (a.app a_1) = (ISAR.shift d c a).app (ISAR.shift d c a_1)

def ISAR.subst (s : LTerm) (c : Nat) : LTerm → LTerm

Equations

• ISAR.subst s c (ISAR.LTerm.var a) = if a < c then ISAR.LTerm.var a else if a = c then ISAR.shift c 0 s else ISAR.LTerm.var (a - 1)
• ISAR.subst s c a.abs = (ISAR.subst s (c + 1) a).abs
• ISAR.subst s c (a.app a_1) = (ISAR.subst s c a).app (ISAR.subst s c a_1)

inductive ISAR.LStep : LTerm → LTerm → Prop

• beta (body s : LTerm) : LStep (body.abs.app s) (subst s 0 body)
• appL {f f' x : LTerm} : LStep f f' → LStep (f.app x) (f'.app x)
• appR {f x x' : LTerm} : LStep x x' → LStep (f.app x) (f.app x')

@[reducible, inline]

abbrev ISAR.LRed (a : LTerm) : LTerm → Prop

Equations

• ISAR.LRed = Relation.ReflTransGen ISAR.LStep

theorem ISAR.LRed_app_left {f f' x : LTerm} (h : LRed f f') : LRed (f.app x) (f'.app x)

theorem ISAR.LRed_app_right {f x x' : LTerm} (h : LRed x x') : LRed (f.app x) (f.app x')

theorem ISAR.LRed_app {f f' x x' : LTerm} (hf : LRed f f') (hx : LRed x x') : LRed (f.app x) (f'.app x')

def ISAR.occurs0 : ITerm → Bool

Equations

• ISAR.occurs0 (ISAR.ITerm.var 0) = true
• ISAR.occurs0 (ISAR.ITerm.var a) = false
• ISAR.occurs0 ISAR.ITerm.norm = false
• ISAR.occurs0 ISAR.ITerm.konst = false
• ISAR.occurs0 ISAR.ITerm.dup = false
• ISAR.occurs0 ISAR.ITerm.swap = false
• ISAR.occurs0 ISAR.ITerm.comp = false
• ISAR.occurs0 ISAR.ITerm.sₛ = false
• ISAR.occurs0 (f · x_1) = (ISAR.occurs0 f || ISAR.occurs0 x_1)

def ISAR.shift_down : ITerm → ITerm

Equations

• ISAR.shift_down (ISAR.ITerm.var 0) = ISAR.ITerm.var 0
• ISAR.shift_down (ISAR.ITerm.var a) = ISAR.ITerm.var (a - 1)
• ISAR.shift_down ISAR.ITerm.norm = ISAR.ITerm.norm
• ISAR.shift_down ISAR.ITerm.konst = ISAR.ITerm.konst
• ISAR.shift_down ISAR.ITerm.dup = ISAR.ITerm.dup
• ISAR.shift_down ISAR.ITerm.swap = ISAR.ITerm.swap
• ISAR.shift_down ISAR.ITerm.comp = ISAR.ITerm.comp
• ISAR.shift_down ISAR.ITerm.sₛ = ISAR.ITerm.sₛ
• ISAR.shift_down (f · x_1) = ISAR.shift_down f · ISAR.shift_down x_1

def ISAR.shift_isar (d c : Nat) : ITerm → ITerm

Equations

• ISAR.shift_isar d c (ISAR.ITerm.var n) = if n < c then ISAR.ITerm.var n else ISAR.ITerm.var (n + d)
• ISAR.shift_isar d c ISAR.ITerm.norm = ISAR.ITerm.norm
• ISAR.shift_isar d c ISAR.ITerm.konst = ISAR.ITerm.konst
• ISAR.shift_isar d c ISAR.ITerm.dup = ISAR.ITerm.dup
• ISAR.shift_isar d c ISAR.ITerm.swap = ISAR.ITerm.swap
• ISAR.shift_isar d c ISAR.ITerm.comp = ISAR.ITerm.comp
• ISAR.shift_isar d c ISAR.ITerm.sₛ = ISAR.ITerm.sₛ
• ISAR.shift_isar d c (f · x_1) = ISAR.shift_isar d c f · ISAR.shift_isar d c x_1

def ISAR.abstract0 (t : ITerm) : ITerm

Equations

• One or more equations did not get rendered due to their size.
• ISAR.abstract0 (ISAR.ITerm.var 0) = match ISAR.occurs0 (ISAR.ITerm.var 0) with | false => ISAR.ITerm.konst · ISAR.shift_down (ISAR.ITerm.var 0) | true => ISAR.ITerm.norm
• ISAR.abstract0 t = match ISAR.occurs0 t with | false => ISAR.ITerm.konst · ISAR.shift_down t | true => ISAR.ITerm.norm

def ISAR.subst_isar (x : ITerm) : ITerm → ITerm

Equations

• ISAR.subst_isar x (ISAR.ITerm.var 0) = x
• ISAR.subst_isar x (ISAR.ITerm.var a) = ISAR.ITerm.var (a - 1)
• ISAR.subst_isar x ISAR.ITerm.norm = ISAR.ITerm.norm
• ISAR.subst_isar x ISAR.ITerm.konst = ISAR.ITerm.konst
• ISAR.subst_isar x ISAR.ITerm.dup = ISAR.ITerm.dup
• ISAR.subst_isar x ISAR.ITerm.swap = ISAR.ITerm.swap
• ISAR.subst_isar x ISAR.ITerm.comp = ISAR.ITerm.comp
• ISAR.subst_isar x ISAR.ITerm.sₛ = ISAR.ITerm.sₛ
• ISAR.subst_isar x (f · x_2) = ISAR.subst_isar x f · ISAR.subst_isar x x_2

def ISAR.subst_isar_at (c : Nat) (x : ITerm) : ITerm → ITerm

Equations

• ISAR.subst_isar_at c x (ISAR.ITerm.var n) = if n < c then ISAR.ITerm.var n else if n = c then x else ISAR.ITerm.var (n - 1)
• ISAR.subst_isar_at c x ISAR.ITerm.norm = ISAR.ITerm.norm
• ISAR.subst_isar_at c x ISAR.ITerm.konst = ISAR.ITerm.konst
• ISAR.subst_isar_at c x ISAR.ITerm.dup = ISAR.ITerm.dup
• ISAR.subst_isar_at c x ISAR.ITerm.swap = ISAR.ITerm.swap
• ISAR.subst_isar_at c x ISAR.ITerm.comp = ISAR.ITerm.comp
• ISAR.subst_isar_at c x ISAR.ITerm.sₛ = ISAR.ITerm.sₛ
• ISAR.subst_isar_at c x (f · x_2) = ISAR.subst_isar_at c x f · ISAR.subst_isar_at c x x_2

def ISAR.compile : LTerm → ITerm

Equations

• ISAR.compile (ISAR.LTerm.var n) = ISAR.ITerm.var n
• ISAR.compile (f.app x_1) = ISAR.compile f · ISAR.compile x_1
• ISAR.compile body.abs = ISAR.abstract0 (ISAR.compile body)

theorem ISAR.subst_isar_no_occur {t : ITerm} (h : occurs0 t = false) (x : ITerm) : subst_isar x t = shift_down t

theorem ISAR.abstract_sound (t x : ITerm) : IRed (abstract0 t · x) (subst_isar x t)

theorem ISAR.occurs0_shift_isar (d c : Nat) (t : ITerm) (hc : c > 0) : occurs0 (shift_isar d c t) = occurs0 t

theorem ISAR.shift_down_shift_isar (d c : Nat) (t : ITerm) (h : occurs0 t = false) : shift_down (shift_isar d (c + 1) t) = shift_isar d c (shift_down t)

theorem ISAR.abstract0_shift_isar (d c : Nat) (t : ITerm) : shift_isar d c (abstract0 t) = abstract0 (shift_isar d (c + 1) t)

theorem ISAR.compile_shift (d c : Nat) (t : LTerm) : compile (shift d c t) = shift_isar d c (compile t)

theorem ISAR.shift_isar_add (c : Nat) (u : ITerm) : shift_isar (c + 1) 0 u = shift_isar 1 c (shift_isar c 0 u)

theorem ISAR.shift_down_shift_isar_coincide (c : Nat) (s : ITerm) : shift_down (shift_isar 1 c (shift_isar c 0 s)) = shift_isar c 0 s

theorem ISAR.occurs0_subst_isar (c : Nat) (x : ITerm) (hx : occurs0 x = false) (u : ITerm) : occurs0 (subst_isar_at (c + 1) x u) = occurs0 u

theorem ISAR.occurs0_special_X (c : Nat) (s : ITerm) : occurs0 (shift_isar 1 c (shift_isar c 0 s)) = false

theorem ISAR.shift_down_subst_isar_special (c : Nat) (s u : ITerm) (hu : occurs0 u = false) : shift_down (subst_isar_at (c + 1) (shift_isar 1 c (shift_isar c 0 s)) u) = subst_isar_at c (shift_isar c 0 s) (shift_down u)

theorem ISAR.abstract0_subst_isar_special (c : Nat) (s u : ITerm) : abstract0 (subst_isar_at (c + 1) (shift_isar 1 c (shift_isar c 0 s)) u) = subst_isar_at c (shift_isar c 0 s) (abstract0 u)

theorem ISAR.compile_subst (s : LTerm) (c : Nat) (t : LTerm) : compile (subst s c t) = subst_isar_at c (shift_isar c 0 (compile s)) (compile t)

theorem ISAR.shift_isar_zero (c : Nat) (s : ITerm) : shift_isar 0 c s = s

theorem ISAR.subst_isar_eq_subst_isar_at_0 (x t : ITerm) : subst_isar x t = subst_isar_at 0 x t

theorem ISAR.compile_simulates_step {t u : LTerm} (h : LStep t u) : IRed (compile t) (compile u)

theorem ISAR.compile_simulates_red {t u : LTerm} (h : LRed t u) : IRed (compile t) (compile u)