Theory Lifschitz_Consistency

section ‹Soundness theorem for the STRIPS semantics›
text ‹We prove the soundness theorem according to ~cite"lifschitz1987semantics".›

theory Lifschitz_Consistency
imports PDDL_STRIPS_Semantics
begin


text ‹States are modeled as valuations of our underlying predicate logic.›
type_synonym state = "(predicate×object list) valuation"

context ast_domain begin
  text ‹An action is a partial function from states to states. ›
  type_synonym action = "state  state"

  text ‹The Isabelle/HOL formula @{prop f s = Some s'} means
    that f› is applicable in state s›, and the result is s'›. ›

  text ‹Definition B (i)--(iv) in Lifschitz's paper~cite"lifschitz1987semantics"

  fun is_NegPredAtom where
    "is_NegPredAtom (Not x) = is_predAtom x" | "is_NegPredAtom _ = False"

  definition "close_eq s = (λpredAtm p xs  s (p,xs) | Eq a b  a=b)"

  lemma close_eq_predAtm[simp]: "close_eq s (predAtm p xs)  s (p,xs)"
    by (auto simp: close_eq_def)                    

  lemma close_eq_Eq[simp]: "close_eq s (Eq a b)  a=b"
    by (auto simp: close_eq_def)


  abbreviation entail_eq :: "state  object atom formula  bool" (infix "=" 55)
    where "entail_eq s f  close_eq s  f"


  fun sound_opr :: "ground_action  action  bool" where
    "sound_opr (Ground_Action pre (Effect add del)) f 
      (s. s = pre 
        (s'. f s = Some s'  (atm. is_predAtom atm  atm  set del  s = atm  s' = atm)
                (atm. is_predAtom atm  atm  set add  s = Not atm  s' = Not atm)
               (fmla. fmla  set add  s' = fmla)
               (fmla. fmla  set del  fmla  set add  s' = (Not fmla))
              ))
         (fmlaset add. is_predAtom fmla)"

  lemma sound_opr_alt:
    "sound_opr opr f =
      ((s. s = (precondition opr) 
          (s'. f s = (Some s')
                 (atm. is_predAtom atm  atm  set(dels (effect opr))  s = atm  s' = atm)
                 (atm. is_predAtom atm  atm  set (adds (effect opr))  s = Not atm  s' = Not atm)
                 (atm. atm  set(adds (effect opr))  s' = atm)
                 (fmla. fmla  set (dels (effect opr))  fmla  set(adds (effect opr))  s' = (Not fmla))
                 (a b. s = Atom (Eq a b)  s' = Atom (Eq a b))
                 (a b. s = Not (Atom (Eq a b))  s' = Not (Atom (Eq a b)))
                ))
         (fmlaset(adds (effect opr)). is_predAtom fmla))"
    by (cases "(opr,f)" rule: sound_opr.cases) auto

  text ‹Definition B (v)--(vii) in  Lifschitz's paper~cite"lifschitz1987semantics"
definition sound_system
    :: "ground_action set
       world_model
       state
       (ground_action  action)
       bool"
    where
    "sound_system Σ M0 s0 f 
      ((fmlaclose_world M0. s0  = fmla)
       wm_basic M0
       (αΣ. sound_opr α (f α)))"

  text ‹Composing two actions›
  definition compose_action :: "action  action  action" where
    "compose_action f1 f2 x = (case f2 x of Some y  f1 y | None  None)"

  text ‹Composing a list of actions›
  definition compose_actions :: "action list  action" where
    "compose_actions fs  fold compose_action fs Some"

  text ‹Composing a list of actions satisfies some natural lemmas: ›
  lemma compose_actions_Nil[simp]:
    "compose_actions [] = Some" unfolding compose_actions_def by auto

  lemma compose_actions_Cons[simp]:
    "f s = Some s'  compose_actions (f#fs) s = compose_actions fs s'"
  proof -
    interpret monoid_add compose_action Some
      apply unfold_locales
      unfolding compose_action_def
      by (auto split: option.split)
    assume "f s = Some s'"
    then show ?thesis
      unfolding compose_actions_def
      by (simp add: compose_action_def fold_plus_sum_list_rev)
  qed

  text ‹Soundness Theorem in Lifschitz's paper~cite"lifschitz1987semantics".›
theorem STRIPS_sema_sound:
  assumes "sound_system Σ M0 s0 f"
    ― ‹For a sound system Σ›
  assumes "set αs  Σ"
    ― ‹And a plan αs›
  assumes "ground_action_path M0 αs M'"
    ― ‹Which is accepted by the system, yielding result M'›
          (called R(αs)› in Lifschitz's paper~\cite{lifschitz1987semantics}.)›
  obtains s'
    ― ‹We have that f(αs)› is applicable
          in initial state, yielding state s'› (called fαs(s0)› in Lifschitz's paper~\cite{lifschitz1987semantics}.)›
  where "compose_actions (map f αs) s0 = Some s'"
    ― ‹The result world model M'› is satisfied in state s'›
    and "fmlaclose_world M'. s' = fmla"
proof -
  have "(valuation M'  fmla)" if "wm_basic M'" "fmlaM'" for fmla
    using that apply (induction fmla)
    by (auto simp: valuation_def wm_basic_def split: atom.split)
  have "s'. compose_actions (map f αs) s0 = Some s'  (fmlaclose_world M'. s' = fmla)"
    using assms
  proof(induction αs arbitrary: s0 M0 )
    case Nil
    then show ?case by (auto simp add: close_world_def compose_action_def sound_system_def)
  next
    case ass: (Cons α αs)
    then obtain pre add del where a: "α = Ground_Action pre (Effect add del)"
      using ground_action.exhaust ast_effect.exhaust by metis
    let ?M1 = "execute_ground_action α M0"
    have "close_world M0  precondition α"
      using ass(4)
      by auto
    moreover have s0_ent_cwM0: "fmla(close_world M0). close_eq s0  fmla"
      using ass(2)
      unfolding sound_system_def
      by auto
    ultimately have s0_ent_alpha_precond: "close_eq s0  precondition α"
      unfolding entailment_def
      by auto
    then obtain s1 where s1: "(f α) s0 = Some s1"
      "(atm. is_predAtom atm  atm  set(dels (effect α))
                                             close_eq s0  atm
                                             close_eq s1  atm)"
      "(fmla. fmla  set(adds (effect α))
                                             close_eq s1  fmla)"
      "(atm. is_predAtom atm  atm  set (adds (effect α))  close_eq s0  Not atm  close_eq s1  Not atm)"
      "(fmla. fmla  set (dels (effect α))  fmla  set(adds (effect α))  close_eq s1  (Not fmla))"
      "(a b. close_eq s0  Atom (Eq a b)  close_eq s1  Atom (Eq a b))"
      "(a b. close_eq s0  Not (Atom (Eq a b))  close_eq s1  Not (Atom (Eq a b)))"
      using ass(2-4)
      unfolding sound_system_def sound_opr_alt by force
    have "close_eq s1  fmla" if "fmlaclose_world ?M1" for fmla
      using ass(2)
      using that s1 s0_ent_cwM0
      unfolding sound_system_def execute_ground_action_def wm_basic_def
      apply (auto simp: in_close_world_conv)
      subgoal
        by (metis (no_types, lifting) DiffE UnE a apply_effect.simps ground_action.sel(2) ast_effect.sel(1) ast_effect.sel(2) close_world_extensive subsetCE)
      subgoal
        by (metis Diff_iff Un_iff a ground_action.sel(2) ast_domain.apply_effect.simps ast_domain.close_eq_predAtm ast_effect.sel(1) ast_effect.sel(2) formula_semantics.simps(1) formula_semantics.simps(3) in_close_world_conv is_predAtom.simps(1))
      done
    moreover have "(atm. fmla  formula.Atom atm)  s  fmla" if "fmla?M1" for fmla s
    proof-
      have alpha: "(s.fmlaset(adds (effect α)). ¬ is_predAtom fmla  s  fmla)"
        using ass(2,3)
        unfolding sound_system_def ast_domain.sound_opr_alt
        by auto
      then show ?thesis
        using that
        unfolding a execute_ground_action_def
        using ass.prems(1)[unfolded sound_system_def]
        by(cases fmla; fastforce simp: wm_basic_def)

    qed
    moreover have "(oprΣ. sound_opr opr (f opr))"
      using ass(2) unfolding sound_system_def
      by (auto simp add:)
    moreover have "wm_basic ?M1"
      using ass(2,3)
      unfolding sound_system_def execute_ground_action_def
      thm sound_opr.cases
      apply (cases "(α,f α)" rule: sound_opr.cases)
      apply (auto simp: wm_basic_def)
      done
    ultimately have "sound_system Σ ?M1 s1 f"
      unfolding sound_system_def
      by (auto simp: wm_basic_def)
    from ass.IH[OF this] ass.prems obtain s' where
      "compose_actions (map f αs) s1 = Some s'  (aclose_world M'. s' = a)"
      by auto
    thus ?case by (auto simp: s1(1))
  qed
  with that show ?thesis by blast
qed

  text ‹More compact notation of the soundness theorem.›
  theorem STRIPS_sema_sound_compact_version:
    "sound_system Σ M0 s0 f  set αs  Σ
     ground_action_path M0 αs M'
     s'. compose_actions (map f αs) s0 = Some s'
           (fmlaclose_world M'. s' = fmla)"
    using STRIPS_sema_sound by metis

end ― ‹Context of ast_domain›

subsection ‹Soundness Theorem for PDDL›

context wf_ast_problem begin

  text ‹Mapping world models to states›
  definition state_to_wm :: "state  world_model"
    where "state_to_wm s = ({formula.Atom (predAtm p xs) | p xs. s (p,xs)})"
  definition wm_to_state :: "world_model  state"
    where "wm_to_state M = (λ(p,xs). (formula.Atom (predAtm p xs))  M)"


  lemma wm_to_state_eq[simp]: "wm_to_state M (p, as)  Atom (predAtm p as)  M"
    by (auto simp: wm_to_state_def)




  lemma wm_to_state_inv[simp]: "wm_to_state (state_to_wm s) = s"
    by (auto simp: wm_to_state_def
      state_to_wm_def image_def)

  text ‹Mapping AST action instances to actions›
  definition "pddl_opr_to_act g_opr s = (
    let M = state_to_wm s in
    if (wm_to_state (close_world M)) = (precondition g_opr) then
      Some (wm_to_state (apply_effect (effect g_opr) M))
    else
      None)"

definition "close_eq_M M = (M  {Atom (predAtm p xs) | p xs. True })  {Atom (Eq a a) | a. True}  {¬(Atom (Eq a b)) | a b. ab}"

  lemma atom_in_wm_eq:
    "s = (formula.Atom atm)
       ((formula.Atom atm)  close_eq_M (state_to_wm s))"
    by (auto simp: wm_to_state_def
      state_to_wm_def image_def close_eq_M_def close_eq_def split: atom.splits)

lemma atom_in_wm_2_eq:
    "close_eq (wm_to_state M)  (formula.Atom atm)
       ((formula.Atom atm)  close_eq_M M)"
    by (auto simp: wm_to_state_def
      state_to_wm_def image_def close_eq_def close_eq_M_def split:atom.splits)

  lemma not_dels_preserved:
    assumes "f  (set d)" " f  M"
    shows "f  apply_effect (Effect a d) M"
    using assms
    by auto

  lemma adds_satisfied:
    assumes "f  (set a)"
    shows "f  apply_effect (Effect a d) M"
    using assms
    by auto

  lemma dels_unsatisfied:
    assumes "f  (set d)" "f  set a"
    shows "f  apply_effect (Effect a d) M"
    using assms
    by auto

  lemma dels_unsatisfied_2:
    assumes "f  set (dels eff)" "f  set (adds eff)"
    shows "f  apply_effect eff M"
    using assms
    by (cases eff; auto)

  lemma wf_fmla_atm_is_atom: "wf_fmla_atom objT f  is_predAtom f"
    by (cases f rule: wf_fmla_atom.cases) auto

  lemma wf_act_adds_are_atoms:
    assumes "wf_effect_inst effs" "ae  set (adds effs)"
    shows "is_predAtom ae"
    using assms
    by (cases effs) (auto simp: wf_fmla_atom_alt)

  lemma wf_act_adds_dels_atoms:
    assumes "wf_effect_inst effs" "ae  set (dels effs)"
    shows "is_predAtom ae"
    using assms
    by (cases effs) (auto simp: wf_fmla_atom_alt)

  lemma to_state_close_from_state_eq[simp]: "wm_to_state (close_world (state_to_wm s)) = s"
    by (auto simp: wm_to_state_def close_world_def
      state_to_wm_def image_def)



lemma wf_eff_pddl_ground_act_is_sound_opr:
  assumes "wf_effect_inst (effect g_opr)"
  shows "sound_opr g_opr ((pddl_opr_to_act g_opr))"
  unfolding sound_opr_alt
  apply(cases g_opr; safe)
  subgoal for pre eff s
    apply (rule exI[where x="wm_to_state(apply_effect eff (state_to_wm s))"])
    apply (auto simp: pddl_opr_to_act_def Let_def split:if_splits)
    subgoal for atm
      by (cases eff; cases atm; auto simp: close_eq_def wm_to_state_def state_to_wm_def split: atom.splits)
    subgoal for atm
      by (cases eff; cases atm; auto simp: close_eq_def wm_to_state_def state_to_wm_def split: atom.splits)
    subgoal for atm
      using assms
      by (cases eff; cases atm; force simp: close_eq_def wm_to_state_def state_to_wm_def split: atom.splits)
    subgoal for fmla
      using assms
      by (cases eff; cases fmla rule: wf_fmla_atom.cases; force simp: close_eq_def wm_to_state_def state_to_wm_def split: atom.splits)
    done
  subgoal for pre eff fmla
    using assms
    by (cases eff; cases fmla rule: wf_fmla_atom.cases; force)
  done



  lemma wf_eff_impt_wf_eff_inst: "wf_effect objT eff  wf_effect_inst eff"
    by (cases eff; auto simp add: wf_fmla_atom_alt)

  lemma wf_pddl_ground_act_is_sound_opr:
    assumes "wf_ground_action g_opr"
    shows "sound_opr g_opr (pddl_opr_to_act g_opr)"
    using wf_eff_impt_wf_eff_inst wf_eff_pddl_ground_act_is_sound_opr assms
    by (cases g_opr; auto)

  lemma wf_action_schema_sound_inst:
    assumes "action_params_match act args" "wf_action_schema act"
    shows "sound_opr
      (instantiate_action_schema act args)
      ((pddl_opr_to_act (instantiate_action_schema act args)))"
    using
      wf_pddl_ground_act_is_sound_opr[
        OF wf_instantiate_action_schema[OF assms]]
      by blast

  lemma wf_plan_act_is_sound:
    assumes "wf_plan_action (PAction n args)"
    shows "sound_opr
      (instantiate_action_schema (the (resolve_action_schema n)) args)
      ((pddl_opr_to_act
        (instantiate_action_schema (the (resolve_action_schema n)) args)))"
    using assms
    using wf_action_schema_sound_inst wf_eff_pddl_ground_act_is_sound_opr
    by (auto split: option.splits)

  lemma wf_plan_act_is_sound':
    assumes "wf_plan_action π"
    shows "sound_opr
      (resolve_instantiate π)
      ((pddl_opr_to_act (resolve_instantiate π)))"
    using assms wf_plan_act_is_sound
    by (cases π; auto )

  lemma wf_world_model_has_atoms: "fM  wf_world_model M  is_predAtom f"
    using wf_fmla_atm_is_atom
    unfolding wf_world_model_def
    by auto

  lemma wm_to_state_works_for_wf_wm_closed:
    "wf_world_model M  fmlaclose_world M  close_eq (wm_to_state M)  fmla"
    apply (cases fmla rule: wf_fmla_atom.cases)
    by (auto simp: wf_world_model_def close_eq_def wm_to_state_def close_world_def)

  lemma wm_to_state_works_for_wf_wm: "wf_world_model M  fmlaM  close_eq (wm_to_state M)  fmla"
    apply (cases fmla rule: wf_fmla_atom.cases)
    by (auto simp: wf_world_model_def close_eq_def wm_to_state_def)



  lemma wm_to_state_works_for_I_closed:
    assumes "x  close_world I"
    shows "close_eq (wm_to_state I)  x"
    apply (rule wm_to_state_works_for_wf_wm_closed)
    using assms wf_I by auto


  lemma wf_wm_imp_basic: "wf_world_model M  wm_basic M"
    by (auto simp: wf_world_model_def wm_basic_def wf_fmla_atm_is_atom)

theorem wf_plan_sound_system:
  assumes "π set πs. wf_plan_action π"
  shows "sound_system
      (set (map resolve_instantiate πs))
      I
      (wm_to_state I)
      ((λα. pddl_opr_to_act α))"
  unfolding sound_system_def
proof(intro conjI ballI)
  show "close_eq(wm_to_state I)  x" if "x  close_world I" for x
    using that[unfolded in_close_world_conv]
      wm_to_state_works_for_I_closed wm_to_state_works_for_wf_wm
    by (auto simp: wf_I)

  show "wm_basic I" using wf_wm_imp_basic[OF wf_I] .

  show "sound_opr α (pddl_opr_to_act α)" if "α  set (map resolve_instantiate πs)" for α
    using that
    using wf_plan_act_is_sound' assms
    by auto
qed

theorem wf_plan_soundness_theorem:
    assumes "plan_action_path I πs M"
    defines "αs  map (pddl_opr_to_act  resolve_instantiate) πs"
    defines "s0  wm_to_state I"
    shows "s'. compose_actions αs s0 = Some s'  (φclose_world M. s' = φ)"
    apply (rule STRIPS_sema_sound)
    apply (rule wf_plan_sound_system)
    using assms
    unfolding plan_action_path_def
    by (auto simp add: image_def)

end ― ‹Context of wf_ast_problem›

end