# Theory Soundness

```section "Soundness"

theory Soundness imports Completeness begin

lemma permutation_validS: "mset fs = mset gs --> (validS fs = validS gs)"
using mset_eq_setD apply blast
done

lemma modelAssigns_vblcase: "phi ∈ modelAssigns M ⟹  x ∈ objects M ⟹ vblcase x phi ∈ modelAssigns M"
apply(erule_tac rangeE)
apply(case_tac xaa rule: vbl_casesE, auto)
done

lemma tmp: "(!x : A. P x | Q) ==> (! x : A. P x) | Q " by blast

lemma soundnessFAll: "!!Gamma.
[| u ~: freeVarsFL (FAll Pos A # Gamma);
validS (instanceF u A # Gamma) |]
==> validS (FAll Pos A # Gamma)"
apply (drule_tac x=M in spec, rule)
apply (rule tmp, rule)
apply(drule_tac x="% y. if y = u then x else phi y" in bspec)
apply(erule disjE)
apply (rule disjI1, simp)
apply(subgoal_tac "evalF M (vblcase x (λy. if y = u then x else phi y)) A = evalF M (vblcase x phi) A")
apply force
apply(rule evalF_equiv)
apply(rule equalOn_vblcaseI)
apply(rule,rule)
apply (rule equalOnI, force)
apply(rule disjI2)
apply(subgoal_tac "evalS M (λy. if y = u then x else phi y) Gamma = evalS M phi Gamma")
apply force
apply(rule evalS_equiv)
apply(rule equalOnI)
apply(force simp: freeVarsFL_cons)
done

lemma soundnessFEx: "validS (instanceF x A # Gamma) ==> validS (FAll Neg A # Gamma)"
apply (simp add: evalF_instance, rule, rule)
apply(drule_tac x=M in spec)
apply (drule_tac x=phi in bspec, assumption)
apply(erule disjE)
apply(rule disjI1)
apply (rule_tac x="phi x" in bexI, assumption)
apply(force dest: modelAssignsD subsetD)
apply (rule disjI2, assumption)
done

lemma soundnessFCut: "[| validS (C # Gamma); validS (FNot C # Delta) |] ==> validS (Gamma @ Delta)"
(*  apply(force simp: validS_def evalS_append evalS_cons evalF_FNot)*)
apply (simp add: validS_def, rule, rule)
apply(drule_tac x=M in spec)
apply(drule_tac x=M in spec)
apply(drule_tac x=phi in bspec) apply assumption
apply(drule_tac x=phi in bspec) apply assumption
apply (simp add: evalS_append evalF_FNot, blast)
done

lemma soundness: "fs : deductions(PC) ==> (validS fs)"
apply(erule_tac deductions.induct)
apply(drule_tac PowD)
apply(subgoal_tac "prems ⊆  {x. validS x}") prefer 2 apply force apply(thin_tac "prems ⊆ deductions PC ∩ {x. validS x}")
apply(elim disjE)
apply (subst permutation_validS)
defer
apply assumption
apply simp_all
apply(force simp: Axioms_def validS_def evalS_def)
apply(force simp: Conjs_def validS_def evalS_def)
apply(force simp: Disjs_def validS_def evalS_def)
apply(force intro: soundnessFAll)
apply(force intro: soundnessFEx)
apply(force simp: Weaks_def validS_def evalS_def)
apply(force simp: Contrs_def validS_def evalS_def)
apply(force simp: Cuts_def intro: soundnessFCut)
done

lemma completeness: "fs : deductions (PC) = validS fs"
apply rule
apply(rule soundness) apply assumption
apply(subgoal_tac "fs : deductions CutFreePC")
apply(rule subsetD) prefer 2 apply assumption
apply(rule mono_deductions)
apply(simp add: PC_def CutFreePC_def) apply blast