Theory PDDL_STRIPS_Semantics

section ‹PDDL and STRIPS Semantics›
theory PDDL_STRIPS_Semantics
imports
  "Propositional_Proof_Systems.Formulas"
  "Propositional_Proof_Systems.Sema"
  "Propositional_Proof_Systems.Consistency"
  "Automatic_Refinement.Misc"
  "Automatic_Refinement.Refine_Util"
begin
no_notation insert (‹_ ▹ _› [56,55] 55)

subsection ‹Utility Functions›
definition "index_by f l ≡ map_of (map (λx. (f x,x)) l)"

lemma index_by_eq_Some_eq[simp]:
  assumes "distinct (map f l)"
  shows "index_by f l n = Some x ⟷ (x∈set l ∧ f x = n)"
  unfolding index_by_def
  using assms
  by (auto simp: o_def)

lemma index_by_eq_SomeD:
  shows "index_by f l n = Some x ⟹ (x∈set l ∧ f x = n)"
  unfolding index_by_def
  by (auto dest: map_of_SomeD)


lemma lookup_zip_idx_eq:
  assumes "length params = length args"
  assumes "i<length args"
  assumes "distinct params"
  assumes "k = params ! i"
  shows "map_of (zip params args) k = Some (args ! i)"
  using assms
  by (auto simp: in_set_conv_nth)

lemma rtrancl_image_idem[simp]: "R⇧* `` R⇧* `` s = R⇧* `` s"
  by (metis relcomp_Image rtrancl_idemp_self_comp)


subsection ‹Abstract Syntax›

subsubsection ‹Generic Entities›
type_synonym name = string

datatype predicate = Pred (name: name)

text ‹Some of the AST entities are defined over a polymorphic ‹'val› type,
  which gets either instantiated by variables (for domains)
  or objects (for problems).
›

text ‹An atom is either a predicate with arguments, or an equality statement.›
datatype 'ent atom = predAtm (predicate: predicate) (arguments: "'ent list")
                     | Eq (lhs: 'ent) (rhs: 'ent)

text ‹A type is a list of primitive type names.
  To model a primitive type, we use a singleton list.›
datatype type = Either (primitives: "name list")

text ‹An effect contains a list of values to be added, and a list of values
  to be removed.›
