Commit 9e3b3437 by Lawrence Paulson

### new entry AI_Planning_Languages_Semantics

parent e02037dfc6c4
 theory Error_Monad_Add imports "Certification_Monads.Check_Monad" "Show.Show_Instances" begin (* TODO: Move *) abbreviation "assert_opt \ \ if \ then Some () else None" definition "lift_opt m e \ case m of Some x \ Error_Monad.return x | None \ Error_Monad.error e" lemma lift_opt_simps[simp]: "lift_opt None e = error e" "lift_opt (Some v) e = return v" by (auto simp: lift_opt_def) (* TODO: Move *) lemma reflcl_image_iff[simp]: "R\<^sup>=``S = S\R``S" by blast named_theorems return_iff lemma bind_return_iff[return_iff]: "Error_Monad.bind m f = Inr y \ (\x. m = Inr x \ f x = Inr y)" by auto lemma lift_opt_return_iff[return_iff]: "lift_opt m e = Inr x \ m=Some x" unfolding lift_opt_def by (auto split: option.split) lemma check_return_iff[return_iff]: "check \ e = Inr uu \ \" by (auto simp: check_def) lemma check_simps[simp]: "check True e = succeed" "check False e = error e" by (auto simp: check_def) lemma Let_return_iff[return_iff]: "(let x=v in f x) = Inr w \ f v = Inr w" by simp abbreviation ERR :: "shows \ (unit \ shows)" where "ERR s \ \_. s" abbreviation ERRS :: "String.literal \ (unit \ shows)" where "ERRS s \ ERR (shows s)" lemma error_monad_bind_split: "P (bind m f) \ (\v. m = Inl v \ P (Inl v)) \ (\v. m = Inr v \ P (f v))" by (cases m) auto lemma error_monad_bind_split_asm: "P (bind m f) \ \ (\x. m = Inl x \ \ P (Inl x) \ (\x. m = Inr x \ \ P (f x)))" by (cases m) auto lemmas error_monad_bind_splits =error_monad_bind_split error_monad_bind_split_asm end
 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 "\\<^sub>=" 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 \\<^sub>= pre \ (\s'. f s = Some s' \ (\atm. is_predAtom atm \ atm \ set del \ s \\<^sub>= atm \ s' \\<^sub>= atm) \ (\atm. is_predAtom atm \ atm \ set add \ s \\<^sub>= Not atm \ s' \\<^sub>= Not atm) \ (\fmla. fmla \ set add \ s' \\<^sub>= fmla) \ (\fmla. fmla \ set del \ fmla \ set add \ s' \\<^sub>= (Not fmla)) )) \ (\fmla\set add. is_predAtom fmla)" lemma sound_opr_alt: "sound_opr opr f = ((\s. s \\<^sub>= (precondition opr) \ (\s'. f s = (Some s') \ (\atm. is_predAtom atm \ atm \ set(dels (effect opr)) \ s \\<^sub>= atm \ s' \\<^sub>= atm) \ (\atm. is_predAtom atm \ atm \ set (adds (effect opr)) \ s \\<^sub>= Not atm \ s' \\<^sub>= Not atm) \ (\atm. atm \ set(adds (effect opr)) \ s' \\<^sub>= atm) \ (\fmla. fmla \ set (dels (effect opr)) \ fmla \ set(adds (effect opr)) \ s' \\<^sub>= (Not fmla)) \ (\a b. s \\<^sub>= Atom (Eq a b) \ s' \\<^sub>= Atom (Eq a b)) \ (\a b. s \\<^sub>= Not (Atom (Eq a b)) \ s' \\<^sub>= 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\<^sub>0 s\<^sub>0 f \ ((\fmla\close_world M\<^sub>0. s\<^sub>0 \\<^sub>= fmla) \ wm_basic M\<^sub>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\<^sub>0 s\<^sub>0 f" \ \For a sound system \\\\ assumes "set \s \ \" \ \And a plan \\s\\ assumes "ground_action_path M\<^sub>0 \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\<^sub>\\<^sub>s(s\<^sub>0)\ in Lifschitz's paper~\cite{lifschitz1987semantics}.)\ where "compose_actions (map f \s) s\<^sub>0 = Some s'" \ \The result world model \M'\ is satisfied in state \s'\\ and "\fmla\close_world M'. s' \\<^sub>= 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\<^sub>0 = Some s' \ (\fmla\close_world M'. s' \\<^sub>= fmla)" using assms proof(induction \s arbitrary: s\<^sub>0 M\<^sub>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\<^sub>1 = "execute_ground_action \ M\<^sub>0" have "close_world M\<^sub>0 \ precondition \" using ass(4) by auto moreover have s0_ent_cwM0: "\fmla\(close_world M\<^sub>0). close_eq s\<^sub>0 \ fmla" using ass(2) unfolding sound_system_def by auto ultimately have s0_ent_alpha_precond: "close_eq s\<^sub>0 \ precondition \" unfolding entailment_def by auto then obtain s\<^sub>1 where s1: "(f \) s\<^sub>0 = Some s\<^sub>1" "(\atm. is_predAtom atm \ atm \ set(dels (effect \)) \ close_eq s\<^sub>0 \ atm \ close_eq s\<^sub>1 \ atm)" "(\fmla. fmla \ set(adds (effect \)) \ close_eq s\<^sub>1 \ fmla)" "(\atm. is_predAtom atm \ atm \ set (adds (effect \)) \ close_eq s\<^sub>0 \ Not atm \ close_eq s\<^sub>1 \ Not atm)" "(\fmla. fmla \ set (dels (effect \)) \ fmla \ set(adds (effect \)) \ close_eq s\<^sub>1 \ (Not fmla))" "(\a b. close_eq s\<^sub>0 \ Atom (Eq a b) \ close_eq s\<^sub>1 \ Atom (Eq a b))" "(\a b. close_eq s\<^sub>0 \ Not (Atom (Eq a b)) \ close_eq s\<^sub>1 \ Not (Atom (Eq a b)))" using ass(2-4) unfolding sound_system_def sound_opr_alt by force have "close_eq s\<^sub>1 \ fmla" if "fmla\close_world ?M\<^sub>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\<^sub>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\<^sub>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\<^sub>1 s\<^sub>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\<^sub>1 = Some s' \ (\a\close_world M'. s' \\<^sub>= 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\<^sub>0 s\<^sub>0 f \ set \s \ \ \ ground_action_path M\<^sub>0 \s M' \ \s'. compose_actions (map f \s) s\<^sub>0 = Some s' \ (\fmla\close_world M'. s' \\<^sub>= 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)) \\<^sub>= (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} \ {\<^bold>\(Atom (Eq a b)) | a b. a\b}" lemma atom_in_wm_eq: "s \\<^sub>= (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\<^sub>0 \ wm_to_state I" shows "\s'. compose_actions \s s\<^sub>0 = Some s' \ (\\\close_world M. s' \\<^sub>= \)" 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
 theory Option_Monad_Add imports "HOL-Library.Monad_Syntax" begin definition "oassert \ \ if \ then Some () else None" fun omap :: "('a\'b) \ 'a list \ 'b list" where "omap f [] = Some []" | "omap f (x#xs) = do { y \ f x; ys \ omap f xs; Some (y#ys) }" lemma omap_cong[fundef_cong]: assumes "\x. x\set l' \ f x = f' x" assumes "l=l'" shows "omap f l = omap f' l'" unfolding assms(2) using assms(1) by (induction l') (auto) lemma assert_eq_iff[simp]: "oassert \ = None \ \\" "oassert \ = Some u \ \" unfolding oassert_def by auto lemma omap_length[simp]: "omap f l = Some l' \ length l' = length l" apply (induction l arbitrary: l') apply (auto split: Option.bind_splits) done lemma omap_append[simp]: "omap f (xs@ys) = do {xs \ omap f xs; ys \ omap f ys; Some (xs@ys)}" by (induction xs) (auto) lemma omap_alt: "omap f l = Some l' \ (l' = map (the o f) l \ (\x\set l. f x \ None))" apply (induction l arbitrary: l') apply (auto split: Option.bind_splits) done lemma omap_alt_None: "omap f l = None \ (\x\set l. f x = None)" apply (induction l) apply (auto split: Option.bind_splits) done lemma omap_nth: "\omap f l = Some l'; i \ f (l!i) = Some (l'!i)" apply (induction l arbitrary: l' i) apply (auto split: Option.bind_splits simp: nth_Cons split: nat.splits) done lemma omap_eq_Nil_conv[simp]: "omap f xs = Some [] \ xs=[]" apply (cases xs) apply (auto split: Option.bind_splits) done lemma omap_eq_Cons_conv[simp]: "omap f xs = Some (y#ys') \ (\x xs'. xs=x#xs' \ f x = Some y \ omap f xs' = Some ys')" apply (cases xs) apply (auto split: Option.bind_splits) done lemma omap_eq_append_conv[simp]: "omap f xs = Some (ys\<^sub>1@ys\<^sub>2) \ (\xs\<^sub>1 xs\<^sub>2. xs=xs\<^sub>1@xs\<^sub>2 \ omap f xs\<^sub>1 = Some ys\<^sub>1 \ omap f xs\<^sub>2 = Some ys\<^sub>2)" apply (induction ys\<^sub>1 arbitrary: xs) apply (auto 0 3 split: Option.bind_splits) apply (metis append_Cons) done lemma omap_list_all2_conv: "omap f xs = Some ys \ (list_all2 (\x y. f x = Some y)) xs ys" apply (induction xs arbitrary: ys) apply (auto split: Option.bind_splits simp: ) apply (simp add: list_all2_Cons1) apply (simp add: list_all2_Cons1) apply (simp add: list_all2_Cons1) apply clarsimp by (metis option.inject) fun omap_option where "omap_option f None = Some None" | "omap_option f (Some x) = do { x \ f x; Some (Some x) }" lemma omap_option_conv: "omap_option f xx = None \ (\x. xx=Some x \ f x = None)" "omap_option f xx = (Some (Some x')) \ (\x. xx=Some x \ f x = Some x')" "omap_option f xx = (Some None) \ xx=None" by (cases xx;auto split: Option.bind_splits)+ lemma omap_option_eq: "omap_option f x = (case x of None \ Some None | Some x \ do { x \ f x; Some (Some x) })" by (auto split: option.split) fun omap_prod where "omap_prod f\<^sub>1 f\<^sub>2 (a,b) = do { a\f\<^sub>1 a; b\f\<^sub>2 b; Some (a,b) }" (* Extend map function for datatype to option monad. TODO: Show reasonable lemmas, like parametricity, etc. Hopefully only depending on BNF-property of datatype *) definition "omap_dt setf mapf f obj \ do { oassert (\x\setf obj. f x \ None); Some (mapf (the o f) obj) }" end
 section \Executable PDDL Checker\ theory PDDL_STRIPS_Checker imports PDDL_STRIPS_Semantics Error_Monad_Add "HOL.String" (*"HOL-Library.Code_Char" TODO: This might lead to performance loss! CHECK! *) "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)