Theory Executable_Subsumption

(*  Title:       An Executable Algorithm for Clause Subsumption
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2017
    Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
*)

section ‹An Executable Algorithm for Clause Subsumption›

text ‹
This theory provides an executable functional implementation of clause
subsumption, building on the \textsf{IsaFoR} library.
›

theory Executable_Subsumption
  imports
    IsaFoR_Term
    First_Order_Terms.Matching
begin


subsection ‹Naive Implementation of Clause Subsumption›

fun subsumes_list where
  "subsumes_list [] Ks σ = True"
| "subsumes_list (L # Ls) Ks σ =
     (∃K ∈ set Ks. is_pos K = is_pos L ∧
       (case match_term_list [(atm_of L, atm_of K)] σ of
         None ⇒ False
       | Some ρ ⇒ subsumes_list Ls (remove1 K Ks) ρ))"

lemma atm_of_map_literal[simp]: "atm_of (map_literal f l) = f (atm_of l)"
  by (cases l; simp)

definition "extends_subst σ τ = (∀x ∈ dom σ. σ x = τ x)"

lemma extends_subst_refl[simp]: "extends_subst σ σ"
  unfolding extends_subst_def by auto

lemma extends_subst_trans: "extends_subst σ τ ⟹ extends_subst τ ρ ⟹ extends_subst σ ρ"
  unfolding extends_subst_def dom_def by (metis mem_Collect_eq)

lemma extends_subst_dom: "extends_subst σ τ ⟹ dom σ ⊆ dom τ"
  unfolding extends_subst_def dom_def by auto

lemma extends_subst_extends: "extends_subst σ τ ⟹ x ∈ dom σ ⟹ τ x = σ x"
  unfolding extends_subst_def dom_def by auto

lemma extends_subst_fun_upd_new:
  "σ x = None ⟹ extends_subst (σ(x ↦ t)) τ ⟷ extends_subst σ τ ∧ τ x = Some t"
  unfolding extends_subst_def dom_fun_upd subst_of_map_def
  by (force simp add: dom_def split: option.splits)

lemma extends_subst_fun_upd_matching:
  "σ x = Some t ⟹ extends_subst (σ(x ↦ t)) τ ⟷ extends_subst σ τ"
  unfolding extends_subst_def dom_fun_upd subst_of_map_def
  by (auto simp add: dom_def split: option.splits)

lemma extends_subst_empty[simp]: "extends_subst Map.empty τ"
  unfolding extends_subst_def by auto

lemma extends_subst_cong_term:
  "extends_subst σ τ ⟹ vars_term t ⊆ dom σ ⟹ t ⋅ subst_of_map Var σ = t ⋅ subst_of_map Var τ"
  by (force simp: extends_subst_def subst_of_map_def split: option.splits intro!: term_subst_eq)

lemma extends_subst_cong_lit:
  "extends_subst σ τ ⟹ vars_lit L ⊆ dom σ ⟹ L ⋅lit subst_of_map Var σ = L ⋅lit subst_of_map Var τ"
  by (cases L) (auto simp: extends_subst_cong_term)