datatype 'ent ast_effect = Effect (adds: "('ent atom formula) list") (dels: "('ent atom formula) list")

text ‹Variables are identified by their names.›
datatype variable = varname: Var name
text ‹Objects and constants are identified by their names›
datatype object = name: Obj name

datatype "term" = VAR variable | CONST object
hide_const (open) VAR CONST ― ‹Refer to constructors by qualified names only›




subsubsection ‹Domains›

text ‹An action schema has a name, a typed parameter list, a precondition,
  and an effect.›
datatype ast_action_schema = Action_Schema
  (name: name)
  (parameters: "(variable × type) list")
  (precondition: "term atom formula")
  (effect: "term ast_effect")

text ‹A predicate declaration contains the predicate's name and its
  argument types.›
datatype predicate_decl = PredDecl
  (pred: predicate)
  (argTs: "type list")

text ‹A domain contains the declarations of primitive types, predicates,
  and action schemas.›
datatype ast_domain = Domain
  (types: "(name × name) list") ― ‹ ‹(type, supertype)› declarations. ›
  (predicates: "predicate_decl list")
  ("consts": "(object × type) list")
  (actions: "ast_action_schema list")

subsubsection ‹Problems›


text ‹A fact is a predicate applied to objects.›
type_synonym fact = "predicate × object list"

text ‹A problem consists of a domain, a list of objects,
  a description of the initial state, and a description of the goal state. ›
datatype ast_problem = Problem
  (domain: ast_domain)
  (objects: "(object × type) list")
  (init: "object atom formula list")
  (goal: "object atom formula")


subsubsection ‹Plans›
datatype plan_action = PAction
  (name: name)
  (arguments: "object list")

type_synonym plan = "plan_action list"

subsubsection ‹Ground Actions›
text ‹The following datatype represents an action scheme that has been
  instantiated by replacing the arguments with concrete objects,
  also called ground action.
›
datatype ground_action = Ground_Action
  (precondition: "(object atom) formula")
  (effect: "object ast_effect")



subsection ‹Closed-World Assumption, Equality, and Negation›
  text ‹Discriminator for atomic predicate formulas.›
  fun is_predAtom where
    "is_predAtom (Atom (predAtm _ _)) = True" | "is_predAtom _ = False"


  text ‹The world model is a set of (atomic) formulas›
  type_synonym world_model = "object atom formula set"

  text ‹It is basic, if it only contains atoms›
  definition "wm_basic M ≡ ∀a∈M. is_predAtom a"

  text ‹A valuation extracted from the atoms of the world model›
  definition valuation :: "world_model ⇒ object atom valuation"
    where "valuation M ≡ λpredAtm p xs ⇒ Atom (predAtm p xs) ∈ M | Eq a b ⇒ a=b"

  text ‹Augment a world model by adding negated versions of all atoms
    not contained in it, as well as interpretations of equality.›
  definition close_world :: "world_model ⇒ world_model" where "close_world M =
    M ∪ {❙¬(Atom (predAtm p as)) | p as. Atom (predAtm p as) ∉ M}
    ∪ {Atom (Eq a a) | a. True} ∪ {❙¬(Atom (Eq a b)) | a b. a≠b}"

  definition "close_neg M ≡ M ∪ {❙¬(Atom a) | a. Atom a ∉ M}"
  lemma "wm_basic M ⟹ close_world M = close_neg (M ∪ {Atom (Eq a a) | a. True})"
    unfolding close_world_def close_neg_def wm_basic_def
    apply clarsimp
    apply (auto 0 3)
    by (metis atom.exhaust)


  abbreviation cw_entailment (infix ‹⇧c⊫⇩=› 53) where
    "M ⇧c⊫⇩= φ ≡ close_world M ⊫ φ"


  lemma
    close_world_extensive: "M ⊆ close_world M" and
    close_world_idem[simp]: "close_world (close_world M) = close_world M"
    by (auto simp: close_world_def)

  lemma in_close_world_conv:
    "φ ∈ close_world M ⟷ (
        φ∈M
      ∨ (∃p as. φ=❙¬(Atom (predAtm p as)) ∧ Atom (predAtm p as)∉M)
      ∨ (∃a. φ=Atom (Eq a a))
      ∨ (∃a b. φ=❙¬(Atom (Eq a b)) ∧ a≠b)
    )"
    by (auto simp: close_world_def)

  lemma valuation_aux_1:
    fixes M :: world_model and φ :: "object atom formula"
    defines "C ≡ close_world M"
    assumes A: "∀φ∈C. 𝒜 ⊨ φ"
    shows "𝒜 = valuation M"
    using A unfolding C_def
    apply -
    apply (auto simp: in_close_world_conv valuation_def Ball_def intro!: ext split: atom.split)
    apply (metis formula_semantics.simps(1) formula_semantics.simps(3))
    apply (metis formula_semantics.simps(1) formula_semantics.simps(3))
    by (metis atom.collapse(2) formula_semantics.simps(1) is_predAtm_def)



  lemma valuation_aux_2:
    assumes "wm_basic M"
    shows "(∀G∈close_world M. valuation M ⊨ G)"
    using assms unfolding wm_basic_def
    by (force simp: in_close_world_conv valuation_def elim: is_predAtom.elims)

  lemma val_imp_close_world: "valuation M ⊨ φ ⟹ M ⇧c⊫⇩= φ"
    unfolding entailment_def
    using valuation_aux_1
    by blast

  lemma close_world_imp_val:
    "wm_basic M ⟹ M ⇧c⊫⇩= φ ⟹ valuation M ⊨ φ"
    unfolding entailment_def using valuation_aux_2 by blast

  text ‹Main theorem of this section:
    If a world model ‹M› contains only atoms, its induced valuation
    satisfies a formula ‹φ› if and only if the closure of ‹M› entails ‹φ›.

    Note that there are no syntactic restrictions on ‹φ›,
    in particular, ‹φ› may contain negation.
  ›
  theorem valuation_iff_close_world:
    assumes "wm_basic M"
    shows "valuation M ⊨ φ ⟷ M ⇧c⊫⇩= φ"
    using assms val_imp_close_world close_world_imp_val by blast


subsubsection ‹Proper Generalization›
text ‹Adding negation and equality is a proper generalization of the
  case without negation and equality›

fun is_STRIPS_fmla :: "'ent atom formula ⇒ bool" where
  "is_STRIPS_fmla (Atom (predAtm _ _)) ⟷ True"
| "is_STRIPS_fmla (⊥) ⟷ True"
| "is_STRIPS_fmla (φ⇩1 ❙∧ φ⇩2) ⟷ is_STRIPS_fmla φ⇩1 ∧ is_STRIPS_fmla φ⇩2"
| "is_STRIPS_fmla (φ⇩1 ❙∨ φ⇩2) ⟷ is_STRIPS_fmla φ⇩1 ∧ is_STRIPS_fmla φ⇩2"
| "is_STRIPS_fmla (❙¬⊥) ⟷ True"
| "is_STRIPS_fmla _ ⟷ False"

lemma aux1: "⟦wm_basic M; is_STRIPS_fmla φ; valuation M ⊨ φ; ∀G∈M. 𝒜 ⊨ G⟧ ⟹ 𝒜 ⊨ φ"
  apply(induction φ rule: is_STRIPS_fmla.induct)
  by (auto simp: valuation_def)

