Theory SAT_Plan_Extensions

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory SAT_Plan_Extensions
  imports SAT_Plan_Base
begin
section "Serializable SATPlan Encodings"

text ‹ A SATPlan encoding with exclusion of operator interference (see definition
\ref{def:sat-plan-encoding-with-interference-exclusion}) can be defined by extending the basic
SATPlan encoding with clauses

  @{text[display, indent=4] "
    ¬(Atom (Operator k (index ops op1))
    ∨ ¬(Atom (Operator k (index ops op2))"}

for all pairs of distinct interfering operators term‹op1›, term‹op2› for all time points
term‹k < t› for a given estimated plan length term‹t›. Definitions
\ref{isadef:interfering-operator-pair-exclusion-encoding} and
\ref{isadef:interfering-operator-exclusion-encoding} implement the encoding for operator pairs
resp. for all interfering operator pairs and all time points. ›

definition encode_interfering_operator_pair_exclusion
  :: "'variable strips_problem
    ⇒ nat
    ⇒ 'variable strips_operator
    ⇒ 'variable strips_operator
    ⇒ sat_plan_variable formula"
  where "encode_interfering_operator_pair_exclusion Π k op1 op2
    ≡ let ops = operators_of Π in
      ¬(Atom (Operator k (index ops op1)))
      ∨ ¬(Atom (Operator k (index ops op2)))"

definition encode_interfering_operator_exclusion
  :: "'variable strips_problem ⇒ nat ⇒ sat_plan_variable formula"
  where "encode_interfering_operator_exclusion Π t ≡ let
      ops = operators_of Π
      ; interfering = filter (λ(op1, op2). index ops op1 ≠ index ops op2
        ∧ are_operators_interfering op1 op2) (List.product ops ops)
    in foldr (∧) [encode_interfering_operator_pair_exclusion Π k op1 op2.
      (op1, op2) ← interfering, k ← [0..<t]] (¬⊥)"

text ‹ A SATPlan encoding with interfering operator pair exclusion can now be defined by
simplying adding the conjunct term‹encode_interfering_operator_exclusion Π t› to the basic
SATPlan encoding. ›

― ‹ NOTE This is the quadratic size encoding for the $\forall$-step semantics as defined in @{cite
‹3.2.1, p.1045› "DBLP:journals/ai/RintanenHN06"}. This encoding ensures that decoded plans are
sequentializable by simply excluding the simultaneous execution of operators with potential
interference at any timepoint. Note that this yields a $\forall$-step plan for which parallel
operator execution at any time step may be sequentialised in any order (due to non-interference). ›

definition encode_problem_with_operator_interference_exclusion
  :: "'variable strips_problem ⇒ nat ⇒ sat_plan_variable formula"
  (‹Φ∀ _ _› 52)
  where "encode_problem_with_operator_interference_exclusion Π t
    ≡ encode_initial_state Π
      ∧ (encode_operators Π t
      ∧ (encode_all_frame_axioms Π t
      ∧ (encode_interfering_operator_exclusion Π t
      ∧ (encode_goal_state Π t))))"


― ‹ Immediately proof the sublocale proposition for strips in order to gain access to definitions
and lemmas. ›


lemma cnf_of_encode_interfering_operator_pair_exclusion_is_i[simp]:
  "cnf (encode_interfering_operator_pair_exclusion Π k op1 op2) = {{
    (Operator k (index (strips_problem.operators_of Π) op1))¯
      , (Operator k (index (strips_problem.operators_of Π) op2))¯ }}"
proof -
  let ?ops = "strips_problem.operators_of Π"
  have "cnf (encode_interfering_operator_pair_exclusion Π k op1 op2)
    = cnf (¬(Atom (Operator k (index ?ops op1))) ∨ ¬(Atom (Operator k (index ?ops op2))))"
    unfolding encode_interfering_operator_pair_exclusion_def
    by metis
  also have "… = { C ∪ D | C D.
    C ∈ cnf (¬(Atom (Operator k (index ?ops op1))))
    ∧ D ∈ cnf (¬(Atom (Operator k (index ?ops op2)))) }"
    by simp
  finally show ?thesis
    by auto
qed

