Session AI_Planning_Languages_Semantics

Theory Error_Monad_Add

theory Error_Monad_Add
imports
  "Certification_Monads.Check_Monad"
  "Show.Show_Instances"
begin
  (* TODO: Move *)  
  abbreviation "assert_opt Φ  if Φ then Some () else None"  

  definition "lift_opt m e  case m of Some x  Error_Monad.return x | None  Error_Monad.error e"
    
  lemma lift_opt_simps[simp]: 
    "lift_opt None e = error e"
    "lift_opt (Some v) e = return v"
    by (auto simp: lift_opt_def)
  
  (* TODO: Move *)  
  lemma reflcl_image_iff[simp]: "R=``S = SR``S" by blast 
    
  named_theorems return_iff
      
  lemma bind_return_iff[return_iff]: "Error_Monad.bind m f = Inr y  (x. m = Inr x  f x = Inr y)"
    by auto
    
  lemma lift_opt_return_iff[return_iff]: "lift_opt m e = Inr x  m=Some x"
    unfolding lift_opt_def by (auto split: option.split)
      
  lemma check_return_iff[return_iff]: "check Φ e = Inr uu  Φ"    
    by (auto simp: check_def)
  
  
  lemma check_simps[simp]:  
    "check True e = succeed"
    "check False e = error e"
    by (auto simp: check_def)
        
  lemma Let_return_iff[return_iff]: "(let x=v in f x) = Inr w  f v = Inr w" by simp

  
  abbreviation ERR :: "shows  (unit  shows)" where "ERR s  λ_. s"
  abbreviation ERRS :: "String.literal  (unit  shows)" where "ERRS s  ERR (shows s)"
  
  
  lemma error_monad_bind_split: "P (bind m f)  (v. m = Inl v  P (Inl v))  (v. m = Inr v  P (f v))"
    by (cases m) auto
  
  lemma error_monad_bind_split_asm: "P (bind m f)  ¬ (x. m = Inl x  ¬ P (Inl x)  (x. m = Inr x  ¬ P (f x)))"
    by (cases m) auto
  
  lemmas error_monad_bind_splits =error_monad_bind_split error_monad_bind_split_asm
  
  
end

Theory Option_Monad_Add

theory Option_Monad_Add
imports "HOL-Library.Monad_Syntax"
begin
  definition "oassert Φ  if Φ then Some () else None"

  fun omap :: "('a'b)  'a list  'b list" where
    "omap f [] = Some []" 
  | "omap f (x#xs) = do { y  f x; ys  omap f xs; Some (y#ys) }"  
    
  lemma omap_cong[fundef_cong]:
    assumes "x. xset l'  f x = f' x"
    assumes "l=l'"
    shows "omap f l = omap f' l'"
    unfolding assms(2) using assms(1) by (induction l') (auto)

  lemma assert_eq_iff[simp]: 
    "oassert Φ = None  ¬Φ"  
    "oassert Φ = Some u  Φ"  
    unfolding oassert_def by auto

  lemma omap_length[simp]: "omap f l = Some l'  length l' = length l" 
    apply (induction l arbitrary: l') 
    apply (auto split: Option.bind_splits)
    done 

  lemma omap_append[simp]: "omap f (xs@ys) = do {xs  omap f xs; ys  omap f ys; Some (xs@ys)}"
    by (induction xs) (auto)
    
        
  lemma omap_alt: "omap f l = Some l'  (l' = map (the o f) l  (xset l. f x  None))"  
    apply (induction l arbitrary: l')
    apply (auto split: Option.bind_splits)
    done
    
  lemma omap_alt_None: "omap f l = None  (xset l. f x = None)"
    apply (induction l)
    apply (auto split: Option.bind_splits)
    done
    
  lemma omap_nth: "omap f l = Some l'; i<length l  f (l!i) = Some (l'!i)"
    apply (induction l arbitrary: l' i)
    apply (auto split: Option.bind_splits simp: nth_Cons split: nat.splits)
    done

  lemma omap_eq_Nil_conv[simp]: "omap f xs = Some []  xs=[]"
    apply (cases xs) 
    apply (auto split: Option.bind_splits)
    done

  lemma omap_eq_Cons_conv[simp]: "omap f xs = Some (y#ys')  (x xs'. xs=x#xs'  f x = Some y  omap f xs' = Some ys')"  
    apply (cases xs) 
    apply (auto split: Option.bind_splits)
    done
        
  lemma omap_eq_append_conv[simp]: "omap f xs = Some (ys1@ys2)  (xs1 xs2. xs=xs1@xs2  omap f xs1 = Some ys1  omap f xs2 = Some ys2)"
    apply (induction ys1 arbitrary: xs)
    apply (auto 0 3 split: Option.bind_splits)
    apply (metis append_Cons)
    done
  
  lemma omap_list_all2_conv: "omap f xs = Some ys  (list_all2 (λx y. f x = Some y)) xs ys"  
    apply (induction xs arbitrary: ys)
    apply (auto split: Option.bind_splits simp: )
    apply (simp add: list_all2_Cons1)
    apply (simp add: list_all2_Cons1)
    apply (simp add: list_all2_Cons1)
    apply clarsimp
    by (metis option.inject)
    
    
    
    
  fun omap_option where
    "omap_option f None = Some None"    
  | "omap_option f (Some x) = do { x  f x; Some (Some x) }"
  
  lemma omap_option_conv:
    "omap_option f xx = None  (x. xx=Some x  f x = None)" 
    "omap_option f xx = (Some (Some x'))  (x. xx=Some x  f x = Some x')"
    "omap_option f xx = (Some None)  xx=None"
    by (cases xx;auto split: Option.bind_splits)+
  
  lemma omap_option_eq: "omap_option f x = (case x of None  Some None | Some x  do { x  f x; Some (Some x) })"  
    by (auto split: option.split)
      
  fun omap_prod where
    "omap_prod f1 f2 (a,b) = do { af1 a; bf2 b; Some (a,b) }"
    
      
  (* Extend map function for datatype to option monad.
    TODO: Show reasonable lemmas, like parametricity, etc. 
    Hopefully only depending on BNF-property of datatype
   *)
  definition "omap_dt setf mapf f obj  do {
    oassert (xsetf obj. f x  None);
    Some (mapf (the o f) obj)
  }"
    
    
    
end

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

Theory 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, hide_lams) 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
    file "code/SASP_Checker_Exported.sml"

end

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  (xset 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  (xset 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  aM. 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. ab}"

  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))  ab)
    )"
    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 "(Gclose_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  φ; GM. 𝒜  G  𝒜  φ"
  apply(induction φ rule: is_STRIPS_fmla.induct)
  by (auto simp: valuation_def)

