internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.imp_ psi)
Tactic:
apply isFreeInInd.imp_right_
Proof state after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.and_ psi)
Tactic:
apply isFreeInInd.and_right_
Proof state after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.or_ psi)
Tactic:
apply isFreeInInd.or_right_
Proof state after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
Tactic:
apply isFreeInInd.iff_right_
Proof state after:
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : ¬v = x ∧ isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)
Tactic:
cases h1
Proof state after:
case intro
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
left✝ : ¬v = x
right✝ : isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)
Tactic:
first | apply isFreeInInd.forall_ | apply isFreeInInd.exists_
Proof state after:
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ ¬v = x

case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v phi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v (forall_ x phi)
Tactic:
apply isFreeInInd.forall_
Proof state after:
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ ¬v = x

case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v phi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)
Tactic:
apply isFreeInInd.exists_
Proof state after:
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ ¬v = x

case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v phi
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ ¬v = x
Tactic:
exact h1_left
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_imp_isFreeInInd
Proof state before:
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v phi
Tactic:
exact phi_ih h1_right
Proof state after:
no goals
Theorem: FOL.NV.isFreeInInd_imp_isFreeIn
Proof state before:
v : VarName
F : Formula
h1 : isFreeInInd v F
⊢ isFreeIn v F
Tactic:
induction h1
Proof state after:
case pred_const_
v : VarName
F : Formula
X✝ : PredName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (pred_const_ X✝ xs✝)

case pred_var_
v : VarName
F : Formula
X✝ : PredName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (pred_var_ X✝ xs✝)

case eq_
v : VarName
F : Formula
x✝ y✝ : VarName
a✝ : v = x✝ ∨ v = y✝
⊢ isFreeIn v (eq_ x✝ y✝)

case not_
v : VarName
F phi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v phi✝.not_

case imp_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.imp_ psi✝)

case imp_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.imp_ psi✝)

case and_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.and_ psi✝)

case and_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.and_ psi✝)

case or_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.or_ psi✝)

case or_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.or_ psi✝)

case iff_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.iff_ psi✝)

case iff_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.iff_ psi✝)

case forall_
v : VarName
F : Formula
x✝ : VarName
phi✝ : Formula
a✝¹ : ¬v = x✝
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (forall_ x✝ phi✝)

case exists_
v : VarName
F : Formula
x✝ : VarName
phi✝ : Formula
a✝¹ : ¬v = x✝
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (exists_ x✝ phi✝)

case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (def_ X✝ xs✝)
Theorem: FOL.NV.isFreeInInd_imp_isFreeIn
Proof state before:
case pred_const_
v : VarName
F : Formula
X✝ : PredName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (pred_const_ X✝ xs✝)

case pred_var_
v : VarName
F : Formula
X✝ : PredName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (pred_var_ X✝ xs✝)

case eq_
v : VarName
F : Formula
x✝ y✝ : VarName
a✝ : v = x✝ ∨ v = y✝
⊢ isFreeIn v (eq_ x✝ y✝)

case not_
v : VarName
F phi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v phi✝.not_

case imp_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.imp_ psi✝)

case imp_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.imp_ psi✝)

case and_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.and_ psi✝)

case and_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.and_ psi✝)

case or_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.or_ psi✝)

case or_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.or_ psi✝)

case iff_left_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (phi✝.iff_ psi✝)

case iff_right_
v : VarName
F phi✝ psi✝ : Formula
a✝ : isFreeInInd v psi✝
a_ih✝ : isFreeIn v psi✝
⊢ isFreeIn v (phi✝.iff_ psi✝)

case forall_
v : VarName
F : Formula
x✝ : VarName
phi✝ : Formula
a✝¹ : ¬v = x✝
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (forall_ x✝ phi✝)

case exists_
v : VarName
F : Formula
x✝ : VarName
phi✝ : Formula
a✝¹ : ¬v = x✝
a✝ : isFreeInInd v phi✝
a_ih✝ : isFreeIn v phi✝
⊢ isFreeIn v (exists_ x✝ phi✝)

case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (def_ X✝ xs✝)
Tactic:
all_goals
  simp only [isFreeIn]
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeInInd_imp_isFreeIn
Proof state before:
case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ isFreeIn v (def_ X✝ xs✝)
Tactic:
simp only [isFreeIn]
Proof state after:
case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ v ∈ xs✝
Theorem: FOL.NV.isFreeInInd_imp_isFreeIn
Proof state before:
case def_
v : VarName
F : Formula
X✝ : DefName
xs✝ : List VarName
a✝ : v ∈ xs✝
⊢ v ∈ xs✝
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_isFreeInInd
Proof state before:
v : VarName
F : Formula
⊢ isFreeIn v F ↔ isFreeInInd v F
Tactic:
constructor
Proof state after:
case mp
v : VarName
F : Formula
⊢ isFreeIn v F → isFreeInInd v F