lemma aux2: "⟦wm_basic M; is_STRIPS_fmla φ; ∀𝒜. (∀G∈M. 𝒜 ⊨ G) ⟶ 𝒜 ⊨ φ⟧ ⟹ valuation M ⊨ φ"
  apply(induction φ rule: is_STRIPS_fmla.induct)
  apply simp_all
  apply (metis in_close_world_conv valuation_aux_2)
  using in_close_world_conv valuation_aux_2 apply blast
  using in_close_world_conv valuation_aux_2 by auto


lemma valuation_iff_STRIPS:
  assumes "wm_basic M"
  assumes "is_STRIPS_fmla φ"
  shows "valuation M ⊨ φ ⟷ M ⊫ φ"
proof -
  have aux1: "⋀𝒜. ⟦valuation M ⊨ φ; ∀G∈M. 𝒜 ⊨ G⟧ ⟹ 𝒜 ⊨ φ"
    using assms apply(induction φ rule: is_STRIPS_fmla.induct)
    by (auto simp: valuation_def)
  have aux2: "⟦∀𝒜. (∀G∈M. 𝒜 ⊨ G) ⟶ 𝒜 ⊨ φ⟧ ⟹ valuation M ⊨ φ"
    using assms
    apply(induction φ rule: is_STRIPS_fmla.induct)
    apply simp_all
    apply (metis in_close_world_conv valuation_aux_2)
    using in_close_world_conv valuation_aux_2 apply blast
    using in_close_world_conv valuation_aux_2 by auto
  show ?thesis
    by (auto simp: entailment_def intro: aux1 aux2)
qed

text ‹Our extension to negation and equality is a proper generalization of the
  standard STRIPS semantics for formula without negation and equality›
theorem proper_STRIPS_generalization:
  "⟦wm_basic M; is_STRIPS_fmla φ⟧ ⟹ M ⇧c⊫⇩= φ ⟷ M ⊫ φ"
  by (simp add: valuation_iff_close_world[symmetric] valuation_iff_STRIPS)

subsection ‹STRIPS Semantics›

text ‹For this section, we fix a domain ‹D›, using Isabelle's
  locale mechanism.›
locale ast_domain =
  fixes D :: ast_domain
