Theory SAS_Plus_Semantics

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory SAS_Plus_Semantics  
  imports "SAS_Plus_Representation" "List_Supplement"
    "Map_Supplement"
begin
section "SAS+ Semantics"


subsection "Serial Execution Semantics"

text ‹ Serial plan execution is implemented recursively just like in the STRIPS case. By and large, 
compared to definition \ref{isadef:plan-execution-strips}, we only substitute the operator 
applicability function with its SAS+ counterpart. ›

primrec execute_serial_plan_sas_plus
  where "execute_serial_plan_sas_plus s [] = s"
  | "execute_serial_plan_sas_plus s (op # ops) 
    = (if is_operator_applicable_in s op 
    then execute_serial_plan_sas_plus (execute_operator_sas_plus s op) ops
    else s)" 

text ‹ Similarly, serial SAS+ solutions are defined just like in STRIPS but based on the 
corresponding SAS+ definitions. ›

definition is_serial_solution_for_problem
  :: "('variable, 'domain) sas_plus_problem  ('variable, 'domain) sas_plus_plan  bool" 
  where "is_serial_solution_for_problem Ψ ψ
     let 
        I = sas_plus_problem.initial_of Ψ
        ; G = sas_plus_problem.goal_of Ψ
        ; ops = sas_plus_problem.operators_of Ψ
      in G m execute_serial_plan_sas_plus I ψ
         list_all (λop. ListMem op ops) ψ" 


context
begin

private lemma execute_operator_sas_plus_effect_i:
  assumes "is_operator_applicable_in s op"
    and "(v, a)  set (effect_of op). (v', a')  set (effect_of op).
      v  v'  a = a'"
    and"(v, a)  set (effect_of op)"
  shows "(s + op) v = Some a"
proof -
  let ?effect = "effect_of op"
  have "map_of ?effect v = Some a" 
    using map_of_constant_assignments_defined_if[OF assms(2, 3)] try0
    by blast
  thus ?thesis 
    unfolding execute_operator_sas_plus_def map_add_def
    by fastforce
qed
    
private lemma  execute_operator_sas_plus_effect_ii:
  assumes "is_operator_applicable_in s op"
    and "(v', a')  set (effect_of op). v'  v"
  shows "(s + op) v = s v"
proof -
  let ?effect = "effect_of op" 
  {
    have "v  fst ` set ?effect" 
      using assms(2)
      by fastforce
    then have "v  dom (map_of ?effect)"
      using dom_map_of_conv_image_fst[of ?effect]
      by argo
    hence "(s ++ map_of ?effect) v = s v" 
      using map_add_dom_app_simps(3)[of v "map_of ?effect" s]
      by blast
  }
  thus ?thesis 
    by fastforce
qed

text ‹ Given an operator termop that is applicable in a state terms and has a consistent set 
of effects (second assumption) we can now show that the successor state terms'  s + op 
has the following properties:
\begin{itemize}
  \item terms' v = Some a if term(v, a) exist in termset (effect_of op); and,
  \item terms' v = s v if no term(v, a') exist in termset (effect_of op).
\end{itemize} 
The second property is the case if the operator doesn't have an effect for a variable termv. ›

theorem execute_operator_sas_plus_effect:
  assumes "is_operator_applicable_in s op"
    and "(v, a)  set (effect_of op). 
      (v', a')  set (effect_of op). v  v'  a = a'"
  shows "(v, a)  set (effect_of op) 
       (s + op) v = Some a"
    and "(a. (v, a)  set (effect_of op)) 
       (s + op) v = s v"
proof -
  show "(v, a)  set (effect_of op) 
     (s + op) v = Some a" 
    using execute_operator_sas_plus_effect_i[OF assms(1, 2)]
    by blast
next 
  show "(a. (v, a)  set (effect_of op)) 
     (s + op) v = s v" 
    using execute_operator_sas_plus_effect_ii[OF assms(1)]
    by blast
qed

end


subsection "Parallel Execution Semantics"

― ‹ Define a type synonym for \emph{SAS+ parallel plans} and add a definition lifting SAS+
operator applicability to parallel plans. ›

type_synonym ('variable, 'domain) sas_plus_parallel_plan 
  = "('variable, 'domain) sas_plus_operator list list" 
    
definition are_all_operators_applicable_in
  :: "('variable, 'domain) state 
     ('variable, 'domain) sas_plus_operator list
     bool"
  where "are_all_operators_applicable_in s ops 
     list_all (is_operator_applicable_in s) ops"