lemma cnf_of_encode_interfering_operator_exclusion_is_ii[simp]:
  "set [encode_interfering_operator_pair_exclusion Π k op1 op2.
      (op1, op2) ← filter (λ(op1, op2).
          index (strips_problem.operators_of Π) op1 ≠ index (strips_problem.operators_of Π) op2
          ∧ are_operators_interfering op1 op2)
        (List.product (strips_problem.operators_of Π) (strips_problem.operators_of Π))
        , k ← [0..<t]]
    = (⋃(op1, op2)
        ∈ { (op1, op2) ∈ set (operators_of Π) × set (operators_of Π).
          index (strips_problem.operators_of Π) op1 ≠ index (strips_problem.operators_of Π) op2
          ∧ are_operators_interfering op1 op2 }.
      (λk. encode_interfering_operator_pair_exclusion Π k op1 op2) ` {0..<t})"
proof -
  let ?ops = "strips_problem.operators_of Π"
  let ?interfering = "filter (λ(op1, op2). index ?ops op1 ≠ index ?ops op2
    ∧ are_operators_interfering op1 op2) (List.product ?ops ?ops)"
  let ?fs = "[encode_interfering_operator_pair_exclusion Π k op1 op2.
    (op1, op2) ← ?interfering, k ← [0..<t]]"
  have "set ?fs = ⋃(set
    ` (λ(op1, op2). map (λk. encode_interfering_operator_pair_exclusion Π k op1 op2) [0..<t])
    ` (set (filter (λ(op1, op2). index ?ops op1 ≠ index ?ops op2 ∧ are_operators_interfering op1 op2)
      (List.product ?ops ?ops))))"
    unfolding set_concat set_map
    by blast
  ― ‹ TODO slow. ›
  also have "… = ⋃((λ(op1, op2).
      set (map (λk. encode_interfering_operator_pair_exclusion Π k op1 op2) [0..<t]))
    ` (set (filter (λ(op1, op2). index ?ops op1 ≠ index ?ops op2 ∧ are_operators_interfering op1 op2)
      (List.product ?ops ?ops))))"
    unfolding image_comp[of
        set "λ(op1, op2). map (λk. encode_interfering_operator_pair_exclusion Π k op1 op2) [0..<t]"]
      comp_apply
    by fast
  also have "… = ⋃((λ(op1, op2).
      (λk. encode_interfering_operator_pair_exclusion Π k op1 op2) ` {0..<t})
    ` (set (filter (λ(op1, op2). index ?ops op1 ≠ index ?ops op2 ∧ are_operators_interfering op1 op2)
      (List.product ?ops ?ops))))"
    unfolding set_map[of _ "[0..<t]"] atLeastLessThan_upt[of 0 t]
    by blast
  also have "… = ⋃((λ(op1, op2).
      (λk. encode_interfering_operator_pair_exclusion Π k op1 op2) ` {0..<t})
    ` (Set.filter (λ(op1, op2). index ?ops op1 ≠ index ?ops op2 ∧ are_operators_interfering op1 op2)
      (set (List.product ?ops ?ops))))"
    unfolding set_filter[of "λ(op1, op2). are_operators_interfering op1 op2" "List.product ?ops ?ops"]
    by force
  ― ‹ TODO slow.›
  finally show ?thesis
    unfolding operators_of_def set_product[of ?ops ?ops]
    by fastforce
qed

(* TODO refactor using above lemma *)
lemma cnf_of_encode_interfering_operator_exclusion_is_iii[simp]:
  (* TODO why is this necessary? *)
  fixes Π :: "'variable strips_problem"
  shows "cnf ` set [encode_interfering_operator_pair_exclusion Π k op1 op2.
      (op1, op2) ← filter (λ(op1, op2).
          index (strips_problem.operators_of Π) op1 ≠ index (strips_problem.operators_of Π) op2
          ∧ are_operators_interfering op1 op2)
        (List.product (strips_problem.operators_of Π) (strips_problem.operators_of Π))
      , k ← [0..<t]]
    = (⋃(op1, op2)
        ∈ { (op1, op2) ∈ set (strips_problem.operators_of Π) × set (strips_problem.operators_of Π).
          index (strips_problem.operators_of Π) op1 ≠ index (strips_problem.operators_of Π) op2
          ∧ are_operators_interfering op1 op2 }.
      {{{ (Operator k (index (strips_problem.operators_of Π) op1))¯
        , (Operator k (index (strips_problem.operators_of Π) op2))¯ }} | k. k ∈ {0..<t}})"
proof -
  let ?ops = "strips_problem.operators_of Π"
  let ?interfering = "filter (λ(op1, op2). index ?ops op1 ≠ index ?ops op2
    ∧ are_operators_interfering op1 op2) (List.product ?ops ?ops)"
  let ?fs = "[encode_interfering_operator_pair_exclusion Π k op1 op2.
    (op1, op2) ← ?interfering, k ← [0..<t]]"
  have "cnf ` set ?fs = cnf ` (⋃(op1, op2) ∈ { (op1, op2).
    (op1, op2) ∈ set (operators_of Π) × set (operators_of Π) ∧ index ?ops op1 ≠ index ?ops op2
      ∧ are_operators_interfering op1 op2 }.
    (λk. encode_interfering_operator_pair_exclusion Π k op1 op2) ` {0..<t})"
    unfolding cnf_of_encode_interfering_operator_exclusion_is_ii
    by blast
  also have "… = (⋃(op1, op2) ∈ { (op1, op2).
    (op1, op2) ∈ set (operators_of Π) × set (operators_of Π) ∧ index ?ops op1 ≠ index ?ops op2
      ∧ are_operators_interfering op1 op2 }.
    (λk. cnf (encode_interfering_operator_pair_exclusion Π k op1 op2)) ` {0..<t})"
    unfolding image_Un image_comp comp_apply
    by blast
  also have "… = (⋃(op1, op2) ∈ { (op1, op2).
    (op1, op2) ∈ set (operators_of Π) × set (operators_of Π) ∧ index ?ops op1 ≠ index ?ops op2
      ∧ are_operators_interfering op1 op2 }.
    (λk. {{ (Operator k (index ?ops op1))¯, (Operator k (index ?ops op2))¯ }}) ` {0..<t})"
    by simp
  also have "… = (⋃(op1, op2) ∈ { (op1, op2).
    (op1, op2) ∈ set (operators_of Π) × set (operators_of Π) ∧ index ?ops op1 ≠ index ?ops op2
        ∧ are_operators_interfering op1 op2 }.
      (λk. {{ (Operator k (index ?ops op1))¯, (Operator k (index ?ops op2))¯ }})
        ` { k | k. k ∈ {0..<t}})"
    by blast
  ― ‹ TODO slow.›
  finally show ?thesis
    unfolding operators_of_def setcompr_eq_image[of _ "λk. k ∈ {0..<t}"]
    by force
