Theory AI_Planning_Languages_Semantics.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"
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
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)
∧ (∀(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 ≡
length astI = numVars
∧ (∀x<numVars. astI!x < numVals x)
∧ wf_partial_state astG
∧ (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
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