Theory AcycSspace

theory AcycSspace
  imports
    FactoredSystem
    ActionSeqProcess
    SystemAbstraction
    Acyclicity
    FmapUtils
begin


section "Acyclic State Spaces"


― ‹NOTE name shortened.›
― ‹NOTE type for `max` had to be fixed to natural number maximum (due to problem with loose
typing).›
value "(state_successors (prob_proj PROB vs))"
definition S
  where "S vs lss PROB s ≡ wlp
    (λx y. y ∈ (state_successors (prob_proj PROB vs) x))
    (λs. problem_plan_bound (snapshot PROB s))
    (max :: nat ⇒ nat ⇒ nat) (λx y. x + y + 1) s lss
  "

― ‹NOTE name shortened.›
― ‹NOTE using `fun` because of multiple defining equations.›
fun vars_change where
  "vars_change [] vs s = []"
| "vars_change (a # as) vs s = (if fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s
    then state_succ s a # vars_change as vs (state_succ s a)
    else vars_change as vs (state_succ s a)
  )"


lemma vars_change_cat:
  fixes s
  shows "
    vars_change (as1 @ as2) vs s
    = (vars_change as1 vs s @ vars_change as2 vs (exec_plan s as1))
  "
  by (induction as1 arbitrary: s as2 vs) auto


lemma empty_change_no_change:
  fixes s
  assumes "(vars_change as vs s = [])"
  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 show ?case
  proof (cases "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s")
    case True
      ― ‹NOTE This case violates the induction premise @{term "vars_change (a # as) vs s = []"} since the
        empty list is impossible.›
    then have "state_succ s a # vars_change as vs (state_succ s a) = []"
      using Cons.prems True
      by simp
    then show "fmrestrict_set vs (exec_plan s (a # as)) = fmrestrict_set vs s"
      by blast
  next
    case False
    then have "vars_change as vs (state_succ s a) = []"
      using Cons.prems False
      by force
    then have
      "fmrestrict_set vs (exec_plan (state_succ s a) as) = fmrestrict_set vs (state_succ s a)"
      using Cons.IH[of vs "(state_succ s a)"]
      by blast
    then show "fmrestrict_set vs (exec_plan s (a # as)) = fmrestrict_set vs s"
      using False
      by simp
  qed
qed auto


― ‹NOTE renamed variable `a` to `b` to not conflict with naming for list head in induction step.›
lemma zero_change_imp_all_effects_submap:
  fixes s s'
  assumes "(vars_change as vs s = [])" "(sat_precond_as s as)" "(ListMem b as)"
    "(fmrestrict_set vs s = fmrestrict_set vs s')"
  shows "(fmrestrict_set vs (snd b) ⊆⇩f fmrestrict_set vs s')"
  using assms
