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 =  [(va, True). va  add_effects_of op] @ [(vd, False). vd  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 termTrue resp. 
converting the list of delete effect to a list of assignments to termFalse and then adding the 
map corresponding to the assignments to the given state terms 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