definition "subsumes_modulo C D σ =
   (∃τ. dom τ = vars_clause C ∪ dom σ ∧ extends_subst σ τ ∧ subst_cls C (subst_of_map Var τ) ⊆# D)"

abbreviation subsumes_list_modulo where
  "subsumes_list_modulo Ls Ks σ ≡ subsumes_modulo (mset Ls) (mset Ks) σ"

lemma vars_clause_add_mset[simp]: "vars_clause (add_mset L C) = vars_lit L ∪ vars_clause C"
  unfolding vars_clause_def by auto

lemma subsumes_list_modulo_Cons: "subsumes_list_modulo (L # Ls) Ks σ ⟷
  (∃K ∈ set Ks. ∃τ. extends_subst σ τ ∧ dom τ = vars_lit L ∪ dom σ ∧ L ⋅lit (subst_of_map Var τ) = K
     ∧ subsumes_list_modulo Ls (remove1 K Ks) τ)"
  unfolding subsumes_modulo_def
proof (safe, goal_cases left_right right_left)
  case (left_right τ)
  then show ?case
    by (intro bexI[of _ "L ⋅lit subst_of_map Var τ"]
      exI[of _ "λx. if x ∈ vars_lit L ∪ dom σ then τ x else None"], intro conjI exI[of _ τ])
      (auto 0 3 simp: extends_subst_def dom_def split: if_splits
      simp: insert_subset_eq_iff subst_lit_def  intro!: extends_subst_cong_lit)
next
  case (right_left K τ τ')
  then show ?case
    by (intro bexI[of _ "L ⋅lit subst_of_map Var τ"] exI[of _ τ'], intro conjI exI[of _ τ])
     (auto simp: insert_subset_eq_iff subst_lit_def extends_subst_cong_lit
       intro: extends_subst_trans)
qed

lemma decompose_Some_var_terms: "decompose (Fun f ss) (Fun g ts) = Some eqs ⟹
   f = g ∧ length ss = length ts ∧ eqs = zip ss ts ∧
   (⋃(t, u)∈set ((Fun f ss, Fun g ts) # P). vars_term t) =
   (⋃(t, u)∈set (eqs @ P). vars_term t)"
  by (drule decompose_Some)
    (fastforce simp: in_set_zip in_set_conv_nth Bex_def image_iff)

lemma match_term_list_sound: "match_term_list tus σ = Some τ ⟹
  extends_subst σ τ ∧ dom τ = (⋃(t, u)∈set tus. vars_term t) ∪ dom σ ∧
  (∀(t,u)∈set tus. t ⋅ subst_of_map Var τ = u)"
proof (induct tus σ rule: match_term_list.induct)
  case (2 x t P σ)
  then show ?case
    by (auto 0 3 simp: extends_subst_fun_upd_new extends_subst_fun_upd_matching
      subst_of_map_def dest: extends_subst_extends simp del: fun_upd_apply
      split: if_splits option.splits)
next
  case (3 f ss g ts P σ)
  from 3(2) obtain eqs where "decompose (Fun f ss) (Fun g ts) = Some eqs"
    "match_term_list (eqs @ P) σ = Some τ" by (auto split: option.splits)
  with 3(1)[OF this] show ?case
  proof (elim decompose_Some_var_terms[where P = P, elim_format] conjE, intro conjI, goal_cases extend dom subst)
    case subst
    from subst(3,5,6,7) show ?case
      by (auto 0 6 simp: in_set_conv_nth list_eq_iff_nth_eq Ball_def)
  qed auto
qed auto

lemma match_term_list_complete: "match_term_list tus σ = None ⟹
   extends_subst σ τ ⟹ dom τ = (⋃(t, u)∈set tus. vars_term t) ∪ dom σ ⟹
    (∃(t,u)∈set tus. t ⋅ subst_of_map Var τ ≠ u)"
proof (induct tus σ arbitrary: τ rule: match_term_list.induct)
  case (2 x t P σ)
  then show ?case
    by (auto simp: extends_subst_fun_upd_new extends_subst_fun_upd_matching
      subst_of_map_def dest: extends_subst_extends simp del: fun_upd_apply
      split: if_splits option.splits)
next
  case (3 f ss g ts P σ)
  show ?case
  proof (cases "decompose (Fun f ss) (Fun g ts) = None")
    case False
    with 3(2) obtain eqs where "decompose (Fun f ss) (Fun g ts) = Some eqs"
      "match_term_list (eqs @ P) σ = None" by (auto split: option.splits)
    with 3(1)[OF this 3(3) trans[OF 3(4) arg_cong[of _ _ "λx. x ∪ dom σ"]]] show ?thesis
    proof (elim decompose_Some_var_terms[where P = P, elim_format] conjE, goal_cases subst)
      case subst
      from subst(1)[OF subst(6)] subst(4,5) show ?case
        by (auto 0 3 simp: in_set_conv_nth list_eq_iff_nth_eq Ball_def)
    qed
  qed auto
qed auto

lemma unique_extends_subst:
  assumes extends: "extends_subst σ τ" "extends_subst σ ρ" and
    dom: "dom τ = vars_term t ∪ dom σ" "dom ρ = vars_term t ∪ dom σ" and
    eq: "t ⋅ subst_of_map Var ρ = t ⋅ subst_of_map Var τ"
  shows "ρ = τ"
proof
  fix x
  consider (a) "x ∈ dom σ" | (b) "x ∈ vars_term t" | (c) "x ∉ dom τ" using assms by auto
  then show "ρ x = τ x"
  proof cases
    case a
    then show ?thesis using extends unfolding extends_subst_def by auto
  next
    case b
    with eq show ?thesis
    proof (induct t)
      case (Var x)
      with trans[OF dom(1) dom(2)[symmetric]] show ?case
        by (auto simp: subst_of_map_def split: option.splits)
    qed auto
  next
    case c
    then have "ρ x = None" "τ x = None" using dom by auto
    then show ?thesis by simp
  qed
qed

lemma subsumes_list_alt:
  "subsumes_list Ls Ks σ ⟷ subsumes_list_modulo Ls Ks σ"
proof (induction Ls Ks σ rule: subsumes_list.induct[case_names Nil Cons])
  case (Cons L Ls Ks σ)
  show ?case
    unfolding subsumes_list_modulo_Cons subsumes_list.simps
  proof ((intro bex_cong[OF refl] ext iffI; elim exE conjE), goal_cases LR RL)
    case (LR K)
    show ?case
      by (insert LR; cases K; cases L; auto simp: Cons.IH split: option.splits dest!: match_term_list_sound)
  next
    case (RL K τ)
    then show ?case
    proof (cases "match_term_list [(atm_of L, atm_of K)] σ")
      case None
      with RL show ?thesis
        by (auto simp: Cons.IH dest!: match_term_list_complete)
    next
      case (Some τ')
      with RL show ?thesis
        using unique_extends_subst[of σ τ τ' "atm_of L"]
        by (auto simp: Cons.IH dest!: match_term_list_sound)
    qed
  qed
qed (auto simp: subsumes_modulo_def subst_cls_def vars_clause_def intro: extends_subst_refl)

lemma subsumes_subsumes_list[code_unfold]:
  "subsumes (mset Ls) (mset Ks) = subsumes_list Ls Ks Map.empty"
unfolding subsumes_list_alt[of Ls Ks Map.empty]
proof
  assume "subsumes (mset Ls) (mset Ks)"
  then obtain σ where "subst_cls (mset Ls) σ ⊆# mset Ks" unfolding subsumes_def by blast
  moreover define τ where "τ = (λx. if x ∈ vars_clause (mset Ls) then Some (σ x) else None)"
  ultimately show "subsumes_list_modulo Ls Ks Map.empty"
    unfolding subsumes_modulo_def
    by (subst (asm) same_on_vars_clause[of _ σ "subst_of_map Var τ"])
      (auto intro!: exI[of _ τ] simp: subst_of_map_def[abs_def] split: if_splits)
qed (auto simp: subsumes_modulo_def subst_lit_def subsumes_def)

lemma strictly_subsumes_subsumes_list[code_unfold]:
  "strictly_subsumes (mset Ls) (mset Ks) =
    (subsumes_list Ls Ks Map.empty ∧ ¬ subsumes_list Ks Ls Map.empty)"
  unfolding strictly_subsumes_def subsumes_subsumes_list by simp

lemma subsumes_list_filterD: "subsumes_list Ls (filter P Ks) σ ⟹ subsumes_list Ls Ks σ"
proof (induction Ls arbitrary: Ks σ)
  case (Cons L Ls)
  from Cons.prems show ?case
    by (auto dest!: Cons.IH simp: filter_remove1[symmetric] split: option.splits)
qed simp

lemma subsumes_list_filterI:
  assumes match: "(⋀L K σ τ. L ∈ set Ls ⟹
    match_term_list [(atm_of L, atm_of K)] σ = Some τ ⟹ is_pos L = is_pos K ⟹ P K)"
  shows "subsumes_list Ls Ks σ ⟹ subsumes_list Ls (filter P Ks) σ"
using assms proof (induction Ls Ks σ rule: subsumes_list.induct[case_names Nil Cons])
  case (Cons L Ls Ks σ)
  from Cons.prems show ?case
    unfolding subsumes_list.simps set_filter bex_simps conj_assoc
    by (elim bexE conjE)
      (rule exI, rule conjI, assumption,
        auto split: option.splits simp: filter_remove1[symmetric] intro!: Cons.IH)
qed simp

lemma subsumes_list_Cons_filter_iff:
  assumes sorted_wrt: "sorted_wrt leq (L # Ls)" and trans: "transp leq"
  and match: "(⋀L K σ τ.
    match_term_list [(atm_of L, atm_of K)] σ = Some τ ⟹ is_pos L = is_pos K ⟹ leq L K)"
shows "subsumes_list (L # Ls) (filter (leq L) Ks) σ ⟷ subsumes_list (L # Ls) Ks σ"
  apply (rule iffI[OF subsumes_list_filterD subsumes_list_filterI]; assumption?)
  unfolding list.set insert_iff
  apply (elim disjE)
  subgoal by (auto split: option.splits elim!: match)
  subgoal for L K σ τ
    using sorted_wrt unfolding List.sorted_wrt.simps(2)
    apply (elim conjE)
    apply (drule bspec, assumption)
    apply (erule transpD[OF trans])
    apply (erule match)
    by auto
  done

definition leq_head  :: "('f::linorder, 'v) term ⇒ ('f, 'v) term ⇒ bool" where
  "leq_head t u = (case (root t, root u) of
    (None, _) ⇒ True
  | (_, None) ⇒ False
  | (Some f, Some g) ⇒ f ≤ g)"
definition "leq_lit L K = (case (K, L) of
    (Neg _, Pos _) ⇒ True
  | (Pos _, Neg _) ⇒ False
  | _ ⇒ leq_head (atm_of L) (atm_of K))"

lemma transp_leq_lit[simp]: "transp leq_lit"
  unfolding transp_def leq_lit_def leq_head_def by (force split: option.splits literal.splits)

lemma reflp_leq_lit[simp]: "reflp_on A leq_lit"
  unfolding reflp_on_def leq_lit_def leq_head_def by (auto split: option.splits literal.splits)

lemma total_leq_lit[simp]: "totalp_on A leq_lit"
  unfolding totalp_on_def leq_lit_def leq_head_def by (auto split: option.splits literal.splits)

lemma leq_head_subst[simp]: "leq_head t (t ⋅ σ)"
  by (induct t) (auto simp: leq_head_def)

lemma leq_lit_match:
  fixes L K :: "('f :: linorder, 'v) term literal"
  shows "match_term_list [(atm_of L, atm_of K)] σ = Some τ ⟹ is_pos L = is_pos K ⟹ leq_lit L K"
  by (cases L; cases K)
    (auto simp: leq_lit_def dest!: match_term_list_sound split: option.splits)


subsection ‹Optimized Implementation of Clause Subsumption›

fun subsumes_list_filter where
  "subsumes_list_filter [] Ks σ = True"
| "subsumes_list_filter (L # Ls) Ks σ =
     (let Ks = filter (leq_lit L) Ks in
     (∃K ∈ set Ks. is_pos K = is_pos L ∧
       (case match_term_list [(atm_of L, atm_of K)] σ of
         None ⇒ False
       | Some ρ ⇒ subsumes_list_filter Ls (remove1 K Ks) ρ)))"

lemma sorted_wrt_subsumes_list_subsumes_list_filter:
  "sorted_wrt leq_lit Ls ⟹ subsumes_list Ls Ks σ = subsumes_list_filter Ls Ks σ"
proof (induction Ls arbitrary: Ks σ)
  case (Cons L Ls)
  from Cons.prems have "subsumes_list (L # Ls) Ks σ = subsumes_list (L # Ls) (filter (leq_lit L) Ks) σ"
    by (intro subsumes_list_Cons_filter_iff[symmetric]) (auto dest: leq_lit_match)
  also have "subsumes_list (L # Ls) (filter (leq_lit L) Ks) σ = subsumes_list_filter (L # Ls) Ks σ"
    using Cons.prems by (auto simp: Cons.IH split: option.splits)
  finally show ?case .
qed simp


subsection ‹Definition of Deterministic QuickSort›

text ‹
  This is the functional description of the standard variant of deterministic
  QuickSort that always chooses the first list element as the pivot as given
  by Hoare in 1962. For a list that is already sorted, this leads to $n(n-1)$
  comparisons, but as is well known, the average case is much better.

  The code below is adapted from Manuel Eberl's ‹Quick_Sort_Cost› AFP
  entry, but without invoking probability theory and using a predicate instead
  of a set.
›

fun quicksort :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
  "quicksort _ [] = []"
| "quicksort R (x # xs) =
     quicksort R (filter (λy. R y x) xs) @ [x] @ quicksort R (filter (λy. ¬ R y x) xs)"

text ‹
  We can easily show that this QuickSort is correct:
›

theorem mset_quicksort [simp]: "mset (quicksort R xs) = mset xs"
  by (induction R xs rule: quicksort.induct) simp_all

corollary set_quicksort [simp]: "set (quicksort R xs) = set xs"
  by (induction R xs rule: quicksort.induct) auto

theorem sorted_wrt_quicksort:
  assumes "transp R" and "totalp_on (set xs) R" and "reflp_on (set xs) R"
  shows   "sorted_wrt R (quicksort R xs)"
using assms
proof (induction R xs rule: quicksort.induct)
  case (2 R x xs)
  have total: "R a b" if "¬ R b a" "a ∈ set (x#xs)" "b ∈ set (x#xs)" for a b
    using "2.prems" that unfolding totalp_on_def reflp_on_def by (cases "a = b") auto

  have "sorted_wrt R (quicksort R (filter (λy. R y x) xs))"
          "sorted_wrt R (quicksort R (filter (λy. ¬ R y x) xs))"
    using "2.prems" by (intro "2.IH"; auto simp: totalp_on_def reflp_on_def)+
  then show ?case
    by (auto simp: sorted_wrt_append ‹transp R›
     intro: transpD[OF ‹transp R›] dest!: total)
qed auto

text ‹
End of the material adapted from Eberl's ‹Quick_Sort_Cost›.
›

lemma subsumes_list_subsumes_list_filter[abs_def, code_unfold]:
  "subsumes_list Ls Ks σ = subsumes_list_filter (quicksort leq_lit Ls) Ks σ"
  by (rule trans[OF box_equals[OF _ subsumes_list_alt[symmetric] subsumes_list_alt[symmetric]]
    sorted_wrt_subsumes_list_subsumes_list_filter])
    (auto simp: sorted_wrt_quicksort)

end