Theory Nonground_Entailment

theory Nonground_Entailment
  imports
    Nonground_Context
    Nonground_Clause
    Term_Rewrite_System
    Entailment_Lifting
    Fold_Extra
begin

section ‹Entailment›

context nonground_term
begin

lemma var_in_term:
  assumes "x ∈ vars t"
  obtains c where "t = c⟨Var x⟩"
  using assms
proof(induction t)
  case Var
  then show ?case
    by (meson supteq_Var supteq_ctxtE)
next
  case (Fun f args)
  then obtain t' where "t' ∈ set args " "x ∈ vars t'"
    by (metis term.distinct(1) term.sel(4) term.set_cases(2))

  moreover then obtain args1 args2 where
    "args1 @ [t'] @ args2 = args"
    by (metis append_Cons append_Nil split_list)

  moreover then have "(More f args1 □ args2)⟨t'⟩ = Fun f args"
    by simp

  ultimately show ?case
    using Fun(1)
    by (meson assms supteq_ctxtE that vars_term_supteq)
qed

lemma vars_term_ms_count:
  assumes "is_ground t"
  shows
    "size {#x' ∈# vars_term_ms c⟨Var x⟩. x' = x#} = Suc (size {#x' ∈# vars_term_ms c⟨t⟩. x' = x#})"
  by(induction c)(auto simp: assms filter_mset_empty_conv)

end

context nonground_clause
begin

lemma not_literal_entails [simp]:
  "¬ upair ` I ⊫l Neg a ⟷ upair ` I ⊫l Pos a"
  "¬ upair ` I ⊫l Pos a ⟷ upair ` I ⊫l Neg a"
  by auto

lemmas literal_entails_unfolds =
  not_literal_entails true_lit_simps

end

locale clause_entailment = nonground_clause +
  fixes I :: "('f gterm × 'f gterm) set"
  assumes
    trans: "trans I" and
    sym: "sym I" and
    compatible_with_gctxt: "compatible_with_gctxt I"
begin

lemma symmetric_context_congruence:
  assumes "(t, t') ∈ I"
  shows "(c⟨t⟩⇩G, t'') ∈ I ⟷ (c⟨t'⟩⇩G, t'') ∈ I"
  by (meson assms compatible_with_gctxt compatible_with_gctxtD sym trans symD transE)

lemma symmetric_upair_context_congruence:
  assumes "Upair t t' ∈ upair ` I"
  shows "Upair c⟨t⟩⇩G t'' ∈  upair ` I ⟷ Upair c⟨t'⟩⇩G t'' ∈  upair ` I"
  using assms uprod_mem_image_iff_prod_mem[OF sym] symmetric_context_congruence
  by simp

lemma upair_compatible_with_gctxtI [intro]:
  "Upair t t' ∈ upair ` I ⟹ Upair c⟨t⟩⇩G c⟨t'⟩⇩G ∈ upair ` I"
  using compatible_with_gctxt
  unfolding compatible_with_gctxt_def
  by (simp add: sym)

sublocale "term": symmetric_base_entailment where vars = "term.vars :: ('f, 'v) term ⇒ 'v set" and
  id_subst = Var and comp_subst = "(⊙)" and subst = "(⋅t)" and to_ground = term.to_ground and
  from_ground = term.from_ground
proof unfold_locales
  fix γ :: "('f, 'v) subst" and t t' update var

  assume
    update_is_ground: "term.is_ground update" and
    var_grounding: "term.is_ground (γ var)" and
    var_update: "(term.to_ground (γ var), term.to_ground update) ∈ I" and
    term_grounding: "term.is_ground (t ⋅t γ)" and
    updated_term: "(term.to_ground (t ⋅t γ(var := update)), t') ∈ I"

  from term_grounding updated_term
  show "(term.to_ground (t ⋅t γ), t') ∈ I"
  proof(induction "size (filter_mset (λvar'. var' = var) (vars_term_ms t))" arbitrary: t)
    case 0

    then have "var ∉ term.vars t"
      by (metis (mono_tags, lifting) filter_mset_empty_conv set_mset_vars_term_ms
          size_eq_0_iff_empty)

    then have "t ⋅t γ(var := update) = t ⋅t γ"
      using term.subst_reduntant_upd
      by (simp add: eval_with_fresh_var)

    with 0 show ?case
      by argo
  next
    case (Suc n)

    let ?context_to_ground = "map_args_actxt term.to_ground"

    have "var ∈ term.vars t"
      using Suc.hyps(2)
      by (metis (full_types) filter_mset_empty_conv nonempty_has_size set_mset_vars_term_ms
          zero_less_Suc)

    then obtain c where t [simp]: "t = c⟨Var var⟩"
      by (meson term.var_in_term)

    have [simp]:
      "(?context_to_ground (c ⋅t⇩c γ))⟨term.to_ground (γ var)⟩⇩G = term.to_ground (c⟨Var var⟩ ⋅t γ)"
      using Suc
      by(induction c) simp_all

    have context_update [simp]:
      "(?context_to_ground (c ⋅t⇩c γ))⟨term.to_ground update⟩⇩G = term.to_ground (c⟨update⟩ ⋅t γ)"
      using Suc update_is_ground
      by(induction c) auto

    have "n = size {#var' ∈# vars_term_ms c⟨update⟩. var' = var#}"
      using Suc term.vars_term_ms_count[OF update_is_ground, of var c]
      by auto

    moreover have "term.is_ground (c⟨update⟩ ⋅t γ)"
      using Suc.prems update_is_ground
      by auto

    moreover have "(term.to_ground (c⟨update⟩ ⋅t γ(var := update)), t') ∈ I"
      using Suc.prems update_is_ground
      by auto

    moreover have "(term.to_ground update, term.to_ground (γ var)) ∈ I"
      using var_update sym
      by (metis symD)

    moreover have "(term.to_ground (c⟨update⟩ ⋅t γ), t') ∈ I"
      using Suc calculation
      by blast

    ultimately have "((?context_to_ground (c ⋅t⇩c γ))⟨term.to_ground (γ var)⟩⇩G, t') ∈ I"
      using symmetric_context_congruence context_update
      by metis

    then show ?case
      by simp
  qed
