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 = S∪R``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
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. x∈set 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 ∧ (∀x∈set l. f x ≠ None))"  
    apply (induction l arbitrary: l')
    apply (auto split: Option.bind_splits)
    done
    
  lemma omap_alt_None: "omap f l = None ⟷ (∃x∈set 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 (ys⇩1@ys⇩2) ⟷ (∃xs⇩1 xs⇩2. xs=xs⇩1@xs⇩2 ∧ omap f xs⇩1 = Some ys⇩1 ∧ omap f xs⇩2 = Some ys⇩2)"
    apply (induction ys⇩1 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 f⇩1 f⇩2 (a,b) = do { a←f⇩1 a; b←f⇩2 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 (∀x∈setf obj. f x ≠ None);
    Some (mapf (the o f) obj)
  }"
    
    
    
end

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 ∧ (∀x∈Dom. 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 ≡ { s∈valid_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,_). vpre≠None) 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,_) ⇒ 
              s∈subsuming_states (map_of pres)
            ∧ s∈subsuming_states (map_of (implicit_pres effs))
        | None ⇒ False"
      
    definition eff_enabled :: "state ⇒ ast_effect ⇒ bool" where
      "eff_enabled s ≡ λ(pres,_,_,_). s∈subsuming_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 "s∈valid_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 ‹s∈valid_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 "s∈valid_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
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: "m⊆⇩mm' ⟹ 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 ≡ ∀pre∈set 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(x↦v)) 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 "s∈valid_states"  
      shows "match_pres pres s ⟷ s∈subsuming_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 "s∈valid_states"  
      shows "match_implicit_pres effs s ⟷ s∈subsuming_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: "s∈valid_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: "s∈valid_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: "s∈valid_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: "s∈valid_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: "s∈valid_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 "s∈valid_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 "s∈valid_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

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 ⟷ (x∈set 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 ⟹ (x∈set 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 ≡ ∀a∈M. 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. a≠b}"

  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)) ∧ a≠b)
    )"
    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 "(∀G∈close_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 ⊨ φ; ∀G∈M. 𝒜 ⊨ G⟧ ⟹ 𝒜 ⊨ φ"
  apply(induction φ rule: is_STRIPS_fmla.induct)
  by (auto simp: valuation_def)

lemma aux2: "⟦wm_basic M; is_STRIPS_fmla φ; ∀𝒜. (∀G∈M. 𝒜 ⊨ 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 ⊨ φ; ∀G∈M. 𝒜 ⊨ G⟧ ⟹ 𝒜 ⊨ φ"
    using assms apply(induction φ rule: is_STRIPS_fmla.induct)
    by (auto simp: valuation_def)
  have aux2: "⟦∀𝒜. (∀G∈M. 𝒜 ⊨ 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 ‹M⇩0…M⇩N› 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 φ = (∀a∈atoms φ. 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) ⟷
          (∀ae∈set a. wf_fmla_atom ae)
        ∧ (∀de∈set 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) ⟷ (∀T∈set 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))
    ∧ (∀p∈set (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))
    ∧ (∀a∈set (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 = (∀f∈M. 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))
      ⟷ (∀a∈set 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›