internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ Function.updateITE V x d v = V' v
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ (if v = x then d else V v) = V' v
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ (if v = x then d else V v) = V' v
Tactic:
simp at a1
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∧ ¬v = x
⊢ (if v = x then d else V v) = V' v
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∧ ¬v = x
⊢ (if v = x then d else V v) = V' v
Tactic:
push_neg at a1
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∧ v ≠ x
⊢ (if v = x then d else V v) = V' v
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∧ v ≠ x
⊢ (if v = x then d else V v) = V' v
Tactic:
cases a1
Proof state after:
case h.intro
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
left✝ : v ∉ binders
right✝ : v ≠ x
⊢ (if v = x then d else V v) = V' v
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ (if v = x then d else V v) = V' v
Tactic:
case h.intro a1_left a1_right =>
  simp only [if_neg a1_right]
  exact h2 v a1_left
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ (∀ (d : D), Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x d) E_ref phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V x d) E_ref (replace P zs H phi)
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ∀ (a : D),
    Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x a) E_ref phi ↔
      Holds D I (Function.updateITE V x a) E_ref (replace P zs H phi)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ (∃ d, Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x d) E_ref phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) E_ref (replace P zs H phi)
Tactic:
apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ∀ (a : D),
    Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x a) E_ref phi ↔
      Holds D I (Function.updateITE V x a) E_ref (replace P zs H phi)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ (if v = x then d else V v) = V' v
Tactic:
simp only [if_neg a1_right]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V v = V' v
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V v = V' v
Tactic:
exact h2 v a1_left
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (replace P zs H (def_ X xs))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (def_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (def_ X xs)
Tactic:
simp only [E_ref]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' [] P zs H) V [] (def_ X xs) ↔ Holds D I V [] (def_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' [] P zs H) V [] (def_ X xs) ↔ Holds D I V [] (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (replace P zs H (def_ X xs))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (def_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (def_ X xs)
Tactic:
simp only [E_ref]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' (hd :: tl) P zs H) V (hd :: tl) (def_ X xs) ↔ Holds D I V (hd :: tl) (def_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' (hd :: tl) P zs H) V (hd :: tl) (def_ X xs) ↔ Holds D I V (hd :: tl) (def_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D (I' D I V' (hd :: tl) P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D (I' D I V' (hd :: tl) P zs H) V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)