Theory PDDL_STRIPS_Checker
section ‹Executable PDDL Checker›
theory PDDL_STRIPS_Checker
imports
PDDL_STRIPS_Semantics
Error_Monad_Add
"HOL.String"
"HOL-Library.Code_Target_Nat"
"HOL-Library.While_Combinator"
"Containers.Containers"
begin
subsection ‹Generic DFS Reachability Checker›
text ‹Used for subtype checks›
definition "E_of_succ succ ≡ { (u,v). v∈set (succ u) }"
lemma succ_as_E: "set (succ x) = E_of_succ succ `` {x}"
unfolding E_of_succ_def by auto
context
fixes succ :: "'a ⇒ 'a list"
begin
private abbreviation (input) "E ≡ E_of_succ succ"
definition "dfs_reachable D w ≡
let (V,w,brk) = while (λ(V,w,brk). ¬brk ∧ w≠[]) (λ(V,w,_).
case w of v#w ⇒
if D v then (V,v#w,True)
else if v∈V then (V,w,False)
else
let V = insert v V in
let w = succ v @ w in
(V,w,False)
) ({},w,False)
in brk"
context
fixes w⇩0 :: "'a list"
assumes finite_dfs_reachable[simp, intro!]: "finite (E⇧* `` set w⇩0)"
begin
private abbreviation (input) "W⇩0 ≡ set w⇩0"
definition "dfs_reachable_invar D V W brk ⟷
W⇩0 ⊆ W ∪ V
∧ W ∪ V ⊆ E⇧* `` W⇩0
∧ E``V ⊆ W ∪ V
∧ Collect D ∩ V = {}
∧ (brk ⟶ Collect D ∩ E⇧* `` W⇩0 ≠ {})"
lemma card_decreases: "
⟦finite V; y ∉ V; dfs_reachable_invar D V (Set.insert y W) brk ⟧
⟹ card (E⇧* `` W⇩0 - Set.insert y V) < card (E⇧* `` W⇩0 - V)"
apply (rule psubset_card_mono)
apply (auto simp: dfs_reachable_invar_def)
done
lemma all_neq_Cons_is_Nil[simp]:
"(∀y ys. x2 ≠ y # ys) ⟷ x2 = []" by (cases x2) auto
lemma dfs_reachable_correct: "dfs_reachable D w⇩0 ⟷ Collect D ∩ E⇧* `` set w⇩0 ≠ {}"
unfolding dfs_reachable_def
apply (rule while_rule[where
P="λ(V,w,brk). dfs_reachable_invar D V (set w) brk ∧ finite V"
and r="measure (λV. card (E⇧* `` (set w⇩0) - V)) <*lex*> measure length <*lex*> measure (λTrue⇒0 | False⇒1)"
])
subgoal by (auto simp: dfs_reachable_invar_def)
subgoal
apply (auto simp: neq_Nil_conv succ_as_E[of succ] split: if_splits)
by (auto simp: dfs_reachable_invar_def Image_iff intro: rtrancl.rtrancl_into_rtrancl)
subgoal by (fastforce simp: dfs_reachable_invar_def dest: Image_closed_trancl)
subgoal by blast
subgoal by (auto simp: neq_Nil_conv card_decreases)
done
end
definition "tab_succ l ≡ Mapping.lookup_default [] (fold (λ(u,v). Mapping.map_default u [] (Cons v)) l Mapping.empty)"
lemma Some_eq_map_option [iff]: "(Some y = map_option f xo) = (∃z. xo = Some z ∧ f z = y)"
by (auto simp add: map_option_case split: option.split)
lemma tab_succ_correct: "E_of_succ (tab_succ l) = set l"
proof -
have "set (Mapping.lookup_default [] (fold (λ(u,v). Mapping.map_default u [] (Cons v)) l m) u) = set l `` {u} ∪ set (Mapping.lookup_default [] m u)"
for m u
apply (induction l arbitrary: m)
by (auto
simp: Mapping.lookup_default_def Mapping.map_default_def Mapping.default_def
simp: lookup_map_entry' lookup_update' keys_is_none_rep Option.is_none_def
split: if_splits
)
from this[where m=Mapping.empty] show ?thesis
by (auto simp: E_of_succ_def tab_succ_def lookup_default_empty)
qed
end
lemma finite_imp_finite_dfs_reachable:
"⟦finite E; finite S⟧ ⟹ finite (E⇧*``S)"
apply (rule finite_subset[where B="S ∪ (Relation.Domain E ∪ Relation.Range E)"])
apply (auto simp: intro: finite_Domain finite_Range elim: rtranclE)
done
lemma dfs_reachable_tab_succ_correct: "dfs_reachable (tab_succ l) D vs⇩0 ⟷ Collect D ∩ (set l)⇧*``set vs⇩0 ≠ {}"
apply (subst dfs_reachable_correct)
by (simp_all add: tab_succ_correct finite_imp_finite_dfs_reachable)
subsection ‹Implementation Refinements›
subsubsection ‹Of-Type›
definition "of_type_impl G oT T ≡ (∀pt∈set (primitives oT). dfs_reachable G ((=) pt) (primitives T))"
fun ty_term' where
"ty_term' varT objT (term.VAR v) = varT v"
| "ty_term' varT objT (term.CONST c) = Mapping.lookup objT c"
lemma ty_term'_correct_aux: "ty_term' varT objT t = ty_term varT (Mapping.lookup objT) t"
by (cases t) auto
lemma ty_term'_correct[simp]: "ty_term' varT objT = ty_term varT (Mapping.lookup objT)"
using ty_term'_correct_aux by auto
context ast_domain begin
definition "of_type1 pt T ⟷ pt ∈ subtype_rel⇧* `` set (primitives T)"
lemma of_type_refine1: "of_type oT T ⟷ (∀pt∈set (primitives oT). of_type1 pt T)"
unfolding of_type_def of_type1_def by auto
definition "STG ≡ (tab_succ (map subtype_edge (types D)))"
lemma subtype_rel_impl: "subtype_rel = E_of_succ (tab_succ (map subtype_edge (types D)))"
by (simp add: tab_succ_correct subtype_rel_def)
lemma of_type1_impl: "of_type1 pt T ⟷ dfs_reachable (tab_succ (map subtype_edge (types D))) ((=)pt) (primitives T)"
by (simp add: subtype_rel_impl of_type1_def dfs_reachable_tab_succ_correct tab_succ_correct)
lemma of_type_impl_correct: "of_type_impl STG oT T ⟷ of_type oT T"
unfolding of_type1_impl STG_def of_type_impl_def of_type_refine1 ..
definition mp_constT :: "(object, type) mapping" where
"mp_constT = Mapping.of_alist (consts D)"
lemma mp_objT_correct[simp]: "Mapping.lookup mp_constT = constT"
unfolding mp_constT_def constT_def
by transfer (simp add: Map_To_Mapping.map_apply_def)
text ‹Lifting the subtype-graph through wf-checker›
context
fixes ty_ent :: "'ent ⇀ type"
begin
definition "is_of_type' stg v T ⟷ (
case ty_ent v of
Some vT ⇒ of_type_impl stg vT T
| None ⇒ False)"
lemma is_of_type'_correct: "is_of_type' STG v T = is_of_type ty_ent v T"
unfolding is_of_type'_def is_of_type_def of_type_impl_correct ..
fun wf_pred_atom' where "wf_pred_atom' stg (p,vs) ⟷ (case sig p of
None ⇒ False
| Some Ts ⇒ list_all2 (is_of_type' stg) vs Ts)"
lemma wf_pred_atom'_correct: "wf_pred_atom' STG pvs = wf_pred_atom ty_ent pvs"
by (cases pvs) (auto simp: is_of_type'_correct[abs_def] split:option.split)
fun wf_atom' :: "_ ⇒ 'ent atom ⇒ bool" where
"wf_atom' stg (atom.predAtm p vs) ⟷ wf_pred_atom' stg (p,vs)"
| "wf_atom' stg (atom.Eq a b) = (ty_ent a ≠ None ∧ ty_ent b ≠ None)"
lemma wf_atom'_correct: "wf_atom' STG a = wf_atom ty_ent a"
by (cases a) (auto simp: wf_pred_atom'_correct is_of_type'_correct[abs_def] split: option.splits)
fun wf_fmla' :: "_ ⇒ ('ent atom) formula ⇒ bool" where
"wf_fmla' stg (Atom a) ⟷ wf_atom' stg a"
| "wf_fmla' stg ⊥ ⟷ True"
| "wf_fmla' stg (φ1 ❙∧ φ2) ⟷ (wf_fmla' stg φ1 ∧ wf_fmla' stg φ2)"
| "wf_fmla' stg (φ1 ❙∨ φ2) ⟷ (wf_fmla' stg φ1 ∧ wf_fmla' stg φ2)"
| "wf_fmla' stg (φ1 ❙→ φ2) ⟷ (wf_fmla' stg φ1 ∧ wf_fmla' stg φ2)"
| "wf_fmla' stg (❙¬φ) ⟷ wf_fmla' stg φ"
lemma wf_fmla'_correct: "wf_fmla' STG φ ⟷ wf_fmla ty_ent φ"
by (induction φ rule: wf_fmla.induct) (auto simp: wf_atom'_correct)
fun wf_fmla_atom1' where
"wf_fmla_atom1' stg (Atom (predAtm p vs)) ⟷ wf_pred_atom' stg (p,vs)"
| "wf_fmla_atom1' stg _ ⟷ False"
lemma wf_fmla_atom1'_correct: "wf_fmla_atom1' STG φ = wf_fmla_atom ty_ent φ"
by (cases φ rule: wf_fmla_atom.cases) (auto
simp: wf_atom'_correct is_of_type'_correct[abs_def] split: option.splits)
fun wf_effect' where
"wf_effect' stg (Effect a d) ⟷
(∀ae∈set a. wf_fmla_atom1' stg ae)
∧ (∀de∈set d. wf_fmla_atom1' stg de)"
lemma wf_effect'_correct: "wf_effect' STG e = wf_effect ty_ent e"
by (cases e) (auto simp: wf_fmla_atom1'_correct)
end
fun wf_action_schema' :: "_ ⇒ _ ⇒ ast_action_schema ⇒ bool" where
"wf_action_schema' stg conT (Action_Schema n params pre eff) ⟷ (
let
tyv = ty_term' (map_of params) conT
in
distinct (map fst params)
∧ wf_fmla' tyv stg pre
∧ wf_effect' tyv stg eff)"
lemma wf_action_schema'_correct: "wf_action_schema' STG mp_constT s = wf_action_schema s"
by (cases s) (auto simp: wf_fmla'_correct wf_effect'_correct)
definition wf_domain' :: "_ ⇒ _ ⇒ bool" where
"wf_domain' stg conT ≡
wf_types
∧ distinct (map (predicate_decl.pred) (predicates D))
∧ (∀p∈set (predicates D). wf_predicate_decl p)
∧ distinct (map fst (consts D))
∧ (∀(n,T)∈set (consts D). wf_type T)
∧ distinct (map ast_action_schema.name (actions D))
∧ (∀a∈set (actions D). wf_action_schema' stg conT a)
"
lemma wf_domain'_correct: "wf_domain' STG mp_constT = wf_domain"
unfolding wf_domain_def wf_domain'_def
by (auto simp: wf_action_schema'_correct)
end
subsubsection ‹Application of Effects›
context ast_domain begin
text ‹We implement the application of an effect by explicit iteration over
the additions and deletions›
fun apply_effect_exec
:: "object ast_effect ⇒ world_model ⇒ world_model"
where
"apply_effect_exec (Effect a d) s
= fold (λadd s. Set.insert add s) a
(fold (λdel s. Set.remove del s) d s)"
lemma apply_effect_exec_refine[simp]:
"apply_effect_exec (Effect (a) (d)) s
= apply_effect (Effect (a) (d)) s"
proof(induction a arbitrary: s)
case Nil
then show ?case
proof(induction d arbitrary: s)
case Nil
then show ?case by auto
next
case (Cons a d)
then show ?case
by (auto simp add: image_def)
qed
next
case (Cons a a)
then show ?case
proof(induction d arbitrary: s)
case Nil
then show ?case by (auto; metis Set.insert_def sup_assoc insert_iff)
next
case (Cons a d)
then show ?case
by (auto simp: Un_commute minus_set_fold union_set_fold)
qed
qed
lemmas apply_effect_eq_impl_eq
= apply_effect_exec_refine[symmetric, unfolded apply_effect_exec.simps]
end
subsubsection ‹Well-Formedness›
context ast_problem begin
text ‹ We start by defining a mapping from objects to types. The container
framework will generate efficient, red-black tree based code for that
later. ›
type_synonym objT = "(object, type) mapping"
definition mp_objT :: "(object, type) mapping" where
"mp_objT = Mapping.of_alist (consts D @ objects P)"
lemma mp_objT_correct[simp]: "Mapping.lookup mp_objT = objT"
unfolding mp_objT_def objT_alt
by transfer (simp add: Map_To_Mapping.map_apply_def)
text ‹We refine the typecheck to use the mapping›
definition "is_obj_of_type_impl stg mp n T = (
case Mapping.lookup mp n of None ⇒ False | Some oT ⇒ of_type_impl stg oT T
)"
lemma is_obj_of_type_impl_correct[simp]:
"is_obj_of_type_impl STG mp_objT = is_obj_of_type"
apply (intro ext)
apply (auto simp: is_obj_of_type_impl_def is_obj_of_type_def of_type_impl_correct split: option.split)
done
text ‹We refine the well-formedness checks to use the mapping›
definition wf_fact' :: "objT ⇒ _ ⇒ fact ⇒ bool"
where
"wf_fact' ot stg ≡ wf_pred_atom' (Mapping.lookup ot) stg"
lemma wf_fact'_correct[simp]: "wf_fact' mp_objT STG = wf_fact"
by (auto simp: wf_fact'_def wf_fact_def wf_pred_atom'_correct[abs_def])
definition "wf_fmla_atom2' mp stg f
= (case f of formula.Atom (predAtm p vs) ⇒ (wf_fact' mp stg (p,vs)) | _ ⇒ False)"
lemma wf_fmla_atom2'_correct[simp]:
"wf_fmla_atom2' mp_objT STG φ = wf_fmla_atom objT φ"
apply (cases φ rule: wf_fmla_atom.cases)
by (auto simp: wf_fmla_atom2'_def wf_fact_def split: option.splits)
definition "wf_problem' stg conT mp ≡
wf_domain' stg conT
∧ distinct (map fst (objects P) @ map fst (consts D))
∧ (∀(n,T)∈set (objects P). wf_type T)
∧ distinct (init P)
∧ (∀f∈set (init P). wf_fmla_atom2' mp stg f)
∧ wf_fmla' (Mapping.lookup mp) stg (goal P)"
lemma wf_problem'_correct:
"wf_problem' STG mp_constT mp_objT = wf_problem"
unfolding wf_problem_def wf_problem'_def wf_world_model_def
by (auto simp: wf_domain'_correct wf_fmla'_correct)
text ‹Instantiating actions will yield well-founded effects.
Corollary of @{thm wf_instantiate_action_schema}.›
lemma wf_effect_inst_weak:
fixes a args
defines "ai ≡ instantiate_action_schema a args"
assumes A: "action_params_match a args"
"wf_action_schema a"
shows "wf_effect_inst (effect ai)"
using wf_instantiate_action_schema[OF A] unfolding ai_def[symmetric]
by (cases ai) (auto simp: wf_effect_inst_alt)
end
context wf_ast_domain begin
text ‹Resolving an action yields a well-founded action schema.›
lemma resolve_action_wf:
assumes "resolve_action_schema n = Some a"
shows "wf_action_schema a"
proof -
from wf_domain have
X1: "distinct (map ast_action_schema.name (actions D))"
and X2: "∀a∈set (actions D). wf_action_schema a"
unfolding wf_domain_def by auto
show ?thesis
using assms unfolding resolve_action_schema_def
by (auto simp add: index_by_eq_Some_eq[OF X1] X2)
qed
end
subsubsection ‹Execution of Plan Actions›
text ‹We will perform two refinement steps, to summarize redundant operations›
text ‹We first lift action schema lookup into the error monad. ›
context ast_domain begin
definition "resolve_action_schemaE n ≡
lift_opt
(resolve_action_schema n)
(ERR (shows ''No such action schema '' o shows n))"
end
context ast_problem begin
text ‹We define a function to determine whether a formula holds in
a world model›
definition "holds M F ≡ (valuation M) ⊨ F"
text ‹Justification of this function›
lemma holds_for_wf_fmlas:
assumes "wm_basic s"
shows "holds s F ⟷ close_world s ⊫ F"
unfolding holds_def using assms valuation_iff_close_world
by blast
text ‹The first refinement summarizes the enabledness check and the execution
of the action. Moreover, we implement the precondition evaluation by our
@{const holds} function. This way, we can eliminate redundant resolving
and instantiation of the action.
›
definition en_exE :: "plan_action ⇒ world_model ⇒ _+world_model" where
"en_exE ≡ λ(PAction n args) ⇒ λs. do {
a ← resolve_action_schemaE n;
check (action_params_match a args) (ERRS ''Parameter mismatch'');
let ai = instantiate_action_schema a args;
check (wf_effect_inst (effect ai)) (ERRS ''Effect not well-formed'');
check ( holds s (precondition ai)) (ERRS ''Precondition not satisfied'');
Error_Monad.return (apply_effect (effect ai) s)
}"
text ‹Justification of implementation.›
lemma (in wf_ast_problem) en_exE_return_iff:
assumes "wm_basic s"
shows "en_exE a s = Inr s'
⟷ plan_action_enabled a s ∧ s' = execute_plan_action a s"
apply (cases a)
using assms holds_for_wf_fmlas wf_domain
unfolding plan_action_enabled_def execute_plan_action_def
and execute_ground_action_def en_exE_def wf_domain_def
by (auto
split: option.splits
simp: resolve_action_schemaE_def return_iff)
text ‹Next, we use the efficient implementation @{const is_obj_of_type_impl}
for the type check, and omit the well-formedness check, as effects obtained
from instantiating well-formed action schemas are always well-formed
(@{thm [source] wf_effect_inst_weak}).›
abbreviation "action_params_match2 stg mp a args
≡ list_all2 (is_obj_of_type_impl stg mp)
args (map snd (ast_action_schema.parameters a))"
definition en_exE2
:: "_ ⇒ (object, type) mapping ⇒ plan_action ⇒ world_model ⇒ _+world_model"
where
"en_exE2 G mp ≡ λ(PAction n args) ⇒ λM. do {
a ← resolve_action_schemaE n;
check (action_params_match2 G mp a args) (ERRS ''Parameter mismatch'');
let ai = instantiate_action_schema a args;
check (holds M (precondition ai)) (ERRS ''Precondition not satisfied'');
Error_Monad.return (apply_effect (effect ai) M)
}"
text ‹Justification of refinement›
lemma (in wf_ast_problem) wf_en_exE2_eq:
shows "en_exE2 STG mp_objT pa s = en_exE pa s"
apply (cases pa; simp add: en_exE2_def en_exE_def Let_def)
apply (auto
simp: return_iff resolve_action_schemaE_def resolve_action_wf
simp: wf_effect_inst_weak action_params_match_def
split: error_monad_bind_split)
done
text ‹Combination of the two refinement lemmas›
lemma (in wf_ast_problem) en_exE2_return_iff:
assumes "wm_basic M"
shows "en_exE2 STG mp_objT a M = Inr M'
⟷ plan_action_enabled a M ∧ M' = execute_plan_action a M"
unfolding wf_en_exE2_eq
apply (subst en_exE_return_iff)
using assms
by (auto)
lemma (in wf_ast_problem) en_exE2_return_iff_compact_notation:
"⟦wm_basic s⟧ ⟹
en_exE2 STG mp_objT a s = Inr s'
⟷ plan_action_enabled a s ∧ s' = execute_plan_action a s"
using en_exE2_return_iff .
end
subsubsection ‹Checking of Plan›
context ast_problem begin
text ‹First, we combine the well-formedness check of the plan actions and
their execution into a single iteration.›
fun valid_plan_from1 :: "world_model ⇒ plan ⇒ bool" where
"valid_plan_from1 s [] ⟷ close_world s ⊫ (goal P)"
| "valid_plan_from1 s (π#πs)
⟷ plan_action_enabled π s
∧ (valid_plan_from1 (execute_plan_action π s) πs)"
lemma valid_plan_from1_refine: "valid_plan_from s πs = valid_plan_from1 s πs"
proof(induction πs arbitrary: s)
case Nil
then show ?case by (auto simp add: plan_action_path_def valid_plan_from_def)
next
case (Cons a πs)
then show ?case
by (auto
simp: valid_plan_from_def plan_action_path_def plan_action_enabled_def
simp: execute_ground_action_def execute_plan_action_def)
qed
text ‹Next, we use our efficient combined enabledness check and execution
function, and transfer the implementation to use the error monad: ›
fun valid_plan_fromE
:: "_ ⇒ (object, type) mapping ⇒ nat ⇒ world_model ⇒ plan ⇒ _+unit"
where
"valid_plan_fromE stg mp si s []
= check (holds s (goal P)) (ERRS ''Postcondition does not hold'')"
| "valid_plan_fromE stg mp si s (π#πs) = do {
s ← en_exE2 stg mp π s
<+? (λe _. shows ''at step '' o shows si o shows '': '' o e ());
valid_plan_fromE stg mp (si+1) s πs
}"
text ‹For the refinement, we need to show that the world models only
contain atoms, i.e., containing only atoms is an invariant under execution
of well-formed plan actions.›
lemma (in wf_ast_problem) wf_actions_only_add_atoms:
"⟦ wm_basic s; wf_plan_action a ⟧
⟹ wm_basic (execute_plan_action a s)"
using wf_problem wf_domain
unfolding wf_problem_def wf_domain_def
apply (cases a)
apply (clarsimp
split: option.splits
simp: wf_fmla_atom_alt execute_plan_action_def wm_basic_def
simp: execute_ground_action_def)
subgoal for n args schema fmla
apply (cases "effect (instantiate_action_schema schema args)"; simp)
by (metis ground_action.sel(2) ast_domain.wf_effect.simps
ast_domain.wf_fmla_atom_alt resolve_action_wf
wf_ground_action.elims(2) wf_instantiate_action_schema)
done
text ‹Refinement lemma for our plan checking algorithm›
lemma (in wf_ast_problem) valid_plan_fromE_return_iff[return_iff]:
assumes "wm_basic s"
shows "valid_plan_fromE STG mp_objT k s πs = Inr () ⟷ valid_plan_from s πs"
using assms unfolding valid_plan_from1_refine
proof (induction stg≡STG mp≡mp_objT k s πs rule: valid_plan_fromE.induct)
case (1 si s)
then show ?case
using wf_problem holds_for_wf_fmlas
by (auto
simp: return_iff Let_def wf_en_exE2_eq wf_problem_def
split: plan_action.split)
next
case (2 si s π πs)
then show ?case
apply (clarsimp
simp: return_iff en_exE2_return_iff
split: plan_action.split)
by (meson ast_problem.plan_action_enabled_def wf_actions_only_add_atoms)
qed
lemmas valid_plan_fromE_return_iff'[return_iff]
= wf_ast_problem.valid_plan_fromE_return_iff[of P, OF wf_ast_problem.intro]
end
subsection ‹Executable Plan Checker›
text ‹We obtain the main plan checker by combining the well-formedness check
and executability check. ›
definition "check_all_list P l msg msgf ≡
forallM (λx. check (P x) (λ_::unit. shows msg o shows '': '' o msgf x) ) l <+? snd"
lemma check_all_list_return_iff[return_iff]: "check_all_list P l msg msgf = Inr () ⟷ (∀x∈set l. P x)"
unfolding check_all_list_def
by (induction l) (auto)
definition "check_wf_types D ≡ do {
check_all_list (λ(_,t). t=''object'' ∨ t∈fst`set (types D)) (types D) ''Undeclared supertype'' (shows o snd)
}"
lemma check_wf_types_return_iff[return_iff]: "check_wf_types D = Inr () ⟷ ast_domain.wf_types D"
unfolding ast_domain.wf_types_def check_wf_types_def
by (force simp: return_iff)
definition "check_wf_domain D stg conT ≡ do {
check_wf_types D;
check (distinct (map (predicate_decl.pred) (predicates D))) (ERRS ''Duplicate predicate declaration'');
check_all_list (ast_domain.wf_predicate_decl D) (predicates D) ''Malformed predicate declaration'' (shows o predicate.name o predicate_decl.pred);
check (distinct (map fst (consts D))) (ERRS ''Duplicate constant declaration'');
check (∀(n,T)∈set (consts D). ast_domain.wf_type D T) (ERRS ''Malformed type'');
check (distinct (map ast_action_schema.name (actions D)) ) (ERRS ''Duplicate action name'');
check_all_list (ast_domain.wf_action_schema' D stg conT) (actions D) ''Malformed action'' (shows o ast_action_schema.name)
}"
lemma check_wf_domain_return_iff[return_iff]:
"check_wf_domain D stg conT = Inr () ⟷ ast_domain.wf_domain' D stg conT"
proof -
interpret ast_domain D .
show ?thesis
unfolding check_wf_domain_def wf_domain'_def
by (auto simp: return_iff)
qed
definition "prepend_err_msg msg e ≡ λ_::unit. shows msg o shows '': '' o e ()"
definition "check_wf_problem P stg conT mp ≡ do {
let D = ast_problem.domain P;
check_wf_domain D stg conT <+? prepend_err_msg ''Domain not well-formed'';
check (distinct (map fst (objects P) @ map fst (consts D))) (ERRS ''Duplicate object declaration'');
check ((∀(n,T)∈set (objects P). ast_domain.wf_type D T)) (ERRS ''Malformed type'');
check (distinct (init P)) (ERRS ''Duplicate fact in initial state'');
check (∀f∈set (init P). ast_problem.wf_fmla_atom2' P mp stg f) (ERRS ''Malformed formula in initial state'');
check (ast_domain.wf_fmla' D (Mapping.lookup mp) stg (goal P)) (ERRS ''Malformed goal formula'')
}"
lemma check_wf_problem_return_iff[return_iff]:
"check_wf_problem P stg conT mp = Inr () ⟷ ast_problem.wf_problem' P stg conT mp"
proof -
interpret ast_problem P .
show ?thesis
unfolding check_wf_problem_def wf_problem'_def
by (auto simp: return_iff)
qed
definition "check_plan P πs ≡ do {
let stg=ast_domain.STG (ast_problem.domain P);
let conT = ast_domain.mp_constT (ast_problem.domain P);
let mp = ast_problem.mp_objT P;
check_wf_problem P stg conT mp;
ast_problem.valid_plan_fromE P stg mp 1 (ast_problem.I P) πs
} <+? (λe. String.implode (e () ''''))"
text ‹Correctness theorem of the plan checker: It returns @{term "Inr ()"}
if and only if the problem is well-formed and the plan is valid.
›
theorem check_plan_return_iff[return_iff]: "check_plan P πs = Inr ()
⟷ ast_problem.wf_problem P ∧ ast_problem.valid_plan P πs"
proof -
interpret ast_problem P .
show ?thesis
unfolding check_plan_def
by (auto
simp: return_iff wf_world_model_def wf_fmla_atom_alt I_def wf_problem_def isOK_iff
simp: wf_problem'_correct ast_problem.I_def ast_problem.valid_plan_def wm_basic_def
)
qed
subsection ‹Code Setup›
text ‹In this section, we set up the code generator to generate verified
code for our plan checker.›
subsubsection ‹Code Equations›
text ‹We first register the code equations for the functions of the checker.
Note that we not necessarily register the original code equations, but also
optimized ones.
›
lemmas wf_domain_code =
ast_domain.sig_def
ast_domain.wf_types_def
ast_domain.wf_type.simps
ast_domain.wf_predicate_decl.simps
ast_domain.STG_def
ast_domain.is_of_type'_def
ast_domain.wf_atom'.simps
ast_domain.wf_pred_atom'.simps
ast_domain.wf_fmla'.simps
ast_domain.wf_fmla_atom1'.simps
ast_domain.wf_effect'.simps
ast_domain.wf_action_schema'.simps
ast_domain.wf_domain'_def
ast_domain.subst_term.simps
ast_domain.mp_constT_def
declare wf_domain_code[code]
lemmas wf_problem_code =
ast_problem.wf_problem'_def
ast_problem.wf_fact'_def
ast_problem.is_obj_of_type_alt
ast_problem.wf_fact_def
ast_problem.wf_plan_action.simps
ast_domain.subtype_edge.simps
declare wf_problem_code[code]
lemmas check_code =
ast_problem.valid_plan_def
ast_problem.valid_plan_fromE.simps
ast_problem.en_exE2_def
ast_problem.resolve_instantiate.simps
ast_domain.resolve_action_schema_def
ast_domain.resolve_action_schemaE_def
ast_problem.I_def
ast_domain.instantiate_action_schema.simps
ast_domain.apply_effect_exec.simps
ast_domain.apply_effect_eq_impl_eq
ast_problem.holds_def
ast_problem.mp_objT_def
ast_problem.is_obj_of_type_impl_def
ast_problem.wf_fmla_atom2'_def
valuation_def
declare check_code[code]
subsubsection ‹Setup for Containers Framework›
derive ceq predicate atom object formula
derive ccompare predicate atom object formula
derive (rbt) set_impl atom formula
derive (rbt) mapping_impl object
derive linorder predicate object atom "object atom formula"
subsubsection ‹More Efficient Distinctness Check for Linorders›
fun no_stutter :: "'a list ⇒ bool" where
"no_stutter [] = True"
| "no_stutter [_] = True"
| "no_stutter (a#b#l) = (a≠b ∧ no_stutter (b#l))"
lemma sorted_no_stutter_eq_distinct: "sorted l ⟹ no_stutter l ⟷ distinct l"
apply (induction l rule: no_stutter.induct)
apply (auto simp: )
done
definition distinct_ds :: "'a::linorder list ⇒ bool"
where "distinct_ds l ≡ no_stutter (quicksort l)"
lemma [code_unfold]: "distinct = distinct_ds"
apply (intro ext)
unfolding distinct_ds_def
apply (auto simp: sorted_no_stutter_eq_distinct)
done
subsubsection ‹Code Generation›
export_code
check_plan
nat_of_integer integer_of_nat Inl Inr
predAtm Eq predicate Pred Either Var Obj PredDecl BigAnd BigOr
formula.Not formula.Bot Effect ast_action_schema.Action_Schema
map_atom Domain Problem PAction
term.CONST term.VAR
String.explode String.implode
in SML
module_name PDDL_Checker_Exported
file "PDDL_STRIPS_Checker_Exported.sml"
export_code ast_domain.apply_effect_exec in SML module_name ast_domain
end