qed

lemma cnf_of_encode_interfering_operator_exclusion_is:
  "cnf (encode_interfering_operator_exclusion Π t) = ⋃(⋃(op1, op2)
      ∈ { (op1, op2) ∈ set (operators_of Π) × set (operators_of Π).
        index (strips_problem.operators_of Π) op1 ≠ index (strips_problem.operators_of Π) op2
          ∧ are_operators_interfering op1 op2 }.
    {{{ (Operator k (index (strips_problem.operators_of Π) op1))¯
      , (Operator k (index (strips_problem.operators_of Π) op2))¯ }} | k. k ∈ {0..<t}})"
proof -
  let ?ops = "strips_problem.operators_of Π"
  let ?interfering = "filter (λ(op1, op2). index ?ops op1 ≠ index ?ops op2
    ∧ are_operators_interfering op1 op2) (List.product ?ops ?ops)"
  let ?fs = "[encode_interfering_operator_pair_exclusion Π k op1 op2.
    (op1, op2) ← ?interfering, k ← [0..<t]]"
  have "cnf (encode_interfering_operator_exclusion Π t) = cnf (foldr (∧) ?fs (¬⊥))"
    unfolding encode_interfering_operator_exclusion_def
    by metis
  also have "… = ⋃(cnf ` set ?fs)"
    unfolding cnf_foldr_and[of ?fs]..
  finally show ?thesis
    unfolding cnf_of_encode_interfering_operator_exclusion_is_iii[of Π t]
    by blast
qed

lemma cnf_of_encode_interfering_operator_exclusion_contains_clause_if:
  (* TODO why do we need to fix the problem type? *)
  fixes Π :: "'variable strips_problem"
  assumes "k < t"
    and "op1 ∈ set (strips_problem.operators_of Π)" and "op2 ∈ set (strips_problem.operators_of Π)"
    and "index (strips_problem.operators_of Π) op1 ≠ index (strips_problem.operators_of Π) op2"
    and "are_operators_interfering op1 op2"
  shows "{ (Operator k (index (strips_problem.operators_of Π) op1))¯
      , (Operator k (index (strips_problem.operators_of Π) op2))¯}
    ∈ cnf (encode_interfering_operator_exclusion Π t)"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?ΦX = "encode_interfering_operator_exclusion Π t"
  let ?Ops = "{ (op1, op2) ∈ set (operators_of Π) × set (operators_of Π).
        index ?ops op1 ≠ index ?ops op2 ∧ are_operators_interfering op1 op2 }"
    and ?f = "λ(op1, op2). {{{ (Operator k (index ?ops op1))¯, (Operator k (index ?ops op2))¯ }}
      | k. k ∈ {0..<t}}"
  let ?A = "(⋃(op1, op2) ∈ ?Ops. ?f (op1, op2))"
  let ?B = "⋃?A"
    and ?C = "{ (Operator k (index ?ops op1))¯, (Operator k (index ?ops op2))¯ }"
  {
    have "(op1, op2) ∈ ?Ops"
      using assms(2, 3, 4, 5)
      unfolding operators_of_def
      by force
    moreover have "{ ?C } ∈ ?f (op1, op2)"
      using assms(1)
      by auto
    moreover have "{ ?C } ∈ ?A"
      using UN_iff[of ?C _ ?Ops] calculation(1, 2)
      by blast
    (* TODO slow *)
    ultimately have "∃X ∈ ?A. ?C ∈ X"
      by auto
  }
  (* TODO slow *)
  thus ?thesis
    unfolding cnf_of_encode_interfering_operator_exclusion_is
    using Union_iff[of ?C ?A]
    by auto
qed

lemma is_cnf_encode_interfering_operator_exclusion:
  (* TODO why is this necessary? *)
  fixes Π :: "'variable strips_problem"
  shows "is_cnf (encode_interfering_operator_exclusion Π t)"
