Isotope.STm.Sym

source

def Isotope.STm.use {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} :

STm L A → Set A

Equations

(Isotope.STm.sym a).use = {a}
(Isotope.STm.const a).use = ∅
(Isotope.STm.op a es).use = ⋃ i ∈ Isotope.Args.posFinset arity, (es i).use

Instances For

source

@[simp]

theorem Isotope.STm.use_sym {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (a : A) :

(sym a).use = {a}

source

theorem Isotope.STm.mem_use_sym_iff {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {a b : A} :

a ∈ (sym b).use ↔ a = b

source

@[simp]

theorem Isotope.STm.use_const {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (c : L.Val) :

(const c).use = ∅

source

theorem Isotope.STm.not_mem_use_const {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {a : A} {c : L.Val} :

a ∉ (const c).use

source

theorem Isotope.STm.use_op {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {arity : Arity} (o : L.Op arity) (es : UArgs.Ix arity → STm L A) :

(op o es).use = ⋃ i ∈ Args.posFinset arity, (es i).use

source

@[simp]

theorem Isotope.STm.mem_use_op_iff {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {a : A} {arity : Arity} (o : L.Op arity) (es : UArgs.Ix arity → STm L A) :

a ∈ (op o es).use ↔ ∃ i ∈ Args.posFinset arity, a ∈ (es i).use

source

def Isotope.STm.subtrees {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} :

STm L A → Set (STm L A)

Equations

(Isotope.STm.sym a).subtrees = {Isotope.STm.sym a}
(Isotope.STm.const a).subtrees = {Isotope.STm.const a}
(Isotope.STm.op a es).subtrees = {Isotope.STm.op a es} ∪ ⋃ i ∈ Isotope.Args.posFinset arity, (es i).subtrees

Instances For

source

@[simp]

theorem Isotope.STm.subtrees_sym {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (a : A) :

(sym a).subtrees = {sym a}

source

theorem Isotope.STm.mem_subtrees_sym_iff {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {e : STm L A} {a : A} :

e ∈ (sym a).subtrees ↔ e = sym a

source

@[simp]

theorem Isotope.STm.subtrees_const {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (c : L.Val) :

(const c).subtrees = {const c}

source

theorem Isotope.STm.mem_subtrees_const_iff {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {e : STm L A} {c : L.Val} :

e ∈ (const c).subtrees ↔ e = const c

source

theorem Isotope.STm.subtrees_op {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {arity : Arity} (o : L.Op arity) (es : UArgs.Ix arity → STm L A) :

(op o es).subtrees = {op o es} ∪ ⋃ i ∈ Args.posFinset arity, (es i).subtrees

source

theorem Isotope.STm.mem_subtrees_op_iff {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {e : STm L A} {arity : Arity} (o : L.Op arity) (es : UArgs.Ix arity → STm L A) :

e ∈ (op o es).subtrees ↔ e = op o es ∨ ∃ i ∈ Args.posFinset arity, e ∈ (es i).subtrees

source

@[simp]

theorem Isotope.STm.mem_subtrees {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {e : STm L A} :

e ∈ e.subtrees

source

theorem Isotope.STm.mem_subtrees_use_iff {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {a : A} {e : STm L A} :

(∃ s ∈ e.subtrees, a ∈ s.use) ↔ a ∈ e.use

source

@[simp]

theorem Isotope.STm.subtrees_use {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {e : STm L A} :

⋃ s ∈ e.subtrees, s.use = e.use

source

def Isotope.STm.useL {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} :

STm L A → List A

Equations

(Isotope.STm.sym a).useL = [a]
(Isotope.STm.const a).useL = []
(Isotope.STm.op a es).useL = List.flatMap (fun (i : Isotope.UArgs.Ix arity) => (es i).useL) (Isotope.Args.posList arity)

Instances For

source

@[simp]

theorem Isotope.STm.useL_sym {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (a : A) :

(sym a).useL = [a]

source

@[simp]

theorem Isotope.STm.useL_const {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (c : L.Val) :

(const c).useL = []

source

theorem Isotope.STm.useL_op {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {arity : Arity} (o : L.Op arity) (es : UArgs.Ix arity → STm L A) :

(op o es).useL = List.flatMap (fun (i : UArgs.Ix arity) => (es i).useL) (Args.posList arity)

source

@[simp]

theorem Isotope.STm.mem_useL_iff {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {a : A} {e : STm L A} :

a ∈ e.useL ↔ a ∈ e.use

source

theorem Isotope.STm.useL_toSet {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (e : STm L A) :

{a : A | a ∈ e.useL} = e.use

source

def Isotope.STm.useF {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq A] :

STm L A → Finset A

Equations

(Isotope.STm.sym a).useF = {a}
(Isotope.STm.const a).useF = ∅
(Isotope.STm.op a es).useF = (Isotope.Args.posFinset arity).biUnion fun (i : Isotope.UArgs.Ix arity) => (es i).useF

Instances For

source

@[simp]

theorem Isotope.STm.mem_useF_iff {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq A] {a : A} {e : STm L A} :

a ∈ e.useF ↔ a ∈ e.use

source

@[simp]

theorem Isotope.STm.useL_toFinset {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq A] (e : STm L A) :

e.useL.toFinset = e.useF

source

theorem Isotope.STm.useF_toSet {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq A] (e : STm L A) :

{a : A | a ∈ e.useF} = e.use

source

def Isotope.STm.subtreesL {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} :

STm L A → List (STm L A)

Equations

(Isotope.STm.sym a).subtreesL = [Isotope.STm.sym a]
(Isotope.STm.const a).subtreesL = [Isotope.STm.const a]
(Isotope.STm.op a es).subtreesL = Isotope.STm.op a es :: List.flatMap (fun (i : Isotope.UArgs.Ix arity) => (es i).subtreesL) (Isotope.Args.posList arity)

Instances For

source

@[simp]

theorem Isotope.STm.subtreesL_sym {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {a : A} :

(sym a).subtreesL = [sym a]

source

@[simp]

theorem Isotope.STm.subtreesL_const {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {c : L.Val} :

(const c).subtreesL = [const c]

source

theorem Isotope.STm.subtreesL_op {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {arity : Arity} (o : L.Op arity) (es : UArgs.Ix arity → STm L A) :

(op o es).subtreesL = op o es :: List.flatMap (fun (i : UArgs.Ix arity) => (es i).subtreesL) (Args.posList arity)

source

@[simp]

theorem Isotope.STm.mem_subtreesL_iff {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {s e : STm L A} :

s ∈ e.subtreesL ↔ s ∈ e.subtrees

source

theorem Isotope.STm.subtreesL_toSet {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (e : STm L A) :

{s : STm L A | s ∈ e.subtreesL} = e.subtrees

source

def Isotope.STm.subtreesF {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq (STm L A)] :

STm L A → Finset (STm L A)

Equations

(Isotope.STm.sym a).subtreesF = {Isotope.STm.sym a}
(Isotope.STm.const a).subtreesF = {Isotope.STm.const a}
(Isotope.STm.op a es).subtreesF = {Isotope.STm.op a es} ∪ (Isotope.Args.posFinset arity).biUnion fun (i : Isotope.UArgs.Ix arity) => (es i).subtreesF

Instances For

source

@[simp]

theorem Isotope.STm.subtreesF_sym {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq (STm L A)] {a : A} :

(sym a).subtreesF = {sym a}

source

@[simp]

theorem Isotope.STm.subtreesF_const {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq (STm L A)] {c : L.Val} :

(const c).subtreesF = {const c}

source

theorem Isotope.STm.subtreesF_op {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq (STm L A)] {arity : Arity} (o : L.Op arity) (es : UArgs.Ix arity → STm L A) :

(op o es).subtreesF = {op o es} ∪ (Args.posFinset arity).biUnion fun (i : UArgs.Ix arity) => (es i).subtreesF

source

@[simp]

theorem Isotope.STm.mem_subtreesF_iff {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq (STm L A)] {s e : STm L A} :

s ∈ e.subtreesF ↔ s ∈ e.subtrees

source

@[simp]

theorem Isotope.STm.subtreesL_toFinset {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq (STm L A)] (e : STm L A) :

e.subtreesL.toFinset = e.subtreesF

source

theorem Isotope.STm.subtreesF_toSet {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} [DecidableEq (STm L A)] (e : STm L A) :

{s : STm L A | s ∈ e.subtreesF} = e.subtrees

source

def Isotope.STm.children {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} :

STm L A → List (STm L A)

Equations

(Isotope.STm.sym a).children = []
(Isotope.STm.const a).children = []
(Isotope.STm.op a es).children = List.map (fun (i : Isotope.UArgs.Ix arity) => es i) (Isotope.Args.posList arity)

Instances For

source

def Isotope.STm.childrenS {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (e : STm L A) :

Set (STm L A)

Equations

e.childrenS = {c : Isotope.STm L A | c ∈ e.children}

Instances For

source

@[simp]

theorem Isotope.STm.childrenS_sym {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (a : A) :

(sym a).childrenS = ∅

source

@[simp]

theorem Isotope.STm.childrenS_const {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (c : L.Val) :

(const c).childrenS = ∅

source

@[simp]

theorem Isotope.STm.childrenS_op {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} {arity : Arity} (o : L.Op arity) (es : UArgs.Ix arity → STm L A) :

(op o es).childrenS = {x : STm L A | ∃ i ∈ Args.posList arity, es i = x}

source

@[simp]

theorem Isotope.STm.childrenS_subset_subtrees {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (e : STm L A) :

e.childrenS ⊆ e.subtrees

source

def Isotope.STm.strictSubtrees {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} :

STm L A → Set (STm L A)

Equations

(Isotope.STm.sym a).strictSubtrees = ∅
(Isotope.STm.const a).strictSubtrees = ∅
(Isotope.STm.op a es).strictSubtrees = ⋃ i ∈ Isotope.Args.posFinset arity, (es i).subtrees

Instances For

source

@[simp]

theorem Isotope.STm.strictSubtrees_sym {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (a : A) :

(sym a).strictSubtrees = ∅

source

@[simp]

theorem Isotope.STm.strictSubtrees_const {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (c : L.Val) :

(const c).strictSubtrees = ∅

source

@[simp]

theorem Isotope.STm.strictSubtrees_subset_subtrees {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (e : STm L A) :

e.strictSubtrees ⊆ e.subtrees

source

theorem Isotope.STm.strictSubtrees_eq_subtrees_children {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} (e : STm L A) :

e.strictSubtrees = ⋃ c ∈ e.children, c.subtrees

source

def Isotope.STm.depth {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} :

STm L A → ℕ

Equations

(Isotope.STm.sym a).depth = 0
(Isotope.STm.const a).depth = 0
(Isotope.STm.op a es).depth = 1 + List.foldl (fun (acc : ℕ) (i : Isotope.UArgs.Ix arity) => max acc (es i).depth) 0 (Isotope.Args.posList arity)

Instances For

source

def Isotope.STm.size {Arity : Type uargs} [instArgs : Args Arity] {L : Lang Arity} {A : Type ua} :

STm L A → ℕ

Equations

(Isotope.STm.sym a).size = 1
(Isotope.STm.const a).size = 1
(Isotope.STm.op a es).size = 1 + List.foldl (fun (acc : ℕ) (i : Isotope.UArgs.Ix arity) => acc + (es i).size) 0 (Isotope.Args.posList arity)

Instances For