Theory Given_Clause_Architectures_Revisited

(*  Title:       New Fairness Proofs for the Given Clause Prover Architectures
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2020
*)

section ‹New Fairness Proofs for the Given Clause Prover Architectures›

theory Given_Clause_Architectures_Revisited
  imports Saturation_Framework.Given_Clause_Architectures
begin

text ‹The given clause and lazy given clause procedures satisfy key invariants. This
provides an alternative way to prove fairness and hence saturation of the limit.›


subsection ‹Given Clause Procedure›

context given_clause
begin

definition gc_invar :: "('f × 'l) set llist ⇒ enat ⇒ bool" where
  "gc_invar Ns i ⟷
   Inf_from (active_subset (Liminf_upto_llist Ns i)) ⊆ Sup_upto_llist (lmap Red_I_𝒢 Ns) i"

lemma gc_invar_infinity:
  assumes
    nnil: "¬ lnull Ns" and
    invar: "∀i. enat i < llength Ns ⟶ gc_invar Ns (enat i)"
  shows "gc_invar Ns ∞"
  unfolding gc_invar_def
proof (intro subsetI, unfold Liminf_upto_llist_infinity Sup_upto_llist_infinity)
  fix ι
  assume ι_inff: "ι ∈ Inf_from (active_subset (Liminf_llist Ns))"

  define As where
    "As = lmap active_subset Ns"

  have act_ns: "active_subset (Liminf_llist Ns) = Liminf_llist As"
    unfolding As_def active_subset_def Liminf_set_filter_commute[symmetric] ..

  note ι_inf = Inf_if_Inf_from[OF ι_inff]
  note ι_inff' = ι_inff[unfolded act_ns]

  have "¬ lnull As"
    unfolding As_def using nnil by auto
  moreover have "set (prems_of ι) ⊆ Liminf_llist As"
    using ι_inff'[unfolded Inf_from_def] by simp
  ultimately obtain i where
    i_lt_as: "enat i < llength As" and
    prems_sub_ge_i: "set (prems_of ι) ⊆ (⋂j ∈ {j. i ≤ j ∧ enat j < llength As}. lnth As j)"
    using finite_subset_Liminf_llist_imp_exists_index by blast

  note i_lt_ns = i_lt_as[unfolded As_def, simplified]

  have "set (prems_of ι) ⊆ lnth As i"
    using prems_sub_ge_i i_lt_as by auto
  then have "ι ∈ Inf_from (active_subset (lnth Ns i))"
    using i_lt_as ι_inf unfolding Inf_from_def As_def by auto
  then have "ι ∈ Sup_upto_llist (lmap Red_I_𝒢 Ns) (enat i)"
    using nnil i_lt_ns invar[unfolded gc_invar_def] by auto
  then show "ι ∈ Sup_llist (lmap Red_I_𝒢 Ns)"
    using Sup_upto_llist_subset_Sup_llist by fastforce
qed

lemma gc_invar_gc_init:
  assumes
    "¬ lnull Ns" and
    "active_subset (lhd Ns) = {}"
  shows "gc_invar Ns 0"
  using assms labeled_inf_have_prems unfolding gc_invar_def Inf_from_def by auto

lemma gc_invar_gc_step:
  assumes
    Si_lt: "enat (Suc i) < llength Ns" and
    invar: "gc_invar Ns i" and
    step: "lnth Ns i ↝GC lnth Ns (Suc i)"
  shows "gc_invar Ns (Suc i)"
  using step Si_lt invar