proof -
  let ?ops = "strips_problem.operators_of Π"
  let ?interfering = "filter (λ(op1, op2). index ?ops op1 ≠ index ?ops op2
    ∧ are_operators_interfering op1 op2) (List.product ?ops ?ops)"
  let ?fs = "[encode_interfering_operator_pair_exclusion Π k op1 op2.
    (op1, op2) ← ?interfering, k ← [0..<t]]"
  let ?Fs = "(⋃(op1, op2)
        ∈ { (op1, op2) ∈ set (operators_of Π) × set (operators_of Π). are_operators_interfering op1 op2 }.
      (λk. encode_interfering_operator_pair_exclusion Π k op1 op2) ` {0..<t})"
  {
    fix f
    assume "f ∈ set ?fs"
    then have "f ∈ ?Fs"
      unfolding cnf_of_encode_interfering_operator_exclusion_is_ii
      by blast
    then obtain op1 op2
      where "(op1, op2) ∈ set (operators_of Π) × set (operators_of Π)"
      and "are_operators_interfering op1 op2"
      and "f ∈ (λk. encode_interfering_operator_pair_exclusion Π k op1 op2) ` {0..<t}"
      by fast
    then obtain k where "f = encode_interfering_operator_pair_exclusion Π k op1 op2"
      by blast
    then have "f = ¬(Atom (Operator k (index ?ops op1))) ∨ ¬(Atom (Operator k (index ?ops op2)))"
      unfolding encode_interfering_operator_pair_exclusion_def
      by metis
    hence "is_cnf f"
      by force
  }
  thus ?thesis
    unfolding encode_interfering_operator_exclusion_def
    using is_cnf_foldr_and_if[of ?fs]
    by meson
qed

lemma is_cnf_encode_problem_with_operator_interference_exclusion:
  assumes "is_valid_problem_strips Π"
  shows "is_cnf (Φ∀ Π t)"
  using is_cnf_encode_problem is_cnf_encode_interfering_operator_exclusion assms
  unfolding encode_problem_with_operator_interference_exclusion_def SAT_Plan_Base.encode_problem_def
    is_cnf.simps(1)
  by blast

lemma cnf_of_encode_problem_with_operator_interference_exclusion_structure:
  shows "cnf (ΦI Π) ⊆ cnf (Φ∀ Π t)"
    and "cnf ((ΦG Π) t) ⊆ cnf (Φ∀ Π t)"
    and "cnf (encode_operators Π t) ⊆ cnf (Φ∀ Π t)"
    and "cnf (encode_all_frame_axioms Π t) ⊆ cnf (Φ∀ Π t)"
    and "cnf (encode_interfering_operator_exclusion Π t) ⊆ cnf (Φ∀ Π t)"
  unfolding encode_problem_with_operator_interference_exclusion_def encode_problem_def SAT_Plan_Base.encode_problem_def
    encode_initial_state_def
    encode_goal_state_def
  by auto+

(* TODO remove (unused)? *)
lemma encode_problem_with_operator_interference_exclusion_has_model_then_also_partial_encodings:
  assumes "𝒜 ⊨ Φ∀ Π t"
  shows "𝒜 ⊨ SAT_Plan_Base.encode_initial_state Π"
    and "𝒜 ⊨ SAT_Plan_Base.encode_operators Π t"
    and "𝒜 ⊨ SAT_Plan_Base.encode_all_frame_axioms Π t"
    and "𝒜 ⊨ encode_interfering_operator_exclusion Π t"
    and "𝒜 ⊨ SAT_Plan_Base.encode_goal_state Π t"
  using assms
  unfolding encode_problem_with_operator_interference_exclusion_def encode_problem_def SAT_Plan_Base.encode_problem_def
  by simp+



text ‹ Just as for the basic SATPlan encoding we defined local context for the SATPlan encoding
with interfering operator exclusion. We omit this here since it is basically identical to the one
shown in the basic SATPlan theory replacing only the definitions of \isaname{encode_transitions}
and \isaname{encode_problem}. The sublocale proof is shown below. It confirms that the new
encoding again a CNF as required by locale \isaname{sat_encode_strips}. ›

subsection "Soundness"


text ‹ The Proof of soundness for the SATPlan encoding with interfering operator exclusion follows
directly from the proof of soundness of the basic SATPlan encoding. By looking at the structure of
the new encoding which simply extends the basic SATPlan encoding with a conjunct, any model for
encoding with exclusion of operator interference also models the basic SATPlan encoding and the
soundness of the new encoding therefore follows from theorem
\ref{isathm:soundness-satplan-encoding}.

Moreover, since we additionally added interfering operator exclusion clauses at every timestep, the
decoded parallel plan cannot contain any interfering operators in any parallel operator (making it
serializable). ›

― ‹ NOTE We use the ‹subseq› formulation in the fourth assumption to be able to instantiate the
induction hypothesis on the subseq ‹ops› given the induction premise
‹op # ops ∈ set (subseqs (Φ¯ Π 𝒜 t ! k))›. We do not use subsets in the
assumption since we would otherwise lose the distinctness property which can be infered from
‹ops ∈ set (subseqs (Φ¯ Π 𝒜 t ! k))› using lemma ‹subseqs_distinctD›. ›
lemma encode_problem_serializable_sound_i:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ∀ Π t"
    and "k < t"
    and "ops ∈ set (subseqs ((Φ¯ Π 𝒜 t) ! k))"
  shows "are_all_operators_non_interfering ops"