begin
  text ‹It seems to be agreed upon that, in case of a contradictory effect,
    addition overrides deletion. We model this behaviour by first executing
    the deletions, and then the additions.›
  fun apply_effect :: "object ast_effect ⇒ world_model ⇒ world_model"
  where
     "apply_effect (Effect a d) s = (s - set d) ∪ (set a)"

  text ‹Execute a ground action›
  definition execute_ground_action :: "ground_action ⇒ world_model ⇒ world_model"
  where
    "execute_ground_action a M = apply_effect (effect a) M"

  text ‹Predicate to model that the given list of action instances is
    executable, and transforms an initial world model ‹M› into a final
    model ‹M'›.

    Note that this definition over the list structure is more convenient in HOL
    than to explicitly define an indexed sequence ‹M⇩0…M⇩N› of intermediate world
     models, as done in [Lif87].
  ›
  fun ground_action_path
    :: "world_model ⇒ ground_action list ⇒ world_model ⇒ bool"
  where
    "ground_action_path M [] M' ⟷ (M = M')"
  | "ground_action_path M (α#αs) M' ⟷ M ⇧c⊫⇩= precondition α
    ∧ ground_action_path (execute_ground_action α M) αs M'"

  text ‹Function equations as presented in paper,
    with inlined @{const execute_ground_action}.›
  lemma ground_action_path_in_paper:
    "ground_action_path M [] M' ⟷ (M = M')"
    "ground_action_path M (α#αs) M' ⟷ M ⇧c⊫⇩= precondition α
    ∧ (ground_action_path (apply_effect (effect α) M) αs M')"
    by (auto simp: execute_ground_action_def)

end ― ‹Context of ‹ast_domain››



subsection ‹Well-Formedness of PDDL›

(* Well-formedness *)

(*
  Compute signature: predicate/arity
  Check that all atoms (schemas and facts) satisfy signature

  for action:
    Check that used parameters ⊆ declared parameters

  for init/goal: Check that facts only use declared objects
*)


fun ty_term where
  "ty_term varT objT (term.VAR v) = varT v"
| "ty_term varT objT (term.CONST c) = objT c"


lemma ty_term_mono: "varT ⊆⇩m varT' ⟹ objT ⊆⇩m objT' ⟹
  ty_term varT objT ⊆⇩m ty_term varT' objT'"
  apply (rule map_leI)
  subgoal for x v
    apply (cases x)
    apply (auto dest: map_leD)
    done
  done


context ast_domain begin

  text ‹The signature is a partial function that maps the predicates
    of the domain to lists of argument types.›
  definition sig :: "predicate ⇀ type list" where
    "sig ≡ map_of (map (λPredDecl p n ⇒ (p,n)) (predicates D))"

  text ‹We use a flat subtype hierarchy, where every type is a subtype
    of object, and there are no other subtype relations.

    Note that we do not need to restrict this relation to declared types,
    as we will explicitly ensure that all types used in the problem are
    declared.
    ›

  fun subtype_edge where
    "subtype_edge (ty,superty) = (superty,ty)"

  definition "subtype_rel ≡ set (map subtype_edge (types D))"

  (*
  definition "subtype_rel ≡ {''object''}×UNIV"
  *)

  definition of_type :: "type ⇒ type ⇒ bool" where
    "of_type oT T ≡ set (primitives oT) ⊆ subtype_rel⇧* `` set (primitives T)"
  text ‹This checks that every primitive on the LHS is contained in or a
    subtype of a primitive on the RHS›


  text ‹For the next few definitions, we fix a partial function that maps
    a polymorphic entity type @{typ "'e"} to types. An entity can be
    instantiated by variables or objects later.›
  context
    fixes ty_ent :: "'ent ⇀ type"  ― ‹Entity's type, None if invalid›
  begin

    text ‹Checks whether an entity has a given type›
    definition is_of_type :: "'ent ⇒ type ⇒ bool" where
      "is_of_type v T ⟷ (
        case ty_ent v of
          Some vT ⇒ of_type vT T
        | None ⇒ False)"

    fun wf_pred_atom :: "predicate × 'ent list ⇒ bool" where
      "wf_pred_atom (p,vs) ⟷ (
        case sig p of
          None ⇒ False
        | Some Ts ⇒ list_all2 is_of_type vs Ts)"

    text ‹Predicate-atoms are well-formed if their arguments match the
      signature, equalities are well-formed if the arguments are valid
      objects (have a type).

      TODO: We could check that types may actually overlap
    ›
    fun wf_atom :: "'ent atom ⇒ bool" where
      "wf_atom (predAtm p vs) ⟷ wf_pred_atom (p,vs)"
    | "wf_atom (Eq a b) ⟷ ty_ent a ≠ None ∧ ty_ent b ≠ None"

    text ‹A formula is well-formed if it consists of valid atoms,
      and does not contain negations, except for the encoding ‹❙¬⊥› of true.
    ›
    fun wf_fmla :: "('ent atom) formula ⇒ bool" where
      "wf_fmla (Atom a) ⟷ wf_atom a"
    | "wf_fmla (⊥) ⟷ True"
    | "wf_fmla (φ1 ❙∧ φ2) ⟷ (wf_fmla φ1 ∧ wf_fmla φ2)"
    | "wf_fmla (φ1 ❙∨ φ2) ⟷ (wf_fmla φ1 ∧ wf_fmla φ2)"
    | "wf_fmla (❙¬φ) ⟷ wf_fmla φ"
    | "wf_fmla (φ1 ❙→ φ2) ⟷ (wf_fmla φ1 ∧ wf_fmla φ2)"

    lemma "wf_fmla φ = (∀a∈atoms φ. wf_atom a)"
      by (induction φ) auto

    (*lemma wf_fmla_add_simps[simp]: "wf_fmla (❙¬φ) ⟷ φ=⊥"
      by (cases φ) auto*)

    text ‹Special case for a well-formed atomic predicate formula›
    fun wf_fmla_atom where
      "wf_fmla_atom (Atom (predAtm a vs)) ⟷ wf_pred_atom (a,vs)"
    | "wf_fmla_atom _ ⟷ False"

    lemma wf_fmla_atom_alt: "wf_fmla_atom φ ⟷ is_predAtom φ ∧ wf_fmla φ"
      by (cases φ rule: wf_fmla_atom.cases) auto

    text ‹An effect is well-formed if the added and removed formulas
      are atomic›
    fun wf_effect where
      "wf_effect (Effect a d) ⟷
          (∀ae∈set a. wf_fmla_atom ae)
        ∧ (∀de∈set d.  wf_fmla_atom de)"

  end ― ‹Context fixing ‹ty_ent››


  definition constT :: "object ⇀ type" where
    "constT ≡ map_of (consts D)"

  text ‹An action schema is well-formed if the parameter names are distinct,
    and the precondition and effect is well-formed wrt.\ the parameters.
  ›
  fun wf_action_schema :: "ast_action_schema ⇒ bool" where
    "wf_action_schema (Action_Schema n params pre eff) ⟷ (
      let
        tyt = ty_term (map_of params) constT
      in
        distinct (map fst params)
      ∧ wf_fmla tyt pre
      ∧ wf_effect tyt eff)"

  text ‹A type is well-formed if it consists only of declared primitive types,
     and the type object.›
  fun wf_type where
    "wf_type (Either Ts) ⟷ set Ts ⊆ insert ''object'' (fst`set (types D))"

  text ‹A predicate is well-formed if its argument types are well-formed.›
  fun wf_predicate_decl where
    "wf_predicate_decl (PredDecl p Ts) ⟷ (∀T∈set Ts. wf_type T)"

  text ‹The types declaration is well-formed, if all supertypes are declared types (or object)›
  definition "wf_types ≡ snd`set (types D) ⊆ insert ''object'' (fst`set (types D))"

  text ‹A domain is well-formed if
    ▪ there are no duplicate declared predicate names,
    ▪ all declared predicates are well-formed,
    ▪ there are no duplicate action names,
    ▪ and all declared actions are well-formed
    ›
  definition wf_domain :: "bool" where
    "wf_domain ≡
      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 a)
    "

