Theory Prop_Logic_Multiset

theory Prop_Logic_Multiset
imports Nested_Multisets_Ordinals.Multiset_More Prop_Normalisation
  Entailment_Definition.Partial_Herbrand_Interpretation
begin

section ‹Link with Multiset Version›

subsection ‹Transformation to Multiset›

fun mset_of_conj :: "'a propo ⇒ 'a literal multiset" where
"mset_of_conj (FOr φ ψ) = mset_of_conj φ + mset_of_conj ψ" |
"mset_of_conj (FVar v) = {# Pos v #}" |
"mset_of_conj (FNot (FVar v)) = {# Neg v #}" |
"mset_of_conj FF = {#}"

fun mset_of_formula :: "'a propo ⇒ 'a literal multiset set" where
"mset_of_formula (FAnd φ ψ) = mset_of_formula φ ∪ mset_of_formula ψ" |
"mset_of_formula (FOr φ ψ) = {mset_of_conj (FOr φ ψ)}" |
"mset_of_formula (FVar ψ) = {mset_of_conj (FVar ψ)}" |
"mset_of_formula (FNot ψ) = {mset_of_conj (FNot ψ)}" |
"mset_of_formula FF = {{#}}" |
"mset_of_formula FT = {}"

subsection ‹Equisatisfiability of the two Versions›

lemma is_conj_with_TF_FNot:
  "is_conj_with_TF (FNot φ) ⟷ (∃v. φ = FVar v ∨ φ = FF ∨ φ = FT)"
  unfolding is_conj_with_TF_def apply (rule iffI)
  apply (induction "FNot φ" rule: super_grouped_by.induct)
  apply (induction "FNot φ" rule: grouped_by.induct)
     apply simp
    apply (cases φ; simp)
  apply auto
  done

lemma grouped_by_COr_FNot:
  "grouped_by COr (FNot φ) ⟷ (∃v. φ = FVar v ∨ φ = FF ∨ φ = FT)"
  unfolding is_conj_with_TF_def apply (rule iffI)
  apply (induction "FNot φ" rule: grouped_by.induct)
     apply simp
    apply (cases φ; simp)
  apply auto
  done

lemma
  shows no_T_F_FF[simp]: "¬no_T_F FF" and
    no_T_F_FT[simp]: "¬no_T_F FT"
  unfolding no_T_F_def all_subformula_st_def by auto

lemma grouped_by_CAnd_FAnd:
  "grouped_by CAnd (FAnd φ1 φ2) ⟷ grouped_by CAnd φ1 ∧ grouped_by CAnd φ2"
  apply (rule iffI)
  apply (induction "FAnd φ1 φ2" rule: grouped_by.induct)
  using connected_is_group[of CAnd φ1 φ2] by auto

lemma grouped_by_COr_FOr:
  "grouped_by COr (FOr φ1 φ2) ⟷ grouped_by COr φ1 ∧ grouped_by COr φ2"
  apply (rule iffI)
  apply (induction "FOr φ1 φ2" rule: grouped_by.induct)
  using connected_is_group[of COr φ1 φ2] by auto


lemma grouped_by_COr_FAnd[simp]: "¬ grouped_by COr (FAnd φ1 φ2)"
  apply clarify
   apply (induction "FAnd φ1 φ2" rule: grouped_by.induct)
   apply auto
  done

lemma grouped_by_COr_FEq[simp]: "¬ grouped_by COr (FEq φ1 φ2)"
  apply clarify
   apply (induction "FEq φ1 φ2" rule: grouped_by.induct)
   apply auto
  done

lemma [simp]: "¬grouped_by COr (FImp φ ψ)"
  apply clarify
  by (induction "FImp φ ψ" rule: grouped_by.induct) simp_all

lemma [simp]: "¬ is_conj_with_TF (FImp φ ψ)"
  unfolding is_conj_with_TF_def apply clarify
  by (induction "FImp φ ψ" rule: super_grouped_by.induct) simp_all

lemma [simp]: "¬ is_conj_with_TF (FEq φ ψ)"
  unfolding is_conj_with_TF_def apply clarify
  by (induction "FEq φ ψ" rule: super_grouped_by.induct) simp_all

lemma is_conj_with_TF_Fand:
  "is_conj_with_TF (FAnd φ1 φ2) ⟹ is_conj_with_TF φ1 ∧  is_conj_with_TF φ2"
  unfolding is_conj_with_TF_def
  apply (induction "FAnd φ1 φ2" rule: super_grouped_by.induct)
   apply (auto simp: grouped_by_CAnd_FAnd intro: grouped_is_super_grouped)[]
  apply auto[]
  done