proof cases
  have i_lt: "enat i < llength Ns"
    using Si_lt Suc_ile_eq order.strict_implies_order by blast
  have lim_i: "Liminf_upto_llist Ns (enat i) = lnth Ns i"
    using i_lt by auto
  have lim_Si: "Liminf_upto_llist Ns (enat (Suc i)) = lnth Ns (Suc i)"
    using Si_lt by auto

  {
    case (process N M M')
    note ni = this(1) and nSi = this(2) and m'_pas = this(4)

    have "Inf_from (active_subset (N ∪ M')) ⊆ Inf_from (active_subset (N ∪ M))"
      using m'_pas by (simp add: Inf_from_mono)
    also have "… ⊆ Sup_upto_llist (lmap Red_I_𝒢 Ns) (enat i)"
      using invar unfolding gc_invar_def lim_i ni by auto
    also have "… ⊆ Sup_upto_llist (lmap Red_I_𝒢 Ns) (enat (Suc i))"
      by simp
    finally show ?thesis
      unfolding gc_invar_def lim_Si nSi .
  next
    case (infer N C L M)
    note ni = this(1) and nSi = this(2) and l_pas = this(3) and m_pas = this(4) and
      inff_red = this(5)

    {
      fix ι
      assume ι_inff: "ι ∈ Inf_from (active_subset (N ∪ {(C, active)} ∪ M))"

      have ι_inf: "ι ∈ Inf_FL"
        using ι_inff unfolding Inf_from_def by auto
      then have Fι_inf: "to_F ι ∈ Inf_F"
        using in_Inf_FL_imp_to_F_in_Inf_F by blast

      have "ι ∈ Inf_from (active_subset N ∪ {(C, active)})"
        using ι_inff m_pas by simp
      then have Fι_inff:
        "to_F ι ∈ no_labels.Inf_from (fst ` (active_subset N ∪ {(C, active)}))"
        using Fι_inf unfolding to_F_def Inf_from_def no_labels.Inf_from_def by auto

      have "ι ∈ Sup_upto_llist (lmap Red_I_𝒢 Ns) (enat (Suc i))"
      proof (cases "to_F ι ∈ no_labels.Inf_between (fst ` active_subset N) {C}")
        case True
        then have "to_F ι ∈ no_labels.Red_I_𝒢 (fst ` (N ∪ {(C, active)} ∪ M))"
          using inff_red by auto
        then have "ι ∈ Red_I_𝒢 (N ∪ {(C, active)} ∪ M)"
          by (subst labeled_red_inf_eq_red_inf[OF ι_inf])
        then show ?thesis
          using Si_lt using nSi by auto
      next
        case False
        then have "to_F ι ∈ no_labels.Inf_from (fst ` active_subset N)"
          using Fι_inff unfolding no_labels.Inf_from_def no_labels.Inf_between_def by auto
        then have "ι ∈ Inf_from (active_subset N)"
          using ι_inf l_pas unfolding to_F_def Inf_from_def no_labels.Inf_from_def
          by clarsimp (smt ι_inff[unfolded Inf_from_def] active_subset_def imageE image_subset_iff
              in_mono mem_Collect_eq prod.collapse)
        then show ?thesis
          using invar l_pas unfolding gc_invar_def lim_i ni by auto
      qed
    }
    then show ?thesis
      unfolding gc_invar_def lim_Si nSi by blast
  }
qed

lemma gc_invar_gc:
  assumes
    gc: "chain (↝GC) Ns" and
    init: "active_subset (lhd Ns) = {}" and
    i_lt: "i < llength Ns"
  shows "gc_invar Ns i"
  using i_lt
proof (induct i)
  case (enat i)
  then show ?case
  proof (induct i)
    case 0
    then show ?case
      using gc_invar_gc_init[OF chain_not_lnull[OF gc] init] by (simp add: enat_0)
  next
    case (Suc i)
    note ih = this(1) and Si_lt = this(2)
    have i_lt: "enat i < llength Ns"
      using Si_lt Suc_ile_eq less_le by blast
    show ?case
      by (rule gc_invar_gc_step[OF Si_lt ih[OF i_lt] chain_lnth_rel[OF gc Si_lt]])
  qed
qed simp

lemma gc_fair_new_proof:
  assumes
    gc: "chain (↝GC) Ns" and
    init: "active_subset (lhd Ns) = {}" and
    lim: "passive_subset (Liminf_llist Ns) = {}"
  shows "fair Ns"
  unfolding fair_def
proof -
  have "Inf_from (Liminf_llist Ns) ⊆ Inf_from (active_subset (Liminf_llist Ns))" (is "?lhs ⊆ _")
    using lim unfolding active_subset_def passive_subset_def
    by (metis (no_types, lifting) Inf_from_mono empty_Collect_eq mem_Collect_eq subsetI)
  also have "... ⊆ Sup_llist (lmap Red_I_𝒢 Ns)" (is "_ ⊆ ?rhs")
    using gc_invar_infinity[OF chain_not_lnull[OF gc]] gc_invar_gc[OF gc init]
    unfolding gc_invar_def by fastforce
  finally show "?lhs ⊆ ?rhs"
    .
qed

end


subsection ‹Lazy Given Clause›

context lazy_given_clause
begin

definition from_F :: "'f inference ⇒ ('f × 'l) inference set" where
  "from_F ι = {ι' ∈ Inf_FL. to_F ι' = ι}"

definition lgc_invar :: "('f inference set × ('f × 'l) set) llist ⇒ enat ⇒ bool" where
  "lgc_invar TNs i ⟷
   Inf_from (active_subset (Liminf_upto_llist (lmap snd TNs) i))
   ⊆ ⋃ (from_F ` Liminf_upto_llist (lmap fst TNs) i) ∪ Sup_upto_llist (lmap (Red_I_𝒢 ∘ snd) TNs) i"

lemma lgc_invar_infinity:
  assumes
    nnil: "¬ lnull TNs" and
    invar: "∀i. enat i < llength TNs ⟶ lgc_invar TNs (enat i)"
  shows "lgc_invar TNs ∞"
  unfolding lgc_invar_def
proof (intro subsetI, unfold Liminf_upto_llist_infinity Sup_upto_llist_infinity)
  fix ι
  assume ι_inff: "ι ∈ Inf_from (active_subset (Liminf_llist (lmap snd TNs)))"

  define As where
    "As = lmap (active_subset ∘ snd) TNs"

  have act_ns: "active_subset (Liminf_llist (lmap snd TNs)) = Liminf_llist As"
    unfolding As_def active_subset_def Liminf_set_filter_commute[symmetric] llist.map_comp ..

  note ι_inf = Inf_if_Inf_from[OF ι_inff]
  note ι_inff' = ι_inff[unfolded act_ns]

  show "ι ∈ ⋃ (from_F ` Liminf_llist (lmap fst TNs)) ∪ Sup_llist (lmap (Red_I_𝒢 ∘ snd) TNs)"
  proof -
    {
      assume ι_ni_lim: "ι ∉ ⋃ (from_F ` Liminf_llist (lmap fst TNs))"

      have "¬ lnull As"
        unfolding As_def using nnil by auto
      moreover have "set (prems_of ι) ⊆ Liminf_llist As"
        using ι_inff'[unfolded Inf_from_def] by simp
      ultimately obtain i where
        i_lt_as: "enat i < llength As" and
        prems_sub_ge_i: "set (prems_of ι) ⊆ (⋂j ∈ {j. i ≤ j ∧ enat j < llength As}. lnth As j)"
        using finite_subset_Liminf_llist_imp_exists_index by blast

      have ts_nnil: "¬ lnull (lmap fst TNs)"
        using As_def nnil by simp

      have Fι_ni_lim: "to_F ι ∉ Liminf_llist (lmap fst TNs)"
        using ι_inf ι_ni_lim unfolding from_F_def by auto
      obtain i' where
        i_le_i': "i ≤ i'" and
        i'_lt_as: "enat i' < llength As" and
        Fι_ni_i': "to_F ι ∉ lnth (lmap fst TNs) i'"
        using i_lt_as not_Liminf_llist_imp_exists_index[OF ts_nnil Fι_ni_lim, of i] unfolding As_def
        by auto

      have ι_ni_i': "ι ∉ ⋃ (from_F ` fst (lnth TNs i'))"
        using Fι_ni_i' i'_lt_as[unfolded As_def] unfolding from_F_def by auto

      have "set (prems_of ι) ⊆ (⋂j ∈ {j. i' ≤ j ∧ enat j < llength As}. lnth As j)"
        using prems_sub_ge_i i_le_i' by auto
      then have "set (prems_of ι) ⊆ lnth As i'"
        using i'_lt_as by auto
      then have "ι ∈ Inf_from (active_subset (snd (lnth TNs i')))"
        using i'_lt_as ι_inf unfolding Inf_from_def As_def by auto
      then have ι_in_i': "ι ∈ Sup_upto_llist (lmap (Red_I_𝒢 ∘ snd) TNs) (enat i')"
        using ι_ni_i' i'_lt_as[unfolded As_def] invar[unfolded lgc_invar_def] by auto
      then have "ι ∈ Sup_llist (lmap (Red_I_𝒢 ∘ snd) TNs)"
        using Sup_upto_llist_subset_Sup_llist by fastforce
    }
    then show ?thesis
      by blast
  qed