definition are_operator_effects_consistent
  :: "('variable, 'domain) sas_plus_operator
     ('variable, 'domain) sas_plus_operator
     bool"
  where "are_operator_effects_consistent op op' 
     let 
        effect = effect_of op
        ; effect' = effect_of op'
      in list_all (λ(v, a). list_all (λ(v', a'). v  v'  a = a') effect') effect"

definition are_all_operator_effects_consistent
  :: "('variable, 'domain) sas_plus_operator list
     bool"
  where "are_all_operator_effects_consistent ops 
     list_all (λop. list_all (are_operator_effects_consistent op) ops) ops"   

definition execute_parallel_operator_sas_plus
  :: "('variable, 'domain) state 
     ('variable, 'domain) sas_plus_operator list 
     ('variable, 'domain) state"
  where "execute_parallel_operator_sas_plus s ops 
     foldl (++) s (map (map_of  effect_of) ops)" 

text ‹ We now define parallel execution and parallel traces for SAS+ by lifting the tests for 
applicability and effect consistency to parallel SAS+ operators. The definitions are again very
similar to their STRIPS analogs (definitions \ref{isadef:parallel-plan-execution-strips} and 
\ref{isadef:parallel-plan-trace-strips}). ›

fun execute_parallel_plan_sas_plus
  :: "('variable, 'domain) state 
     ('variable, 'domain) sas_plus_parallel_plan
     ('variable, 'domain) state" 
  where "execute_parallel_plan_sas_plus s [] = s"
  | "execute_parallel_plan_sas_plus s (ops # opss) = (if 
      are_all_operators_applicable_in s ops 
       are_all_operator_effects_consistent ops
    then execute_parallel_plan_sas_plus 
      (execute_parallel_operator_sas_plus s ops) opss
    else s)"

fun trace_parallel_plan_sas_plus
  :: "('variable, 'domain) state  
     ('variable, 'domain) sas_plus_parallel_plan 
     ('variable, 'domain) state list"
  where "trace_parallel_plan_sas_plus s [] = [s]"
  | "trace_parallel_plan_sas_plus s (ops # opss) = s # (if 
      are_all_operators_applicable_in s ops 
       are_all_operator_effects_consistent ops
    then trace_parallel_plan_sas_plus 
      (execute_parallel_operator_sas_plus s ops) opss
    else [])"

text ‹ A plan termψ is a solution for a SAS+ problem termΨ if 
\begin{enumerate}
  \item starting from the initial state termΨ, SAS+ parallel plan execution 
    reaches a state which satisfies the described goal state termsas_plus_problem.goal_of Ψ; and,
  \item all parallel operators termops in the plan termψ only consist of operators that
    are specified in the problem description.
\end{enumerate} ›
definition is_parallel_solution_for_problem 
  :: "('variable, 'domain) sas_plus_problem 
     ('variable, 'domain) sas_plus_parallel_plan 
     bool"
  where "is_parallel_solution_for_problem Ψ ψ 
     let 
        G = sas_plus_problem.goal_of Ψ
        ; I = sas_plus_problem.initial_of Ψ
        ; Ops = sas_plus_problem.operators_of Ψ
      in G m execute_parallel_plan_sas_plus I ψ
       list_all (λops. list_all (λop. ListMem op Ops) ops) ψ" 

context 
begin

lemma execute_parallel_operator_sas_plus_cons[simp]:
  "execute_parallel_operator_sas_plus s (op # ops)
    = execute_parallel_operator_sas_plus (s ++  map_of (effect_of op)) ops" 
  unfolding execute_parallel_operator_sas_plus_def
  by simp

text ‹The following lemmas show the properties of SAS+ parallel plan execution traces. 
The results are analogous to those for STRIPS. So, let termτ  trace_parallel_plan_sas_plus I ψ 
be a trace of a parallel SAS+ plan termψ with initial state termI, then
\begin{itemize}
  \item the head of the trace termτ ! 0 is the initial state of the 
problem (lemma \ref{isathm:head-parallel-plan-trace-sas-plus}); moreover,
  \item for all but the last element of the trace---i.e. elements with index 
termk < length τ - 1---the parallel operator termπ ! k is executable (lemma 
\ref{isathm:parallel-plan-trace-operator-execution-conditions-sas-plus}); and 
finally, 
  \item for all termk < length τ, the parallel execution of the plan prefix termtake k ψ with 
initial state termI equals the termk-th element of the trace termτ ! k (lemma 
\ref{isathm:parallel-trace-plan-prefixes-sas-plus}).
\end{itemize} ›

(* TODO? Make invisible? *)
lemma trace_parallel_plan_sas_plus_head_is_initial_state: 
  "trace_parallel_plan_sas_plus I ψ ! 0 = I"
proof (cases ψ)
  case (Cons a list)
  then show ?thesis 
    by (cases "are_all_operators_applicable_in I a  are_all_operator_effects_consistent a"; 
        simp+)
qed simp

lemma trace_parallel_plan_sas_plus_length_gt_one_if:
  assumes "k < length (trace_parallel_plan_sas_plus I ψ) - 1"  
  shows "1 < length (trace_parallel_plan_sas_plus I ψ)" 
  using assms
  by linarith
    
lemma length_trace_parallel_plan_sas_plus_lte_length_plan_plus_one:
  shows "length (trace_parallel_plan_sas_plus I ψ)  length ψ + 1" 
