Session Factored_Transition_System_Bounding

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. ›


subsection ‹Semantics of Map Addition›

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 
addition semantics.›
hide_const (open) Map.map_add
no_notation Map.map_add (infixl "++" 100)
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

lemma nempty_list_append_length_add: 
  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

― ‹NOTE added lemma (listScript.sml:810).›
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"
          by (simp add: ListMem_iff)
        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


― ‹NOTE added lemma (listScript.sml:2784)›
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`).
›

― ‹NOTE added definition›
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))"


― ‹NOTE added lemma›
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
    by (simp add: ListMem_iff) 
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
  by (simp add: sublist_length)


― ‹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" "(uset l1. P1 u)" "¬ P1 a  x = [xl2 . ¬ 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)"
      by (simp add: Cons.prems(4))
    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) 
        add_mono_thms_linordered_semiring(1) 
      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.›
hide_const (open) Map.map_add
no_notation Map.map_add (infixl "++" 100)

― ‹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'')"
    by (metis calculation disjnt_iff fmap_add_ltr_def fmdom'_notD fmdom_notI fmlookup_add)
  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")
        apply(auto simp add: "1")
      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
      subgoal by (simp add: fmdom'_notD)
      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
      by (simp add: map_le_def)
  }
  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)
      by (metis fmap_add_ltr_def fmap_ext fmdom'_notD fmdom_notI fmlookup_add)
    then have b: "v  vs"
      using assms(1)
      by blast
    moreover {
      have "fmdom' (fmrestrict_set vs (f1 ++ f2)) = vs  fmdom' (f1 ++ f2)"
        by (simp add: fmdom'_alt_def fmfilter_alt_defs(4))
      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)"
by (auto simp add: fmdom'_restrict_set_precise)

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.›
hide_const (open) Map.map_add
no_notation Map.map_add (infixl "++" 100)


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)"
  by (simp add: state_succ_def)


― ‹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"}.
›

― ‹NOTE added lemma.›
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

― ‹NOTE added lemma.›
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

― ‹NOTE added lemma.›
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

― ‹NOTE added lemma.›
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

― ‹NOTE added lemma.›
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)


― ‹NOTE added lemma.›
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

― ‹NOTE added lemma.›
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")
          (auto simp add: assms calculation)
    }
    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}"
    by (simp add: empty_domain_fmap_set)
  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

― ‹NOTE added lemma.›
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

― ‹NOTE added lemma.›
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
        "xX. x  v  fmlookup (?f s1) x = fmlookup s1 x"
        "xX. x  v  fmlookup (?f s2) x = fmlookup s2 x"
        by simp+
      then have
        "xX. 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

― ‹NOTE added lemma.›
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

― ‹NOTE added lemma.›
lemma updates_disjoint:
  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})
        = {}
      "
      using False insert.hyps(1) updates_disjoint
      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


― ‹NOTE added lemma.›
lemma state_set_card_i:
  fixes X a
  shows "[a]  (Cons a ` state_set X)"
  by (induction X) auto

― ‹NOTE added lemma.›
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

― ‹NOTE added lemma.›
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)"
  unfolding state_succ_def fmap_add_ltr_def
  using assms
  by force


lemma FDOM_state_succ_subset:
  "fmdom' (state_succ s a)  (fmdom' s  fmdom' (snd a))"
  unfolding state_succ_def fmap_add_ltr_def
  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"


lemma valid_plan_valid_head:
  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
  by (simp add: valid_plans_def)


― ‹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
  by (simp add: valid_plans_def)


lemma valid_append_valid_pref:
  assumes "as1 @ as2  (valid_plans PROB)"
  shows "as1  (valid_plans PROB)"
  using assms
  by (simp add: valid_plans_def)


lemma valid_pref_suff_valid_append:
  assumes "as1  (valid_plans PROB)" "as2  (valid_plans PROB)"
  shows "(as1 @ as2)  (valid_plans PROB)"
  using assms
  by (simp add: valid_plans_def)


― ‹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"
        using Cons.prems(2) valid_plan_valid_head
        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
        by (simp add: ListMem_iff)
    }
    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.›
― ‹NOTE added lemma.›
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.›
― ‹NOTE added lemma.›
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"
          using Cons.prems(2) valid_plan_valid_head
          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))"
  by (simp add: state_list_length_lemma_2 state_set_card)


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' Ras)
    then have a: "state_succ s a'  valid_states PROB"
      using cons_1.prems(3, 4) valid_action_valid_succ valid_plan_valid_head
      by metis
    then have b: "Ras  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'' Rslist)
      then have i: "a'' # Rslist  state_set (state_list (state_succ s a') Ras)"
        using 1 cons_2 cons_in_state_set_2
        by blast
      then show ?thesis
      proof (cases Ras)
        case Nil
        then show ?thesis
          using i cons_2 cons_3
          by auto
      next
        case (Cons a''' Ras')
        then obtain as' where
          "prefix as' (a''' # Ras')" "exec_plan (state_succ s a') as' = last slist"
          "length slist = Suc (length as')"
          using cons_1.IH[of "a''' # Ras'" "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)"
      by (simp add: action_dom_def case_prod_beta')
    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)"
      by (auto simp add: fmdom'_alt_def)
    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 "¬(xstate_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"
    using 1 nempty_list_append_length_add
    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"
    using valid_plan_valid_head
    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
        Cons.prems FDOM_eff_subset_prob_dom_pair sup_absorb2 sup_assoc valid_plan_valid_head)
  ultimately show ?case
    by (metis (no_types, lifting)
        FDOM_state_succ_subset exec_plan.simps(2) order_refl subset_trans sup.mono)
qed simp


― ‹NOTE added lemma.›
lemma reachable_s_finite_thm_1_a:
  fixes s and PROB :: "'a problem"
  assumes "(s :: 'a state)  valid_states PROB"
  shows "(lreachable_s PROB s. lvalid_states PROB)"
proof -
  have 1: "lreachable_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)"
  by (simp add: valid_plans_def)


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


― ‹TODO refactor›
― ‹NOTE added lemma›
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"
            using cons.prems(1, 2) valid_action_valid_succ valid_plan_valid_head
            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
              valid_head_and_tail_valid_plan valid_plan_valid_head)
      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: "(xs. 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"
    using nempty_list_append_length_add 1
    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)
    by (simp add: valid_states_def)
  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
  by (auto simp add: sublist_valid_is_valid)


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)