lemma is_conj_with_TF_FOr:
  "is_conj_with_TF (FOr φ1 φ2) ⟹ grouped_by COr φ1 ∧ grouped_by COr φ2"
  unfolding is_conj_with_TF_def
  apply (induction "FOr φ1 φ2" rule: super_grouped_by.induct)
   apply (auto simp: grouped_by_COr_FOr)[]
  apply auto[]
  done

lemma grouped_by_COr_mset_of_formula:
  "grouped_by COr φ ⟹ mset_of_formula φ = (if φ = FT then {} else {mset_of_conj φ})"
  by (induction φ) (auto simp add: grouped_by_COr_FNot)

text ‹When a formula is in CNF form, then there is equisatisfiability between the multiset version
  and the CNF form. Remark that the definition for the entailment are slightly different:
  @{term eval} uses a function assigning @{term True} or @{term False}, while
  @{term Partial_Herbrand_Interpretation.true_clss} uses a set where being in the list means entailment of a
  literal.
  ›
theorem cnf_eval_true_clss:
  fixes φ :: "'v propo"
  assumes "is_cnf φ"
  shows "eval A φ ⟷ Partial_Herbrand_Interpretation.true_clss ({Pos v|v. A v} ∪ {Neg v|v. ¬A v})
    (mset_of_formula φ)"
  using assms
proof (induction φ)
  case FF
  then show ?case by auto
next
  case FT
  then show ?case by auto
next
  case (FVar v)
  then show ?case by auto
next
  case (FAnd φ ψ)
  then show ?case
    unfolding is_cnf_def by (auto simp: is_conj_with_TF_FNot dest: is_conj_with_TF_Fand
    dest!: is_conj_with_TF_FOr)
next
  case (FOr φ ψ)
  then have [simp]: "mset_of_formula φ = {mset_of_conj φ}" "mset_of_formula ψ = {mset_of_conj ψ}"
    unfolding is_cnf_def by (auto dest!:is_conj_with_TF_FOr simp: grouped_by_COr_mset_of_formula
      split: if_splits)
  have "is_conj_with_TF φ" "is_conj_with_TF ψ"
    using FOr(3) unfolding is_cnf_def no_T_F_def
    by (metis grouped_is_super_grouped is_conj_with_TF_FOr is_conj_with_TF_def)+
  then show ?case using FOr
    unfolding is_cnf_def by simp
next
  case (FImp φ ψ)
  then show ?case
    unfolding is_cnf_def by auto
next
  case (FEq φ ψ)
  then show ?case
    unfolding is_cnf_def by auto
next
  case (FNot φ)
  then show ?case
    unfolding is_cnf_def by (auto simp: is_conj_with_TF_FNot)
qed

