# Theory FactoredSystem

```theory FactoredSystem
imports Main "HOL-Library.Finite_Map" "HOL-Library.Sublist" FSSublist
FactoredSystemLib ListUtils HoArithUtils FmapUtils
begin

section "Factored System"

― ‹NOTE hide the '++' operator from 'Map' to prevent warnings.›

subsection "Semantics of Plan Execution"

text ‹ This section aims at characterizing the semantics of executing plans---i.e. sequences
of actions---on a given initial state.

The semantics of action execution were previously introduced
via the notion of succeding state (`state\_succ`). Plan execution (`exec\_plan`) extends this notion
to sequences of actions by calculating the succeding state from the given state and action pair and
then recursively executing the remaining actions on the succeding state. [Abdulaziz et al., HOL4
Definition 3, p.9] ›

lemma state_succ_pair: "state_succ s (p, e) = (if (p ⊆⇩f s) then (e ++ s) else s)"

― ‹NOTE shortened to 'exec\_plan'›
― ‹NOTE using 'fun' because of multiple definining equations.›
― ‹NOTE first argument was curried.›
fun exec_plan where
"exec_plan s [] = s"
| "exec_plan s (a # as) = exec_plan (state_succ s a) as"

lemma exec_plan_Append:
fixes as_a as_b s
shows "exec_plan s (as_a @ as_b) = exec_plan (exec_plan s as_a) as_b"
by (induction as_a arbitrary: s as_b) auto

text ‹ Plan execution effectively eliminates cycles: i.e., if a given plan `as` may be partitioned
into plans `as1`, `as2` and `as3`, s.t. the sequential execution of `as1` and `as2` yields the same
state, `as2` may be skipped during plan execution. ›

lemma cycle_removal_lemma:
fixes as1 as2 as3
assumes "(exec_plan s (as1 @ as2) = exec_plan s as1)"
shows "(exec_plan s (as1 @ as2 @ as3) = exec_plan s (as1 @ as3))"
using assms exec_plan_Append
by metis

subsubsection "Characterization of the Set of Possible States"

text ‹ To show the construction principle of the set of possible states---in lemma
`construction\_of\_all\_possible\_states\_lemma`---the following ancillary proves of finite map
properties are required.

Most importantly, in lemma `fmupd\_fmrestrict\_subset` we show how finite mappings `s` with domain
@{term "{v} ∪ X"} and `s v = (Some x)` are constructed from their restrictions to `X` via update, i.e.

s = fmupd v x (fmrestrict\_set X s)

This is used in lemma `construction\_of\_all\_possible\_states\_lemma` to show that the set of possible
states for variables @{term "{v} ∪ X"} is constructed inductively from the set of all possible states for
variables `X` via update on point @{term "v ∉ X"}.
›

lemma empty_domain_fmap_set: "{s. fmdom' s = {}} = {fmempty}"
proof -
let ?A = "{s. fmdom' s = {}}"
let ?B = "{fmempty}"
fix s
show ?thesis proof(rule ccontr)
assume C: "?A ≠ ?B"
then show False proof -
{
assume C1: "?A ⊂ ?B"
have "?A = {}" using C1 by force
then have False using fmdom'_empty by blast
}
moreover
{
assume C2: "¬(?A ⊂ ?B)"
then have "fmdom' fmempty = {}"
by auto
moreover have "fmempty ∈ ?A"
by auto
moreover have "?A ≠ {}"
using calculation(2) by blast
moreover have "∀a∈?A.a∉?B"
by (metis (mono_tags, lifting)
C Collect_cong calculation(1) fmrestrict_set_dom fmrestrict_set_null singleton_conv)
moreover have "fmempty ∈ ?B" by auto
moreover have "∃a∈?A.a∈?B"
by simp
moreover have "¬(∀a∈?A.a∉?B)"
by simp
ultimately have False
by blast
}
ultimately show False
by fastforce
qed
qed
qed

lemma possible_states_set_ii_a:
fixes s x v
assumes "(v ∈ fmdom' s)"
shows "(fmdom' ((λs. fmupd v x s) s) = fmdom' s)"
using assms insert_absorb
by auto

lemma possible_states_set_ii_b:
fixes s x v
assumes "(v ∉ fmdom' s)"
shows "(fmdom' ((λs. fmupd v x s) s) = fmdom' s ∪ {v})"
by auto

lemma fmap_neq:
fixes s :: "('a, bool) fmap" and s' :: "('a, bool) fmap"
assumes "(fmdom' s = fmdom' s')"
shows "((s ≠ s') ⟷ (∃v∈(fmdom' s). fmlookup s v ≠ fmlookup s' v))"
using assms fmap_ext fmdom'_notD
by metis

lemma fmdom'_fmsubset_restrict_set:
fixes X1 X2 and s :: "('a, bool) fmap"
assumes "X1 ⊆ X2" "fmdom' s = X2"
shows "fmdom' (fmrestrict_set X1 s) = X1"
using assms
by (metis (no_types, lifting)
antisym_conv fmdom'_notD fmdom'_notI fmlookup_restrict_set rev_subsetD subsetI)

lemma fmsubset_restrict_set:
fixes X1 X2 and s :: "'a state"
assumes "X1 ⊆ X2" "s ∈ {s. fmdom' s = X2}"
shows "fmrestrict_set X1 s ∈ {s. fmdom' s = X1}"
using assms fmdom'_fmsubset_restrict_set
by blast

lemma fmupd_fmsubset_restrict_set:
fixes X v x and s :: "'a state"
assumes "s ∈ {s. fmdom' s = insert v X}" "fmlookup s v = Some x"
shows "s = fmupd v x (fmrestrict_set X s)"
proof -
― ‹Show that domains of 's' and 'fmupd v x (fmrestrict\_set X s)' are identical.›
have 1: "fmdom' s = insert v X"
using assms(1)
by simp
{
have "X ⊆ insert v X"
by auto
then have "fmdom' (fmrestrict_set X s) = X"
using 1 fmdom'_fmsubset_restrict_set
by metis
then have "fmdom' (fmupd v x (fmrestrict_set X s)) = insert v X"
using assms(1) fmdom'_fmupd
by auto
}
note 2 = this
moreover
{
fix w
― ‹Show case for undefined variables (where lookup yields 'None').›
{
assume "w ∉ insert v X"
then have "w ∉ fmdom' s" "w ∉ fmdom' (fmupd v x (fmrestrict_set X s))"
using 1 2
by argo+
then have "fmlookup s w = fmlookup (fmupd v x (fmrestrict_set X s)) w"
using fmdom'_notD
by metis
}
― ‹Show case for defined variables (where lookup yields 'Some y').›
moreover {
assume "w ∈ insert v X"
then have "w ∈ fmdom' s" "w ∈ fmdom' (fmupd v x (fmrestrict_set X s))"
using 1 2
by argo+
then have "fmlookup s w = fmlookup (fmupd v x (fmrestrict_set X s)) w"
by (cases "w = v")
}
ultimately have "fmlookup s w = fmlookup (fmupd v x (fmrestrict_set X s)) w"
by blast
}
then show ?thesis
using fmap_ext
by blast
qed

lemma construction_of_all_possible_states_lemma:
fixes v X
assumes "(v ∉ X)"
shows "({s. fmdom' s = insert v X}
= ((λs. fmupd v True s) ` {s. fmdom' s = X})
∪ ((λs. fmupd v False s) ` {s. fmdom' s = X})
)"
proof -
fix v X
let ?A = "{s :: 'a state. fmdom' s = insert v X}"
let ?B = "
((λs. fmupd v True s) ` {s :: 'a state. fmdom' s = X})
∪ ((λs. fmupd v False s) ` {s :: 'a state. fmdom' s = X})
"
text ‹Show the goal by mutual inclusion. The inclusion @{term "?B ⊆ ?A"} is trivial and can be solved by
automation. For the complimentary proof @{term "?A ⊆ ?B"} however we need to do more work.
In our case we choose a proof by contradiction and show that an @{term "s ∈ ?A"} which is not also in
'?B' cannot exist.›
{
have "?A ⊆ ?B" proof(rule ccontr)
assume C: "¬(?A ⊆ ?B)"
moreover have "∃s∈?A. s∉?B"
using C
by auto
moreover obtain s where obtain_s: "s∈?A ∧ s∉?B"
using calculation
by auto
moreover have "s∉?B"
using obtain_s
by auto
moreover have "fmdom' s = X ∪ {v}"
using obtain_s
by auto
moreover have "∀s'∈?B. fmdom' s' = X ∪ {v}"
by auto
moreover have
"(s ∉ ((λs. fmupd v True s) ` {s. fmdom' s = X}))"
"(s ∉ ((λs. fmupd v False s) ` {s. fmdom' s = X}))"
using obtain_s
by blast+
text ‹ Show that every state @{term "s ∈ ?A"} has been constructed from another state with domain
'X'. ›
moreover
{
fix s :: "'a state"
assume 1: "s ∈ {s :: 'a state. fmdom' s = insert v X}"
then have "fmrestrict_set X s ∈ {s :: 'a state. fmdom' s = X}"
using subset_insertI fmsubset_restrict_set
by metis
moreover
{
assume "fmlookup s v = Some True"
then have "s = fmupd v True (fmrestrict_set X s)"
using 1 fmupd_fmsubset_restrict_set
by metis
}
moreover {
assume "fmlookup s v = Some False"
then have "s = fmupd v False (fmrestrict_set X s)"
using 1 fmupd_fmsubset_restrict_set
by fastforce
}
moreover have "fmlookup s v ≠ None"
using 1 fmdom'_notI
by fastforce
ultimately have "
(s ∈ ((λs. fmupd v True s) ` {s. fmdom' s = X}))
∨ (s ∈ ((λs. fmupd v False s) ` {s. fmdom' s = X}))
"
by force
}
ultimately show False
by meson
qed
}
moreover have "?B ⊆ ?A"
by force
ultimately show "?A = ?B" by blast
qed

text ‹ Another important property of the state set is cardinality, i.e. the number of distinct
states which can be modelled using a given finite variable set.

As lemma `card\_of\_set\_of\_all\_possible\_states` shows, for a finite variable set `X`, the number of
possible states is `2 \^ card X`, i.e. the number of assigning two discrete values to `card X` slots
as known from combinatorics.

Again, some additional properties of finite maps had to be proven. Pivotally, in lemma
`updates\_disjoint`, it is shown that the image of updating a set of states with domain `X` on a
point @{term "x ∉ X"} with either `True` or `False` yields two distinct sets of states with domain
@{term "{x} ∪ X"}. ›

― ‹NOTE goal has to stay implication otherwise induction rule won't watch.›
lemma FINITE_states:
fixes X :: "'a set"
shows "finite X ⟹ finite {(s :: 'a state). fmdom' s = X}"
proof (induction  rule: finite.induct)
case emptyI
then have "{s. fmdom' s  = {}} = {fmempty}"
then show ?case
by (simp add: ‹{s. fmdom' s = {}} = {fmempty}›)
next
case (insertI A a)
assume P1: "finite A"
and P2: "finite {s. fmdom' s = A}"
then show ?case
proof (cases "a ∈ A")
case True
then show ?thesis
using insertI.IH insert_Diff
by fastforce
next
case False
then show ?thesis
proof -
have "finite (
((λs. fmupd a True s) ` {s. fmdom' s = A})
∪ ((λs. fmupd a False s) ` {s. fmdom' s = A}))"
using False construction_of_all_possible_states_lemma insertI.IH
by blast
then show ?thesis
using False construction_of_all_possible_states_lemma
by fastforce
qed
qed
qed

lemma bool_update_effect:
fixes s X x v b
assumes "finite X" "s ∈ {s :: 'a state. fmdom' s = X}" "x ∈ X" "x ≠ v"
shows "fmlookup ((λs :: 'a state. fmupd v b s) s) x = fmlookup s x"
using assms fmupd_lookup
by auto

lemma bool_update_inj:
fixes X :: "'a set" and v b
assumes "finite X" "v ∉ X"
shows "inj_on (λs. fmupd v b s) {s :: 'a state. fmdom' s = X}"
proof -
let ?f = "λs :: 'a state. fmupd v b s"
{
fix s1 s2 :: "'a state"
assume "s1 ∈ {s :: 'a state. fmdom' s = X}" "s2 ∈ {s :: 'a state. fmdom' s = X}"
"?f s1 = ?f s2"
moreover
{
have
"∀x∈X. x ≠ v ⟶ fmlookup (?f s1) x = fmlookup s1 x"
"∀x∈X. x ≠ v ⟶ fmlookup (?f s2) x = fmlookup s2 x"
by simp+
then have
"∀x∈X. x ≠ v ⟶ fmlookup s1 x = fmlookup s2 x"
using calculation(3)
by auto
}
moreover have "fmlookup s1 v = fmlookup s2 v"
using calculation ‹v ∉ X›
by force
ultimately have "s1 = s2"
using fmap_neq
by fastforce
}
then show "inj_on (λs. fmupd v b s) {s :: 'a state. fmdom' s = X}"
using inj_onI
by blast
qed

lemma card_update:
fixes X v b
assumes "finite (X :: 'a set)" "v ∉ X"
shows "
card ((λs. fmupd v b s) ` {s :: 'a state. fmdom' s = X})
= card {s :: 'a state. fmdom' s = X}
"
proof -
have "inj_on (λs. fmupd v b s) {s :: 'a state. fmdom' s = X}"
using assms bool_update_inj
by fast
then show
"card ((λs. fmupd v b s) ` {s :: 'a state. fmdom' s = X}) = card {s :: 'a state. fmdom' s = X}"
using card_image by blast
qed

fixes X x
assumes "finite X" "x ∉ X"
shows "
((λs. fmupd x True s) ` {s. fmdom' s = X})
∩ ((λs. fmupd x False s) ` {s. fmdom' s = X}) = {}
"
proof -
let ?A = "((λs. fmupd x True s) ` {s. fmdom' s = X})"
let ?B = "((λs. fmupd x False s) ` {s. fmdom' s = X})"
{
assume C: "¬(∀a∈?A. ∀b∈?B. a ≠ b)"
then have
"∀a∈?A. ∀b∈?B. fmlookup a x ≠ fmlookup b x"
by simp
then have "∀a∈?A. ∀b∈?B. a ≠ b"
by blast
then have False
using C
by blast
}
then show "?A ∩ ?B = {}"
using disjoint_iff_not_equal
by blast
qed

lemma card_of_set_of_all_possible_states:
fixes X :: "'a set"
assumes "finite X"
shows "card {(s :: 'a state). fmdom' s = X} = 2 ^ (card X)"
using assms
proof (induction X)
case empty
then have 1: "{s :: 'a state. fmdom' s = {}} = {fmempty}"
using empty_domain_fmap_set
by simp
then have "card {fmempty} = 1"
using is_singleton_altdef
by blast
then have "2^(card {}) = 1"
by auto
then show ?case
using 1
by auto
next
case (insert x F)
then show ?case
― ‹TODO refactor and simplify proof further.›
proof (cases "x ∈ F")
case True
then show ?thesis
using insert.hyps(2)
by blast
next
case False
then have "
{s :: 'a state. fmdom' s = insert x F}
= (λs. fmupd x True s) ` {s. fmdom' s = F} ∪ (λs. fmupd x False s) ` {s. fmdom' s = F}
"
using False construction_of_all_possible_states_lemma
by metis
then have 2: "
card ({s :: 'a state. fmdom' s = insert x F})
= card ((λs. fmupd x True s) ` {s. fmdom' s = F} ∪ (λs. fmupd x False s) ` {s. fmdom' s = F})
"
by argo
then have 3: "2^(card (insert x F)) = 2 * 2^(card F)"
using False insert.hyps(1)
by simp
then have
"card ((λs. fmupd x True s) ` {s. fmdom' s = F}) = 2^(card F)"
"card ((λs. fmupd x False s) ` {s. fmdom' s = F}) = 2^(card F)"
using False card_update insert.IH insert.hyps(1)
by metis+
moreover have "
((λs. fmupd x True s) ` {s. fmdom' s = F})
∩ ((λs. fmupd x False s) ` {s. fmdom' s = F})
= {}
"
by metis
moreover have "card (
((λs. fmupd x True s) ` {s. fmdom' s = F})
∪ ((λs. fmupd x False s) ` {s. fmdom' s = F})
)
= card (((λs. fmupd x True s) ` {s. fmdom' s = F}))
+ card ((λs. fmupd x False s) ` {s. fmdom' s = F})
"
using calculation card_Un_disjoint card.infinite
power_eq_0_iff rel_simps(76)
by metis
then have "card (
((λs. fmupd x True s) ` {s. fmdom' s = F})
∪ ((λs. fmupd x False s) ` {s. fmdom' s = F})
)
= 2 * (2^(card F))"
using calculation(1, 2)
by presburger
then have "card (
((λs. fmupd x True s) ` {s. fmdom' s = F})
∪ ((λs. fmupd x False s) ` {s. fmdom' s = F})
)
= 2^(card (insert x F))"
using insert.IH 3
by metis
then show ?thesis
using "2"
by argo
qed
qed

subsubsection "State Lists and State Sets"

― ‹NOTE using fun because of two defining equations.›
― ‹NOTE paired argument replaced by currying.›
fun state_list where
"state_list s [] = [s]"
| "state_list s (a # as) = s # state_list (state_succ s a) as"

lemma empty_state_list_lemma:
fixes as s
shows "¬([] = state_list s as)"
proof (induction as)
qed auto

lemma state_list_length_non_zero:
fixes as s
shows "¬(0 = length (state_list s as))"
proof (induction as)
qed auto

lemma state_list_length_lemma:
fixes as s
shows "length as = length (state_list s as) - 1"
proof (induction as arbitrary: s)
next case (Cons a as)
have "length (state_list s (Cons a as)) - 1 =  length (state_list (state_succ s a) as)"
by auto
― ‹TODO unwrap metis proof.›
then show "length (Cons a as) = length (state_list s (Cons a as)) - 1"
by (metis Cons.IH Suc_diff_1 empty_state_list_lemma length_Cons length_greater_0_conv)
qed simp

lemma state_list_length_lemma_2:
fixes as s
shows "(length (state_list s as)) = (length as + 1)"
proof (induction as arbitrary: s)
qed auto

― ‹NOTE using fun because of multiple defining equations.›
― ‹NOTE name shortened to 'state\_def'›
fun state_set where
"state_set [] = {}"
| "state_set (s # ss) = insert [s] (Cons s ` (state_set ss))"

lemma state_set_thm:
fixes s1
shows "s1 ∈ state_set s2 ⟷ prefix s1 s2 ∧ s1 ≠ []"
proof -
― ‹NOTE Show equivalence by proving both directions. Left-to-right is trivial. Right-to-Left
primarily involves exploiting the prefix premise, induction hypothesis  and  `state\_set`
definition.›
have "s1 ∈ state_set s2 ⟹ prefix s1 s2 ∧ s1 ≠ []"
by (induction s2 arbitrary: s1) auto
moreover {
assume P: "prefix s1 s2" "s1 ≠ []"
then have "s1 ∈ state_set s2"
proof (induction s2 arbitrary: s1)
case (Cons a s2)
obtain s1' where 1: "s1 = a # s1'" "prefix s1' s2"
using Cons.prems(1, 2) prefix_Cons
by metis
then show ?case proof (cases "s1' = []")
case True
then show ?thesis
using 1
by force
next
case False
then have "s1' ∈ state_set s2"
using 1 False Cons.IH
by blast
then show ?thesis
using 1
by fastforce
qed
qed simp
}
ultimately show "s1 ∈ state_set s2 ⟷ prefix s1 s2 ∧ s1 ≠ []"
by blast
qed

lemma state_set_finite:
fixes X
shows "finite (state_set X)"
by (induction X) auto

lemma LENGTH_state_set:
fixes X e
assumes "e ∈ state_set X"
shows "length e ≤ length X"
using assms
by (induction X arbitrary: e) auto

lemma lemma_temp:
fixes x s as h
assumes "x ∈ state_set (state_list s as)"
shows "length (h # state_list s as) > length x"
using assms LENGTH_state_set le_imp_less_Suc
by force

lemma NIL_NOTIN_stateset:
fixes X
shows "[] ∉ state_set X"
by (induction X) auto

lemma state_set_card_i:
fixes X a
shows "[a] ∉ (Cons a ` state_set X)"
by (induction X) auto

lemma state_set_card_ii:
fixes X a
shows "card (Cons a ` state_set X) = card (state_set X)"
proof -
have "inj_on (Cons a) (state_set X)"
by simp
then show ?thesis
using card_image
by blast
qed

lemma state_set_card_iii:
fixes X a
shows "card (state_set (a # X)) = 1 + card (state_set X)"
proof -
have "card (state_set (a # X)) = card (insert [a] (Cons a ` state_set X))"
by auto
― ‹TODO unwrap this metis step.›
also have "… = 1 + card (Cons a ` state_set X)"
using state_set_card_i
by (metis Suc_eq_plus1_left card_insert_disjoint finite_imageI state_set_finite)
also have"… = 1 + card (state_set X)"
using state_set_card_ii
by metis
finally show "card (state_set (a # X)) = 1 + card (state_set X)"
by blast
qed

lemma state_set_card:
fixes X
shows "card (state_set X) = length X"
proof (induction X)
case (Cons a X)
then have "card (state_set (a # X)) = 1 + card (state_set X)"
using state_set_card_iii
by fast
then show ?case
using Cons
by fastforce
qed auto

subsubsection "Properties of Domain Changes During Plan Execution"

lemma FDOM_state_succ:
assumes "fmdom' (snd a) ⊆ fmdom' s"
shows "(fmdom' (state_succ s a) = fmdom' s)"
using assms
by force

lemma FDOM_state_succ_subset:
"fmdom' (state_succ s a) ⊆ (fmdom' s ∪ fmdom' (snd a))"
by simp

― ‹NOTE definition `qispl\_then` removed (was not being used).›

lemma FDOM_eff_subset_FDOM_valid_states:
fixes p e s
assumes "(p, e) ∈ PROB" "(s ∈ valid_states PROB)"
shows "(fmdom' e ⊆ fmdom' s)"
proof -
{
have "fmdom' e ⊆ action_dom p e"
unfolding action_dom_def
by blast
also have "… ⊆ prob_dom PROB"
unfolding action_dom_def prob_dom_def
using assms(1)
by blast
finally have "fmdom' e ⊆ fmdom' s"
using assms
by (auto simp: valid_states_def)
}
then show "fmdom' e ⊆ fmdom' s"
by simp
qed

lemma FDOM_eff_subset_FDOM_valid_states_pair:
fixes a s
assumes "a ∈ PROB" "s ∈ valid_states PROB"
shows "fmdom' (snd a) ⊆ fmdom' s"
proof -
{
have "fmdom' (snd a) ⊆ (λ(s1, s2). action_dom s1 s2) a"
unfolding action_dom_def
using case_prod_beta
by fastforce
also have "… ⊆ prob_dom PROB"
using assms(1) prob_dom_def Sup_upper
by fast
finally have "fmdom' (snd a) ⊆ fmdom' s"
using assms(2) valid_states_def
by fast
}
then show ?thesis
by simp
qed

lemma FDOM_pre_subset_FDOM_valid_states:
fixes p e s
assumes "(p, e) ∈ PROB" "s ∈ valid_states PROB"
shows "fmdom' p ⊆ fmdom' s"
proof -
{
have "fmdom' p ⊆ (λ(s1, s2). action_dom s1 s2) (p, e)"
using action_dom_def
by fast
also have "… ⊆ prob_dom PROB"
using assms(1)
by (simp add: Sup_upper pair_imageI prob_dom_def)
finally have "fmdom' p ⊆ fmdom' s"
using assms(2) valid_states_def
by fast
}
then show ?thesis
by simp
qed

lemma FDOM_pre_subset_FDOM_valid_states_pair:
fixes a s
assumes "a ∈ PROB" "s ∈ valid_states PROB"
shows "fmdom' (fst a) ⊆ fmdom' s"
proof -
{
have "fmdom' (fst a) ⊆ (λ(s1, s2). action_dom s1 s2) a"
using action_dom_def
by force
also have "… ⊆ prob_dom PROB"
using assms(1)
by (simp add: Sup_upper pair_imageI prob_dom_def)
finally have "fmdom' (fst a) ⊆ fmdom' s"
using assms(2) valid_states_def
by fast
}
then show ?thesis
by simp
qed

― ‹TODO unwrap the simp proof.›
lemma action_dom_subset_valid_states_FDOM:
fixes p e s
assumes "(p, e) ∈ PROB" "s ∈ valid_states PROB"
shows "action_dom p e ⊆ fmdom' s"
using assms
by (simp add: Sup_upper pair_imageI prob_dom_def valid_states_def)

― ‹TODO unwrap the metis proof.›
lemma FDOM_eff_subset_prob_dom:
fixes p e
assumes "(p, e) ∈ PROB"
shows "fmdom' e ⊆ prob_dom PROB"
using assms
by (metis Sup_upper Un_subset_iff action_dom_def pair_imageI prob_dom_def)

lemma FDOM_eff_subset_prob_dom_pair:
fixes a
assumes "a ∈ PROB"
shows "fmdom' (snd a) ⊆ prob_dom PROB"
using assms(1) FDOM_eff_subset_prob_dom surjective_pairing
by metis

― ‹TODO unwrap metis proof.›
lemma FDOM_pre_subset_prob_dom:
fixes p e
assumes "(p, e) ∈ PROB"
shows "fmdom' p ⊆ prob_dom PROB"
using assms
by (metis (no_types) Sup_upper Un_subset_iff action_dom_def pair_imageI prob_dom_def)

lemma FDOM_pre_subset_prob_dom_pair:
fixes a
assumes "a ∈ PROB"
shows "fmdom' (fst a) ⊆ prob_dom PROB"
using assms FDOM_pre_subset_prob_dom surjective_pairing
by metis

subsubsection "Properties of Valid Plans"

assumes "(h # as ∈ valid_plans PROB)"
shows  "h ∈ PROB"
using assms valid_plans_def
by force

lemma valid_plan_valid_tail:
assumes "(h # as ∈ valid_plans PROB)"
shows "(as ∈ valid_plans PROB)"
using assms

― ‹TODO unwrap simp proof.›
lemma valid_plan_pre_subset_prob_dom_pair:
assumes "as ∈ valid_plans PROB"
shows "(∀a. ListMem a as ⟶ fmdom' (fst a) ⊆ (prob_dom PROB))"
unfolding valid_plans_def
using assms
by (simp add: FDOM_pre_subset_prob_dom_pair ListMem_iff rev_subsetD valid_plans_def)

lemma valid_append_valid_suff:
assumes "as1 @ as2 ∈ (valid_plans PROB)"
shows "as2 ∈ (valid_plans PROB)"
using assms

lemma valid_append_valid_pref:
assumes "as1 @ as2 ∈ (valid_plans PROB)"
shows "as1 ∈ (valid_plans PROB)"
using assms

lemma valid_pref_suff_valid_append:
assumes "as1 ∈ (valid_plans PROB)" "as2 ∈ (valid_plans PROB)"
shows "(as1 @ as2) ∈ (valid_plans PROB)"
using assms

― ‹NOTE showcase (case split seems necessary for MP of IH but the original proof does not need it).›
lemma MEM_statelist_FDOM:
fixes PROB h as s0
assumes "s0 ∈ (valid_states PROB)" "as ∈ (valid_plans PROB)" "ListMem h (state_list s0 as)"
shows "(fmdom' h = fmdom' s0)"
using assms
proof (induction as arbitrary: PROB h s0)
case Nil
have "h = s0"
using Nil.prems(3) ListMem_iff
by force
then show ?case
by simp
next
case (Cons a as)
then show ?case
― ‹NOTE This case split seems necessary to be able to infer

'ListMem h (state\_list (state\_succ s0 a) as)'

which is required in order to apply MP to the induction hypothesis.›
proof (cases "h = s0")
case False
― ‹TODO proof steps could be refactored into auxillary lemmas.›
{
have "a ∈ PROB"
by fast
then have "fmdom' (snd a) ⊆ fmdom' s0"
using Cons.prems(1) FDOM_eff_subset_FDOM_valid_states_pair
by blast
then have "fmdom' (state_succ s0 a) = fmdom' s0"
using FDOM_state_succ[of _ s0] Cons.prems(1) valid_states_def
by presburger
}
note 1 = this
{
have "fmdom' s0 = prob_dom PROB"
using Cons.prems(1) valid_states_def
by fast
then have "state_succ s0 a ∈ valid_states PROB"
unfolding valid_states_def
using 1
by force
}
note 2 = this
{
have "ListMem h (state_list (state_succ s0 a) as)"
using Cons.prems(3) False
}
note 3 = this
{
have "as ∈ valid_plans PROB"
using Cons.prems(2) valid_plan_valid_tail
by fast
then have "fmdom' h = fmdom' (state_succ s0 a)"
using 1 2 3 Cons.IH[of "state_succ s0 a"]
by blast
}
then show ?thesis
using 1
by argo
qed simp
qed

― ‹TODO unwrap metis proof.›
lemma MEM_statelist_valid_state:
fixes PROB h as s0
assumes "s0 ∈ valid_states PROB" "as ∈ valid_plans PROB" "ListMem h (state_list s0 as)"
shows "(h ∈ valid_states PROB)"
using assms
by (metis MEM_statelist_FDOM mem_Collect_eq valid_states_def)

― ‹TODO refactor (characterization lemma for 'state\_succ').›
― ‹TODO unwrap metis proof.›
lemma lemma_1_i:
fixes s a PROB
assumes "s ∈ valid_states PROB" "a ∈ PROB"
shows "state_succ s a ∈ valid_states PROB"
using assms
by (metis FDOM_eff_subset_FDOM_valid_states_pair FDOM_state_succ mem_Collect_eq  valid_states_def)

― ‹TODO unwrap smt proof.›
lemma lemma_1_ii:
"last ` ((#) s ` state_set (state_list (state_succ s a) as))
= last ` state_set (state_list (state_succ s a) as)"
by (smt NIL_NOTIN_stateset image_cong image_image last_ConsR)

lemma lemma_1:
fixes as :: "(('a, 'b) fmap × ('a, 'b) fmap) list" and PPROB
assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "((last ` (state_set (state_list s as))) ⊆ valid_states PROB)"
using assms
proof (induction as arbitrary: s PROB)
― ‹NOTE Base case simplifies to @{term "{s} ⊆ valid_states PROB"} which itself follows directly from
1st assumption.›
case (Cons a as)
text ‹ Split the 'insert' term produced by @{term "state_set (state_list s (a # as))"} and proof
inclusion in 'valid\_states PROB' for both parts. ›
{
― ‹NOTE Inclusion of the first subset follows from the induction premise by simplification.
The inclusion of the second subset is shown by applying the induction hypothesis to
`state\_succ s a` and some elementary set simplifications.›
have "last [s] ∈ valid_states PROB"
using Cons.prems(1)
by simp
moreover {
{
have "a ∈ PROB"
by fast
then have "state_succ s a ∈ valid_states PROB"
using Cons.prems(1) lemma_1_i
by blast
}
moreover have "as ∈ valid_plans PROB"
using Cons.prems(2) valid_plan_valid_tail
by fast
then have "(last ` state_set (state_list (state_succ s a) as)) ⊆ valid_states PROB"
using  calculation Cons.IH[of "state_succ s a"]
by presburger
then have "(last ` ((#) s ` state_set (state_list (state_succ s a) as))) ⊆ valid_states PROB"
using lemma_1_ii
by metis
}
ultimately have
"(last ` insert [s] ((#) s ` state_set (state_list (state_succ s a) as))) ⊆ valid_states PROB"
by simp
}
then show ?case
by fastforce
qed auto

― ‹TODO unwrap metis proof.›
lemma len_in_state_set_le_max_len:
fixes as x PROB
assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "¬(as = [])"
"(x ∈ state_set (state_list s as))"
shows "(length x ≤ (Suc (length as)))"
using assms
by (metis LENGTH_state_set Suc_eq_plus1_left add.commute state_list_length_lemma_2)

lemma card_state_set_cons:
fixes as s h
shows "
(card (state_set (state_list s (h # as)))
= Suc (card (state_set (state_list (state_succ s h) as))))
"
by (metis length_Cons state_list.simps(2) state_set_card)

lemma card_state_set:
fixes as s
shows "(Suc (length as)) = card (state_set (state_list s as))"

lemma neq_mems_state_set_neq_len:
fixes as x y s
assumes "x ∈ state_set (state_list s as)" "(y ∈ state_set (state_list s as))" "¬(x = y)"
shows "¬(length x = length y)"
proof -
have "x ≠ []" "prefix x (state_list s as)"
using assms(1) state_set_thm
by blast+
moreover have "y ≠ []" "prefix y (state_list s as)"
using assms(2) state_set_thm
by blast+
ultimately show ?thesis
using assms(3) append_eq_append_conv prefixE
by metis
qed

― ‹NOTE added definition (imported from pred\_setScript.sml:1562).›
definition inj :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ bool" where
"inj f A B ≡ (∀x ∈ A. f x ∈ B) ∧ inj_on f A"

― ‹NOTE added lemma; refactored from `not\_eq\_last\_diff\_paths`.›
lemma not_eq_last_diff_paths_i:
fixes s as PROB
assumes "s ∈ valid_states PROB" "as ∈ valid_plans PROB" "x ∈ state_set (state_list s as)"
shows "last x ∈ valid_states PROB"
proof -
have "last x ∈ last ` (state_set (state_list s as))"
using assms(3)
by simp
then show ?thesis
using assms(1, 2) lemma_1
by blast
qed

lemma not_eq_last_diff_paths_ii:
assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
"¬(inj (last) (state_set (state_list s as)) (valid_states PROB))"
shows "∃l1. ∃l2.
l1 ∈ state_set (state_list s as)
∧ l2 ∈ state_set (state_list s as)
∧ last l1 = last l2
∧ l1 ≠ l2
"
proof -
let ?S="state_set (state_list s as)"
have 1: "¬(∀x∈?S. last x ∈ valid_states PROB) = False"
using assms(1, 2) not_eq_last_diff_paths_i
by blast
{
have
"(¬(inj (last) ?S (valid_states PROB))) = (¬((∀x∈?S. ∀y∈?S. last x = last y ⟶ x = y)))"
unfolding inj_def inj_on_def
using 1
by blast
then have "
(¬(inj (last) ?S (valid_states PROB)))
= (∃x. ∃y. x∈?S ∧ y∈?S ∧ last x = last y ∧ x ≠ y)
"
using assms(3)
by blast
}
then show ?thesis
using assms(3) by blast
qed

lemma not_eq_last_diff_paths:
fixes as PROB s
assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
"¬(inj (last) (state_set (state_list s as)) (valid_states PROB))"
shows "(∃slist_1 slist_2.
(slist_1 ∈ state_set (state_list s as))
∧ (slist_2 ∈ state_set (state_list s as))
∧ ((last slist_1) = (last slist_2))
∧ ¬(length slist_1 = length slist_2))
"
proof -
obtain l1 l2 where "
l1 ∈ state_set (state_list s as)
∧ l2 ∈ state_set (state_list s as)
∧ last l1 = last l2
∧ l1 ≠ l2
"
using assms(1, 2, 3) not_eq_last_diff_paths_ii
by blast
then show ?thesis
using neq_mems_state_set_neq_len
by blast
qed

― ‹NOTE this lemma was removed due to being redundant and being shadowed later on:

lemma empty\_list\_nin\_state\_set›

lemma nempty_sl_in_state_set:
fixes sl
assumes "sl ≠ []"
shows "sl ∈ state_set sl"
using assms state_set_thm
by auto

lemma empty_list_nin_state_set:
fixes h slist as
assumes "(h # slist) ∈ state_set (state_list s as)"
shows "(h = s)"
using assms
by (induction as) auto

lemma cons_in_state_set_2:
fixes s slist h t
assumes "(slist ≠ [])" "((s # slist) ∈ state_set (state_list s (h # t)))"
shows "(slist ∈ state_set (state_list (state_succ s h) t))"
using assms
by (induction slist) auto

― ‹TODO move up and replace 'FactoredSystem.lemma\_1\_i'?›
lemma valid_action_valid_succ:
assumes "h ∈ PROB" "s ∈ valid_states PROB"
shows "(state_succ s h) ∈ valid_states PROB"
using assms lemma_1_i
by blast

lemma in_state_set_imp_eq_exec_prefix:
fixes slist as PROB s
assumes "(as ≠ [])" "(slist ≠ [])" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
"(slist ∈ state_set (state_list s as))"
shows
"(∃as'. (prefix as' as) ∧ (exec_plan s as' = last slist) ∧ (length slist = Suc (length as')))"
using assms
proof (induction slist arbitrary: as s PROB)
case cons_1: (Cons a slist)
have 1: "s # slist ∈ state_set (state_list s as)"
using cons_1.prems(5) empty_list_nin_state_set
by auto
then show ?case
using cons_1
proof (cases as)
case cons_2: (Cons a' R⇩a⇩s)
then have a: "state_succ s a' ∈ valid_states PROB"
by metis
then have b: "R⇩a⇩s ∈ valid_plans PROB"
using cons_1.prems(4) cons_2 valid_plan_valid_tail
by fast
then show ?thesis
proof (cases slist)
case Nil
then show ?thesis
using cons_1.prems(5) empty_list_nin_state_set
by auto
next
case cons_3: (Cons a'' R⇩s⇩l⇩i⇩s⇩t)
then have i: "a'' # R⇩s⇩l⇩i⇩s⇩t ∈ state_set (state_list (state_succ s a') R⇩a⇩s)"
using 1 cons_2 cons_in_state_set_2
by blast
then show ?thesis
proof (cases R⇩a⇩s)
case Nil
then show ?thesis
using i cons_2 cons_3
by auto
next
case (Cons a''' R⇩a⇩s')
then obtain as' where
"prefix as' (a''' # R⇩a⇩s')" "exec_plan (state_succ s a') as' = last slist"
"length slist = Suc (length as')"
using cons_1.IH[of "a''' # R⇩a⇩s'" "state_succ s a'" PROB]
using i a b cons_3
by blast
then show ?thesis
using Cons_prefix_Cons cons_2 cons_3 exec_plan.simps(2) last.simps length_Cons
list.distinct(1) local.Cons
by metis
qed
qed
qed auto
qed auto

lemma eq_last_state_imp_append_nempty_as:
fixes as PROB slist_1 slist_2
assumes "(as ≠ [])" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "(slist_1 ≠ [])"
"(slist_2 ≠ [])" "(slist_1 ∈ state_set (state_list s as))"
"(slist_2 ∈ state_set (state_list s as))" "¬(length slist_1 = length slist_2)"
"(last slist_1 = last slist_2)"
shows "(∃as1 as2 as3.
(as1 @ as2 @ as3 = as)
∧ (exec_plan s (as1 @ as2) = exec_plan s as1)
∧  ¬(as2 = [])
)"
proof -
obtain as_1 where 1: "(prefix as_1 as)" "(exec_plan s as_1 = last slist_1)"
"length slist_1 = Suc (length as_1)"
using assms(1, 2, 3, 4, 6) in_state_set_imp_eq_exec_prefix
by blast
obtain as_2 where 2: "(prefix as_2 as)" "(exec_plan s as_2 = last slist_2)"
"(length slist_2) = Suc (length as_2)"
using assms(1, 2, 3, 5, 7) in_state_set_imp_eq_exec_prefix
by blast
then have "length as_1 ≠ length as_2"
using assms(8) 1(3) 2(3)
by fastforce
then consider (i) "length as_1 < length as_2" | (ii) "length as_1 > length as_2"
by force
then show ?thesis
proof (cases)
case i
then have "prefix as_1 as_2"
using 1(1) 2(1) len_gt_pref_is_pref
by blast
then obtain a where a1: "as_2 = as_1 @ a"
using prefixE
by blast
then obtain b where b1: "as = as_2 @ b"
using prefixE 2(1)
by blast
let ?as1="as_1"
let ?as2="a"
let ?as3="b"
have "as = ?as1 @ ?as2 @ ?as3"
using a1 b1
by simp
moreover have "exec_plan s (?as1 @ ?as2) = exec_plan s ?as1"
using 1(2) 2(2) a1 assms(9)
by auto
moreover have "?as2 ≠ []"
using i a1
by simp
ultimately show ?thesis
by blast
next
case ii
then have "prefix as_2 as_1"
using 1(1) 2(1) len_gt_pref_is_pref
by blast
then obtain a where a2: "as_1 = as_2 @ a"
using prefixE
by blast
then obtain b where b2: "as = as_1 @ b"
using prefixE 1(1)
by blast
let ?as1="as_2"
let ?as2="a"
let ?as3="b"
have "as = ?as1 @ ?as2 @ ?as3"
using a2 b2
by simp
moreover have "exec_plan s (?as1 @ ?as2) = exec_plan s ?as1"
using 1(2) 2(2) a2 assms(9)
by auto
moreover have "?as2 ≠ []"
using ii a2
by simp
ultimately show ?thesis
by blast
qed
qed

lemma FINITE_prob_dom:
assumes "finite PROB"
shows  "finite (prob_dom PROB)"
proof -
{
fix x
assume P2: "x ∈ PROB"
then have 1: "(λ(s1, s2). action_dom s1 s2) x = fmdom' (fst x) ∪ fmdom' (snd x)"
then have 2: "finite (fset (fmdom (fst x)))" "finite (fset (fmdom (snd x)))"
by auto
then have 3: "fset (fmdom (fst x)) = fmdom' (fst x)" "fset (fmdom (snd x)) = fmdom' (snd x)"
then have "finite (fmdom' (fst x))"
using 2 by auto
then have "finite (fmdom' (snd x))"
using 2 3 by auto
then have "finite ((λ(s1, s2). action_dom s1 s2) x)"
using 1 2 3
by simp
}
then show "finite (prob_dom PROB)"
unfolding prob_dom_def
using assms
by blast
qed

lemma CARD_valid_states:
assumes "finite (PROB :: 'a problem)"
shows "(card (valid_states PROB :: 'a state set) = 2 ^ card (prob_dom PROB))"
proof -
have 1: "finite (prob_dom PROB)"
using assms FINITE_prob_dom
by blast
have"(card (valid_states PROB :: 'a state set)) = card {s :: 'a state. fmdom' s = prob_dom PROB}"
unfolding valid_states_def
by simp
also have "...  = 2 ^ (card (prob_dom PROB))"
using 1 card_of_set_of_all_possible_states
by blast
finally show ?thesis
by blast
qed

― ‹NOTE type of 'valid\_states PROB' has to be asserted to match 'FINITE\_states' in the proof.›
lemma FINITE_valid_states:
fixes PROB :: "'a problem"
shows "finite PROB ⟹ finite ((valid_states PROB) :: 'a state set)"
proof (induction PROB rule: finite.induct)
case emptyI
then have "valid_states {} = {fmempty}"
unfolding valid_states_def prob_dom_def
using empty_domain_fmap_set
by force
then show ?case
by(subst ‹valid_states {} = {fmempty}›) auto
next
case (insertI A a)
{
then have "finite (insert a A)"
by blast
then have "finite (prob_dom (insert a A))"
using FINITE_prob_dom
by blast
then have "finite {s :: 'a state. fmdom' s = prob_dom (insert a A)}"
using FINITE_states
by blast
}
then show ?case
unfolding valid_states_def
by simp
qed

― ‹NOTE type of 'PROB' had to be fixed for use of 'FINITE\_valid\_states'.›
lemma lemma_2:
fixes PROB :: "'a problem" and as :: "('a action) list" and s :: "'a state"
assumes "finite PROB" "s ∈ (valid_states PROB)" "(as ∈ valid_plans PROB)"
"((length as) > (2 ^ (card (fmdom' s)) - 1))"
shows "(∃as1 as2 as3.
(as1 @ as2 @ as3 = as)
∧ (exec_plan s (as1 @ as2) = exec_plan s as1)
∧ ¬(as2 = [])
)"
proof -
have "Suc (length as) > 2^(card (fmdom' s))"
using assms(4)
by linarith
then have 1: "card (state_set (state_list s as)) > 2^card (fmdom' s)"
using card_state_set[symmetric]
by metis
{
― ‹NOTE type of 'valid\_states PROB' had to be asserted to match 'FINITE\_valid\_states'.›
have 2: "finite (prob_dom PROB)" "finite ((valid_states PROB)  :: 'a state set)"
using assms(1) FINITE_prob_dom FINITE_valid_states
by blast+
have 3: "fmdom' s = prob_dom PROB"
using assms(2) valid_states_def
by fast
then have "card ((valid_states PROB) :: 'a state set) = 2^card (fmdom' s)"
using assms(1) CARD_valid_states
by auto
then have 4: "card (state_set (state_list (s :: 'a state) as)) > card ((valid_states PROB) :: 'a state set)"
unfolding valid_states_def
using 1 2(1) 3 card_of_set_of_all_possible_states[of "prob_dom PROB"]
by argo
― ‹TODO refactor into lemma.›
{
let ?S="state_set (state_list (s :: 'a state) as)"
let ?T="valid_states PROB :: 'a state set"
assume C2: "inj_on last ?S"
― ‹TODO unwrap the metis step or refactor into lemma.›
have a: "?T ⊆ last ` ?S"
using C2
by (metis "2"(2) "4" assms(2) assms(3) card_image card_mono lemma_1 not_less)
have "finite (state_set (state_list s as))"
using state_set_finite
by auto
then have "card (last ` ?S) = card ?S"
using C2 inj_on_iff_eq_card
by blast
also have "… > card ?T"
using 4
by blast
then have "∃x. x ∈ (last ` ?S) ∧ x ∉ ?T"
using C2 a assms(2) assms(3) calculation lemma_1
by fastforce
}
note 5 = this
moreover
{
assume C: "inj last (state_set (state_list (s :: 'a state) as)) (valid_states PROB)"
then have "inj_on last (state_set (state_list (s :: 'a state) as))"
using C inj_def
by blast
then obtain x where "x ∈ last ` (state_set (state_list s as)) ∧ x ∉ valid_states PROB"
using 5
by presburger
then have "¬(∀x∈state_set (state_list s as). last x ∈ valid_states PROB)"
by blast
then have "¬inj last (state_set (state_list (s :: 'a state) as)) (valid_states PROB)"
using inj_def
by metis
then have False
using C
by simp
}
ultimately have "¬inj last (state_set (state_list (s :: 'a state) as)) (valid_states PROB)"
unfolding inj_def
by blast
}
then obtain slist_1 slist_2 where 6:
"slist_1 ∈ state_set (state_list s as)"
"slist_2 ∈ state_set (state_list s as)"
"(last slist_1 = last slist_2)"
"length slist_1 ≠ length slist_2"
using assms(2, 3) not_eq_last_diff_paths
by blast
then show ?thesis
proof (cases as)
case Nil
text ‹ 4th assumption is violated in the 'Nil' case. ›
then have "¬(2 ^ card (fmdom' s) - 1 < length as)"
using Nil
by simp
then show ?thesis
using assms(4)
by blast
next
case (Cons a list)
then have "as ≠ []"
by simp
moreover have "slist_1 ≠ []" "slist_2 ≠ []"
using 6(1, 2) NIL_NOTIN_stateset
by blast+
ultimately show ?thesis
using assms(2, 3) 6(1, 2, 3, 4) eq_last_state_imp_append_nempty_as
by fastforce
qed
qed

lemma lemma_2_prob_dom:
fixes PROB and as :: "('a action) list" and s :: "'a state"
assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
"(length as > (2 ^ (card (prob_dom PROB))) - 1)"
shows "(∃as1 as2 as3.
(as1 @ as2 @ as3 = as)
∧ (exec_plan s (as1 @ as2) = exec_plan s as1)
∧ ¬(as2 = [])
)"
proof -
have "prob_dom PROB = fmdom' s"
using assms(2) valid_states_def
by fast
then have "2 ^ card (fmdom' s) - 1 < length as"
using assms(4)
by argo
then show ?thesis
using assms(1, 2, 3) lemma_2
by blast
qed

― ‹NOTE type for `s` had to be fixed (type mismatch in obtain statement).›
― ‹NOTE type for `as1`, `as2` and `as3` had to be fixed (due type mismatch on `as1` in
`cycle\_removal\_lemma`)›
lemma lemma_3:
fixes PROB :: "'a problem" and s :: "'a state"
assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
"(length as > (2 ^ (card (prob_dom PROB)) - 1))"
shows "(∃as'.
(exec_plan s as = exec_plan s as')
∧ (length as' < length as)
∧ (subseq as' as)
)"
proof -
have "prob_dom PROB = fmdom' s"
using assms(2) valid_states_def
by fast
then have "2 ^ card (fmdom' s) - 1 < length as"
using assms(4)
by argo
then obtain as1 as2 as3 :: "'a action list" where 1:
"as1 @ as2 @ as3 = as" "exec_plan s (as1 @ as2) = exec_plan s as1" "as2 ≠ []"
using assms(1, 2, 3) lemma_2
by metis
have 2: "exec_plan s (as1 @ as3) = exec_plan s (as1 @ as2 @ as3)"
using 1 cycle_removal_lemma
by fastforce
let ?as' = "as1 @ as3"
have "exec_plan s as = exec_plan s ?as'"
using 1 2
by auto
moreover have "length ?as' < length as"
by blast
moreover have "subseq ?as' as"
using 1 subseq_append'
by blast
ultimately show "(∃as'.
(exec_plan s as = exec_plan s as') ∧ (length as' < length as) ∧ (subseq as' as))"
by blast
qed

― ‹TODO unwrap meson step.›
lemma sublist_valid_is_valid:
fixes as' as PROB
assumes "(as ∈ valid_plans PROB)" "(subseq as' as)"
shows "as' ∈ valid_plans PROB"
using assms
by (simp add: valid_plans_def) (meson dual_order.trans fset_of_list_subset sublist_subset)

― ‹NOTE type of 's' had to be fixed (type mismatch in goal).›
theorem main_lemma:
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' ≤ (2 ^ (card (prob_dom PROB))) - 1)
)"
proof (cases "length as ≤ (2 ^ (card (prob_dom PROB))) - 1")
case True
then have "exec_plan s as = exec_plan s as"
by simp
then have "subseq as as"
by auto
then have "length as ≤ (2^(card (prob_dom PROB)) - 1)"
using True
by auto
then show ?thesis
by blast
next
case False
then have "length as > (2 ^ (card (prob_dom PROB))) - 1"
using False
by auto
then obtain as' where 1:
"exec_plan s as = exec_plan s as'" "length as' < length as" "subseq as' as"
using assms lemma_3
by blast
{
fix p
assume "exec_plan s as = exec_plan s p" "subseq p as"
"2 ^ card (prob_dom PROB) - 1 < length p"
then have "(∃p'. (exec_plan s as = exec_plan s p' ∧ subseq p' as) ∧ length p' < length p)"
using assms(1, 2, 3) lemma_3 sublist_valid_is_valid
by fastforce
}
then have "∀p. exec_plan s as = exec_plan s p ∧ subseq p as ⟶
(∃p'. (exec_plan s as = exec_plan s p' ∧ subseq p' as)
∧ length p' ≤ 2 ^ card (prob_dom PROB) - 1)"
using general_theorem[where
P = "λ(as'' :: 'a action list). (exec_plan s as = exec_plan s as'') ∧ subseq as'' as"
and l = "(2 ^ (card (prob_dom (PROB ::'a problem)))) - 1" and f = length]
by blast
then obtain p' where
"exec_plan s as = exec_plan s p'" "subseq p' as" "length p' ≤ 2 ^ card (prob_dom PROB) - 1"
by blast
then show ?thesis
using sublist_refl
by blast
qed

subsection "Reachable States"

― ‹NOTE shortened to 'reachable\_s'›
definition reachable_s where
"reachable_s PROB s ≡ {exec_plan s as | as. as ∈ valid_plans PROB}"

― ‹NOTE types for `s` and `PROB` had to be fixed (type mismatch in goal).›
lemma valid_as_valid_exec:
fixes as and s :: "'a state" and PROB :: "'a problem"
assumes "(as ∈ valid_plans PROB)" "(s ∈ valid_states PROB)"
shows "(exec_plan s as ∈ valid_states PROB)"
using assms
proof (induction as arbitrary: s PROB)
case (Cons a as)
then have "a ∈ PROB"
by metis
then have "state_succ s a ∈ valid_states PROB"
using Cons.prems(2) valid_action_valid_succ
by blast
moreover have "as ∈ valid_plans PROB"
using Cons.prems(1) valid_plan_valid_tail
by fast
ultimately show ?case
using Cons.IH
by force
qed simp

lemma exec_plan_fdom_subset:
fixes as s PROB
assumes "(as ∈ valid_plans PROB)"
shows "(fmdom' (exec_plan s as) ⊆ (fmdom' s ∪ prob_dom PROB))"
using assms
proof (induction as arbitrary: s PROB)
case (Cons a as)
have "as ∈ valid_plans PROB"
using Cons.prems valid_plan_valid_tail
by fast
then have "fmdom' (exec_plan (state_succ s a) as) ⊆ fmdom' (state_succ s a) ∪ prob_dom PROB"
using Cons.IH[of _ "state_succ s a"]
by simp
― ‹TODO unwrap metis proofs.›
moreover have "fmdom' s ∪ fmdom' (snd a) ∪ prob_dom PROB = fmdom' s ∪ prob_dom PROB"
by (metis
ultimately show ?case
by (metis (no_types, lifting)
FDOM_state_succ_subset exec_plan.simps(2) order_refl subset_trans sup.mono)
qed simp

lemma reachable_s_finite_thm_1_a:
fixes s and PROB :: "'a problem"
assumes "(s :: 'a state) ∈ valid_states PROB"
shows "(∀l∈reachable_s PROB s. l∈valid_states PROB)"
proof -
have 1: "∀l∈reachable_s PROB s. ∃as. l = exec_plan s as ∧ as ∈ valid_plans PROB"
using reachable_s_def
by fastforce
{
fix l
assume P1: "l ∈ reachable_s PROB s"
― ‹NOTE type for 's' and 'as' had to be fixed due to type mismatch in obtain statement.›
then obtain as :: "'a action list" where a: "l = exec_plan s as ∧ as ∈ valid_plans PROB"
using 1
by blast
then have "exec_plan s as ∈ valid_states PROB"
using assms a valid_as_valid_exec
by blast
then have "l ∈ valid_states PROB"
using a
by simp
}
then show "∀l ∈ reachable_s PROB s. l ∈ valid_states PROB"
by blast
qed

lemma reachable_s_finite_thm_1:
assumes "((s :: 'a state) ∈ valid_states PROB)"
shows "(reachable_s PROB s ⊆ valid_states PROB)"
using assms reachable_s_finite_thm_1_a
by blast

― ‹NOTE second declaration skipped (this is declared twice in the source; see above)›
― ‹NOTE type for `s` had to be fixed (type mismatch in goal).›
lemma reachable_s_finite_thm:
fixes s :: "'a state"
assumes "finite (PROB :: 'a problem)" "(s ∈ valid_states PROB)"
shows "finite (reachable_s PROB s)"
using assms
by (meson FINITE_valid_states reachable_s_finite_thm_1 rev_finite_subset)

lemma empty_plan_is_valid: "[] ∈ (valid_plans PROB)"

assumes "(h ∈ PROB)" "(as ∈ valid_plans PROB)"
shows "((h # as) ∈ valid_plans PROB)"
using assms
by (auto simp: valid_plans_def)

― ‹TODO refactor›
lemma lemma_1_reachability_s_i:
fixes PROB s
assumes "s ∈ valid_states PROB"
shows "s ∈ reachable_s PROB s"
proof -
have "[] ∈ valid_plans PROB"
using empty_plan_is_valid
by blast
then show ?thesis
unfolding reachable_s_def
by force
qed

― ‹NOTE types for 'PROB' and 's' had to be fixed (type mismatch in goal).›
lemma lemma_1_reachability_s:
fixes PROB :: "'a problem" and s :: "'a state" and as
assumes "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "((last ` state_set (state_list s as)) ⊆ (reachable_s PROB s))"
using assms
proof(induction as arbitrary: PROB s)
case Nil
then have "(last ` state_set (state_list s [])) = {s}"
by force
then show ?case
unfolding reachable_s_def
using empty_plan_is_valid
by force
next
case cons: (Cons a as)
let ?S="last ` state_set (state_list s (a # as))"
{
let ?as="[]"
have "last [s] = exec_plan s ?as"
by simp
moreover have "?as ∈ valid_plans PROB"
using empty_plan_is_valid
by auto
ultimately have "∃as. (last [s] = exec_plan s as) ∧ as ∈ valid_plans PROB"
by blast
}
note 1 = this
{
fix x
assume P: "x ∈ ?S"
then consider
(a) "x = last [s]"
| (b) "x ∈ last ` ((#) s ` state_set (state_list (state_succ s a) as))"
by auto
then have "x ∈ reachable_s PROB s"
proof (cases)
case a
then have "x = s"
by simp
then show ?thesis
using cons.prems(1) P lemma_1_reachability_s_i
by blast
next
case b
then obtain x'' where i:
"x'' ∈ state_set (state_list (state_succ s a) as)"
"x = last (s # x'')"
by blast
then show ?thesis
proof (cases "x''")
case Nil
then have "x = s"
using i
by fastforce
then show ?thesis
using cons.prems(1) lemma_1_reachability_s_i
by blast
next
case (Cons a' list)
then obtain x' where a:
"last (a' # list) = last x'" "x' ∈ state_set (state_list (state_succ s a) as)"
using i(1)
by blast
{
have "state_succ s a ∈ valid_states PROB"
by metis
moreover have "as ∈ valid_plans PROB"
using cons.prems(2) valid_plan_valid_tail
by fast
ultimately have
"last ` state_set (state_list (state_succ s a) as) ⊆ reachable_s PROB (state_succ s a)"
using cons.IH[of "state_succ s a"]
by auto
then have "∃as'.
last (a' # list) = exec_plan (state_succ s a) as' ∧ (as' ∈ (valid_plans PROB))"
unfolding state_set.simps state_list.simps reachable_s_def
using i(1) Cons
by blast
}
then obtain as' where b:
"last (a' # list) = exec_plan (state_succ s a) as'" "(as' ∈ (valid_plans PROB))"
by blast
then have "x = exec_plan (state_succ s a) as'"
using i(2) Cons a(1)
by auto
then show ?thesis unfolding reachable_s_def
using cons.prems(2) b(2)
by (metis (mono_tags, lifting)  exec_plan.simps(2) mem_Collect_eq
qed
qed
}
then show ?case
by blast
qed

― ‹NOTE types for `PROB` and `s` had to be fixed for use of `lemma\_1\_reachability\_s`.›
lemma not_eq_last_diff_paths_reachability_s:
fixes PROB :: "'a problem" and s :: "'a state" and as
assumes "s ∈ valid_states PROB" "as ∈ valid_plans PROB"
"¬(inj last (state_set (state_list s as)) (reachable_s PROB s))"
shows "(∃slist_1 slist_2.
slist_1 ∈ state_set (state_list s as)
∧ slist_2 ∈ state_set (state_list s as)
∧ (last slist_1 = last slist_2)
∧ ¬(length slist_1 = length slist_2)
)"
proof -
{
fix x
assume P1: "x ∈ state_set (state_list s as)"
have a: "last ` state_set (state_list s as) ⊆ reachable_s PROB s"
using assms(1, 2) lemma_1_reachability_s
by fast
then have "∀as PROB. s ∈ (valid_states PROB) ∧ as ∈ (valid_plans PROB) ⟶ (last ` (state_set (state_list s as)) ⊆ reachable_s PROB s)"
using lemma_1_reachability_s
by fast
then have "last x ∈ valid_states PROB"
using assms(1, 2) P1 lemma_1
by fast
then have "last x ∈ reachable_s PROB s"
using P1 a
by fast
}
note 1 = this
text ‹ Show the goal by disproving the contradiction. ›
{
assume C: "(∀slist_1 slist_2. (slist_1 ∈ state_set (state_list s as)
∧ slist_2 ∈ state_set (state_list s as)
∧ (last slist_1 = last slist_2)) ⟶ (length slist_1 = length slist_2))"
moreover {
fix slist_1 slist_2
assume C1: "slist_1 ∈ state_set (state_list s as)" "slist_2 ∈ state_set (state_list s as)"
"(last slist_1 = last slist_2)"
moreover have i: "(length slist_1 = length slist_2)"
using C1 C
by blast
moreover have "slist_1 = slist_2"
using C1(1, 2) i neq_mems_state_set_neq_len
by auto
ultimately have "inj_on last (state_set (state_list s as))"
unfolding inj_on_def
using C neq_mems_state_set_neq_len
by blast
then have False
using 1 inj_def assms(3)
by blast
}
ultimately have False
by (metis empty_state_list_lemma nempty_sl_in_state_set)
}
then show ?thesis
by blast
qed

― ‹NOTE added lemma ( translation of `PHP` in pred\_setScript.sml:3155).›
lemma lemma_2_reachability_s_i:
fixes f :: "'a ⇒ 'b" and s t
assumes "finite t" "card t < card s"
shows "¬(inj f s t)"
proof -
{
assume C: "inj f s t"
then have 1: "(∀x∈s. f x ∈ t)" "inj_on f s"
unfolding inj_def
by blast+
moreover {
have "f ` s ⊆ t"
using 1
by fast
then have "card (f ` s) ≤ card t"
using assms(1) card_mono
by auto
}
moreover have "card (f ` s) = card s"
using 1 card_image
by fast
ultimately have False
using assms(2)
by linarith
}
then show ?thesis
by blast
qed

lemma lemma_2_reachability_s:
fixes PROB :: "'a problem" and as s
assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
"(length as > card (reachable_s PROB s) - 1)"
shows "(∃as1 as2 as3.
(as1 @ as2 @ as3 = as) ∧ (exec_plan s (as1 @ as2) = exec_plan s as1) ∧ ¬(as2 = []))"
proof -
{
have "Suc (length as) > card (reachable_s PROB s)"
using assms(4)
by fastforce
then have "card (state_set (state_list s as)) > card (reachable_s PROB s)"
using card_state_set
by metis
}
note 1 = this
{
have "finite (reachable_s PROB s)"
using assms(1, 2) reachable_s_finite_thm
by blast
then have "¬(inj last (state_set (state_list s as)) (reachable_s PROB s))"
using assms(4) 1 lemma_2_reachability_s_i
by blast
}
note 2 = this
obtain slist_1 slist_2 where 3:
"slist_1 ∈ state_set (state_list s as)" "slist_2 ∈ state_set (state_list s as)"
"(last slist_1 = last slist_2)" "length slist_1 ≠ length slist_2"
using assms(2, 3) 2 not_eq_last_diff_paths_reachability_s
by blast
then show ?thesis using assms
proof(cases as)
case (Cons a list)
then show ?thesis
using assms(2, 3) 3 eq_last_state_imp_append_nempty_as state_set_thm list.distinct(1)
by metis
qed force
qed

lemma lemma_3_reachability_s:
fixes as and PROB :: "'a problem" and s
assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
"(length as > (card (reachable_s PROB s) - 1))"
shows "(∃as'.
(exec_plan s as = exec_plan s as')
∧ (length as' < length as)
∧ (subseq as' as)
)"
proof -
obtain as1 as2 as3 :: "'a action list" where 1:
"(as1 @ as2 @ as3 = as)" "(exec_plan s (as1 @ as2) = exec_plan s as1)" "~(as2=[])"
using assms lemma_2_reachability_s
by metis
then have "(exec_plan s (as1 @ as2) = exec_plan s as1)"
using 1
by blast
then have 2: "exec_plan s (as1 @ as3) = exec_plan s (as1 @ as2 @ as3)"
using 1 cycle_removal_lemma
by fastforce
let ?as' = "as1 @ as3"
have 3: "exec_plan s as = exec_plan s ?as'"
using 1 2
by argo
then have "as2 ≠ []"
using 1
by blast
then have 4: "length ?as' < length as"
by blast
then have "subseq ?as' as"
using 1 subseq_append'
by blast
then show ?thesis
using 3 4
by blast
qed

― ‹NOTE type for `as` had to be fixed (type mismatch in goal).›
lemma main_lemma_reachability_s:
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' ≤ (card (reachable_s PROB s) - 1)))"
proof (cases "length as ≤ card (reachable_s PROB s) - 1")
case False
let ?as' = "as"
have "length as > card (reachable_s PROB s) - 1"
using False
by simp
{
fix p
assume P: "exec_plan s as = exec_plan s p" "subseq p as"
"card (reachable_s PROB s) - 1 < length p"
moreover have "p ∈ valid_plans PROB"
using assms(3) P(2) sublist_valid_is_valid
by blast
ultimately obtain as' where 1:
"exec_plan s p = exec_plan s as'" "length as' < length p" "subseq as' p"
using assms lemma_3_reachability_s
by blast
then have "exec_plan s as = exec_plan s as'"
using P
by presburger
moreover have "subseq as' as"
using P 1 sublist_trans
by blast
ultimately have "(∃p'. (exec_plan s as = exec_plan s p' ∧ subseq p' as) ∧ length p' < length p)"
using 1
by blast
}
then have "∀p.
exec_plan s as = exec_plan s p ∧ subseq p as
⟶ (∃p'.
(exec_plan s as = exec_plan s p' ∧ subseq p' as)
∧ length p' ≤ card (reachable_s PROB s) - 1)"
using general_theorem[of "λas''. (exec_plan s as = exec_plan s as'') ∧ subseq as'' as"
"(card (reachable_s (PROB :: 'a problem) (s :: 'a state)) - 1)" length]
by blast
then show ?thesis
by blast
qed blast

lemma reachable_s_non_empty: "¬(reachable_s PROB s = {})"
using empty_plan_is_valid reachable_s_def
by blast

lemma card_reachable_s_non_zero:
fixes s
assumes "finite (PROB :: 'a problem)" "(s ∈ valid_states PROB)"
shows "(0 < card (reachable_s PROB s))"
using assms
by (simp add: card_gt_0_iff reachable_s_finite_thm reachable_s_non_empty)

lemma exec_fdom_empty_prob:
fixes s
assumes "(prob_dom PROB = {})" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(exec_plan s as = fmempty)"
proof -
have "fmdom' s = {}"
using assms(1, 2)
then show "exec_plan s as = fmempty"
using assms(1, 3)
by (metis
exec_plan_fdom_subset fmrestrict_set_dom fmrestrict_set_null subset_empty
sup_bot.left_neutral)
qed

― ‹NOTE types for `PROB` and `s` had to be fixed (type mismatch in goal).›
lemma reachable_s_empty_prob:
fixes PROB :: "'a problem" and s :: "'a state"
assumes "(prob_dom PROB = {})" "(s ∈ valid_states PROB)"
shows "((reachable_s PROB s) ⊆ {fmempty})"
proof -
{
fix x
assume P1: "x ∈ reachable_s PROB s"
then obtain as :: "'a action list" where a:
"as ∈ valid_plans PROB" "x = exec_plan s as"
using reachable_s_def
by blast
then have "as ∈ valid_plans PROB" "x = exec_plan s as"
using a
by auto
then have "x = fmempty" using assms(1, 2) exec_fdom_empty_prob
by blast
}
then show "((reachable_s PROB s) ⊆ {fmempty})"
by blast
qed

― ‹NOTE this is semantically equivalent to `sublist\_valid\_is\_valid`.›
― ‹NOTE Renamed to 'sublist\_valid\_plan\_alt' because another lemma by the same name is declared
later.›
lemma sublist_valid_plan__alt:
assumes "(as1 ∈ valid_plans PROB)" "(subseq as2 as1)"
shows "(as2 ∈ valid_plans PROB)"
using assms

lemma fmsubset_eq:
assumes "s1 ⊆⇩f s2"
shows "(∀a. a |∈| fmdom s1 ⟶ fmlookup s1 a = fmlookup s2 a)"
using assms
by (metis (mono_tags, lifting) domIff fmdom_notI fmsubset.rep_eq map_le_def)

― ‹TODO refactor/move into 'FmapUtils.thy'.›
lemma submap_imp_state_succ_submap_a:
assumes "s1 ⊆⇩f s2" "s2 ⊆⇩f s3"
shows "s1 ⊆⇩f s3"
using assms fmsubset.rep_eq map_le_trans
by blast

― ‹TODO refactor into FmapUtils?›
lemma submap_imp_state_succ_submap_b:
assumes "s1 ⊆⇩f s2"
shows "(s0 ++ s1) ⊆⇩f (s0 ++ s2)"
proof -
{
assume C: "¬((s0 ++ s1) ⊆⇩f (s0 ++ s2))"
then have 1: "(s0 ++ s1) = (s1 ++⇩f s0)"
by blast
then have 2: "(s0 ++ s2) = (s2 ++⇩f s0)"
by auto
then obtain a where 3:
"a |∈| fmdom (s1 ++⇩f s0) ∧ fmlookup (s1 ++⇩f s0) ≠ fmlookup (s2 ++⇩f s0)"
using C 1 2 fmsubset.rep_eq domIff fmdom_notD map_le_def
by (metis (no_types, lifting))
then have False
using assms(1) C proof (cases "a |∈| fmdom s1")
case True
moreover have "fmlookup s1 a = fmlookup s2 a"
by (meson assms(1) calculation fmsubset_eq)
moreover have "fmlookup (s0 ++⇩f s1) a = fmlookup s1 a"
moreover have "a |∈| fmdom s2"
using True calculation(2) fmdom_notD by fastforce
moreover have "fmlookup (s0 ++⇩f s2) a = fmlookup s2 a"
moreover have "fmlookup (s0 ++⇩f s1) a = fmlookup (s0 ++⇩f s2) a"
using calculation(2, 3, 5)
by auto
ultimately show ?thesis
by (smt "1" "2" C assms domIff fmlookup_add fmsubset.rep_eq map_le_def)
next
case False
moreover have "fmlookup (s0 ++⇩f s1) a = fmlookup s0 a"
ultimately show ?thesis proof (cases "a |∈| fmdom s0")
case True
have "a |∉| fmdom (s1 ++⇩f s0)"
then show ?thesis
using 3 by blast
next
case False
then have "a |∉| fmdom (s1 ++⇩f s0)"
using ‹fmlookup (s0 ++⇩f s1) a = fmlookup s0 a›
by force
then show ?thesis
using 3
by blast
qed
qed
}
then show ?thesis
by blast
qed

― ‹NOTE type for `a` had to be fixed (type mismatch in goal).›
lemma submap_imp_state_succ_submap:
fixes a :: "'a action" and s1 s2
assumes "(fst a ⊆⇩f s1)" "(s1 ⊆⇩f s2)"
shows "(state_succ s1 a ⊆⇩f state_succ s2 a```