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, opaque_lifting) domIff map_le_def map_of_SomeD not_Some_eq)
lemma [simp]: "fst ∘ (λ(a, b, c, d). (f a b c d, g a b c d)) = (λ(a,b,c,d). f a b c d)"
by auto
lemma map_mp: "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"
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.›
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:
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
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_code verify_plan nat_of_integer integer_of_nat nat_opt_of_integer Inl Inr String.explode String.implode
in SML
module_name SASP_Checker_Exported
end