Theory Substitution

subsection‹Substitutions›
theory Substitution
imports Formulas
begin

primrec subst where
"subst A F (Atom B) = (if A = B then F else Atom B)" |
"subst _ _ ⊥ = ⊥" |
"subst A F (G ❙∨ H) = (subst A F G ❙∨ subst A F H)" |
"subst A F (G ❙∧ H) = (subst A F G ❙∧ subst A F H)" |
"subst A F (G ❙→ H) = (subst A F G ❙→ subst A F H)" |
"subst A F (❙¬ H) = (❙¬ (subst A F H))"
term subst
abbreviation subst_syntax (‹(_[/(_/'//_)])› [70,70] 69) where
"A[B / C] ≡ subst C B A"

lemma no_subst[simp]: "k ∉ atoms F ⟹ F[G / k] = F" by(induction F; simp)
lemma subst_atoms: "k ∈ atoms F ⟹ atoms (F[G / k]) = atoms F - {k} ∪ atoms G" 
proof(induction F)
  case (And F G) thus ?case by(cases "k ∈ atoms F"; force) next
  case (Or F G) thus ?case by(cases "k ∈ atoms F"; force) next
  case (Imp F G) thus ?case by(cases "k ∈ atoms F"; force) next
qed simp_all

lemma subst_atoms_simp: "atoms (F[G / k]) = atoms F - {k} ∪ (if k ∈ atoms F then atoms G else {})"
  by(simp add: subst_atoms)

end