end ― ‹locale ‹ast_domain››

text ‹We fix a problem, and also include the definitions for the domain
  of this problem.›
locale ast_problem = ast_domain "domain P"
  for P :: ast_problem
begin
  text ‹We refer to the problem domain as ‹D››
  abbreviation "D ≡ ast_problem.domain P"

  definition objT :: "object ⇀ type" where
    "objT ≡ map_of (objects P) ++ constT"

  lemma objT_alt: "objT = map_of (consts D @ objects P)"
    unfolding objT_def constT_def
    apply (clarsimp)
    done

  definition wf_fact :: "fact ⇒ bool" where
    "wf_fact = wf_pred_atom objT"

  text ‹This definition is needed for well-formedness of the initial model,
    and forward-references to the concept of world model.
  ›
  definition wf_world_model where
    "wf_world_model M = (∀f∈M. wf_fmla_atom objT f)"

  (*Note: current semantics assigns each object a unique type *)
  definition wf_problem where
    "wf_problem ≡
      wf_domain
    ∧ distinct (map fst (objects P) @ map fst (consts D))
    ∧ (∀(n,T)∈set (objects P). wf_type T)
    ∧ distinct (init P)
    ∧ wf_world_model (set (init P))
    ∧ wf_fmla objT (goal P)
    "

  fun wf_effect_inst :: "object ast_effect ⇒ bool" where
    "wf_effect_inst (Effect (a) (d))
      ⟷ (∀a∈set a ∪ set d. wf_fmla_atom objT a)"

  lemma wf_effect_inst_alt: "wf_effect_inst eff = wf_effect objT eff"
    by (cases eff) auto

end ― ‹locale ‹ast_problem››

text ‹Locale to express a well-formed domain›
locale wf_ast_domain = ast_domain +
  assumes wf_domain: wf_domain

text ‹Locale to express a well-formed problem›
locale wf_ast_problem = ast_problem P for P +
  assumes wf_problem: wf_problem
begin
  sublocale wf_ast_domain "domain P"
    apply unfold_locales
    using wf_problem
    unfolding wf_problem_def by simp

end ― ‹locale ‹wf_ast_problem››

subsection ‹PDDL Semantics›

(* Semantics *)

(*  To apply plan_action:
    find action schema, instantiate, check precond, apply effect
*)



context ast_domain begin

  definition resolve_action_schema :: "name ⇀ ast_action_schema" where
    "resolve_action_schema n = index_by ast_action_schema.name (actions D) n"

  fun subst_term where
    "subst_term psubst (term.VAR x) = psubst x"
  | "subst_term psubst (term.CONST c) = c"

  text ‹To instantiate an action schema, we first compute a substitution from
    parameters to objects, and then apply this substitution to the
    precondition and effect. The substitution is applied via the ‹map_xxx›
    functions generated by the datatype package.
    ›
  fun instantiate_action_schema
    :: "ast_action_schema ⇒ object list ⇒ ground_action"
  where
    "instantiate_action_schema (Action_Schema n params pre eff) args = (let
        tsubst = subst_term (the o (map_of (zip (map fst params) args)));
        pre_inst = (map_formula o map_atom) tsubst pre;
        eff_inst = (map_ast_effect) tsubst eff
      in
        Ground_Action pre_inst eff_inst
      )"

end ― ‹Context of ‹ast_domain››