proof (induction ψ arbitrary: I)
  case (Cons a ψ)
  then show ?case 
    proof (cases "are_all_operators_applicable_in I a  are_all_operator_effects_consistent a")
      case True
      let ?I' = "execute_parallel_operator_sas_plus I a" 
      {
        have "trace_parallel_plan_sas_plus I (a # ψ) = I # trace_parallel_plan_sas_plus ?I' ψ" 
          using True
          by auto
        then have "length (trace_parallel_plan_sas_plus I (a # ψ)) 
          = length (trace_parallel_plan_sas_plus ?I' ψ) + 1"
          by simp
        moreover have "length (trace_parallel_plan_sas_plus ?I' ψ)  length ψ + 1"
          using Cons.IH[of ?I']
          by blast
        ultimately have "length (trace_parallel_plan_sas_plus I (a # ψ))  length (a # ψ) + 1"
          by simp
      }
      thus ?thesis
        by blast
    qed auto
qed simp
    
lemma plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements:
  assumes "k < length (trace_parallel_plan_sas_plus I ψ) - 1" 
  obtains ops ψ' where "ψ = ops # ψ'" 
proof -
  let  = "trace_parallel_plan_sas_plus I ψ"
  have "length   length ψ + 1" 
    using length_trace_parallel_plan_sas_plus_lte_length_plan_plus_one
    by fast
  then have "0 < length ψ"
    using trace_parallel_plan_sas_plus_length_gt_one_if[OF assms]
    by fastforce
  then obtain k' where "length ψ = Suc k'"
    using gr0_implies_Suc
    by meson
  thus ?thesis using that  
    using length_Suc_conv[of ψ k']
    by blast
qed

lemma trace_parallel_plan_sas_plus_step_implies_operator_execution_condition_holds:
  assumes "k < length (trace_parallel_plan_sas_plus I π) - 1"
  shows "are_all_operators_applicable_in (trace_parallel_plan_sas_plus I π ! k) (π ! k)
       are_all_operator_effects_consistent (π ! k)"
using assms 
proof  (induction "π" arbitrary: I k)
  ― ‹ NOTE Base case yields contradiction with assumption and can be left to automation. ›
  case (Cons a π)
  then show ?case 
    proof (cases "are_all_operators_applicable_in I a  are_all_operator_effects_consistent a")
      case True
      have trace_parallel_plan_sas_plus_cons: "trace_parallel_plan_sas_plus I (a # π) 
        = I # trace_parallel_plan_sas_plus (execute_parallel_operator_sas_plus I a) π"
        using True
        by simp  
      then show ?thesis 
      proof (cases "k")
        case 0
        have "trace_parallel_plan_sas_plus I (a # π) ! 0 = I" 
          using trace_parallel_plan_sas_plus_cons
          by simp
        moreover have "(a # π) ! 0 = a"
          by simp
        ultimately show ?thesis 
          using True 0
          by presburger
      next
        case (Suc k')
        have "trace_parallel_plan_sas_plus I (a # π) ! Suc k' 
          = trace_parallel_plan_sas_plus (execute_parallel_operator_sas_plus I a) π ! k'" 
          using trace_parallel_plan_sas_plus_cons
          by simp
        moreover have "(a # π) ! Suc k' = π ! k'"
          by simp
        moreover {
          let ?I' = "execute_parallel_operator_sas_plus I a"
          have "length (trace_parallel_plan_sas_plus I (a # π)) 
            = 1 + length (trace_parallel_plan_sas_plus ?I' π)" 
            using trace_parallel_plan_sas_plus_cons 
            by auto
          then have "k' < length (trace_parallel_plan_sas_plus ?I' π) - 1" 
            using Cons.prems Suc
            unfolding Suc_eq_plus1
            by fastforce
          hence "are_all_operators_applicable_in
            (trace_parallel_plan_sas_plus (execute_parallel_operator_sas_plus I a) π ! k')
            (π ! k') 
           are_all_operator_effects_consistent (π ! k')"
            using Cons.IH[of k' "execute_parallel_operator_sas_plus I a"] Cons.prems Suc trace_parallel_plan_sas_plus_cons
            by simp
        }
        ultimately show ?thesis 
          using Suc
          by argo
      qed 
    next
      case False
      then have "trace_parallel_plan_sas_plus I (a # π) = [I]"
        by force
      then have "length (trace_parallel_plan_sas_plus I (a # π)) - 1 = 0" 
        by simp
      ― ‹ NOTE Thesis follows from contradiction with assumption. ›
      then show ?thesis 
        using Cons.prems
        by force 
    qed
qed auto

lemma trace_parallel_plan_sas_plus_prefix:
  assumes "k < length (trace_parallel_plan_sas_plus I ψ)"
  shows "trace_parallel_plan_sas_plus I ψ ! k = execute_parallel_plan_sas_plus I (take k ψ)" 
  using assms
proof  (induction ψ arbitrary: I k)
  case (Cons a ψ)
  then show ?case 
    proof (cases "are_all_operators_applicable_in I a  are_all_operator_effects_consistent a")
      case True
      let  = "trace_parallel_plan_sas_plus I (a # ψ)"
        and ?I' = "execute_parallel_operator_sas_plus I a" 
      have σ_equals: " = I # trace_parallel_plan_sas_plus ?I' ψ" 
        using True
        by auto
      then show ?thesis 
        proof (cases "k = 0")
          case False
          obtain k' where k_is_suc_of_k': "k = Suc k'" 
            using not0_implies_Suc[OF False]
            by blast
          then have "execute_parallel_plan_sas_plus I (take k (a # ψ))
            = execute_parallel_plan_sas_plus ?I' (take k' ψ)" 
            using True
            by simp
          moreover have "trace_parallel_plan_sas_plus I (a # ψ) ! k 
            = trace_parallel_plan_sas_plus ?I' ψ ! k'" 
            using σ_equals k_is_suc_of_k'
            by simp
          moreover {
            have "k' < length (trace_parallel_plan_sas_plus ?I' ψ)"
              using Cons.prems σ_equals k_is_suc_of_k'
              by force
            hence "trace_parallel_plan_sas_plus ?I' ψ ! k' 
              = execute_parallel_plan_sas_plus ?I' (take k' ψ)" 
              using Cons.IH[of k' ?I']
              by blast
          }
          ultimately show ?thesis
            by presburger
        qed simp
    next
      case operator_precondition_violated: False
      then show ?thesis 
      proof (cases "k = 0")
        case False
        then have "trace_parallel_plan_sas_plus I (a # ψ) = [I]"
          using operator_precondition_violated
          by force
        moreover have "execute_parallel_plan_sas_plus I (take k (a # ψ)) = I" 
          using Cons.prems operator_precondition_violated 
          by force
        ultimately show ?thesis 
          using Cons.prems nth_Cons_0
          by auto
      qed simp
    qed
qed simp

lemma trace_parallel_plan_sas_plus_step_effect_is:
  assumes "k < length (trace_parallel_plan_sas_plus I ψ) - 1"
  shows "trace_parallel_plan_sas_plus I ψ ! Suc k 
    = execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus I ψ ! k) (ψ ! k)" 
proof -
  let  = "trace_parallel_plan_sas_plus I ψ"
  let k = " ! k"
    and k' = " ! Suc k"
  ― ‹ NOTE rewrite the goal using the subplan formulation to be able. This allows us to make the 
    initial state arbitrary. ›
  {
    have suc_k_lt_length_τ: "Suc k < length " 
      using assms 
      by linarith
    hence "k' = execute_parallel_plan_sas_plus I (take (Suc k) ψ)"
      using trace_parallel_plan_sas_plus_prefix[of "Suc k"]
      by blast
  } note rewrite_goal = this
  have "execute_parallel_plan_sas_plus I (take (Suc k) ψ) 
    = execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus I ψ ! k) (ψ ! k)" 
    using assms
    proof (induction k arbitrary: I ψ)
      case 0
      obtain ops ψ' where ψ_is: "ψ = ops # ψ'" 
        using plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements[OF "0.prems"] 
        by force
      {
        have "take (Suc 0) ψ  = [ψ ! 0]" 
          using ψ_is
          by simp
        hence "execute_parallel_plan_sas_plus I (take (Suc 0) ψ) 
          = execute_parallel_plan_sas_plus I [ψ ! 0]"
          by argo
      }
      moreover {
        have "trace_parallel_plan_sas_plus I ψ ! 0 = I" 
          using trace_parallel_plan_sas_plus_head_is_initial_state.
        moreover {
          have "are_all_operators_applicable_in I (ψ ! 0)" 
            and "are_all_operator_effects_consistent (ψ ! 0)" 
            using trace_parallel_plan_sas_plus_step_implies_operator_execution_condition_holds[OF
                "0.prems"] calculation 
            by argo+
          then have "execute_parallel_plan_sas_plus I [ψ ! 0] 
            = execute_parallel_operator_sas_plus I (ψ ! 0)"
            by simp
        }
        ultimately have "execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus I ψ ! 0) 
            (ψ ! 0)
          = execute_parallel_plan_sas_plus I [ψ ! 0]"
          by argo
      }
      ultimately show ?case 
        by argo
    next
      case (Suc k)
      obtain ops ψ' where ψ_is: "ψ = ops # ψ'" 
        using plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements[OF Suc.prems]
        by blast
      let ?I' = "execute_parallel_operator_sas_plus I ops"
      have "execute_parallel_plan_sas_plus I (take (Suc (Suc k)) ψ)
        = execute_parallel_plan_sas_plus ?I' (take (Suc k) ψ')" 
        using Suc.prems ψ_is
        by fastforce
      moreover {
        thm Suc.IH[of ]
        have "length (trace_parallel_plan_sas_plus I ψ)
          = 1 + length (trace_parallel_plan_sas_plus ?I' ψ')" 
          using ψ_is Suc.prems
          by fastforce
        moreover have "k < length (trace_parallel_plan_sas_plus ?I' ψ') - 1"
          using Suc.prems calculation
          by fastforce
        ultimately have "execute_parallel_plan_sas_plus ?I' (take (Suc k) ψ') =
          execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus ?I' ψ' ! k) 
          (ψ' ! k)"
          using Suc.IH[of ?I' ψ']
          by blast          
      }
      moreover have "execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus ?I' ψ' ! k) 
          (ψ' ! k)
        = execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus I ψ ! Suc k)
          (ψ ! Suc k)" 
        using Suc.prems ψ_is
        by auto
      ultimately show ?case
        by argo 
    qed 
  thus ?thesis 
    using rewrite_goal
    by argo
qed

text ‹ Finally, we obtain the result corresponding to lemma 
\ref{isathm:parallel-solution-trace-strips} in the SAS+ case: it is equivalent to say that parallel 
SAS+ execution reaches the problem's goal state and that the last element of the corresponding 
trace satisfies the goal state. ›
lemma  execute_parallel_plan_sas_plus_reaches_goal_iff_goal_is_last_element_of_trace:
  "G m execute_parallel_plan_sas_plus I ψ 
     G m last (trace_parallel_plan_sas_plus I ψ)" 
proof   -
  let  = "trace_parallel_plan_sas_plus I ψ" 
  show ?thesis 
  proof (rule iffI)
    assume "G m execute_parallel_plan_sas_plus I ψ"
    thus "G m last " 
      proof (induction ψ arbitrary: I)
        ― ‹ NOTE Base case follows from simplification. ›
        case (Cons ops ψ)
        show ?case
          proof (cases "are_all_operators_applicable_in I ops 
             are_all_operator_effects_consistent ops")
            case True
            let ?s = "execute_parallel_operator_sas_plus I ops"
            {
              have "G m execute_parallel_plan_sas_plus ?s ψ"
                using True Cons.prems
                by simp
              hence "G m last (trace_parallel_plan_sas_plus ?s ψ)" 
                using Cons.IH
                by auto
            }
            moreover {
              have "trace_parallel_plan_sas_plus I (ops # ψ) 
                = I # trace_parallel_plan_sas_plus ?s ψ" 
                using True 
                by simp
              moreover have "trace_parallel_plan_sas_plus ?s ψ  []" 
                using trace_parallel_plan_sas_plus.elims
                by blast 
              ultimately have "last (trace_parallel_plan_sas_plus I (ops # ψ)) 
                = last (trace_parallel_plan_sas_plus ?s ψ)" 
                using last_ConsR
                  by simp
            }
            ultimately show ?thesis 
              by argo
          next
            case False
            then have "G m I"
              using Cons.prems 
              by force
            thus ?thesis
              using False
              by force
          qed
      qed force
  next 
    assume "G m last "
    thus "G m execute_parallel_plan_sas_plus I ψ" 
      proof (induction ψ arbitrary: I)
        case (Cons ops ψ)
        thus ?case
          proof (cases "are_all_operators_applicable_in I ops
             are_all_operator_effects_consistent ops")
            case True
            let ?s = "execute_parallel_operator_sas_plus I ops"
            {
              have "trace_parallel_plan_sas_plus I (ops # ψ) 
                = I # trace_parallel_plan_sas_plus ?s ψ" 
                using True 
                by simp
              moreover have "trace_parallel_plan_sas_plus ?s ψ  []" 
                using trace_parallel_plan_sas_plus.elims
                by blast 
              ultimately have "last (trace_parallel_plan_sas_plus I (ops # ψ)) 
                = last (trace_parallel_plan_sas_plus ?s ψ)" 
                using last_ConsR
                by simp
              hence "G m execute_parallel_plan_sas_plus ?s ψ"
                using Cons.IH[of ?s] Cons.prems 
                by argo
            }
            moreover have "execute_parallel_plan_sas_plus I (ops # ψ) 
                = execute_parallel_plan_sas_plus ?s ψ" 
              using True
              by force
            ultimately show ?thesis 
              by argo
          next
            case False
            have "G m I"
              using Cons.prems False 
              by simp
            thus ?thesis
              using False
              by force
          qed
      qed simp
  qed
qed

lemma is_parallel_solution_for_problem_plan_operator_set:
  (* TODO refactor move + make visible? *)
  fixes Ψ :: "('v, 'd) sas_plus_problem"
  assumes "is_parallel_solution_for_problem Ψ ψ" 
  shows "ops  set ψ. op  set ops. op  set ((Ψ)𝒪+)"
  using assms
  unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff operators_of_def 
  by presburger

end


subsection "Serializable Parallel Plans"

text ‹ Again we want to establish conditions for the serializability of plans. Let
termΨ be a SAS+ problem instance and let termψ be a serial solution. We obtain the following 
two important results, namely that
\begin{enumerate}
  \item the embedding termembed ψ of termψ is a parallel solution for termΨ 
(lemma \ref{isathm:serial-sas-plus-embedding}); and conversely that,
  \item a parallel solution to termΨ that has the form of an embedded serial plan can be 
concatenated to obtain a serial solution (lemma 
\ref{isathm:embedded-serial-solution-flattening-sas-plus}).
\end{enumerate} ›


context
begin

(* TODO refactor *)
lemma execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_i:
  assumes "is_operator_applicable_in s op"
    "are_operator_effects_consistent op op" 
  shows "s + op = execute_parallel_operator_sas_plus s [op]"
proof -
  have "are_all_operators_applicable_in s [op]"
    unfolding are_all_operators_applicable_in_def 
       SAS_Plus_Representation.execute_operator_sas_plus_def
      is_operator_applicable_in_def SAS_Plus_Representation.is_operator_applicable_in_def
      list_all_iff  
    using assms(1) 
    by fastforce
  moreover have "are_all_operator_effects_consistent [op]"
    unfolding are_all_operator_effects_consistent_def list_all_iff
    using assms(2)
    by fastforce
  ultimately show ?thesis
    unfolding execute_parallel_operator_sas_plus_def execute_operator_sas_plus_def
    by simp
qed

lemma execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_ii:
  fixes I :: "('variable, 'domain) state"
  assumes "op  set ψ. are_operator_effects_consistent op op"
    and "G m execute_serial_plan_sas_plus I ψ" 
  shows "G m execute_parallel_plan_sas_plus I (embed ψ)" 
  using assms
proof (induction ψ arbitrary: I)
  case (Cons op ψ)
  show ?case 
    proof (cases "are_all_operators_applicable_in I [op]")
      case True
      let ?J = "execute_operator_sas_plus I op" 
        let ?J' = "execute_parallel_operator_sas_plus I [op]" 
      have "SAS_Plus_Representation.is_operator_applicable_in I op"
        using True 
        unfolding are_all_operators_applicable_in_def list_all_iff
        by force
      moreover have "G m execute_serial_plan_sas_plus ?J ψ" 
        using Cons.prems(2) calculation(1) 
        by simp
      moreover have "are_all_operator_effects_consistent [op]" 
        unfolding are_all_operator_effects_consistent_def list_all_iff Let_def
        using Cons.prems(1)
        by simp
      moreover have "execute_parallel_plan_sas_plus I ([op] # embed ψ) 
        = execute_parallel_plan_sas_plus ?J' (embed ψ)"
        using True calculation(3) 
        by simp
      moreover {
        have "is_operator_applicable_in I op" 
          "are_operator_effects_consistent op op" 
          using True Cons.prems(1)
          unfolding are_all_operators_applicable_in_def 
            SAS_Plus_Representation.is_operator_applicable_in_def list_all_iff 
          by fastforce+
        hence "?J = ?J'" 
          using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_i
            calculation(1) 
          by blast
      }
      ultimately show ?thesis 
        using Cons.IH[of ?J] Cons.prems(1)
        by simp
    next
      case False
      moreover have "¬is_operator_applicable_in I op" 
        using calculation 
        unfolding are_all_operators_applicable_in_def 
          SAS_Plus_Representation.is_operator_applicable_in_def list_all_iff 
        by fastforce
      moreover have "G m I" 
        using Cons.prems(2) calculation(2)
        unfolding is_operator_applicable_in_def
        by simp
      moreover have "execute_parallel_plan_sas_plus I ([op] # embed ψ) = I" 
        using calculation(1)
        by fastforce
      ultimately show ?thesis
        by force
    qed
  qed simp

lemma execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_iii:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "is_serial_solution_for_problem Ψ ψ"
    and "op  set ψ"
  shows "are_operator_effects_consistent op op"
proof -
  have "op  set ((Ψ)𝒪+)"
    using assms(2) assms(3)
    unfolding is_serial_solution_for_problem_def Let_def list_all_iff ListMem_iff 
    by fastforce
  then have "is_valid_operator_sas_plus Ψ op" 
    using is_valid_problem_sas_plus_then(2) assms(1, 3) 
    by auto
  thus ?thesis
    unfolding are_operator_effects_consistent_def Let_def list_all_iff ListMem_iff
    using is_valid_operator_sas_plus_then(6)
    by fast
qed

lemma execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_iv:
  fixes Ψ :: "('v, 'd) sas_plus_problem"
  assumes "op  set ψ. op  set ((Ψ)𝒪+)"
  shows "ops  set (embed ψ). op  set ops. op  set ((Ψ)𝒪+)"
proof -
  let ?ψ' = "embed ψ"
  have nb: "set ?ψ' = { [op] | op. op  set ψ }" 
    by (induction ψ; force)
  {
    fix ops
    assume "ops  set ?ψ'"
    moreover obtain op where "ops = [op]" and "op  set ((Ψ)𝒪+)"
      using assms(1) nb calculation 
      by blast
    ultimately have "op  set ops. op  set ((Ψ)𝒪+)"
      by fastforce
  }
  thus ?thesis..
qed

theorem execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "is_serial_solution_for_problem Ψ ψ" 
  shows "is_parallel_solution_for_problem Ψ (embed ψ)" 
proof  -
  let ?ops = "sas_plus_problem.operators_of Ψ" 
    and ?ψ' = "embed ψ" 
  {
    thm execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_ii[OF]
    have "(Ψ)G+ m execute_serial_plan_sas_plus ((Ψ)I+) ψ"
      using assms(2) 
      unfolding is_serial_solution_for_problem_def Let_def
      by simp
    moreover have "op  set ψ. are_operator_effects_consistent op op" 
      using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_iii[OF assms]..
    ultimately have "(Ψ)G+ m execute_parallel_plan_sas_plus ((Ψ)I+) ?ψ'" 
      using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_ii
      by blast
  }
  moreover {
    have "op  set ψ. op  set ((Ψ)𝒪+)"
      using assms(2) 
      unfolding is_serial_solution_for_problem_def Let_def list_all_iff ListMem_iff
      by fastforce
    hence "ops  set ?ψ'. op  set ops. op  set ((Ψ)𝒪+)" 
      using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_iv
      by blast
  }
  ultimately show ?thesis
    unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff Let_def goal_of_def 
      initial_of_def
    by fastforce
qed

lemma flattening_lemma_i:
  fixes Ψ :: "('v, 'd) sas_plus_problem"
  assumes "ops  set π. op  set ops. op  set ((Ψ)𝒪+)"
  shows "op  set (concat π). op  set ((Ψ)𝒪+)"
proof -
  {
    fix op
    assume "op  set (concat π)" 
    moreover have "op  (ops  set π. set ops)" 
      using calculation
      unfolding set_concat.
    then obtain ops where "ops  set π" and "op  set ops" 
      using UN_iff
      by blast
    ultimately have "op  set ((Ψ)𝒪+)" 
      using assms
      by blast
  }
  thus ?thesis..
qed

lemma flattening_lemma_ii:
  fixes I :: "('variable, 'domain) state"
  assumes "ops  set ψ. op. ops = [op]  is_valid_operator_sas_plus Ψ op " 
    and "G m execute_parallel_plan_sas_plus I ψ" 
  shows "G m execute_serial_plan_sas_plus I (concat ψ)"
proof -
  show ?thesis 
    using assms
    proof (induction ψ arbitrary: I)
      case (Cons ops ψ)
      obtain op where ops_is: "ops = [op]" and is_valid_op: "is_valid_operator_sas_plus Ψ op" 
        using Cons.prems(1)
        by auto
      then show ?case 
        proof (cases "are_all_operators_applicable_in I ops")
          case True
          let ?J = "execute_parallel_operator_sas_plus I [op]" 
            and ?J' = "execute_operator_sas_plus I op" 
          have nb1: "is_operator_applicable_in I op" 
            using True ops_is
            unfolding are_all_operators_applicable_in_def is_operator_applicable_in_def 
              list_all_iff 
            by force
          have nb2: "are_operator_effects_consistent op op" 
            unfolding are_operator_effects_consistent_def list_all_iff Let_def 
            using is_valid_operator_sas_plus_then(6)[OF is_valid_op]
            by blast
          have "are_all_operator_effects_consistent ops" 
            using ops_is 
            unfolding are_all_operator_effects_consistent_def list_all_iff
            using nb2
            by force
          moreover have "G m execute_parallel_plan_sas_plus ?J ψ"
            using Cons.prems(2) True calculation ops_is
            by fastforce
          moreover have "execute_serial_plan_sas_plus I (concat (ops # ψ)) 
              = execute_serial_plan_sas_plus ?J' (concat ψ)"
              using ops_is nb1 is_operator_applicable_in_def
              by simp
          moreover have "?J = ?J'" 
            using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_i[OF nb1 nb2]
            by simp
          ultimately show ?thesis
            using Cons.IH[of ?J] Cons.prems(1)
            by force
        next
          case False
          moreover have "G m I" 
            using Cons.prems(2) calculation
            by fastforce
          moreover {
            have "¬is_operator_applicable_in I op" 
              using False ops_is
              unfolding are_all_operators_applicable_in_def 
                is_operator_applicable_in_def list_all_iff
              by force
            moreover have "execute_serial_plan_sas_plus I (concat (ops # ψ)) 
              = execute_serial_plan_sas_plus I (op # concat ψ)" 
              using ops_is 
              by force
            ultimately have "execute_serial_plan_sas_plus I (concat (ops # ψ)) = I"
              using False 
              unfolding is_operator_applicable_in_def
              by fastforce
          }
          ultimately show ?thesis
            by argo
        qed  
    qed force
qed

lemma flattening_lemma:
  assumes "is_valid_problem_sas_plus Ψ"
    and "ops  set ψ. op. ops = [op]" 
    and "is_parallel_solution_for_problem Ψ ψ"
  shows "is_serial_solution_for_problem Ψ (concat ψ)"
proof  -
  let ?ψ' = "concat ψ" 
  {
    have "ops  set ψ. op  set ops. op  set ((Ψ)𝒪+)" 
      using assms(3)
      unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff
      by force
    hence "op  set ?ψ'. op  set ((Ψ)𝒪+)"
      using flattening_lemma_i
      by blast
  }
  moreover {
    {
      fix ops
      assume "ops  set ψ" 
      moreover obtain op where "ops = [op]" 
        using assms(2) calculation
        by blast
      moreover have "op  set ((Ψ)𝒪+)" 
        using assms(3) calculation
        unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff 
        by force
      moreover have "is_valid_operator_sas_plus Ψ op" 
        using assms(1) calculation(3)
        unfolding is_valid_problem_sas_plus_def Let_def list_all_iff 
          ListMem_iff
        by simp
      ultimately have "op. ops = [op]  is_valid_operator_sas_plus Ψ op"
        by blast
    }
    moreover have "(Ψ)G+ m execute_parallel_plan_sas_plus ((Ψ)I+) ψ" 
      using assms(3) 
      unfolding is_parallel_solution_for_problem_def
      by fastforce
    ultimately have "(Ψ)G+ m execute_serial_plan_sas_plus ((Ψ)I+) ?ψ'" 
      using flattening_lemma_ii
      by blast
  }
  ultimately show "is_serial_solution_for_problem Ψ ?ψ'" 
    unfolding is_serial_solution_for_problem_def list_all_iff ListMem_iff
    by fastforce
qed
end

subsection "Auxiliary lemmata on SAS+"


context
begin

― ‹ Relate the locale definition range_of› with its corresponding implementation for valid 
operators and given an effect (v, a)›. ›
lemma is_valid_operator_sas_plus_then_range_of_sas_plus_op_is_set_range_of_op:
  assumes "is_valid_operator_sas_plus Ψ op"
    and "(v, a)  set (precondition_of op)  (v, a)  set (effect_of op)"
  shows "(+ Ψ v) = set (the (sas_plus_problem.range_of Ψ v))" 
proof -
  consider (A) "(v, a)  set (precondition_of op)"
    | (B)  "(v, a)  set (effect_of op)"
    using assms(2)..
  thus ?thesis 
    proof (cases)
      case A
      then have "(+ Ψ v)  {}" and "a  + Ψ v" 
        using assms 
        unfolding range_of_def
        using is_valid_operator_sas_plus_then(2)
        by fast+
      thus ?thesis
        unfolding range_of'_def option.case_eq_if
        by auto
    next
      case B
      then have "(+ Ψ v)  {}" and "a  + Ψ v" 
        using assms 
        unfolding range_of_def
        using is_valid_operator_sas_plus_then(4)
        by fast+
      thus ?thesis
        unfolding range_of'_def option.case_eq_if
        by auto
    qed  
qed 

lemma set_the_range_of_is_range_of_sas_plus_if:
  fixes Ψ :: "('v, 'd) sas_plus_problem"
  assumes "is_valid_problem_sas_plus Ψ"
    "v  set ((Ψ)𝒱+)"
  shows "set (the (sas_plus_problem.range_of Ψ v)) = + Ψ v"
proof-
  have "v  set((Ψ)𝒱+)" 
    using assms(2)
    unfolding variables_of_def.
  moreover have "(+ Ψ v)  {}"
    using assms(1) calculation is_valid_problem_sas_plus_then(1)
    by blast
  moreover have "sas_plus_problem.range_of Ψ v  None" 
    and "sas_plus_problem.range_of Ψ v  Some []"
    using calculation(2) range_of_not_empty
    unfolding range_of_def 
    by fast+
  ultimately show ?thesis
    unfolding option.case_eq_if range_of'_def
    by force
qed

lemma sublocale_sas_plus_finite_domain_representation_ii:
  fixes Ψ::"('v,'d) sas_plus_problem"
  assumes "is_valid_problem_sas_plus Ψ"
  shows "v  set ((Ψ)𝒱+). (+ Ψ v)  {}"
    and "op  set ((Ψ)𝒪+). is_valid_operator_sas_plus Ψ op"
    and "dom ((Ψ)I+) = set ((Ψ)𝒱+)"
    and "v  dom ((Ψ)I+). the (((Ψ)I+) v)  + Ψ v"
    and "dom ((Ψ)G+)  set ((Ψ)𝒱+)"
    and "v  dom ((Ψ)G+). the (((Ψ)G+) v)  + Ψ v"
  using is_valid_problem_sas_plus_then[OF assms]
  by auto

end

end