Theory SASP_Semantics

theory SASP_Semantics
imports Main
begin

section ‹Semantics of Fast-Downward's Multi-Valued Planning Tasks Language›

subsection ‹Syntax›
  type_synonym name = string
  type_synonym ast_variable = "name × nat option × name list" (* var name, axiom layer, atom names *)
  type_synonym ast_variable_section = "ast_variable list"
  type_synonym ast_initial_state = "nat list"
  type_synonym ast_goal = "(nat × nat) list"
  type_synonym ast_precond = "(nat × nat)"
  type_synonym ast_effect = "ast_precond list × nat × nat option × nat"
  type_synonym ast_operator = "name × ast_precond list × ast_effect list × nat"
  type_synonym ast_operator_section = "ast_operator list"
  
  type_synonym ast_problem = 
    "ast_variable_section × ast_initial_state × ast_goal × ast_operator_section"

  type_synonym plan = "name list"
    
  subsubsection ‹Well-Formedness›
    
  locale ast_problem =
    fixes problem :: ast_problem
  begin    
    definition astDom :: ast_variable_section (* TODO: Dom → Vars, D → X*)
      where "astDom  case problem of (D,I,G,δ)  D"
    definition astI :: ast_initial_state
      where "astI  case problem of (D,I,G,δ)  I"
    definition astG :: ast_goal
      where "astG  case problem of (D,I,G,δ)  G"
    definition astδ :: ast_operator_section
      where "astδ  case problem of (D,I,G,δ)  δ"
    
    definition "numVars  length astDom"
    definition "numVals x  length (snd (snd (astDom!x)))"

    definition "wf_partial_state ps  
        distinct (map fst ps) 
       ((x,v)  set ps. x < numVars  v < numVals x)"
      
    definition wf_operator :: "ast_operator  bool" 
      where "wf_operator  λ(name, pres, effs, cost). 
        wf_partial_state pres 
       distinct (map (λ(_, v, _, _). v) effs) ― ‹This may be too restrictive›
       ((epres,x,vp,v)set effs. 
          wf_partial_state epres 
         x < numVars  v < numVals x  
         (case vp of None  True | Some v  v<numVals x)
        )
    "
      
    definition "well_formed  
      ― ‹Initial state›
      length astI = numVars
     (x<numVars. astI!x < numVals x)

      ― ‹Goal›
     wf_partial_state astG

    ― ‹Operators›
     (distinct (map fst astδ))
     (πset astδ. wf_operator π)
    "
      
  end  
  
  locale wf_ast_problem = ast_problem +
    assumes wf: well_formed
  begin
    lemma wf_initial: 
      "length astI = numVars" 
      "x<numVars. astI!x < numVals x"
      using wf unfolding well_formed_def by auto

    lemma wf_goal: "wf_partial_state astG"    
      using wf unfolding well_formed_def by auto

    lemma wf_operators: 
      "distinct (map fst astδ)"
      "πset astδ. wf_operator π"
      using wf unfolding well_formed_def by auto
  end      
    
    
  subsection ‹Semantics as Transition System›  
    
  type_synonym state = "nat  nat"
  type_synonym pstate = "nat  nat"
    
    
  context ast_problem
  begin    
    
    definition Dom :: "nat set" where "Dom = {0..<numVars}"

    definition range_of_var where "range_of_var x  {0..<numVals x}"

    definition valid_states :: "state set" where "valid_states  {
      s. dom s = Dom  (xDom. the (s x)  range_of_var x)
    }"

    definition I :: state 
      where "I v  if v<length astI then Some (astI!v) else None"

    definition subsuming_states :: "pstate  state set"
      where "subsuming_states partial  { svalid_states. partial m s }"

    definition G :: "state set" 
      where "G  subsuming_states (map_of astG)"
end

    definition implicit_pres :: "ast_effect list  ast_precond list" where 
      "implicit_pres effs  
      map (λ(_,v,vpre,_). (v,the vpre))
          (filter (λ(_,_,vpre,_). vpreNone) effs)"