lemma aux2: "wm_basic M; is_STRIPS_fmla φ; 𝒜. (GM. 𝒜  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  φ; GM. 𝒜  G  𝒜  φ"
    using assms apply(induction φ rule: is_STRIPS_fmla.induct)
    by (auto simp: valuation_def)
  have aux2: "𝒜. (GM. 𝒜  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 M0…MN 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 φ = (aatoms φ. 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) 
          (aeset a. wf_fmla_atom ae)
         (deset 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)  (Tset 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))
     (pset (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))
     (aset (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 = (fM. 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))
       (aset 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, hide_lams)
      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›

Theory PDDL_STRIPS_Checker

section ‹Executable PDDL Checker›
theory PDDL_STRIPS_Checker
imports
  PDDL_STRIPS_Semantics

  Error_Monad_Add
  "HOL.String"

  (*"HOL-Library.Code_Char"     TODO: This might lead to performance loss! CHECK! *)
  "HOL-Library.Code_Target_Nat"

  "HOL-Library.While_Combinator"

  "Containers.Containers"
begin

subsection ‹Generic DFS Reachability Checker›
text ‹Used for subtype checks›

definition "E_of_succ succ  { (u,v). vset (succ u) }"
lemma succ_as_E: "set (succ x) = E_of_succ succ `` {x}"
  unfolding E_of_succ_def by auto

context
  fixes succ :: "'a  'a list"
begin

  private abbreviation (input) "E  E_of_succ succ"


definition "dfs_reachable D w 
  let (V,w,brk) = while (λ(V,w,brk). ¬brk  w[]) (λ(V,w,_).
    case w of v#w 
    if D v then (V,v#w,True)
    else if vV then (V,w,False)
    else
      let V = insert v V in
      let w = succ v @ w in
      (V,w,False)
    ) ({},w,False)
  in brk"


context
  fixes w0 :: "'a list"
  assumes finite_dfs_reachable[simp, intro!]: "finite (E* `` set w0)"
begin

  private abbreviation (input) "W0  set w0"

definition "dfs_reachable_invar D V W brk 
    W0  W  V
   W  V  E* `` W0
   E``V  W  V
   Collect D  V = {}
   (brk  Collect D  E* `` W0  {})"

lemma card_decreases: "
   finite V; y  V; dfs_reachable_invar D V (Set.insert y W) brk 
    card (E* `` W0 - Set.insert y V) < card (E* `` W0 - V)"
  apply (rule psubset_card_mono)
  apply (auto simp: dfs_reachable_invar_def)
  done

lemma all_neq_Cons_is_Nil[simp]: (* Odd term remaining in goal … *)
  "(y ys. x2  y # ys)  x2 = []" by (cases x2) auto

lemma dfs_reachable_correct: "dfs_reachable D w0  Collect D  E* `` set w0  {}"
  unfolding dfs_reachable_def
  apply (rule while_rule[where
    P="λ(V,w,brk). dfs_reachable_invar D V (set w) brk  finite V"
    and r="measure (λV. card (E* `` (set w0) - V)) <*lex*> measure length <*lex*> measure (λTrue0 | False1)"
    ])
  subgoal by (auto simp: dfs_reachable_invar_def)
  subgoal
    apply (auto simp: neq_Nil_conv succ_as_E[of succ] split: if_splits)
    by (auto simp: dfs_reachable_invar_def Image_iff intro: rtrancl.rtrancl_into_rtrancl)
  subgoal by (fastforce simp: dfs_reachable_invar_def dest: Image_closed_trancl)
  subgoal by blast
  subgoal by (auto simp: neq_Nil_conv card_decreases)
  done

end

definition "tab_succ l  Mapping.lookup_default [] (fold (λ(u,v). Mapping.map_default u [] (Cons v)) l Mapping.empty)"


lemma Some_eq_map_option [iff]: "(Some y = map_option f xo) = (z. xo = Some z  f z = y)"
  by (auto simp add: map_option_case split: option.split)


lemma tab_succ_correct: "E_of_succ (tab_succ l) = set l"
proof -
  have "set (Mapping.lookup_default [] (fold (λ(u,v). Mapping.map_default u [] (Cons v)) l m) u) = set l `` {u}  set (Mapping.lookup_default [] m u)"
    for m u
    apply (induction l arbitrary: m)
    by (auto
      simp: Mapping.lookup_default_def Mapping.map_default_def Mapping.default_def
      simp: lookup_map_entry' lookup_update' keys_is_none_rep Option.is_none_def
      split: if_splits
    )
  from this[where m=Mapping.empty] show ?thesis
    by (auto simp: E_of_succ_def tab_succ_def lookup_default_empty)
qed

end

lemma finite_imp_finite_dfs_reachable:
  "finite E; finite S  finite (E*``S)"
  apply (rule finite_subset[where B="S  (Relation.Domain E  Relation.Range E)"])
  apply (auto simp: intro: finite_Domain finite_Range elim: rtranclE)
  done

lemma dfs_reachable_tab_succ_correct: "dfs_reachable (tab_succ l) D vs0  Collect D  (set l)*``set vs0  {}"
  apply (subst dfs_reachable_correct)
  by (simp_all add: tab_succ_correct finite_imp_finite_dfs_reachable)



subsection ‹Implementation Refinements›

subsubsection ‹Of-Type›

definition "of_type_impl G oT T  (ptset (primitives oT). dfs_reachable G ((=) pt) (primitives T))"


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

lemma ty_term'_correct_aux: "ty_term' varT objT t = ty_term varT (Mapping.lookup objT) t"
  by (cases t) auto

lemma ty_term'_correct[simp]: "ty_term' varT objT = ty_term varT (Mapping.lookup objT)"
  using ty_term'_correct_aux by auto

context ast_domain begin

  definition "of_type1 pt T  pt  subtype_rel* `` set (primitives T)"

  lemma of_type_refine1: "of_type oT T  (ptset (primitives oT). of_type1 pt T)"
    unfolding of_type_def of_type1_def by auto

  definition "STG  (tab_succ (map subtype_edge (types D)))"

  lemma subtype_rel_impl: "subtype_rel = E_of_succ (tab_succ (map subtype_edge (types D)))"
    by (simp add: tab_succ_correct subtype_rel_def)

  lemma of_type1_impl: "of_type1 pt T  dfs_reachable (tab_succ (map subtype_edge (types D))) ((=)pt) (primitives T)"
    by (simp add: subtype_rel_impl of_type1_def dfs_reachable_tab_succ_correct tab_succ_correct)

  lemma of_type_impl_correct: "of_type_impl STG oT T  of_type oT T"
    unfolding of_type1_impl STG_def of_type_impl_def of_type_refine1 ..

  definition mp_constT :: "(object, type) mapping" where
    "mp_constT = Mapping.of_alist (consts D)"

  lemma mp_objT_correct[simp]: "Mapping.lookup mp_constT = constT"
    unfolding mp_constT_def constT_def
    by transfer (simp add: Map_To_Mapping.map_apply_def)






  text ‹Lifting the subtype-graph through wf-checker›
  context
    fixes ty_ent :: "'ent  type"  ― ‹Entity's type, None if invalid›
  begin

    definition "is_of_type' stg v T  (
      case ty_ent v of
        Some vT  of_type_impl stg vT T
      | None  False)"

    lemma is_of_type'_correct: "is_of_type' STG v T = is_of_type ty_ent v T"
      unfolding is_of_type'_def is_of_type_def of_type_impl_correct ..

    fun wf_pred_atom' where "wf_pred_atom' stg (p,vs)  (case sig p of
          None  False
        | Some Ts  list_all2 (is_of_type' stg) vs Ts)"

    lemma wf_pred_atom'_correct: "wf_pred_atom' STG pvs = wf_pred_atom ty_ent pvs"
      by (cases pvs) (auto simp: is_of_type'_correct[abs_def] split:option.split)

    fun wf_atom' :: "_  'ent atom  bool" where
      "wf_atom' stg (atom.predAtm p vs)  wf_pred_atom' stg (p,vs)"
    | "wf_atom' stg (atom.Eq a b) = (ty_ent a  None  ty_ent b  None)"

    lemma wf_atom'_correct: "wf_atom' STG a = wf_atom ty_ent a"
      by (cases a) (auto simp: wf_pred_atom'_correct is_of_type'_correct[abs_def] split: option.splits)

    fun wf_fmla' :: "_  ('ent atom) formula  bool" where
      "wf_fmla' stg (Atom a)  wf_atom' stg a"
    | "wf_fmla' stg   True"
    | "wf_fmla' stg (φ1  φ2)  (wf_fmla' stg φ1  wf_fmla' stg φ2)"
    | "wf_fmla' stg (φ1  φ2)  (wf_fmla' stg φ1  wf_fmla' stg φ2)"
    | "wf_fmla' stg (φ1  φ2)  (wf_fmla' stg φ1  wf_fmla' stg φ2)"
    | "wf_fmla' stg (¬φ)  wf_fmla' stg φ"

    lemma wf_fmla'_correct: "wf_fmla' STG φ  wf_fmla ty_ent φ"
      by (induction φ rule: wf_fmla.induct) (auto simp: wf_atom'_correct)

    fun wf_fmla_atom1' where
      "wf_fmla_atom1' stg (Atom (predAtm p vs))  wf_pred_atom' stg (p,vs)"
    | "wf_fmla_atom1' stg _  False"

    lemma wf_fmla_atom1'_correct: "wf_fmla_atom1' STG φ = wf_fmla_atom ty_ent φ"
      by (cases φ rule: wf_fmla_atom.cases) (auto
        simp: wf_atom'_correct is_of_type'_correct[abs_def] split: option.splits)

    fun wf_effect' where
      "wf_effect' stg (Effect a d) 
          (aeset a. wf_fmla_atom1' stg ae)
         (deset d.  wf_fmla_atom1' stg de)"

    lemma wf_effect'_correct: "wf_effect' STG e = wf_effect ty_ent e"
      by (cases e) (auto simp: wf_fmla_atom1'_correct)

  end ― ‹Context fixing ty_ent›

  fun wf_action_schema' :: "_  _  ast_action_schema  bool" where
    "wf_action_schema' stg conT (Action_Schema n params pre eff)  (
      let
        tyv = ty_term' (map_of params) conT
      in
        distinct (map fst params)
       wf_fmla' tyv stg pre
       wf_effect' tyv stg eff)"

  lemma wf_action_schema'_correct: "wf_action_schema' STG mp_constT s = wf_action_schema s"
    by (cases s) (auto simp: wf_fmla'_correct wf_effect'_correct)

  definition wf_domain' :: "_  _  bool" where
    "wf_domain' stg conT 
      wf_types
     distinct (map (predicate_decl.pred) (predicates D))
     (pset (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))
     (aset (actions D). wf_action_schema' stg conT a)
    "

  lemma wf_domain'_correct: "wf_domain' STG mp_constT = wf_domain"
    unfolding wf_domain_def wf_domain'_def
    by (auto simp: wf_action_schema'_correct)


end ― ‹Context of ast_domain›

subsubsection ‹Application of Effects›

context ast_domain begin
  text ‹We implement the application of an effect by explicit iteration over
    the additions and deletions›
  fun apply_effect_exec
    :: "object ast_effect  world_model  world_model"
  where
    "apply_effect_exec (Effect a d) s
      = fold (λadd s. Set.insert add s) a
          (fold (λdel s. Set.remove del s) d s)"

  lemma apply_effect_exec_refine[simp]:
    "apply_effect_exec (Effect (a) (d)) s
    = apply_effect (Effect (a) (d)) s"
  proof(induction a arbitrary: s)
    case Nil
    then show ?case
    proof(induction d arbitrary: s)
      case Nil
      then show ?case by auto
    next
      case (Cons a d)
      then show ?case
        by (auto simp add: image_def)
    qed
  next
    case (Cons a a)
    then show ?case
    proof(induction d arbitrary: s)
      case Nil
      then show ?case by (auto; metis Set.insert_def sup_assoc insert_iff)
    next
      case (Cons a d)
      then show ?case
        by (auto simp: Un_commute minus_set_fold union_set_fold)
    qed
  qed

  lemmas apply_effect_eq_impl_eq
    = apply_effect_exec_refine[symmetric, unfolded apply_effect_exec.simps]

end ― ‹Context of ast_domain›

subsubsection ‹Well-Formedness›

context ast_problem begin

  text ‹ We start by defining a mapping from objects to types. The container
    framework will generate efficient, red-black tree based code for that
    later. ›

  type_synonym objT = "(object, type) mapping"

  definition mp_objT :: "(object, type) mapping" where
    "mp_objT = Mapping.of_alist (consts D @ objects P)"

  lemma mp_objT_correct[simp]: "Mapping.lookup mp_objT = objT"
    unfolding mp_objT_def objT_alt
    by transfer (simp add: Map_To_Mapping.map_apply_def)

  text ‹We refine the typecheck to use the mapping›

  definition "is_obj_of_type_impl stg mp n T = (
    case Mapping.lookup mp n of None  False | Some oT  of_type_impl stg oT T
  )"

  lemma is_obj_of_type_impl_correct[simp]:
    "is_obj_of_type_impl STG mp_objT = is_obj_of_type"
    apply (intro ext)
    apply (auto simp: is_obj_of_type_impl_def is_obj_of_type_def of_type_impl_correct split: option.split)
    done

  text ‹We refine the well-formedness checks to use the mapping›

  definition wf_fact' :: "objT  _  fact  bool"
    where
    "wf_fact' ot stg  wf_pred_atom' (Mapping.lookup ot) stg"

  lemma wf_fact'_correct[simp]: "wf_fact' mp_objT STG = wf_fact"
    by (auto simp: wf_fact'_def wf_fact_def wf_pred_atom'_correct[abs_def])


  definition "wf_fmla_atom2' mp stg f
    = (case f of formula.Atom (predAtm p vs)  (wf_fact' mp stg (p,vs)) | _  False)"

  lemma wf_fmla_atom2'_correct[simp]:
    "wf_fmla_atom2' mp_objT STG φ = wf_fmla_atom objT φ"
    apply (cases φ rule: wf_fmla_atom.cases)
    by (auto simp: wf_fmla_atom2'_def wf_fact_def split: option.splits)

  definition "wf_problem' stg conT mp 
      wf_domain' stg conT
     distinct (map fst (objects P) @ map fst (consts D))
     ((n,T)set (objects P). wf_type T)
     distinct (init P)
     (fset (init P). wf_fmla_atom2' mp stg f)
     wf_fmla' (Mapping.lookup mp) stg (goal P)"

  lemma wf_problem'_correct:
    "wf_problem' STG mp_constT mp_objT = wf_problem"
    unfolding wf_problem_def wf_problem'_def wf_world_model_def
    by (auto simp: wf_domain'_correct wf_fmla'_correct)


  text ‹Instantiating actions will yield well-founded effects.
    Corollary of @{thm wf_instantiate_action_schema}.›
  lemma wf_effect_inst_weak:
    fixes a args
    defines "ai  instantiate_action_schema a args"
    assumes A: "action_params_match a args"
      "wf_action_schema a"
    shows "wf_effect_inst (effect ai)"
    using wf_instantiate_action_schema[OF A] unfolding ai_def[symmetric]
    by (cases ai) (auto simp: wf_effect_inst_alt)


end ― ‹Context of ast_problem›


context wf_ast_domain begin
  text ‹Resolving an action yields a well-founded action schema.›
  (* TODO: This must be implicitly proved when showing that plan execution
    preserves wf. Try to remove this redundancy!*)
  lemma resolve_action_wf:
    assumes "resolve_action_schema n = Some a"
    shows "wf_action_schema a"
  proof -
    from wf_domain have
      X1: "distinct (map ast_action_schema.name (actions D))"
      and X2: "aset (actions D). wf_action_schema a"
      unfolding wf_domain_def by auto

    show ?thesis
      using assms unfolding resolve_action_schema_def
      by (auto simp add: index_by_eq_Some_eq[OF X1] X2)
  qed

end ― ‹Context of ast_domain›


subsubsection ‹Execution of Plan Actions›

text ‹We will perform two refinement steps, to summarize redundant operations›

text ‹We first lift action schema lookup into the error monad. ›
context ast_domain begin
  definition "resolve_action_schemaE n 
    lift_opt
      (resolve_action_schema n)
      (ERR (shows ''No such action schema '' o shows n))"
end ― ‹Context of ast_domain›

end ― ‹Theory›

Theory Lifschitz_Consistency

section ‹Soundness theorem for the STRIPS semantics›
text ‹We prove the soundness theorem according to ~\cite{lifschitz1987semantics}.›

theory Lifschitz_Consistency
imports PDDL_STRIPS_Semantics
begin


text ‹States are modeled as valuations of our underlying predicate logic.›
type_synonym state = "(predicate×object list) valuation"

context ast_domain begin
  text ‹An action is a partial function from states to states. ›
  type_synonym action = "state  state"

  text ‹The Isabelle/HOL formula @{prop f s = Some s'} means
    that f› is applicable in state s›, and the result is s'›. ›

  text ‹Definition B (i)--(iv) in Lifschitz's paper~\cite{lifschitz1987semantics}›

  fun is_NegPredAtom where
    "is_NegPredAtom (Not x) = is_predAtom x" | "is_NegPredAtom _ = False"

  definition "close_eq s = (λpredAtm p xs  s (p,xs) | Eq a b  a=b)"

  lemma close_eq_predAtm[simp]: "close_eq s (predAtm p xs)  s (p,xs)"
    by (auto simp: close_eq_def)                    

  lemma close_eq_Eq[simp]: "close_eq s (Eq a b)  a=b"
    by (auto simp: close_eq_def)


  abbreviation entail_eq :: "state  object atom formula  bool" (infix "=" 55)
    where "entail_eq s f  close_eq s  f"


  fun sound_opr :: "ground_action  action  bool" where
    "sound_opr (Ground_Action pre (Effect add del)) f 
      (s. s = pre 
        (s'. f s = Some s'  (atm. is_predAtom atm  atm  set del  s = atm  s' = atm)
                (atm. is_predAtom atm  atm  set add  s = Not atm  s' = Not atm)
               (fmla. fmla  set add  s' = fmla)
               (fmla. fmla  set del  fmla  set add  s' = (Not fmla))
              ))
         (fmlaset add. is_predAtom fmla)"

  lemma sound_opr_alt:
    "sound_opr opr f =
      ((s. s = (precondition opr) 
          (s'. f s = (Some s')
                 (atm. is_predAtom atm  atm  set(dels (effect opr))  s = atm  s' = atm)
                 (atm. is_predAtom atm  atm  set (adds (effect opr))  s = Not atm  s' = Not atm)
                 (atm. atm  set(adds (effect opr))  s' = atm)
                 (fmla. fmla  set (dels (effect opr))  fmla  set(adds (effect opr))  s' = (Not fmla))
                 (a b. s = Atom (Eq a b)  s' = Atom (Eq a b))
                 (a b. s = Not (Atom (Eq a b))  s' = Not (Atom (Eq a b)))
                ))
         (fmlaset(adds (effect opr)). is_predAtom fmla))"
    by (cases "(opr,f)" rule: sound_opr.cases) auto

  text ‹Definition B (v)--(vii) in  Lifschitz's paper~\cite{lifschitz1987semantics}›
definition sound_system
    :: "ground_action set
       world_model
       state
       (ground_action  action)
       bool"
    where
    "sound_system Σ M0 s0 f 
      ((fmlaclose_world M0. s0  = fmla)
       wm_basic M0
       (αΣ. sound_opr α (f α)))"

  text ‹Composing two actions›
  definition compose_action :: "action  action  action" where
    "compose_action f1 f2 x = (case f2 x of Some y  f1 y | None  None)"

  text ‹Composing a list of actions›
  definition compose_actions :: "action list  action" where
    "compose_actions fs  fold compose_action fs Some"

  text ‹Composing a list of actions satisfies some natural lemmas: ›
  lemma compose_actions_Nil[simp]:
    "compose_actions [] = Some" unfolding compose_actions_def by auto

  lemma compose_actions_Cons[simp]:
    "f s = Some s'  compose_actions (f#fs) s = compose_actions fs s'"
  proof -
    interpret monoid_add compose_action Some
      apply unfold_locales
      unfolding compose_action_def
      by (auto split: option.split)
    assume "f s = Some s'"
    then show ?thesis
      unfolding compose_actions_def
      by (simp add: compose_action_def fold_plus_sum_list_rev)
  qed

  text ‹Soundness Theorem in Lifschitz's paper~\cite{lifschitz1987semantics}.›
theorem STRIPS_sema_sound:
  assumes "sound_system Σ M0 s0 f"
    ― ‹For a sound system Σ›
  assumes "set αs  Σ"
    ― ‹And a plan αs›
  assumes "ground_action_path M0 αs M'"
    ― ‹Which is accepted by the system, yielding result M'›
          (called R(αs)› in Lifschitz's paper~\cite{lifschitz1987semantics}.)›
  obtains s'
    ― ‹We have that f(αs)› is applicable
          in initial state, yielding state s'› (called fαs(s0)› in Lifschitz's paper~\cite{lifschitz1987semantics}.)›
  where "compose_actions (map f αs) s0 = Some s'"
    ― ‹The result world model M'› is satisfied in state s'›
    and "fmlaclose_world M'. s' = fmla"
proof -
  have "(valuation M'  fmla)" if "wm_basic M'" "fmlaM'" for fmla
    using that apply (induction fmla)
    by (auto simp: valuation_def wm_basic_def split: atom.split)
  have "s'. compose_actions (map f αs) s0 = Some s'  (fmlaclose_world M'. s' = fmla)"
    using assms
  proof(induction αs arbitrary: s0 M0 )
    case Nil
    then show ?case by (auto simp add: close_world_def compose_action_def sound_system_def)
  next
    case ass: (Cons α αs)
    then obtain pre add del where a: "α = Ground_Action pre (Effect add del)"
      using ground_action.exhaust ast_effect.exhaust by metis
    let ?M1 = "execute_ground_action α M0"
    have "close_world M0  precondition α"
      using ass(4)
      by auto
    moreover have s0_ent_cwM0: "fmla(close_world M0). close_eq s0  fmla"
      using ass(2)
      unfolding sound_system_def
      by auto
    ultimately have s0_ent_alpha_precond: "close_eq s0  precondition α"
      unfolding entailment_def
      by auto
    then obtain s1 where s1: "(f α) s0 = Some s1"
      "(atm. is_predAtom atm  atm  set(dels (effect α))
                                             close_eq s0  atm
                                             close_eq s1  atm)"
      "(fmla. fmla  set(adds (effect α))
                                             close_eq s1  fmla)"
      "(atm. is_predAtom atm  atm  set (adds (effect α))  close_eq s0  Not atm  close_eq s1  Not atm)"
      "(fmla. fmla  set (dels (effect α))  fmla  set(adds (effect α))  close_eq s1  (Not fmla))"
      "(a b. close_eq s0  Atom (Eq a b)  close_eq s1  Atom (Eq a b))"
      "(a b. close_eq s0  Not (Atom (Eq a b))  close_eq s1  Not (Atom (Eq a b)))"
      using ass(2-4)
      unfolding sound_system_def sound_opr_alt by force
    have "close_eq s1  fmla" if "fmlaclose_world ?M1" for fmla
      using ass(2)
      using that s1 s0_ent_cwM0
      unfolding sound_system_def execute_ground_action_def wm_basic_def
      apply (auto simp: in_close_world_conv)
      subgoal
        by (metis (no_types, lifting) DiffE UnE a apply_effect.simps ground_action.sel(2) ast_effect.sel(1) ast_effect.sel(2) close_world_extensive subsetCE)
      subgoal
        by (metis Diff_iff Un_iff a ground_action.sel(2) ast_domain.apply_effect.simps ast_domain.close_eq_predAtm ast_effect.sel(1) ast_effect.sel(2) formula_semantics.simps(1) formula_semantics.simps(3) in_close_world_conv is_predAtom.simps(1))
      done
    moreover have "(atm. fmla  formula.Atom atm)  s  fmla" if "fmla?M1" for fmla s
    proof-
      have alpha: "(s.fmlaset(adds (effect α)). ¬ is_predAtom fmla  s  fmla)"
        using ass(2,3)
        unfolding sound_system_def ast_domain.sound_opr_alt
        by auto
      then show ?thesis
        using that
        unfolding a execute_ground_action_def
        using ass.prems(1)[unfolded sound_system_def]
        by(cases fmla; fastforce simp: wm_basic_def)

    qed
    moreover have "(oprΣ. sound_opr opr (f opr))"
      using ass(2) unfolding sound_system_def
      by (auto simp add:)
    moreover have "wm_basic ?M1"
      using ass(2,3)
      unfolding sound_system_def execute_ground_action_def
      thm sound_opr.cases
      apply (cases "(α,f α)" rule: sound_opr.cases)
      apply (auto simp: wm_basic_def)
      done
    ultimately have "sound_system Σ ?M1 s1 f"
      unfolding sound_system_def
      by (auto simp: wm_basic_def)
    from ass.IH[OF this] ass.prems obtain s' where
      "compose_actions (map f αs) s1 = Some s'  (aclose_world M'. s' = a)"
      by auto
    thus ?case by (auto simp: s1(1))
  qed
  with that show ?thesis by blast
qed

  text ‹More compact notation of the soundness theorem.›
  theorem STRIPS_sema_sound_compact_version:
    "sound_system Σ M0 s0 f  set αs  Σ
     ground_action_path M0 αs M'
     s'. compose_actions (map f αs) s0 = Some s'
           (fmlaclose_world M'. s' = fmla)"
    using STRIPS_sema_sound by metis

end ― ‹Context of ast_domain›

subsection ‹Soundness Theorem for PDDL›

context wf_ast_problem begin

  text ‹Mapping world models to states›
  definition state_to_wm :: "state  world_model"
    where "state_to_wm s = ({formula.Atom (predAtm p xs) | p xs. s (p,xs)})"
  definition wm_to_state :: "world_model  state"
    where "wm_to_state M = (λ(p,xs). (formula.Atom (predAtm p xs))  M)"


  lemma wm_to_state_eq[simp]: "wm_to_state M (p, as)  Atom (predAtm p as)  M"
    by (auto simp: wm_to_state_def)




  lemma wm_to_state_inv[simp]: "wm_to_state (state_to_wm s) = s"
    by (auto simp: wm_to_state_def
      state_to_wm_def image_def)

  text ‹Mapping AST action instances to actions›
  definition "pddl_opr_to_act g_opr s = (
    let M = state_to_wm s in
    if (wm_to_state (close_world M)) = (precondition g_opr) then
      Some (wm_to_state (apply_effect (effect g_opr) M))
    else
      None)"

definition "close_eq_M M = (M  {Atom (predAtm p xs) | p xs. True })  {Atom (Eq a a) | a. True}  {¬(Atom (Eq a b)) | a b. ab}"

  lemma atom_in_wm_eq:
    "s = (formula.Atom atm)
       ((formula.Atom atm)  close_eq_M (state_to_wm s))"
    by (auto simp: wm_to_state_def
      state_to_wm_def image_def close_eq_M_def close_eq_def split: atom.splits)

lemma atom_in_wm_2_eq:
    "close_eq (wm_to_state M)  (formula.Atom atm)
       ((formula.Atom atm)  close_eq_M M)"
    by (auto simp: wm_to_state_def
      state_to_wm_def image_def close_eq_def close_eq_M_def split:atom.splits)

  lemma not_dels_preserved:
    assumes "f  (set d)" " f  M"
    shows "f  apply_effect (Effect a d) M"
    using assms
    by auto

  lemma adds_satisfied:
    assumes "f  (set a)"
    shows "f  apply_effect (Effect a d) M"
    using assms
    by auto

  lemma dels_unsatisfied:
    assumes "f  (set d)" "f  set a"
    shows "f  apply_effect (Effect a d) M"
    using assms
    by auto

  lemma dels_unsatisfied_2:
    assumes "f  set (dels eff)" "f  set (adds eff)"
    shows "f  apply_effect eff M"
    using assms
    by (cases eff; auto)

  lemma wf_fmla_atm_is_atom: "wf_fmla_atom objT f  is_predAtom f"
    by (cases f rule: wf_fmla_atom.cases) auto

  lemma wf_act_adds_are_atoms:
    assumes "wf_effect_inst effs" "ae  set (adds effs)"
    shows "is_predAtom ae"
    using assms
    by (cases effs) (auto simp: wf_fmla_atom_alt)

  lemma wf_act_adds_dels_atoms:
    assumes "wf_effect_inst effs" "ae  set (dels effs)"
    shows "is_predAtom ae"
    using assms
    by (cases effs) (auto simp: wf_fmla_atom_alt)

  lemma to_state_close_from_state_eq[simp]: "wm_to_state (close_world (state_to_wm s)) = s"
    by (auto simp: wm_to_state_def close_world_def
      state_to_wm_def image_def)



lemma wf_eff_pddl_ground_act_is_sound_opr:
  assumes "wf_effect_inst (effect g_opr)"
  shows "sound_opr g_opr ((pddl_opr_to_act g_opr))"
  unfolding sound_opr_alt
  apply(cases g_opr; safe)
  subgoal for pre eff s
    apply (rule exI[where x="wm_to_state(apply_effect eff (state_to_wm s))"])
    apply (auto simp: pddl_opr_to_act_def Let_def split:if_splits)
    subgoal for atm
      by (cases eff; cases atm; auto simp: close_eq_def wm_to_state_def state_to_wm_def split: atom.splits)
    subgoal for atm
      by (cases eff; cases atm; auto simp: close_eq_def wm_to_state_def state_to_wm_def split: atom.splits)
    subgoal for atm
      using assms
      by (cases eff; cases atm; force simp: close_eq_def wm_to_state_def state_to_wm_def split: atom.splits)
    subgoal for fmla
      using assms
      by (cases eff; cases fmla rule: wf_fmla_atom.cases; force simp: close_eq_def wm_to_state_def state_to_wm_def split: atom.splits)
    done
  subgoal for pre eff fmla
    using assms
    by (cases eff; cases fmla rule: wf_fmla_atom.cases; force)
  done



  lemma wf_eff_impt_wf_eff_inst: "wf_effect objT eff  wf_effect_inst eff"
    by (cases eff; auto simp add: wf_fmla_atom_alt)

  lemma wf_pddl_ground_act_is_sound_opr:
    assumes "wf_ground_action g_opr"
    shows "sound_opr g_opr (pddl_opr_to_act g_opr)"
    using wf_eff_impt_wf_eff_inst wf_eff_pddl_ground_act_is_sound_opr assms
    by (cases g_opr; auto)

  lemma wf_action_schema_sound_inst:
    assumes "action_params_match act args" "wf_action_schema act"
    shows "sound_opr
      (instantiate_action_schema act args)
      ((pddl_opr_to_act (instantiate_action_schema act args)))"
    using
      wf_pddl_ground_act_is_sound_opr[
        OF wf_instantiate_action_schema[OF assms]]
      by blast

  lemma wf_plan_act_is_sound:
    assumes "wf_plan_action (PAction n args)"
    shows "sound_opr
      (instantiate_action_schema (the (resolve_action_schema n)) args)
      ((pddl_opr_to_act
        (instantiate_action_schema (the (resolve_action_schema n)) args)))"
    using assms
    using wf_action_schema_sound_inst wf_eff_pddl_ground_act_is_sound_opr
    by (auto split: option.splits)

  lemma wf_plan_act_is_sound':
    assumes "wf_plan_action π"
    shows "sound_opr
      (resolve_instantiate π)
      ((pddl_opr_to_act (resolve_instantiate π)))"
    using assms wf_plan_act_is_sound
    by (cases π; auto )

  lemma wf_world_model_has_atoms: "fM  wf_world_model M  is_predAtom f"
    using wf_fmla_atm_is_atom
    unfolding wf_world_model_def
    by auto

  lemma wm_to_state_works_for_wf_wm_closed:
    "wf_world_model M  fmlaclose_world M  close_eq (wm_to_state M)  fmla"
    apply (cases fmla rule: wf_fmla_atom.cases)
    by (auto simp: wf_world_model_def close_eq_def wm_to_state_def close_world_def)

  lemma wm_to_state_works_for_wf_wm: "wf_world_model M  fmlaM  close_eq (wm_to_state M)  fmla"
    apply (cases fmla rule: wf_fmla_atom.cases)
    by (auto simp: wf_world_model_def close_eq_def wm_to_state_def)



  lemma wm_to_state_works_for_I_closed:
    assumes "x  close_world I"
    shows "close_eq (wm_to_state I)  x"
    apply (rule wm_to_state_works_for_wf_wm_closed)
    using assms wf_I by auto


  lemma wf_wm_imp_basic: "wf_world_model M  wm_basic M"
    by (auto simp: wf_world_model_def wm_basic_def wf_fmla_atm_is_atom)

theorem wf_plan_sound_system:
  assumes "π set πs. wf_plan_action π"
  shows "sound_system
      (set (map resolve_instantiate πs))
      I
      (wm_to_state I)
      ((λα. pddl_opr_to_act α))"
  unfolding sound_system_def
proof(intro conjI ballI)
  show "close_eq(wm_to_state I)  x" if "x  close_world I" for x
    using that[unfolded in_close_world_conv]
      wm_to_state_works_for_I_closed wm_to_state_works_for_wf_wm
    by (auto simp: wf_I)

  show "wm_basic I" using wf_wm_imp_basic[OF wf_I] .

  show "sound_opr α (pddl_opr_to_act α)" if "α  set (map resolve_instantiate πs)" for α
    using that
    using wf_plan_act_is_sound' assms
    by auto
qed

theorem wf_plan_soundness_theorem:
    assumes "plan_action_path I πs M"
    defines "αs  map (pddl_opr_to_act  resolve_instantiate) πs"
    defines "s0  wm_to_state I"
    shows "s'. compose_actions αs s0 = Some s'  (φclose_world M. s' = φ)"
    apply (rule STRIPS_sema_sound)
    apply (rule wf_plan_sound_system)
    using assms
    unfolding plan_action_path_def
    by (auto simp add: image_def)

end ― ‹Context of wf_ast_problem›

end