internlm/Lean-Github huggingface dataset:
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
⊢ (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)
Tactic:
split_ifs
Proof state after:
case pos
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
h✝ : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q

case neg
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
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) V tl (def_ X xs) ↔ Holds D I V 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
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
specialize ih (Function.updateListITE V hd.args (List.map V xs)) hd.q
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) (Function.updateListITE V hd.args (List.map V xs)) E_ref hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) E_ref (replace P zs H hd.q)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
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
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) (Function.updateListITE V hd.args (List.map V xs)) E_ref hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) E_ref (replace P zs H hd.q)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
simp only [replace_no_predVar P zs H hd.q hd.h2] at ih
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
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
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
apply Holds_coincide_PredVar
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ (I' D I V' (hd :: tl) P zs H).pred_const_ = I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ ∀ (P_1 : PredName) (ds : List D),
    predVarOccursIn P_1 ds.length hd.q → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ (I' D I V' (hd :: tl) P zs H).pred_const_ = I.pred_const_
Tactic:
simp only [I']
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ (Interpretation.usingPred D I fun Q ds =>
        if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H
        else I.pred_var_ Q ds).pred_const_ =
    I.pred_const_
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ (Interpretation.usingPred D I fun Q ds =>
        if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H
        else I.pred_var_ Q ds).pred_const_ =
    I.pred_const_
Tactic:
simp only [Interpretation.usingPred]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ ∀ (P_1 : PredName) (ds : List D),
    predVarOccursIn P_1 ds.length hd.q → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Tactic:
simp only [predVarOccursIn_iff_mem_predVarSet]
Proof state after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ ∀ (P_1 : PredName) (ds : List D),
    (P_1, ds.length) ∈ hd.q.predVarSet → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ ∀ (P_1 : PredName) (ds : List D),
    (P_1, ds.length) ∈ hd.q.predVarSet → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Tactic:
simp only [hd.h2]
Proof state after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ ∀ (P_1 : PredName) (ds : List D),
    (P_1, ds.length) ∈ ∅ → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
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
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ ∀ (P_1 : PredName) (ds : List D),
    (P_1, ds.length) ∈ ∅ → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Tactic:
simp
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) V tl (def_ X xs) ↔ Holds D I V tl (def_ X xs)
Tactic:
apply Holds_coincide_PredVar
Proof state after:
case h1
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ (I' D I V' (hd :: tl) P zs H).pred_const_ = I.pred_const_

case h2
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P_1 : PredName) (ds : List D),
    predVarOccursIn P_1 ds.length (def_ X xs) → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h1
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ (I' D I V' (hd :: tl) P zs H).pred_const_ = I.pred_const_
Tactic:
simp only [I']
Proof state after:
case h1
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ (Interpretation.usingPred D I fun Q ds =>
        if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H
        else I.pred_var_ Q ds).pred_const_ =
    I.pred_const_
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h1
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ (Interpretation.usingPred D I fun Q ds =>
        if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H
        else I.pred_var_ Q ds).pred_const_ =
    I.pred_const_
Tactic:
simp only [Interpretation.usingPred]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h2
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P_1 : PredName) (ds : List D),
    predVarOccursIn P_1 ds.length (def_ X xs) → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Tactic:
simp only [predVarOccursIn]
Proof state after:
case h2
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P_1 : PredName) (ds : List D), False → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case h2
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P_1 : PredName) (ds : List D), False → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
⊢ Holds D (I' D I V E P zs H) V E F ↔ Holds D I V E (replace P zs H F)
Tactic:
apply substitution_theorem_aux D I V V E F P zs H ∅
Proof state after:
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
⊢ admitsAux P zs H ∅ F

case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
h1 : admits P zs H F
⊢ ∀ x ∉ ∅, V x = V x