Metatheory for Expression.freeVars (defined in Subst.lean): membership lemmas that unfold freeVars's foldl (· ∪ ·) list cases to plain ∃ e ∈ es, …, plus the same freeVars vocabulary lifted over ComputableGuardedPlusCal.

def ComputableTLAPlus.Expression.FreshIn {α : Type} (x : String) (e : Expression α) : Prop

x does not occur free in e — the freshness side condition every binder-introducing lemma needs.

Equations

• ComputableTLAPlus.Expression.FreshIn x e = (x ∉ e.freeVars)

theorem ComputableTLAPlus.Expression.not_mem_of_fresh {α : Type} {x : String} {inScope : List String} {e : Expression α} (fresh : x ∉ inScope) (sub : ∀ z ∈ e.freeVars, z ∈ inScope) : x ∉ e.freeVars

If x avoids every name e could possibly read, x isn't one of them. The bridge from a scope-membership fact (WellFormedness.WellScoped's vocabulary) to an actual freshness fact (ExprSemantics.evalSubst's vocabulary): a with's bound name is fresh against inScope by construction, and a substituted-in expression's free variables are always a subset of inScope (it can only mention already-declared names), so the two never collide.

Membership lemmas

freeVars's list cases fold (· ∪ ·) over es.attach.map (…); these unfold that fold to a plain ∃ e ∈ es, …, so evalLocal/evalSubst's inductions can move a memory-agreement hypothesis from a compound expression down to its components.

theorem ComputableTLAPlus.Expression.mem_freeVars_opCall {α : Type} {z : String} {f : Expression α} {es : List (Expression α)} : z ∈ (f.opCall es).freeVars ↔ z ∈ f.freeVars ∨ ∃ e ∈ es, z ∈ e.freeVars

theorem ComputableTLAPlus.Expression.mem_freeVars_set {α : Type} {z : String} {es : List (Expression α)} {τ : α} : z ∈ (set es τ).freeVars ↔ ∃ e ∈ es, z ∈ e.freeVars

theorem ComputableTLAPlus.Expression.mem_freeVars_seq {α : Type} {z : String} {es : List (Expression α)} {τ : α} : z ∈ (seq es τ).freeVars ↔ ∃ e ∈ es, z ∈ e.freeVars

theorem ComputableTLAPlus.Expression.mem_freeVars_tuple {α : Type} {z : String} {es : List (α × Expression α)} : z ∈ (tuple es).freeVars ↔ ∃ e ∈ es, z ∈ e.2.freeVars

theorem ComputableTLAPlus.Expression.mem_freeVars_record {α : Type} {z : String} {fs : List (α × String × Expression α)} : z ∈ (record fs).freeVars ↔ ∃ f ∈ fs, z ∈ f.2.2.freeVars

theorem ComputableTLAPlus.Expression.mem_freeVars_case {α : Type} {z : String} {bs : List (Expression α × Expression α)} {other : Option (Expression α)} {τ : α} : z ∈ (case bs other τ).freeVars ↔ (∃ b ∈ bs, z ∈ b.1.freeVars ∨ z ∈ b.2.freeVars) ∨ ∃ (e : Expression α), other = some e ∧ z ∈ e.freeVars

theorem ComputableTLAPlus.Expression.mem_freeVars_except {α : Type} {z : String} {f : Expression α} {τ : α} {upds : List (List (String ⊕ Expression α) × Expression α)} : z ∈ (f.except τ upds).freeVars ↔ z ∈ f.freeVars ∨ ∃ u ∈ upds, (∃ (e : Expression α), Sum.inr e ∈ u.1 ∧ z ∈ e.freeVars) ∨ z ∈ u.2.freeVars

theorem ComputableTLAPlus.Expression.mem_freeVars_except_single {α : Type} {z : String} {f : Expression α} {τ : α} {path : List (String ⊕ Expression α)} {rhs : Expression α} : z ∈ (f.except τ [(path, rhs)]).freeVars ↔ z ∈ f.freeVars ∨ (∃ (e : Expression α), Sum.inr e ∈ path ∧ z ∈ e.freeVars) ∨ z ∈ rhs.freeVars

De Bruijn traversals

liftBound/openVar/close/subst/instantiate are each mapVars f 0 for a specific per-node f. freeVars_mapVars_subset bounds the free names of a mapVars result once — every other free-variable fact about those operations is a corollary.

theorem ComputableTLAPlus.Expression.freeVars_mapVars_subset {α : Type} {f : ℕ → α → Origin → SourceSpan → Expression α} {S : Finset String} (hf : ∀ (k : ℕ) (τ : α) (o : Origin) (pos : SourceSpan), ∀ z ∈ (f k τ o pos).freeVars, (z ∈ match o with | TypedTLAPlus.Origin.free n => {n} | x => ∅) ∨ z ∈ S) (k : ℕ) (e : Expression α) {z : String} : z ∈ (mapVars f k e).freeVars → z ∈ e.freeVars ∨ z ∈ S

Every free name of e.mapVars f k is either a free name f keeps at some .var _ (.free _) node of e, or a name in S — the extra set f may introduce at .bound nodes.

theorem ComputableTLAPlus.Expression.freeVars_liftBound_subset {α : Type} {d : ℕ} {e : Expression α} : (liftBound d e).freeVars ⊆ e.freeVars

liftBound shifts .bound indices and never touches a .free name.

theorem ComputableTLAPlus.Expression.freeVars_openVar_subset {α : Type} {x : String} {e : Expression α} : (openVar x e).freeVars ⊆ insert x e.freeVars

openVar turns the removed binder's index into the free name x, and moves no other name in or out.

theorem ComputableTLAPlus.Expression.freeVars_openVar_erase {α : Type} {x : String} {e : Expression α} : (openVar x e).freeVars.erase x ⊆ e.freeVars

A name free in e.openVar x, other than x itself, was already free in e.

theorem ComputableTLAPlus.Expression.freeVars_instantiate {α : Type} {args : List (Expression α)} {body : Expression α} {z : String} (hz : z ∈ (instantiate args body).freeVars) : z ∈ body.freeVars ∨ ∃ a ∈ args, z ∈ a.freeVars

A name free after instantiating the outermost binders is free in the body or in one of the instantiated arguments.

theorem ComputableTLAPlus.Expression.subst_fresh {α : Type} {x : String} {e' : Expression α} (t : Expression α) : x ∉ t.freeVars → subst x e' t = t

subst of a name not free in the target is the identity.

theorem ComputableTLAPlus.Expression.subst_instantiate {α : Type} {x : String} {e' : Expression α} (hlc : e'.LC) {body : Expression α} (hbody : x ∉ body.freeVars) (args : List (Expression α)) : subst x e' (instantiate args body) = instantiate (List.map (subst x e') args) body

