Theorem: repl_in_F_non_occ_eq (Pdl/Substitution.lean)

State before:
x : ℕ
φ ρ : Formula
⊢ x ∉ voc φ → repl_in_F x ρ φ = φ
Tactic:
intro x_notin_phi
State after:
x : ℕ
φ ρ : Formula
x_notin_phi : x ∉ voc φ
⊢ repl_in_F x ρ φ = φ

State before:
x : ℕ
φ ρ : Formula
x_notin_phi : x ∉ voc φ
⊢ repl_in_F x ρ φ = φ
Tactic:
cases φ
State after:
case bottom
x : ℕ
ρ : Formula
x_notin_phi : x ∉ voc Formula.bottom
⊢ repl_in_F x ρ Formula.bottom = Formula.bottom

case atom_prop
x : ℕ
ρ : Formula
a✝ : ℕ
x_notin_phi : x ∉ voc (·a✝)
⊢ repl_in_F x ρ (·a✝) = ·a✝

case neg
x : ℕ
ρ a✝ : Formula
x_notin_phi : x ∉ voc (~a✝)
⊢ repl_in_F x ρ (~a✝) = (~a✝)

case and
x : ℕ
ρ a✝¹ a✝ : Formula
x_notin_phi : x ∉ voc (a✝¹⋀a✝)
⊢ repl_in_F x ρ (a✝¹⋀a✝) = a✝¹⋀a✝

case box
x : ℕ
ρ : Formula
a✝¹ : Program
a✝ : Formula
x_notin_phi : x ∉ voc (⌈a✝¹⌉a✝)
⊢ repl_in_F x ρ (⌈a✝¹⌉a✝) = ⌈a✝¹⌉a✝

State before:
x : ℕ
ρ : Formula
x_notin_phi : x ∉ voc Formula.bottom
⊢ repl_in_F x ρ Formula.bottom = Formula.bottom
Tactic:
case bottom => simp
State after:
no goals

State before:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
⊢ repl_in_F x ρ (·c) = ·c
Tactic:
case atom_prop c =>
  simp only [repl_in_F, beq_iff_eq, ite_eq_right_iff]
  intro c_is_x; simp [voc,vocabOfFormula] at *; tauto
State after:
no goals

State before:
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ voc (~φ0)
⊢ repl_in_F x ρ (~φ0) = (~φ0)
Tactic:
case neg φ0 =>
  simp [voc,vocabOfFormula] at *
  apply repl_in_F_non_occ_eq; tauto
State after:
no goals

State before:
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ voc (φ1⋀φ2)
⊢ repl_in_F x ρ (φ1⋀φ2) = φ1⋀φ2
Tactic:
case and φ1 φ2 =>
  simp [voc,vocabOfFormula] at *
  constructor <;> (apply repl_in_F_non_occ_eq ; tauto)
State after:
no goals

State before:
x : ℕ
ρ : Formula
x_notin_phi : x ∉ voc Formula.bottom
⊢ repl_in_F x ρ Formula.bottom = Formula.bottom
Tactic:
simp
State after:
no goals

State before:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
⊢ repl_in_F x ρ (·c) = ·c
Tactic:
simp only [repl_in_F, beq_iff_eq, ite_eq_right_iff]
State after:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
⊢ c = x → ρ = ·c

State before:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
⊢ c = x → ρ = ·c
Tactic:
intro c_is_x
State after:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
c_is_x : c = x
⊢ ρ = ·c

State before:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
c_is_x : c = x
⊢ ρ = ·c
Tactic:
simp [voc,vocabOfFormula] at *
State after:
x : ℕ
ρ : Formula
c : ℕ
c_is_x : c = x
x_notin_phi : ¬x = c
⊢ ρ = ·c

State before:
x : ℕ
ρ : Formula
c : ℕ
c_is_x : c = x
x_notin_phi : ¬x = c
⊢ ρ = ·c
Tactic:
tauto
State after:
no goals

State before:
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ voc (~φ0)
⊢ repl_in_F x ρ (~φ0) = (~φ0)
Tactic:
simp [voc,vocabOfFormula] at *
State after:
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ vocabOfFormula φ0
⊢ repl_in_F x ρ φ0 = φ0

State before:
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ vocabOfFormula φ0
⊢ repl_in_F x ρ φ0 = φ0
Tactic:
apply repl_in_F_non_occ_eq
State after:
case a
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ vocabOfFormula φ0
⊢ x ∉ voc φ0

State before:
case a
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ vocabOfFormula φ0
⊢ x ∉ voc φ0
Tactic:
tauto
State after:
no goals

State before:
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ voc (φ1⋀φ2)
⊢ repl_in_F x ρ (φ1⋀φ2) = φ1⋀φ2
Tactic:
simp [voc,vocabOfFormula] at *
State after:
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ repl_in_F x ρ φ1 = φ1 ∧ repl_in_F x ρ φ2 = φ2

State before:
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ repl_in_F x ρ φ1 = φ1 ∧ repl_in_F x ρ φ2 = φ2
Tactic:
constructor <;> (apply repl_in_F_non_occ_eq ; tauto)
State after:
no goals

State before:
case right
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ repl_in_F x ρ φ2 = φ2
Tactic:
apply repl_in_F_non_occ_eq
State after:
case right.a
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ x ∉ voc φ2

State before:
case right.a
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ x ∉ voc φ2
Tactic:
tauto
State after:
no goals

State before:
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ voc (⌈α⌉φ0)
⊢ repl_in_F x ρ (⌈α⌉φ0) = ⌈α⌉φ0
Tactic:
simp [voc,vocabOfFormula] at *
State after:
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_P x ρ α = α ∧ repl_in_F x ρ φ0 = φ0

State before:
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_P x ρ α = α ∧ repl_in_F x ρ φ0 = φ0
Tactic:
constructor
State after:
case left
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_P x ρ α = α

case right
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_F x ρ φ0 = φ0

State before:
case left
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_P x ρ α = α
Tactic:
apply repl_in_P_non_occ_eq
State after:
case left.a
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ x ∉ voc α

State before:
case left.a
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ x ∉ voc α
Tactic:
tauto
State after:
no goals

State before:
case right
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_F x ρ φ0 = φ0
Tactic:
apply repl_in_F_non_occ_eq
State after:
case right.a
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ x ∉ voc φ0

State before:
case right.a
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ x ∉ voc φ0
Tactic:
tauto
State after:
no goals