Theory Usemantics

section ‹Bounded semantics›

theory Usemantics imports SeCaV begin

text ‹In this theory, we define an alternative semantics for SeCaV formulas where the quantifiers
  are bounded to terms in a specific set.
  This is needed to construct a countermodel from a Hintikka set.›

text ‹This function defines the semantics, which are bounded by the set ‹u›.›
primrec usemantics where
  ‹usemantics u e f g (Pre i l) = g i (semantics_list e f l)›
| ‹usemantics u e f g (Imp p q) = (usemantics u e f g p ⟶ usemantics u e f g q)›
| ‹usemantics u e f g (Dis p q) = (usemantics u e f g p ∨ usemantics u e f g q)›
| ‹usemantics u e f g (Con p q) = (usemantics u e f g p ∧ usemantics u e f g q)›
| ‹usemantics u e f g (Exi p) = (∃x ∈ u. usemantics u (SeCaV.shift e 0 x) f g p)›
| ‹usemantics u e f g (Uni p) = (∀x ∈ u. usemantics u (SeCaV.shift e 0 x) f g p)›
| ‹usemantics u e f g (Neg p) = (¬ usemantics u e f g p)›

text ‹An environment is well-formed if the variables are actually in the quantifier set ‹u›.›
definition is_env :: ‹'a set ⇒ (nat ⇒ 'a) ⇒ bool› where
  ‹is_env u e ≡ ∀n. e n ∈ u›

text ‹A function interpretation is well-formed if it is closed in the quantifier set ‹u›.›
definition is_fdenot :: ‹'a set ⇒ (nat ⇒ 'a list ⇒ 'a) ⇒ bool› where
  ‹is_fdenot u f ≡ ∀i l. list_all (λx. x ∈ u) l ⟶ f i l ∈ u›

text ‹If we choose to quantify over the universal set, we obtain the usual semantics›
lemma usemantics_UNIV: ‹usemantics UNIV e f g p ⟷ semantics e f g p›
  by (induct p arbitrary: e) auto

text ‹If a function name ‹n› is not in a formula, it does not matter whether it is in
  the function interpretation or not.›
lemma uupd_lemma [iff]: ‹n ∉ params p ⟹ usemantics u e (f(n := x)) g p ⟷ usemantics u e f g p›
  by (induct p arbitrary: e) simp_all

text ‹The semantics of substituting variable i by term t in formula a are well-defined›
lemma usubst_lemma [iff]:
  ‹usemantics u e f g (subst a t i) ⟷ usemantics u (SeCaV.shift e i (semantics_term e f t)) f g a›
  by (induct a arbitrary: e i t) simp_all

subsubsection ‹Soundness of SeCaV with regards to the bounded semantics›
text ‹We would like to prove that the SeCaV proof system is sound under the bounded semantics.›

text ‹If the environment and the function interpretation are well-formed, the semantics of terms
  are in the quantifier set ‹u›.›
lemma usemantics_term [simp]:
  assumes ‹is_env u e› ‹is_fdenot u f›
  shows ‹semantics_term e f t ∈ u› ‹list_all (λx. x ∈ u) (semantics_list e f ts)›
  using assms by (induct t and ts rule: semantics_term.induct semantics_list.induct)
    (simp_all add: is_env_def is_fdenot_def)

text ‹If a function interpretation is well-formed, replacing the value by one in the quantifier set
  results in a well-formed function interpretation.›
lemma is_fdenot_shift [simp]: ‹is_fdenot u f ⟹ x ∈ u ⟹ is_fdenot u (f(i := λ_. x))›
  unfolding is_fdenot_def SeCaV.shift_def by simp

text ‹If a sequent is provable in the SeCaV proof system and the environment
  and function interpretation are well-formed, the sequent is valid under the bounded semantics.›
theorem sound_usemantics:
  assumes ‹⊩ z› and ‹is_env u e› and ‹is_fdenot u f›
  shows ‹∃p ∈ set z. usemantics u e f g p›
  using assms
proof (induct arbitrary: f rule: sequent_calculus.induct)
  case (10 i p z)
  then show ?case
  proof (cases ‹∀x ∈ u. usemantics u e (f(i := λ_. x)) g (sub 0 (Fun i []) p)›)
    case False
    moreover have ‹∀x ∈ u. ∃p ∈ set (sub 0 (Fun i []) p # z). usemantics u e (f(i := λ_. x)) g p›
      using 10 is_fdenot_shift by metis
    ultimately have ‹∃x ∈ u. ∃p ∈ set z. usemantics u e (f(i := λ_. x)) g p›
      by fastforce
    moreover have ‹list_all (λp. i ∉ params p) z›
      using 10 by simp
    ultimately show ?thesis
      using 10 Ball_set insert_iff list.set(2) uupd_lemma by metis
  qed simp
next
  case (11 i p z)
  then show ?case
  proof (cases ‹∀x ∈ u. usemantics u e (f(i := λ_. x)) g (Neg (sub 0 (Fun i []) p))›)
    case False
    moreover have
      ‹∀x ∈ u. ∃p ∈ set (Neg (sub 0 (Fun i []) p) # z). usemantics u e (f(i := λ_. x)) g p›
      using 11 is_fdenot_shift by metis
    ultimately have ‹∃x ∈ u. ∃p ∈ set z. usemantics u e (f(i := λ_. x)) g p›
      by fastforce
    moreover have ‹list_all (λp. i ∉ params p) z›
      using 11 by simp
    ultimately show ?thesis
      using 11 Ball_set insert_iff list.set(2) uupd_lemma by metis
  qed simp
qed fastforce+

end