# Session AI_Planning_Languages_Semantics

theory Error_Monad_Add
imports
"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∪RS" 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

end


theory Option_Monad_Add
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 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

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

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)

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
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


# 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 ⟷ (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 ⊫ φ"

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'' (fstset (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 ≡ sndset (types D) ⊆ insert ''object'' (fstset (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)

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)

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 (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

"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). v∈set (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 v∈V 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 w⇩0 :: "'a list"
assumes finite_dfs_reachable[simp, intro!]: "finite (E⇧*  set w⇩0)"
begin

private abbreviation (input) "W⇩0 ≡ set w⇩0"

definition "dfs_reachable_invar D V W brk ⟷
W⇩0 ⊆ W ∪ V
∧ W ∪ V ⊆ E⇧*  W⇩0
∧ EV ⊆ W ∪ V
∧ Collect D ∩ V = {}
∧ (brk ⟶ Collect D ∩ E⇧*  W⇩0 ≠ {})"

lemma card_decreases: "
⟦finite V; y ∉ V; dfs_reachable_invar D V (Set.insert y W) brk ⟧
⟹ card (E⇧*  W⇩0 - Set.insert y V) < card (E⇧*  W⇩0 - 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 w⇩0 ⟷ Collect D ∩ E⇧*  set w⇩0 ≠ {}"
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 w⇩0) - V)) <*lex*> measure length <*lex*> measure (λTrue⇒0 | False⇒1)"
])
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 vs⇩0 ⟷ Collect D ∩ (set l)⇧*set vs⇩0 ≠ {}"
apply (subst dfs_reachable_correct)

subsection ‹Implementation Refinements›

subsubsection ‹Of-Type›

definition "of_type_impl G oT T ≡ (∀pt∈set (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 ⟷ (∀pt∈set (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)))"

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

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) ⟷
(∀ae∈set a. wf_fmla_atom1' stg ae)
∧ (∀de∈set 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))
∧ (∀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' 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
fun apply_effect_exec
:: "object ast_effect ⇒ world_model ⇒ world_model"
where
"apply_effect_exec (Effect a d) s
(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
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

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)
∧ (∀f∈set (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: "∀a∈set (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))
))

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)))
))
∧ (∀fmla∈set(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 Σ M⇩0 s⇩0 f ⟷
((∀fmla∈close_world M⇩0. s⇩0  ⊨⇩= fmla)
∧ wm_basic M⇩0
∧ (∀α∈Σ. 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 -
apply unfold_locales
unfolding compose_action_def
by (auto split: option.split)
assume "f s = Some s'"
then show ?thesis
unfolding compose_actions_def
qed

text ‹Soundness Theorem in Lifschitz's paper~\cite{lifschitz1987semantics}.›
theorem STRIPS_sema_sound:
assumes "sound_system Σ M⇩0 s⇩0 f"
― ‹For a sound system ‹Σ››
assumes "set αs ⊆ Σ"
― ‹And a plan ‹αs››
assumes "ground_action_path M⇩0 α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(s⇩0)› in Lifschitz's paper~\cite{lifschitz1987semantics}.)›
where "compose_actions (map f αs) s⇩0 = Some s'"
― ‹The result world model ‹M'› is satisfied in state ‹s'››
and "∀fmla∈close_world M'. s' ⊨⇩= fmla"
proof -
have "(valuation M' ⊨ fmla)" if "wm_basic M'" "fmla∈M'" 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) s⇩0 = Some s' ∧ (∀fmla∈close_world M'. s' ⊨⇩= fmla)"
using assms
proof(induction αs arbitrary: s⇩0 M⇩0 )
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 ?M⇩1 = "execute_ground_action α M⇩0"
have "close_world M⇩0 ⊫ precondition α"
using ass(4)
by auto
moreover have s0_ent_cwM0: "∀fmla∈(close_world M⇩0). close_eq s⇩0 ⊨ fmla"
using ass(2)
unfolding sound_system_def
by auto
ultimately have s0_ent_alpha_precond: "close_eq s⇩0 ⊨ precondition α"
unfolding entailment_def
by auto
then obtain s⇩1 where s1: "(f α) s⇩0 = Some s⇩1"
"(∀atm. is_predAtom atm ⟶ atm ∉ set(dels (effect α))
⟶ close_eq s⇩0 ⊨ atm
⟶ close_eq s⇩1 ⊨ atm)"
"(∀fmla. fmla ∈ set(adds (effect α))
⟶ close_eq s⇩1 ⊨ fmla)"
"(∀atm. is_predAtom atm ∧ atm ∉ set (adds (effect α)) ∧ close_eq s⇩0 ⊨ Not atm ⟶ close_eq s⇩1 ⊨ Not atm)"
"(∀fmla. fmla ∈ set (dels (effect α)) ∧ fmla ∉ set(adds (effect α)) ⟶ close_eq s⇩1 ⊨ (Not fmla))"
"(∀a b. close_eq s⇩0 ⊨ Atom (Eq a b) ⟶ close_eq s⇩1 ⊨ Atom (Eq a b))"
"(∀a b. close_eq s⇩0 ⊨ Not (Atom (Eq a b)) ⟶ close_eq s⇩1 ⊨ Not (Atom (Eq a b)))"
using ass(2-4)
unfolding sound_system_def sound_opr_alt by force
have "close_eq s⇩1 ⊨ fmla" if "fmla∈close_world ?M⇩1" 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∈?M⇩1" for fmla s
proof-
have alpha: "(∀s.∀fmla∈set(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
moreover have "wm_basic ?M⇩1"
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 Σ ?M⇩1 s⇩1 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) s⇩1 = Some s' ∧ (∀a∈close_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 Σ M⇩0 s⇩0 f ⟹ set αs ⊆ Σ
⟹ ground_action_path M⇩0 αs M'
⟹ ∃s'. compose_actions (map f αs) s⇩0 = Some s'
∧ (∀fmla∈close_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. a≠b}"

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

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

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

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: "f∈M ⟹ 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 ⟹ fmla∈close_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 ⟹ fmla∈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)

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 "s⇩0 ≡ wm_to_state I"
shows "∃s'. compose_actions αs s⇩0 = Some s' ∧ (∀φ∈close_world M. s' ⊨⇩= φ)"
apply (rule STRIPS_sema_sound)
apply (rule wf_plan_sound_system)
using assms
unfolding plan_action_path_def