# Theory FactoredSystemLib

theory FactoredSystemLib
imports Main "HOL-Library.Finite_Map"
begin

section ‹Factored Systems Library›

text ‹This section contains definitions used in the factored system theory (FactoredSystem.thy) and in
other theories. ›

text ‹ Most importantly, we are redefining the map addition operator (++) to reflect HOL4
semantics which are left to right (ltr), rather than right-to-left as in Isabelle/HOL.

This means that given a finite map (M = M1 ++ M2) and a variable v which is in the domain of
both M1 and M2, the lookup M v will yield M1 v in HOL4 but M2 v in Isabelle/HOL.
This behavior can be confirmed  by looking at the definition of fmap\_add (++f,
Finite\_Map.thy:460)---which is lifted from map\_add (Map.thy:24)

@{const map_add}  (infixl "++" 100) where
@{term "m1 ++ m2 = (λx. case m2 x of None ⇒ m1 x | Some y ⇒ Some y)"}

to finite sets---and the HOL4 definition of "FUNION (finite\_mapScript.sml:770) which recurs
on union\_lemma (finite\_mapScript.sml:756)

!\^fmap g.
?union.
(FDOM union = FDOM f Union (g  FDOM)) /\
(!x. FAPPLY union x = if x IN FDOM f then FAPPLY f x else FAPPLY g x)

The ltr semantics are also reflected in [Abdulaziz et al., Definition 2, p.9].
›

― ‹NOTE hide Map.map\_add to free the operator symbol ++ and redefine it to reflect HOL4 map
definition fmap_add_ltr :: "('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap" (infixl "++" 100) where
"m1 ++ m2 ≡ m2 ++⇩f m1"

subsection ‹States, Actions and Problems.›

text ‹ Planning problems are typically formalized by considering possible states and the effect
of actions upon these states.

In this case we consider a world model in propositional logic: i.e. states are finite maps of
variables (with arbitrary type 'a) to boolean values and actions are pairs of states where the first
component specifies preconditions and the second component specifies effects (postconditions) of
applying the action to a given state. [Abdulaziz et al., Definition 2, p.9] ›

type_synonym ('a) state = "('a, bool) fmap"
type_synonym ('a) action = "('a state × 'a state)"
type_synonym ('a) problem = "('a state × 'a state) set"

text ‹ For a given action @{term "π = (p, e)"} the action domain @{term "𝒟(π)"} is the set of variables v where
a value is assigned to v in either p or e, i.e. p v or e v are defined. [Abdulaziz et al.,
Definition 2, p.9] ›
definition action_dom where
"action_dom s1 s2 ≡ (fmdom' s1 ∪ fmdom' s2)"

― ‹NOTE lemma action\_dom\_pair

action\_dom a = FDOM (FST a) Union ((SND a)  FDOM)

was removed because the curried definition of action\_dom in the translation makes it redundant.›

text ‹ Now, for a given problem (i.e. action set) @{term "δ"}, the problem domain @{term "𝒟(δ)"} is given by the
union of the action domains of all actions in @{term "δ"}. [Abdulaziz et al., Definition 3, p.9]

Moreover, the set of valid states @{term "U(δ)"} is given by the union over all states whose domain is equal
to the problem domain and the set of valid action sequences (or, valid plans) is given by the
Kleene closure of @{term "δ"}, i.e. @{term "δ_star = {π. set(π) ⊆ δ}"}. [Abdulaziz et al., Definition 3, p.9]

Ultimately, the effect of executing an action a on a state s is given by calculating the
succeding state. In general, the succeding state is either the preceding state---if the action does
not apply to the state, i.e. if the preconditions are not met---; or, the union of the effects of
the action application and the state. [Abdulaziz et al., Definition 3, p.9]
›

― ‹NOTE name shortened to 'prob\_dom'.›
― ‹NOTE lambda added to convert problem pairs to arguments of 'action\_dom'.›
definition prob_dom where
"prob_dom prob ≡ ⋃ ((λ (s1, s2). action_dom s1 s2)  prob)"

definition valid_states where
"valid_states prob ≡ {s. fmdom' s = prob_dom prob}"

definition valid_plans  where
"valid_plans prob ≡ {as. set as ⊆ prob}"

definition state_succ where
"state_succ s a ≡ (if fst a ⊆⇩f s then (snd a ++ s) else s)"

end

# Theory ListUtils

theory ListUtils
imports Main "HOL-Library.Sublist"
begin

― ‹TODO assure translations
* 'sublist' --> 'subseq'
* list\_frag l l' --> sublist l' l (switch operands!)›

lemma len_ge_0:
fixes l
shows "length l ≥ 0"
by simp

lemma len_gt_pref_is_pref:
fixes l l1 l2
assumes "(length l2 > length l1)" "(prefix l1 l)" "(prefix l2 l)"
shows "(prefix l1 l2)"
using assms proof (induction l2 arbitrary: l1 l)
case Nil
then have "¬(length [] > length l1)"
by simp
then show ?case
using Nil
by blast
next
case (Cons a l2)
then show ?case proof(induction l1 arbitrary: l)
case Nil
then show ?case
using Nil_prefix
by blast
next
case (Cons b l1)
then show ?case proof(cases l)
case Nil
then have "¬(prefix (a # l2) l)"
by simp
then show ?thesis using Cons.prems(4)
by simp
next
case (Cons c l)
then have 1: "length l2 > length l1"
using Cons.prems(2)
by fastforce
then show ?thesis using Cons proof(cases l)
case Nil
then have "l1 = [c]" "l2 = [c]"
using Cons.prems(3, 4) local.Cons 1
by fastforce+
then show ?thesis
using 1
by auto
next
case (Cons d l')
{
thm len_ge_0
have "length l1 ≥ 0"
by simp
then have "length l2 > 0"
using 1
by force
then have "l2 ≠ []" using 1
by blast
}
then have "length (a # l1) ≤ length (b # l2)"
using 1 le_eq_less_or_eq
by simp
then show ?thesis
using Cons.prems(3, 4) prefix_length_prefix
by fastforce
qed
qed
qed
qed

fixes l1 l2 l3
assumes "l2 ≠ []"
shows "length (l1 @ l3) < length (l1 @ l2 @l3)"
using assms
by (induction l2) auto

lemma append_filter:
fixes f1 :: "'a ⇒ bool" and f2 as1 as2 and p :: "'a list"
assumes "(as1 @ as2 = filter f1 (map f2 p))"
shows "(∃p_1 p_2.
(p_1 @ p_2 = p)
∧ (as1 = filter f1 (map f2 p_1))
∧ (as2 = filter f1 (map f2 p_2))
)"
using assms
proof (induction p arbitrary: f1 f2 as1 as2)
case Nil
from Nil have 1: "as1 @ as2 = []"
by force
then have 2: "as1 = []" "as2 = []"
by blast+
let ?p1="[]"
let ?p2="[]"
from 1 2
have "?p1 @ ?p2 = []" "as1 = (filter f1 (map f2 ?p1))" "as2 = (filter f1 (map f2 ?p2))"
subgoal by blast
subgoal using 2(1) by simp
subgoal using 2(2) by simp
done
then show ?case
by fast
next
case cons: (Cons a p)
then show ?case
proof (cases "as1")
case Nil
from cons.prems Nil
have 1: "as2 = filter f1 (map f2 (a # p))"
by simp
let ?p1="[]"
let ?p2="a # p"
have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)"
subgoal by simp
subgoal using Nil by simp
subgoal using 1 by auto
done
then show ?thesis
by blast
next
case (Cons a' p')
then show ?thesis
proof (cases "¬f1 (f2 a)")
case True
hence "filter f1 (map f2 (a # p)) = filter f1 (map f2 p)"
by fastforce
hence "as1 @ as2 = filter f1 (map f2 p)"
using cons.prems
by argo
then obtain p1 p2 where a:
"p1 @ p2 = p" "as1 = filter f1 (map f2 p1)" "as2 = filter f1 (map f2 p2)"
using cons.IH
by meson
let ?p1="a # p1"
let ?p2="p2"
have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)"
subgoal using a(1) by fastforce
subgoal using True a(2) by auto
subgoal using a(3) by blast
done
then show ?thesis
by blast
next
case False
hence "filter f1 (map f2 (a # p)) = f2 a # filter f1 (map f2 p)"
by fastforce
then have 1: "a' = f2 a" "p' @ as2 = filter f1 (map f2 p)" "as1 = a' # p'"
using cons.prems Cons
by fastforce+
then obtain p1 p2 where 2:
"p1 @ p2 = p" "p' = filter f1 (map f2 p1)" "as2 = filter f1 (map f2 p2)"
using cons.IH
by meson
let ?p1="a # p1"
let ?p2="p2"
have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)"
subgoal using 2(1) by simp
subgoal using False 1(1, 3) 2(2) by force
subgoal using 2(3) by blast
done
then show ?thesis
by blast
qed
qed
qed

― ‹NOTE types of f1 and p had to be fixed for append\_eq\_as\_proj\_1.›
lemma append_eq_as_proj_1:
fixes f1 :: "'a ⇒ bool" and f2 as1 as2 as3 and p :: "'a list"
assumes "(as1 @ as2 @ as3 = filter f1 (map f2  p))"
shows "(∃p_1 p_2 p_3.
(p_1 @ p_2 @ p_3 = p)
∧ (as1 = filter f1 (map f2 p_1))
∧ (as2 = filter f1 (map f2 p_2))
∧ (as3 = filter f1 (map f2 p_3))
)"
proof -
from assms
obtain p_1 p_2 where 1: "(p_1 @ p_2 = p)" "(as1 = filter f1 (map f2 p_1))"
"(as2 @ as3 = filter f1 (map f2 p_2))"
using append_filter[of as1 "(as2 @ as3)"]
by meson
moreover from 1
obtain p_a p_b where "(p_a @ p_b = p_2)" "(as2 = filter f1 (map f2 p_a))"
"(as3 = filter f1 (map f2 p_b))"
using append_filter[where p=p_2]
by meson
ultimately show ?thesis
by blast
qed

lemma filter_empty_every_not: "⋀P l. (filter (λx. P x) l = []) = list_all (λx. ¬P x) l"
proof -
fix P l
show "(filter (λx. P x) l = []) = list_all (λx. ¬P x) l"
apply(induction l)
apply(auto)
done
qed

lemma MEM_SPLIT:
fixes x l
assumes "¬ListMem x l"
shows "∀l1 l2. l ≠ l1 @ [x] @ l2"
proof -
{
assume C: "¬(∀l1 l2. l ≠ l1 @ [x] @ l2)"
then have "∃l1 l2. l = l1 @ [x] @ l2"
by blast
then obtain l1 l2 where 1: "l = l1 @ [x] @ l2"
by blast
from assms
have 2: "(∀xs. l ≠ x # xs) ∧ (∀xs. (∀y. l ≠ y # xs) ∨ ¬ ListMem x xs)"
using ListMem_iff
by fastforce
then have False
proof (cases l1)
case Nil
let ?xs="l2"
from 1 Nil have "l = [x] @ ?xs"
by blast
then show ?thesis
using 2
by simp
next
case (Cons a list)
{
let ?y="a"
let ?xs="list @ [x] @ l2"
from 1 Cons have "l = ?y # ?xs"
by simp
moreover have "ListMem x ?xs"
ultimately have "∃xs. ∃y. l = y # xs ∧ ListMem x xs"
by blast
then have "¬(∀xs. (∀y. l ≠ y # xs) ∨ ¬ ListMem x xs)"
by presburger
}
then show ?thesis
using 2
by auto
qed
}
then show ?thesis
by blast
qed

lemma APPEND_EQ_APPEND_MID:
fixes l1 l2 m1 m2 e
shows
"(l1 @ [e] @ l2 = m1 @ m2)
⟷
(∃l. (m1 = l1 @ [e] @ l) ∧ (l2 = l @ m2)) ∨
(∃l. (l1 = m1 @ l) ∧ (m2 = l @ [e] @ l2))"
proof (induction "l1" arbitrary: m1)
case Nil
then show ?case
by (simp; metis Cons_eq_append_conv)+
next
case (Cons a l1)
then show ?case
by (cases m1; simp; blast)
qed

― ‹NOTE variable P was removed (redundant).›
lemma LIST_FRAG_DICHOTOMY:
fixes l la x lb
assumes "sublist l (la @ [x] @ lb)" "¬ListMem x l"
shows "sublist l la ∨ sublist l lb"
proof -
{
from assms(1)
obtain pfx sfx where 1: "pfx @ l @ sfx = la @ [x] @ lb"
unfolding sublist_def
by force
from assms(2)
have 2: "∀l1 l2. l ≠ l1 @ [x] @ l2"
using MEM_SPLIT[OF assms(2)]
by blast
from 1
consider (a) "(∃lc. pfx = la @ [x] @ lc ∧ lb = lc @ l @ sfx)"
| (b) "(∃lc. la = pfx @ lc ∧ l @ sfx = lc @ [x] @ lb)"
using APPEND_EQ_APPEND_MID[of la x lb pfx "l @ sfx"]
by presburger
then have "∃pfx' sfx. (pfx' @ l @ sfx = la) ∨ (pfx'@  l @ sfx = lb)"
proof (cases)
case a
― ‹NOTE lc is l' in original proof.›
then obtain lc where a: "pfx = la @ [x] @ lc" "lb = lc @ l @ sfx"
by blast
then show ?thesis
by blast
next
case b
then obtain lc where i: "la = pfx @ lc" "l @ sfx = lc @ [x] @ lb"
by blast
then show ?thesis
using 2
by (metis APPEND_EQ_APPEND_MID)
qed
}
then show ?thesis
unfolding sublist_def
by blast
qed

