Theory ND_Sound

theory ND_Sound
imports ND Sema
begin

lemma BigAndImp: "A ⊨ (❙⋀P ❙→ G) ⟷ ((∀F ∈ set P. A ⊨ F) ⟶ A ⊨ G)"
  by(induction P; simp add: entailment_def)

lemma ND_sound: "Γ ⊢ F ⟹ Γ ⊫ F"
  by(induction rule: ND.induct; simp add: entailment_def; blast)
(* yeah, Isabelle's facilities are very good with this kind of problem… maybe we should show one or the other case. *)

end