qed (rule sym)

sublocale atom: symmetric_entailment
  where comp_subst = "(⊙)" and id_subst = Var
    and base_subst = "(⋅t)" and base_vars = term.vars and subst = "(⋅a)" and vars = atom.vars
    and base_to_ground = term.to_ground and base_from_ground = term.from_ground and I = I
    and entails_def = "λa. atom.to_ground a ∈ upair ` I"
proof unfold_locales
  fix a :: "('f, 'v) atom" and  γ var update P

  assume assms:
    "term.is_ground update"
    "term.is_ground (γ var)"
    "(term.to_ground (γ var), term.to_ground update) ∈ I"
    "atom.is_ground (a ⋅a γ)"
    "(atom.to_ground (a ⋅a γ(var := update)) ∈ upair ` I)"

  show "(atom.to_ground (a ⋅a γ) ∈ upair ` I)"
  proof(cases a)
    case (Upair t t')

    moreover have
      "(term.to_ground (t' ⋅t γ), term.to_ground (t ⋅t γ)) ∈ I ⟷
       (term.to_ground (t ⋅t γ), term.to_ground (t' ⋅t γ)) ∈ I"
      by (metis local.sym symD)

    ultimately show ?thesis
      using assms
      unfolding atom.to_ground_def atom.subst_def atom.vars_def
      by(auto simp: sym term.simultaneous_congruence)
  qed
qed (simp_all add: sym)

sublocale literal: entailment_lifting_conj
  where comp_subst = "(⊙)" and id_subst = Var
    and base_subst = "(⋅t)" and base_vars = term.vars and sub_subst = "(⋅a)" and sub_vars = atom.vars
    and base_to_ground = term.to_ground and base_from_ground = term.from_ground and I = I
    and sub_entails = atom.entails and map = "map_literal" and to_set = "set_literal"
    and is_negated = is_neg and entails_def = "λl. upair ` I ⊫l literal.to_ground l"
proof unfold_locales
  fix l :: "('f, 'v) atom literal"

  show "(upair ` I ⊫l literal.to_ground l) =
    (if is_neg l then Not else (λx. x))
      (Finite_Set.fold (∧) True ((λa. atom.to_ground a ∈ upair ` I) ` set_literal l))"
    unfolding literal.vars_def literal.to_ground_def
    by(cases l)(auto)

qed auto

sublocale clause: entailment_lifting_disj
  where comp_subst = "(⊙)" and id_subst = Var
    and base_subst = "(⋅t)" and base_vars = term.vars
    and base_to_ground = term.to_ground and base_from_ground = term.from_ground and I = I
    and sub_subst = "(⋅l)" and sub_vars = literal.vars and sub_entails = literal.entails
    and map = image_mset and to_set = set_mset and is_negated = "λ_. False"
    and entails_def = "λC. upair ` I ⊫ clause.to_ground C"
proof unfold_locales
  fix C :: "('f, 'v) atom clause"

  show "upair ` I ⊫ clause.to_ground C ⟷
    (if False then Not else (λx. x)) (Finite_Set.fold (∨) False (literal.entails ` set_mset C))"
    unfolding clause.to_ground_def
    by(induction C) auto

qed auto

lemma literal_compatible_with_gctxtI [intro]:
   "literal.entails (t ≈ t') ⟹ literal.entails (c⟨t⟩ ≈ c⟨t'⟩)"
  by (simp add: upair_compatible_with_gctxtI)

lemma symmetric_literal_context_congruence:
  assumes "Upair t t' ∈ upair ` I"
  shows
    "upair ` I ⊫l c⟨t⟩⇩G ≈ t'' ⟷ upair ` I ⊫l c⟨t'⟩⇩G ≈ t''"
    "upair ` I ⊫l c⟨t⟩⇩G !≈ t'' ⟷ upair ` I ⊫l c⟨t'⟩⇩G !≈ t''"
  using assms symmetric_upair_context_congruence
  by auto

end

end