Theorem: FOL.NV.evalPrime_prime (FOL/NV/Margaris/Prop.lean)

State before:
F : Formula
V : VarBoolAssignment
h1 : F.IsPrime
⊢ evalPrime V F = (V F = true)
Tactic:
induction F
State after:
case pred_const_
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_const_ a✝¹ a✝).IsPrime
⊢ evalPrime V (pred_const_ a✝¹ a✝) = (V (pred_const_ a✝¹ a✝) = true)

case pred_var_
V : VarBoolAssignment
a✝¹ : PredName
a✝ : List VarName
h1 : (pred_var_ a✝¹ a✝).IsPrime
⊢ evalPrime V (pred_var_ a✝¹ a✝) = (V (pred_var_ a✝¹ a✝) = true)

case eq_
V : VarBoolAssignment
a✝¹ a✝ : VarName
h1 : (eq_ a✝¹ a✝).IsPrime
⊢ evalPrime V (eq_ a✝¹ a✝) = (V (eq_ a✝¹ a✝) = true)

case true_
V : VarBoolAssignment
h1 : true_.IsPrime
⊢ evalPrime V true_ = (V true_ = true)

case false_
V : VarBoolAssignment
h1 : false_.IsPrime
⊢ evalPrime V false_ = (V false_ = true)

case not_
V : VarBoolAssignment
a✝ : Formula
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : a✝.not_.IsPrime
⊢ evalPrime V a✝.not_ = (V a✝.not_ = true)

case imp_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.imp_ a✝).IsPrime
⊢ evalPrime V (a✝¹.imp_ a✝) = (V (a✝¹.imp_ a✝) = true)

case and_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.and_ a✝).IsPrime
⊢ evalPrime V (a✝¹.and_ a✝) = (V (a✝¹.and_ a✝) = true)

case or_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.or_ a✝).IsPrime
⊢ evalPrime V (a✝¹.or_ a✝) = (V (a✝¹.or_ a✝) = true)

case iff_
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrime V (a✝¹.iff_ a✝) = (V (a✝¹.iff_ a✝) = true)

case forall_
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (forall_ a✝¹ a✝).IsPrime
⊢ evalPrime V (forall_ a✝¹ a✝) = (V (forall_ a✝¹ a✝) = true)

case exists_
V : VarBoolAssignment
a✝¹ : VarName
a✝ : Formula
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (exists_ a✝¹ a✝).IsPrime
⊢ evalPrime V (exists_ a✝¹ a✝) = (V (exists_ a✝¹ a✝) = true)

case def_
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrime V (def_ a✝¹ a✝) = (V (def_ a✝¹ a✝) = true)

State before:
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrime V (a✝¹.iff_ a✝) = (V (a✝¹.iff_ a✝) = true)
Tactic:
case true_ | false_ | not_ | imp_ | and_ | or_ | iff_ =>
  simp only [Formula.IsPrime] at h1
State after:
no goals

State before:
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrime V (def_ a✝¹ a✝) = (V (def_ a✝¹ a✝) = true)
Tactic:
case pred_const_ | pred_var_ | eq_ | forall_ | exists_ | def_ =>
  rfl
State after:
no goals

State before:
V : VarBoolAssignment
a✝¹ a✝ : Formula
a_ih✝¹ : a✝¹.IsPrime → evalPrime V a✝¹ = (V a✝¹ = true)
a_ih✝ : a✝.IsPrime → evalPrime V a✝ = (V a✝ = true)
h1 : (a✝¹.iff_ a✝).IsPrime
⊢ evalPrime V (a✝¹.iff_ a✝) = (V (a✝¹.iff_ a✝) = true)
Tactic:
simp only [Formula.IsPrime] at h1
State after:
no goals

State before:
V : VarBoolAssignment
a✝¹ : DefName
a✝ : List VarName
h1 : (def_ a✝¹ a✝).IsPrime
⊢ evalPrime V (def_ a✝¹ a✝) = (V (def_ a✝¹ a✝) = true)
Tactic:
rfl
State after:
no goals