Theory STRIPS_Representation

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory STRIPS_Representation
  imports State_Variable_Representation
begin

section "STRIPS Representation"

(*<*)
type_synonym  ('variable) strips_state = "('variable, bool) state"
(*>*)
text ‹ We start by declaring a \isakeyword{record} for STRIPS operators.
This which allows us to define a data type and automatically generated selector operations. 
\footnote{For the full reference on records see \<^cite>‹‹11.6, pp.260-265› in "wenzel--2018"›} 

The record specification given below closely resembles the canonical representation of
STRIPS operators with fields corresponding to precondition, add effects as well as delete effects.›

record  ('variable) strips_operator = 
  precondition_of :: "'variable list" 
  add_effects_of :: "'variable list" 
  delete_effects_of :: "'variable list" 

― ‹ This constructor function is sometimes a more descriptive and replacement for the record 
syntax and can moreover be helpful if the record syntax leads to type ambiguity.›
abbreviation  operator_for
  :: "'variable list ⇒ 'variable list ⇒ 'variable list ⇒ 'variable strips_operator"
  where "operator_for pre add delete ≡ ⦇ 
    precondition_of = pre
    , add_effects_of = add
    , delete_effects_of = delete ⦈" 

definition  to_precondition
  :: "'variable strips_operator ⇒ ('variable, bool) assignment list"
  where "to_precondition op ≡ map (λv. (v, True)) (precondition_of op)" 

definition  to_effect
  :: "'variable strips_operator ⇒ ('variable, bool) Effect" 
  where "to_effect op =  [(v⇩a, True). v⇩a ← add_effects_of op] @ [(v⇩d, False). v⇩d ← delete_effects_of op]"

text ‹ Similar to the operator definition, we use a record to represent STRIPS problems and specify
fields for the variables, operators, as well as the initial and goal state. ›

record  ('variable) strips_problem =
  variables_of :: "'variable list" ("(_⇩𝒱)" [1000] 999)
  operators_of :: "'variable strips_operator list" ("(_⇩𝒪)" [1000] 999)
  initial_of :: "'variable strips_state" ("(_⇩I)" [1000] 999)
  goal_of :: "'variable strips_state" ("(_⇩G)" [1000] 999)

value  "stop" (* Tell document preparation to stop collecting for the last tag *)
(*<*)
― ‹ This constructor function is sometimes a more descriptive and replacement for the record 
syntax and can moreover be helpful if the record syntax leads to type ambiguity.›
(* TODO change identifier gs ~> G *)
abbreviation problem_for 
  :: "'variable list 
  ⇒ 'variable strips_operator list 
  ⇒ 'variable strips_state 
  ⇒ 'variable strips_state
  ⇒ ('variable) strips_problem"
  where "problem_for vs ops I gs ≡ ⦇ 
    variables_of = vs
    , operators_of = ops
    , initial_of = I
    , goal_of = gs ⦈" 

type_synonym ('variable) strips_plan = "'variable strips_operator list"

type_synonym ('variable) strips_parallel_plan = "'variable strips_operator list list"

definition is_valid_operator_strips
  :: "'variable strips_problem ⇒ 'variable strips_operator ⇒ bool"
  where "is_valid_operator_strips Π op ≡ let 
      vs = variables_of Π 
      ; pre = precondition_of op
      ; add = add_effects_of op
      ; del = delete_effects_of op
    in list_all (λv. ListMem v vs) pre 
    ∧ list_all (λv. ListMem v vs) add
    ∧ list_all (λv. ListMem v vs) del
    ∧ list_all (λv. ¬ListMem v del) add
    ∧ list_all (λv. ¬ListMem v add) del"

definition "is_valid_problem_strips Π
  ≡ let ops = operators_of Π
      ; vs = variables_of Π
      ; I = initial_of Π
      ; G = goal_of Π
    in  list_all (is_valid_operator_strips Π) ops 
    ∧ (∀v. I v ≠ None ⟷ ListMem v vs) 
    ∧ (∀v. G v ≠ None ⟶ ListMem v vs)"

definition is_operator_applicable_in
  :: "'variable strips_state ⇒ 'variable strips_operator ⇒ bool"
  where "is_operator_applicable_in s op ≡ let p = precondition_of op in
    list_all (λv. s v = Some True) p"

(* TODO effect_to_strips and effect_to_assignments could just be removed if we prove a lemma 
  showing the equivalence to effcond semantics.*)
definition effect__strips 
  :: "'variable strips_operator ⇒ ('variable, bool) Effect"
  where "effect__strips op 
    = 
      map (λv. (v, True)) (add_effects_of op)
      @ map (λv. (v, False)) (delete_effects_of op)"

definition effect_to_assignments 
  where "effect_to_assignments op ≡ effect__strips op"
(*>*)

text ‹ As discussed in \autoref{sub:serial-sas-plus-and-parallel-strips}, the effect of
a STRIPS operator can be normalized to a conjunction of atomic effects. We can therefore construct 
the successor state by simply converting the list of add effects to assignments to \<^term>‹True› resp. 
converting the list of delete effect to a list of assignments to \<^term>‹False› and then adding the 
map corresponding to the assignments to the given state \<^term>‹s› as shown below in definition 
\ref{isadef:operator-execution-strips}. 
\footnote{Function \path{effect_to_assignments} converts the operator effect to a list of 
assignments. }›

definition  execute_operator
  :: "'variable strips_state 
    ⇒ 'variable strips_operator 
    ⇒ 'variable strips_state" (infixl "⪢" 52)
  where "execute_operator s op
    ≡ s ++ map_of (effect_to_assignments op)"

end