proof (induction as arbitrary: s s' vs b)
  case (Cons a as)
    ― ‹NOTE Having either @{term "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s"} or
    @{term "¬ListMem b as"} leads to simpler propositions so we split here.›
  then show "(fmrestrict_set vs (snd b) ⊆⇩f fmrestrict_set vs s')"
    using Cons.prems(1)
  proof (cases "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s ∧ ListMem b as")
    case True
    let ?s="state_succ s a"
    have "vars_change as vs ?s = []"
      using True Cons.prems(1)
      by auto
    moreover have "sat_precond_as ?s as"
      using Cons.prems(2) sat_precond_as.simps(2)
      by blast
    ultimately show ?thesis
      using True Cons.prems(4) Cons.IH
      by auto
  next
    case False
    then consider
      (i) "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s"
      | (ii) "¬ListMem b as"
      by blast
    then show ?thesis
      using Cons.prems(1)
    proof (cases)
      case ii
      then have "a = b"
        using Cons.prems(3) ListMem_iff set_ConsD
        by metis
          ― ‹NOTE Mysteriously sledgehammer finds a proof here while the premises of
            `no\_change\_vs\_eff\_submap` cannot be proven individually.›
      then show ?thesis
        using Cons.prems(1, 2, 4) no_change_vs_eff_submap
        by (metis list.distinct(1) sat_precond_as.simps(2) vars_change.simps(2))
    qed simp
  qed
qed (simp add: ListMem_iff)


lemma zero_change_imp_all_preconds_submap:
  fixes s s'
  assumes "(vars_change as vs s = [])" "(sat_precond_as s as)" "(ListMem b as)"
    "(fmrestrict_set vs s = fmrestrict_set vs s')"
  shows "(fmrestrict_set vs (fst b) ⊆⇩f fmrestrict_set vs s')"
  using assms
proof (induction as arbitrary: vs s s')
  case (Cons a as)
    ― ‹NOTE Having either @{term "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s"} or
    @{term "¬ListMem b as"} leads to simpler propositions so we split here.›
  then show "(fmrestrict_set vs (fst b) ⊆⇩f fmrestrict_set vs s')"
    using Cons.prems(1)
  proof (cases "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s ∧ ListMem b as")
    case True
    let ?s="state_succ s a"
    have "vars_change as vs ?s = []"
      using True Cons.prems(1)
      by auto
    moreover have "sat_precond_as ?s as"
      using Cons.prems(2) sat_precond_as.simps(2)
      by blast
    ultimately show ?thesis
      using True Cons.prems(4) Cons.IH
      by auto
  next
    case False
    then consider
      (i) "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s"
      | (ii) "¬ListMem b as"
      by blast
    then show ?thesis
      using Cons.prems(1)
    proof (cases)
      case ii
      then have "a = b"
        using Cons.prems(3) ListMem_iff set_ConsD
        by metis
      then show ?thesis
        using Cons.prems(2, 4) fmsubset_restrict_set_mono
        by (metis sat_precond_as.simps(2))
    qed simp
  qed
qed (simp add: ListMem_iff)


lemma no_vs_change_valid_in_snapshot:
  assumes "(as ∈ valid_plans PROB)" "(sat_precond_as s as)" "(vars_change as vs s = [])"
  shows "(as ∈ valid_plans (snapshot PROB (fmrestrict_set vs s)))"
proof -
  {
    fix a
    assume P: "ListMem a as"
    then have "agree (fst a) (fmrestrict_set vs s)"
      by (metis agree_imp_submap assms(2) assms(3) fmdom'_restrict_set
          restricted_agree_imp_agree zero_change_imp_all_preconds_submap)
    moreover have "agree (snd a) (fmrestrict_set vs s)"
      by (metis (no_types) P agree_imp_submap assms(2) assms(3) fmdom'_restrict_set
          restricted_agree_imp_agree zero_change_imp_all_effects_submap)
    ultimately have "agree (fst a) (fmrestrict_set vs s)" "agree (snd a) (fmrestrict_set vs s)"
      by simp+
  }
  then show ?thesis
    using assms(1) as_mem_agree_valid_in_snapshot
    by blast
qed


― ‹NOTE type of `PROB` had to be fixed for `problem\_plan\_bound\_works`.›
lemma no_vs_change_obtain_snapshot_bound_1st_step:
  fixes PROB :: "'a problem"
  assumes "finite PROB" "(vars_change as vs s = [])" "(sat_precond_as s as)"
    "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
  shows "(∃as'.
    (
      exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as
      = exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as'
    )
    ∧ (subseq as' as)
    ∧ (length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
  )"
proof -
  let ?s="(fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s)"
  let ?PROB="(snapshot PROB (fmrestrict_set vs s))"
  {
    have "finite (snapshot PROB (fmrestrict_set vs s))"
      using assms(1) FINITE_snapshot
      by blast
  }
  moreover {
    have "
      fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s
      ∈ valid_states (snapshot PROB (fmrestrict_set vs s))"
      using assms(4) graph_plan_not_eq_last_diff_paths valid_states_snapshot
      by blast
  }
  moreover {
    have "as ∈ valid_plans (snapshot PROB (fmrestrict_set vs s))"
      using assms(2, 3, 5) no_vs_change_valid_in_snapshot
      by blast
  }
  ultimately show ?thesis
    using problem_plan_bound_works[of ?PROB ?s as]
    by blast
qed


― ‹NOTE type of `PROB` had to be fixed for `no\_vs\_change\_obtain\_snapshot\_bound\_1st\_step`.›
lemma no_vs_change_obtain_snapshot_bound_2nd_step:
  fixes PROB :: "'a problem"
  assumes "finite PROB" "(vars_change as vs s = [])" "(sat_precond_as s as)"
    "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
  shows "(∃as'.
    (
      exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s)))  s) as
      = exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as'
    )
    ∧ (subseq as' as)
    ∧ (sat_precond_as s as')
    ∧ (length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
  )"
proof -
  obtain as'' where 1:
    "
      exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as
      = exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as''"
    "subseq as'' as" "length as'' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
    using assms no_vs_change_obtain_snapshot_bound_1st_step
    by blast
  let ?s'="(fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s)"
  let ?as'="rem_condless_act ?s' [] as''"
  have "exec_plan ?s' as = exec_plan ?s' as''"
    using 1(1) rem_condless_valid_1
    by blast
  moreover have "subseq ?as' as"
    using 1(2) rem_condless_valid_8 sublist_trans
    by blast
  moreover have "sat_precond_as s ?as'"
    using sat_precond_drest_sat_precond rem_condless_valid_2
    by fast
  moreover have "(length ?as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))"
    using 1 rem_condless_valid_3 le_trans
    by blast
  ultimately show ?thesis
    using 1 rem_condless_valid_1
    by auto
qed


lemma no_vs_change_obtain_snapshot_bound_3rd_step:
  assumes "finite (PROB :: 'a problem)" "(vars_change as vs s = [])" "(no_effectless_act as)"
    "(sat_precond_as s as)" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
  shows "(∃as'.
    (
      fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as)
      = fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as')
    )
    ∧ (subseq as' as)
    ∧ (length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
  )"
proof -
  obtain as' :: "(('a, bool) fmap × ('a, bool) fmap) list" where
    "(
      exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as
      = exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as'
    )" "subseq as' as" "sat_precond_as s as'"
    "length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
    using assms(1, 2, 4, 5, 6) no_vs_change_obtain_snapshot_bound_2nd_step
    by blast
  moreover have
    "exec_plan (fmrestrict_set vs s) (as_proj as vs) = fmrestrict_set vs (exec_plan s as)"
    using assms(4) sat_precond_exec_as_proj_eq_proj_exec
    by blast
  moreover have "as_proj as (prob_dom (snapshot PROB (fmrestrict_set vs s))) = as"
    using assms(2, 3, 4, 6) as_proj_eq_as no_vs_change_valid_in_snapshot
    by blast
  ultimately show ?thesis
    using sublist_as_proj_eq_as proj_exec_proj_eq_exec_proj'
    by metis
qed

― ‹NOTE added lemma.›
― ‹TODO remove unused assumptions.›
lemma no_vs_change_snapshot_s_vs_is_valid_bound_i:
  fixes PROB :: "'a problem"
  assumes  "finite PROB" "(vars_change as vs s = [])" "(no_effectless_act as)"
    "(sat_precond_as s as)" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
    "fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as) =
        fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as')"
    "subseq as' as" "length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
  shows
    "fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
        (exec_plan s as)
      = fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
        s
    ∧ fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
        (exec_plan s as')
      = fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
        s"
proof -
  let ?vs="(prob_dom (snapshot PROB (fmrestrict_set vs s)))"
  let ?vs'="(fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))"
  let ?vs''="(fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))"
  let ?s="(exec_plan s as)"
  let ?s'="(exec_plan s as')"
  have 1: "as ∈ valid_plans (snapshot PROB (fmrestrict_set vs s))"
    using assms(2, 4, 6) no_vs_change_valid_in_snapshot
    by blast
  {
    {
      fix a
      assume "ListMem a as"
      then have "fmdom' (snd a) ⊆ prob_dom (snapshot PROB (fmrestrict_set vs s))"
        using 1 FDOM_eff_subset_prob_dom_pair valid_plan_mems
        by metis
      then have "fmdom' (fmrestrict_set (fmdom' (exec_plan s as)
          - prob_dom (snapshot PROB (fmrestrict_set vs s))) (snd a))
        = {}"
        using subset_inter_diff_empty[of "fmdom' (snd a)"
            "prob_dom (snapshot PROB (fmrestrict_set vs s))"] fmdom'_restrict_set_precise
        by metis
    }
    then have
      "fmrestrict_set ?vs' (exec_plan s as) = fmrestrict_set ?vs' s"
      using disjoint_effects_no_effects[of as ?vs' s]
      by blast
  }
  moreover {
    {
      fix a
      assume P: "ListMem a as'"
      moreover have α: "as' ∈ valid_plans (snapshot PROB (fmrestrict_set vs s))"
        using assms(8) 1 sublist_valid_plan
        by blast
      moreover have "a ∈ PROB"
        using P α snapshot_subset subsetCE valid_plan_mems
        by fast
      ultimately have "fmdom' (snd a) ⊆ prob_dom (snapshot PROB (fmrestrict_set vs s))"
        using FDOM_eff_subset_prob_dom_pair valid_plan_mems
        by metis
      then have "fmdom' (fmrestrict_set (fmdom' (exec_plan s as')
          - prob_dom (snapshot PROB (fmrestrict_set vs s))) (snd a))
        = {}"
        using subset_inter_diff_empty[of "fmdom' (snd a)"
            "prob_dom (snapshot PROB (fmrestrict_set vs s))"] fmdom'_restrict_set_precise
        by metis
    }
    then have
      "fmrestrict_set ?vs'' (exec_plan s as') = fmrestrict_set ?vs'' s"
      using disjoint_effects_no_effects[of as' ?vs'' s]
      by blast
  }
  ultimately show ?thesis
    by blast