qed

lemma lgc_invar_lgc_init:
  assumes
    nnil: "¬ lnull TNs" and
    n_init: "active_subset (snd (lhd TNs)) = {}" and
    t_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd TNs)"
  shows "lgc_invar TNs 0"
  unfolding lgc_invar_def
proof -
  have "Inf_from (active_subset (Liminf_upto_llist (lmap snd TNs) 0)) =
    Inf_from {}" (is "?lhs = _")
    using nnil n_init by auto
  also have "... ⊆ ⋃ (from_F ` fst (lhd TNs))"
    using t_init Inf_FL_to_Inf_F unfolding Inf_from_def from_F_def to_F_def by force
  also have "... ⊆ ⋃ (from_F ` fst (lhd TNs)) ∪ Red_I_𝒢 (snd (lhd TNs))"
    by fast
  also have "... = ⋃ (from_F ` Liminf_upto_llist (lmap fst TNs) 0)
    ∪ Sup_upto_llist (lmap (Red_I_𝒢 ∘ snd) TNs) 0" (is "_ = ?rhs")
    using nnil by auto
  finally show "?lhs ⊆ ?rhs"
    .
qed

lemma lgc_invar_lgc_step:
  assumes
    Si_lt: "enat (Suc i) < llength TNs" and
    invar: "lgc_invar TNs i" and
    step: "lnth TNs i ↝LGC lnth TNs (Suc i)"
  shows "lgc_invar TNs (Suc i)"
  using step Si_lt invar