context ast_problem
begin

    definition lookup_operator :: "name  ast_operator option" where
      "lookup_operator name  find (λ(n,_,_,_). n=name) astδ"

    definition enabled :: "name  state  bool"
      where "enabled name s 
        case lookup_operator name of
          Some (_,pres,effs,_)  
              ssubsuming_states (map_of pres)
             ssubsuming_states (map_of (implicit_pres effs))
        | None  False"
      
    definition eff_enabled :: "state  ast_effect  bool" where
      "eff_enabled s  λ(pres,_,_,_). ssubsuming_states (map_of pres)"

    definition execute :: "name  state  state" where
      "execute name s  
        case lookup_operator name of
          Some (_,_,effs,_) 
            s ++ map_of (map (λ(_,x,_,v). (x,v)) (filter (eff_enabled s) effs))
        | None  undefined                                    
        "

    fun path_to where
      "path_to s [] s'  s'=s"
    | "path_to s (π#πs) s'  enabled π s  path_to (execute π s) πs s'"

    definition valid_plan :: "plan  bool" 
      where "valid_plan πs  s'G. path_to I πs s'"


  end

  (*
    Next steps:
      * well-formed stuff
      * Executable SAS+ validator (well_formed and execute function)

  *)  
    
  subsubsection ‹Preservation of well-formedness›  
  context wf_ast_problem 
  begin      
    lemma I_valid: "I  valid_states"
      using wf_initial 
      unfolding valid_states_def Dom_def I_def range_of_var_def
      by (auto split:if_splits)
      
    lemma lookup_operator_wf:
      assumes "lookup_operator name = Some π"
      shows "wf_operator π" "fst π = name"  
    proof -
      obtain name' pres effs cost where [simp]: "π=(name',pres,effs,cost)" by (cases π)
      hence [simp]: "name'=name" and IN_AST: "(name,pres,effs,cost)  set astδ"
        using assms
        unfolding lookup_operator_def
        apply -
        apply (metis (mono_tags, lifting) case_prodD find_Some_iff)  
        by (metis (mono_tags, lifting) case_prodD find_Some_iff nth_mem)  
      
      from IN_AST show WF: "wf_operator π" "fst π = name"   
        unfolding enabled_def using wf_operators by auto
    qed
        
        
    lemma execute_preserves_valid:
      assumes "svalid_states"  
      assumes "enabled name s"  
      shows "execute name s  valid_states"  
    proof -
      from enabled name s obtain name' pres effs cost where
        [simp]: "lookup_operator name = Some (name',pres,effs,cost)"
        unfolding enabled_def by (auto split: option.splits)
      from lookup_operator_wf[OF this] have WF: "wf_operator (name,pres,effs,cost)" by simp   
      
      have X1: "s ++ m  valid_states" if "x v. m x = Some v  x<numVars  v<numVals x" for m
        using that svalid_states
        by (auto 
            simp: valid_states_def Dom_def range_of_var_def map_add_def dom_def 
            split: option.splits)  
      
      have X2: "x<numVars" "v<numVals x" 
        if "map_of (map (λ(_, x, _, y). (x, y)) (filter (eff_enabled s) effs)) x = Some v"    
        for x v
      proof -
        from that obtain epres vp where "(epres,x,vp,v)  set effs"
          by (auto dest!: map_of_SomeD)
        with WF show "x<numVars" "v<numVals x"
          unfolding wf_operator_def by auto
      qed
          
      show ?thesis
        using assms  
        unfolding enabled_def execute_def 
        by (auto intro!: X1 X2)
    qed      
    
    lemma path_to_pres_valid:
      assumes "svalid_states"
      assumes "path_to s πs s'"
      shows "s'valid_states"
      using assms
      by (induction s πs s' rule: path_to.induct) (auto simp: execute_preserves_valid)  
      
  end

end