subst distributes over instantiate when the substituend is locally closed and the body is closed (Ξ.WellScoped gives operator bodies freeVars = ∅).

Lifted over ComputableGuardedPlusCal — flat by construction (module doc, Core/GuardedPlusCal/Syntax.lean), so every Expr field is a direct component, not a nested Block: no well-founded recursion is needed here, unlike Expression.freeVars above.

def GuardedPlusCal.Ref.freeVars (r : ComputableGuardedPlusCal.Ref) : Finset String

Every name a Ref's base variable and index expressions read. The base name itself is a use, same as any other Expression.var occurrence — a Ref is how a statement spells "read/write this variable", not a binder.

Equations

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

theorem GuardedPlusCal.Ref.name_mem_freeVars (r : ComputableGuardedPlusCal.Ref) : r.name ∈ freeVars r

The base name is one of them — the {r.name} ∪ … above, named, so that a freshness hypothesis stated over a whole Ref yields the inequality against r.name that memory lemmas need.

def GuardedPlusCal.Multicast.freeVars (m : ComputableGuardedPlusCal.Multicast) : Finset String

set's recipients are read in the enclosing scope; recipient then binds inside val, same shape as Expression.fn/.map'.

Equations

• GuardedPlusCal.Multicast.freeVars m = ComputableTLAPlus.Expression.freeVars m.set ∪ (ComputableTLAPlus.Expression.freeVars m.val).erase m.recipient

def GuardedPlusCal.Statement.freeVars {b b' : Bool} (S : ComputableGuardedPlusCal.Statement b b') : Finset String

Every name a statement reads — every Expr/Ref field's free variables, unioned. A with's own bound name is not included (it's introduced, not read); its domain/bound expression e is.

Equations

• (GuardedPlusCal.Statement.with name ann bound e).freeVars = ComputableTLAPlus.Expression.freeVars e
• (GuardedPlusCal.Statement.await e).freeVars = ComputableTLAPlus.Expression.freeVars e
• (GuardedPlusCal.Statement.receive c r coe).freeVars = c.freeVars ∪ r.freeVars
• GuardedPlusCal.Statement.skip.freeVars = ∅
• (GuardedPlusCal.Statement.print e).freeVars = ComputableTLAPlus.Expression.freeVars e
• (GuardedPlusCal.Statement.assert e).freeVars = ComputableTLAPlus.Expression.freeVars e
• (GuardedPlusCal.Statement.send c e).freeVars = c.freeVars ∪ ComputableTLAPlus.Expression.freeVars e
• (GuardedPlusCal.Statement.multicast c filter).freeVars = filter.freeVars
• (GuardedPlusCal.Statement.assign r e).freeVars = r.freeVars ∪ ComputableTLAPlus.Expression.freeVars e
• (GuardedPlusCal.Statement.goto label).freeVars = ∅

def GuardedPlusCal.Block.freeVars {g b : Bool} (B : Block (ComputableGuardedPlusCal.Statement g) b) : Finset String

Every name any statement in B reads.

Equations

• B.freeVars = List.foldl (fun (x1 x2 : Finset String) => x1 ∪ x2) ∅ (List.map GuardedPlusCal.Statement.freeVars B.begin) ∪ GuardedPlusCal.Statement.freeVars B.last

def GuardedPlusCal.AtomicBranch.FreshIn (x : String) (Br : ComputableGuardedPlusCal.AtomicBranch) : Prop

x is read nowhere in Br — precondition guard list (if any) and action block alike. The AtomicBranch-level freshness side condition the reorder_assign_guard pair needs: a preceding action's assigned name must stay fresh in every later guard for the substitution 𝒞_reord performs to be sound.

Equations

• GuardedPlusCal.AtomicBranch.FreshIn x Br = (x ∉ (match Br.precondition with | none => ∅ | some B => B.freeVars) ∪ Br.action.freeVars)