Theory TopologicalProps
theory TopologicalProps
imports Main FactoredSystem ActionSeqProcess SetUtils
begin
section "Topological Properties"
subsection "Basic Definitions and Properties"
definition PLS_charles where
"PLS_charles s as PROB ≡ {length as' | as'.
(as' ∈ valid_plans PROB) ∧ (exec_plan s as' = exec_plan s as)}"
definition MPLS_charles where
"MPLS_charles PROB ≡ {Inf (PLS_charles (fst p) (snd p) PROB) | p.
((fst p) ∈ valid_states PROB)
∧ ((snd p) ∈ valid_plans PROB)
}"
definition problem_plan_bound_charles where
"problem_plan_bound_charles PROB ≡ Sup (MPLS_charles PROB)"
definition PLS_state_1 where
"PLS_state_1 s as ≡ length ` {as'. (exec_plan s as' = exec_plan s as)}"
definition MPLS_stage_1 where
"MPLS_stage_1 PROB ≡
(λ (s, as). Inf (PLS_state_1 s as))
` {(s, as). (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)}
"
definition problem_plan_bound_stage_1 where
"problem_plan_bound_stage_1 PROB ≡ Sup (MPLS_stage_1 PROB)"
for PROB :: "'a problem"
definition PLS where
"PLS s as ≡ length ` {as'. (exec_plan s as' = exec_plan s as) ∧ (subseq as' as)}"
lemma finite_PLS: "finite (PLS s as)"
proof -
let ?S = "{as'. (exec_plan s as' = exec_plan s as) ∧ (subseq as' as)}"
let ?S1 = "length ` {as'. (exec_plan s as' = exec_plan s as) }"
let ?S2 = "length ` {as'. (subseq as' as)}"
let ?n = "length as + 1"
have "finite ?S2"
using bounded_nat_set_is_finite[where n = ?n and N = ?S2]
by fastforce
moreover have "length ` ?S ⊆ (?S1 ∩ ?S2)"
by blast
ultimately have "finite (length ` ?S)"
using infinite_super
by auto
then show ?thesis
unfolding PLS_def
by blast
qed
definition MPLS where
"MPLS PROB ≡
(λ (s, as). Inf (PLS s as))
` {(s, as). (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)}
"
definition problem_plan_bound where
"problem_plan_bound PROB ≡ Sup (MPLS PROB)"
lemma expanded_problem_plan_bound_thm_1:
fixes PROB
shows "
(problem_plan_bound PROB) = Sup (
(λ(s,as). Inf (PLS s as)) `
{(s, as). (s ∈ (valid_states PROB)) ∧ (as ∈ valid_plans PROB)}
)
"
unfolding problem_plan_bound_def MPLS_def
by blast
lemma expanded_problem_plan_bound_thm:
fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set"
shows "
problem_plan_bound PROB = Sup ({Inf (PLS s as) | s as.
(s ∈ valid_states PROB)
∧ (as ∈ valid_plans PROB)
})
"
proof -
{
have "(
{Inf (PLS s as) | s as. (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)}
) = ((λ(s, as). Inf (PLS s as)) ` {(s, as).
(s ∈ valid_states PROB)
∧ (as ∈ valid_plans PROB)
})
"
by fast
also have "… =
(λ(s, as). Inf (PLS s as)) `
({s. fmdom' s = prob_dom PROB} × {as. set as ⊆ PROB})
"
unfolding valid_states_def valid_plans_def
by simp
finally have "
Sup ({Inf (PLS s as) | s as. (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)})
= Sup (
(λ(s, as). Inf (PLS s as)) `
({s. fmdom' s = prob_dom PROB} × {as. set as ⊆ PROB})
)
"
by argo
}
moreover have "
problem_plan_bound PROB
=
Sup ((λ(s, as). Inf (PLS s as)) `
({s. fmdom' s = prob_dom PROB} × {as. set as ⊆ PROB}))
"
unfolding problem_plan_bound_def MPLS_def valid_states_def valid_plans_def
by fastforce
ultimately show "
problem_plan_bound PROB
= Sup ({Inf (PLS s as) | s as.
(s ∈ valid_states PROB)
∧ (as ∈ valid_plans PROB)
})
"
by argo
qed
subsection "Recurrence Diameter"
text ‹ The recurrence diameter---defined as the longest simple path in the digraph modelling the
state space---provides a loose upper bound on the system diameter. [Abdulaziz et al., Definition 9,
p.15] ›
fun valid_path where
"valid_path Pi [] = True"
| "valid_path Pi [s] = (s ∈ valid_states Pi)"
| "valid_path Pi (s1 # s2 # rest) = (
(s1 ∈ valid_states Pi)
∧ (∃a. (a ∈ Pi) ∧ (exec_plan s1 [a] = s2))
∧ (valid_path Pi (s2 # rest))
)"
lemma valid_path_ITP2015: "
(valid_path Pi [] ⟷ True)
∧ (valid_path Pi [s] ⟷ (s ∈ valid_states Pi))
∧ (valid_path Pi (s1 # s2 # rest) ⟷
(s1 ∈ valid_states Pi)
∧ (∃a.
(a ∈ Pi)
∧ (exec_plan s1 [a] = s2)
)
∧ (valid_path Pi (s2 # rest))
)
"
using valid_states_def
by simp
definition RD where
"RD Pi ≡ (Sup {length p - 1 | p. valid_path Pi p ∧ distinct p})"
for Pi :: "'a problem"
lemma in_PLS_leq_2_pow_n:
fixes PROB :: "'a problem" and s :: "'a state" and as
assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(∃x.
(x ∈ PLS s as)
∧ (x ≤ (2 ^ card (prob_dom PROB)) - 1)
)"
proof -
obtain as' where 1:
"exec_plan s as = exec_plan s as'" "subseq as' as" "length as' ≤ 2 ^ card (prob_dom PROB) - 1"
using assms main_lemma
by blast
let ?x="length as'"
have "?x ∈ PLS s as"
unfolding PLS_def
using 1
by simp
moreover have "?x ≤ 2 ^ card (prob_dom PROB) - 1"
using 1(3)
by blast
ultimately show "(∃x.
(x ∈ PLS s as)
∧ (x ≤ (2 ^ card (prob_dom PROB)) - 1)
)"
unfolding PLS_def
by blast
qed
lemma in_MPLS_leq_2_pow_n:
fixes PROB :: "'a problem" and x
assumes "finite PROB" "(x ∈ MPLS PROB)"
shows "(x ≤ 2 ^ card (prob_dom PROB) - 1)"
proof -
let ?mpls = "MPLS PROB"
have "?mpls =
(λ (s, as). Inf (PLS s as)) `
{(s, as). (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)}
"
using MPLS_def
by blast
then obtain s :: "('a, bool) fmap" and as :: "(('a, bool) fmap × ('a, bool) fmap) list"
where obtain_s_as: "x ∈
((λ (s, as). Inf (PLS s as)) `
{(s, as). (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)})
"
using assms(2)
by blast
then have
"x ∈ {Inf (PLS (fst p) (snd p)) | p. (fst p ∈ valid_states PROB) ∧ (snd p ∈ valid_plans PROB)}"
using assms(1) obtain_s_as
by auto
then have
"∃ p. x = Inf (PLS (fst p) (snd p)) ∧ (fst p ∈ valid_states PROB) ∧ (snd p ∈ valid_plans PROB)"
by blast
then obtain p :: "('a, bool) fmap × (('a, bool) fmap × ('a, bool) fmap) list" where obtain_p:
"x = Inf (PLS (fst p) (snd p))" "(fst p ∈ valid_states PROB)" "(snd p ∈ valid_plans PROB)"
by blast
then have "fst p ∈ valid_states PROB" "snd p ∈ valid_plans PROB"
using obtain_p
by blast+
then obtain x' :: nat where obtain_x':
"x' ∈ PLS (fst p) (snd p) ∧ x' ≤ 2 ^ card (prob_dom PROB) - 1"
using assms(1) in_PLS_leq_2_pow_n[where s = "fst p" and as = "snd p"]
by blast
then have 1: "x' ≤ 2 ^ card (prob_dom PROB) - 1" "x' ∈ PLS (fst p) (snd p)"
"x = Inf (PLS (fst p) (snd p))" "finite (PLS (fst p) (snd p))"
using obtain_x' obtain_p finite_PLS
by blast+
moreover have "x ≤ x'"
using 1(2, 4) obtain_p(1) cInf_le_finite
by blast
ultimately show "(x ≤ 2 ^ card (prob_dom PROB) - 1)"
by linarith
qed
lemma FINITE_MPLS:
assumes "finite (Pi :: 'a problem)"
shows "finite (MPLS Pi)"
proof -
have "∀x ∈ MPLS Pi. x ≤ 2 ^ card (prob_dom Pi) - 1"
using assms in_MPLS_leq_2_pow_n
by blast
then show "finite (MPLS Pi)"
using mems_le_finite[of "MPLS Pi" "2 ^ card (prob_dom Pi) - 1"]
by blast
qed
fun statelist' where
"statelist' s [] = [s]"
| "statelist' s (a # as) = (s # statelist' (state_succ s a) as)"
lemma LENGTH_statelist':
fixes as s
shows "length (statelist' s as) = (length as + 1)"
by (induction as arbitrary: s) auto
lemma valid_path_statelist':
fixes as and s :: "('a, 'b) fmap"
assumes "(as ∈ valid_plans Pi)" "(s ∈ valid_states Pi)"
shows "(valid_path Pi (statelist' s as))"
using assms
proof (induction as arbitrary: s Pi)
case cons: (Cons a as)
then have 1: "a ∈ Pi" "as ∈ valid_plans Pi"
using valid_plan_valid_head valid_plan_valid_tail
by metis+
then show ?case
proof (cases as)
case Nil
{
have "state_succ s a ∈ valid_states Pi"
using 1 cons.prems(2) valid_action_valid_succ
by blast
then have "valid_path Pi [state_succ s a]"
using 1 cons.prems(2) cons.IH
by force
moreover have "(∃aa. aa ∈ Pi ∧ exec_plan s [aa] = state_succ s a)"
using 1(1)
by fastforce
ultimately have "valid_path Pi (statelist' s [a])"
using cons.prems(2)
by simp
}
then show ?thesis
using Nil
by blast
next
case (Cons b list)
{
have "s ∈ valid_states Pi"
using cons.prems(2)
by simp
then have
"valid_path Pi (state_succ s a # statelist' (state_succ (state_succ s a) b) list)"
using 1 cons.IH cons.prems(2) Cons lemma_1_i
by fastforce
moreover have
"(∃aa b. (aa, b) ∈ Pi ∧ state_succ s (aa, b) = state_succ s a)"
using 1(1) surjective_pairing
by metis
ultimately have "valid_path Pi (statelist' s (a # b # list))"
using cons.prems(2)
by auto
}
then show ?thesis
using Cons
by blast
qed
qed simp
lemma statelist'_exec_plan:
fixes a s p
assumes "(statelist' s as = p)"
shows "(exec_plan s as = last p)"
using assms
apply(induction as arbitrary: s p)
apply(auto)
apply(cases "as")
by
(metis LENGTH_statelist' One_nat_def add_Suc_right list.size(3) nat.simps(3))
(metis (no_types) LENGTH_statelist' One_nat_def add_Suc_right list.size(3) nat.simps(3))
lemma statelist'_EQ_NIL: "statelist' s as ≠ []"
by (cases as) auto
lemma statelist'_TAKE_i:
assumes "Suc m ≤ length (a # as)"
shows "m ≤ length as"
using assms
by (induction as arbitrary: a m) auto
lemma statelist'_TAKE:
fixes as s p
assumes "(statelist' s as = p)"
shows "(∀n. n ≤ length as ⟶ (exec_plan s (take n as)) = (p ! n))"
using assms
proof (induction as arbitrary: s p)
case Nil
{
fix n
assume P1: "n ≤ length []"
then have "exec_plan s (take n []) = s"
by simp
moreover have "p ! 0 = s"
using Nil.prems
by force
ultimately have "exec_plan s (take n []) = p ! n"
using P1
by simp
}
then show ?case by blast
next
case (Cons a as)
{
fix n
assume P2: "n ≤ length (a # as)"
then have "exec_plan s (take n (a # as)) = p ! n"
using Cons.prems
proof (cases "n = 0")
case False
then obtain m where a: "n = Suc m"
using not0_implies_Suc
by presburger
moreover have b: "statelist' s (a # as) ! n = statelist' (state_succ s a) as ! m"
using a nth_Cons_Suc
by simp
moreover have c: "exec_plan s (take n (a # as)) = exec_plan (state_succ s a) (take m as)"
using a
by force
moreover have "m ≤ length as"
using a P2 statelist'_TAKE_i
by simp
moreover have
"exec_plan (state_succ s a) (take m as) = statelist' (state_succ s a) as ! m"
using calculation(2, 3, 4) Cons.IH
by blast
ultimately show ?thesis
using Cons.prems
by argo
qed fastforce
}
then show ?case by blast
qed
lemma MPLS_nempty:
fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set"
assumes "finite PROB"
shows "MPLS PROB ≠ {}"
proof -
let ?S="{(s, as). s ∈ valid_states PROB ∧ as ∈ valid_plans PROB}"
obtain s :: "('a, 'b) fmap" where "s ∈ valid_states PROB"
using assms valid_states_nempty
by blast
moreover have "[] ∈ valid_plans PROB"
using empty_plan_is_valid
by auto
ultimately have "(s, []) ∈ ?S"
by blast
then show ?thesis
unfolding MPLS_def
by blast
qed
theorem bound_main_lemma:
fixes PROB :: "'a problem"
assumes "finite PROB"
shows "(problem_plan_bound PROB ≤ (2 ^ (card (prob_dom PROB))) - 1)"
proof -
have "MPLS PROB ≠ {}"
using assms MPLS_nempty
by auto
moreover have "(∀x. x ∈ MPLS PROB ⟶ x ≤ 2 ^ card (prob_dom PROB) - 1)"
using assms in_MPLS_leq_2_pow_n
by blast
ultimately show ?thesis
unfolding problem_plan_bound_def
using cSup_least
by blast
qed
lemma bound_child_parent_card_state_set_cons:
fixes P f
assumes "(∀(PROB :: 'a problem) as (s :: 'a state).
(P PROB)
∧ (as ∈ valid_plans PROB)
∧ (s ∈ valid_states PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB)
)
)"
shows "(∀PROB s as.
(P PROB)
∧ (as ∈ valid_plans PROB)
∧ (s ∈ (valid_states PROB))
⟶ (∃x.
(x ∈ PLS s as)
∧ (x < f PROB)
)
)"
proof -
{
fix PROB :: "'a problem" and as and s :: "'a state"
assume P1: "(P PROB)"
"(as ∈ valid_plans PROB)"
"(s ∈ valid_states PROB)"
"(∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB)
)"
have "(exec_plan s as ∈ valid_states PROB)"
using assms P1 valid_as_valid_exec
by blast
then have "(P PROB)
∧ (as ∈ valid_plans PROB)
∧ (s ∈ (valid_states PROB))
⟶ (∃x.
(x ∈ PLS s as)
∧ (x < f PROB)
)
"
unfolding PLS_def
using P1
by force
}
then show "(∀PROB s as.
(P PROB)
∧ (as ∈ valid_plans PROB)
∧ (s ∈ (valid_states PROB))
⟶ (∃x.
(x ∈ PLS s as)
∧ (x < f PROB)
)
)"
using assms
by simp
qed
lemma bound_on_all_plans_bounds_MPLS:
fixes P f
assumes "(∀(PROB :: 'a problem) as (s :: 'a state).
(P PROB)
∧ (s ∈ valid_states PROB)
∧ (as ∈ valid_plans PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB)
)
)"
shows "(∀PROB x. P PROB
⟶ (x ∈ MPLS(PROB))
⟶ (x < f PROB)
)"
proof -
{
fix PROB :: "'a problem" and as and s :: "'a state"
assume "(P PROB)"
"(s ∈ valid_states PROB)"
"(as ∈ valid_plans PROB)"
"(∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB)
)"
then have "(∃x. x ∈ PLS s as ∧ x < f PROB)"
using assms(1) bound_child_parent_card_state_set_cons[where P = P and f = f]
by presburger
}
note 1 = this
{
fix PROB x
assume P1: "P PROB" "x ∈ MPLS PROB"
then obtain s as where a:
"x = Inf (PLS s as)" "s ∈ valid_states PROB" "as ∈ valid_plans PROB"
unfolding MPLS_def
by auto
moreover have "(∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB)
)"
using P1(1) assms calculation(2, 3)
by blast
ultimately obtain x' where "x' ∈ PLS s as" "x' < f PROB"
using P1 1
by blast
then have "x < f PROB"
using a(1) mem_lt_imp_MIN_lt
by fastforce
}
then show ?thesis
by blast
qed
lemma bound_child_parent_card_state_set_cons_finite:
fixes P f
assumes "(∀PROB as s.
P PROB ∧ finite PROB ∧ as ∈ (valid_plans PROB) ∧ s ∈ (valid_states PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ subseq as' as
∧ length as' < f(PROB)
)
)"
shows "(∀PROB s as.
P PROB ∧ finite PROB ∧ as ∈ (valid_plans PROB) ∧ (s ∈ (valid_states PROB))
⟶ (∃x. (x ∈ PLS s as) ∧ x < f PROB)
)"
proof -
{
fix PROB s as
assume "P PROB" "finite PROB" "as ∈ (valid_plans PROB)" "s ∈ (valid_states PROB)"
" (∃as'.
(exec_plan s as = exec_plan s as')
∧ subseq as' as
∧ length as' < f PROB
)"
then obtain as' where
"(exec_plan s as = exec_plan s as')" "subseq as' as" "length as' < f PROB"
by blast
moreover have "length as' ∈ PLS s as"
unfolding PLS_def
using calculation
by fastforce
ultimately have "(∃x. (x ∈ PLS s as) ∧ x < f PROB)"
by blast
}
then show "(∀PROB s as.
P PROB
∧ finite PROB
∧ as ∈ (valid_plans PROB)
∧ (s ∈ (valid_states PROB))
⟶ (∃x. (x ∈ PLS s as) ∧ x < f PROB)
)"
using assms
by auto
qed
lemma bound_on_all_plans_bounds_MPLS_finite:
fixes P f
assumes "(∀PROB as s.
P PROB ∧ finite PROB ∧ s ∈ (valid_states PROB) ∧ as ∈ (valid_plans PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ subseq as' as
∧ length as' < f(PROB)
)
)"
shows "(∀PROB x.
P PROB ∧ finite PROB
⟶ (x ∈ MPLS PROB)
⟶ x < f PROB
)"
proof -
{
fix PROB x
assume P1: "P PROB" "finite PROB" "x ∈ MPLS PROB"
then obtain s as where a:
"x = Inf (PLS s as)" "s ∈ valid_states PROB" "as ∈ valid_plans PROB"
unfolding MPLS_def
by auto
moreover have "(∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB)
)"
using P1(1, 2) assms calculation(2, 3)
by blast
moreover obtain x' where "x' ∈ PLS s as" "x' < f PROB"
using PLS_def calculation(4)
by fastforce
then have "x < f PROB"
using a(1) mem_lt_imp_MIN_lt
by fastforce
}
then show ?thesis
using assms
by blast
qed
lemma bound_on_all_plans_bounds_problem_plan_bound:
fixes P f
assumes "(∀PROB as s.
(P PROB)
∧ finite PROB
∧ (s ∈ valid_states PROB)
∧ (as ∈ valid_plans PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB)
)
)"
shows "(∀PROB.
(P PROB)
∧ finite PROB
⟶ (problem_plan_bound PROB < f PROB)
)"
proof -
have 1: "∀PROB x.
P PROB
∧ finite PROB
⟶ x ∈ MPLS PROB
⟶ x < f PROB
"
using assms bound_on_all_plans_bounds_MPLS_finite
by blast
{
fix PROB x
assume "P PROB ∧ finite PROB
⟶ x ∈ MPLS PROB
⟶ x < f PROB
"
then have "∀PROB.
P PROB ∧ finite PROB
⟶ problem_plan_bound PROB < f PROB
"
unfolding problem_plan_bound_def
using 1 bound_child_parent_not_eq_last_diff_paths 1 MPLS_nempty
by metis
then have "∀PROB.
P PROB ∧ finite PROB
⟶ problem_plan_bound PROB < f PROB
"
using MPLS_nempty
by blast
}
then show "(∀PROB.
(P PROB)
∧ finite PROB
⟶ (problem_plan_bound PROB < f PROB)
)"
using 1
by blast
qed
lemma bound_child_parent_card_state_set_cons_thesis:
assumes "finite PROB" "(∀as s.
as ∈ (valid_plans PROB)
∧ s ∈ (valid_states PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ subseq as' as
∧ length as' < k
)
)" "as ∈ (valid_plans PROB)" "(s ∈ (valid_states PROB))"
shows "(∃x. (x ∈ PLS s as) ∧ x < k)"
unfolding PLS_def
using assms
by fastforce
lemma x_in_MPLS_if:
fixes x PROB
assumes "x ∈ MPLS PROB"
shows "∃s as. s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧ x = Inf (PLS s as)"
using assms
unfolding MPLS_def
by fast
lemma bound_on_all_plans_bounds_MPLS_thesis:
assumes "finite PROB" "(∀as s.
(s ∈ valid_states PROB)
∧ (as ∈ valid_plans PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < k)
)
)" "(x ∈ MPLS PROB)"
shows "(x < k)"
proof -
obtain s as where 1: "s ∈ valid_states PROB" "as ∈ valid_plans PROB" "x = Inf (PLS s as)"
using assms(3) x_in_MPLS_if
by blast
then obtain x' :: nat where "x' ∈ PLS s as" "x' < k"
using assms(1, 2) bound_child_parent_card_state_set_cons_thesis
by blast
then have "Inf (PLS s as) < k"
using mem_lt_imp_MIN_lt
by blast
then show "x < k"
using 1
by simp
qed
lemma bounded_MPLS_contains_supremum:
fixes PROB
assumes "finite PROB" "(∃k. ∀x ∈ MPLS PROB. x < k)"
shows "Sup (MPLS PROB) ∈ MPLS PROB"
proof -
obtain k where "∀x ∈ MPLS PROB. x < k"
using assms(2)
by blast
moreover have "finite (MPLS PROB)"
using assms(2) finite_nat_set_iff_bounded
by presburger
moreover have "MPLS PROB ≠ {}"
using assms(1) MPLS_nempty
by auto
ultimately show "Sup (MPLS PROB) ∈ MPLS PROB"
unfolding Sup_nat_def
by simp
qed
lemma bound_on_all_plans_bounds_problem_plan_bound_thesis':
assumes "finite PROB" "(∀as s.
s ∈ (valid_states PROB)
∧ as ∈ (valid_plans PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ subseq as' as
∧ length as' < k
)
)"
shows "problem_plan_bound PROB < k"
proof -
have 1: "∀x ∈ MPLS PROB. x < k"
using assms(1, 2) bound_on_all_plans_bounds_MPLS_thesis
by blast
then have "Sup (MPLS PROB) ∈ MPLS PROB"
using assms(1) bounded_MPLS_contains_supremum
by auto
then have "Sup (MPLS PROB) < k"
using 1
by blast
then show ?thesis
unfolding problem_plan_bound_def
by simp
qed
lemma bound_on_all_plans_bounds_problem_plan_bound_thesis:
assumes "finite PROB" "(∀as s.
(s ∈ valid_states PROB)
∧ (as ∈ valid_plans PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' ≤ k)
)
)"
shows "(problem_plan_bound PROB ≤ k)"
proof -
have 1: "∀x∈MPLS PROB. x < k + 1"
using assms(1, 2) bound_on_all_plans_bounds_MPLS_thesis[where k = "k + 1"] Suc_eq_plus1
less_Suc_eq_le
by metis
then have "Sup (MPLS PROB) ∈ MPLS PROB"
using assms(1) bounded_MPLS_contains_supremum
by fast
then show "(problem_plan_bound PROB ≤ k)"
unfolding problem_plan_bound_def
using 1
by fastforce
qed
lemma bound_on_all_plans_bounds_problem_plan_bound_:
fixes P f PROB
assumes "(∀PROB' as s.
finite PROB ∧ (P PROB') ∧ (s ∈ valid_states PROB') ∧ (as ∈ valid_plans PROB')
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB')
)
)" "(P PROB)" "finite PROB"
shows "(problem_plan_bound PROB < f PROB)"
unfolding problem_plan_bound_def MPLS_def
using assms bound_on_all_plans_bounds_problem_plan_bound_thesis' expanded_problem_plan_bound_thm_1
by metis
lemma S_VALID_AS_VALID_IMP_MIN_IN_PLS:
fixes PROB s as
assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(Inf (PLS s as) ∈ (MPLS PROB))"
unfolding MPLS_def
using assms
by fast
lemma problem_plan_bound_ge_min_pls:
fixes PROB :: "'a problem" and s :: "'a state" and as k
assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
"(problem_plan_bound PROB ≤ k)"
shows "(Inf (PLS s as) ≤ problem_plan_bound PROB)"
proof -
have "Inf (PLS s as) ∈ MPLS PROB"
using assms(2, 3) S_VALID_AS_VALID_IMP_MIN_IN_PLS
by blast
moreover have "finite (MPLS PROB)"
using assms(1) FINITE_MPLS
by blast
ultimately have "Inf (PLS s as) ≤ Sup (MPLS PROB)"
using le_cSup_finite
by blast
then show ?thesis
unfolding problem_plan_bound_def
by simp
qed
lemma PLS_NEMPTY:
fixes s as
shows "PLS s as ≠ {}"
unfolding PLS_def
by blast
lemma PLS_nempty_and_has_min:
fixes s as
shows "(∃x. (x ∈ PLS s as) ∧ (x = Inf (PLS s as)))"
proof -
have "PLS s as ≠ {}"
using PLS_NEMPTY
by blast
then have "Inf (PLS s as) ∈ PLS s as"
unfolding Inf_nat_def
using LeastI_ex Max_in finite_PLS
by metis
then show ?thesis
by blast
qed
lemma PLS_works:
fixes x s as
assumes "(x ∈ PLS s as)"
shows"(∃as'.
(exec_plan s as = exec_plan s as')
∧ (length as' = x)
∧ (subseq as' as)
)"
using assms
unfolding PLS_def
by (smt imageE mem_Collect_eq)
lemma problem_plan_bound_works:
fixes PROB :: "'a problem" and as and s :: "'a state"
assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' ≤ problem_plan_bound PROB)
)"
proof -
have "problem_plan_bound PROB ≤ 2 ^ card (prob_dom PROB) - 1"
using assms(1) bound_main_lemma
by blast
then have 1: "Inf (PLS s as) ≤ problem_plan_bound PROB"
using
assms(1, 2, 3)
problem_plan_bound_ge_min_pls
by blast
then have "∃x. x ∈ PLS s as ∧ x = Inf (PLS s as)"
using PLS_nempty_and_has_min
by blast
then have "Inf (PLS s as) ∈ (PLS s as)"
by blast
then obtain as' where 2:
"exec_plan s as = exec_plan s as'" "length as' = Inf (PLS s as)" "subseq as' as"
using PLS_works
by blast
then have "length as' ≤ problem_plan_bound PROB"
using 1
by argo
then show "(∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' ≤ problem_plan_bound PROB)
)"
using 2(1) 2(3)
by blast
qed
definition MPLS_s where
"MPLS_s PROB s ≡ (λ (s, as). Inf (PLS s as)) ` {(s, as) | as. as ∈ valid_plans PROB}"
lemma bound_main_lemma_s_3:
fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set" and s
shows "MPLS_s PROB s ≠ {}"
proof -
have "[] ∈ valid_plans PROB"
using empty_plan_is_valid
by blast
then have "(s, []) ∈ {(s, as). as ∈ valid_plans PROB}"
by simp
then show "MPLS_s PROB s ≠ {}"
unfolding MPLS_s_def
by blast
qed
definition problem_plan_bound_s where
"problem_plan_bound_s PROB s = Sup (MPLS_s PROB s)"
lemma bound_on_all_plans_bounds_PLS_s:
fixes P f
assumes "(∀PROB as s.
finite PROB ∧ (P PROB) ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB s)
)
)"
shows "(∀PROB s as.
finite PROB ∧ (P PROB) ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB)
⟶ (∃x.
(x ∈ PLS s as)
∧ (x < f PROB s)
)
)"
using assms
unfolding PLS_def
by fastforce
lemma bound_on_all_plans_bounds_MPLS_s_i:
fixes PROB s x
assumes "s ∈ valid_states PROB" "x ∈ MPLS_s PROB s"
shows "∃as. x = Inf (PLS s as) ∧ as ∈ valid_plans PROB"
proof -
let ?S="{(s, as) | as. as ∈ valid_plans PROB}"
obtain x' where 1:
"x' ∈ ?S"
"x = (λ (s, as). Inf (PLS s as)) x'"
using assms
unfolding MPLS_s_def
by blast
let ?as="snd x'"
let ?s="fst x'"
have "?as ∈ valid_plans PROB"
using 1(1)
by auto
moreover have "?s = s"
using 1(1)
by fastforce
moreover have "x = Inf (PLS ?s ?as)"
using 1(2)
by (simp add: case_prod_unfold)
ultimately show ?thesis
by blast
qed
lemma bound_on_all_plans_bounds_MPLS_s:
fixes P f
assumes "(∀PROB as s.
finite PROB ∧ (P PROB) ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB s)
)
)"
shows "(∀PROB x s.
finite PROB ∧ (P PROB) ∧ (s ∈ valid_states PROB) ⟶ (x ∈ MPLS_s PROB s)
⟶ (x < f PROB s)
)"
using assms
unfolding MPLS_def
proof -
have 1: "∀PROB s as.
finite PROB ∧ P PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB ⟶
(∃x. x ∈ PLS s as ∧ x < f PROB s)"
using bound_on_all_plans_bounds_PLS_s[OF assms] .
{
fix PROB x and s :: "('a, 'b) fmap"
assume P1: "finite PROB" "(P PROB)" "(s ∈ valid_states PROB)"
{
assume "(x ∈ MPLS_s PROB s)"
then obtain as where i: "x = Inf (PLS s as)" "as ∈ valid_plans PROB"
using P1 bound_on_all_plans_bounds_MPLS_s_i
by blast
then obtain x' where "x' ∈ PLS s as" "x' < f PROB s"
using P1 i 1
by blast
then have "x < f PROB s"
using mem_lt_imp_MIN_lt i(1)
by blast
}
then have "(x ∈ MPLS_s PROB s) ⟶ (x < f PROB s)"
by blast
}
then show ?thesis
by blast
qed
lemma Sup_MPLS_s_lt_if:
fixes PROB s k
assumes "(∀x∈MPLS_s PROB s. x < k)"
shows "Sup (MPLS_s PROB s) < k"
proof -
have "MPLS_s PROB s ≠ {}"
using bound_main_lemma_s_3
by fast
then have "Sup (MPLS_s PROB s) ∈ MPLS_s PROB s"
using assms Sup_nat_def bounded_nat_set_is_finite
by force
then show "Sup (MPLS_s PROB s) < k"
using assms
by blast
qed
lemma bound_child_parent_lemma_s_2:
fixes PROB :: "'a problem" and P :: "'a problem ⇒ bool" and s f
assumes "(∀(PROB :: 'a problem) as s.
finite PROB ∧ (P PROB) ∧ (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB s)
)
)"
shows "(
finite PROB ∧ (P PROB) ∧ (s ∈ valid_states PROB)
⟶ problem_plan_bound_s PROB s < f PROB s
)"
proof -
have "∀(PROB :: 'a problem) x s.
finite PROB ∧ P PROB ∧ s ∈ valid_states PROB
⟶ x ∈ MPLS_s PROB s
⟶ x < f PROB s
"
using assms bound_on_all_plans_bounds_MPLS_s[of P f]
by simp
then show
"finite PROB ∧ (P PROB) ∧ (s ∈ valid_states PROB) ⟶ (problem_plan_bound_s PROB s < f PROB s)"
unfolding problem_plan_bound_s_def
using Sup_MPLS_s_lt_if problem_plan_bound_s_def
by metis
qed
theorem bound_main_lemma_reachability_s:
fixes PROB :: "'a problem" and s
assumes "finite PROB" "s ∈ valid_states PROB"
shows "(problem_plan_bound_s PROB s < card (reachable_s PROB s))"
proof -
{
fix PROB :: "'a problem" and s :: "'a state" and as
assume P1: "finite PROB" "s ∈ valid_states PROB" "as ∈ valid_plans PROB"
then obtain as' where a: "exec_plan s as = exec_plan s as'" "subseq as' as"
"length as' ≤ card (reachable_s PROB s) - 1"
using P1 main_lemma_reachability_s
by blast
then have "length as' < card (reachable_s PROB s)"
using P1(1, 2) card_reachable_s_non_zero
by fastforce
then have "(∃as'.
exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' < card (reachable_s PROB s))
"
using a
by blast
}
then have "
finite PROB ∧ True ∧ s ∈ valid_states PROB
⟶ problem_plan_bound_s PROB s < card (reachable_s PROB s)
"
using bound_child_parent_lemma_s_2[where PROB = PROB and P = "λ_. True" and s = s
and f = "λPROB s. card (reachable_s PROB s)"]
by blast
then show ?thesis
using assms(1, 2)
by blast
qed
lemma problem_plan_bound_s_LESS_EQ_problem_plan_bound_thm:
fixes PROB :: "'a problem" and s :: "'a state"
assumes "finite PROB" "(s ∈ valid_states PROB)"
shows "(problem_plan_bound_s PROB s < problem_plan_bound PROB + 1)"
proof -
{
fix PROB :: "'a problem" and s :: "'a state" and as
assume "finite PROB" "s ∈ valid_states PROB" "as ∈ valid_plans PROB"
then obtain as' where a: "exec_plan s as = exec_plan s as'" "subseq as' as"
"length as' ≤ problem_plan_bound PROB"
using problem_plan_bound_works
by blast
then have "length as' < problem_plan_bound PROB + 1"
by linarith
then have "∃as'.
exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' ≤ problem_plan_bound PROB + 1
"
using a
by fastforce
}
then have "∀(PROB :: 'a problem) as s.
finite PROB ∧ True ∧ s ∈ valid_states PROB ∧ as ∈ valid_plans PROB
⟶ (∃as'.
exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' < problem_plan_bound PROB + 1)
"
by (metis Suc_eq_plus1 problem_plan_bound_works le_imp_less_Suc)
then show "(problem_plan_bound_s PROB s < problem_plan_bound PROB + 1)"
using assms bound_child_parent_lemma_s_2[where PROB = PROB and s = s and P = "λ_. True"
and f = "λPROB s. problem_plan_bound PROB + 1"]
by fast
qed
lemma AS_VALID_MPLS_VALID:
fixes PROB as
assumes "(as ∈ valid_plans PROB)"
shows "(Inf (PLS s as) ∈ MPLS_s PROB s)"
using assms
unfolding MPLS_s_def
by fast
lemma bound_main_lemma_s_1:
fixes PROB :: "'a problem" and s :: "'a state" and x
assumes "finite PROB" "s ∈ (valid_states PROB)" "x ∈ MPLS_s PROB s"
shows "(x ≤ (2 ^ card (prob_dom PROB)) - 1)"
proof -
obtain as :: "(('a, bool) fmap × ('a, bool) fmap) list" where "as ∈ valid_plans PROB"
using empty_plan_is_valid
by blast
then obtain x where 1: "x ∈ PLS s as" "x ≤ 2 ^ card (prob_dom PROB) - 1"
using assms in_PLS_leq_2_pow_n
by blast
then have "Inf (PLS s as) ≤ 2 ^ card (prob_dom PROB) - 1"
using mem_le_imp_MIN_le[where s = "PLS s as" and k = "2 ^ card (prob_dom PROB) - 1"]
by blast
then have "x ≤ 2 ^ card (prob_dom PROB) - 1"
using assms(3) 1
by blast
then show ?thesis
using assms(1, 2, 3) S_VALID_AS_VALID_IMP_MIN_IN_PLS bound_on_all_plans_bounds_MPLS_s_i
in_MPLS_leq_2_pow_n
by metis
qed
lemma problem_plan_bound_s_ge_min_pls:
fixes PROB :: "'a problem" and as k s
assumes "finite PROB" "s ∈ (valid_states PROB)" "as ∈ (valid_plans PROB)"
"problem_plan_bound_s PROB s ≤ k"
shows "(Inf (PLS s as) ≤ problem_plan_bound_s PROB s)"
proof -
have "∀x∈MPLS_s PROB s. x ≤ 2 ^ card (prob_dom PROB) - 1"
using assms(1, 2) bound_main_lemma_s_1 by blast
then have 1: "finite (MPLS_s PROB s)"
using mems_le_finite[where s = "MPLS_s PROB s" and k = "2 ^ card (prob_dom PROB) - 1"]
by blast
then have "MPLS_s PROB s ≠ {}"
using bound_main_lemma_s_3
by fast
then have "Inf (PLS s as) ∈ MPLS_s PROB s"
using assms AS_VALID_MPLS_VALID
by blast
then show "(Inf (PLS s as) ≤ problem_plan_bound_s PROB s)"
unfolding problem_plan_bound_s_def
using 1 le_cSup_finite
by blast
qed
theorem bound_main_lemma_s:
fixes PROB :: "'a problem" and s
assumes "finite PROB" "(s ∈ valid_states PROB)"
shows "(problem_plan_bound_s PROB s ≤ 2 ^ (card (prob_dom PROB)) - 1)"
proof -
have 1: "∀x∈MPLS_s PROB s. x ≤ 2 ^ card (prob_dom PROB) - 1"
using assms bound_main_lemma_s_1
by metis
then have "MPLS_s PROB s ≠ {}"
using bound_main_lemma_s_3
by fast
then have "Sup (MPLS_s PROB s) ≤ 2 ^ card (prob_dom PROB) - 1"
using 1 bound_main_lemma_2[where s = "MPLS_s PROB s" and k = "2 ^ card (prob_dom PROB) - 1"]
by blast
then show "problem_plan_bound_s PROB s ≤ 2 ^ card (prob_dom PROB) - 1"
unfolding problem_plan_bound_s_def
by blast
qed
lemma problem_plan_bound_s_works:
fixes PROB :: "'a problem" and as s
assumes "finite PROB" "(as ∈ valid_plans PROB)" "(s ∈ valid_states PROB)"
shows "(∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' ≤ problem_plan_bound_s PROB s)
)"
proof -
have "problem_plan_bound_s PROB s ≤ 2 ^ card (prob_dom PROB) - 1"
using assms(1, 3) bound_main_lemma_s
by blast
then have 1: "Inf (PLS s as) ≤ problem_plan_bound_s PROB s"
using assms problem_plan_bound_s_ge_min_pls[of PROB s as " 2 ^ card (prob_dom PROB) - 1"]
by blast
then obtain x where obtain_x: "x ∈ PLS s as ∧ x = Inf (PLS s as)"
using PLS_nempty_and_has_min
by blast
then have "∃as'. exec_plan s as = exec_plan s as' ∧ length as' = Inf (PLS s as) ∧ subseq as' as"
using PLS_works[where s = s and as = as and x = "Inf (PLS s as)"]
obtain_x
by fastforce
then show "(∃as'.
(exec_plan s as = exec_plan s as') ∧ (subseq as' as)
∧ (length as' ≤ problem_plan_bound_s PROB s)
)"
using 1
by metis
qed
lemma PLS_def_ITP2015:
fixes s as
shows "PLS s as = {length as' | as'. (exec_plan s as' = exec_plan s as) ∧ (subseq as' as)}"
using PLS_def
by blast
lemma expanded_problem_plan_bound_charles_thm:
fixes PROB :: "'a problem"
shows "
problem_plan_bound_charles PROB
= Sup (
{
Inf (PLS_charles (fst p) (snd p) PROB)
| p. (fst p ∈ valid_states PROB) ∧ (snd p ∈ valid_plans PROB)})
"
unfolding problem_plan_bound_charles_def MPLS_charles_def
by blast
lemma bound_main_lemma_charles_3:
fixes PROB :: "'a problem"
assumes "finite PROB"
shows "MPLS_charles PROB ≠ {}"
proof -
have 1: "[] ∈ valid_plans PROB"
using empty_plan_is_valid
by auto
then obtain s :: "'a state" where obtain_s: "s ∈ valid_states PROB"
using assms valid_states_nempty
by auto
then have "Inf (PLS_charles s [] PROB) ∈ MPLS_charles PROB"
unfolding MPLS_charles_def
using 1
by auto
then show "MPLS_charles PROB ≠ {}"
by blast
qed
lemma in_PLS_charles_leq_2_pow_n:
fixes PROB :: "'a problem" and s as
assumes "finite PROB" "s ∈ valid_states PROB" "as ∈ valid_plans PROB"
shows "(∃x.
(x ∈ PLS_charles s as PROB)
∧ (x ≤ 2 ^ card (prob_dom PROB) - 1))
"
proof -
obtain as' where 1:
"exec_plan s as = exec_plan s as'" "subseq as' as" "length as' ≤ 2 ^ card (prob_dom PROB) - 1"
using assms main_lemma
by blast
then have "as' ∈ valid_plans PROB"
using assms(3) sublist_valid_plan
by blast
then have "length as' ∈ PLS_charles s as PROB"
unfolding PLS_charles_def
using 1
by auto
then show ?thesis
using 1(3)
by fast
qed
lemma x_in_MPLS_charles_then:
fixes PROB s as
assumes "x ∈ MPLS_charles PROB"
shows "∃s as.
s ∈ valid_states PROB ∧ as ∈ valid_plans PROB ∧ x = Inf (PLS_charles s as PROB)
"
proof -
have "∃p ∈ {p. (fst p) ∈ valid_states PROB ∧ (snd p) ∈ valid_plans PROB}. x = Inf (PLS_charles (fst p) (snd p) PROB)"
using MPLS_charles_def assms
by fast
then obtain p where 1:
"p ∈ {p. (fst p) ∈ valid_states PROB ∧ (snd p) ∈ valid_plans PROB}"
"x = Inf (PLS_charles (fst p) (snd p) PROB)"
by blast
then have "fst p ∈ valid_states PROB" "snd p ∈ valid_plans PROB"
by blast+
then show ?thesis
using 1
by fast
qed
lemma in_MPLS_charles_leq_2_pow_n:
fixes PROB :: "'a problem" and x
assumes "finite PROB" "x ∈ MPLS_charles PROB"
shows "x ≤ 2 ^ card (prob_dom PROB) - 1"
proof -
obtain s as where 1:
"s ∈ valid_states PROB" "as ∈ valid_plans PROB" "x = Inf (PLS_charles s as PROB)"
using assms(2) x_in_MPLS_charles_then
by blast
then obtain x' where 2: "x' ∈ PLS_charles s as PROB""x' ≤ 2 ^ card (prob_dom PROB) - 1"
using assms(1) in_PLS_charles_leq_2_pow_n
by blast
then have "x ≤ x'"
using 1(3) mem_le_imp_MIN_le
by blast
then show ?thesis
using 1 2
by linarith
qed
lemma bound_main_lemma_charles:
fixes PROB :: "'a problem"
assumes "finite PROB"
shows "problem_plan_bound_charles PROB ≤ 2 ^ (card (prob_dom PROB)) - 1"
proof -
have 1: "∀x∈MPLS_charles PROB. x ≤ 2 ^ (card (prob_dom PROB)) - 1"
using assms in_MPLS_charles_leq_2_pow_n
by blast
then have "MPLS_charles PROB ≠ {}"
using assms bound_main_lemma_charles_3
by blast
then have "Sup (MPLS_charles PROB) ≤ 2 ^ (card (prob_dom PROB)) - 1"
using 1 bound_main_lemma_2
by meson
then show ?thesis
using problem_plan_bound_charles_def
by metis
qed
lemma bound_on_all_plans_bounds_PLS_charles:
fixes P and f
assumes "∀(PROB :: 'a problem) as s.
(P PROB) ∧ finite PROB ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as') ∧ (subseq as' as)∧ (length as' < f PROB))
"
shows "(∀PROB s as.
(P PROB) ∧ finite PROB ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB)
⟶ (∃x.
(x ∈ PLS_charles s as PROB)
∧ (x < f PROB)))
"
proof -
{
fix PROB :: "'a problem" and as and s :: "'a state"
assume P:
"P PROB" "finite PROB" "as ∈ valid_plans PROB" "s ∈ valid_states PROB"
"(∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB)
)"
then obtain as' where 1:
"(exec_plan s as = exec_plan s as')" "(subseq as' as)" "(length as' < f PROB)"
using P(5)
by blast
then have 2: "as' ∈ valid_plans PROB"
using P(3) sublist_valid_plan
by blast
let ?x = "length as'"
have "?x ∈ PLS_charles s as PROB"
unfolding PLS_charles_def
using 1 2
by auto
then have "∃x. x ∈ PLS_charles s as PROB ∧ x < f PROB"
using 1 2
by blast
}
then show ?thesis
using assms
by auto
qed
lemma bound_on_all_plans_bounds_MPLS_charles_i:
assumes "∀(PROB :: 'a problem) s as.
(P PROB) ∧ finite PROB ∧ (as ∈ valid_plans PROB) ∧ (s ∈ valid_states PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as') ∧ (subseq as' as) ∧ (length as' < f PROB))
"
shows "∀(PROB :: 'a problem) s as.
P PROB ∧ finite PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB
⟶ Inf {n. n ∈ PLS_charles s as PROB} < f PROB
"
proof -
{
fix PROB :: "'a problem" and s as
have "P PROB ∧ finite PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB
⟶ (∃x. x ∈ PLS_charles s as PROB ∧ x < f PROB)
"
using assms bound_on_all_plans_bounds_PLS_charles[of P f]
by blast
then have "
P PROB ∧ finite PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB
⟶ Inf {n. n ∈ PLS_charles s as PROB} < f PROB
"
using mem_lt_imp_MIN_lt CollectI
by metis
}
then show ?thesis
by blast
qed
lemma bound_on_all_plans_bounds_MPLS_charles:
fixes P f
assumes "(∀(PROB :: 'a problem) as s.
(P PROB) ∧ finite PROB ∧ (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB)
)
)"
shows "(∀PROB x.
(P PROB) ∧ finite PROB
⟶ (x ∈ MPLS_charles PROB)
⟶ (x < f PROB)
)"
proof -
have 1: "∀(PROB :: 'a problem) s as.
P PROB ∧ finite PROB ∧ as ∈ valid_plans PROB ∧ s ∈ valid_states PROB
⟶ Inf {n. n ∈ PLS_charles s as PROB} < f PROB
"
using assms bound_on_all_plans_bounds_MPLS_charles_i
by blast
moreover
{
fix PROB :: "'a problem" and x
assume P1: "(P PROB)" "finite PROB" "x ∈ MPLS_charles PROB"
then obtain s as where a:
"as ∈ valid_plans PROB" "s ∈ valid_states PROB" "x = Inf (PLS_charles s as PROB)"
using x_in_MPLS_charles_then
by blast
then have "Inf {n. n ∈ PLS_charles s as PROB} < f PROB"
using 1 P1
by blast
then have "x < f PROB"
using a
by simp
}
ultimately show ?thesis
by blast
qed
lemma bound_on_all_plans_bounds_problem_plan_bound_charles_i:
fixes PROB :: "'a problem"
assumes "finite PROB" "∀x ∈ MPLS_charles PROB. x < k"
shows "Sup (MPLS_charles PROB) ∈ MPLS_charles PROB"
proof -
have 1: "MPLS_charles PROB ≠ {}"
using assms(1) bound_main_lemma_charles_3
by auto
then have "finite (MPLS_charles PROB)"
using assms(2) finite_nat_set_iff_bounded
by blast
then show ?thesis
unfolding Sup_nat_def
using 1
by simp
qed
lemma bound_on_all_plans_bounds_problem_plan_bound_charles:
fixes P f
assumes "(∀(PROB :: 'a problem) as s.
(P PROB) ∧ finite PROB ∧ (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' < f PROB)))
"
shows "(∀PROB.
(P PROB) ∧ finite PROB ⟶ (problem_plan_bound_charles PROB < f PROB))
"
proof -
have 1: "∀PROB x. P PROB ∧ finite PROB ⟶ x ∈ MPLS_charles PROB ⟶ x < f PROB"
using assms bound_on_all_plans_bounds_MPLS_charles
by blast
moreover
{
fix PROB
assume P: "P PROB" "finite PROB"
moreover have 2: "∀x. x ∈ MPLS_charles PROB ⟶ x < f PROB"
using 1 P
by blast
moreover
{
fix x
assume P1: "x ∈ MPLS_charles PROB"
moreover have "x < f PROB"
using P(1, 2) P1 1
by presburger
moreover have "MPLS_charles PROB ≠ {}"
using P1
by blast
moreover have "Sup (MPLS_charles PROB) < f PROB"
using calculation(3) 2 bound_child_parent_not_eq_last_diff_paths[of "MPLS_charles PROB" "f PROB"]
by blast
ultimately have "(problem_plan_bound_charles PROB < f PROB)"
unfolding problem_plan_bound_charles_def
by blast
}
moreover have "Sup (MPLS_charles PROB) ∈ MPLS_charles PROB"
using P(2) 2 bound_on_all_plans_bounds_problem_plan_bound_charles_i
by blast
ultimately have "problem_plan_bound_charles PROB < f PROB"
unfolding problem_plan_bound_charles_def
by blast
}
ultimately show ?thesis
by blast
qed
subsection "The Relation between Diameter, Sublist Diameter and Recurrence Diameter Bounds."
text ‹ The goal of this subsection is to verify the relation between diameter, sublist diameter
and recurrence diameter bounds given by HOL4 Theorem 1, i.e.
@{term "𝖽(δ) ≤ 𝗅(δ) ∧ 𝗅(δ) ≤ 𝗋𝖽(δ)"}
where @{term "𝖽(δ)"}, @{term "𝗅(δ)"} and @{term "𝗋𝖽(δ)"} denote the diameter, sublist diameter and recurrence diameter bounds.
[Abdualaziz et al., p.20]
The relevant lemmas are `sublistD\_bounds\_D` and `RD\_bounds\_sublistD` which culminate in
theorem `sublistD\_bounds\_D\_and\_RD\_bounds\_sublistD`. ›
lemma sublistD_bounds_D:
fixes PROB :: "'a problem"
assumes "finite PROB"
shows "problem_plan_bound_charles PROB ≤ problem_plan_bound PROB"
proof -
{
fix PROB :: "'a problem" and s :: "'a state" and as
assume P: "finite PROB" "s ∈ valid_states PROB" "as ∈ valid_plans PROB"
then have "∃as'.
exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' ≤ problem_plan_bound PROB
"
using problem_plan_bound_works
by blast
then have "∃as'.
exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' < problem_plan_bound PROB + 1
"
by force
}
then have "problem_plan_bound_charles PROB < problem_plan_bound PROB + 1"
using assms bound_on_all_plans_bounds_problem_plan_bound_charles[where f = "λPROB. problem_plan_bound PROB + 1"
and P = "λ_. True"]
by blast
then show ?thesis
by simp
qed
lemma MAX_SET_ELIM':
fixes P Q
assumes "finite P" "P ≠ {}" "(∀x. (∀y. y ∈ P ⟶ y ≤ x) ∧ x ∈ P ⟶ R x)"
shows "R (Max P)"
using assms
by force
lemma MIN_SET_ELIM':
fixes P Q
assumes "finite P" "P ≠ {}" "∀x. (∀y. y ∈ P ⟶ x ≤ y) ∧ x ∈ P ⟶ Q x"
shows "Q (Min P)"
proof -
let ?x="Min P"
have "Min P ∈ P"
using Min_in[OF assms(1) assms(2)]
by simp
moreover {
fix y
assume P: "y ∈ P"
then have "?x ≤ y"
using Min.coboundedI[OF assms(1)]
by blast
then have "Q ?x" using P assms
by auto
}
ultimately show ?thesis
by blast
qed
lemma RD_bounds_sublistD_i_a:
fixes Pi :: "'a problem"
assumes "finite Pi"
shows "finite {length p - 1 |p. valid_path Pi p ∧ distinct p}"
proof -
{
let ?ss="{length p - 1 |p. valid_path Pi p ∧ distinct p}"
let ?ss'="{p. valid_path Pi p ∧ distinct p}"
have 1: "?ss = (λx. length x - 1) ` ?ss'"
by blast
{
let ?S="{p. distinct p ∧ set p ⊆ (valid_states Pi :: 'a state set)}"
{
from assms have "finite (valid_states Pi :: 'a state set)"
using FINITE_valid_states[of Pi]
by simp
then have "finite ?S"
using FINITE_ALL_DISTINCT_LISTS
by blast
}
moreover {
{
fix x
assume "x ∈ ?ss'"
then have "x ∈ ?S"
proof (induction x)
case (Cons a x)
then have a: "valid_path Pi (a # x)" "distinct (a # x)"
by blast+
moreover {
fix x'
assume P: "x' ∈ set (a # x)"
then have "x' ∈ valid_states Pi"
proof (cases "x")
case Nil
from a(1) Nil
have "a ∈ valid_states Pi"
by simp
moreover from P Nil
have "x' = a"
by force
ultimately show ?thesis
by simp
next
case (Cons a' list)
{
{
from Cons.prems have "valid_path Pi (a # x)"
by simp
then have "a ∈ valid_states Pi" "valid_path Pi (a' # list)"
using Cons
by fastforce+
}
note a = this
moreover {
from Cons.prems have "distinct (a # x)"
by blast
then have "distinct (a' # list)"
using Cons
by simp
}
ultimately
have "(a' # list) ∈ ?ss'"
by blast
then have "(a' # list) ∈ ?S"
using Cons Cons.IH
by argo
}
then show ?thesis
using P a(1) local.Cons set_ConsD
by fastforce
qed
}
ultimately show ?case
by blast
qed simp
}
then have "?ss' ⊆ ?S"
by blast
}
ultimately have "finite ?ss'"
using rev_finite_subset
by auto
}
note 2 = this
from 1 2 have "finite ?ss"
using finite_imageI
by auto
}
then show ?thesis
by blast
qed
lemma RD_bounds_sublistD_i_b:
fixes Pi :: "'a problem"
shows "{length p - 1 |p. valid_path Pi p ∧ distinct p} ≠ {}"
proof -
let ?Q="{length p - 1 |p. valid_path Pi p ∧ distinct p}"
let ?Q'="{p. valid_path Pi p ∧ distinct p}"
{
have "valid_path Pi []"
by simp
moreover have "distinct []"
by simp
ultimately have "[] ∈ ?Q'"
by simp
}
note 1 = this
have "?Q = (λp. length p - 1) ` ?Q'"
by blast
then have "length [] - 1 ∈ ?Q"
using 1
by (metis (mono_tags, lifting) image_iff list.size(3))
then show ?thesis
by blast
qed
lemma RD_bounds_sublistD_i_c:
fixes Pi :: "'a problem" and as :: "(('a, bool) fmap × ('a, bool) fmap) list" and x
and s :: "('a, bool) fmap"
assumes "s ∈ valid_states Pi" "as ∈ valid_plans Pi"
"(∀y. y ∈ {length p - 1 |p. valid_path Pi p ∧ distinct p} ⟶ y ≤ x)"
"x ∈ {length p - 1 |p. valid_path Pi p ∧ distinct p}"
shows "Min (PLS s as) ≤ Max {length p - 1 |p. valid_path Pi p ∧ distinct p}"
proof -
let ?P="(PLS s as)"
let ?Q="{length p - 1 |p. valid_path Pi p ∧ distinct p}"
from assms(4) obtain p where 1:
"x = length p - 1" "valid_path Pi p" "distinct p"
by blast
{
fix p'
assume "valid_path Pi p'" "distinct p'"
then obtain y where "y ∈ ?Q" "y = length p' - 1"
by blast
then have a: "length p' - 1 ≤ length p - 1"
using assms(3) 1(1)
by meson
}
note 2 = this
{
from finite_PLS PLS_NEMPTY
have "finite (PLS s as)" "PLS s as ≠ {}"
by blast+
moreover {
fix n
assume P: "(∀y. y ∈ PLS s as ⟶ n ≤ y)" "n ∈ PLS s as"
from P(2) obtain as' where i:
"n = length as'" "exec_plan s as' = exec_plan s as" "subseq as' as"
unfolding PLS_def
by blast
let ?p'="statelist' s as'"
{
have "length as' = length ?p' - 1"
by (simp add: LENGTH_statelist')
have "1 + (length p - 1) = length p - 1 + 1"
by presburger
{
from assms(2) i(3) sublist_valid_plan
have "as' ∈ valid_plans Pi"
by blast
then have "valid_path Pi ?p'"
using assms(1) valid_path_statelist'
by auto
}
moreover {
{
assume C: "¬distinct ?p'"
then obtain rs pfx drop' tail where C_1: "?p' = pfx @ [rs] @ drop' @ [rs] @ tail"
using not_distinct_decomp[OF C]
by fast
let ?pfxn="length pfx"
have C_2: "?p' ! ?pfxn = rs"
by (simp add: C_1)
from LENGTH_statelist'
have C_3: "length as' + 1 = length ?p'"
by metis
then have "?pfxn ≤ length as'"
using C_1
by fastforce
then have C_4: "exec_plan s (take ?pfxn as') = rs"
using C_2 statelist'_TAKE
by blast
let ?prsd = "length (pfx @ [rs] @ drop')"
let ?ap1 = "take ?pfxn as'"
from C_1
have C_5: "?p' ! ?prsd = rs"
by (metis append_Cons length_append nth_append_length nth_append_length_plus)
from C_1 C_3
have C_6: "?prsd ≤ length as'"
by simp
then have C_7: "exec_plan s (take ?prsd as') = rs"
using C_5 statelist'_TAKE
by auto
let ?ap2="take ?prsd as'"
let ?asfx="drop ?prsd as'"
have C_8: "as' = ?ap2 @ ?asfx"
by force
then have "exec_plan s as' = exec_plan (exec_plan s ?ap2) ?asfx"
using exec_plan_Append
by metis
then have C_9: "exec_plan s as' = exec_plan s (?ap1 @ ?asfx)"
using C_4 C_7 exec_plan_Append
by metis
from C_6
have C_10: "(length ?ap1 = ?pfxn) ∧ (length ?ap2 = ?prsd)"
by fastforce
then have C_11: "length (?ap1 @ ?asfx) < length (?ap2 @ ?asfx)"
by auto
{
from C_10
have "?pfxn + length ?asfx = length (?ap1 @ ?asfx)"
by simp
from C_9 i(2)
have C_12: "exec_plan s (?ap1 @ ?asfx) = exec_plan s as"
by argo
{
{
{
have "prefix ?ap1 ?ap2"
by (metis (no_types) length_append prefix_def take_add)
then have "subseq ?ap1 ?ap2"
using isPREFIX_sublist
by blast
}
moreover have "sublist ?asfx ?asfx"
using sublist_refl
by blast
ultimately have "subseq (?ap1 @ ?asfx) as'"
using C_8 subseq_append
by metis
}
moreover from i(3)
have "subseq as' as"
by simp
ultimately have "subseq (?ap1 @ ?asfx) as"
using sublist_trans
by blast
}
then have "length (?ap1 @ ?asfx) ∈ PLS s as"
unfolding PLS_def
using C_12
by blast
}
then have False
using P(1) i(1) C_10
by auto
}
hence "distinct ?p'"
by auto
}
ultimately have "length ?p' - 1 ≤ length p - 1"
using 2
by blast
}
note ii = this
{
from i(1) have "n + 1 = length ?p'"
using LENGTH_statelist'[symmetric]
by blast
also have "… ≤ 1 + (length p - 1)"
using ii
by linarith
finally have "n ≤ length p - 1"
by fastforce
}
then have "n ≤ length p - 1"
by blast
}
ultimately have "Min ?P ≤ length p - 1"
using MIN_SET_ELIM'[where P="?P" and Q="λx. x ≤ length p - 1"]
by blast
}
note 3 = this
{
have "length p - 1 ≤ Max {length p - 1 |p. valid_path Pi p ∧ distinct p}"
using assms(3, 4) 1(1)
by (smt Max.coboundedI bdd_aboveI bdd_above_nat)
moreover
have "Min (PLS s as) ≤ length p - 1"
using 3
by blast
ultimately
have "Min (PLS s as) ≤ Max {length p - 1 |p. valid_path Pi p ∧ distinct p}"
by linarith
}
then show ?thesis
by blast
qed
lemma RD_bounds_sublistD_i:
fixes Pi :: "'a problem" and x
assumes "finite Pi" "(∀y. y ∈ MPLS Pi ⟶ y ≤ x)" "x ∈ MPLS Pi"
shows "x ≤ Max {length p - 1 |p. valid_path Pi p ∧ distinct p}"
proof -
{
let ?P="MPLS Pi"
let ?Q="{length p - 1 |p. valid_path Pi p ∧ distinct p}"
from assms(3)
obtain s as where 1:
"s ∈ valid_states Pi" "as ∈ valid_plans Pi" "x = Inf (PLS s as)"
unfolding MPLS_def
by fast
have "x ≤ Max ?Q" proof -
text ‹ Show that `x` is not only the infimum but also the minimum of `PLS s as`.›
{
have "finite (PLS s as)"
using finite_PLS
by auto
moreover
have "PLS s as ≠ {}"
using PLS_NEMPTY
by auto
ultimately
have a: "Inf (PLS s as) = Min (PLS s as)"
using cInf_eq_Min[of "PLS s as"]
by blast
from 1(3) a have "x = Min (PLS s as)"
by blast
}
note a = this
{
let ?limit="Min (PLS s as)"
from assms(1)
have a: "finite ?Q"
using RD_bounds_sublistD_i_a
by blast
have b: "?Q ≠ {}"
using RD_bounds_sublistD_i_b
by fast
from 1(1, 2)
have c: "∀x. (∀y. y ∈ ?Q ⟶ y ≤ x) ∧ x ∈ ?Q ⟶ ?limit ≤ Max ?Q"
using RD_bounds_sublistD_i_c
by blast
have "?limit ≤ Max ?Q"
using MAX_SET_ELIM'[where P="?Q" and R="λx. ?limit ≤ Max ?Q", OF a b c]
by blast
}
note b = this
from a b show "x ≤ Max ?Q"
by blast
qed
}
then show ?thesis
using assms
unfolding MPLS_def
by blast
qed
lemma RD_bounds_sublistD:
fixes Pi :: "'a problem"
assumes "finite Pi"
shows "problem_plan_bound Pi ≤ RD Pi"
proof -
let ?P="MPLS Pi"
let ?Q="{length p - 1 |p. valid_path Pi p ∧ distinct p}"
{
from assms
have 1: "finite ?P"
using FINITE_MPLS
by blast
from assms
have 2: "?P ≠ {}"
using MPLS_nempty
by blast
from assms
have 3: "∀x. (∀y. y ∈ ?P ⟶ y ≤ x) ∧ x ∈ ?P ⟶ x ≤ Max ?Q"
using RD_bounds_sublistD_i
by blast
have "Max ?P ≤ Max ?Q"
using MAX_SET_ELIM'[OF 1 2 3]
by blast
}
then show ?thesis
unfolding problem_plan_bound_def RD_def Sup_nat_def
using RD_bounds_sublistD_i_b by auto
qed
theorem sublistD_bounds_D_and_RD_bounds_sublistD:
fixes PROB :: "'a problem"
assumes "finite PROB"
shows "
problem_plan_bound_charles PROB ≤ problem_plan_bound PROB
∧ problem_plan_bound PROB ≤ RD PROB
"
using assms sublistD_bounds_D RD_bounds_sublistD
by auto
lemma empty_problem_bound:
fixes PROB :: "'a problem"
assumes "(prob_dom PROB = {})"
shows "(problem_plan_bound PROB = 0)"
proof -
{
fix PROB' and as :: "(('a, 'b) fmap × ('a, 'b) fmap) list" and s :: "('a, 'b) fmap"
assume
"finite PROB" "prob_dom PROB' = {}" "s ∈ valid_states PROB'" "as ∈ valid_plans PROB'"
then have "exec_plan s [] = exec_plan s as"
using empty_prob_dom_imp_empty_plan_always_good
by blast
then have "(∃as'. exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' < 1)"
by force
}
then show ?thesis
using bound_on_all_plans_bounds_problem_plan_bound_[where P="λP. prob_dom P = {}" and f="λP. 1", of PROB]
using assms empty_prob_dom_finite
by blast
qed
lemma problem_plan_bound_works':
fixes PROB :: "'a problem" and as s
assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(∃as'.
(exec_plan s as' = exec_plan s as)
∧ (subseq as' as)
∧ (length as' ≤ problem_plan_bound PROB)
∧ (sat_precond_as s as')
)"
proof -
obtain as' where 1:
"exec_plan s as = exec_plan s as'" "subseq as' as" "length as' ≤ problem_plan_bound PROB"
using assms problem_plan_bound_works
by blast
moreover have "rem_condless_act s [] as' ∈ valid_plans PROB"
using assms(3) 1(2) rem_condless_valid_10 sublist_valid_plan
by blast
moreover have "subseq (rem_condless_act s [] as') as'"
using rem_condless_valid_8
by blast
moreover have "length (rem_condless_act s [] as') ≤ length as'"
using rem_condless_valid_3
by blast
moreover have "sat_precond_as s (rem_condless_act s [] as')"
using rem_condless_valid_2
by blast
moreover have "exec_plan s as' = exec_plan s (rem_condless_act s [] as')"
using rem_condless_valid_1
by blast
ultimately show ?thesis
by fastforce
qed
lemma problem_plan_bound_UBound:
assumes "(∀as s.
(s ∈ valid_states PROB)
∧ (as ∈ valid_plans PROB)
⟶ (∃as'.
(exec_plan s as = exec_plan s as')
∧ subseq as' as
∧ (length as' < f PROB)
)
)" "finite PROB"
shows "(problem_plan_bound PROB < f PROB)"
proof -
let ?P = "λPr. PROB = Pr"
have "?P PROB" by simp
then show ?thesis
using assms bound_on_all_plans_bounds_problem_plan_bound_[where P = ?P]
by force
qed
subsection "Traversal Diameter"
definition traversed_states where
"traversed_states s as ≡ set (state_list s as)"
lemma finite_traversed_states: "finite (traversed_states s as)"
unfolding traversed_states_def
by simp
lemma traversed_states_nempty: "traversed_states s as ≠ {}"
unfolding traversed_states_def
by (induction as) auto
lemma traversed_states_geq_1:
fixes s
shows "1 ≤ card (traversed_states s as)"
proof -
have "card (traversed_states s as) ≠ 0"
using traversed_states_nempty finite_traversed_states card_0_eq
by blast
then show "1 ≤ card (traversed_states s as)"
by linarith
qed
lemma init_is_traversed: "s ∈ traversed_states s as"
unfolding traversed_states_def
by (induction as) auto
definition td where
"td PROB ≡ Sup {
(card (traversed_states (fst p) (snd p))) - 1
| p. (fst p ∈ valid_states PROB) ∧ (snd p ∈ valid_plans PROB)}
"
lemma traversed_states_rem_condless_act: "⋀s.
traversed_states s (rem_condless_act s [] as) = traversed_states s as
"
apply(induction as)
apply(auto simp add: traversed_states_def rem_condless_act_cons)
subgoal by (simp add: state_succ_pair)
subgoal using init_is_traversed traversed_states_def by blast
subgoal by (simp add: state_succ_pair)
done
lemma td_UBound_i:
fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set"
assumes "finite PROB"
shows "
{
(card (traversed_states (fst p) (snd p))) - 1
| p. (fst p ∈ valid_states PROB) ∧ (snd p ∈ valid_plans PROB)}
≠ {}
"
proof -
let ?S="{p. (fst p ∈ valid_states PROB) ∧ (snd p ∈ valid_plans PROB)}"
obtain s :: "'a state" where "s ∈ valid_states PROB"
using assms valid_states_nempty
by blast
moreover have "[] ∈ valid_plans PROB"
using empty_plan_is_valid
by auto
ultimately have "?S ≠ {}"
using assms valid_states_nempty
by auto
then show ?thesis
by blast
qed
lemma td_UBound:
fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set"
assumes "finite PROB" "(∀s as.
(sat_precond_as s as) ∧ (s ∈ valid_states PROB) ∧ (as ∈ valid_plans PROB)
⟶ (card (traversed_states s as) ≤ k)
)"
shows "(td PROB ≤ k - 1)"
proof -
let ?S="{
(card (traversed_states (fst p) (snd p))) - 1
| p. (fst p ∈ valid_states PROB) ∧ (snd p ∈ valid_plans PROB)}
"
{
fix x
assume "x ∈ ?S"
then obtain p where 1:
"x = card (traversed_states (fst p) (snd p)) - 1" "fst p ∈ valid_states PROB"
"snd p ∈ valid_plans PROB"
by blast
let ?s="fst p"
let ?as="snd p"
{
let ?as'="(rem_condless_act ?s [] ?as)"
have 2: "traversed_states ?s ?as = traversed_states ?s ?as'"
using traversed_states_rem_condless_act
by blast
moreover have "sat_precond_as ?s ?as'"
using rem_condless_valid_2
by blast
moreover have "?as' ∈ valid_plans PROB"
using 1(3) rem_condless_valid_10
by blast
ultimately have "card (traversed_states ?s ?as') ≤ k"
using assms(2) 1(2)
by blast
then have "card (traversed_states ?s ?as) ≤ k"
using 2
by argo
}
then have "x ≤ k - 1"
using 1
by linarith
}
moreover have "?S ≠ {}"
using assms td_UBound_i
by fast
ultimately show ?thesis
unfolding td_def
using td_UBound_i bound_main_lemma_2[of ?S "k - 1"]
by presburger
qed
end