Commit 619a85bf authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

Verified_SAT_Based_AI_Planning files

parent 67cb08d893b5
......@@ -544,6 +544,7 @@ Valuation
VectorSpace
VeriComp
Verified-Prover
Verified_SAT_Based_AI_Planning
VerifyThis2018
VerifyThis2019
Vickrey_Clarke_Groves
......
(*
Author: Fred Kurz
*)
theory CNF_Semantics_Supplement
imports "Propositional_Proof_Systems.CNF_Formulas_Sema" "CNF_Supplement"
begin
lemma not_model_if_exists_unmodeled_singleton_clause:
assumes "is_cnf F"
and "{L} \<in> cnf F"
and "\<not>lit_semantics \<nu> L"
shows "\<not>\<nu> \<Turnstile> F"
proof (rule ccontr)
assume "\<not>\<not>\<nu> \<Turnstile> F"
then have a: "\<nu> \<Turnstile> F"
by blast
moreover have "is_nnf F"
using is_nnf_cnf[OF assms(1)]
by simp
moreover {
let ?C = "{L}"
have "\<not>(\<exists>L'. L' \<in> ?C \<and> lit_semantics \<nu> L')"
using assms(3)
by fast
then have "\<not>(\<forall>C \<in> cnf F. \<exists>L. L \<in> C \<and> lit_semantics \<nu> L)"
using assms(2)
by blast
hence "\<not>cnf_semantics \<nu> (cnf F)"
unfolding cnf_semantics_def clause_semantics_def
by fast
}
ultimately have "\<not> \<nu> \<Turnstile> F"
using cnf_semantics
by blast
thus False
using a
by blast
qed
\<comment> \<open> NOTE This follows by contraposition from the previous lemma
\<open>not_model_if_exists_unmodeled_singleton_clause\<close>. \<close>
corollary model_then_all_singleton_clauses_modelled:
assumes "is_cnf F"
and "{L} \<in> cnf F"
and "\<nu> \<Turnstile> F"
shows "lit_semantics \<nu> L"
using not_model_if_exists_unmodeled_singleton_clause[OF assms(1, 2)] assms(3)
by blast
\<comment> \<open> NOTE This is essentially the \<open>\<Rightarrow>\<close> direction of the compactness theorem when treating CNFs as sets
of formulas (sets of disjunctions in this case). \<close>
lemma model_for_cnf_is_model_of_all_subsets:
assumes "cnf_semantics \<nu> \<F>"
and "\<F>' \<subseteq> \<F>"
shows "cnf_semantics \<nu> \<F>'"
proof -
{
fix C
assume "C \<in> \<F>'"
then have "C \<in> \<F>"
using assms(2)
by blast
then have "clause_semantics \<nu> C"
using assms(1)
unfolding cnf_semantics_def
by blast
}
thus ?thesis
unfolding cnf_semantics_def
by blast
qed
lemma cnf_semantics_monotonous_in_cnf_subsets_if:
assumes "\<A> \<Turnstile> \<Phi>"
and "is_cnf \<Phi>"
and "cnf \<Phi>' \<subseteq> cnf \<Phi>"
shows "cnf_semantics \<A> (cnf \<Phi>')"
proof -
{
have "is_nnf \<Phi>"
using is_nnf_cnf[OF assms(2)].
hence "cnf_semantics \<A> (cnf \<Phi>)"
using cnf_semantics assms(1)
by blast
}
thus ?thesis
using model_for_cnf_is_model_of_all_subsets[OF _ assms(3)]
by simp
qed
corollary modelling_relation_monotonous_in_cnf_subsets_if:
assumes "\<A> \<Turnstile> \<Phi>"
and "is_cnf \<Phi>"
and "is_cnf \<Phi>'"
and "cnf \<Phi>' \<subseteq> cnf \<Phi>"
shows "\<A> \<Turnstile> \<Phi>'"
proof -
have "cnf_semantics \<A> (cnf \<Phi>')"
using cnf_semantics_monotonous_in_cnf_subsets_if[OF assms(1, 2, 4)].
thus ?thesis
using cnf_semantics is_nnf_cnf[OF assms(3)]
by blast
qed
\<comment> \<open> NOTE Show that any clause \<open>C\<close> containing a subset \<open>C\<close> for which all literals
\<open>L\<close> evaluate to \<open>False\<close> for the given valuation \<open>\<A>\<close>, then the clause
semantics evaluation can be reduced to the set \<open>C - C'\<close> where all literals of
\<open>C'\<close> have been removed. \<close>
lemma lit_semantics_reducible_to_subset_if:
assumes "C' \<subseteq> C"
and "\<forall>L \<in> C'. \<not>lit_semantics \<A> L"
shows "clause_semantics \<A> C = clause_semantics \<A> (C - C')"
unfolding clause_semantics_def
using assms
by fast
end
(*
Author: Fred Kurz
*)
theory CNF_Supplement
imports "Propositional_Proof_Systems.CNF_Formulas_Sema"
begin
(* TODO fix warnings *)
fun is_literal_formula
where "is_literal_formula (Atom _) = True"
| "is_literal_formula (\<^bold>\<not>(Atom _)) = True"
| "is_literal_formula _ = False"
fun literal_formula_to_literal :: "'a formula \<Rightarrow> 'a literal"
where "literal_formula_to_literal (Atom a) = a\<^sup>+"
| "literal_formula_to_literal (\<^bold>\<not>(Atom a)) = a\<inverse>"
lemma is_literal_formula_then_cnf_is_singleton_clause:
assumes "is_literal_formula f"
obtains C where "cnf f = { C }"
proof -
consider (f_is_positive_literal) "\<exists>a. f = Atom a"
| (f_is_negative_literal) "\<exists>a. f = \<^bold>\<not>(Atom a)"
using assms is_literal_formula.elims(2)[of f]
by meson
then have "\<exists>C. cnf f = { C }"
proof (cases)
case f_is_positive_literal
then obtain a where "f = Atom a"
by force
then have "cnf f = {{ a\<^sup>+ }}"
by force
thus ?thesis
by simp
next
case f_is_negative_literal
then obtain a where "f = \<^bold>\<not>(Atom a)"
by force
then have "cnf f = {{ a\<inverse> }}"
by force
thus ?thesis
by simp
qed
thus ?thesis
using that
by presburger
qed
lemma literal_formula_to_literal_is_inverse_of_form_of_lit:
"literal_formula_to_literal (form_of_lit L) = L"
by (cases L, simp+)
lemma is_nnf_cnf:
assumes "is_cnf F"
shows "is_nnf F"
using assms
proof (induction F)
case (Or F1 F2)
have "is_disj (F1 \<^bold>\<or> F2)"
using Or.prems is_cnf.simps(5)
by simp
thus ?case
using disj_is_nnf
by blast
qed simp+
lemma cnf_of_literal_formula:
assumes "is_literal_formula f"
shows "cnf f = {{ literal_formula_to_literal f }}"
proof -
consider (f_is_positive_literal) "\<exists>a. f = Atom a"
| (f_is_negative_literal) "\<exists>a. f = (\<^bold>\<not>(Atom a))"
using assms is_literal_formula.elims(2)[of f "\<exists>a. f = Atom a"]
is_literal_formula.elims(2)[of f "\<exists>a. f = (\<^bold>\<not>(Atom a))"]
by blast
thus ?thesis
by(cases, force+)
qed
lemma is_cnf_foldr_and_if:
assumes "\<forall>f \<in> set fs. is_cnf f"
shows "is_cnf (foldr (\<^bold>\<and>) fs (\<^bold>\<not>\<bottom>))"
using assms
proof (induction fs)
case (Cons f fs)
have "foldr (\<^bold>\<and>) (f # fs) (\<^bold>\<not>\<bottom>) = f \<^bold>\<and> (foldr (\<^bold>\<and>) fs (\<^bold>\<not>\<bottom>))"
by simp
moreover {
have "\<forall>f \<in> set fs. is_cnf f"
using Cons.prems
by force
hence "is_cnf (foldr (\<^bold>\<and>) fs (\<^bold>\<not>\<bottom>))"
using Cons.IH
by blast
}
moreover have "is_cnf f"
using Cons.prems
by simp
ultimately show ?case
by simp
qed simp
end
\ No newline at end of file
(*
Author: Fred Kurz
*)
theory List_Supplement
imports Main
begin
lemma list_foot:
assumes "l \<noteq> []"
obtains y ys where "l = ys @ [y]"
proof -
{
assume a: "l \<noteq> []"
have "\<exists>y ys. l = ys @ [y]"
using a
proof (induction l)
case (Cons a l)
then show ?case
proof (cases "l = []")
case True
have "[] @ [a] = a # l"
using True
by simp
thus ?thesis
using Cons.prems(1)
by simp
next
case False
thm Cons
then obtain y ys where "l = ys @ [y]"
using Cons.IH
by blast
then have "a # l = a # ys @ [y]"
by blast
thus ?thesis
by fastforce
qed
qed simp
}
thus ?thesis
using assms that
by blast
qed
lemma list_ex_intersection: "list_ex (\<lambda>v. list_ex ((=) v) ys) xs \<longleftrightarrow> set xs \<inter> set ys \<noteq> {}"
proof -
{
assume "list_ex (\<lambda>v. list_ex ((=) v) ys) xs"
then have "\<exists>v \<in> set xs. list_ex ((=) v) ys"
using list_ex_iff
by fast
moreover have "\<forall>v. list_ex ((=) v) ys = (\<exists>v' \<in> set ys. v = v')"
using list_ex_iff
by blast
ultimately have "\<exists>v \<in> set xs. (\<exists>v' \<in> set ys. v = v')"
by blast
then obtain v v' where "v \<in> set xs" and "v' \<in> set ys" and "v = v'"
by blast
then have "set xs \<inter> set ys \<noteq> {}"
by blast
} moreover {
assume "set xs \<inter> set ys \<noteq> {}"
then obtain v v' where "v \<in> set xs" and "v' \<in> set ys" and "v = v'"
by blast
then have "list_ex (\<lambda>v. \<exists>v' \<in> set ys. v = v') xs"
using list_ex_iff
by fast
moreover have "\<forall>v. (\<exists>v' \<in> set ys. v = v') = list_ex ((=) v) ys"
using list_ex_iff
by blast
ultimately have "list_ex (\<lambda>v. list_ex ((=) v) ys) xs"
by force
} ultimately show ?thesis
by blast
qed
lemma length_map_upt: "length (map f [a..<b]) = b - a"
proof -
have "length [a..<b] = b - a"
using length_upt
by blast
moreover have "length (map f [a..<b]) = length [a..<b]"
by simp
ultimately show ?thesis
by argo
qed
lemma not_list_ex_equals_list_all_not: "(\<not>list_ex P xs) = list_all (\<lambda>x. \<not>P x) xs"
proof -
have "(\<not>list_ex P xs) = (\<not>Bex (set xs) P)"
using list_ex_iff
by blast
also have "\<dots> = Ball (set xs) (\<lambda>x. \<not>P x)"
by blast
finally show ?thesis
by (simp add: Ball_set_list_all)
qed
lemma element_of_subseqs_then_subset:
assumes "l \<in> set (subseqs l')"
shows"set l \<subseteq> set l'"
using assms
proof (induction l' arbitrary: l)
case (Cons x l')
have "set (subseqs (x # l')) = (Cons x) ` set (subseqs l') \<union> set (subseqs l')"
unfolding subseqs.simps(2) Let_def set_map set_append..
then consider (A) "l \<in> (Cons x) ` set (subseqs l')"
| (B) "l \<in> set (subseqs l')"
using Cons.prems
by blast
thus ?case
proof (cases)
case A
then obtain l'' where "l'' \<in> set (subseqs l')" and "l = x # l''"
by blast
moreover have "set l'' \<subseteq> set l'"
using Cons.IH[of l'', OF calculation(1)].
ultimately show ?thesis
by auto
next
case B
then show ?thesis
using Cons.IH
by auto
qed
qed simp
(* TODO rewrite using list comprehension \<open>embed xs = [[x]. x \<leftarrow> xs]\<close> *)
text \<open> Embed a list into a list of singleton lists. \<close>
primrec embed :: "'a list \<Rightarrow> 'a list list"
where "embed [] = []"
| "embed (x # xs) = [x] # embed xs"
lemma set_of_embed_is: "set (embed xs) = { [x] | x. x \<in> set xs }"
by (induction xs; force+)
lemma concat_is_inverse_of_embed:
"concat (embed xs) = xs"
by (induction xs; simp)
lemma embed_append[simp]: "embed (xs @ ys) = embed xs @ embed ys"
proof (induction xs)
case (Cons x xs)
have "embed (x # xs @ ys) = [x] # embed (xs @ ys)"
try0
by simp
also have "\<dots> = [x] # (embed xs @ embed ys)"
using Cons.IH
by simp
finally show ?case
by fastforce
qed simp
end
(*
Author: Fred Kurz
*)
theory Map_Supplement
imports Main
begin
lemma map_of_defined_if_constructed_from_list_of_constant_assignments:
"l = map (\<lambda>x. (x, a)) xs \<Longrightarrow> \<forall>x \<in> set xs. (map_of l) x = Some a"
proof (induction xs arbitrary: l)
case (Cons x xs)
let ?l' = "map (\<lambda>v. (v, a)) xs"
from Cons.prems(1) have "l = (x, a) # map (\<lambda>v. (v, a)) xs"
by force
moreover have "\<forall>v \<in> set xs. (map_of ?l') v = Some a"
using Cons.IH[where l="?l'"]
by blast
ultimately show ?case
by auto
qed auto
\<comment> \<open> NOTE Function graph is the set of pairs (x, f x) for a (total) function f. \<close>
\<comment> \<open> TODO Remove the first premise (follows from the second). \<close>
lemma map_of_from_function_graph_is_some_if:
fixes f :: "'a \<Rightarrow> 'b"
assumes "set xs \<noteq> {}"
and "x \<in> set xs"
shows "(map_of (map (\<lambda>x. (x, f x)) xs)) x = Some (f x)"
using assms
proof (induction xs arbitrary: f x)
\<comment> \<open> NOTE Base case follows trivially from violation of assumption \<open>set xs \<noteq> {}\<close>. \<close>
case (Cons a xs)
thm Cons
let ?m = "map_of (map (\<lambda>x. (x, f x)) xs)"
have a: "map_of (map (\<lambda>x. (x, f x)) (Cons a xs)) = ?m(a \<mapsto> f a)"
unfolding map_of_def
by simp
thus ?case
proof(cases "x = a")
case False
thus ?thesis
proof (cases "set xs = {}")
\<comment> \<open> NOTE Follows from contradiction (\<open>x \<in> set (Cons a xs) \<and> set xs = {} \<and> x \<noteq> a \<equiv> \<bottom>\<close>)\<close>
case True
thus ?thesis
using Cons.prems(2)
by fastforce
next
case False
then have "x \<in> set xs"
using \<open>x \<noteq> a\<close> Cons.prems(2)
by fastforce
moreover have "map_of (map (\<lambda>x. (x, f x)) (Cons a xs)) x = ?m x"
using \<open>x \<noteq> a\<close>
by fastforce
ultimately show ?thesis
using Cons.IH[OF False]
by presburger
qed
qed force
qed blast
lemma foldl_map_append_is_some_if:
assumes "b x = Some y \<or> (\<exists>m \<in> set ms. m x = Some y)"
and "\<forall>m' \<in> set ms. m' x = Some y \<or> m' x = None"
shows "foldl (++) b ms x = Some y"
using assms
proof (induction ms arbitrary: b)
\<comment> \<open> NOTE Induction base case violates first assumption (we have at least one element in ms
and hence \<open>ms \<noteq> []\<close>). \<close>
case (Cons a ms)
consider (b_is_some_y) "b x = Some y"
| (m_is_some_y) "\<exists>m \<in> set (a # ms). m x = Some y"
using Cons.prems(1)
by blast
hence "(b ++ a) x = Some y \<or> (\<exists>m\<in>set ms. m x = Some y)"
proof (cases)
case b_is_some_y
moreover have "a x = Some y \<or> a x = None"
using Cons.prems(2)
by simp
ultimately show ?thesis
using map_add_Some_iff[of b a x y]
by blast
next
case m_is_some_y
then show ?thesis
proof (cases "a x = Some y")
case False
then obtain m where "m \<in> set ms" and "m x = Some y"
using m_is_some_y try0
by auto
thus ?thesis
by blast
qed simp
qed
moreover have "\<forall>m' \<in> set ms. m' x = Some y \<or> m' x = None"
using Cons.prems(2)
by fastforce
ultimately show ?case using Cons.IH[where b="b ++ a"]
by simp
qed auto
(* TODO "\<forall>(v, a) \<in> set l. \<forall>(v', a') \<in> set l. v \<noteq> v' \<or> a = a'" \<leadsto>
"\<forall>(v', a') \<in> set l. v \<noteq> v' \<or> a = a'" (this is too strong; we only consider (v, a), i.e. fixed v)
*)
(* TODO isn't this the same as map_of_is_SomeI? *)
lemma map_of_constant_assignments_defined_if:
assumes "\<forall>(v, a) \<in> set l. \<forall>(v', a') \<in> set l. v \<noteq> v' \<or> a = a'"
and "(v, a) \<in> set l"
shows "map_of l v = Some a"
using assms
proof (induction l)
case (Cons x l)
thm Cons
then show ?case
proof (cases "x = (v, a)")
case False
have v_a_in_l: "(v, a) \<in> set l"
using Cons.prems(2) False
by fastforce
{
have "\<forall>(v, a) \<in> set l. \<forall>(v', a') \<in> set l. v \<noteq> v' \<or> a = a'"
using Cons.prems(1)
by auto
hence "map_of l v = Some a"
using Cons.IH v_a_in_l
by linarith
} note ih = this
{
have "x \<in> set (x # l)"
by auto
hence "fst x \<noteq> v \<or> snd x = a"
using Cons.prems(1) v_a_in_l
by fastforce
} note nb = this
\<comment> \<open> NOTE If @{text "fst x = v"} then @{text "snd x = a"} by fact @{text "nb"}; moreover if
on the other hand @{text "fst x \<noteq> v"}, then the proposition follows from the induction
hypothesis since @{text "map_of (x # l) v = map_of l v"} in that case. \<close>
thus ?thesis
using ih nb
by (cases "fst x = v") fastforce+
qed simp
qed fastforce
end
\ No newline at end of file
chapter AFP
session Verified_SAT_Based_AI_Planning (AFP) = HOL +
description {* Verified SAT-Based AI Planning *}
options [timeout = 600, document_variants = "document=-theory,/proof,/ML"]
sessions
"HOL-Data_Structures"
"AI_Planning_Languages_Semantics"
"Propositional_Proof_Systems"
"List-Index"
theories [document = false]
"List_Supplement"
"Map_Supplement"
"CNF_Supplement"
"CNF_Semantics_Supplement"
theories
"SAS_Plus_STRIPS"
"STRIPS_Representation"
"STRIPS_Semantics"
"SAS_Plus_Representation"
"SAS_Plus_Semantics"
"SAT_Plan_Base"
"SAT_Plan_Extensions"
"SAT_Solve_SAS_Plus"
"Solve_SASP"
document_files
"root.tex"
"root.bib"
(*
Author: Mohammad Abdulaziz, Fred Kurz
*)
theory SAS_Plus_Representation
imports State_Variable_Representation
begin
section "SAS+ Representation"
text \<open> We now continue by defining a concrete implementation of SAS+.\<close>
text \<open> SAS+ operators and SAS+ problems again use records. In contrast to STRIPS, the operator
effect is contracted into a single list however since we now potentially deal with more than two
possible values for each problem variable. \<close>
record ('variable, 'domain) sas_plus_operator =
precondition_of :: "('variable, 'domain) assignment list"
effect_of :: "('variable, 'domain) assignment list"
record ('variable, 'domain) sas_plus_problem =
variables_of :: "'variable list" ("(_\<^sub>\<V>\<^sub>+)" [1000] 999)
operators_of :: "('variable, 'domain) sas_plus_operator list" ("(_\<^sub>\<O>\<^sub>+)" [1000] 999)
initial_of :: "('variable, 'domain) state" ("(_\<^sub>I\<^sub>+)" [1000] 999)
goal_of :: "('variable, 'domain) state" ("(_\<^sub>G\<^sub>+)" [1000] 999)
range_of :: "'variable \<rightharpoonup> 'domain list"
definition range_of':: "('variable, 'domain) sas_plus_problem \<Rightarrow> 'variable \<Rightarrow> 'domain set" ("\<R>\<^sub>+ _ _" 52)
where
"range_of' \<Psi> v \<equiv>
(case sas_plus_problem.range_of \<Psi> v of None \<Rightarrow> {}
| Some as \<Rightarrow> set as)"
definition to_precondition
:: "('variable, 'domain) sas_plus_operator \<Rightarrow> ('variable, 'domain) assignment list"
where "to_precondition \<equiv> precondition_of"
definition to_effect
:: "('variable, 'domain) sas_plus_operator \<Rightarrow> ('variable, 'domain) Effect"
where "to_effect op \<equiv> [(v, a) . (v, a) \<leftarrow> effect_of op]"
type_synonym ('variable, 'domain) sas_plus_plan
= "('variable, 'domain) sas_plus_operator list"
type_synonym ('variable, 'domain) sas_plus_parallel_plan
= "('variable, 'domain) sas_plus_operator list list"
abbreviation empty_operator
:: "('variable, 'domain) sas_plus_operator" ("\<rho>")
where "empty_operator \<equiv> \<lparr> precondition_of = [], effect_of = [] \<rparr>"
definition is_valid_operator_sas_plus
:: "('variable, 'domain) sas_plus_problem \<Rightarrow> ('variable, 'domain) sas_plus_operator \<Rightarrow> bool"
where "is_valid_operator_sas_plus \<Psi> op \<equiv> let
pre = precondition_of op