proof -
  let ?ops = "strips_problem.operators_of Π"
    and ?π = "Φ¯ Π 𝒜 t"
    and ?ΦX = "encode_interfering_operator_exclusion Π t"
  let ?πk = "(Φ¯ Π 𝒜 t) ! k"
  (* TODO refactor *)
  {
    fix C
    assume C_in: "C ∈ cnf ?ΦX"
    have "cnf_semantics 𝒜 (cnf ?ΦX)"
      using cnf_semantics_monotonous_in_cnf_subsets_if[OF assms(2)
        is_cnf_encode_problem_with_operator_interference_exclusion[OF assms(1)]
        cnf_of_encode_problem_with_operator_interference_exclusion_structure(5)].
    hence "clause_semantics 𝒜 C"
      unfolding cnf_semantics_def
      using C_in
      by fast
  } note nb1 = this
  {
    fix op1 op2
    assume "op1 ∈ set ?πk" and "op2 ∈ set ?πk"
      and index_op1_is_not_index_op2: "index ?ops op1 ≠ index ?ops op2"
    moreover have op1_in: "op1 ∈ set ?ops" and 𝒜_models_op1:"𝒜 (Operator k (index ?ops op1))"
      and op2_in: "op2 ∈ set ?ops" and 𝒜_models_op2: "𝒜 (Operator k (index ?ops op2))"
      using decode_plan_step_element_then[OF assms(3)] calculation
      unfolding decode_plan_def
      by blast+
    moreover {
      let ?C = "{ (Operator k (index ?ops op1))¯, (Operator k (index ?ops op2))¯ }"
      assume "are_operators_interfering op1 op2"
      moreover have "?C ∈ cnf ?ΦX"
        using cnf_of_encode_interfering_operator_exclusion_contains_clause_if[OF
            assms(3) op1_in op2_in index_op1_is_not_index_op2] calculation
        by blast
      moreover have "¬clause_semantics 𝒜 ?C"
        using 𝒜_models_op1 𝒜_models_op2
        unfolding clause_semantics_def
        by auto
      ultimately have False
        using nb1
        by blast
    }
    ultimately have "¬are_operators_interfering op1 op2"
      by blast
  } note nb3 = this
  show ?thesis
    using assms
    proof (induction ops)
      case (Cons op1 ops)
      have "are_all_operators_non_interfering ops"
        using Cons.IH[OF Cons.prems(1, 2, 3) Cons_in_subseqsD[OF Cons.prems(4)]]
        by blast
      moreover {
        fix op2
        assume op2_in_ops: "op2 ∈ set ops"
        moreover have op1_in_πk: "op1 ∈ set ?πk" and op2_in_πk: "op2 ∈ set ?πk"
          using element_of_subseqs_then_subset[OF Cons.prems(4)] calculation(1)
          by auto+
        moreover
        {
          have "distinct (op1 # ops)"
            using subseqs_distinctD[OF Cons.prems(4)]
              decode_plan_step_distinct[OF Cons.prems(3)]
            unfolding decode_plan_def
            by blast
          moreover have "op1 ∈ set ?ops" and "op2 ∈ set ?ops"
            using decode_plan_step_element_then(1)[OF Cons.prems(3)] op1_in_πk op2_in_πk
            unfolding decode_plan_def
            by force+
          moreover have "op1 ≠ op2"
            using op2_in_ops calculation(1)
            by fastforce
          ultimately have "index ?ops op1 ≠ index ?ops op2"
            using index_eq_index_conv
            by auto
        }
        ultimately have "¬are_operators_interfering op1 op2"
          using nb3
          by blast
      }
      ultimately show ?case
        using list_all_iff
        by auto
    qed simp
qed

theorem encode_problem_serializable_sound:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ∀ Π t"
  shows "is_parallel_solution_for_problem Π (Φ¯ Π 𝒜 t)"
    and "∀k < length (Φ¯ Π 𝒜 t). are_all_operators_non_interfering ((Φ¯ Π 𝒜 t) ! k)"
proof -
  {
    have "𝒜 ⊨ SAT_Plan_Base.encode_initial_state Π"
      and "𝒜 ⊨ SAT_Plan_Base.encode_operators Π t"
      and "𝒜 ⊨ SAT_Plan_Base.encode_all_frame_axioms Π t"
      and "𝒜 ⊨ SAT_Plan_Base.encode_goal_state Π t"
      using assms(2)
      unfolding encode_problem_with_operator_interference_exclusion_def
      by simp+
    then have "𝒜 ⊨ SAT_Plan_Base.encode_problem Π t"
      unfolding SAT_Plan_Base.encode_problem_def
      by simp
  }
  thus "is_parallel_solution_for_problem Π (Φ¯ Π 𝒜 t)"
    using encode_problem_parallel_sound assms(1, 2)
    unfolding decode_plan_def
    by blast
next
  let ?π = "Φ¯ Π 𝒜 t"
  {
    fix k
    assume "k < t"
    moreover have "?π ! k ∈ set (subseqs (?π ! k))"
      using subseqs_refl
      by blast
    ultimately have "are_all_operators_non_interfering (?π ! k)"
      using encode_problem_serializable_sound_i[OF assms]
      unfolding SAT_Plan_Base.decode_plan_def decode_plan_def
      by blast
  }
  moreover have "length ?π = t"
    unfolding SAT_Plan_Base.decode_plan_def decode_plan_def
    by simp
  ultimately show "∀k < length ?π. are_all_operators_non_interfering (?π ! k)"
    by simp
