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