Theory Countermodel

section ‹Countermodels from Hintikka sets›

theory Countermodel
  imports Hintikka Usemantics ProverLemmas
begin

text ‹In this theory, we will construct a countermodel in the bounded semantics from a Hintikka
  set. This will allow us to prove completeness of the prover.›

text ‹A predicate is satisfied in the model based on a set of formulas S when its negation is in S.›
abbreviation (input)
  ‹G S n ts ≡ Neg (Pre n ts) ∈ S›

text ‹Alternate interpretation for environments: if a variable is not present, we interpret it as
  some existing term.›
abbreviation
  ‹E S n ≡ if Var n ∈ terms S then Var n else SOME t. t ∈ terms S›

text ‹Alternate interpretation for functions: if a function application is not present, we interpret
  it as some existing term.›
abbreviation
  ‹F S i l ≡ if Fun i l ∈ terms S then Fun i l else SOME t. t ∈ terms S›

text ‹The terms function never returns the empty set (because it will add ‹Fun 0 []› if that is the
  case).›
lemma terms_ne [simp]: ‹terms S ≠ {}›
  unfolding terms_def by simp

text ‹If a term is in the set of terms, it is either the default term or a subterm of some formula
  in the set.›
lemma terms_cases: ‹t ∈ terms S ⟹ t = Fun 0 [] ∨ (∃p ∈ S. t ∈ set (subtermFm p))›
  unfolding terms_def by (simp split: if_splits)

text ‹The set of terms is downwards closed under the subterm function.›
lemma terms_downwards_closed: ‹t ∈ terms S ⟹ set (subtermTm t) ⊆ terms S›
proof (induct t)
  case (Fun n ts)
  moreover have ‹∀t ∈ set ts. t ∈ set ts›
    by simp
  moreover have ‹∀t ∈ set ts. t ∈ terms S›
  proof
    fix t
    assume *: ‹t ∈ set ts›
    then show ‹t ∈ terms S›
    proof (cases ‹terms S = {Fun 0 []}›)
      case True
      then show ?thesis
        using Fun * by simp
    next
      case False
      moreover obtain p where p: ‹p ∈ S› ‹Fun n ts ∈ set (subtermFm p)›
        using Fun(2) terms_cases * by fastforce
      then have ‹set ts ⊆ set (subtermFm p)›
        using fun_arguments_subterm by blast
      ultimately show ‹t ∈ terms S›
        unfolding terms_def using * p(1) by (metis UN_iff in_mono)
    qed
  qed
  ultimately have ‹∀t ∈ set ts. set (subtermTm t) ⊆ terms S›
    using Fun by meson
  moreover note ‹Fun n ts ∈ terms S›
  ultimately show ?case
    by auto
next
  case (Var x)
  then show ?case
    by simp
qed

text ‹If terms are actually in a set of formulas, interpreting the environment over these formulas
allows for a Herbrand interpretation.›
lemma usemantics_E:
    ‹t ∈ terms S ⟹ semantics_term (E S) (F S) t = t›
    ‹list_all (λt. t ∈ terms S) ts ⟹ semantics_list (E S) (F S) ts = ts›
proof (induct t and ts arbitrary: ts rule: semantics_term.induct semantics_list.induct)
  case (Fun i ts')
  moreover have ‹∀t' ∈ set ts'. t' ∈ set (subtermTm (Fun i ts'))›
    using subterm_Fun_refl by blast
  ultimately have ‹list_all (λt. t ∈ terms S) ts'›
    using terms_downwards_closed unfolding list_all_def by (metis (no_types, lifting) subsetD)
  then show ?case
    using Fun by simp
qed simp_all

text ‹Our alternate interpretation of environments is well-formed for the terms function.›
lemma is_env_E:
  ‹is_env (terms S) (E S)›
  unfolding is_env_def
proof
  fix n
  show ‹E S n ∈ terms S›
    by (cases ‹Var n ∈ terms S›) (simp_all add: some_in_eq)
qed

text ‹Our alternate function interpretation is well-formed for the terms function.›
lemma is_fdenot_F:
  ‹is_fdenot (terms S) (F S)›
  unfolding is_fdenot_def
proof (intro allI impI)
  fix i l
  assume ‹list_all (λx. x ∈ terms S) l›
  then show ‹F S i l ∈ terms S›
    by (cases ‹∀n. Var n ∈ terms S›) (simp_all add: some_in_eq)
qed

abbreviation
  ‹M S ≡ usemantics (terms S) (E S) (F S) (G S)›

text ‹If S is a Hintikka set, then we can construct a countermodel for any formula using our
  bounded semantics and a Herbrand interpretation.›
theorem Hintikka_counter_model:
  assumes ‹Hintikka S›
  shows ‹(p ∈ S ⟶ ¬ M S p) ∧ (Neg p ∈ S ⟶ M S p)›
proof (induct p rule: wf_induct [where r=‹measure size›])
  case 1
  then show ?case ..
