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))
))
∧ (∀fmla∈set 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)))
))
∧ (∀fmla∈set(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 Σ M⇩0 s⇩0 f ⟷
((∀fmla∈close_world M⇩0. s⇩0 ⊨⇩= fmla)
∧ wm_basic M⇩0
∧ (∀α∈Σ. 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 Σ M⇩0 s⇩0 f"
assumes "set αs ⊆ Σ"
assumes "ground_action_path M⇩0 αs M'"
obtains s'
where "compose_actions (map f αs) s⇩0 = Some s'"
and "∀fmla∈close_world M'. s' ⊨⇩= fmla"
proof -
have "(valuation M' ⊨ fmla)" if "wm_basic M'" "fmla∈M'" 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) s⇩0 = Some s' ∧ (∀fmla∈close_world M'. s' ⊨⇩= fmla)"
using assms
proof(induction αs arbitrary: s⇩0 M⇩0 )
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 ?M⇩1 = "execute_ground_action α M⇩0"
have "close_world M⇩0 ⊫ precondition α"
using ass(4)
by auto
moreover have s0_ent_cwM0: "∀fmla∈(close_world M⇩0). close_eq s⇩0 ⊨ fmla"
using ass(2)
unfolding sound_system_def
by auto
ultimately have s0_ent_alpha_precond: "close_eq s⇩0 ⊨ precondition α"
unfolding entailment_def
by auto
then obtain s⇩1 where s1: "(f α) s⇩0 = Some s⇩1"
"(∀atm. is_predAtom atm ⟶ atm ∉ set(dels (effect α))
⟶ close_eq s⇩0 ⊨ atm
⟶ close_eq s⇩1 ⊨ atm)"
"(∀fmla. fmla ∈ set(adds (effect α))
⟶ close_eq s⇩1 ⊨ fmla)"
"(∀atm. is_predAtom atm ∧ atm ∉ set (adds (effect α)) ∧ close_eq s⇩0 ⊨ Not atm ⟶ close_eq s⇩1 ⊨ Not atm)"
"(∀fmla. fmla ∈ set (dels (effect α)) ∧ fmla ∉ set(adds (effect α)) ⟶ close_eq s⇩1 ⊨ (Not fmla))"
"(∀a b. close_eq s⇩0 ⊨ Atom (Eq a b) ⟶ close_eq s⇩1 ⊨ Atom (Eq a b))"
"(∀a b. close_eq s⇩0 ⊨ Not (Atom (Eq a b)) ⟶ close_eq s⇩1 ⊨ Not (Atom (Eq a b)))"
using ass(2-4)
unfolding sound_system_def sound_opr_alt by force
have "close_eq s⇩1 ⊨ fmla" if "fmla∈close_world ?M⇩1" 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∈?M⇩1" for fmla s
proof-
have alpha: "(∀s.∀fmla∈set(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 ?M⇩1"
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 Σ ?M⇩1 s⇩1 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) s⇩1 = Some s' ∧ (∀a∈close_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 Σ M⇩0 s⇩0 f ⟹ set αs ⊆ Σ
⟹ ground_action_path M⇩0 αs M'
⟹ ∃s'. compose_actions (map f αs) s⇩0 = Some s'
∧ (∀fmla∈close_world M'. s' ⊨⇩= fmla)"
using STRIPS_sema_sound by metis
end
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. a≠b}"
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: "f∈M ⟹ 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 ⟹ fmla∈close_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 ⟹ fmla∈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)
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 "s⇩0 ≡ wm_to_state I"
shows "∃s'. compose_actions αs s⇩0 = 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
end