proof cases
  let ?Sup_Red_i = "Sup_upto_llist (lmap (Red_I_𝒢 ∘ snd) TNs) (enat i)"
  let ?Sup_Red_Si = "Sup_upto_llist (lmap (Red_I_𝒢 ∘ snd) TNs) (enat (Suc i))"

  have i_lt: "enat i < llength TNs"
    using Si_lt Suc_ile_eq order.strict_implies_order by blast

  have lim_i:
    "Liminf_upto_llist (lmap fst TNs) (enat i) = lnth (lmap fst TNs) i"
    "Liminf_upto_llist (lmap snd TNs) (enat i) = lnth (lmap snd TNs) i"
    using i_lt by auto
  have lim_Si:
    "Liminf_upto_llist (lmap fst TNs) (enat (Suc i)) = lnth (lmap fst TNs) (Suc i)"
    "Liminf_upto_llist (lmap snd TNs) (enat (Suc i)) = lnth (lmap snd TNs) (Suc i)"
    using Si_lt by auto

  {
    case (process N1 N M N2 M' T)
    note tni = this(1) and tnSi = this(2) and n1 = this(3) and n2 = this(4) and m_red = this(5) and
      m'_pas = this(6)

    have ni: "lnth (lmap snd TNs) i = N ∪ M"
      by (simp add: i_lt n1 tni)
    have nSi: "lnth (lmap snd TNs) (Suc i) = N ∪ M'"
      by (simp add: Si_lt n2 tnSi)
    have ti: "lnth (lmap fst TNs) i = T"
      by (simp add: i_lt tni)
    have tSi: "lnth (lmap fst TNs) (Suc i) = T"
      by (simp add: Si_lt tnSi)

    have "Inf_from (active_subset (N ∪ M')) ⊆ Inf_from (active_subset (N ∪ M))"
      using m'_pas by (simp add: Inf_from_mono)
    also have "… ⊆ ⋃ (from_F ` T) ∪ ?Sup_Red_i"
      using invar unfolding lgc_invar_def lim_i ni ti .
    also have "… ⊆ ⋃ (from_F ` T) ∪ ?Sup_Red_Si"
      using Sup_upto_llist_mono by auto
    finally show ?thesis
      unfolding lgc_invar_def lim_Si nSi tSi .
  next
    case (schedule_infer T2 T1 T' N1 N C L N2)
    note tni = this(1) and tnSi = this(2) and t2 = this(3) and n1 = this(4) and n2 = this(5) and
      l_pas = this(6) and t' = this(7)

    have ni: "lnth (lmap snd TNs) i = N ∪ {(C, L)}"
      by (simp add: i_lt n1 tni)
    have nSi: "lnth (lmap snd TNs) (Suc i) = N ∪ {(C, active)}"
      by (simp add: Si_lt n2 tnSi)
    have ti: "lnth (lmap fst TNs) i = T1"
      by (simp add: i_lt tni)
    have tSi: "lnth (lmap fst TNs) (Suc i) = T1 ∪ T'"
      by (simp add: Si_lt t2 tnSi)

    {
      fix ι
      assume ι_inff: "ι ∈ Inf_from (active_subset (N ∪ {(C, active)}))"

      have ι_inf: "ι ∈ Inf_FL"
        using ι_inff unfolding Inf_from_def by auto
      then have Fι_inf: "to_F ι ∈ Inf_F"
        using in_Inf_FL_imp_to_F_in_Inf_F by blast

      have "ι ∈ ⋃ (from_F ` (T1 ∪ T')) ∪ ?Sup_Red_Si"
      proof (cases "to_F ι ∈ no_labels.Inf_between (fst ` active_subset N) {C}")
        case True
        then have "ι ∈ ⋃ (from_F ` (T1 ∪ T'))"
          unfolding t' from_F_def using ι_inf by auto
        then show ?thesis
          by blast
      next
        case False
        moreover have "to_F ι ∈ no_labels.Inf_from (fst ` (active_subset N ∪ {(C, active)}))"
          using ι_inff Fι_inf unfolding to_F_def Inf_from_def no_labels.Inf_from_def by auto
        ultimately have "to_F ι ∈ no_labels.Inf_from (fst ` active_subset N)"
          unfolding no_labels.Inf_from_def no_labels.Inf_between_def by auto
        then have "ι ∈ Inf_from (active_subset N)"
          using ι_inf unfolding to_F_def no_labels.Inf_from_def
          by clarsimp (smt Inf_from_def Un_insert_right ι_inff active_subset_def
            boolean_algebra_cancel.sup0 imageE image_subset_iff insert_iff mem_Collect_eq
            prod.collapse snd_conv subset_iff)
        then have "ι ∈ ⋃ (from_F ` (T1 ∪ T')) ∪ ?Sup_Red_i"
          using invar[unfolded lgc_invar_def] l_pas unfolding lim_i ni ti by auto
        then show ?thesis
          using Sup_upto_llist_mono by force
      qed
    }
    then show ?thesis
      unfolding lgc_invar_def lim_i lim_Si nSi tSi by fast
  next
    case (compute_infer T1 T2 ι' N2 N1 M)
    note tni = this(1) and tnSi = this(2) and t1 = this(3) and n2 = this(4) and m_pas = this(5) and
      ι'_red = this(6)

    have ni: "lnth (lmap snd TNs) i = N1"
      by (simp add: i_lt tni)
    have nSi: "lnth (lmap snd TNs) (Suc i) = N1 ∪ M"
      by (simp add: Si_lt n2 tnSi)
    have ti: "lnth (lmap fst TNs) i = T2 ∪ {ι'}"
      by (simp add: i_lt t1 tni)
    have tSi: "lnth (lmap fst TNs) (Suc i) = T2"
      by (simp add: Si_lt tnSi)

    {
      fix ι
      assume ι_inff: "ι ∈ Inf_from (active_subset (N1 ∪ M))"

      have ι_bef: "ι ∈ ⋃ (from_F ` (T2 ∪ {ι'})) ∪ ?Sup_Red_i"
        using ι_inff invar[unfolded lgc_invar_def lim_i ti ni] m_pas by auto
      have "ι ∈ ⋃ (from_F ` T2) ∪ ?Sup_Red_Si"
      proof (cases "ι ∈ from_F ι'")
        case ι_in_ι': True
        then have "ι ∈ Red_I_𝒢 (N1 ∪ M)"
          using ι'_red from_F_def labeled_red_inf_eq_red_inf by auto
        then have "ι ∈ ?Sup_Red_Si"
          using Si_lt by (simp add: n2 tnSi)
        then show ?thesis
          by auto
      next
        case False
        then show ?thesis
          using ι_bef by auto
      qed
    }
    then show ?thesis
      unfolding lgc_invar_def lim_Si tSi nSi by blast
  next
    case (delete_orphan_infers T1 T2 T' N)
    note tni = this(1) and tnSi = this(2) and t1 = this(3) and t'_orph = this(4)

    have ni: "lnth (lmap snd TNs) i = N"
      by (simp add: i_lt tni)
    have nSi: "lnth (lmap snd TNs) (Suc i) = N"
      by (simp add: Si_lt tnSi)
    have ti: "lnth (lmap fst TNs) i = T2 ∪ T'"
      by (simp add: i_lt t1 tni)
    have tSi: "lnth (lmap fst TNs) (Suc i) = T2"
      by (simp add: Si_lt tnSi)

    {
      fix ι
      assume ι_inff: "ι ∈ Inf_from (active_subset N)"

      have "to_F ι ∉ T'"
        using t'_orph ι_inff in_Inf_from_imp_to_F_in_Inf_from by blast
      hence "ι ∉ ⋃ (from_F ` T')"
        unfolding from_F_def by auto
      then have "ι ∈ ⋃ (from_F ` T2) ∪ ?Sup_Red_Si"
        using ι_inff invar unfolding lgc_invar_def lim_i ni ti by auto
    }
    then show ?thesis
      unfolding lgc_invar_def lim_Si tSi nSi by blast
  }
qed

lemma lgc_invar_lgc:
  assumes
    lgc: "chain (↝LGC) TNs" and
    n_init: "active_subset (snd (lhd TNs)) = {}" and
    t_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd TNs)" and
    i_lt: "i < llength TNs"
  shows "lgc_invar TNs i"
  using i_lt
proof (induct i)
  case (enat i)
  then show ?case
  proof (induct i)
    case 0
    then show ?case
      using lgc_invar_lgc_init[OF chain_not_lnull[OF lgc] n_init t_init] by (simp add: enat_0)
  next
    case (Suc i)
    note ih = this(1) and Si_lt = this(2)
    have i_lt: "enat i < llength TNs"
      using Si_lt Suc_ile_eq less_le by blast
    show ?case
      by (rule lgc_invar_lgc_step[OF Si_lt ih[OF i_lt] chain_lnth_rel[OF lgc Si_lt]])
  qed
qed simp

lemma lgc_fair_new_proof:
  assumes
    lgc: "chain (↝LGC) TNs" and
    n_init: "active_subset (snd (lhd TNs)) = {}" and
    n_lim: "passive_subset (Liminf_llist (lmap snd TNs)) = {}" and
    t_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd TNs)" and
    t_lim: "Liminf_llist (lmap fst TNs) = {}"
  shows "fair (lmap snd TNs)"
  unfolding fair_def llist.map_comp
proof -
  have "Inf_from (Liminf_llist (lmap snd TNs))
    ⊆ Inf_from (active_subset (Liminf_llist (lmap snd TNs)))" (is "?lhs ⊆ _")
    by (rule Inf_from_mono) (use n_lim passive_subset_def active_subset_def in blast)
  also have "... ⊆ ⋃ (from_F ` Liminf_upto_llist (lmap fst TNs) ∞)
    ∪ Sup_llist (lmap (Red_I_𝒢 ∘ snd) TNs)"
    using lgc_invar_infinity[OF chain_not_lnull[OF lgc]] lgc_invar_lgc[OF lgc n_init t_init]
    unfolding lgc_invar_def by fastforce
  also have "... ⊆ Sup_llist (lmap (Red_I_𝒢 ∘ snd) TNs)" (is "_ ⊆ ?rhs")
    using t_lim by auto
  finally show "?lhs ⊆ ?rhs"
    .
qed

end

end