context ast_problem begin

  text ‹Initial model›
  definition I :: "world_model" where
    "I ≡ set (init P)"


  text ‹Resolve a plan action and instantiate the referenced action schema.›
  fun resolve_instantiate :: "plan_action ⇒ ground_action" where
    "resolve_instantiate (PAction n args) =
      instantiate_action_schema
        (the (resolve_action_schema n))
        args"

  text ‹Check whether object has specified type›
  definition "is_obj_of_type n T ≡ case objT n of
    None ⇒ False
  | Some oT ⇒ of_type oT T"

  text ‹We can also use the generic ‹is_of_type› function.›
  lemma is_obj_of_type_alt: "is_obj_of_type = is_of_type objT"
    apply (intro ext)
    unfolding is_obj_of_type_def is_of_type_def by auto


  text ‹HOL encoding of matching an action's formal parameters against an
    argument list.
    The parameters of the action are encoded as a list of ‹name×type› pairs,
    such that we map it to a list of types first. Then, the list
    relator @{const list_all2} checks that arguments and types have the same
    length, and each matching pair of argument and type
    satisfies the predicate @{const is_obj_of_type}.
  ›
  definition "action_params_match a args
    ≡ list_all2 is_obj_of_type args (map snd (parameters a))"

  text ‹At this point, we can define well-formedness of a plan action:
    The action must refer to a declared action schema, the arguments must
    be compatible with the formal parameters' types.
  ›
 (* Objects are valid and match parameter types *)
  fun wf_plan_action :: "plan_action ⇒ bool" where
    "wf_plan_action (PAction n args) = (
      case resolve_action_schema n of
        None ⇒ False
      | Some a ⇒
          action_params_match a args
        ∧ wf_effect_inst (effect (instantiate_action_schema a args))
        )"
  text ‹
    TODO: The second conjunct is redundant, as instantiating a well formed
      action with valid objects yield a valid effect.
  ›



  text ‹A sequence of plan actions form a path, if they are well-formed and
    their instantiations form a path.›
  definition plan_action_path
    :: "world_model ⇒ plan_action list ⇒ world_model ⇒ bool"
  where
    "plan_action_path M πs M' =
        ((∀π ∈ set πs. wf_plan_action π)
      ∧ ground_action_path M (map resolve_instantiate πs) M')"

  text ‹A plan is valid wrt.\ a given initial model, if it forms a path to a
    goal model ›
  definition valid_plan_from :: "world_model ⇒ plan ⇒ bool" where
    "valid_plan_from M πs = (∃M'. plan_action_path M πs M' ∧ M' ⇧c⊫⇩= (goal P))"

  (* Implementation note: resolve and instantiate already done inside
      enabledness check, redundancy! *)

  text ‹Finally, a plan is valid if it is valid wrt.\ the initial world
    model @{const I}›
  definition valid_plan :: "plan ⇒ bool"
    where "valid_plan ≡ valid_plan_from I"

  text ‹Concise definition used in paper:›
  lemma "valid_plan πs ≡ ∃M'. plan_action_path I πs M' ∧ M' ⇧c⊫⇩= (goal P)"
    unfolding valid_plan_def valid_plan_from_def by auto


end ― ‹Context of ‹ast_problem››



subsection ‹Preservation of Well-Formedness›

subsubsection ‹Well-Formed Action Instances›
text ‹The goal of this section is to establish that well-formedness of
  world models is preserved by execution of well-formed plan actions.
›

context ast_problem begin

  text ‹As plan actions are executed by first instantiating them, and then
    executing the action instance, it is natural to define a well-formedness
    concept for action instances.›

  fun wf_ground_action :: "ground_action ⇒ bool" where
    "wf_ground_action (Ground_Action pre eff) ⟷ (
        wf_fmla objT pre
      ∧ wf_effect objT eff
      )
    "

  text ‹We first prove that instantiating a well-formed action schema will yield
    a well-formed action instance.

    We begin with some auxiliary lemmas before the actual theorem.
  ›

  lemma (in ast_domain) of_type_refl[simp, intro!]: "of_type T T"
    unfolding of_type_def by auto

  lemma (in ast_domain) of_type_trans[trans]:
    "of_type T1 T2 ⟹ of_type T2 T3 ⟹ of_type T1 T3"
    unfolding of_type_def
    by clarsimp (metis (no_types, opaque_lifting)
      Image_mono contra_subsetD order_refl rtrancl_image_idem)

  lemma is_of_type_map_ofE:
    assumes "is_of_type (map_of params) x T"
    obtains i xT where "i<length params" "params!i = (x,xT)" "of_type xT T"
    using assms
    unfolding is_of_type_def
    by (auto split: option.splits dest!: map_of_SomeD simp: in_set_conv_nth)

  lemma wf_atom_mono:
    assumes SS: "tys ⊆⇩m tys'"
    assumes WF: "wf_atom tys a"
    shows "wf_atom tys' a"
  proof -
    have "list_all2 (is_of_type tys') xs Ts" if "list_all2 (is_of_type tys) xs Ts" for xs Ts
      using that
      apply induction
      by (auto simp: is_of_type_def split: option.splits dest: map_leD[OF SS])
    with WF show ?thesis
      by (cases a) (auto split: option.splits dest: map_leD[OF SS])
  qed

  lemma wf_fmla_atom_mono:
    assumes SS: "tys ⊆⇩m tys'"
    assumes WF: "wf_fmla_atom tys a"
    shows "wf_fmla_atom tys' a"
  proof -
    have "list_all2 (is_of_type tys') xs Ts" if "list_all2 (is_of_type tys) xs Ts" for xs Ts
      using that
      apply induction
      by (auto simp: is_of_type_def split: option.splits dest: map_leD[OF SS])
    with WF show ?thesis
      by (cases a rule: wf_fmla_atom.cases) (auto split: option.splits dest: map_leD[OF SS])
  qed


  lemma constT_ss_objT: "constT ⊆⇩m objT"
    unfolding constT_def objT_def
    apply rule
    by (auto simp: map_add_def split: option.split)

  lemma wf_atom_constT_imp_objT: "wf_atom (ty_term Q constT) a ⟹ wf_atom (ty_term Q objT) a"
    apply (erule wf_atom_mono[rotated])
    apply (rule ty_term_mono)
    by (simp_all add: constT_ss_objT)

  lemma wf_fmla_atom_constT_imp_objT: "wf_fmla_atom (ty_term Q constT) a ⟹ wf_fmla_atom (ty_term Q objT) a"
    apply (erule wf_fmla_atom_mono[rotated])
    apply (rule ty_term_mono)
    by (simp_all add: constT_ss_objT)

  context
    fixes Q and f :: "variable ⇒ object"
    assumes INST: "is_of_type Q x T ⟹ is_of_type objT (f x) T"
  begin

    lemma is_of_type_var_conv: "is_of_type (ty_term Q objT) (term.VAR x) T  ⟷ is_of_type Q x T"
      unfolding is_of_type_def by (auto)

    lemma is_of_type_const_conv: "is_of_type (ty_term Q objT) (term.CONST x) T  ⟷ is_of_type objT x T"
      unfolding is_of_type_def
      by (auto split: option.split)

    lemma INST': "is_of_type (ty_term Q objT) x T ⟹ is_of_type objT (subst_term f x) T"
      apply (cases x) using INST apply (auto simp: is_of_type_var_conv is_of_type_const_conv)
      done


    lemma wf_inst_eq_aux: "Q x = Some T ⟹ objT (f x) ≠ None"
      using INST[of x T] unfolding is_of_type_def
      by (auto split: option.splits)

    lemma wf_inst_eq_aux': "ty_term Q objT x = Some T ⟹ objT (subst_term f x) ≠ None"
      by (cases x) (auto simp: wf_inst_eq_aux)


    lemma wf_inst_atom:
      assumes "wf_atom (ty_term Q constT) a"
      shows "wf_atom objT (map_atom (subst_term f) a)"
    proof -
      have X1: "list_all2 (is_of_type objT) (map (subst_term f) xs) Ts" if
        "list_all2 (is_of_type (ty_term Q objT)) xs Ts" for xs Ts
        using that
        apply induction
        using INST'
        by auto
      then show ?thesis
        using assms[THEN wf_atom_constT_imp_objT] wf_inst_eq_aux'
        by (cases a; auto split: option.splits)

    qed

    lemma wf_inst_formula_atom:
      assumes "wf_fmla_atom (ty_term Q constT) a"
      shows "wf_fmla_atom objT ((map_formula o map_atom o subst_term) f a)"
      using assms[THEN wf_fmla_atom_constT_imp_objT] wf_inst_atom
      apply (cases a rule: wf_fmla_atom.cases; auto split: option.splits)
      by (simp add: INST' list.rel_map(1) list_all2_mono)

    lemma wf_inst_effect:
      assumes "wf_effect (ty_term Q constT) φ"
      shows "wf_effect objT ((map_ast_effect o subst_term) f φ)"
      using assms
      proof (induction φ)
        case (Effect x1a x2a)
        then show ?case using wf_inst_formula_atom by auto
      qed

    lemma wf_inst_formula:
      assumes "wf_fmla (ty_term Q constT) φ"
      shows "wf_fmla objT ((map_formula o map_atom o subst_term) f φ)"
      using assms
      by (induction φ) (auto simp: wf_inst_atom dest: wf_inst_eq_aux)

  end



  text ‹Instantiating a well-formed action schema with compatible arguments
    will yield a well-formed action instance.
  ›
  theorem wf_instantiate_action_schema:
    assumes "action_params_match a args"
    assumes "wf_action_schema a"
    shows "wf_ground_action (instantiate_action_schema a args)"
  proof (cases a)
    case [simp]: (Action_Schema name params pre eff)
    have INST:
      "is_of_type objT ((the ∘ map_of (zip (map fst params) args)) x) T"
      if "is_of_type (map_of params) x T" for x T
      using that
      apply (rule is_of_type_map_ofE)
      using assms
      apply (clarsimp simp: Let_def)
      subgoal for i xT
        unfolding action_params_match_def
        apply (subst lookup_zip_idx_eq[where i=i];
          (clarsimp simp: list_all2_lengthD)?)
        apply (frule list_all2_nthD2[where p=i]; simp?)
        apply (auto
                simp: is_obj_of_type_alt is_of_type_def
                intro: of_type_trans
                split: option.splits)
        done
      done
    then show ?thesis
      using assms(2) wf_inst_formula wf_inst_effect
      by (fastforce split: term.splits simp: Let_def comp_apply[abs_def])
  qed
end ― ‹Context of ‹ast_problem››



subsubsection ‹Preservation›

context ast_problem begin

  text ‹We start by defining two shorthands for enabledness and execution of
    a plan action.›

  text ‹Shorthand for enabled plan action: It is well-formed, and the
    precondition holds for its instance.›
  definition plan_action_enabled :: "plan_action ⇒ world_model ⇒ bool" where
    "plan_action_enabled π M
      ⟷ wf_plan_action π ∧ M ⇧c⊫⇩= precondition (resolve_instantiate π)"

  text ‹Shorthand for executing a plan action: Resolve, instantiate, and
    apply effect›
  definition execute_plan_action :: "plan_action ⇒ world_model ⇒ world_model"
    where "execute_plan_action π M
      = (apply_effect (effect (resolve_instantiate π)) M)"

  text ‹The @{const plan_action_path} predicate can be decomposed naturally
    using these shorthands: ›
  lemma plan_action_path_Nil[simp]: "plan_action_path M [] M' ⟷ M'=M"
    by (auto simp: plan_action_path_def)

  lemma plan_action_path_Cons[simp]:
    "plan_action_path M (π#πs) M' ⟷
      plan_action_enabled π M
    ∧ plan_action_path (execute_plan_action π M) πs M'"
    by (auto
      simp: plan_action_path_def execute_plan_action_def
            execute_ground_action_def plan_action_enabled_def)



end ― ‹Context of ‹ast_problem››

context wf_ast_problem begin
  text ‹The initial world model is well-formed›
  lemma wf_I: "wf_world_model I"
    using wf_problem
    unfolding I_def wf_world_model_def wf_problem_def
    apply(safe) subgoal for f by (induction f) auto
    done

  text ‹Application of a well-formed effect preserves well-formedness
    of the model›
  lemma wf_apply_effect:
    assumes "wf_effect objT e"
    assumes "wf_world_model s"
    shows "wf_world_model (apply_effect e s)"
    using assms wf_problem
    unfolding wf_world_model_def wf_problem_def wf_domain_def
    by (cases e) (auto split: formula.splits prod.splits)

  text ‹Execution of plan actions preserves well-formedness›
  theorem wf_execute:
    assumes "plan_action_enabled π s"
    assumes "wf_world_model s"
    shows "wf_world_model (execute_plan_action π s)"
    using assms
  proof (cases π)
    case [simp]: (PAction name args)

    from ‹plan_action_enabled π s› have "wf_plan_action π"
      unfolding plan_action_enabled_def by auto
    then obtain a where
      "resolve_action_schema name = Some a" and
      T: "action_params_match a args"
      by (auto split: option.splits)

    from wf_domain have
      [simp]: "distinct (map ast_action_schema.name (actions D))"
      unfolding wf_domain_def by auto

    from ‹resolve_action_schema name = Some a› have
      "a ∈ set (actions D)"
      unfolding resolve_action_schema_def by auto
    with wf_domain have "wf_action_schema a"
      unfolding wf_domain_def by auto
    hence "wf_ground_action (resolve_instantiate π)"
      using ‹resolve_action_schema name = Some a› T
        wf_instantiate_action_schema
      by auto
    thus ?thesis
      apply (simp add: execute_plan_action_def execute_ground_action_def)
      apply (rule wf_apply_effect)
      apply (cases "resolve_instantiate π"; simp)
      by (rule ‹wf_world_model s›)
  qed

  theorem wf_execute_compact_notation:
    "plan_action_enabled π s ⟹ wf_world_model s
    ⟹ wf_world_model (execute_plan_action π s)"
    by (rule wf_execute)


  text ‹Execution of a plan preserves well-formedness›
  corollary wf_plan_action_path:
    assumes "wf_world_model M" and " plan_action_path M πs M'"
    shows "wf_world_model M'"
    using assms
    by (induction πs arbitrary: M) (auto intro: wf_execute)


end ― ‹Context of ‹wf_ast_problem››




end ― ‹Theory›