qed


subsection "Completeness"


lemma encode_problem_with_operator_interference_exclusion_complete_i:
  assumes "is_valid_problem_strips Π"
    and "is_parallel_solution_for_problem Π π"
    and "∀k < length π. are_all_operators_non_interfering (π ! k)"
  shows "valuation_for_plan Π π ⊨ encode_interfering_operator_exclusion Π (length π)"
proof -
  let ?𝒜 = "valuation_for_plan Π π"
    and ?ΦX = "encode_interfering_operator_exclusion Π (length π)"
    and ?ops = "strips_problem.operators_of Π"
    and ?t = "length π"
  let ?τ = "trace_parallel_plan_strips ((Π)I) π"
  let ?Ops = "{ (op1, op2). (op1, op2) ∈ set (operators_of Π) × set (operators_of Π)
    ∧ index ?ops op1 ≠ index ?ops op2
    ∧ are_operators_interfering op1 op2 }"
    and ?f = "λ(op1, op2). {{{ (Operator k (index ?ops op1))¯, (Operator k (index ?ops op2))¯ }}
      | k. k ∈ {0..<length π} }"
  let ?A = "⋃(?f ` ?Ops)"
  let ?B = "⋃?A"
  have nb1: "∀ops ∈ set π. ∀op ∈ set ops. op ∈ set (operators_of Π)"
    using is_parallel_solution_for_problem_operator_set[OF assms(2)]
    unfolding operators_of_def
    by blast
  (* TODO refactor (characterization of 𝒜) *)
  {
    fix k op
    assume "k < length π" and "op ∈ set (π ! k)"
    hence "lit_semantics ?𝒜 ((Operator k (index ?ops op))+) = (k < length ?τ - 1)"
      using encode_problem_parallel_complete_vi_a[OF assms(2)]
        encode_problem_parallel_complete_vi_b[OF assms(2)] initial_of_def
      by(cases "k < length ?τ - 1"; simp)
  } note nb2 = this
  {
    fix k op1 op2
    assume "k < length π"
      and "op1 ∈ set (π ! k)"
      and "index ?ops op1 ≠ index ?ops op2"
      and "are_operators_interfering op1 op2"
    moreover have "are_all_operators_non_interfering (π ! k)"
      using assms(3) calculation(1)
      by blast
    moreover have "op1 ≠ op2"
      using calculation(3)
      by blast
    ultimately have "op2 ∉ set (π ! k)"
      using are_all_operators_non_interfering_set_contains_no_distinct_interfering_operator_pairs
        assms(3)
      by blast
  } note nb3 = this
  {
    fix C
    assume "C ∈ cnf ?ΦX"
    then have "C ∈ ?B"
      using cnf_of_encode_interfering_operator_exclusion_is[of Π "length π"]
      by argo
    then obtain C' where "C' ∈ ?A" and C_in: "C ∈ C'"
      using Union_iff[of C ?A]
      by meson
    then obtain op1 op2 where "(op1, op2) ∈ set (operators_of Π) × set (operators_of Π)"
      and index_op1_is_not_index_op2: "index ?ops op1 ≠ index ?ops op2"
      and are_operators_interfering_op1_op2: "are_operators_interfering op1 op2"
      and C'_in: "C' ∈ {{{(Operator k (index ?ops op1))¯, (Operator k (index ?ops op2))¯}}
        | k. k ∈ {0..<length π}}"
      using UN_iff[of C' ?f ?Ops]
      by blast
    then obtain k where "k ∈ {0..<length π}"
      and C_is: "C = { (Operator k (index ?ops op1))¯, (Operator k (index ?ops op2))¯ }"
      using C_in C'_in
      by blast
    then have k_lt_length_π: "k < length π"
      by simp
    consider (A) "op1 ∈ set (π ! k)"
     | (B) "op2 ∈ set (π ! k)"
     | (C) "¬op1 ∈ set (π ! k) ∨ ¬op2 ∈ set (π ! k)"
      by linarith
    hence "clause_semantics ?𝒜 C"
      proof (cases)
        case A
        moreover have "op2 ∉ set (π ! k)"
          using nb3 k_lt_length_π calculation index_op1_is_not_index_op2 are_operators_interfering_op1_op2
          by blast
        moreover have "¬?𝒜 (Operator k (index ?ops op2))"
          using encode_problem_parallel_complete_vi_d[OF assms(2) k_lt_length_π]
            calculation(2)
          by blast
        ultimately show ?thesis
          using C_is
          unfolding clause_semantics_def
          by force
      next
        case B
        moreover have "op1 ∉ set (π ! k)"
          using nb3 k_lt_length_π calculation index_op1_is_not_index_op2 are_operators_interfering_op1_op2
          by blast
        moreover have "¬?𝒜 (Operator k (index ?ops op1))"
          using encode_problem_parallel_complete_vi_d[OF assms(2) k_lt_length_π]
            calculation(2)
          by blast
        ultimately show ?thesis
          using C_is
          unfolding clause_semantics_def
          by force
      next
        case C
        then show ?thesis
          proof (rule disjE)
            assume "op1 ∉ set (π ! k)"
            then have "¬?𝒜 (Operator k (index ?ops op1))"
              using encode_problem_parallel_complete_vi_d[OF assms(2) k_lt_length_π]
              by blast
            thus "clause_semantics (valuation_for_plan Π π) C"
              using C_is
              unfolding clause_semantics_def
              by force
          next
            assume "op2 ∉ set (π ! k)"
            then have "¬?𝒜 (Operator k (index ?ops op2))"
              using encode_problem_parallel_complete_vi_d[OF assms(2) k_lt_length_π]
              by blast
            thus "clause_semantics (valuation_for_plan Π π) C"
              using C_is
              unfolding clause_semantics_def
              by force
          qed
      qed
  }
  then have "cnf_semantics ?𝒜 (cnf ?ΦX)"
    unfolding cnf_semantics_def..
  thus ?thesis
    using cnf_semantics[OF is_nnf_cnf[OF is_cnf_encode_interfering_operator_exclusion]]
    by fast
qed

text ‹ Similar to the soundness proof, we may reuse the previously established
facts about the valuation for the completeness proof of the basic SATPlan encoding
(\ref{isathm:completeness-satplan-encoding}).
To make it clearer why this is true we have a look at the form of the clauses for interfering operator
pairs term‹op1› and term‹op2› at the same time index term‹k› which have the form shown below:
  @{text[display, indent=4] "{ (Operator k (index ops op1))¯, (Operator k (index ops op2))¯ }"}
where term‹ops ≡ strips_problem.operators_of Π›.
Now, consider an operator term‹op1› that is contained in the term‹k›-th plan step term‹π ! k›
(symmetrically for term‹op2›). Since term‹π› is a serializable solution, there can be no
interference between term‹op1› and term‹op2› at time term‹k›. Hence term‹op2› cannot be in term‹π ! k›
This entails that for term‹𝒜 ≡ valuation_for_plan Π π› it holds that
  @{text[display, indent=4] "𝒜 ⊨ ¬ Atom (Operator k (index ops op2))"}
and term‹𝒜› therefore models the clause.

Furthermore, if neither is present, than term‹𝒜› will evaluate both atoms to false and the clause
therefore evaluates to true as well.

It follows from this that each clause in the extension of the SATPlan encoding evaluates to true
for term‹𝒜›. The other parts of the encoding evaluate to true as per the completeness of the
basic SATPlan encoding (theorem \ref{isathm:completeness-satplan-encoding}).›

theorem encode_problem_serializable_complete:
  assumes "is_valid_problem_strips Π"
    and "is_parallel_solution_for_problem Π π"
    and "∀k < length π. are_all_operators_non_interfering (π ! k)"
  shows "valuation_for_plan Π π ⊨ Φ∀ Π (length π)"
proof -
  let ?𝒜 = "valuation_for_plan Π π"
    and ?ΦX = "encode_interfering_operator_exclusion Π (length π)"
  have "?𝒜 ⊨ SAT_Plan_Base.encode_problem Π (length π)"
    using assms(1, 2) encode_problem_parallel_complete
    by auto
  moreover have "?𝒜 ⊨ ?ΦX"
    using encode_problem_with_operator_interference_exclusion_complete_i[OF assms].
  ultimately show ?thesis
    unfolding encode_problem_with_operator_interference_exclusion_def encode_problem_def
      SAT_Plan_Base.encode_problem_def
    by force
qed

value  "stop" (* Tell document preparation to stop collecting for the last tag *)

(* TODO rename encode_problem_with_operator_interference_exclusion_decoded_plan_is_serializable_i *)
lemma encode_problem_forall_step_decoded_plan_is_serializable_i:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ∀ Π t"
  shows "(Π)G ⊆m execute_serial_plan ((Π)I) (concat (Φ¯ Π 𝒜 t))"
proof -
  let ?G = "(Π)G"
    and ?I = "(Π)I"
    and ?π = "Φ¯ Π 𝒜 t"
  let ?π' = "concat (Φ¯ Π 𝒜 t)"
    and ?τ = "trace_parallel_plan_strips ?I ?π"
    and ?σ = "map (decode_state_at Π 𝒜) [0..<Suc (length ?π)]"
  {
    fix k
    assume k_lt_length_π: "k < length ?π"
    moreover have "𝒜 ⊨ SAT_Plan_Base.encode_problem Π t"
      using assms(2)
      unfolding encode_problem_with_operator_interference_exclusion_def
        encode_problem_def SAT_Plan_Base.encode_problem_def
      by simp
    moreover have "length ?σ = length ?τ"
      using encode_problem_parallel_correct_vii assms(1) calculation
      unfolding decode_state_at_def decode_plan_def initial_of_def
      by fast
    ultimately have "k < length ?τ - 1" and "k < t"
      unfolding decode_plan_def SAT_Plan_Base.decode_plan_def
      by force+
  } note nb = this
  {
    have "?G ⊆m execute_parallel_plan ?I ?π"
      using encode_problem_serializable_sound assms
      unfolding is_parallel_solution_for_problem_def decode_plan_def
        goal_of_def initial_of_def
      by blast
    hence "?G ⊆m last (trace_parallel_plan_strips ?I ?π)"
      using execute_parallel_plan_reaches_goal_iff_goal_is_last_element_of_trace
      by fast
  }
  moreover {
    fix k
    assume k_lt_length_π: "k < length ?π"
    moreover have "k < length ?τ - 1" and "k < t"
      using nb calculation
      by blast+
    moreover have "are_all_operators_applicable (?τ ! k) (?π ! k)"
      and "are_all_operator_effects_consistent (?π ! k)"
      using trace_parallel_plan_strips_operator_preconditions calculation(2)
      by blast+
    moreover have "are_all_operators_non_interfering (?π ! k)"
      using encode_problem_serializable_sound(2)[OF assms(1, 2)] k_lt_length_π
      by blast
    ultimately have "are_all_operators_applicable (?τ ! k) (?π ! k)"
      and "are_all_operator_effects_consistent (?π ! k)"
      and "are_all_operators_non_interfering (?π ! k)"
      by blast+
  }
  ultimately show ?thesis
    using execute_parallel_plan_is_execute_sequential_plan_if assms(1)
    by metis
qed

(* TODO rename encode_problem_with_operator_interference_exclusion_decoded_plan_is_serializable_ii *)
lemma encode_problem_forall_step_decoded_plan_is_serializable_ii:
  (* TODO why is the fixed type necessary? *)
  fixes Π :: "'variable strips_problem"
  shows "list_all (λop. ListMem op (strips_problem.operators_of Π))
    (concat (Φ¯ Π 𝒜 t))"
proof -
  let ?π = "Φ¯ Π 𝒜 t"
  let ?π' = "concat ?π"
  (* TODO refactor *)
  {
    have "set ?π' = ⋃(set `  (⋃k < t. { decode_plan' Π 𝒜 k }))"
      unfolding decode_plan_def decode_plan_set_is set_concat
      by auto
    also have "… = ⋃(⋃k < t. { set (decode_plan' Π 𝒜 k) })"
      by blast
    finally have "set ?π' = (⋃k < t. set (decode_plan' Π 𝒜 k))"
      by blast
  } note nb = this
  {
    fix op
    assume "op ∈ set ?π'"
    then obtain k where "k < t" and "op ∈ set (decode_plan' Π 𝒜 k)"
      using nb
      by blast
    moreover have "op ∈ set (decode_plan Π 𝒜 t ! k)"
      using calculation
      unfolding decode_plan_def SAT_Plan_Base.decode_plan_def
      by simp
    ultimately have "op ∈ set (operators_of Π)"
      using decode_plan_step_element_then(1)
      unfolding operators_of_def decode_plan_def
      by blast
  }
  thus ?thesis
    unfolding list_all_iff ListMem_iff operators_of_def
    by blast
qed

text ‹ Given the soundness and completeness of the SATPlan encoding with interfering operator
exclusion term‹Φ∀ Π t›, we can
now conclude this part with showing that for a parallel plan term‹π ≡ Φ¯ Π 𝒜 t›
that was decoded from a model term‹𝒜› of term‹Φ∀ Π t› the serialized plan
term‹π' ≡ concat π› is a serial solution for term‹Π›. To this end, we have to show that
\begin{itemize}
  \item the state reached by serial execution of term‹π'› subsumes term‹G›, and
  \item all operators in term‹π'› are operators contained in term‹𝒪›.
\end{itemize}
While the proof of the latter step is rather straight forward, the proof for the
former requires a bit more work. We use the previously established theorem on serial and parallel
STRIPS equivalence (theorem \ref{isathm:equivalence-parallel-serial-strips-plans}) to show the
serializability of term‹π› and therefore have to show that term‹G› is subsumed by the last state
of the trace of term‹π'›
  @{text[display, indent=4] "G ⊆m last (trace_sequential_plan_strips I π')"}
and moreover that at every step of the parallel plan execution, the parallel operator execution
condition as well as non interference are met
  @{text[display, indent=4] "∀k < length π. are_all_operators_non_interfering (π ! k)"}.
\footnote{These propositions are shown in lemmas \texttt{encode\_problem\_forall\_step\_decoded\_plan\_is\_serializable\_ii} and
\texttt{encode\_problem\_forall\_step\_decoded\_plan\_is\_serializable\_i} which have been omitted for
brevity.}
Note that the parallel operator execution condition is implicit in the existence of the parallel
trace for term‹π› with
  @{text[display, indent=4] "G ⊆m last (trace_parallel_plan_strips I π)"}
warranted by the soundness of term‹Φ∀ Π t›. ›

(* TODO rename encode_problem_with_operator_interference_exclusion_decoded_plan_is_serializable *)
theorem serializable_encoding_decoded_plan_is_serializable:
  assumes "is_valid_problem_strips Π"
    and "𝒜 ⊨ Φ∀ Π t"
  shows "is_serial_solution_for_problem Π (concat (Φ¯ Π 𝒜 t))"
  using encode_problem_forall_step_decoded_plan_is_serializable_i[OF assms]
    encode_problem_forall_step_decoded_plan_is_serializable_ii
  unfolding is_serial_solution_for_problem_def goal_of_def
    initial_of_def decode_plan_def
  by blast

end