lemma LIST_FRAG_DICHOTOMY_2:
fixes l la x lb P
assumes "sublist l (la @ [x] @ lb) " "¬P x" "list_all P l"
shows "sublist l la ∨ sublist l lb"
proof -
{
assume "¬P x" "list_all P l"
then have "¬ListMem x l"
proof (induction l arbitrary: x P)
case Nil
then show ?case
using ListMem_iff
by force
next
case (Cons a l)
{
have "list_all P l"
using Cons.prems(2)
by simp
then have "¬ListMem x l"
using Cons.prems(1) Cons.IH
by blast
}
moreover {
have "P a"
using Cons.prems(2)
by simp
then  have "a ≠ x"
using Cons.prems(1)
by meson
}
ultimately show ?case
using Cons.prems(1, 2) ListMem_iff list.pred_set
by metis
qed
}
then have "¬ListMem x l"
using assms(2, 3)
by fast
then show ?thesis
using assms(1) LIST_FRAG_DICHOTOMY
by metis
qed

lemma frag_len_filter_le:
fixes P l' l
assumes "sublist l' l"
shows "length (filter P l') ≤ length (filter P l)"
proof -
obtain ps ss where "l = ps @ l' @ ss"
using assms sublist_def
by blast
then have 1:
"length (filter P l) = length (filter P ps) + length (filter P l') + length (filter P ss)"
by force
then have "length (filter P ps) ≥ 0" "length (filter P ss) ≥ 0"
by blast+
then show ?thesis
using 1
by linarith
qed

end

# Theory FSSublist

(*
* cf. planning/hol/sublistScript
*)
theory FSSublist
imports Main "HOL-Library.Sublist" ListUtils
begin

text ‹ This file is a port of the original HOL4 source file sublistScript.sml. ›

section "Factored System Sublist"
subsection "Sublist Characterization"

text ‹ We take a look at the characterization of sublists. As a precursor, we are replacing the
original definition of sublist in HOL4 (sublistScript.sml:10) with the semantically equivalent
subseq of Isabelle/HOL's to be able to use the associated theorems and automation.

In HOL4 sublist is defined as

(sublist [] l1 = T) /\
(sublist (h::t) [] = F) /\
(sublist (x::l1) (y::l2) = (x = y) /\ sublist l1 l2 \/ sublist (x::l1) l2)

[Abdulaziz et al., HOL4 Definition 10, p.19]. Whereas subseq (Sublist.tyh:927) is defined as an
abbrevation of list\_emb with the predicate @{term "λ x y. x = y"}, i.e.

@{term "subseq xs ys ≡ list_emb (=) xs ys"}

list\_emb itself is defined as an inductive predicate. However, an equivalent function definition
is provided in list\_emb\_code (Sublist.thy:784) which is very close to sublist in HOL4.

The correctness of the equivalence claim is shown below by the technical lemma
sublist\_HOL4\_equiv\_subseq (where the HOL4 definition of sublist is renamed to sublist\_HOL4).
›

fun sublist_HOL4 where
"sublist_HOL4 [] l1 = True"
| "(sublist_HOL4 (h # t) [] = False)"
| "(sublist_HOL4 (x # l1) (y # l2) = ((x = y) ∧ sublist_HOL4 l1 l2 ∨ sublist_HOL4 (x # l1) l2))"