case mpr
v : VarName
F : Formula
⊢ isFreeInInd v F → isFreeIn v F
Theorem: FOL.NV.isFreeIn_iff_isFreeInInd
Proof state before:
case mp
v : VarName
F : Formula
⊢ isFreeIn v F → isFreeInInd v F
Tactic:
exact isFreeIn_imp_isFreeInInd v F
Proof state after:
no goals
Theorem: FOL.NV.isFreeIn_iff_isFreeInInd
Proof state before:
case mpr
v : VarName
F : Formula
⊢ isFreeInInd v F → isFreeIn v F
Tactic:
exact isFreeInInd_imp_isFreeIn v F
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
F : Formula
⊢ predVarOccursIn P n F ↔ (P, n) ∈ F.predVarSet
Tactic:
induction F
Proof state after:
case pred_const_
P : PredName
n : ℕ
a✝¹ : PredName
a✝ : List VarName
⊢ predVarOccursIn P n (pred_const_ a✝¹ a✝) ↔ (P, n) ∈ (pred_const_ a✝¹ a✝).predVarSet

case pred_var_
P : PredName
n : ℕ
a✝¹ : PredName
a✝ : List VarName
⊢ predVarOccursIn P n (pred_var_ a✝¹ a✝) ↔ (P, n) ∈ (pred_var_ a✝¹ a✝).predVarSet

case eq_
P : PredName
n : ℕ
a✝¹ a✝ : VarName
⊢ predVarOccursIn P n (eq_ a✝¹ a✝) ↔ (P, n) ∈ (eq_ a✝¹ a✝).predVarSet

case true_
P : PredName
n : ℕ
⊢ predVarOccursIn P n true_ ↔ (P, n) ∈ true_.predVarSet

case false_
P : PredName
n : ℕ
⊢ predVarOccursIn P n false_ ↔ (P, n) ∈ false_.predVarSet

case not_
P : PredName
n : ℕ
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n a✝.not_ ↔ (P, n) ∈ a✝.not_.predVarSet

case imp_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.imp_ a✝) ↔ (P, n) ∈ (a✝¹.imp_ a✝).predVarSet

case and_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.and_ a✝) ↔ (P, n) ∈ (a✝¹.and_ a✝).predVarSet

case or_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.or_ a✝) ↔ (P, n) ∈ (a✝¹.or_ a✝).predVarSet

case iff_
P : PredName
n : ℕ
a✝¹ a✝ : Formula
a_ih✝¹ : predVarOccursIn P n a✝¹ ↔ (P, n) ∈ a✝¹.predVarSet
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (a✝¹.iff_ a✝) ↔ (P, n) ∈ (a✝¹.iff_ a✝).predVarSet

case forall_
P : PredName
n : ℕ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (forall_ a✝¹ a✝) ↔ (P, n) ∈ (forall_ a✝¹ a✝).predVarSet

case exists_
P : PredName
n : ℕ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : predVarOccursIn P n a✝ ↔ (P, n) ∈ a✝.predVarSet
⊢ predVarOccursIn P n (exists_ a✝¹ a✝) ↔ (P, n) ∈ (exists_ a✝¹ a✝).predVarSet

case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ predVarOccursIn P n (def_ a✝¹ a✝) ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
X : DefName
xs : List VarName
⊢ False ↔ (P, n) ∈ ∅
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
x y : VarName
⊢ False ↔ (P, n) ∈ ∅
Tactic:
case eq_ x y =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
⊢ False ↔ (P, n) ∈ ∅
Tactic:
case true_ | false_ =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
phi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
⊢ predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
Tactic:
case not_ phi phi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
phi psi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
psi_ih : predVarOccursIn P n psi ↔ (P, n) ∈ psi.predVarSet
⊢ predVarOccursIn P n phi ∨ predVarOccursIn P n psi ↔ (P, n) ∈ phi.predVarSet ∪ psi.predVarSet
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp
  tauto
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
x : VarName
phi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
⊢ predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ predVarOccursIn P n (def_ a✝¹ a✝) ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet
Tactic:
simp only [predVarOccursIn]
Proof state after:
case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet
Tactic:
simp only [Formula.predVarSet]
Proof state after:
case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ (P, n) ∈ ∅
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
X : DefName
xs : List VarName
⊢ False ↔ (P, n) ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
x y : VarName
⊢ False ↔ (P, n) ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
⊢ False ↔ (P, n) ∈ ∅
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
phi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
⊢ predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
phi psi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
psi_ih : predVarOccursIn P n psi ↔ (P, n) ∈ psi.predVarSet
⊢ predVarOccursIn P n phi ∨ predVarOccursIn P n psi ↔ (P, n) ∈ phi.predVarSet ∪ psi.predVarSet
Tactic:
simp
Proof state after:
P : PredName
n : ℕ
phi psi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
psi_ih : predVarOccursIn P n psi ↔ (P, n) ∈ psi.predVarSet
⊢ predVarOccursIn P n phi ∨ predVarOccursIn P n psi ↔ (P, n) ∈ phi.predVarSet ∨ (P, n) ∈ psi.predVarSet
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
phi psi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
psi_ih : predVarOccursIn P n psi ↔ (P, n) ∈ psi.predVarSet
⊢ predVarOccursIn P n phi ∨ predVarOccursIn P n psi ↔ (P, n) ∈ phi.predVarSet ∨ (P, n) ∈ psi.predVarSet
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.predVarOccursIn_iff_mem_predVarSet
Proof state before:
P : PredName
n : ℕ
x : VarName
phi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
⊢ predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_imp_occursIn
Proof state before:
v : VarName
F : Formula
h1 : isBoundIn v F
⊢ occursIn v F
Tactic:
induction F
Proof state after:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isBoundIn v (pred_const_ a✝¹ a✝)
⊢ occursIn v (pred_const_ a✝¹ a✝)

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isBoundIn v (pred_var_ a✝¹ a✝)
⊢ occursIn v (pred_var_ a✝¹ a✝)