next
  fix x
  assume wf: ‹∀q. (q, x) ∈ measure size ⟶
    (q ∈ S ⟶ ¬ M S q) ∧ (Neg q ∈ S ⟶ M S q)›
  show ‹(x ∈ S ⟶ ¬ M S x) ∧ (Neg x ∈ S ⟶ M S x)›
  proof (cases x)
    case (Pre n ts)
    show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ S›
      then have ‹Neg (Pre n ts) ∉ S›
        using assms Pre Hintikka.Basic by blast
      moreover have ‹list_all (λt. t ∈ terms S) ts›
        using ‹x ∈ S› Pre subterm_Pre_refl unfolding terms_def list_all_def by force
      ultimately show ‹¬ M S x›
        using Pre usemantics_E
        by (metis (no_types, lifting) usemantics.simps(1))
    next
      assume ‹Neg x ∈ S›
      then have ‹G S n ts›
        using assms Pre Hintikka.Basic by blast
      moreover have ‹list_all (λt. t ∈ terms S) ts›
        using ‹Neg x ∈ S› Pre subterm_Pre_refl unfolding terms_def list_all_def by force
      ultimately show ‹M S x›
        using Pre usemantics_E
        by (metis (no_types, lifting) usemantics.simps(1))
    qed
  next
    case (Imp p q)
    show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ S›
      then have ‹Neg p ∈ S› ‹q ∈ S›
        using Imp assms Hintikka.AlphaImp by blast+
      then show ‹¬ M S x›
        using wf Imp by fastforce
    next
      assume ‹Neg x ∈ S›
      then have ‹p ∈ S ∨ Neg q ∈ S›
        using Imp assms Hintikka.BetaImp by blast
      then show ‹M S x›
        using wf Imp by fastforce
    qed
  next
    case (Dis p q)
    show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ S›
      then have ‹p ∈ S› ‹q ∈ S›
        using Dis assms Hintikka.AlphaDis by blast+
      then show ‹¬ M S x›
        using wf Dis by fastforce
    next
      assume ‹Neg x ∈ S›
      then have ‹Neg p ∈ S ∨ Neg q ∈ S›
        using Dis assms Hintikka.BetaDis by blast
      then show ‹M S x›
        using wf Dis by fastforce
    qed
  next
    case (Con p q)
    show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ S›
      then have ‹p ∈ S ∨ q ∈ S›
        using Con assms Hintikka.BetaCon by blast
      then show ‹¬ M S x›
        using wf Con by fastforce
    next
      assume ‹Neg x ∈ S›
      then have ‹Neg p ∈ S› ‹Neg q ∈ S›
        using Con assms Hintikka.AlphaCon by blast+
      then show ‹M S x›
        using wf Con by fastforce
    qed
  next
    case (Exi p)
    show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ S›
      then have ‹∀t ∈ terms S. sub 0 t p ∈ S›
        using Exi assms Hintikka.GammaExi by blast
      then have ‹∀t ∈ terms S. ¬ M S (sub 0 t p)›
        using wf Exi size_sub
        by (metis (no_types, lifting) add.right_neutral add_Suc_right fm.size(12) in_measure lessI)
      moreover have ‹∀t ∈ terms S. semantics_term (E S) (F S) t = t›
        using usemantics_E(1) terms_downwards_closed unfolding list_all_def by blast
      ultimately have ‹∀t ∈ terms S. ¬ usemantics (terms S) (SeCaV.shift (E S) 0 t) (F S) (G S) p›
        by simp
      then show ‹¬ M S x›
        using Exi by simp
    next
      assume ‹Neg x ∈ S›
      then obtain t where ‹t ∈ terms S› ‹Neg (sub 0 t p) ∈ S›
        using Exi assms Hintikka.DeltaExi by metis
      then have ‹M S (sub 0 t p)›
        using wf Exi size_sub
        by (metis (no_types, lifting) add.right_neutral add_Suc_right fm.size(12) in_measure lessI)
      moreover have ‹semantics_term (E S) (F S) t = t›
        using ‹t ∈ terms S› usemantics_E(1) terms_downwards_closed unfolding list_all_def by blast
      ultimately show ‹M S x›
        using Exi ‹t ∈ terms S› by auto
    qed
  next
    case (Uni p)
    show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ S›
      then obtain t where ‹t ∈ terms S› ‹sub 0 t p ∈ S›
        using Uni assms Hintikka.DeltaUni by metis
      then have ‹¬ M S (sub 0 t p)›
        using wf Uni size_sub
        by (metis (no_types, lifting) add.right_neutral add_Suc_right fm.size(13) in_measure lessI)
      moreover have ‹semantics_term (E S) (F S) t = t›
        using ‹t ∈ terms S› usemantics_E(1) terms_downwards_closed unfolding list_all_def by blast
      ultimately show ‹¬ M S x›
        using Uni ‹t ∈ terms S› by auto
    next
      assume ‹Neg x ∈ S›
      then have ‹∀t ∈ terms S. Neg (sub 0 t p) ∈ S›
        using Uni assms Hintikka.GammaUni by blast
      then have ‹∀t ∈ terms S. M S (sub 0 t p)›
        using wf Uni size_sub
        by (metis (no_types, lifting) Nat.add_0_right add_Suc_right fm.size(13) in_measure lessI)
      moreover have ‹∀t ∈ terms S. semantics_term (E S) (F S) t = t›
        using usemantics_E(1) terms_downwards_closed unfolding list_all_def by blast
      ultimately have ‹∀t ∈ terms S. ¬ usemantics (terms S) (SeCaV.shift (E S) 0 t) (F S) (G S) (Neg p)›
        by simp
      then show ‹M S x›
        using Uni by simp
    qed
  next
    case (Neg p)
    show ?thesis
    proof (intro conjI impI)
      assume ‹x ∈ S›
      then show ‹¬ M S x›
        using wf Neg by fastforce
    next
      assume ‹Neg x ∈ S›
      then have ‹p ∈ S›
        using Neg assms Hintikka.Neg by blast
      then show ‹M S x›
        using wf Neg by fastforce
    qed
  qed
qed

end