qed

― ‹NOTE type for `PROB` had to be fixed.›
lemma no_vs_change_snapshot_s_vs_is_valid_bound:
  fixes PROB :: "'a problem"
  assumes "finite PROB" "(vars_change as vs s = [])" "(no_effectless_act as)"
    "(sat_precond_as s as)" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
  shows "(∃as'.
    (exec_plan s as = exec_plan s as')
    ∧ (subseq as' as)
    ∧ (length as' <= problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
  )"
proof -
  obtain as' where 1:
    "fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as) =
      fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as')"
    "subseq as' as" "length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
    using assms no_vs_change_obtain_snapshot_bound_3rd_step
    by blast
  {

    have a: "fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
        (exec_plan s as)
      = fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
        s "
      "fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
        (exec_plan s as')
      = fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
        s"
      using assms 1 no_vs_change_snapshot_s_vs_is_valid_bound_i
      by blast+
    moreover have "as' ∈ valid_plans (snapshot PROB (fmrestrict_set vs s))"
      using "1"(2) assms(2) assms(4) assms(6) no_vs_change_valid_in_snapshot sublist_valid_plan
      by blast
    moreover have "(exec_plan s as) ∈ valid_states PROB"
      using assms(5, 6) valid_as_valid_exec
      by blast
    moreover have "(exec_plan s as') ∈ valid_states PROB"
      using assms(5, 6) 1 valid_as_valid_exec sublist_valid_plan
      by blast
    ultimately have "exec_plan s as = exec_plan s as'"
      using assms
      unfolding valid_states_def
      using graph_plan_lemma_5[where vs="prob_dom (snapshot PROB (fmrestrict_set vs s))", OF _ 1(1)]
      by force
  }
  then show ?thesis
    using 1
    by blast
qed


― ‹TODO showcase (problems with stronger typing: Isabelle requires strict typing for `max`; whereas
in HOL4 this is not required, possible because 'MAX' is natural number specific.›
lemma snapshot_bound_leq_S:
  shows "
    problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
    ≤ S vs lss PROB (fmrestrict_set vs s)
  "
proof -
  have "geq_arg (max :: nat ⇒ nat ⇒ nat)"
    unfolding geq_arg_def
    using max.cobounded1
    by simp
  then show ?thesis
    unfolding S_def
    using individual_weight_less_eq_lp[where
        g="max :: nat ⇒ nat ⇒ nat"
        and x="(fmrestrict_set vs s)" and R="(λx y. y ∈ state_successors (prob_proj PROB vs) x)"
        and w="(λs. problem_plan_bound (snapshot PROB s))" and f="(λx y. x + y + 1)" and l=lss]
    by blast
qed


― ‹NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.›
― ‹NOTE the type of `1` had to be restricted to `nat` to ensure the proofs for `geq\_arg` work.›
lemma S_geq_S_succ_plus_ell:
  assumes "(s ∈ valid_states PROB)"
    "(top_sorted_abs (λx y. y ∈ state_successors (prob_proj PROB vs) x) lss)"
    "(s' ∈ state_successors (prob_proj PROB vs) s)" "(set lss = valid_states (prob_proj PROB vs))"
  shows "(
    problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
      + S vs lss PROB (fmrestrict_set vs s')
      + (1 :: nat)
    ≤ S vs lss PROB (fmrestrict_set vs s)
  )"
proof -
  let ?f="λx y. x + y + (1 :: nat)"
  let ?R="(λx y. y ∈ state_successors (prob_proj PROB vs) x)"
  let ?w="(λs. problem_plan_bound (snapshot PROB s))"
  let ?g="max :: nat ⇒ nat ⇒ nat"
  let ?vtx1="(fmrestrict_set vs s')"
  let ?G="lss"
  let ?vtx2="(fmrestrict_set vs s)"
  have "geq_arg ?f"
    unfolding geq_arg_def
    by simp
  moreover have "geq_arg ?g"
    unfolding geq_arg_def
    by simp
  moreover have "∀x. ListMem x lss ⟶ ¬?R x x"
    unfolding state_successors_def
    by blast
  moreover have "?R ?vtx2 ?vtx1"
    unfolding state_successors_def
    using assms(3) state_in_successor_proj_in_state_in_successor state_successors_def
    by blast
  moreover have
    "ListMem ?vtx1 ?G"
    using assms(1, 3, 4)
    by (metis ListMem_iff contra_subsetD graph_plan_not_eq_last_diff_paths proj_successors_of_valid_are_valid)
  moreover have "top_sorted_abs ?R ?G"
    using assms(2)
    by simp
  ultimately show ?thesis
    unfolding S_def
    using lp_geq_lp_from_successor[of ?f ?g ?G ?R ?vtx2 ?vtx1 ?w]
    by blast
qed


lemma vars_change_cons:
  fixes s s'
  assumes "(vars_change as vs s = (s' # ss))"
  shows "(∃as1 act as2.
    (as = as1 @ (act # as2))
    ∧ (vars_change as1 vs s = [])
    ∧ (state_succ (exec_plan s as1) act = s')
    ∧ (vars_change as2 vs (state_succ (exec_plan s as1) act) = ss)
  )"
  using assms
proof (induction as arbitrary: s s' vs ss)
  case (Cons a as)
  then show ?case
  proof (cases "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s")
    case True
    then have "state_succ s a = s'" "vars_change as vs (state_succ s a) = ss"
      using Cons.prems
      by simp+
    then show ?thesis
      by fastforce
  next
    case False
    then have "vars_change as vs (state_succ s a) = s' # ss"
      using Cons.prems
      by simp
    then obtain as1 act as2 where
      "as = as1 @ act # as2" "vars_change as1 vs (state_succ s a) = []"
      "state_succ (exec_plan (state_succ s a) as1) act = s'"
      "vars_change as2 vs (state_succ (exec_plan (state_succ s a) as1) act) = ss"
      using Cons.IH
      by blast
    then show ?thesis
      by (metis False append_Cons exec_plan.simps(2) vars_change.simps(2))
  qed
qed simp


lemma vars_change_cons_2:
  fixes s s'
  assumes "(vars_change as vs s = (s' # ss))"
  shows "(fmrestrict_set vs s' ≠ fmrestrict_set vs s)"
  using assms
  apply(induction as arbitrary: s s' vs ss)
  apply(auto)
  by (metis list.inject)


― ‹NOTE first argument of `top\_sorted\_abs had to be wrapped into lambda.›
lemma problem_plan_bound_S_bound_1st_step:
  fixes PROB :: "'a problem"
  assumes "finite PROB" "(top_sorted_abs (λx y. y ∈ state_successors (prob_proj PROB vs) x) lss)"
    "(set lss = valid_states (prob_proj PROB vs))" "(s ∈ valid_states PROB)"
    "(as ∈ valid_plans PROB)" "(no_effectless_act as)" "(sat_precond_as s as)"
  shows "(∃as'.
      (exec_plan s as' = exec_plan s as)
      ∧ (subseq as' as)
      ∧ (length as' <= S vs lss PROB (fmrestrict_set vs s))
    )"
  using assms
proof (induction "vars_change as vs s" arbitrary: PROB as vs s lss)
  case Nil
  then obtain as' where
    "exec_plan s as = exec_plan s as'" "subseq as' as"
    "length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
    using Nil(1) Nil.prems(1,4,5,6,7) no_vs_change_snapshot_s_vs_is_valid_bound
    by metis
  moreover have "
      problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
      ≤ S vs lss PROB (fmrestrict_set vs s)
    "
    using snapshot_bound_leq_S le_trans
    by fast
  ultimately show ?case
    using le_trans
    by fastforce
next
  case (Cons s' ss)
  then obtain as1 act as2 where 1:
    "as = as1 @ act # as2" "vars_change as1 vs s = []" "state_succ (exec_plan s as1) act = s'"
    "vars_change as2 vs (state_succ (exec_plan s as1) act) = ss"
    using vars_change_cons
    by smt
  text‹ Obtain conclusion of induction hypothesis for 'as2' and
      '(state\_succ (exec\_plan s as1) act)'. ›
  {
    {
      have "as1 ∈ valid_plans PROB"
        using Cons.prems(5) 1(1) valid_append_valid_pref
        by blast
      moreover have "act ∈ PROB"
        using Cons.prems(5) 1 valid_append_valid_suff valid_plan_valid_head
        by fast
      ultimately have "state_succ (exec_plan s as1) act ∈ valid_states PROB"
        using Cons.prems(4) valid_as_valid_exec lemma_1_i
        by blast
    }
    moreover have "as2 ∈ valid_plans PROB"
      using Cons.prems(5) 1(1) valid_append_valid_suff valid_plan_valid_tail
      by fast
    moreover have "no_effectless_act as2"
      using Cons.prems(6) 1(1) rem_effectless_works_13 sublist_append_back
      by blast
    moreover have "sat_precond_as (state_succ (exec_plan s as1) act) as2"
      using Cons.prems(7) 1(1) graph_plan_lemma_17 sat_precond_as.simps(2)
      by blast
    ultimately have "∃as'.
          exec_plan (state_succ (exec_plan s as1) act) as'
          = exec_plan (state_succ (exec_plan s as1) act) as2
        ∧ subseq as' as2
        ∧ length as' ≤ S vs lss PROB (fmrestrict_set vs (state_succ (exec_plan s as1) act))"
      using Cons.prems(1, 2, 3) 1(4)
        Cons(1)[where as="as2" and s="(state_succ (exec_plan s as1) act)"]
      by blast
  }
  note a=this
  {
    have "no_effectless_act as1"
      using Cons.prems(6) 1(1) rem_effectless_works_12
      by blast
    moreover have "sat_precond_as s as1"
      using Cons.prems(7) 1(1) sat_precond_as_pfx
      by blast
    moreover have "as1 ∈ valid_plans PROB"
      using Cons.prems(5) 1(1) valid_append_valid_pref
      by blast
    ultimately have "∃as'. exec_plan s as1 = exec_plan s as' ∧
        subseq as' as1 ∧ length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
      using no_vs_change_snapshot_s_vs_is_valid_bound[of _ as1]
      using Cons.prems(1, 4) 1(2)
      by blast
  }
  then obtain as'' where b:
    "exec_plan s as1 = exec_plan s as''" "subseq as'' as1"
    "length as'' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
    by blast
  {
    obtain as' where i:
      "exec_plan (state_succ (exec_plan s as1) act) as'
          = exec_plan (state_succ (exec_plan s as1) act) as2"
      "subseq as' as2"
      "length as' ≤ S vs lss PROB (fmrestrict_set vs (state_succ (exec_plan s as1) act))"
      using a
      by blast
    let ?as'="as'' @ act # as'"
    have "exec_plan s ?as' = exec_plan s as"
      using 1(1) b(1) i(1) exec_plan_Append exec_plan.simps(2)
      by metis
    moreover have "subseq ?as' as"
      using 1(1) b(2) i(2) subseq_append_iff
      by blast
    moreover
    {
      {
        ― ‹NOTE this is proved earlier in the original proof script. Moved here to improve
            transparency.›
        have "sat_precond_as (exec_plan s as1) (act # as2)"
          using empty_replace_proj_dual7
          using 1(1) Cons.prems(7)
          by blast
        then have "fst act ⊆⇩f (exec_plan s as1)"
          by simp
      }
      note A = this
      {
        have
          "fmrestrict_set vs (state_succ (exec_plan s as1) act)
              = (state_succ (fmrestrict_set vs (exec_plan s as'')) (action_proj act vs))"
          using b(1) A drest_succ_proj_eq_drest_succ[where s="exec_plan s as1", symmetric]
          by simp
        also have "… = (state_succ (fmrestrict_set vs s) (action_proj act vs))"
          using 1(2) b(1) empty_change_no_change
          by fastforce
        finally have "… = fmrestrict_set  vs (state_succ s (action_proj act vs))"
          using  succ_drest_eq_drest_succ
          by blast
      }
      note B = this
      have C: "fmrestrict_set vs (exec_plan s as'') = fmrestrict_set vs s"
        using 1(2) b(1) empty_change_no_change
        by fastforce
      {
        have "act ∈ PROB"
          using Cons.prems(5) 1 valid_append_valid_suff valid_plan_valid_head
          by fast
        then have ℵ: "action_proj act vs ∈ prob_proj PROB vs"
          using action_proj_in_prob_proj
          by blast
        then have "(state_succ s (action_proj act vs)) ∈ (state_successors (prob_proj PROB vs) s)"
        proof (cases "fst (action_proj act vs) ⊆⇩f s")
          case True
          then show ?thesis
            unfolding state_successors_def
            using Cons.hyps(2) 1(3) b(1) A B C ℵ DiffI imageI singletonD vars_change_cons_2
              drest_succ_proj_eq_drest_succ
            by metis
        next
          case False
          then show ?thesis
            unfolding state_successors_def
            using Cons.hyps(2) 1(3) b(1) A B C ℵ DiffI imageI singletonD
              drest_succ_proj_eq_drest_succ vars_change_cons_2
            by metis
        qed
      }
      then have D:
        "problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
                + S vs lss PROB (fmrestrict_set vs (state_succ s (action_proj act vs)))
                + 1
              ≤ S vs lss PROB (fmrestrict_set vs s)"
        using Cons.prems(2, 3, 4) S_geq_S_succ_plus_ell[where s'="state_succ s (action_proj act vs)"]
        by blast
      {
        have
          "length ?as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
                + 1 + S vs lss PROB (fmrestrict_set vs (state_succ (exec_plan s as1) act))"
          using b i
          by fastforce
        then have "length ?as' ≤ S vs lss PROB (fmrestrict_set vs s)"
          using b(1) A B C D drest_succ_proj_eq_drest_succ
          by (smt Suc_eq_plus1 add_Suc dual_order.trans)
      }
    }
    ultimately have ?case
      by blast
  }
  then show ?case
    by blast
qed


― ‹NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.›
lemma problem_plan_bound_S_bound_2nd_step:
  assumes "finite (PROB :: 'a problem)"
    "(top_sorted_abs (λx y. y ∈ state_successors (prob_proj PROB vs) x) lss)"
    "(set lss = valid_states (prob_proj PROB vs))" "(s ∈ valid_states PROB)"
    "(as ∈ valid_plans PROB)"
  shows "(∃as'.
    (exec_plan s as' = exec_plan s as)
    ∧ (subseq as' as)
    ∧ (length as' ≤ S vs lss PROB (fmrestrict_set vs s))
  )"
proof -
  ― ‹NOTE Proof premises and obtain conclusion of `problem\_plan\_bound\_S\_bound\_1st\_step`.›
  {
    have a: "rem_condless_act s [] (rem_effectless_act as) ∈ valid_plans PROB"
      using assms(5) rem_effectless_works_4' rem_condless_valid_10
      by blast
    then have b: "no_effectless_act (rem_condless_act s [] (rem_effectless_act as))"
      using assms rem_effectless_works_6 rem_condless_valid_9
      by fast
    then have "sat_precond_as s (rem_condless_act s [] (rem_effectless_act as))"
      using assms rem_condless_valid_2
      by blast
    then have "∃as'.
      exec_plan s as' = exec_plan s (rem_condless_act s [] (rem_effectless_act as))
      ∧ subseq as' (rem_condless_act s [] (rem_effectless_act as))
      ∧ length as' ≤ S vs lss PROB (fmrestrict_set vs s)
    "
      using assms a b problem_plan_bound_S_bound_1st_step
      by blast
  }
  then obtain as' where 1:
    "exec_plan s as' = exec_plan s (rem_condless_act s [] (rem_effectless_act as))"
    "subseq as' (rem_condless_act s [] (rem_effectless_act as))"
    "length as' ≤ S vs lss PROB (fmrestrict_set vs s)"
    by blast
  then have 2: "exec_plan s as' = exec_plan s as"
    using rem_condless_valid_1 rem_effectless_works_14
    by metis
  then have "subseq as' as"
    using 1(2) rem_condless_valid_8 rem_effectless_works_9 sublist_trans
    by metis
  then show ?thesis
    using 1(3) 2
    by blast
qed


― ‹NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.›
lemma S_in_MPLS_leq_2_pow_n:
  assumes "finite (PROB :: 'a problem)"
    "(top_sorted_abs (λ x y. y ∈ state_successors (prob_proj PROB vs) x) lss)"
    "(set lss = valid_states (prob_proj PROB vs))" "(s ∈ valid_states PROB)"
    "(as ∈ valid_plans PROB)"
  shows "(∃as'.
      (exec_plan s as' = exec_plan s as)
      ∧ (subseq as' as)
      ∧ (length as' ≤ Sup {S vs lss PROB s' | s'. s' ∈ valid_states (prob_proj PROB  vs)})
    )"
proof -
  obtain as' where
    "exec_plan s as' = exec_plan s as" "subseq as' as"
    "length as' ≤ S vs lss PROB (fmrestrict_set vs s)"
    using assms problem_plan_bound_S_bound_2nd_step
    by blast
  moreover {
    ― ‹NOTE Derive sufficient conditions for inferring that `S vs lss PROB` is smaller or equal to
    the supremum of the set @{term "{S vs lss PROB s' | s'. s' ∈ valid_states (prob_proj PROB vs)}"}: i.e.
    being contained and that the supremum is contained as well.›
    let ?S="{S vs lss PROB s' | s'. s' ∈ valid_states (prob_proj PROB vs)}"
    {
      have "fmrestrict_set vs s ∈ valid_states (prob_proj PROB vs)"
        using assms(4) graph_plan_not_eq_last_diff_paths
        by blast
      then have "S vs lss PROB (fmrestrict_set vs s) ∈ ?S"
        using calculation(1)
        by blast
    }
    moreover
    {
      have "finite (prob_proj PROB vs)"
        by (simp add: assms(1) prob_proj_def)
      then have "finite ?S"
        using Setcompr_eq_image assms(3)
        by (metis List.finite_set finite_imageI)
    }
    ultimately have "S vs lss PROB (fmrestrict_set vs s) ≤ Sup ?S"
      using le_cSup_finite by blast
  }
  ultimately show ?thesis
    using le_trans
    by blast
qed


― ‹NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.›
lemma problem_plan_bound_S_bound:
  fixes PROB :: "'a problem"
  assumes "finite PROB" "(top_sorted_abs (λx y. y ∈ state_successors (prob_proj PROB vs) x) lss)"
    "(set lss = valid_states (prob_proj PROB vs))"
  shows "
    problem_plan_bound PROB
    ≤ Sup {S vs lss PROB (s' :: 'a state) | s'. s' ∈ valid_states (prob_proj PROB vs)}
  "
proof -
  let ?f="λPROB.
    Sup {S vs lss PROB (s' :: 'a state) | s'. s' ∈ valid_states (prob_proj PROB vs)} + 1"
  {
    fix as and s :: "'a state"
    assume "s ∈ valid_states PROB" "as ∈ valid_plans PROB"
    then obtain as' where a:
      "exec_plan s as' = exec_plan s as" "subseq as' as"
      "length as' ≤ Sup {S vs lss PROB s' |s'. s' ∈ valid_states (prob_proj PROB vs)}"
      using assms S_in_MPLS_leq_2_pow_n
      by blast
    then have "length as' < ?f PROB"
      by linarith
    moreover have "exec_plan s as = exec_plan s as'"
      using a(1)
      by simp
    ultimately have
      "∃as'. exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' < ?f PROB"
      using a(2)
      by blast
  }
  then show ?thesis
    using assms(1) problem_plan_bound_UBound[where f="?f"]
    by fastforce
qed

subsection "State Space Acyclicity"

text ‹ State space acyclicity is again formalized using graphs to model the state space. However
the relation inducing the graph is the successor relation on states. [Abdulaziz et al.,
Definition 15, HOL4 Definition 15, p.27]

With this, the acyclic system compositional bound `S` can be shown to be an upper bound on the
sublist diameter (lemma `problem\_plan\_bound\_S\_bound\_thesis`). [Abdulaziz et al., p.29] ›

― ‹NOTE name shortened.›
― ‹NOTE first argument of 'top\_sorted\_abs' had to be wrapped into lambda.›
definition sspace_DAG where
  "sspace_DAG PROB lss ≡ (
    (set lss = valid_states PROB)
    ∧ (top_sorted_abs (λx y. y ∈ state_successors PROB x) lss)
  )"


lemma problem_plan_bound_S_bound_2nd_step_thesis:
  assumes "finite (PROB :: 'a problem)" "(sspace_DAG (prob_proj PROB vs) lss)"
    "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
  shows "(∃as'.   (exec_plan s as' = exec_plan s as)
    ∧ (subseq as' as)
    ∧ (length as' ≤ S vs lss PROB (fmrestrict_set vs s))
  )"
  using assms problem_plan_bound_S_bound_2nd_step sspace_DAG_def
  by fast


text ‹And finally, this is the main lemma about the upper bounding algorithm.›

theorem problem_plan_bound_S_bound_thesis:
  assumes "finite (PROB :: 'a problem)" "(sspace_DAG (prob_proj PROB vs) lss)"
  shows "(
    problem_plan_bound PROB
    ≤ Sup {S vs lss PROB s' | s'. s' ∈ valid_states (prob_proj PROB vs)}
  )"
  using assms problem_plan_bound_S_bound sspace_DAG_def
  by fast


end