lemma sublist_HOL4_equiv_subseq:
fixes l1 l2
shows "sublist_HOL4 l1 l2 ⟷ subseq l1 l2"
proof -
have "subseq l1 l2 = list_emb (λx y. x = y) l1 l2"
by blast
moreover {
have "sublist_HOL4 l1 l2 ⟷ list_emb (λx y. x = y) l1 l2"
proof (induction rule: sublist_HOL4.induct)
case (3 x l1 y l2)
then show "sublist_HOL4 (x # l1) (y # l2) ⟷ list_emb (λx y. x = y) (x # l1) (y # l2)"
proof (cases "x = y")
case True
then show ?thesis
using "3.IH"(1, 2)
by (metis sublist_HOL4.simps(3) subseq_Cons' subseq_Cons2_iff)
next
case False
then show ?thesis
using "3.IH"(2)
by force
qed
qed simp+
}
ultimately show ?thesis
by blast
qed

text ‹ Likewise as with sublist and subseq, the HOL4 definition of list\_frag
(list\_utilsScript.sml:207) has a an Isabelle/HOL counterpart in sublist (Sublist.thy:1124).

The equivalence claim is proven in the technical lemma list\_frag\_HOL4\_equiv\_sublist. Note that
sublist reverses the argument order of list\_frag. Other than that, both definitions are
syntactically identical. ›
definition list_frag_HOL4 where
"list_frag_HOL4 l frag ≡ ∃pfx sfx. pfx @ frag @ sfx = l"

lemma list_frag_HOL4_equiv_sublist:
shows "list_frag_HOL4 l l' ⟷ sublist l' l"
unfolding list_frag_HOL4_def sublist_def
by blast

text ‹ Given these equivalences, occurences of sublist and list\_frag in the original HOL4
source are now always translated directly to subseq and sublist respectively.

The remainer of this subsection is concerned with characterizations of sublist/ subseq. ›

lemma sublist_EQNS:
"subseq [] l = True"
"subseq (h # t) [] = False"
by auto

lemma sublist_refl: "subseq l l"
by auto

lemma sublist_cons:
assumes "subseq l1 l2"
shows "subseq l1 (h # l2)"
using assms
by blast

lemma sublist_NIL: "subseq l1 [] = (l1 = [])"
by fastforce

lemma sublist_trans:
fixes l1 l2
assumes "subseq l1 l2" "subseq l2 l3"
shows "subseq l1 l3"
using assms
by force

― ‹NOTE can be solved directly with 'list\_emb\_length'.›
lemma sublist_length:
fixes l l'
assumes "subseq l l'"
shows "length l ≤ length l'"
using assms list_emb_length
by blast

― ‹NOTE can be solved directly with subseq\_Cons'.›
lemma sublist_CONS1_E:
fixes l1 l2
assumes "subseq (h # l1) l2"
shows "subseq l1 l2"
using assms subseq_Cons'
by metis

lemma sublist_equal_lengths:
fixes l1 l2
assumes "subseq l1 l2" "(length l1 = length l2)"
shows "(l1 = l2)"
using assms subseq_same_length
by blast

― ‹NOTE can be solved directly with 'subseq\_order.antisym'.›
lemma sublist_antisym:
assumes "subseq l1 l2" "subseq l2 l1"
shows "(l1 = l2)"
using assms subseq_order.antisym
by blast

lemma sublist_append_back:
fixes l1 l2
shows "subseq l1 (l2 @ l1)"
by blast

― ‹NOTE can be solved directly with 'subseq\_rev\_drop\_many'.›
lemma sublist_snoc:
fixes l1 l2
assumes "subseq l1 l2"
shows "subseq l1 (l2 @ [h])"
using assms subseq_rev_drop_many
by blast

lemma sublist_append_front:
fixes l1 l2
shows "subseq l1 (l1 @ l2)"
by fast

lemma append_sublist_1:
assumes "subseq (l1 @ l2) l"
shows "subseq l1 l ∧ subseq l2 l"
using assms sublist_append_back sublist_append_front sublist_trans
by blast

― ‹NOTE added lemma (eventually wasn't needed in the remaining proofs).›
lemma sublist_prefix:
shows "subseq (h # l1) l2 ⟹ ∃l2a l2b. l2 = l2a @ [h] @ l2b ∧ ¬ListMem h l2a"
proof (induction l2 arbitrary: h l1)
― ‹NOTE l2 cannot be empty when @{term "(h # l1)"} isn't.›
case Nil
have "¬(subseq (h # l1) [])"
by simp
then show ?case
using Nil.prems
by blast
next
case (Cons a l2)
then show ?case proof (cases "a = h")
― ‹NOTE If a = h then a trivial solution exists in l2a = [] and l2b = l2.›
case True
then show "∃ l2a l2b. (Cons a l2) = l2a @ [h] @ l2b ∧ ¬ListMem h l2a"
using ListMem_iff
by force
next
case False
have "subseq (h # l1) l2"
using Cons.prems False subseq_Cons2_neq
by force
then obtain l2a l2b where "l2 = l2a @ [h] @ l2b" "¬ListMem h l2a"
using Cons.IH Cons.prems
by meson
moreover have "a # l2 = (a # l2a) @ [h] @ l2b"
using calculation(1)
by simp
moreover have "¬(ListMem h (a # l2a))"
using False calculation(2) ListMem.simps
by fastforce
ultimately show ?thesis
by blast
qed
qed

― ‹NOTE added lemma (eventually wasn't needed in the remaining proofs).›
lemma sublist_skip:
fixes l1 l2 h l1'
assumes "l1 = (h # l1')" "l2 = l2a @ [h] @ l2b" "subseq l1 l2" "¬(ListMem h l2a)"
shows "subseq l1 (h # l2b)"
using assms
proof (induction l2a arbitrary: l1 l2 h l1')
case Nil
then have "l2 = h # l2b"
by fastforce
then show ?case using Nil.prems(3)
by blast
next
case (Cons a l2a)
have "a ≠ h"
using Cons.prems(4) ListMem.simps
by fast
then have "subseq l1 (l2a @ [h] @ l2b)"
using Cons.prems(1, 2, 3) subseq_Cons2_neq
by force
moreover have "¬ListMem h l2a"
using Cons.prems(4) insert
by metis
ultimately have "subseq l1 (h # l2b)"
using Cons.IH Cons.prems
by meson
then show ?case
by simp
qed

― ‹NOTE added lemma (eventually wasn't needed in the remaining proofs).›
lemma sublist_split_trans:
fixes l1 l2 h l1'
assumes "l1 = (h # l1')" "l2 = l2a @ [h] @ l2b" "subseq l1 l2" "¬(ListMem h l2a)"
shows "subseq l1' l2b"
proof -
have "subseq (h # l1') (h # l2b)"
using assms sublist_skip
by metis
then show ?thesis
using subseq_Cons2'
by metis
qed

lemma sublist_cons_exists:
shows "
subseq (h # l1) l2
⟷ (∃l2a l2b. (l2 = l2a @ [h] @ l2b) ∧ ¬ListMem h l2a ∧ subseq l1 l2b)
"
proof -
― ‹NOTE show both directions of the equivalence in pure proof blocks.›
{
have
"subseq (h # l1) l2 ⟹ (∃l2a l2b. (l2 = l2a @ [h] @ l2b) ∧ ¬ListMem h l2a ∧ subseq l1 l2b)"
proof (induction l2 arbitrary: h l1)
case (Cons a l2)
show ?case
proof (cases "a = h")
case True
― ‹NOTE This case has a trivial solution in '?l2a = []', '?l2b = l2'.›
let ?l2a="[]"
have "(a # l2) = ?l2a @ [h] @ l2"
using True
by auto
moreover have "¬(ListMem h ?l2a)"
using ListMem_iff
by force
moreover have "subseq l1 l2"
using Cons.prems True
by simp
ultimately show ?thesis
by blast
next
case False
have 1: "subseq (h # l1) l2"
using Cons.prems False subseq_Cons2_neq
by metis
then obtain l2a l2b where "l2 = l2a @ [h] @ l2b" "¬ListMem h l2a"
using Cons.IH Cons.prems
by meson
moreover have "a # l2 = (a # l2a) @ [h] @ l2b"
using calculation(1)
by simp
moreover have "¬(ListMem h (a # l2a))"
using False calculation(2) ListMem.simps
by fastforce
ultimately show ?thesis
using 1 sublist_split_trans
by metis
qed
qed simp
}
moreover
{
assume "∃l2a l2b. (l2 = l2a @ [h] @ l2b) ∧ ¬ListMem h l2a ∧ subseq l1 l2b"
then have  "subseq (h # l1) l2"
by auto
}
ultimately show ?thesis
by argo
qed

lemma sublist_append_exists:
fixes l1 l2
shows "subseq (l1 @ l2) l3 ⟹ ∃l3a l3b. (l3 = l3a @ l3b) ∧ subseq l1 l3a ∧ subseq l2 l3b"
using list_emb_appendD
by fast

― ‹NOTE can be solved directly with 'list\_emb\_append\_mono'.›
lemma sublist_append_both_I:
assumes "subseq a b" "subseq c d"
shows "subseq (a @ c) (b @ d)"
using assms list_emb_append_mono
by blast

lemma sublist_append:
assumes "subseq l1 l1'" "subseq l2 l2'"
shows "subseq (l1 @ l2) (l1' @ l2')"
using assms sublist_append_both_I
by blast

lemma sublist_append2:
assumes "subseq l1 l2"
shows "subseq l1 (l2 @ l3)"
using assms sublist_append[of "l1" "l2" "[]" "l3"]
by fast

lemma append_sublist:
shows "subseq (l1 @ l2 @ l3) l ⟹ subseq (l1 @ l3) l"
proof (induction l)
case Nil
then show ?case
using sublist_NIL
by fastforce
next
case (Cons a l)
then show ?case
proof (cases l1)
case Nil
then show ?thesis
using Cons.prems append_sublist_1
by auto
next
case (Cons a list)
then show ?thesis
using Cons.prems subseq_append' subseq_order.dual_order.trans
by blast
qed
qed

lemma sublist_subset:
assumes "subseq l1 l2"
shows "set l1 ⊆ set l2"
using assms set_nths_subset subseq_conv_nths
by metis

lemma sublist_filter:
fixes P l
shows "subseq (filter P l) l"
using subseq_filter_left
by blast

lemma sublist_cons_2:
fixes l1 l2 h
shows "(subseq (h # l1) (h # l2) ⟷ (subseq l1 l2))"
by fastforce

lemma sublist_every:
fixes l1 l2 P
assumes "(subseq l1 l2 ∧ list_all P l2)"
shows "list_all P l1"
by (metis (full_types) Ball_set assms list_emb_set)

lemma sublist_SING_MEM: "subseq [h] l ⟷ ListMem h l"
using ListMem_iff subseq_singleton_left
by metis

― ‹NOTE renamed due to previous declaration of sublist\_append\_exists\_2.›
lemma sublist_append_exists_2:
fixes l1 l2 l3
assumes "subseq (h # l1) l2"
shows "(∃l3 l4. (l2 = l3 @ [h] @ l4) ∧ (subseq l1 l4))"
using assms sublist_cons_exists
by metis

lemma sublist_append_4:
fixes l l1 l2 h
assumes "(subseq (h # l) (l1 @ [h] @ l2))" "(list_all (λx. ¬(h = x)) l1)"
shows "subseq l l2"
using assms
proof (induction l1)
qed auto

lemma sublist_append_5:
fixes l l1 l2 h
assumes "(subseq (h # l) (l1 @ l2))" "(list_all (λx. ¬(h = x)) l1)"
shows "subseq (h # l) l2"
using assms
proof (induction l1)
qed auto

lemma sublist_append_6:
fixes l l1 l2 h
assumes "(subseq (h # l) (l1 @ l2))" "(¬(ListMem h l1))"
shows "subseq (h # l) l2"
using assms
proof (induction l1)
case (Cons a l1)
then show ?case
qed simp

lemma sublist_MEM:
fixes h l1 l2
shows "subseq (h # l1) l2 ⟹ ListMem h l2"
proof (induction l2)
next
case (Cons a l2)
then show ?case
using elem insert subseq_Cons2_neq
by metis
qed simp

lemma sublist_cons_4:
fixes l h l'
shows "subseq l l' ⟹ subseq l (h # l')"
using sublist_cons
by blast

subsection "Main Theorems"

theorem sublist_imp_len_filter_le:
fixes P l l'
assumes "subseq l' l"
shows "length (filter P l') ≤ length (filter P l)"
using assms

― ‹TODO showcase (non-trivial proof translation/ obscurity).›
theorem list_with_three_types_shorten_type2:
fixes P1 P2 P3 k1 f PProbs PProbl s l
assumes "(PProbs s)" "(PProbl l)"
"(∀l s.
(PProbs s)
∧ (PProbl l)
∧ (list_all P1 l)
⟶ (∃l'.
(f s l' = f s l)
∧ (length (filter P2 l') ≤ k1)
∧ (length (filter P3 l') ≤ length (filter P3 l))
∧ (list_all P1 l')
∧ (subseq l' l)
)
)"
"(∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2))"
"(∀s l. (PProbs s) ∧ (PProbl l) ⟶ (PProbs (f s l)))"
"(∀l1 l2. (subseq l1 l2) ∧ (PProbl l2) ⟶ (PProbl l1))"
"(∀l1 l2. PProbl (l1 @ l2) ⟷ (PProbl l1 ∧ PProbl l2))"
shows "(∃l'.
(f s l' = f s l)
∧ (length (filter P3 l') ≤ length (filter P3 l))
∧ (∀l''.
(sublist l'' l') ∧ (list_all P1 l'')
⟶ (length (filter P2 l'') ≤ k1)
)
∧ (subseq l' l)
)"
using assms
proof (induction "filter (λx. ¬P1 x) l" arbitrary: P1 P2 P3 k1 f PProbs PProbl s l)
case Nil
then have "list_all (λx. P1 x) l"
using Nil(1) filter_empty_every_not[of "λx. ¬P1 x" l]
by presburger
then obtain l' where 1:
"(f s l' = f s l)" "length (filter P2 l') ≤ k1" "length (filter P3 l') ≤ length (filter P3 l)"
"list_all P1 l'" "subseq l' l"
using Nil.prems(1, 2, 3)
by blast
moreover {
fix l''
assume "sublist l'' l'" "list_all P1 l''"
then have "subseq l'' l'"
by blast
― ‹NOTE original proof uses frag\_len\_filter\_le which however requires the fact
sublist l' ?l. Unfortunately, this could not be derived in Isabelle/HOL.›
then have "length (filter P2 l'') ≤ length (filter P2 l')"
using sublist_imp_len_filter_le
by blast
then have "length (filter P2 l'') ≤ k1"
using 1
by linarith
}
ultimately show ?case
by blast
next
case (Cons a x)
― ‹NOTE The proof of the induction step basically consists of construction a list
?l'=l'' @ [a] @ l''' where l'' and l''' are lists obtained from certain specifications
of the induction hypothesis.›
then obtain l1 l2 where 2:
"l = l1 @ a # l2" "(∀u∈set l1. P1 u)" "¬ P1 a ∧ x = [x←l2 . ¬ P1 x]"
using Cons(2) filter_eq_Cons_iff[of "λx. ¬P1 x"]
by metis
then have 3: "PProbl l2"
using Cons.prems(2, 6) 2(1) sublist_append_back
by blast
― ‹NOTE Use the induction hypothesis to obtain a specific  l'''.›
{
have "x = filter (λx. ¬P1 x) l2"
using 2(3)
by blast
moreover have "PProbs (f (f s l1) [a])"
using Cons.prems(1, 2, 5, 6, 7) 2(1) elem sublist_SING_MEM
by metis
moreover have "∀l s. PProbs s ∧ PProbl l ∧ list_all P1 l ⟶ (∃l'.
f s l' = f s l ∧ length (filter P2 l') ≤ k1 ∧ length (filter P3 l') ≤ length (filter P3 l)
∧ list_all P1 l' ∧ subseq l' l)"
using Cons.prems(3)
by blast
moreover have "∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2)"
"∀s l. PProbs s ∧ PProbl l ⟶ PProbs (f s l)"
"∀l1 l2. subseq l1 l2 ∧ PProbl l2 ⟶ PProbl l1"
"∀l1 l2. PProbl (l1 @ l2) = (PProbl l1 ∧ PProbl l2)"
using Cons.prems(4, 5, 6, 7)
by blast+
ultimately have "∃l'.
f (f (f s l1) [a]) l' = f (f (f s l1) [a]) l2 ∧ length (filter P3 l') ≤ length (filter P3 l2)
∧ (∀l''. sublist l'' l' ∧ list_all P1 l'' ⟶ length (filter P2 l'') ≤ k1) ∧ subseq l' l2"
using 3 Cons(1)[of P1 l2, where s="(f (f s l1) [a])"]
by blast
}
then obtain l''' where 4:
"f (f (f s l1) [a]) l''' = f (f (f s l1) [a]) l2"
"length (filter P3 l''') ≤ length (filter P3 l2)"
"(∀l''. sublist l'' l''' ∧ list_all P1 l'' ⟶ length (filter P2 l'') ≤ k1) ∧ subseq l''' l2"
by blast
then have "f s (l1 @ [a] @ l''') = f s (l1 @ [a] @ l2)"
using Cons.prems(4)
by auto
then have "subseq l''' l2"
using 4(3)
by blast
― ‹NOTE Use the induction hypothesis to obtain a specific  l''.›
{
have "∀l s.
PProbs s ∧ PProbl l1 ∧ list_all P1 l1
⟶ (∃l''.
f s l'' = f s l1 ∧ length (filter P2 l'') ≤ k1 ∧ length (filter P3 l'') ≤ length (filter P3 l1)
∧ list_all P1 l'' ∧ subseq l'' l1)"
using Cons.prems(3)
by blast
then have "∃l''.
f s l'' = f s l1 ∧ length (filter P2 l'') ≤ k1 ∧ length (filter P3 l'') ≤ length (filter P3 l1)
∧ list_all P1 l'' ∧ subseq l'' l1"
using Cons.prems(1, 2, 7) 2(1, 2)
by (metis Ball_set)
}

then obtain l'' where 5:
"f s l'' = f s l1" "length (filter P2 l'') ≤ k1"
"length (filter P3 l'') ≤ length (filter P3 l1)" "list_all P1 l'' ∧ subseq l'' l1"
by blast
text ‹ Proof the proposition by providing the witness @{term "l'=(l'' @ [a] @ l''')"}. ›
let ?l'="(l'' @ [a] @ l''') "
{
have "∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2)"
text ‹ Rewrite and show the goal.›
have "f s ?l' = f s (l1 @ [a] @ l2) ⟷ f s (l'' @ (a # l''')) = f s (l1 @ (a # l2))"
by simp
also have "… ⟷ f (f (f s l1) [a]) l''' = f (f (f s l1) [a]) l2"
by (metis Cons.prems(4) ‹f s l'' = f s l1› calculation)
finally have "f s ?l' = f s (l1 @ [a] @ l2)"
using 4(1)
by blast
}
moreover
{
have "
length (filter P3 ?l') ≤ length (filter P3 (l1 @ [a] @ l2))
⟷
(length (filter P3 l'') + 1 + length (filter P3 l''')
≤ length (filter P3 l1) + 1 + length (filter P3 l2))"
by force
then have "
length (filter P3 ?l') ≤ length (filter P3 (l1 @ [a] @ l2))
⟷
length (filter P3 l'') + length (filter P3 l''')
≤ length (filter P3 l1) + length (filter P3 l2)"
by linarith
then have "length (filter P3 ?l') ≤ length (filter P3 (l1 @ [a] @ l2))"
using 4(2) ‹length (filter P3 l'') ≤ length (filter P3 l1)›
by blast
}
moreover
{
fix l''''
assume P: "sublist l'''' ?l'" "list_all P1 l''''"
have "list_all P1 l1"
using 2(2) Ball_set
by blast
consider (i) "sublist l'''' l''" | (ii) "sublist l'''' l'''"
using P(1, 2) 2(3)  LIST_FRAG_DICHOTOMY_2
by metis
then have "length (filter P2 l'''') ≤ k1"
proof (cases)
case i
then have "length (filter P2 l'''') ≤ length (filter P2 l'')"
using frag_len_filter_le
by blast
then show ?thesis
using 5(2) order_trans
by blast
next
case ii
then show ?thesis
using 4(3) P(2)
by blast
qed
}
― ‹NOTE the following two steps seem to be necessary to convince Isabelle that the split
@{term "l = l1 @ a # l2"} matches the split (l1 @ [a] @ l2 and the previous proof steps therefore is
prove the goal.›
moreover {
have "subseq ?l' (l1 @ [a] @ l2)"
by (simp add: FSSublist.sublist_append ‹list_all P1 l'' ∧ subseq l'' l1› ‹subseq l''' l2›)
}
moreover have "l = l1 @ [a] @ l2"
using 2
by force
ultimately show ?case
by blast
qed

lemma isPREFIX_sublist:
fixes x y
assumes "prefix x y"
shows "subseq x y"
using assms prefix_order.dual_order.antisym
by blast

end

# Theory HoArithUtils

theory HoArithUtils
imports Main
begin

lemma general_theorem:
fixes P f and l :: nat
assumes "(∀p. P p ∧ f p > l ⟶ (∃p'. P p' ∧ f p' < f p))"
shows "(∀p. P p ⟶ (∃p'. P p' ∧ f p' ≤ l))"
proof-
have "∀p. (n = f p) ∧ P p ⟶ (∃p'. P p' ∧ f p' ≤ l)" for n
apply(rule Nat.nat_less_induct[where ?P = "%n. ∀p. (n = f p) ∧ P p ⟶ (∃p'. P p' ∧ f p' ≤ l)"])
by (metis assms not_less)
then show ?thesis by auto
qed

end

# Theory FmapUtils

theory FmapUtils
imports "HOL-Library.Finite_Map" FactoredSystemLib
begin

― ‹TODO
A lemma 'fmrestrict\_set\_twice\_eq'
'fmrestrict\_set ?vs (fmrestrict\_set ?vs ?f) = fmrestrict\_set ?vs ?f'
to replace the recurring proofs steps using 'by (simp add: fmfilter\_alt\_defs(4))' would make sense.›

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

― ‹TODO more explicit proof.›
lemma IN_FDOM_DRESTRICT_DIFF:
fixes vs v f
assumes "¬(v ∈ vs)" "fmdom' f ⊆ fdom" "v ∈ fmdom' f"
shows "v ∈ fmdom' (fmrestrict_set (fdom - vs) f)"
using assms
by (metis DiffI Int_def Int_iff Set.filter_def fmdom'_filter fmfilter_alt_defs(4) inf.order_iff)

lemma disj_dom_drest_fupdate_eq: "
disjnt (fmdom' x) vs ⟹ (fmrestrict_set vs s = fmrestrict_set vs (x ++ s))
"
proof -
fix vs s x
assume P: "disjnt (fmdom' x) vs"
moreover have 1: "∀x''. (x'' ∈ vs) ⟶ (fmlookup (x ++ s) x'' = fmlookup s  x'')"
moreover
{
fix x''
have "fmlookup (fmrestrict_set vs s) x'' = fmlookup (fmrestrict_set vs (x ++ s)) x''"
apply(cases "x'' ∉ fmdom' x")
apply(cases "x'' ∉ vs")
done
}
ultimately show "(fmrestrict_set vs s = fmrestrict_set vs (x ++ s))"
using fmap_ext by blast
qed

― ‹TODO refactor into 'FmapUtils.thy'.›
lemma graph_plan_card_state_set:
fixes PROB vs
assumes "finite vs"
shows "card (fmdom' (fmrestrict_set vs s)) ≤ card vs"
proof -
let ?vs' = "fmdom' (fmrestrict_set vs s)"
have "?vs' ⊆ vs"
using fmdom'_restrict_set
by metis
moreover have "card ?vs' ≤ card vs"
using assms calculation card_mono
by blast
ultimately show ?thesis by blast
qed

lemma exec_drest_5:
fixes x vs
assumes "fmdom' x ⊆ vs"
shows "(fmrestrict_set vs x = x)"
proof -
― ‹TODO refactor and make into ISAR proof.›
{
fix v
have "fmlookup (fmrestrict_set vs x) v = fmlookup x v"
apply(cases "v ∈ fmdom' x")
subgoal using assms by auto
done
then have "fmlookup (fmrestrict_set vs x) v = fmlookup x v"
by fast
}
moreover have "fmlookup (fmrestrict_set vs x) = fmlookup x"
using calculation fmap_ext
by auto
ultimately show ?thesis
using fmlookup_inject
by blast
qed

lemma graph_plan_lemma_5:
fixes s s' vs
assumes "(fmrestrict_set (fmdom' s - vs) s = fmrestrict_set (fmdom' s' - vs) s')"
"(fmrestrict_set vs s = fmrestrict_set vs s')"
shows "(s = s')"
proof -
have "∀x. fmlookup s x = fmlookup s' x"
using assms(1, 2) fmdom'_notD fminusI fmlookup_restrict_set Diff_iff
by metis
then show ?thesis using fmap_ext
by blast
qed

lemma drest_smap_drest_smap_drest:
fixes x s vs
shows "fmrestrict_set vs x ⊆⇩f s ⟷ fmrestrict_set vs x ⊆⇩f fmrestrict_set vs s"
proof -
― ‹TODO this could be refactored into standalone lemma since it's very common in proofs.›
have 1: "fmlookup (fmrestrict_set vs s) ⊆⇩m fmlookup s"
by (metis fmdom'.rep_eq fmdom'_notI fmlookup_restrict_set map_le_def)
moreover
{
assume P1: "fmrestrict_set vs x ⊆⇩f s"
moreover have 2: "fmlookup (fmrestrict_set vs x) ⊆⇩m fmlookup s"
using P1 fmsubset.rep_eq by blast
{
fix v
assume "v ∈ fmdom' (fmrestrict_set vs x)"
then have "fmlookup (fmrestrict_set vs x) v = fmlookup (fmrestrict_set vs s) v"
by (metis (full_types) "2" domIff fmdom'_notI fmlookup_restrict_set map_le_def)
}
ultimately have "fmrestrict_set vs x ⊆⇩f fmrestrict_set vs s"
unfolding fmsubset.rep_eq
}
moreover
{
assume P2: "fmrestrict_set vs x ⊆⇩f fmrestrict_set vs s"
moreover have "fmrestrict_set vs s ⊆⇩f s"
using 1 fmsubset.rep_eq
by blast
ultimately have "fmrestrict_set vs x ⊆⇩f s"
using fmsubset.rep_eq map_le_trans
by blast
}
ultimately show ?thesis by blast
qed

lemma sat_precond_as_proj_1:
fixes s s' vs x
assumes "fmrestrict_set vs s = fmrestrict_set vs s'"
shows "fmrestrict_set vs x ⊆⇩f s ⟷ fmrestrict_set vs x ⊆⇩f s'"
using assms drest_smap_drest_smap_drest
by metis

lemma sat_precond_as_proj_4:
fixes fm1 fm2 vs
assumes "fm2 ⊆⇩f fm1"
shows "(fmrestrict_set vs fm2 ⊆⇩f fm1)"
using assms fmpred_restrict_set fmsubset_alt_def
by metis

lemma sublist_as_proj_eq_as_1:
fixes x s vs
assumes "(x ⊆⇩f fmrestrict_set vs s)"
shows "(x ⊆⇩f s)"
using assms
by (meson fmsubset.rep_eq fmsubset_alt_def fmsubset_pred drest_smap_drest_smap_drest map_le_refl)

lemma limited_dom_neq_restricted_neq:
assumes "fmdom' f1 ⊆ vs" "f1 ++ f2 ≠ f2"
shows "fmrestrict_set vs (f1 ++ f2) ≠ fmrestrict_set vs f2"
proof -
{
assume C: "fmrestrict_set vs (f1 ++ f2) = fmrestrict_set vs f2"
then have "∀x ∈ fmdom' (fmrestrict_set vs (f1 ++ f2)).
fmlookup (fmrestrict_set vs (f1 ++ f2)) x
= fmlookup (fmrestrict_set vs f2) x"
by simp
obtain v where a: "v ∈ fmdom' f1" "fmlookup (f1 ++ f2) v ≠ fmlookup f2 v"
using assms(2)
then have b: "v ∈ vs"
using assms(1)
by blast
moreover {
have "fmdom' (fmrestrict_set vs (f1 ++ f2)) = vs ∩ fmdom' (f1 ++ f2)"
then have "v ∈ fmdom' (fmrestrict_set vs (f1 ++ f2))"
using C a b
by fastforce
}
then have False
by (metis C a(2) calculation fmlookup_restrict_set)
}
then show ?thesis
by auto
qed

lemma fmlookup_fmrestrict_set_dom: "⋀vs s. dom (fmlookup (fmrestrict_set vs s)) = vs ∩ (fmdom' s)"

end

# 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)"
proof -
have 1: "state_succ s1 a = (snd a ++ s1)"
using assms(1)
then have "fst a ⊆⇩f s2"
using assms(1, 2) submap_imp_state_succ_submap_a
by auto
then have 2: "state_succ s2 a = (snd a ++ s2)"
using 1 state_succ_def
by metis
then have "snd a ++ s1 ⊆⇩f snd a ++ s2"
using assms(2) submap_imp_state_succ_submap_b
by fast
then show ?thesis
using 1 2
by argo
qed

― ‹NOTE types for a, s1 and s2 had to be fixed (type mismatch in goal).›
lemma pred_dom_subset_succ_submap:
fixes a :: "'a action" and s1 s2 :: "'a state"
assumes "(fmdom' (fst a) ⊆ fmdom' s1)" "(s1 ⊆⇩f s2)"
shows "(state_succ s1 a ⊆⇩f state_succ s2 a)"
using assms
unfolding state_succ_def
proof (auto)
assume P1: "fmdom' (fst a) ⊆ fmdom' s1" "s1 ⊆⇩f s2" "fst a ⊆⇩f s1" "fst a ⊆⇩f s2"
then show "snd a ++ s1 ⊆⇩f snd a ++ s2"
using submap_imp_state_succ_submap_b
by fast
next
assume P2: "fmdom' (fst a) ⊆ fmdom' s1" "s1 ⊆⇩f s2" "fst a ⊆⇩f s1" "¬ fst a ⊆⇩f s2"
then show "snd a ++ s1 ⊆⇩f s2"
using submap_imp_state_succ_submap_a
by blast
next
assume P3: "fmdom' (fst a) ⊆ fmdom' s1" "s1 ⊆⇩f s2" "¬ fst a ⊆⇩f s1" "fst a ⊆⇩f s2"
{
have a: "fmlookup s1 ⊆⇩m fmlookup s2"
using P3(2) fmsubset.rep_eq
by blast
{
have "¬(fmlookup (fst a) ⊆⇩m fmlookup s1)"
using P3(3) fmsubset.rep_eq
by blast
then have "∃v ∈ dom (fmlookup (fst a)). fmlookup (fst a) v ≠ fmlookup s1 v"
using map_le_def
by fast
}
then obtain v where b: "v ∈ dom (fmlookup (fst a))" "fmlookup (fst a) v ≠ fmlookup s1 v"
by blast
then have "fmlookup (fst a) v ≠ fmlookup s2 v"
using assms(1) a  contra_subsetD fmdom'.rep_eq map_le_def
by metis
then have "¬(fst a ⊆⇩f s2)"
using b fmsubset.rep_eq map_le_def
by metis
}
then show "s1 ⊆⇩f snd a ++ s2"
using P3(4)
by simp
qed

― ‹TODO refactor.›
lemma valid_as_submap_init_submap_exec_i:
fixes s a
shows "fmdom' s ⊆ fmdom' (state_succ s a)"
proof (cases "fst a ⊆⇩f s")
case True
then have "state_succ s a = s ++⇩f (snd a)"
unfolding state_succ_def
by auto
then have "fmdom' (state_succ s a) = fmdom' s ∪ fmdom' (snd a)"
by simp
then show ?thesis
by simp
next
case False
then show ?thesis
unfolding state_succ_def
by simp
qed

― ‹NOTE types for s1 and s2 had to be fixed in order to apply pred\_dom\_subset\_succ\_submap.›
lemma valid_as_submap_init_submap_exec:
fixes s1 s2 :: "'a state"
assumes "(s1 ⊆⇩f s2) " "(∀a. ListMem a as ⟶ (fmdom' (fst a) ⊆ fmdom' s1))"
shows "(exec_plan s1 as ⊆⇩f exec_plan s2 as)"
using assms
proof (induction as arbitrary: s1 s2)
case (Cons a as)
{
have "ListMem a (a # as)"
using elem
by fast
then have "fmdom' (fst a) ⊆ fmdom' s1"
using Cons.prems(2)
by blast
then have "state_succ s1 a ⊆⇩f state_succ s2 a"
using Cons.prems(1) pred_dom_subset_succ_submap
by fast
}
note 1 = this
{
fix b
assume "ListMem b as"
then have "ListMem b (a # as)"
using insert
by fast
then have a: "fmdom' (fst b) ⊆ fmdom' s1"
using Cons.prems(2)
by blast
then have "fmdom' s1 ⊆ fmdom' (state_succ s1 a)"
using valid_as_submap_init_submap_exec_i
by metis
then have "fmdom' (fst b) ⊆ fmdom' (state_succ s1 a)"
using a
by simp
}
then show ?case
using 1 Cons.IH[of "(state_succ s1 a)" "(state_succ s2 a)"]
by fastforce
qed auto

lemma valid_plan_mems:
assumes "(as ∈ valid_plans PROB)" "(ListMem a as)"
shows "a ∈ PROB"
using assms ListMem_iff in_set_conv_decomp valid_append_valid_suff valid_plan_valid_head
by (metis)

― ‹NOTE typing moved into 'fixes' due to type mismatches when using lemma.›
― ‹NOTE showcase (this can't be used due to type problems when the type is specified within
proposition.›
lemma valid_states_nempty:
fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set"
assumes "finite PROB"
shows "∃s. s ∈ (valid_states PROB)"
unfolding valid_states_def
using fmchoice'[OF FINITE_prob_dom[OF assms], where Q = "λ_ _. True"]
by auto

lemma empty_prob_dom_single_val_state:
assumes "(prob_dom PROB = {})"
shows "(∃s. valid_states PROB = {s})"
proof -
{
assume C: "¬(∃s. valid_states PROB = {s})"
then have "valid_states PROB = {s. fmdom' s = {}}"
using assms
then have "∃s. valid_states PROB = {s}"
using empty_domain_fmap_set
by blast
then have False
using C
by blast
}
then show ?thesis
by blast
qed

lemma empty_prob_dom_imp_empty_plan_always_good:
fixes PROB s
assumes "(prob_dom PROB = {})" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(exec_plan s [] = exec_plan s as)"
using assms empty_plan_is_valid exec_fdom_empty_prob
by fastforce

lemma empty_prob_dom:
fixes PROB
assumes "(prob_dom PROB = {})"
shows "(PROB = {(fmempty, fmempty)} ∨ PROB = {})"
using assms
proof (cases "PROB = {}")
case False
have "⋃((λ(s1, s2). fmdom' s1 ∪ fmdom' s2)  PROB) = {}"
using assms
then have 1:"∀a∈PROB. (λ(s1, s2). fmdom' s1 ∪ fmdom' s2) a = {}"
using  Union_empty_conv
by auto
{
fix a
assume P1: "a∈PROB"
then have "(λ(s1, s2). fmdom' s1 ∪ fmdom' s2) a = {}"
using 1
by simp
then have a: "fmdom' (fst a) = {}" "fmdom' (snd a) = {}"
by auto+
then have b: "fst a = fmempty"
using fmrestrict_set_dom fmrestrict_set_null
by metis
then have "snd a = fmempty"
using a(2) fmrestrict_set_dom fmrestrict_set_null
by metis
then have "a = (fmempty, fmempty)"
using b surjective_pairing
by metis
}
then have "PROB = {(fmempty, fmempty)}"
using False
by blast
then show ?thesis
by blast
qed simp

lemma empty_prob_dom_finite:
fixes PROB :: "'a problem"
assumes "prob_dom PROB = {}"
shows "finite PROB"
proof -
consider (i) "PROB = {(fmempty, fmempty)}" | (ii) "PROB = {}"
using assms empty_prob_dom
by auto
then show ?thesis by (cases) auto
qed

― ‹NOTE type for a had to be fixed (type mismatch in goal).›
lemma disj_imp_eq_proj_exec:
fixes a :: "('a, 'b) fmap × ('a, 'b) fmap" and vs s
assumes "(fmdom' (snd a) ∩ vs) = {}"
shows "(fmrestrict_set vs s = fmrestrict_set vs (state_succ s a))"
proof -
have "disjnt (fmdom' (snd a)) vs"
using assms disjnt_def
by fast
then show ?thesis
using disj_dom_drest_fupdate_eq state_succ_pair surjective_pairing
by metis
qed

lemma no_change_vs_eff_submap:
fixes a vs s
assumes "(fmrestrict_set vs s = fmrestrict_set vs (state_succ s a))" "(fst a ⊆⇩f s)"
shows "(fmrestrict_set vs (snd a) ⊆⇩f (fmrestrict_set vs s))"
proof -
{
fix x
assume P3: "x ∈ dom (fmlookup (fmrestrict_set vs (snd a)))"
then have "(fmlookup (fmrestrict_set vs (snd a))) x = (fmlookup (fmrestrict_set vs s)) x"
proof (cases "fmlookup (fmrestrict_set vs (snd a)) x")
case None
then show ?thesis using P3 by blast
next
case (Some y)
then have "fmrestrict_set vs s = fmrestrict_set vs (s ++⇩f snd a)"
using assms
then have "fmlookup (fmrestrict_set vs s) = fmlookup (fmrestrict_set vs (s ++⇩f snd a))"
by auto
then have 1: "
fmlookup (fmrestrict_set vs s) x
= (if x ∈ vs then fmlookup (s ++⇩f snd a) x else None)
"
using fmlookup_restrict_set
by metis
then show ?thesis
proof (cases "x ∈ vs")
case True
then have "fmlookup (fmrestrict_set vs s) x = fmlookup (s ++⇩f snd a) x"
using True 1
by auto
then show ?thesis
by (metis (mono_tags, lifting))
next
case False
then have 1: "fmlookup (fmrestrict_set vs s) x = None"
using False "1"
by auto
then show ?thesis
using 1 False
by auto
qed
qed
}
then have "(fmlookup (fmrestrict_set vs (snd a)) ⊆⇩m fmlookup (fmrestrict_set vs s))"
using map_le_def
by blast
then show ?thesis
using fmsubset.rep_eq
by blast
qed

― ‹NOTE type of a had to be fixed.›
lemma sat_precond_as_proj_3:
fixes s and a :: "('a, 'b) fmap × ('a, 'b) fmap" and vs
assumes "(fmdom' (fmrestrict_set vs (snd a)) = {})"
shows "((fmrestrict_set vs (state_succ s a)) = (fmrestrict_set vs s))"
proof -
have "fmdom' (fmrestrict_set vs (fmrestrict_set vs (snd a))) = {}"
using assms fmrestrict_set_dom fmrestrict_set_empty fmrestrict_set_null
by metis
{
fix x
assume C: "x ∈ fmdom' (snd a) ∧ x ∈ vs"
then have a: "x ∈ fmdom' (snd a)" "x ∈ vs"
using C
by blast+
then have "fmlookup (snd a) x ≠ None"
using fmdom'_notI
by metis
then have "fmlookup (fmrestrict_set vs (snd a)) x ≠ None"
using a(2)
by force
then have "x ∈ fmdom' (fmrestrict_set vs (snd a))"
using fmdom'_notD
by metis
then have "fmdom' (fmrestrict_set vs (snd a)) ≠ {}"
by blast
then have False
using assms
by blast
}
then have "∀x. ¬(x ∈ fmdom' (snd a) ∧ x ∈ vs)"
by blast
then have 1: "fmdom' (snd a) ∩ vs = {}"
by blast
have "disjnt (fmdom' (snd a)) vs"
using 1 disjnt_def
by blast
then show ?thesis
using 1 disj_imp_eq_proj_exec
by metis
qed

― ‹NOTE type for a had to be fixed (type mismatch in goal).›
― ‹TODO showcase (quick win with simp).›
lemma proj_eq_proj_exec_eq:
fixes s s' vs and a :: "('a, 'b) fmap × ('a, 'b) fmap" and a'
assumes "((fmrestrict_set vs s) = (fmrestrict_set vs s'))" "((fst a ⊆⇩f s) = (fst a' ⊆⇩f s'))"
"(fmrestrict_set vs (snd a) = fmrestrict_set vs (snd a'))"
shows "(fmrestrict_set vs (state_succ s a) = fmrestrict_set vs (state_succ s' a'))"
using assms

lemma empty_eff_exec_eq:
fixes s a
assumes "(fmdom' (snd a) = {})"
shows "(state_succ s a = s)"
using assms

lemma exec_as_proj_valid_2:
fixes a
assumes "a ∈ PROB"
shows "(action_dom (fst a) (snd a) ⊆ prob_dom PROB)"
using assms
by (simp add: FDOM_eff_subset_prob_dom_pair FDOM_pre_subset_prob_dom_pair action_dom_def)

lemma valid_filter_valid_as:
assumes "(as ∈ valid_plans PROB)"
shows "(filter P as ∈ valid_plans PROB)"
using assms
by(auto simp: valid_plans_def)

lemma sublist_valid_plan:
assumes "(subseq as' as)" "(as ∈ valid_plans PROB)"
shows "(as' ∈ valid_plans PROB)"
using assms
by (auto simp: valid_plans_def) (meson fset_mp fset_of_list_elem sublist_subset subsetCE)

lemma prob_subset_dom_subset:
assumes "PROB1 ⊆ PROB2"
shows "(prob_dom PROB1 ⊆ prob_dom PROB2)"
using assms

lemma state_succ_valid_act_disjoint:
assumes "(a ∈ PROB)" "(vs ∩ (prob_dom PROB) = {})"
shows "(fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s)"
using assms
by (smt
FDOM_eff_subset_prob_dom_pair disj_imp_eq_proj_exec inf.absorb1
inf_bot_right inf_commute inf_left_commute
)

lemma exec_valid_as_disjoint:
fixes s
assumes "(vs ∩ (prob_dom PROB) = {})" "(as ∈ valid_plans PROB)"
shows "(fmrestrict_set vs (exec_plan s as) = fmrestrict_set vs s)"
using assms
proof (induction as arbitrary: s vs PROB)
case (Cons a as)
then show ?case
valid_plan_valid_tail)
qed simp

definition state_successors where
"state_successors PROB s ≡ ((state_succ s  PROB) - {s})"

subsection "State Spaces"

definition stateSpace where
"stateSpace ss vs ≡ (∀s. s ∈ ss ⟶ (fmdom' s = vs))"

lemma EQ_SS_DOM:
assumes "¬(ss = {})" "(stateSpace ss vs1)" "(stateSpace ss vs2)"
shows "(vs1 = vs2)"
using assms
by (auto simp: stateSpace_def)

― ‹NOTE Name 'dom' changed to 'domain' because of name clash with 'Map.dom'.›
lemma FINITE_SS:
fixes ss :: "('a, bool) fmap set"
assumes "¬(ss = {})" "(stateSpace ss domain)"
shows "finite ss"
proof -
have 1: "stateSpace ss domain = (∀s. s ∈ ss ⟶ (fmdom' s = domain))"
{
fix s
assume P1: "s ∈ ss"
have "fmdom' s = domain"
using assms 1 P1
by blast
then have "s ∈ {s. fmdom' s = domain}"
by auto
}
then have 2: "ss ⊆ {s. fmdom' s = domain}"
by blast
― ‹TODO add lemma (finite (fmdom' s))›
then have "finite domain"
using 1 assms
by fastforce
then have "finite {s :: 'a state. fmdom' s = domain}"
using FINITE_states
by blast
then show ?thesis
using 2 finite_subset
by auto
qed

lemma disjoint_effects_no_effects:
fixes s
assumes "(∀a. ListMem a as ⟶ (fmdom' (fmrestrict_set vs (snd a)) = {}))"
shows "(fmrestrict_set vs (exec_plan s as) = (fmrestrict_set vs s))"
using assms
proof (induction as arbitrary: s vs)
case (Cons a as)
then have "ListMem a (a # as)"
using elem
by fast
then have "fmdom' (fmrestrict_set vs (snd a)) = {}"
using Cons.prems(1)
by blast
then have "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s"
using sat_precond_as_proj_3
by blast
then show ?case
by (simp add: Cons.IH Cons.prems insert)
qed auto

subsection "Needed Asses"

― ‹NOTE name shortened.›
definition action_needed_vars where
"action_needed_vars a s ≡ {v. (v ∈ fmdom' s) ∧ (v ∈ fmdom' (fst a))
∧ (fmlookup (fst a) v = fmlookup s v)}"
― ‹NOTE name shortened to 'action\_needed\_asses'.›
definition action_needed_asses where
"action_needed_asses a s ≡ fmrestrict_set (action_needed_vars a s) s"

― ‹NOTE type for 'a' had to be fixed (type mismatch in goal).›
lemma act_needed_asses_submap_succ_submap:
fixes a s1 s2
assumes "(action_needed_asses a s2 ⊆⇩f action_needed_asses a s1)" "(s1 ⊆⇩f s2)"
shows "(state_succ s1 a ⊆⇩f state_succ s2 a)"
using assms
unfolding state_succ_def
proof (auto)
assume P1: "action_needed_asses a s2 ⊆⇩f action_needed_asses a s1" "s1 ⊆⇩f s2" "fst a ⊆⇩f s1"
"fst a ⊆⇩f s2"
then show "snd a ++ s1 ⊆⇩f snd a ++ s2"
using submap_imp_state_succ_submap_b
by blast
next
assume P2: "action_needed_asses a s2 ⊆⇩f action_needed_asses a s1" "s1 ⊆⇩f s2" "fst a ⊆⇩f s1"
"¬ fst a ⊆⇩f s2"
then show "snd a ++ s1 ⊆⇩f s2"
using submap_imp_state_succ_submap_a
by blast
next
assume P3: "action_needed_asses a s2 ⊆⇩f action_needed_asses a s1" "s1 ⊆⇩f s2" "¬ fst a ⊆⇩f s1"
"fst a ⊆⇩f s2"
let ?vs1="{v ∈ fmdom' s1. v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup s1 v}"
let ?vs2="{v ∈ fmdom' s2. v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup s2 v}"
let ?f="fmrestrict_set ?vs1 s1"
let ?g="fmrestrict_set ?vs2 s2"
have 1: "fmdom' ?f = ?vs1" "fmdom' ?g = ?vs2"
unfolding action_needed_asses_def action_needed_vars_def fmdom'_restrict_set_precise
by blast+
have 2: "fmlookup ?g ⊆⇩m fmlookup ?f"
using P3(1)
unfolding action_needed_asses_def action_needed_vars_def
using fmsubset.rep_eq
by blast
{
{
fix v
assume P3_1: "v ∈ fmdom' ?g"
then have "v ∈ fmdom' s2" "v ∈ fmdom' (fst a)" "fmlookup (fst a) v = fmlookup s2 v"
using 1
by simp+
then have "fmlookup (fst a) v = fmlookup ?g v"
by simp
then have "fmlookup (fst a) v = fmlookup ?f v"
using 2
by (metis (mono_tags, lifting) P3_1 domIff fmdom'_notI map_le_def)
}
then have i: "fmlookup (fst a) ⊆⇩m fmlookup ?f"
using P3(4) 1(2)
by (smt domIff fmdom'_notD fmsubset.rep_eq map_le_def mem_Collect_eq)
{
fix v
assume P3_2: "v ∈ dom (fmlookup (fst a))"
then have "fmlookup (fst a) v = fmlookup ?f v"
using i
by (meson domIff fmdom'_notI map_le_def)
then have "v ∈ ?vs1"
using P3_2 1(1)
by (metis (no_types, lifting) domIff fmdom'_notD)
then have "fmlookup (fst a) v = fmlookup s1 v"
by blast
}
then have "fst a ⊆⇩f s1"
}
then show "s1 ⊆⇩f snd a ++ s2"
using P3(3)
by simp
qed

― ‹TODO refactor.›
lemma as_needed_asses_submap_exec_i:
fixes a s
assumes "v ∈ fmdom' (action_needed_asses a s)"
shows "
fmlookup (action_needed_asses a s) v = fmlookup s v
∧ fmlookup (action_needed_asses a s) v = fmlookup (fst a) v"
using assms
unfolding action_needed_asses_def action_needed_vars_def
using fmdom'_notI fmlookup_restrict_set
by (smt mem_Collect_eq)

― ‹TODO refactor.›
lemma as_needed_asses_submap_exec_ii:
fixes f g v
assumes "v ∈ fmdom' f" "f ⊆⇩f g"
shows "fmlookup f v = fmlookup g v"
using assms
by (meson fmdom'_notI fmdom_notD fmsubset_eq)

― ‹TODO refactor.›
lemma as_needed_asses_submap_exec_iii:
fixes f g v
shows "
fmdom' (action_needed_asses a s)
= {v ∈ fmdom' s. v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup s v}"
unfolding action_needed_asses_def action_needed_vars_def

lemma as_needed_asses_submap_exec_iv:
fixes f a v
assumes "v ∈ fmdom' (action_needed_asses a s)"
shows "
fmlookup (action_needed_asses a s) v = fmlookup s v
∧ fmlookup (action_needed_asses a s) v = fmlookup (fst a) v
∧ fmlookup (fst a) v = fmlookup s v"
using assms
proof -
have 1: "v ∈ {v ∈ fmdom' s. v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup s v}"
using assms as_needed_asses_submap_exec_iii
by metis
then have 2: "fmlookup (action_needed_asses a s) v = fmlookup s v"
unfolding action_needed_asses_def action_needed_vars_def
by force
moreover have 3: "fmlookup (action_needed_asses a s) v = fmlookup (fst a) v"
using 1 2
by simp
moreover have "fmlookup (fst a) v = fmlookup s v"
using 2 3
by argo
ultimately show ?thesis
by blast
qed

― ‹TODO refactor (into Fmap\_Utils.thy).›
lemma as_needed_asses_submap_exec_v:
fixes f g v
assumes "v ∈ fmdom' f" "f ⊆⇩f g"
shows "v ∈ fmdom' g"
proof -
obtain b where 1: "fmlookup f v = b" "b ≠ None"
using assms(1)
by (meson fmdom'_notI)
then have "fmlookup g v = b"
using as_needed_asses_submap_exec_ii[OF assms]
by argo
then show ?thesis
using 1 fmdom'_notD
by fastforce
qed

― ‹TODO refactor.›
lemma as_needed_asses_submap_exec_vi:
fixes a s1 s2 v
assumes "v ∈ fmdom' (action_needed_asses a s1)"
"(action_needed_asses a s1) ⊆⇩f (action_needed_asses a s2)"
shows
"(fmlookup (action_needed_asses a s1) v) = fmlookup (fst a) v
∧ (fmlookup (action_needed_asses a s2) v) = fmlookup (fst a) v ∧
fmlookup s1 v = fmlookup (fst a) v ∧ fmlookup s2 v = fmlookup (fst a) v"
using assms
proof -
have 1:
"fmlookup (action_needed_asses a s1) v = fmlookup s1 v"
"fmlookup (action_needed_asses a s1) v = fmlookup (fst a) v"
"fmlookup (fst a) v = fmlookup s1 v"
using as_needed_asses_submap_exec_iv[OF assms(1)]
by blast+
moreover {
have "fmlookup (action_needed_asses a s1) v = fmlookup (action_needed_asses a s2) v"
using as_needed_asses_submap_exec_ii[OF assms]
by simp
then have "fmlookup (action_needed_asses a s2) v = fmlookup (fst a) v"
using 1(2)
by argo
}
note 2 = this
moreover {
have "v ∈ fmdom' (action_needed_asses a s2)"
using as_needed_asses_submap_exec_v[OF assms]
by simp
then have "fmlookup s2 v = fmlookup (action_needed_asses a s2) v"
using as_needed_asses_submap_exec_i
by metis
also have "… = fmlookup (fst a) v"
using 2
by simp
finally have "fmlookup s2 v = fmlookup (fst a) v"
by simp
}
ultimately show ?thesis
by argo
qed

― ‹TODO refactor.›
lemma as_needed_asses_submap_exec_vii:
fixes f g v
assumes "∀v ∈ fmdom' f. fmlookup f v = fmlookup g v"
shows "f ⊆⇩f g"
proof -
{
fix v
assume a: "v ∈ fmdom' f"
then have "v ∈ dom (fmlookup f)"
by simp
moreover have "fmlookup f v = fmlookup g v"
using assms a
by blast
ultimately have "v ∈ dom (fmlookup f) ⟶ fmlookup f v = fmlookup g v"
by blast
}
then have "fmlookup f ⊆⇩m fmlookup g"
then show ?thesis
qed

― ‹TODO refactor.›
lemma as_needed_asses_submap_exec_viii:
fixes f g v
assumes "f ⊆⇩f g"
shows "∀v ∈ fmdom' f. fmlookup f v = fmlookup g v"
proof -
have 1: "fmlookup f ⊆⇩m fmlookup g"
using assms
{
fix v
assume "v ∈ fmdom' f"
then have "v ∈ dom (fmlookup f)"
by simp
then have "fmlookup f v = fmlookup g v"
using 1 map_le_def
by metis
}
then show ?thesis
by blast
qed

lemma as_needed_asses_submap_exec_viii':
fixes f g v
assumes "f ⊆⇩f g"
shows "fmdom' f ⊆ fmdom' g"
using assms as_needed_asses_submap_exec_v subsetI
by metis

― ‹TODO refactor.›
lemma as_needed_asses_submap_exec_ix:
fixes f g
shows "f ⊆⇩f g = (∀v ∈ fmdom' f. fmlookup f v = fmlookup g v)"
using as_needed_asses_submap_exec_vii  as_needed_asses_submap_exec_viii
by metis

lemma as_needed_asses_submap_exec_x:
fixes f a v
assumes "v ∈ fmdom' (action_needed_asses a f)"
shows "v ∈ fmdom' (fst a) ∧ v ∈ fmdom' f ∧ fmlookup (fst a) v = fmlookup f v"
using assms
unfolding action_needed_asses_def action_needed_vars_def
using as_needed_asses_submap_exec_i assms
by (metis fmdom'_notD fmdom'_notI)

― ‹TODO refactor.›
lemma as_needed_asses_submap_exec_xi:
fixes v a f g
assumes "v ∈ fmdom' (action_needed_asses a (f ++ g))" "v ∈ fmdom' f"
shows "
fmlookup (action_needed_asses a (f ++ g)) v = fmlookup f v
∧ fmlookup (action_needed_asses a (f ++ g)) v = fmlookup (fst a) v"
proof -
have 1: "v ∈ {v ∈ fmdom' (f ++ g). v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup (f ++ g) v}"
using as_needed_asses_submap_exec_x[OF assms(1)]
by blast
{
have "v |∈| fmdom f"
using assms(2)
by (meson fmdom'_notI fmdom_notD)
then have "fmlookup (f ++ g) v = fmlookup f v"
by simp
}
note 2 = this
{

have "fmlookup (action_needed_asses a (f ++ g)) v = fmlookup (f ++ g) v"
unfolding action_needed_asses_def action_needed_vars_def
using 1
by force
then have "fmlookup (action_needed_asses a (f ++ g)) v = fmlookup f v"
using 2
by simp
}
note 3 = this
moreover {
have "fmlookup (fst a) v = fmlookup (f ++ g) v"
using 1
by simp
also have "… = fmlookup f v"
using 2
by simp
also have "… = fmlookup (action_needed_asses a (f ++ g)) v"
using 3
by simp
finally have "fmlookup (action_needed_asses a (f ++ g)) v = fmlookup (fst a) v"
by simp
}
ultimately show ?thesis
by blast
qed

― ‹TODO refactor (into Fmap\_Utils.thy).›
lemma as_needed_asses_submap_exec_xii:
fixes f g v
assumes "v ∈ fmdom' f"
shows "fmlookup (f ++ g) v = fmlookup f v"
proof -
have "v |∈| fmdom f"
using assms(1) fmdom'_notI fmdom_notD
by metis
then show ?thesis
by force
qed

lemma as_needed_asses_submap_exec_xii':
fixes f g v
assumes "v ∉ fmdom' f" "v ∈ fmdom' g"
shows "fmlookup (f ++ g) v = fmlookup g v"
proof -
have "¬(v |∈| fmdom f)"
using assms(1) fmdom'_notI fmdom_notD
by fastforce
moreover have "v |∈| fmdom g"
using assms(2) fmdom'_notI fmdom_notD
by metis
ultimately show ?thesis
by simp
qed

― ‹NOTE showcase.›
lemma as_needed_asses_submap_exec:
fixes s1 s2
assumes "(s1 ⊆⇩f s2)"
"(∀a. ListMem a as ⟶ (action_needed_asses a s2 ⊆⇩f action_needed_asses a s1))"
shows "(exec_plan s1 as ⊆⇩f exec_plan s2 as)"
using assms
proof (induction as arbitrary: s1 s2)
case (Cons a as)
― ‹Proof the premises of the induction hypothesis for 'state\_succ s1 a' and 'state\_succ s2 a'.›
{
then have "action_needed_asses a s2 ⊆⇩f action_needed_asses a s1"
using Cons.prems(2) elem
by metis
then have "state_succ s1 a ⊆⇩f state_succ s2 a"
using Cons.prems(1) act_needed_asses_submap_succ_submap
by blast
}
note 1 = this
moreover {
fix a'
assume P: "ListMem a' as"
― ‹Show the goal by rule 'as\_needed\_asses\_submap\_exec\_ix'.›
let ?f="action_needed_asses a' (state_succ s2 a)"
let ?g="action_needed_asses a' (state_succ s1 a)"
{
fix v
assume P_1: "v ∈ fmdom' ?f"
then have "fmlookup ?f v = fmlookup ?g v"
unfolding state_succ_def
text ‹ Split cases on the if-then branches introduced by the definition of 'state\_succ'.›
proof (auto)
assume P_1_1: "v ∈ fmdom' (action_needed_asses a' (snd a ++ s2))" "fst a ⊆⇩f s2"
"fst a ⊆⇩f s1"
have i: "action_needed_asses a' s2 ⊆⇩f action_needed_asses a' s1"
using Cons.prems(2) P insert
by fast
then show "
fmlookup (action_needed_asses a' (snd a ++ s2)) v
= fmlookup (action_needed_asses a' (snd a ++ s1)) v"
proof (cases "v ∈ fmdom' ?g")
case true: True
then have A:
"v ∈ fmdom' (fst a') ∧ v ∈ fmdom' (snd a ++ s1)
∧ fmlookup (fst a') v = fmlookup (snd a ++ s1) v"
using as_needed_asses_submap_exec_x[OF true]
unfolding state_succ_def
using P_1_1(3)
by simp
then have B:
"v ∈ fmdom' (fst a') ∧ v ∈ fmdom' (snd a ++ s2)
∧ fmlookup (fst a') v = fmlookup (snd a ++ s2) v"
using as_needed_asses_submap_exec_x[OF P_1]
unfolding state_succ_def
using P_1_1(2)
by simp
then show ?thesis
proof (cases "v ∈ fmdom' (snd a)")
case True
then have I:
"fmlookup (snd a ++ s2) v = fmlookup (snd a) v"
"fmlookup (snd a ++ s1) v = fmlookup (snd a) v"
using as_needed_asses_submap_exec_xii
by fast+
moreover {
have "fmlookup ?f v = fmlookup (snd a ++ s2) v"
using as_needed_asses_submap_exec_iv[OF P_1]
unfolding state_succ_def
using P_1_1(2)
by presburger
then have "fmlookup ?f v = fmlookup (snd a) v"
using I(1)
by argo
}
moreover {
have "fmlookup ?g v = fmlookup (snd a ++ s1) v"
using as_needed_asses_submap_exec_iv[OF true]
unfolding state_succ_def
using P_1_1(3)
by presburger
then have "fmlookup ?g v = fmlookup (snd a) v"
using I(2)
by argo
}
ultimately show ?thesis
unfolding state_succ_def
using P_1_1(2, 3)
by presburger
next
case False
then have I: "v ∈ fmdom' s1" "v ∈ fmdom' s2"
using A B
by blast+
{
have "fmlookup ?g v = fmlookup (snd a ++ s1) v"
using as_needed_asses_submap_exec_iv[OF true]
unfolding state_succ_def
using P_1_1(3)
by presburger
then have "fmlookup ?g v = fmlookup s1 v"
using as_needed_asses_submap_exec_xii'[OF False I(1)]
by simp
moreover {
have "fmlookup (snd a ++ s1) v = fmlookup s1 v"
using as_needed_asses_submap_exec_xii'[OF False I(1)]
by simp
moreover from ‹fmlookup (snd a ++ s1) v = fmlookup s1 v›
have "fmlookup (fst a') v = fmlookup s1 v"
using A(1)
by argo
ultimately have "fmlookup (action_needed_asses a' s1) v = fmlookup s1 v"
using A(1) I(1)
unfolding action_needed_asses_def action_needed_vars_def
fmlookup_restrict_set
by simp
}
ultimately have "fmlookup ?g v = fmlookup (action_needed_asses a' s1) v"
by argo
}
note II = this
{
have "fmlookup ?f v = fmlookup (snd a ++ s2) v"
using as_needed_asses_submap_exec_iv[OF P_1]
unfolding state_succ_def
using P_1_1(2)
by presburger
moreover from ‹fmlookup ?f v = fmlookup (snd a ++ s2) v›
have α: "fmlookup ?f v = fmlookup s2 v"
using as_needed_asses_submap_exec_xii'[OF False I(2)]
by argo
ultimately have "fmlookup (snd a ++ s2) v = fmlookup s2 v"
by argo
moreover {
from ‹fmlookup (snd a ++ s2) v = fmlookup s2 v›
have "fmlookup (fst a') v = fmlookup s2 v"
using B(1)
by argo
then have "fmlookup (action_needed_asses a' s2) v = fmlookup s2 v"
using B(1) I(2)
unfolding action_needed_asses_def action_needed_vars_def
fmlookup_restrict_set
by simp
}
ultimately have "fmlookup ?f v = fmlookup (action_needed_asses a' s2) v"
using α
by argo
}
note III = this
{
have "v ∈ fmdom' (action_needed_asses a' s2)"
proof -
have "fmlookup (fst a') v = fmlookup s1 v"
by (simp add: A False I(1) as_needed_asses_submap_exec_xii')
then show ?thesis
by (simp add: A Cons.prems(1) I(1, 2)
as_needed_asses_submap_exec_ii as_needed_asses_submap_exec_iii)
qed
then have "
fmlookup (action_needed_asses a' s2) v
= fmlookup (action_needed_asses a' s1) v"
using i as_needed_asses_submap_exec_ix[of "action_needed_asses a' s2"
"action_needed_asses a' s1"]
by blast
}
note IV = this
{
have "fmlookup ?f v = fmlookup (action_needed_asses a' s2) v"
using III
by simp
also have "… = fmlookup (action_needed_asses a' s1) v"
using IV
by simp
finally have "… = fmlookup ?g v"
using II
by simp
}
then show ?thesis
unfolding action_needed_asses_def action_needed_vars_def state_succ_def
using P_1_1 A B
by simp
qed
next
case false: False
have A:
"v ∈ fmdom' (fst a') ∧ v ∈ fmdom' (snd a ++ s2)
∧ fmlookup (fst a') v = fmlookup (snd a ++ s2) v"
using as_needed_asses_submap_exec_x[OF P_1]
unfolding state_succ_def
using P_1_1(2)
by simp
from false have B:
"¬(v ∈ fmdom' (snd a ++ s1)) ∨ ¬(fmlookup (fst a') v = fmlookup (snd a ++ s1) v)"
by (simp add: A P_1_1(3) as_needed_asses_submap_exec_iii state_succ_def)
then show ?thesis
proof (cases "v ∈ fmdom' (snd a)")
case True
then have I: "v ∈ fmdom' (snd a ++ s1)"
by simp
{
from True have
"fmlookup (snd a ++ s2) v = fmlookup (snd a) v"
"fmlookup (snd a ++ s1) v = fmlookup (snd a) v"
using as_needed_asses_submap_exec_xii
by fast+
then have "fmlookup (snd a ++ s1) v = fmlookup (snd a ++ s2) v"
by auto
also have " … = fmlookup (fst a') v"
using A
by simp
finally have "fmlookup (snd a ++ s1) v = fmlookup (fst a') v"
by simp
}
then show ?thesis using B I
by presburger
next
case False
then have I: "v ∈ fmdom' s2"
by blast
{
from P_1 have "fmlookup ?f v ≠ None"
by (meson fmdom'_notI)
moreover from false
have "fmlookup ?g v = None"
ultimately have "fmlookup ?f v ≠ fmlookup ?g v"
by simp
}
moreover
{
{
from P_1_1(2) have "state_succ s2 a = snd a ++ s2"
unfolding state_succ_def
by simp
moreover from ‹state_succ s2 a = snd a ++ s2› have
"fmlookup (state_succ s2 a) v = fmlookup s2 v"
using as_needed_asses_submap_exec_xii'[OF False I]
by simp
ultimately have "fmlookup ?f v = fmlookup (action_needed_asses a' s2) v"
unfolding action_needed_asses_def action_needed_vars_def
}
note I = this
moreover {
from P_1_1(3) have "state_succ s1 a = snd a ++ s1"
unfolding state_succ_def
by simp
moreover from ‹state_succ s1 a = snd a ++ s1› False
have "fmlookup (state_succ s1 a) v = fmlookup s1 v"
ultimately have "fmlookup ?g v = fmlookup (action_needed_asses a' s1) v"
unfolding action_needed_asses_def action_needed_vars_def
using FDOM_state_succ_subset
by auto
}
moreover {
have "v ∈ fmdom' (action_needed_asses a' s2)"
proof -
have "v ∈ fmdom' s2 ∪ fmdom' (snd a)"
by (metis (no_types) A FDOM_state_succ_subset P_1_1(2) state_succ_def subsetCE)
then show ?thesis
by (simp add: A False as_needed_asses_submap_exec_iii as_needed_asses_submap_exec_xii')
qed
then have "
fmlookup (action_needed_asses a' s2) v
= fmlookup (action_needed_asses a' s1) v"
using i as_needed_asses_submap_exec_ix[of "action_needed_asses a' s2"
"action_needed_asses a' s1"]
by blast
}
ultimately have "fmlookup ?f v = fmlookup ?g v"
by simp
}
ultimately show ?thesis
by simp
qed
qed
next
assume P2: "v ∈ fmdom' (action_needed_asses a' (snd a ++ s2))" "fst a ⊆⇩f s2"
"¬ fst a ⊆⇩f s1"
then show "
fmlookup (action_needed_asses a' (snd a ++ s2)) v
= fmlookup (action_needed_asses a' s1) v"
proof -
obtain aa :: "('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ 'a" where
"∀x0 x1. (∃v2. v2 ∈ fmdom' x1
∧ fmlookup x1 v2 ≠ fmlookup x0 v2) = (aa x0 x1 ∈ fmdom' x1
∧ fmlookup x1 (aa x0 x1) ≠ fmlookup x0 (aa x0 x1))"
by moura
then have f1: "∀f fa. aa fa f ∈ fmdom' f
∧ fmlookup f (aa fa f) ≠ fmlookup fa (aa fa f) ∨ f ⊆⇩f fa"
by (meson as_needed_asses_submap_exec_vii)
then have f2: "aa s1 (fst a) ∈ fmdom' (fst a)
∧ fmlookup (fst a) (aa s1 (fst a)) ≠ fmlookup s1 (aa s1 (fst a))"
using P2(3) by blast
then have "aa s1 (fst a) ∈ fmdom' s2"
by (metis (full_types) P2(2) as_needed_asses_submap_exec_v)
then have "aa s1 (fst a) ∈ fmdom' (action_needed_asses a s2)"
using f2 by (simp add: P2(2) as_needed_asses_submap_exec_iii
as_needed_asses_submap_exec_viii)
then show ?thesis
using f1 by (metis (no_types) Cons.prems(2) P2(3) as_needed_asses_submap_exec_vi elem)
qed
next
assume P3: "v ∈ fmdom' (action_needed_asses a' s2)" "¬ fst a ⊆⇩f s2" "fst a ⊆⇩f s1"
then show "
fmlookup (action_needed_asses a' s2) v
= fmlookup (action_needed_asses a' (snd a ++ s1)) v"
using Cons.prems(1) submap_imp_state_succ_submap_a
by blast
next
assume P4: "v ∈ fmdom' (action_needed_asses a' s2)" "¬ fst a ⊆⇩f s2" "¬ fst a ⊆⇩f s1"
then show "
fmlookup (action_needed_asses a' s2) v
= fmlookup (action_needed_asses a' s1) v"
by (simp add: Cons.prems(2) P as_needed_asses_submap_exec_ii insert)
qed
}
then have a: "?f ⊆⇩f ?g"
using as_needed_asses_submap_exec_ix
by blast
}
note 2 = this
then show ?case
unfolding exec_plan.simps
using Cons.IH[of "state_succ s1 a" "state_succ s2 a", OF 1]
by blast
qed simp

― ‹NOTE name shortened.›
definition system_needed_vars where
"system_needed_vars PROB s ≡ (⋃{action_needed_vars a s | a. a ∈ PROB})"

― ‹NOTE name shortened.›
definition system_needed_asses where
"system_needed_asses PROB s ≡ (fmrestrict_set (system_needed_vars PROB s) s)"

lemma action_needed_vars_subset_sys_needed_vars_subset:
assumes "(a ∈ PROB)"
shows "(action_needed_vars a s ⊆ system_needed_vars PROB s)"
using assms
by (auto simp: system_needed_vars_def) (metis surjective_pairing)

lemma action_needed_asses_submap_sys_needed_asses:
assumes "(a ∈ PROB)"
shows "(action_needed_asses a s ⊆⇩f system_needed_asses PROB s)"
proof -
have "action_needed_asses a s = fmrestrict_set (action_needed_vars a s) s"
unfolding action_needed_asses_def
by simp
then have "system_needed_asses PROB s = (fmrestrict_set (system_needed_vars PROB s) s)"
unfolding system_needed_asses_def
by simp
then have 1: "action_needed_vars a s ⊆ system_needed_vars PROB s"
unfolding action_needed_vars_subset_sys_needed_vars_subset
using assms action_needed_vars_subset_sys_needed_vars_subset
by fast
{
fix x
assume P1: "x ∈ dom (fmlookup (fmrestrict_set (action_needed_vars a s) s))"
then have a: "fmlookup (fmrestrict_set (action_needed_vars a s) s) x = fmlookup s x"
by (auto simp: fmdom'_restrict_set_precise)
then have "fmlookup (fmrestrict_set (system_needed_vars PROB s) s) x = fmlookup s x"
using 1 contra_subsetD
by fastforce
then have "
fmlookup (fmrestrict_set (action_needed_vars a s) s) x
= fmlookup (fmrestrict_set (system_needed_vars PROB s) s) x
"
using a
by argo
}
then have "
fmlookup (fmrestrict_set (action_needed_vars a s) s)
⊆⇩m fmlookup (fmrestrict_set (system_needed_vars PROB s) s)
"
using map_le_def
by blast
then show "(action_needed_asses a s ⊆⇩f system_needed_asses PROB s)"
by (simp add: fmsubset.rep_eq action_needed_asses_def system_needed_asses_def)
qed

lemma system_needed_asses_include_action_needed_asses_1:
assumes "(a ∈ PROB)"
shows "(action_needed_vars a (fmrestrict_set (system_needed_vars PROB s) s) = action_needed_vars a s)"
proof -
let ?A="{v ∈ fmdom' (fmrestrict_set (system_needed_vars PROB s) s).
v ∈ fmdom' (fst a)
∧ fmlookup (fst a) v = fmlookup (fmrestrict_set (system_needed_vars PROB s) s) v}"
let ?B="{v ∈ fmdom' s. v ∈ fmdom' (fst a) ∧ fmlookup (fst a) v = fmlookup s v}"
{
fix v
assume "v ∈ ?A"
then have i: "v ∈ fmdom' (fmrestrict_set (system_needed_vars PROB s) s)" "v ∈ fmdom' (fst a)"
"fmlookup (fst a) v = fmlookup (fmrestrict_set (system_needed_vars PROB s) s) v"
by blast+
then have "v ∈ fmdom' s"
moreover have "fmlookup (fst a) v = fmlookup s v"
using i(2, 3) fmdom'_notI
by force
ultimately have "v ∈ ?B"
using i
by blast
}
then have 1: "?A ⊆ ?B"
by blast
{
fix v
assume P: "v ∈ ?B"
then have ii: "v ∈ fmdom' s" "v ∈ fmdom' (fst a)" "fmlookup (fst a) v = fmlookup s v"
by blast+
moreover {
have "∃s'. v ∈ s' ∧ (∃a. (s' = action_needed_vars a s) ∧ a ∈ PROB)"
unfolding action_needed_vars_def
using assms P action_needed_vars_def
by metis
then obtain s' where α: "v ∈ s'" "(∃a. (s' = action_needed_vars a s) ∧ a ∈ PROB)"
by blast
moreover obtain a' where "s' = action_needed_vars a' s" "a' ∈ PROB"
using α
by blast
ultimately have "v ∈ fmdom' (fmrestrict_set (system_needed_vars PROB s) s)"
unfolding fmdom'_restrict_set_precise
using action_needed_vars_subset_sys_needed_vars_subset ii(1) by blast
}
note iii = this
moreover have "fmlookup (fst a) v = fmlookup (fmrestrict_set (system_needed_vars PROB s) s) v"
using ii(3) iii fmdom'_notI
by force
ultimately have "v ∈ ?A"
by blast
}
then have "?B ⊆ ?A"
by blast
then show ?thesis
unfolding action_needed_vars_def
using 1
by blast
qed

― ‹TODO refactor (proven elsewhere?).›
lemma system_needed_asses_include_action_needed_asses_i:
fixes A B f
assumes "A ⊆ B"
shows "fmrestrict_set A (fmrestrict_set B f) = fmrestrict_set A f"
proof -
{
let ?f'="fmrestrict_set A f"
let ?f''="fmrestrict_set A (fmrestrict_set B f)"
assume C: "?f'' ≠ ?f'"
then obtain v where 1: "fmlookup ?f'' v ≠ fmlookup ?f' v"
by (meson fmap_ext)
then have False
proof (cases "v ∈ A")
case True
have "fmlookup ?f'' v = fmlookup (fmrestrict_set B f) v"
using True fmlookup_restrict_set
by simp
moreover have "fmlookup (fmrestrict_set B f) v = fmlookup ?f' v"
using True assms(1)
by auto
ultimately show ?thesis
using 1
by argo
next
case False
then have "fmlookup ?f' v = None" "fmlookup ?f'' v = None"
using fmlookup_restrict_set
by auto+
then show ?thesis
using 1
by argo
qed
}
then show ?thesis
by blast
qed

lemma system_needed_asses_include_action_needed_asses:
assumes "(a ∈ PROB)"
shows "(action_needed_asses a (system_needed_asses PROB s) = action_needed_asses a s)"
proof -
{
have " action_needed_vars a s ⊆ system_needed_vars PROB s"
using action_needed_vars_subset_sys_needed_vars_subset[OF assms]
by simp
then have "
fmrestrict_set (action_needed_vars a s) (fmrestrict_set (system_needed_vars PROB s) s) =
fmrestrict_set (action_needed_vars a s) s"
using system_needed_asses_include_action_needed_asses_i
by fast
}
moreover
{
have
"action_needed_vars a (fmrestrict_set (system_needed_vars PROB s) s) = action_needed_vars a s"
using system_needed_asses_include_action_needed_asses_1[OF assms]
by simp
then have "fmrestrict_set (action_needed_vars a (fmrestrict_set (system_needed_vars PROB s) s))
(fmrestrict_set (system_needed_vars PROB s) s) =
fmrestrict_set (action_needed_vars a s) s
⟷ fmrestrict_set (action_needed_vars a s) (fmrestrict_set (system_needed_vars PROB s) s) =
fmrestrict_set (action_needed_vars a s) s"
by simp
}
ultimately show ?thesis
unfolding  action_needed_asses_def system_needed_asses_def
by simp
qed

lemma system_needed_asses_submap:
"system_needed_asses PROB s ⊆⇩f s"
proof -
{
fix x
assume P: "x∈ dom (fmlookup (system_needed_asses PROB s))"
then have "system_needed_asses PROB s = (fmrestrict_set (system_needed_vars PROB s) s)"
then have "fmlookup (system_needed_asses PROB s) x = fmlookup s x"
using P
by (auto simp: fmdom'_restrict_set_precise)
}
then have "fmlookup (system_needed_asses PROB s) ⊆⇩m fmlookup s"
using map_le_def
by blast
then show ?thesis
using fmsubset.rep_eq
by fast
qed

lemma as_works_from_system_needed_asses:
assumes "(as ∈ valid_plans PROB)"
shows "(exec_plan (system_needed_asses PROB s) as ⊆⇩f exec_plan s as)"
using assms
by (metis
action_needed_asses_def
as_needed_asses_submap_exec
fmsubset_restrict_set_mono system_needed_asses_def
system_needed_asses_include_action_needed_asses
system_needed_asses_include_action_needed_asses_1
system_needed_asses_submap
valid_plan_mems
)

end

# Theory ActionSeqProcess

theory ActionSeqProcess
imports Main "HOL-Library.Sublist" FactoredSystemLib FactoredSystem FSSublist
begin

section "Action Sequence Process"

text ‹ This section defines the preconditions satisfied predicate for action sequences and shows
relations between the execution of action sequnences and their projections some. The preconditions
satisfied predicate (sat\_precond\_as) states that in each recursion step, the given state and the
next action are compatible, i.e. the actions preconditions are met by the state. This is used as
premise to propositions on projections of action sequences to avoid that an invalid unprojected
sequence is suddenly valid after projection. [Abdulaziz et al., p.13] ›

― ‹NOTE curried.›
― ‹NOTE 'fun' because of multiple defining equations.›
fun sat_precond_as where
"sat_precond_as s [] = True"
| "sat_precond_as s (a # as) = (fst a ⊆⇩f s ∧ sat_precond_as (state_succ s a) as)"

lemma sat_precond_as_pair:
"sat_precond_as s ((p, e) # as) = (p ⊆⇩f s ∧ sat_precond_as (state_succ s (p, e)) as)"
by simp

― ‹NOTE 'fun' because of multiple defining equations.›
fun rem_effectless_act where
"rem_effectless_act [] = []"
| "rem_effectless_act (a # as) = (if fmdom' (snd a) ≠ {}
then (a # rem_effectless_act as)
else rem_effectless_act as
)"

― ‹NOTE 'fun' because of multiple defining equations.›
fun no_effectless_act where
"no_effectless_act [] = True"
| "no_effectless_act (a # as) = ((fmdom' (snd a) ≠ {}) ∧ no_effectless_act as)"

lemma graph_plan_lemma_4:
fixes s s' as vs P
assumes "(∀a. (ListMem a as ∧ P a) ⟶ ((fmdom' (snd a) ∩ vs) = {}))" "sat_precond_as s as"
"sat_precond_as s' (filter (λa. ¬(P a)) as)" "(fmrestrict_set vs s = fmrestrict_set vs s')"
shows "
(fmrestrict_set vs (exec_plan s as)
= fmrestrict_set vs (exec_plan s' (filter (λ a. ¬(P a)) as)))
"
using assms
unfolding exec_plan.simps
proof(induction as arbitrary: s s' vs P)
case (Cons a as)
then have 1: "fst a ⊆⇩f s" "sat_precond_as (state_succ s a) as"
by auto
then have 2: "∀a'. ListMem a' as ∧ P a' ⟶ fmdom' (snd a') ∩ vs = {}"
then show ?case
proof (cases "P a")
case True
{
then have "filter (λa. ¬(P a)) (a # as) = filter (λa. ¬(P a)) as"
by simp
then have "sat_precond_as s' (filter (λa. ¬(P a)) as)"
using Cons.prems(3) True
by argo
}
note a = this
{
then have "ListMem a (a # as)"
using elem
by fast
then have "(fmdom' (snd a) ∩ vs) = {}"
using Cons.prems(1) True
by blast
then have "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s"
using disj_imp_eq_proj_exec[symmetric]
by fast
}
then show ?thesis
unfolding exec_plan.simps
using Cons.prems(4) 1(2) 2 True a Cons.IH[where s="state_succ s a" and s'=s']
by fastforce
next
case False
{
have "filter (λa. ¬(P a)) (a # as) = a # filter (λa. ¬(P a)) as"
using False
by auto
then have "fst a ⊆⇩f s'" "sat_precond_as (state_succ s' a) (filter (λa. ¬(P a)) as)"
using Cons.prems(3) False
by force+
}
note b = this
then have "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs (state_succ s' a)"
using proj_eq_proj_exec_eq
using Cons.prems(4) 1(1)
by blast
then show ?thesis
unfolding exec_plan.simps
using 1(2) 2 False b Cons.IH[where s="state_succ s a" and s'="state_succ s' a"]
by force
qed
qed simp

― ‹NOTE curried instead of triples.›
― ‹NOTE 'fun' because of multiple defining equations.›
fun rem_condless_act where
"rem_condless_act s pfx_a [] = pfx_a"
| "rem_condless_act s pfx_a (a # as) = (if fst a ⊆⇩f exec_plan s pfx_a
then rem_condless_act s (pfx_a @ [a]) as
else rem_condless_act s pfx_a as
)"

lemma rem_condless_act_pair: "
rem_condless_act s pfx_a ((p, e) # as) = (if p ⊆⇩f exec_plan s pfx_a
then rem_condless_act s (pfx_a @ [(p,e)]) as
else rem_condless_act s pfx_a as
)
"
"(rem_condless_act s pfx_a [] = pfx_a)"
by simp+

lemma exec_remcondless_cons:
fixes s h as pfx
shows "
exec_plan s (rem_condless_act s (h # pfx) as)
= exec_plan (state_succ s h) (rem_condless_act (state_succ s h) pfx as)
"
by (induction as arbitrary: s h pfx) auto

lemma rem_condless_valid_1:
fixes as s
shows "(exec_plan s as = exec_plan s (rem_condless_act s [] as))"
by (induction as arbitrary: s)
(auto simp add: exec_remcondless_cons FDOM_state_succ state_succ_def)

lemma rem_condless_act_cons:
fixes h' pfx as s
shows "(rem_condless_act s (h' # pfx) as) = (h' # rem_condless_act (state_succ s h') pfx as)"
by (induction as arbitrary: h' pfx s) auto

lemma rem_condless_act_cons_prefix:
fixes h h' as as' s
assumes "prefix (h' # as') (rem_condless_act s [h] as)"
shows "(
(prefix as' (rem_condless_act (state_succ s h) [] as))
∧ h' = h
)"
using assms
proof (induction as arbitrary: h h' as' s)
case Nil
then have "rem_condless_act s [h] [] = [h]"
by simp
then have 1: "as' = []"
using Nil.prems
by simp
then have "rem_condless_act (state_succ s h) [] [] = []"
by simp
then have 2: "prefix as' (rem_condless_act (state_succ s h) [] [])"
using 1
by simp
then have "h = h'"
using Nil.prems
by force
then show ?case
using 2
by blast
next
case (Cons a as)
{
have "rem_condless_act s [h] (a # as) = h # rem_condless_act (state_succ s h) [] (a # as)"
using rem_condless_act_cons
by fast
then have "h = h'"
using Cons.prems
by simp
}
moreover {
obtain l where "(h' # as') @ l = (h # rem_condless_act (state_succ s h) [] (a # as))"
using Cons.prems rem_condless_act_cons prefixE
by metis
then have "prefix (as' @ l) (rem_condless_act (state_succ s h) [] (a # as))"
by simp
then have "prefix as' (rem_condless_act (state_succ s h) [] (a # as))"
using append_prefixD
by blast
}
ultimately show ?case
by fastforce
qed

lemma rem_condless_valid_2:
fixes as s
shows "sat_precond_as s (rem_condless_act s [] as)"
by (induction as arbitrary: s) (auto simp: rem_condless_act_cons)

lemma rem_condless_valid_3:
fixes as s
shows "length (rem_condless_act s [] as) ≤ length as"
by (induction as arbitrary: s)
(auto simp: rem_condless_act_cons le_SucI)

lemma rem_condless_valid_4:
fixes as A s
assumes "(set as ⊆ A)"
shows "(set (rem_condless_act s [] as) ⊆ A)"
using assms
by (induction as arbitrary: A s) (auto simp: rem_condless_act_cons)

lemma rem_condless_valid_6:
fixes as s P
shows "length (filter P (rem_condless_act s [] as)) ≤ length (filter P as)"
proof (induction as arbitrary: P s)
case (Cons a as)
then show ?case
qed simp

lemma rem_condless_valid_7:
fixes s P as as2
assumes "(list_all P as ∧ list_all P as2)"
shows "list_all P (rem_condless_act s as2 as)"
using assms
by (induction as arbitrary: P s as2) auto

lemma rem_condless_valid_8:
fixes s as
shows "subseq (rem_condless_act s [] as) as"
by (induction as arbitrary: s) (auto simp: sublist_cons_4 rem_condless_act_cons)

lemma rem_condless_valid_10:
fixes PROB as
assumes "as ∈ (valid_plans PROB)"
shows "(rem_condless_act s [] as ∈ valid_plans PROB)"
using assms valid_plans_def rem_condless_valid_1 rem_condless_valid_4
by blast

lemma rem_condless_valid:
fixes as A s
assumes "(exec_plan s as = exec_plan s (rem_condless_act s [] as))"
"(sat_precond_as s (rem_condless_act s [] as))"
"(length (rem_condless_act s [] as) ≤ length as)"
"((set as ⊆ A) ⟶ (set (rem_condless_act s [] as) ⊆ A))"
shows "(∀P. (length (filter P (rem_condless_act s [] as)) ≤ length (filter P as)))"
using rem_condless_valid_1  rem_condless_valid_2 rem_condless_valid_3 rem_condless_valid_6
rem_condless_valid_4
by fast

― ‹NOTE type of as had to be fixed for lemma submap`