function formula_of_mset :: "'a clause ⇒ 'a propo" where
  ‹formula_of_mset φ =
     (if φ = {#} then FF
      else
         let v = (SOME v. v ∈# φ);
             v' = (if is_pos v then FVar (atm_of v) else FNot (FVar (atm_of v))) in
         if remove1_mset v φ = {#} then v'
         else FOr v' (formula_of_mset (remove1_mset v φ)))›
  by auto
termination
  apply (relation ‹measure size›)
   apply (auto simp: size_mset_remove1_mset_le_iff)
  by (meson multiset_nonemptyE someI_ex)

lemma formula_of_mset_empty[simp]: ‹formula_of_mset {#} = FF›
  by (auto simp: Let_def)

lemma formula_of_mset_empty_iff[iff]: ‹formula_of_mset φ = FF ⟷ φ = {#}›
  by (induction φ) (auto simp: Let_def)

declare formula_of_mset.simps[simp del]

function formula_of_msets :: "'a literal multiset set ⇒ 'a propo" where
  ‹formula_of_msets φs =
     (if φs = {} ∨ infinite φs then FT
      else
         let v = (SOME v. v ∈ φs);
             v' = formula_of_mset v in
         if φs - {v} = {} then v'
         else FAnd v' (formula_of_msets (φs - {v})))›
  by auto
termination
  apply (relation ‹measure card›)
   apply (auto simp: some_in_eq)
  by (metis all_not_in_conv card_gt_0_iff diff_less lessI)

declare formula_of_msets.simps[simp del]

lemma remove1_mset_empty_iff:
  ‹remove1_mset v φ = {#} ⟷ (φ = {#} ∨ φ = {#v#})›
  using remove1_mset_eqE by force

definition fun_of_set where
  ‹fun_of_set A x = (if Pos x ∈ A then True else if Neg x ∈ A then False else undefined)›

lemma grouped_by_COr_formula_of_mset: ‹grouped_by COr (formula_of_mset φ)›
proof (induction ‹size φ› arbitrary: φ)
  case 0
  then show ?case by (subst formula_of_mset.simps) (auto simp: Let_def)
next
  case (Suc n) note IH = this(1) and s = this(2)
  then have ‹n = size (remove1_mset (SOME v. v ∈# φ) φ)› if ‹φ ≠ {#}›
    using that by (auto simp: size_Diff_singleton_if some_in_eq)
  then show ?case
    using IH[of ‹remove1_mset (SOME v. v ∈# φ) φ›]
    by(subst formula_of_mset.simps) (auto simp: Let_def grouped_by_COr_FOr)
qed
lemma no_T_F_formula_of_mset: ‹no_T_F (formula_of_mset φ)› if ‹formula_of_mset φ ≠ FF› for φ
  using that
proof (induction ‹size φ› arbitrary: φ)
  case 0
  then show ?case by (subst formula_of_mset.simps) (auto simp: Let_def no_T_F_def
        all_subformula_st_def)
next
  case (Suc n) note IH = this(1) and s = this(2) and FF = this(3)
  then have ‹n = size (remove1_mset (SOME v. v ∈# φ) φ)› if ‹φ ≠ {#}›
    using that by (auto simp: size_Diff_singleton_if some_in_eq)
  moreover have ‹no_T_F (FVar (atm_of (SOME v. v ∈# φ)))›
    by (auto simp: no_T_F_def)
  ultimately show ?case
    using IH[of ‹remove1_mset (SOME v. v ∈# φ) φ›] FF
    by(subst formula_of_mset.simps) (auto simp: Let_def grouped_by_COr_FOr)
qed

lemma mset_of_conj_formula_of_mset[simp]: ‹mset_of_conj(formula_of_mset φ) = φ› for φ
proof (induction ‹size φ› arbitrary: φ)
  case 0
  then show ?case by (subst formula_of_mset.simps) (auto simp: Let_def no_T_F_def
        all_subformula_st_def)
next
  case (Suc n) note IH = this(1) and s = this(2)
  then have ‹n = size (remove1_mset (SOME v. v ∈# φ) φ)› if ‹φ ≠ {#}›
    using that by (auto simp: size_Diff_singleton_if some_in_eq)
  moreover have ‹no_T_F (FVar (atm_of (SOME v. v ∈# φ)))›
    by (auto simp: no_T_F_def)
  ultimately show ?case
    using IH[of ‹remove1_mset (SOME v. v ∈# φ) φ›]
    by(subst formula_of_mset.simps) (auto simp: some_in_eq Let_def grouped_by_COr_FOr remove1_mset_empty_iff)
qed

lemma mset_of_formula_formula_of_mset [simp]: ‹mset_of_formula (formula_of_mset φ) = {φ}› for φ
proof (induction ‹size φ› arbitrary: φ)
  case 0
  then show ?case by (subst formula_of_mset.simps) (auto simp: Let_def no_T_F_def
        all_subformula_st_def)
next
  case (Suc n) note IH = this(1) and s = this(2)
  then have ‹n = size (remove1_mset (SOME v. v ∈# φ) φ)› if ‹φ ≠ {#}›
    using that by (auto simp: size_Diff_singleton_if some_in_eq)
  moreover have ‹no_T_F (FVar (atm_of (SOME v. v ∈# φ)))›
    by (auto simp: no_T_F_def)
  ultimately show ?case
    using IH[of ‹remove1_mset (SOME v. v ∈# φ) φ›]
    by(subst formula_of_mset.simps) (auto simp: some_in_eq Let_def grouped_by_COr_FOr remove1_mset_empty_iff)
qed

lemma formula_of_mset_is_cnf: ‹is_cnf (formula_of_mset φ)›
  by (auto simp: is_cnf_def is_conj_with_TF_def grouped_by_COr_formula_of_mset no_T_F_formula_of_mset
        intro!: grouped_is_super_grouped)

lemma eval_clss_iff:
  assumes ‹consistent_interp A› and ‹total_over_set A UNIV›
  shows ‹eval (fun_of_set A) (formula_of_mset φ) ⟷ Partial_Herbrand_Interpretation.true_clss A {φ}›
  apply (subst cnf_eval_true_clss[OF formula_of_mset_is_cnf])
  using assms
  apply (auto simp add: true_cls_def fun_of_set_def consistent_interp_def total_over_set_def)
  apply (case_tac L)
  by (fastforce simp add: true_cls_def fun_of_set_def consistent_interp_def total_over_set_def)+

lemma is_conj_with_TF_Fand_iff:
  "is_conj_with_TF (FAnd φ1 φ2) ⟷ is_conj_with_TF φ1 ∧ is_conj_with_TF φ2 "
  unfolding is_conj_with_TF_def by (subst super_grouped_by.simps) auto

lemma is_CNF_Fand:
  ‹is_cnf (FAnd φ ψ) ⟷ (is_cnf φ ∧ no_T_F φ) ∧ is_cnf ψ ∧ no_T_F ψ›
  by (auto simp: is_cnf_def is_conj_with_TF_Fand_iff)

lemma no_T_F_formula_of_mset_iff: ‹no_T_F (formula_of_mset φ) ⟷ φ ≠ {#}›
proof (induction ‹size φ› arbitrary: φ)
  case 0
  then show ?case by (subst formula_of_mset.simps) (auto simp: Let_def no_T_F_def
        all_subformula_st_def)
next
  case (Suc n) note IH = this(1) and s = this(2)
  then have ‹n = size (remove1_mset (SOME v. v ∈# φ) φ)› if ‹φ ≠ {#}›
    using that by (auto simp: size_Diff_singleton_if some_in_eq)
  moreover have ‹no_T_F (FVar (atm_of (SOME v. v ∈# φ)))›
    by (auto simp: no_T_F_def)
  ultimately show ?case
    using IH[of ‹remove1_mset (SOME v. v ∈# φ) φ›]
    by(subst formula_of_mset.simps) (auto simp: some_in_eq Let_def grouped_by_COr_FOr remove1_mset_empty_iff)
qed

lemma no_T_F_formula_of_msets:
  assumes ‹finite φ› and ‹{#} ∉ φ› and ‹φ ≠ {}›
  shows ‹no_T_F (formula_of_msets (φ))›
  using assms apply (induction ‹card φ› arbitrary: φ)
  subgoal by (subst formula_of_msets.simps) (auto simp: no_T_F_def all_subformula_st_def)[]
  subgoal
    apply (subst formula_of_msets.simps)
    apply (auto split:  simp: Let_def formula_of_mset_is_cnf is_CNF_Fand
        no_T_F_formula_of_mset_iff some_in_eq)
    apply (metis (mono_tags, lifting) some_eq_ex)
    done
  done

lemma is_cnf_formula_of_msets:
  assumes ‹finite φ› and ‹{#} ∉ φ›
  shows ‹is_cnf (formula_of_msets φ)›
  using assms apply (induction ‹card φ› arbitrary: φ)
  subgoal by (subst formula_of_msets.simps) (auto simp: is_cnf_def is_conj_with_TF_def)[]
  subgoal
    apply (subst formula_of_msets.simps)
    apply (auto split:  simp: Let_def formula_of_mset_is_cnf is_CNF_Fand
        no_T_F_formula_of_mset_iff some_in_eq intro: no_T_F_formula_of_msets)
    apply (metis (mono_tags, lifting) some_eq_ex)
    done
  done

lemma mset_of_formula_formula_of_msets:
  assumes ‹finite φ›
  shows ‹mset_of_formula (formula_of_msets φ) = φ›
  using assms apply (induction ‹card φ› arbitrary: φ)
  subgoal by (subst formula_of_msets.simps) (auto simp: is_cnf_def is_conj_with_TF_def)[]
  subgoal
    apply (subst formula_of_msets.simps)
    apply (auto split:  simp: Let_def formula_of_mset_is_cnf is_CNF_Fand
        no_T_F_formula_of_mset_iff some_in_eq intro: no_T_F_formula_of_msets)
    done
  done

lemma
  assumes ‹consistent_interp A› and ‹total_over_set A UNIV› and ‹finite φ› and ‹{#} ∉ φ›
  shows ‹eval (fun_of_set A) (formula_of_msets φ) ⟷ Partial_Herbrand_Interpretation.true_clss A φ›
  apply (subst cnf_eval_true_clss[OF is_cnf_formula_of_msets[OF assms(3-4)]])
  using assms(3) unfolding mset_of_formula_formula_of_msets[OF assms(3)]
  by (induction φ)
    (use eval_clss_iff[OF assms(1,2)] in ‹simp_all add: cnf_eval_true_clss formula_of_mset_is_cnf›)

end