― ‹NOTE added lemma.›
― ‹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


― ‹NOTE added lemma.›
― ‹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)"
      using fmap_add_ltr_def
      by blast
    then have 2: "(s0 ++ s2) = (s2 ++f s0)"
      using fmap_add_ltr_def
      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"
        by (simp add: True)
      moreover have "a |∈| fmdom s2"
        using True calculation(2) fmdom_notD by fastforce
      moreover have "fmlookup (s0 ++f s2) a = fmlookup s2 a"
        by (simp add: calculation(4))
      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"
        by (auto simp add: False)
      ultimately show ?thesis proof (cases "a |∈| fmdom s0")
        case True
        have "a |∉| fmdom (s1 ++f s0)"
          by (smt "1" "2" C UnE assms dom_map_add fmadd.rep_eq fmsubset.rep_eq map_add_def
              map_add_dom_app_simps(1) map_le_def)
        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)
    by (simp add: state_succ_def)
  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


― ‹NOTE added lemma.›
― ‹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
    using fmap_add_ltr_def
    by auto
  then have "fmdom' (state_succ s a) = fmdom' s  fmdom' (snd a)"
    using fmdom'_add
    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
      by (simp add: valid_states_def)
    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
    by (simp add: prob_dom_def action_dom_def)
  then have 1:"aPROB. (λ(s1, s2). fmdom' s1  fmdom' s2) a = {}"
    using  Union_empty_conv
    by auto
  {
    fix a
    assume P1: "aPROB"
    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
        by (simp add: state_succ_def fmap_add_ltr_def)
      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
          using Some fmadd.rep_eq fmlookup_restrict_set map_add_Some_iff
          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
  by (simp add: fmap_add_ltr_def state_succ_def)


lemma empty_eff_exec_eq:
  fixes s a
  assumes "(fmdom' (snd a) = {})"
  shows "(state_succ s a = s)"
  using assms
  unfolding state_succ_def fmap_add_ltr_def
  by (metis fmadd_empty(2) fmrestrict_set_dom fmrestrict_set_null)


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
  by (auto simp add: prob_dom_def)


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
    by (metis exec_plan.simps(2) state_succ_valid_act_disjoint valid_plan_valid_head
        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))"
    by (simp add: stateSpace_def)
  {
    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"
      by (simp add: map_le_def fmsubset.rep_eq)
  }
  then show "s1 f snd a ++ s2"
    using P3(3)
    by simp
qed


― ‹NOTE added lemma.›
― ‹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)

― ‹NOTE added lemma.›
― ‹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)

― ‹NOTE added lemma.›
― ‹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
  by (simp add: Set.filter_def fmfilter_alt_defs(4))

― ‹NOTE added lemma.›
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

― ‹NOTE added lemma.›
― ‹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

― ‹NOTE added lemma.›
― ‹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.›
― ‹NOTE added lemma.›
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"
    by (simp add: map_le_def)
  then show ?thesis
    by (simp add: fmsubset.rep_eq)
qed

― ‹TODO refactor.›
― ‹NOTE added lemma.›
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
    by (simp add: fmsubset.rep_eq)
  {
    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

― ‹NOTE added lemma.›
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

― ‹NOTE added lemma.›
― ‹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

― ‹NOTE added lemma.›
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)

― ‹NOTE added lemma.›
― ‹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"
      unfolding fmap_add_ltr_def fmlookup_add
      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

― ‹NOTE added lemma.›
― ‹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
    unfolding fmap_add_ltr_def
    using fmlookup_add
    by force
qed

― ‹NOTE added lemma.›
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
    unfolding fmap_add_ltr_def
    using fmlookup_add
    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
              unfolding fmap_add_ltr_def fmdom'_add
              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)"
              unfolding fmap_add_ltr_def fmdom'_add
              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"
              using A unfolding fmap_add_ltr_def fmdom'_add
              by blast
            {
              from P_1 have "fmlookup ?f v  None"
                by (meson fmdom'_notI)
              moreover from false
              have "fmlookup ?g v = None"
                by (simp add: fmdom'_notD)
              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
                  by (simp add: A I)
              }
              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"
                  unfolding fmap_add_ltr_def
                  using fmlookup_add
                  by (simp add: fmdom'_alt_def fmember.rep_eq)
                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"
      by (simp add: fmdom'_restrict_set_precise)
    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

― ‹NOTE added lemma.›
― ‹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)"
      by (simp add: system_needed_asses_def)
    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)"


― ‹NOTE added lemma.›
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 = {}"
    by (simp add: Cons.prems(1) insert)
  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
    by (simp add: rem_condless_act_cons le_SucI)
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