Theory AI_Planning_Languages_Semantics.SASP_Checker

theory SASP_Checker
imports SASP_Semantics
  "HOL-Library.Code_Target_Nat"
begin

section ‹An Executable Checker for Multi-Valued Planning Problem Solutions›


  subsection ‹Auxiliary Lemmas›
  lemma map_of_leI:
    assumes "distinct (map fst l)"
    assumes "k v. (k,v)set l  m k = Some v"
    shows "map_of l m m"  
    using assms
    by (metis (no_types, opaque_lifting) domIff map_le_def map_of_SomeD not_Some_eq)  

  lemma [simp]: "fst  (λ(a, b, c, d). (f a b c d, g a b c d)) = (λ(a,b,c,d). f a b c d)"
    by auto
      
  lemma map_mp: "mmm'  m k = Some v  m' k = Some v"    
    by (auto simp: map_le_def dom_def)
      
      
  lemma map_add_map_of_fold: 
    fixes ps and m :: "'a  'b"
    assumes "distinct (map fst ps)"
    shows "m ++ map_of ps = fold (λ(k, v) m. m(k  v)) ps m"
  proof -
    have X1: "(fold (λ(k, v) m. m(k  v)) ps m)(a  b) 
            = fold (λ(k, v) m. m(k  v)) ps (m(a  b))" 
      if "a  fst ` set ps"
      for a b ps and m :: "'a  'b"
      using that
      by (induction ps arbitrary: m) (auto simp: fun_upd_twist)
    
    show ?thesis
      using assms
      by (induction ps arbitrary: m) (auto simp: X1)
  qed    

  

  subsection ‹Well-formedness Check›
  lemmas wf_code_thms = 
      ast_problem.astDom_def ast_problem.astI_def ast_problem.astG_def ast_problem.astδ_def
      ast_problem.numVars_def ast_problem.numVals_def 
      ast_problem.wf_partial_state_def ast_problem.wf_operator_def ast_problem.well_formed_def
      
      
  declare wf_code_thms[code]
      
  export_code ast_problem.well_formed in SML

    
  subsection ‹Execution›  
    
  definition match_pre :: "ast_precond  state  bool" where
    "match_pre  λ(x,v) s. s x = Some v"
    
  definition match_pres :: "ast_precond list  state  bool" where 
    "match_pres pres s  preset pres. match_pre pre s"
    
  definition match_implicit_pres :: "ast_effect list  state  bool" where
    "match_implicit_pres effs s  (_,x,vp,_)set effs. 
      (case vp of None  True | Some v  s x = Some v)"
    
  definition enabled_opr' :: "ast_operator  state  bool" where 
    "enabled_opr'  λ(name,pres,effs,cost) s. match_pres pres s  match_implicit_pres effs s"
      
  definition eff_enabled' :: "state  ast_effect  bool" where
    "eff_enabled' s  λ(pres,_,_,_). match_pres pres s"
    
  definition "execute_opr'  λ(name,_,effs,_) s. 
    let effs = filter (eff_enabled' s) effs
    in fold (λ(_,x,_,v) s. s(xv)) effs s
  "  

  definition lookup_operator' :: "ast_problem  name  ast_operator" 
    where "lookup_operator'  λ(D,I,G,δ) name. find (λ(n,_,_,_). n=name) δ"
    
  definition enabled' :: "ast_problem  name  state  bool" where
    "enabled' problem name s  
      case lookup_operator' problem name of 
        Some π  enabled_opr' π s
      | None  False"

  definition execute' :: "ast_problem  name  state  state" where
    "execute' problem name s  
      case lookup_operator' problem name of 
        Some π  execute_opr' π s
      | None  undefined"
    
    
  context wf_ast_problem begin  
    
    lemma match_pres_correct:
      assumes D: "distinct (map fst pres)"
      assumes "svalid_states"  
      shows "match_pres pres s  ssubsuming_states (map_of pres)"
    proof -
      have "match_pres pres s  map_of pres m s"
        unfolding match_pres_def match_pre_def
        apply (auto split: prod.splits)
        using map_le_def map_of_SomeD apply fastforce  
        by (metis (full_types) D domIff map_le_def map_of_eq_Some_iff option.simps(3))
    
      with assms show ?thesis          
        unfolding subsuming_states_def 
        by auto
    qed
       
    lemma match_implicit_pres_correct:
      assumes D: "distinct (map (λ(_, v, _, _). v) effs)"
      assumes "svalid_states"  
      shows "match_implicit_pres effs s  ssubsuming_states (map_of (implicit_pres effs))"
    proof -
      from assms show ?thesis
        unfolding subsuming_states_def 
        unfolding match_implicit_pres_def implicit_pres_def
        apply (auto 
            split: prod.splits option.splits 
            simp: distinct_map_filter
            intro!: map_of_leI)
        apply (force simp: distinct_map_filter split: prod.split elim: map_mp)  
        done  
    qed
          
    lemma enabled_opr'_correct:
      assumes V: "svalid_states"
      assumes "lookup_operator name = Some π"  
      shows "enabled_opr' π s  enabled name s"  
      using lookup_operator_wf[OF assms(2)] assms
      unfolding enabled_opr'_def enabled_def wf_operator_def
      by (auto 
          simp: match_pres_correct[OF _ V] match_implicit_pres_correct[OF _ V]
          simp: wf_partial_state_def
          split: option.split
          )  
       
    lemma eff_enabled'_correct:
      assumes V: "svalid_states"
      assumes "case eff of (pres,_,_,_)  wf_partial_state pres"  
      shows "eff_enabled' s eff  eff_enabled s eff"  
      using assms  
      unfolding eff_enabled'_def eff_enabled_def wf_partial_state_def
      by (auto simp: match_pres_correct)  
    
    
    lemma execute_opr'_correct:
      assumes V: "svalid_states"
      assumes LO: "lookup_operator name = Some π"  
      shows "execute_opr' π s = execute name s"  
    proof (cases π)
      case [simp]: (fields name pres effs)
        
      have [simp]: "filter (eff_enabled' s) effs = filter (eff_enabled s) effs"  
        apply (rule filter_cong[OF refl])
        apply (rule eff_enabled'_correct[OF V])
        using lookup_operator_wf[OF LO]  
        unfolding wf_operator_def by auto  
          
      have X1: "distinct (map fst (map (λ(_, x, _, y). (x, y)) (filter (eff_enabled s) effs)))"
        using lookup_operator_wf[OF LO]
        unfolding wf_operator_def 
        by (auto simp: distinct_map_filter)
        
      term "filter (eff_enabled s) effs"    
          
      have [simp]: 
        "fold (λ(_, x, _, v) s. s(x  v)) l s =
         fold (λ(k, v) m. m(k  v)) (map (λ(_, x, _, y). (x, y)) l) s" 
        for l :: "ast_effect list"
        by (induction l arbitrary: s) auto
          
      show ?thesis 
        unfolding execute_opr'_def execute_def using LO
        by (auto simp: map_add_map_of_fold[OF X1])
    qed
        
      
    lemma lookup_operator'_correct: 
      "lookup_operator' problem name = lookup_operator name"
      unfolding lookup_operator'_def lookup_operator_def
      unfolding astδ_def  
      by (auto split: prod.split)  
        
    lemma enabled'_correct:
      assumes V: "svalid_states"
      shows "enabled' problem name s = enabled name s"
      unfolding enabled'_def  
      using enabled_opr'_correct[OF V]
      by (auto split: option.splits simp: enabled_def lookup_operator'_correct)  
        
    lemma execute'_correct:
      assumes V: "svalid_states"
      assumes "enabled name s"      (* Intentionally put this here, also we could resolve non-enabled case by reflexivity (undefined=undefined) *)
      shows "execute' problem name s = execute name s"  
      unfolding execute'_def  
      using execute_opr'_correct[OF V] enabled name s
      by (auto split: option.splits simp: enabled_def lookup_operator'_correct)  
        
        
        
  end    

  context ast_problem 
  begin  
    
    fun simulate_plan :: "plan  state  state" where
      "simulate_plan [] s = Some s"
    | "simulate_plan (π#πs) s = (
        if enabled π s then 
          let s' = execute π s in
          simulate_plan πs s'
        else
          None
      )"  
    
    lemma simulate_plan_correct: "simulate_plan πs s = Some s'  path_to s πs s'"
      by (induction s πs s' rule: path_to.induct) auto  
      
    definition check_plan :: "plan  bool" where
      "check_plan πs = (
        case simulate_plan πs I of 
          None  False 
        | Some s'  s'  G)"
      
    lemma check_plan_correct: "check_plan πs  valid_plan πs"
      unfolding check_plan_def valid_plan_def 
      by (auto split: option.split simp: simulate_plan_correct[symmetric])
      
  end  
    
  fun simulate_plan' :: "ast_problem  plan  state  state" where
    "simulate_plan' problem [] s = Some s"
  | "simulate_plan' problem (π#πs) s = (
      if enabled' problem π s then
        let s = execute' problem π s in
        simulate_plan' problem πs s
      else
        None
    )"  
    
  text ‹Avoiding duplicate lookup.›
  (*[code]  *)  
  lemma simulate_plan'_code[code]:
    "simulate_plan' problem [] s = Some s"
    "simulate_plan' problem (π#πs) s = (
      case lookup_operator' problem π of
        None  None
      | Some π  
          if enabled_opr' π s then 
            simulate_plan' problem πs (execute_opr' π s)
          else None
    )"
    by (auto simp: enabled'_def execute'_def split: option.split)
    
    
  definition initial_state' :: "ast_problem  state" where
    "initial_state' problem  let astI = ast_problem.astI problem in (
       λv. if v<length astI then Some (astI!v) else None
     )"
      
  definition check_plan' :: "ast_problem  plan  bool" where
    "check_plan' problem πs = (
      case simulate_plan' problem πs (initial_state' problem) of 
        None  False 
      | Some s'  match_pres (ast_problem.astG problem) s')"
      
      
  context wf_ast_problem 
  begin  
    
    lemma simulate_plan'_correct:
      assumes "svalid_states"
      shows "simulate_plan' problem πs s = simulate_plan πs s"
      using assms
      apply (induction πs s rule: simulate_plan.induct)
      apply (auto simp: enabled'_correct execute'_correct execute_preserves_valid)  
      done
        
    lemma simulate_plan'_correct_paper: (* For presentation in paper. 
        Summarizing intermediate refinement step. *)
      assumes "svalid_states"
      shows "simulate_plan' problem πs s = Some s'
             path_to s πs s'"
      using simulate_plan'_correct[OF assms] simulate_plan_correct by simp
      
        
    lemma initial_state'_correct: 
      "initial_state' problem = I"
      unfolding initial_state'_def I_def by (auto simp: Let_def)

    lemma check_plan'_correct:
      "check_plan' problem πs = check_plan πs"
    proof -
      have D: "distinct (map fst astG)" using wf_goal unfolding wf_partial_state_def by auto 
        
      have S'V: "s'valid_states" if "simulate_plan πs I = Some s'" for s'
        using that by (auto simp: simulate_plan_correct path_to_pres_valid[OF I_valid])
          
      show ?thesis
        unfolding check_plan'_def check_plan_def
        by (auto 
            split: option.splits 
            simp: initial_state'_correct simulate_plan'_correct[OF I_valid]
            simp: match_pres_correct[OF D S'V] G_def
            )
    qed  
        
  end

    
  (* Overall checker *)  
    
  definition verify_plan :: "ast_problem  plan  String.literal + unit" where
    "verify_plan problem πs = (
      if ast_problem.well_formed problem then
        if check_plan' problem πs then Inr () else Inl (STR ''Invalid plan'')
      else Inl (STR ''Problem not well formed'')
    )"

  lemma verify_plan_correct:
    "verify_plan problem πs = Inr () 
     ast_problem.well_formed problem  ast_problem.valid_plan problem πs"
  proof -
    {
      assume "ast_problem.well_formed problem"
      then interpret wf_ast_problem by unfold_locales
          
      from check_plan'_correct check_plan_correct 
      have "check_plan' problem πs = valid_plan πs" by simp
    } 
    then show ?thesis  
      unfolding verify_plan_def
      by auto  
  qed

  definition nat_opt_of_integer :: "integer  nat option" where
       "nat_opt_of_integer i = (if (i  0) then Some (nat_of_integer i) else None)"

  (*Export functions, which includes constructors*)
  export_code verify_plan nat_of_integer integer_of_nat nat_opt_of_integer Inl Inr String.explode String.implode
    in SML
    module_name SASP_Checker_Exported

end