case eq_
v a✝¹ a✝ : VarName
h1 : isBoundIn v (eq_ a✝¹ a✝)
⊢ occursIn v (eq_ a✝¹ a✝)

case true_
v : VarName
h1 : isBoundIn v true_
⊢ occursIn v true_

case false_
v : VarName
h1 : isBoundIn v false_
⊢ occursIn v false_

case not_
v : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝.not_
⊢ occursIn v a✝.not_

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (a✝¹.imp_ a✝)
⊢ occursIn v (a✝¹.imp_ a✝)

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (a✝¹.and_ a✝)
⊢ occursIn v (a✝¹.and_ a✝)

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (a✝¹.or_ a✝)
⊢ occursIn v (a✝¹.or_ a✝)

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (a✝¹.iff_ a✝)
⊢ occursIn v (a✝¹.iff_ a✝)

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (forall_ a✝¹ a✝)
⊢ occursIn v (forall_ a✝¹ a✝)

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (exists_ a✝¹ a✝)
⊢ occursIn v (exists_ a✝¹ a✝)

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isBoundIn v (def_ a✝¹ a✝)
⊢ occursIn v (def_ a✝¹ a✝)
Theorem: FOL.NV.isBoundIn_imp_occursIn
Proof state before:
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isBoundIn v (pred_const_ a✝¹ a✝)
⊢ occursIn v (pred_const_ a✝¹ a✝)

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
h1 : isBoundIn v (pred_var_ a✝¹ a✝)
⊢ occursIn v (pred_var_ a✝¹ a✝)

case eq_
v a✝¹ a✝ : VarName
h1 : isBoundIn v (eq_ a✝¹ a✝)
⊢ occursIn v (eq_ a✝¹ a✝)

case true_
v : VarName
h1 : isBoundIn v true_
⊢ occursIn v true_

case false_
v : VarName
h1 : isBoundIn v false_
⊢ occursIn v false_

case not_
v : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝.not_
⊢ occursIn v a✝.not_

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (a✝¹.imp_ a✝)
⊢ occursIn v (a✝¹.imp_ a✝)

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (a✝¹.and_ a✝)
⊢ occursIn v (a✝¹.and_ a✝)

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (a✝¹.or_ a✝)
⊢ occursIn v (a✝¹.or_ a✝)

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (a✝¹.iff_ a✝)
⊢ occursIn v (a✝¹.iff_ a✝)

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (forall_ a✝¹ a✝)
⊢ occursIn v (forall_ a✝¹ a✝)

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v (exists_ a✝¹ a✝)
⊢ occursIn v (exists_ a✝¹ a✝)

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isBoundIn v (def_ a✝¹ a✝)
⊢ occursIn v (def_ a✝¹ a✝)
Tactic:
all_goals
  simp only [isBoundIn] at h1
Proof state after:
case not_
v : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝
⊢ occursIn v a✝.not_

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (a✝¹.imp_ a✝)

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (a✝¹.and_ a✝)

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (a✝¹.or_ a✝)

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (a✝¹.iff_ a✝)

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : v = a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (forall_ a✝¹ a✝)

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : v = a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (exists_ a✝¹ a✝)
Theorem: FOL.NV.isBoundIn_imp_occursIn
Proof state before:
case not_
v : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝
⊢ occursIn v a✝.not_

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (a✝¹.imp_ a✝)

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (a✝¹.and_ a✝)

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (a✝¹.or_ a✝)

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isBoundIn v a✝¹ → occursIn v a✝¹
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : isBoundIn v a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (a✝¹.iff_ a✝)

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : v = a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (forall_ a✝¹ a✝)

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : v = a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (exists_ a✝¹ a✝)
Tactic:
all_goals
  simp only [occursIn]
  tauto
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_imp_occursIn
Proof state before:
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : isBoundIn v (def_ a✝¹ a✝)
⊢ occursIn v (def_ a✝¹ a✝)
Tactic:
simp only [isBoundIn] at h1
Proof state after:
no goals
Theorem: FOL.NV.isBoundIn_imp_occursIn
Proof state before:
case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : v = a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (exists_ a✝¹ a✝)
Tactic:
simp only [occursIn]
Proof state after:
case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : v = a✝¹ ∨ isBoundIn v a✝
⊢ v = a✝¹ ∨ occursIn v a✝
Theorem: FOL.NV.isBoundIn_imp_occursIn
Proof state before:
case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : v = a✝¹ ∨ isBoundIn v a✝
⊢ v = a✝¹ ∨ occursIn v a✝
Tactic:
tauto
Proof state after:
no goals