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

(*
 * 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" "(∀u∈set l1. P1 u)" "¬ P1 a ∧ x = [x←l2 . ¬ P1 x]"
    using Cons(2) filter_eq_Cons_iff[of "λx. ¬P1 x"] 
    by metis
  then have 3: "PProbl l2" 
    using Cons.prems(2, 6) 2(1) sublist_append_back 
    by blast
      ― ‹NOTE Use the induction hypothesis to obtain a specific  `l'''`.›
  {
    have "x = filter (λx. ¬P1 x) l2"
      using 2(3)
      by blast
    moreover have "PProbs (f (f s l1) [a])"
      using Cons.prems(1, 2, 5, 6, 7) 2(1) elem sublist_SING_MEM
      by metis
    moreover have "∀l s. PProbs s ∧ PProbl l ∧ list_all P1 l ⟶ (∃l'. 
      f s l' = f s l ∧ length (filter P2 l') ≤ k1 ∧ length (filter P3 l') ≤ length (filter P3 l)
      ∧ list_all P1 l' ∧ subseq l' l)"
      using Cons.prems(3)
      by blast
    moreover have "∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2)" 
      "∀s l. PProbs s ∧ PProbl l ⟶ PProbs (f s l)" 
      "∀l1 l2. subseq l1 l2 ∧ PProbl l2 ⟶ PProbl l1"
      "∀l1 l2. PProbl (l1 @ l2) = (PProbl l1 ∧ PProbl l2)"
      using Cons.prems(4, 5, 6, 7)
      by blast+
    ultimately have "∃l'. 
      f (f (f s l1) [a]) l' = f (f (f s l1) [a]) l2 ∧ length (filter P3 l') ≤ length (filter P3 l2)
      ∧ (∀l''. sublist l'' l' ∧ list_all P1 l'' ⟶ length (filter P2 l'') ≤ k1) ∧ subseq l' l2" 
      using 3 Cons(1)[of P1 l2, where s="(f (f s l1) [a])"]
      by blast
  }
  then obtain l''' where 4:
    "f (f (f s l1) [a]) l''' = f (f (f s l1) [a]) l2" 
    "length (filter P3 l''') ≤ length (filter P3 l2)" 
    "(∀l''. sublist l'' l''' ∧ list_all P1 l'' ⟶ length (filter P2 l'') ≤ k1) ∧ subseq l''' l2" 
    by blast
  then have "f s (l1 @ [a] @ l''') = f s (l1 @ [a] @ l2)" 
    using Cons.prems(4)
    by auto
  then have "subseq l''' l2"
    using 4(3) 
    by blast
      ― ‹NOTE Use the induction hypothesis to obtain a specific  `l''`.›
  {
    have "∀l s. 
        PProbs s ∧ PProbl l1 ∧ list_all P1 l1 
        ⟶ (∃l''. 
          f s l'' = f s l1 ∧ length (filter P2 l'') ≤ k1 ∧ length (filter P3 l'') ≤ length (filter P3 l1)
          ∧ list_all P1 l'' ∧ subseq l'' l1)"
      using Cons.prems(3)
      by blast
    then have "∃l''. 
        f s l'' = f s l1 ∧ length (filter P2 l'') ≤ k1 ∧ length (filter P3 l'') ≤ length (filter P3 l1)
        ∧ list_all P1 l'' ∧ subseq l'' l1"
      using Cons.prems(1, 2, 7) 2(1, 2) 
      by (metis Ball_set) 
  }

  then obtain l'' where 5:
    "f s l'' = f s l1" "length (filter P2 l'') ≤ k1" 
    "length (filter P3 l'') ≤ length (filter P3 l1)" "list_all P1 l'' ∧ subseq l'' l1"
    by blast
  text ‹ Proof the proposition by providing the witness @{term "l'=(l'' @ [a] @ l''')"}. ›
  let ?l'="(l'' @ [a] @ l''') " 
  {
    have "∀s l1 l2. f (f s l1) l2 = f s (l1 @ l2)"
      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
  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
  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