Theory Correctness_Lemmas

(*  Title:       Extension of Stateful Intransitive Noninterference with Inputs, Outputs, and Nondeterminism in Language IMP
    Author:      Pasquale Noce
                 Senior Staff Firmware Engineer at HID Global, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at hidglobal dot com
*)

section "Sufficiency of well-typedness for information flow correctness: propaedeutic lemmas"

theory Correctness_Lemmas
  imports Overapproximation
begin

text ‹
\null

The purpose of this section is to prove some further lemmas used in the proof of the main theorem,
which is the subject of the next section.

The proof of one of these lemmas uses the lemmas @{text ctyping1_idem} and @{text ctyping2_approx}
proven in the previous sections.
›


subsection "Global context proofs"

lemma bvars_bval:
 "s = t (⊆ bvars b) ⟹ bval b s = bval b t"
by (induction b, simp_all, rule arg_cong2, auto intro: avars_aval)

lemma eq_streams_subset:
 "⟦f = f' (⊆ vs, vs', T); T' ⊆ T⟧ ⟹ f = f' (⊆ vs, vs', T')"
by (auto simp: eq_streams_def)


lemma flow_append_1:
  assumes A: "⋀cfs' :: (com × stage) list.
    c # map fst (cfs :: (com × stage) list) = map fst cfs' ⟹
      flow_aux (map fst cfs' @ map fst cfs'') =
      flow_aux (map fst cfs') @ flow_aux (map fst cfs'')"
  shows "flow_aux (c # map fst cfs @ map fst cfs'') =
    flow_aux (c # map fst cfs) @ flow_aux (map fst cfs'')"
using A [of "(c, λx. 0, λx n. 0, [], []) # cfs"] by simp

lemma flow_append:
 "flow (cfs @ cfs') = flow cfs @ flow cfs'"
by (simp add: flow_def, induction "map fst cfs" arbitrary: cfs
 rule: flow_aux.induct, auto, rule flow_append_1)

lemma flow_cons:
 "flow (cf # cfs) = flow_aux (fst cf # []) @ flow cfs"
by (subgoal_tac "cf # cfs = [cf] @ cfs", simp only: flow_append,
 simp_all add: flow_def)


lemma in_flow_length:
 "length [p←in_flow cs vs f. fst p = x] = length [c←cs. c = IN x]"
by (induction cs vs f rule: in_flow.induct, simp_all)

lemma in_flow_append:
 "in_flow (cs @ cs') vs f =
    in_flow cs vs f @ in_flow cs' (vs @ in_flow cs vs f) f"
by (induction cs' vs f rule: in_flow.induct,
 (simp only: append_assoc [symmetric] in_flow.simps,
 simp add: in_flow_length ac_simps)+)

lemma in_flow_one:
 "in_flow [c] vs f = (case c of
    IN x ⇒ [(x, f x (length [p←vs. fst p = x]))] | _ ⇒ [])"
by (subst append_Nil [symmetric], cases c, simp_all only: in_flow.simps,
 simp_all)


lemma run_flow_append:
 "run_flow (cs @ cs') vs s f =
    run_flow cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f"
by (induction cs' vs s f rule: run_flow.induct,
 (simp only: append_assoc [symmetric] run_flow.simps,
 simp add: in_flow_length ac_simps)+)

lemma run_flow_one:
 "run_flow [c] vs s f = (case c of
    x ::= a ⇒ s(x := aval a s) |
    IN x ⇒ s(x := f x (length [p←vs. fst p = x])) |
    _ ⇒ s)"
by (subst append_Nil [symmetric], cases c, simp_all only: run_flow.simps,
 simp_all)

lemma run_flow_observe:
 "run_flow (⟨X⟩ # cs) vs s f = run_flow cs vs s f"
  apply (rule subst [of "([] @ [⟨X⟩]) @ cs" _
   "λcs'. run_flow cs' vs s f = run_flow cs vs s f"])
   apply fastforce
by (subst run_flow_append, simp only: in_flow.simps run_flow.simps, simp)


lemma out_flow_append:
 "out_flow (cs @ cs') vs s f =
    out_flow cs vs s f @
    out_flow cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f"
by (induction cs' vs s f rule: out_flow.induct,
 (simp only: append_assoc [symmetric] out_flow.simps,
 simp add: run_flow_append)+)

lemma out_flow_one:
 "out_flow [c] vs s f = (case c of
    OUT x ⇒ [(x, s x)] | _ ⇒ [])"
by (subst append_Nil [symmetric], cases c, simp_all only: out_flow.simps,
 simp_all)


lemma no_upd_empty:
 "no_upd cs {}"
by (induction cs "{} :: vname set" rule: no_upd.induct, simp_all)

lemma no_upd_append:
 "no_upd (cs @ cs') X = (no_upd cs X ∧ no_upd cs' X)"
by (induction cs X rule: no_upd.induct, simp_all)

lemma no_upd_in_flow:
 "no_upd cs X ⟹ [p←in_flow cs vs f. fst p ∈ X] = []"
by (induction cs vs f rule: in_flow.induct, simp_all add: no_upd_append)

lemma no_upd_run_flow:
 "no_upd cs X ⟹ run_flow cs vs s f = s (⊆ X)"
by (induction cs vs s f rule: run_flow.induct, auto simp: Let_def no_upd_append)

lemma no_upd_out_flow:
 "no_upd cs X ⟹ [p←out_flow cs vs s f. fst p ∈ X] = []"
by (induction cs vs s f rule: out_flow.induct, simp_all add: no_upd_append)


lemma small_stepsl_append:
 "⟦cf →*{cfs} cf'; cf' →*{cfs'} cf''⟧ ⟹ cf →*{cfs @ cfs'} cf''"
by (induction cf' cfs' cf'' rule: small_stepsl.induct, simp,
 simp only: append_assoc [symmetric] small_stepsl.simps)

lemma small_step_stream:
 "(c, s, f, vs, ws) → (c', p) ⟹ ∃s' vs' ws'. p = (s', f, vs', ws')"
by (induction "(c, s, f, vs, ws)" "(c', p)" arbitrary: c s f vs ws c' p
 rule: small_step.induct, simp_all)

lemma small_stepsl_stream:
 "(c, s, f, vs, ws) →*{cfs} (c', p) ⟹ ∃s' vs' ws'. p = (s', f, vs', ws')"
by (induction "(c, s, f, vs, ws)" cfs "(c', p)" arbitrary: c s f vs ws c' p
 rule: small_stepsl.induct, auto dest: small_step_stream)


lemma small_steps_stepsl_1:
 "∃cfs. cf →*{cfs} cf"
by (rule exI [of _ "[]"], simp)

lemma small_steps_stepsl_2:
 "⟦cf → cf'; cf' →*{cfs} cf''⟧ ⟹ ∃cfs'. cf →*{cfs'} cf''"
by (rule exI [of _ "[cf] @ cfs"], rule small_stepsl_append,
 subst append_Nil [symmetric], simp only: small_stepsl.simps)

lemma small_steps_stepsl:
 "cf →* cf' ⟹ ∃cfs. cf →*{cfs} cf'"
by (induction cf cf' rule: star.induct, rule small_steps_stepsl_1,
 blast intro: small_steps_stepsl_2)

lemma small_stepsl_steps:
 "cf →*{cfs} cf' ⟹ cf →* cf'"
by (induction cf cfs cf' rule: small_stepsl.induct, auto intro: star_trans)

lemma small_steps_stream:
 "(c, s, f, vs, ws) →* (c', p) ⟹ ∃s' vs' ws'. p = (s', f, vs', ws')"
by (blast dest: small_steps_stepsl intro: small_stepsl_stream)


lemma small_stepsl_cons_1:
 "cf →*{[cf']} cf'' ⟹ cf' = cf ∧ (∃cf'. cf → cf' ∧ cf' →*{[]} cf'')"
by (subst (asm) append_Nil [symmetric], simp only: small_stepsl.simps,
 cases cf'', simp)

lemma small_stepsl_cons_2:
 "⟦cf →*{cf' # cfs} cf'' ⟹
    cf' = cf ∧ (∃cf'. cf → cf' ∧ cf' →*{cfs} cf'');
  cf →*{cf' # cfs @ [cf'']} cf'''⟧ ⟹
    cf' = cf ∧ (∃cf'. cf → cf' ∧ cf' →*{cfs @ [cf'']} cf''')"
by (simp only: append_Cons [symmetric], simp only: small_stepsl.simps, simp)

lemma small_stepsl_cons:
 "cf →*{cf' # cfs} cf'' ⟹
    cf' = cf ∧
    (∃cf'. cf → cf' ∧ cf' →*{cfs} cf'')"
by (induction cf cfs cf'' rule: small_stepsl.induct,
 erule small_stepsl_cons_1, rule small_stepsl_cons_2)


lemma small_stepsl_skip:
 "(SKIP, p) →*{cfs} cf ⟹ cf = (SKIP, p) ∧ flow cfs = []"
by (induction "(SKIP, p)" cfs cf rule: small_stepsl.induct,
 auto simp: flow_def)

lemma small_stepsl_assign:
 "(x ::= a, s, p) →*{cfs} cf ⟹
    cf = (x ::= a, s, p) ∧
      flow cfs = [] ∨
    cf = (SKIP, s(x := aval a s), p) ∧
      flow cfs = [x ::= a]"
by (induction "(x ::= a :: com, s, p)" cfs cf rule: small_stepsl.induct,
 force simp: flow_def, auto simp: flow_append, simp_all add: flow_def)

lemma small_stepsl_input:
 "(IN x, s, f, vs, ws) →*{cfs} cf ⟹
    cf = (IN x, s, f, vs, ws) ∧
      flow cfs = [] ∨
   (let n = length [p←vs. fst p = x]
    in cf = (SKIP, s(x := f x n), f, vs @ [(x, f x n)], ws) ∧
      flow cfs = [IN x])"
by (induction "(IN x :: com, s, f, vs, ws)" cfs cf rule:
 small_stepsl.induct, force simp: flow_def, auto simp: Let_def flow_append,
 simp_all add: flow_def)

lemma small_stepsl_output:
 "(OUT x, s, f, vs, ws) →*{cfs} cf ⟹
    cf = (OUT x, s, f, vs, ws) ∧
      flow cfs = [] ∨
    cf = (SKIP, s, f, vs, ws @ [(x, s x)]) ∧
      flow cfs = [OUT x]"
by (induction "(OUT x :: com, s, f, vs, ws)" cfs cf rule:
 small_stepsl.induct, force simp: flow_def, auto simp: flow_append,
 simp_all add: flow_def)


lemma small_stepsl_seq_1:
 "(c⇩1;; c⇩2, p) →*{[]} (c, q) ⟹
    (∃c' cfs'. c = c';; c⇩2 ∧
      (c⇩1, p) →*{cfs'} (c', q) ∧
      flow [] = flow cfs') ∨
    (∃p' cfs' cfs''. length cfs'' < length [] ∧
      (c⇩1, p) →*{cfs'} (SKIP, p') ∧
      (c⇩2, p') →*{cfs''} (c, q) ∧
      flow [] = flow cfs' @ flow cfs'')"
by force

lemma small_stepsl_seq_2:
  assumes A: "⋀c' q'. cf = (c', q') ⟹
    (c⇩1;; c⇩2, p) →*{cfs} (c', q') ⟹
      (∃c'' cfs'. c' = c'';; c⇩2 ∧
        (c⇩1, p) →*{cfs'} (c'', q') ∧
        flow cfs = flow cfs') ∨
      (∃p' cfs' cfs''. length cfs'' < length cfs ∧
        (c⇩1, p) →*{cfs'} (SKIP, p') ∧
        (c⇩2, p') →*{cfs''} (c', q') ∧
        flow cfs = flow cfs' @ flow cfs'')"
    (is "⋀c' q'. _ ⟹ _ ⟹
      (∃c'' cfs'. ?P c' q' c'' cfs') ∨
      (∃p' cfs' cfs''. ?Q c' q' p' cfs' cfs'')")
  assumes B: "(c⇩1;; c⇩2, p) →*{cfs @ [cf]} (c, q)"
  shows
   "(∃c' cfs'. c = c';; c⇩2 ∧
      (c⇩1, p) →*{cfs'} (c', q) ∧
      flow (cfs @ [cf]) = flow cfs') ∨
    (∃p' cfs' cfs''. length cfs'' < length (cfs @ [cf]) ∧
      (c⇩1, p) →*{cfs'} (SKIP, p') ∧
      (c⇩2, p') →*{cfs''} (c, q) ∧
      flow (cfs @ [cf]) = flow cfs' @ flow cfs'')"
    (is "?T ∨ ?U")
proof (cases cf)
  fix c' q'
  assume C: "cf = (c', q')"
  moreover {
    assume D: "(c', q') → (c, q)"
    assume
     "(∃c'' cfs'. ?P c' q' c'' cfs') ∨
      (∃p' cfs' cfs''. ?Q c' q' p' cfs' cfs'')"
    hence ?thesis
    proof
      assume "∃c'' cfs'. ?P c' q' c'' cfs'"
      then obtain c'' and cfs' where
        E: "c' = c'';; c⇩2" and
        F: "(c⇩1, p) →*{cfs'} (c'', q')" and
        G: "flow cfs = flow cfs'"
        by blast
      hence "(c'';; c⇩2, q') → (c, q)"
        using D by simp
      moreover {
        assume
          H: "c'' = SKIP" and
          I: "(c, q) = (c⇩2, q')"
        have ?U
        proof (rule exI [of _ q'], rule exI [of _ cfs'],
         rule exI [of _ "[]"])
          from C and E and F and G and H and I show
           "length [] < length (cfs @ [cf]) ∧
            (c⇩1, p) →*{cfs'} (SKIP, q') ∧
            (c⇩2, q') →*{[]} (c, q) ∧
            flow (cfs @ [cf]) = flow cfs' @ flow []"
            by (simp add: flow_append, simp add: flow_def)
        qed
      }
      moreover {
        fix d q''
        assume
          H: "(c'', q') → (d, q'')" and
          I: "(c, q) = (d;; c⇩2, q'')"
        have ?T
        proof (rule exI [of _ d],
         rule exI [of _ "cfs' @ [(c'', q')]"])
          from C and E and F and G and H and I show
           "c = d;; c⇩2 ∧
            (c⇩1, p) →*{cfs' @ [(c'', q')]} (d, q) ∧
            flow (cfs @ [cf]) = flow (cfs' @ [(c'', q')])"
            by (simp add: flow_append, simp add: flow_def)
        qed
      }
      ultimately show ?thesis
        by blast
    next
      assume "∃p' cfs' cfs''. ?Q c' q' p' cfs' cfs''"
      then obtain p' and cfs' and cfs'' where
        E: "length cfs'' < length cfs" and
        F: "(c⇩1, p) →*{cfs'} (SKIP, p')" and
        G: "(c⇩2, p') →*{cfs''} (c', q')" and
        H: "flow cfs = flow cfs' @ flow cfs''"
        by blast
      show ?thesis
      proof (rule disjI2, rule exI [of _ p'], rule exI [of _ cfs'],
       rule exI [of _ "cfs'' @ [(c', q')]"])
        from C and D and E and F and G and H show
         "length (cfs'' @ [(c', q')]) < length (cfs @ [cf]) ∧
          (c⇩1, p) →*{cfs'} (SKIP, p') ∧
          (c⇩2, p') →*{cfs'' @ [(c', q')]} (c, q) ∧
          flow (cfs @ [cf]) = flow cfs' @ flow (cfs'' @ [(c', q')])"
          by (simp add: flow_append)
      qed
    qed
  }
  ultimately show ?thesis
    using A and B by simp
qed

lemma small_stepsl_seq:
 "(c⇩1;; c⇩2, p) →*{cfs} (c, q) ⟹
    (∃c' cfs'. c = c';; c⇩2 ∧
      (c⇩1, p) →*{cfs'} (c', q) ∧
      flow cfs = flow cfs') ∨
    (∃p' cfs' cfs''. length cfs'' < length cfs ∧
      (c⇩1, p) →*{cfs'} (SKIP, p') ∧ (c⇩2, p') →*{cfs''} (c, q) ∧
      flow cfs = flow cfs' @ flow cfs'')"
by (induction "(c⇩1;; c⇩2, p)" cfs "(c, q)" arbitrary: c⇩1 c⇩2 p c q
 rule: small_stepsl.induct, erule small_stepsl_seq_1,
 rule small_stepsl_seq_2)


lemma small_stepsl_or_1:
  assumes A: "(c⇩1 OR c⇩2, p) →*{cfs} cf ⟹
    cf = (c⇩1 OR c⇩2, p) ∧
      flow cfs = [] ∨
    (c⇩1, p) →*{tl cfs} cf ∧
      flow cfs = flow (tl cfs) ∨
    (c⇩2, p) →*{tl cfs} cf ∧
      flow cfs = flow (tl cfs)"
    (is "_ ⟹ ?P ∨ ?Q ∨ ?R")
  assumes B: "(c⇩1 OR c⇩2, p) →*{cfs @ [cf]} cf'"
  shows
   "cf' = (c⇩1 OR c⇩2, p) ∧
      flow (cfs @ [cf]) = [] ∨
    (c⇩1, p) →*{tl (cfs @ [cf])} cf' ∧
      flow (cfs @ [cf]) = flow (tl (cfs @ [cf])) ∨
    (c⇩2, p) →*{tl (cfs @ [cf])} cf' ∧
      flow (cfs @ [cf]) = flow (tl (cfs @ [cf]))"
    (is "_ ∨ ?T")
proof -
  {
    assume
      C: "(c⇩1 OR c⇩2, p) →*{cfs} cf" and
      D: "cf → cf'"
    assume "?P ∨ ?Q ∨ ?R"
    hence ?T
    proof (rule disjE, erule_tac [2] disjE)
      assume ?P
      moreover from this have "(c⇩1 OR c⇩2, p) → cf'"
        using D by simp
      ultimately show ?thesis
        using C by (auto dest: small_stepsl_cons
         simp: tl_append flow_cons split: list.split)
    next
      assume ?Q
      with C and D show ?thesis
        by (auto simp: tl_append flow_cons split: list.split)
    next
      assume ?R
      with C and D show ?thesis
        by (auto simp: tl_append flow_cons split: list.split)
    qed
  }
  with A and B show ?thesis
    by simp
qed

lemma small_stepsl_or:
 "(c⇩1 OR c⇩2, p) →*{cfs} cf ⟹
    cf = (c⇩1 OR c⇩2, p) ∧
      flow cfs = [] ∨
    (c⇩1, p) →*{tl cfs} cf ∧
      flow cfs = flow (tl cfs) ∨
    (c⇩2, p) →*{tl cfs} cf ∧
      flow cfs = flow (tl cfs)"
by (induction "(c⇩1 OR c⇩2, p)" cfs cf rule: small_stepsl.induct,
 force simp: flow_def, rule small_stepsl_or_1)


lemma small_stepsl_if_1:
  assumes A: "(IF b THEN c⇩1 ELSE c⇩2, s, p) →*{cfs} cf ⟹
    cf = (IF b THEN c⇩1 ELSE c⇩2, s, p) ∧
      flow cfs = [] ∨
    bval b s ∧ (c⇩1, s, p) →*{tl cfs} cf ∧
      flow cfs = ⟨bvars b⟩ # flow (tl cfs) ∨
    ¬ bval b s ∧ (c⇩2, s, p) →*{tl cfs} cf ∧
      flow cfs = ⟨bvars b⟩ # flow (tl cfs)"
    (is "_ ⟹ ?P ∨ ?Q ∨ ?R")
  assumes B: "(IF b THEN c⇩1 ELSE c⇩2, s, p) →*{cfs @ [cf]} cf'"
  shows
   "cf' = (IF b THEN c⇩1 ELSE c⇩2, s, p) ∧
      flow (cfs @ [cf]) = [] ∨
    bval b s ∧ (c⇩1, s, p) →*{tl (cfs @ [cf])} cf' ∧
      flow (cfs @ [cf]) = ⟨bvars b⟩ # flow (tl (cfs @ [cf])) ∨
    ¬ bval b s ∧ (c⇩2, s, p) →*{tl (cfs @ [cf])} cf' ∧
      flow (cfs @ [cf]) = ⟨bvars b⟩ # flow (tl (cfs @ [cf]))"
    (is "_ ∨ ?T")
proof -
  {
    assume
      C: "(IF b THEN c⇩1 ELSE c⇩2, s, p) →*{cfs} cf" and
      D: "cf → cf'"
    assume "?P ∨ ?Q ∨ ?R"
    hence ?T
    proof (rule disjE, erule_tac [2] disjE)
      assume ?P
      moreover from this have "(IF b THEN c⇩1 ELSE c⇩2, s, p) → cf'"
        using D by simp
      ultimately show ?thesis
        using C by (auto dest: small_stepsl_cons
         simp: tl_append flow_cons split: list.split)
    next
      assume ?Q
      with D show ?thesis
        by (auto simp: tl_append flow_cons split: list.split)
    next
      assume ?R
      with D show ?thesis
        by (auto simp: tl_append flow_cons split: list.split)
    qed
  }
  with A and B show ?thesis
    by simp
qed

lemma small_stepsl_if:
 "(IF b THEN c⇩1 ELSE c⇩2, s, p) →*{cfs} cf ⟹
    cf = (IF b THEN c⇩1 ELSE c⇩2, s, p) ∧
      flow cfs = [] ∨
    bval b s ∧ (c⇩1, s, p) →*{tl cfs} cf ∧
      flow cfs = ⟨bvars b⟩ # flow (tl cfs) ∨
    ¬ bval b s ∧ (c⇩2, s, p) →*{tl cfs} cf ∧
      flow cfs = ⟨bvars b⟩ # flow (tl cfs)"
by (induction "(IF b THEN c⇩1 ELSE c⇩2, s, p)" cfs cf rule:
 small_stepsl.induct, force simp: flow_def, rule small_stepsl_if_1)


lemma small_stepsl_while_1:
  assumes A: "(WHILE b DO c, s, p) →*{cfs} cf ⟹
    cf = (WHILE b DO c, s, p) ∧
      flow cfs = [] ∨
    bval b s ∧ (c;; WHILE b DO c, s, p) →*{tl cfs} cf ∧
      flow cfs = ⟨bvars b⟩ # flow (tl cfs) ∨
    ¬ bval b s ∧ cf = (SKIP, s, p) ∧
      flow cfs = [⟨bvars b⟩]"
    (is "_ ⟹ ?P ∨ ?Q ∨ ?R")
  assumes B: "(WHILE b DO c, s, p) →*{cfs @ [cf]} cf'"
  shows
   "cf' = (WHILE b DO c, s, p) ∧
      flow (cfs @ [cf]) = [] ∨
    bval b s ∧ (c;; WHILE b DO c, s, p) →*{tl (cfs @ [cf])} cf' ∧
      flow (cfs @ [cf]) = ⟨bvars b⟩ # flow (tl (cfs @ [cf])) ∨
    ¬ bval b s ∧ cf' = (SKIP, s, p) ∧
      flow (cfs @ [cf]) = [⟨bvars b⟩]"
    (is "_ ∨ ?T")
proof -
  {
    assume
      C: "(WHILE b DO c, s, p) →*{cfs} cf" and
      D: "cf → cf'"
    assume "?P ∨ ?Q ∨ ?R"
    hence ?T
    proof (rule disjE, erule_tac [2] disjE)
      assume ?P
      moreover from this have "(WHILE b DO c, s, p) → cf'"
        using D by simp
      ultimately show ?thesis
        using C by (auto dest: small_stepsl_cons
         simp: tl_append flow_cons split: list.split)
    next
      assume ?Q
      with D show ?thesis
        by (auto simp: tl_append flow_cons split: list.split)
    next
      assume ?R
      with D show ?thesis
        by blast
    qed
  }
  with A and B show ?thesis
    by simp
qed

lemma small_stepsl_while:
 "(WHILE b DO c, s, p) →*{cfs} cf ⟹
    cf = (WHILE b DO c, s, p) ∧
      flow cfs = [] ∨
    bval b s ∧ (c;; WHILE b DO c, s, p) →*{tl cfs} cf ∧
      flow cfs = ⟨bvars b⟩ # flow (tl cfs) ∨
    ¬ bval b s ∧ cf = (SKIP, s, p) ∧
      flow cfs = [⟨bvars b⟩]"
by (induction "(WHILE b DO c, s, p)" cfs cf rule: small_stepsl.induct,
 force simp: flow_def, rule small_stepsl_while_1)


lemma small_steps_in_flow_1:
 "⟦(c, s, f, vs, ws) → (c', s', f', vs', ws');
    vs'' = vs' @ drop (length vs') vs''⟧ ⟹
  vs'' = vs @ drop (length vs) vs''"
by (induction "(c, s, f, vs, ws)" "(c', s', f', vs', ws')"
 arbitrary: c c' s s' f f' vs vs' ws ws' rule: small_step.induct,
 auto elim: ssubst)

lemma small_steps_in_flow:
 "(c, s, f, vs, ws) →* (c', s', f', vs', ws') ⟹
    vs' = vs @ drop (length vs) vs'"
by (induction "(c, s, f, vs, ws)" "(c', s', f', vs', ws')"
 arbitrary: c c' s s' f f' vs vs' ws ws' rule: star.induct,
 auto intro: small_steps_in_flow_1)


lemma small_steps_out_flow_1:
 "⟦(c, s, f, vs, ws) → (c', s', f', vs', ws');
    ws'' = ws' @ drop (length ws') ws''⟧ ⟹
  ws'' = ws @ drop (length ws) ws''"
by (induction "(c, s, f, vs, ws)" "(c', s', f', vs', ws')"
 arbitrary: c c' s s' f f' vs vs' ws ws' rule: small_step.induct,
 auto elim: ssubst)

lemma small_steps_out_flow:
 "(c, s, f, vs, ws) →* (c', s', f', vs', ws') ⟹
    ws' = ws @ drop (length ws) ws'"
by (induction "(c, s, f, vs, ws)" "(c', s', f', vs', ws')"
 arbitrary: c c' s s' f f' vs vs' ws ws' rule: star.induct,
 auto intro: small_steps_out_flow_1)


lemma small_stepsl_in_flow_1:
  assumes
    A: "(c, s, f, vs, ws) →*{cfs} (c', s', f', vs @ vs', ws')" and
    B: "(c', s', f', vs @ vs', ws') → (c'', s'', f'', vs'', ws'')"
  shows "vs'' = vs @ vs' @
    in_flow (flow [(c', s', f', vs @ vs', ws')]) (vs @ vs') f"
using small_stepsl_stream [OF A] and B
by (induction "[c']" arbitrary: c' c'' rule: flow_aux.induct,
 auto simp: flow_def in_flow_one)

lemma small_stepsl_in_flow:
 "(c, s, f, vs, ws) →*{cfs} (c', s', f', vs', ws') ⟹
    vs' = vs @ in_flow (flow cfs) vs f"
by (induction "(c, s, f, vs, ws)" cfs "(c', s', f', vs', ws')"
 arbitrary: c' s' f' vs' ws' rule: small_stepsl.induct, simp add: flow_def,
 auto intro: small_stepsl_in_flow_1 simp: flow_append in_flow_append)


lemma small_stepsl_run_flow_1:
  assumes
    A: "(c, s, f, vs, ws) →*{cfs}
      (c', run_flow (flow cfs) vs s f, f', vs', ws')" and
    B: "(c', run_flow (flow cfs) vs s f, f', vs', ws') →
      (c'', s'', f'', vs'', ws'')"
  shows "s'' = run_flow (flow [(c', run_flow (flow cfs) vs s f, f', vs', ws')])
    (vs @ in_flow (flow cfs) vs f) (run_flow (flow cfs) vs s f) f"
using small_stepsl_stream [OF A] and small_stepsl_in_flow [OF A] and B
by (induction "[c']" arbitrary: c' c'' rule: flow_aux.induct,
 auto simp: flow_def run_flow_one)

lemma small_stepsl_run_flow:
 "(c, s, f, vs, ws) →*{cfs} (c', s', f', vs', ws') ⟹
    s' = run_flow (flow cfs) vs s f"
by (induction "(c, s, f, vs, ws)" cfs "(c', s', f', vs', ws')"
 arbitrary: c' s' f' vs' ws' rule: small_stepsl.induct, simp add: flow_def,
 auto intro: small_stepsl_run_flow_1 simp: flow_append run_flow_append)


lemma small_stepsl_out_flow_1:
  assumes
    A: "(c, s, f, vs, ws) →*{cfs} (c', s', f', vs', ws @ ws')" and
    B: "(c', s', f', vs', ws @ ws') → (c'', s'', f'', vs'', ws'')"
  shows "ws'' = ws @ ws' @
    out_flow (flow [(c', s', f', vs', ws @ ws')]) (vs @ in_flow (flow cfs) vs f)
      (run_flow (flow cfs) vs s f) f"
using small_stepsl_run_flow [OF A] and B
by (induction "[c']" arbitrary: c' c'' rule: flow_aux.induct,
 auto simp: flow_def out_flow_one)

lemma small_stepsl_out_flow:
 "(c, s, f, vs, ws) →*{cfs} (c', s', f', vs', ws') ⟹
    ws' = ws @ out_flow (flow cfs) vs s f"
by (induction "(c, s, f, vs, ws)" cfs "(c', s', f', vs', ws')"
 arbitrary: c' s' f' vs' ws' rule: small_stepsl.induct, simp add: flow_def,
 auto intro: small_stepsl_out_flow_1 simp: flow_append out_flow_append)


lemma small_steps_inputs:
  assumes
    A: "(c, s, f, vs⇩0, ws⇩0) →*{cfs⇩1} (c⇩0, s⇩1, f, vs⇩1, ws⇩1)" and
    B: "(c⇩1, s⇩1, f, vs⇩1, ws⇩1) →*{cfs⇩2} (c⇩2, s⇩2, f, vs⇩2, ws⇩2)" and
    C: "(c, s', f', vs⇩0', ws⇩0') →* (c⇩0', s⇩1', f', vs⇩1', ws⇩1')" and
    D: "(c⇩1', s⇩1', f', vs⇩1', ws⇩1') →* (c⇩2', s⇩2', f', vs⇩2', ws⇩2')" and
    E: "map fst [p←drop (length vs⇩0) vs⇩1. P p] =
      map fst [p←drop (length vs⇩0') vs⇩1'. P p]" and
    F: "map fst [p←drop (length vs⇩1) vs⇩2. P p] =
      map fst [p←drop (length vs⇩1') vs⇩2'. P p]"
  shows "map fst [p←drop (length vs⇩0) vs⇩2. P p] =
    map fst [p←drop (length vs⇩0') vs⇩2'. P p]"
proof -
  have G: "vs⇩1 = vs⇩0 @ drop (length vs⇩0) vs⇩1"
    using small_stepsl_steps [OF A] by (rule small_steps_in_flow)
  have "vs⇩2 = vs⇩1 @ drop (length vs⇩1) vs⇩2"
    using small_stepsl_steps [OF B] by (rule small_steps_in_flow)
  hence H: "vs⇩2 = vs⇩0 @ drop (length vs⇩0) vs⇩1 @ drop (length vs⇩1) vs⇩2"
    by (subst (asm) G, simp)
  have I: "vs⇩1' = vs⇩0' @ drop (length vs⇩0') vs⇩1'"
    using C by (rule small_steps_in_flow)
  have "vs⇩2' = vs⇩1' @ drop (length vs⇩1') vs⇩2'"
    using D by (rule small_steps_in_flow)
  hence J: "vs⇩2' = vs⇩0' @ drop (length vs⇩0') vs⇩1' @ drop (length vs⇩1') vs⇩2'"
    by (subst (asm) I, simp)
  from E and F show ?thesis
    by (subst H, subst J, simp)
qed

lemma small_steps_outputs:
  assumes
    A: "(c, s, f, vs⇩0, ws⇩0) →*{cfs⇩1} (c⇩0, s⇩1, f, vs⇩1, ws⇩1)" and
    B: "(c⇩1, s⇩1, f, vs⇩1, ws⇩1) →*{cfs⇩2} (c⇩2, s⇩2, f, vs⇩2, ws⇩2)" and
    C: "(c, s', f', vs⇩0', ws⇩0') →* (c⇩0', s⇩1', f', vs⇩1', ws⇩1')" and
    D: "(c⇩1', s⇩1', f', vs⇩1', ws⇩1') →* (c⇩2', s⇩2', f', vs⇩2', ws⇩2')" and
    E: "[p←drop (length ws⇩0) ws⇩1. P p] =
      [p←drop (length ws⇩0') ws⇩1'. P p]" and
    F: "[p←drop (length ws⇩1) ws⇩2. P p] =
      [p←drop (length ws⇩1') ws⇩2'. P p]"
  shows "[p←drop (length ws⇩0) ws⇩2. P p] =
    [p←drop (length ws⇩0') ws⇩2'. P p]"
proof -
  have G: "ws⇩1 = ws⇩0 @ drop (length ws⇩0) ws⇩1"
    using small_stepsl_steps [OF A] by (rule small_steps_out_flow)
  have "ws⇩2 = ws⇩1 @ drop (length ws⇩1) ws⇩2"
    using small_stepsl_steps [OF B] by (rule small_steps_out_flow)
  hence H: "ws⇩2 = ws⇩0 @ drop (length ws⇩0) ws⇩1 @ drop (length ws⇩1) ws⇩2"
    by (subst (asm) G, simp)
  have I: "ws⇩1' = ws⇩0' @ drop (length ws⇩0') ws⇩1'"
    using C by (rule small_steps_out_flow)
  have "ws⇩2' = ws⇩1' @ drop (length ws⇩1') ws⇩2'"
    using D by (rule small_steps_out_flow)
  hence J: "ws⇩2' = ws⇩0' @ drop (length ws⇩0') ws⇩1' @ drop (length ws⇩1') ws⇩2'"
    by (subst (asm) I, simp)
  from E and F show ?thesis
    by (subst H, subst J, simp)
qed


subsection "Local context proofs"

context noninterf
begin


lemma no_upd_sources:
 "no_upd cs X ⟹ ∀x ∈ X. x ∈ sources cs vs s f x"
by (induction cs rule: rev_induct, auto simp: no_upd_append
 split: com_flow.split)

lemma sources_aux_append:
 "sources_aux cs vs s f x ⊆ sources_aux (cs @ cs') vs s f x"
by (induction cs' rule: rev_induct, simp, subst append_assoc [symmetric],
 auto simp del: append_assoc split: com_flow.split)

lemma sources_out_append:
 "sources_out cs vs s f x ⊆ sources_out (cs @ cs') vs s f x"
by (induction cs' rule: rev_induct, simp, subst append_assoc [symmetric],
 auto simp del: append_assoc split: com_flow.split)

lemma sources_aux_sources:
 "sources_aux cs vs s f x ⊆ sources cs vs s f x"
by (induction cs rule: rev_induct, auto split: com_flow.split)

lemma sources_aux_sources_out:
 "sources_aux cs vs s f x ⊆ sources_out cs vs s f x"
by (induction cs rule: rev_induct, auto split: com_flow.split)

lemma sources_aux_observe_hd_1:
 "∀y ∈ X. s: dom y ↝ dom x ⟹ X ⊆ sources_aux [⟨X⟩] vs s f x"
by (subst append_Nil [symmetric], subst sources_aux.simps, auto)

lemma sources_aux_observe_hd_2:
 "⟦∀y ∈ X. s: dom y ↝ dom x ⟹ X ⊆ sources_aux (⟨X⟩ # xs) vs s f x;
    ∀y ∈ X. s: dom y ↝ dom x⟧ ⟹
  X ⊆ sources_aux (⟨X⟩ # xs @ [x']) vs s f x"
by (subst append_Cons [symmetric], subst sources_aux.simps,
 auto split: com_flow.split)

lemma sources_aux_observe_hd:
 "∀y ∈ X. s: dom y ↝ dom x ⟹ X ⊆ sources_aux (⟨X⟩ # cs) vs s f x"
by (induction cs rule: rev_induct,
 erule sources_aux_observe_hd_1, rule sources_aux_observe_hd_2)

lemma sources_aux_bval:
  assumes
    A: "S ⊆ {x. s = t (⊆ sources_aux (⟨bvars b⟩ # cs) vs s f x)}" and
    B: "s ∈ Univ A (⊆ state ∩ X)" and
    C: "bval b s ≠ bval b t"
  shows "Univ? A X: bvars b ↝| S"
proof -
  have "¬ s = t (⊆ bvars b)"
    using A and C by (erule_tac contrapos_nn, auto dest: bvars_bval)
  hence "∀x ∈ S. ¬ bvars b ⊆ sources_aux (⟨bvars b⟩ # cs) vs s f x"
    using A by blast
  hence D: "{s}: bvars b ↝| S"
    by (fastforce dest: sources_aux_observe_hd)
  {
    fix r y
    assume "r ∈ A" and "y ∈ S"
    moreover assume "s = r (⊆ state ∩ X)" and "state ⊆ X"
    hence "interf s = interf r"
      by (blast intro: interf_state)
    ultimately have "A: bvars b ↝| {y}"
      using D by fastforce
  }
  with B and D show ?thesis
    by (fastforce simp: univ_states_if_def)
qed

lemma ok_flow_aux_degen:
  assumes A: "∄S. S ≠ {} ∧ S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_aux cs vs⇩1 s⇩1 f x)}"
  shows "∀c⇩2' t⇩2 vs⇩2' ws⇩2'.
    ok_flow_aux_1 c⇩1 c⇩2 c⇩2' s⇩1 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' vs⇩2 vs⇩2' ws⇩1' ws⇩2' cs ∧
    ok_flow_aux_2 s⇩1 s⇩2 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' cs ∧
    ok_flow_aux_3 s⇩1 t⇩1 f f' vs⇩1 vs⇩1' ws⇩1 ws⇩1' ws⇩2 ws⇩2' cs"
    (is "∀c⇩2' t⇩2 vs⇩2' ws⇩2'. ?P1 c⇩2' t⇩2 vs⇩2' ws⇩2' ∧ ?P2 t⇩2 ∧ ?P3 ws⇩2'")
proof clarify
  fix c⇩2' t⇩2 vs⇩2' ws⇩2'
  {
    fix S
    assume "S ≠ {}" and "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_aux cs vs⇩1 s⇩1 f x)}"
    hence "?P1 c⇩2' t⇩2 vs⇩2' ws⇩2'"
      using A by blast
  }
  moreover {
    fix S
    assume "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources cs vs⇩1 s⇩1 f x)}"
    moreover have "∀x. sources_aux cs vs⇩1 s⇩1 f x ⊆ sources cs vs⇩1 s⇩1 f x"
      by (blast intro: subsetD [OF sources_aux_sources])
    ultimately have "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_aux cs vs⇩1 s⇩1 f x)}"
      by blast
    moreover assume "S ≠ {}"
    ultimately have "?P2 t⇩2"
      using A by blast
  }
  moreover {
    fix S
    assume "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_out cs vs⇩1 s⇩1 f x)}"
    moreover have "∀x. sources_aux cs vs⇩1 s⇩1 f x ⊆ sources_out cs vs⇩1 s⇩1 f x"
      by (blast intro: subsetD [OF sources_aux_sources_out])
    ultimately have "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_aux cs vs⇩1 s⇩1 f x)}"
      by blast
    moreover assume "S ≠ {}"
    ultimately have "?P3 ws⇩2'"
      using A by blast
  }
  ultimately show "?P1 c⇩2' t⇩2 vs⇩2' ws⇩2' ∧ ?P2 t⇩2 ∧ ?P3 ws⇩2'"
    by auto
qed


lemma tags_aux_append:
 "tags_aux cs vs s f x ⊆ tags_aux (cs @ cs') vs s f x"
by (induction cs' rule: rev_induct, simp, subst append_assoc [symmetric],
 auto simp del: append_assoc split: com_flow.split)

lemma tags_out_append:
 "tags_out cs vs s f x ⊆ tags_out (cs @ cs') vs s f x"
by (induction cs' rule: rev_induct, simp, subst append_assoc [symmetric],
 auto simp del: append_assoc split: com_flow.split)

lemma tags_aux_tags:
 "tags_aux cs vs s f x ⊆ tags cs vs s f x"
by (induction cs rule: rev_induct, auto split: com_flow.split)

lemma tags_aux_tags_out:
 "tags_aux cs vs s f x ⊆ tags_out cs vs s f x"
by (induction cs rule: rev_induct, auto split: com_flow.split)


lemma tags_ubound_1:
  assumes
    A: "(y, Suc (length [c←cs. c = IN y] + n)) ∈ tags_aux cs vs s f x" and
    B: "⋀z n. y = z ⟹
      (z, length [c←cs. c = IN z] + n) ∉ tags_aux cs vs s f x"
  shows False
proof -
  have "(y, length [c←cs. c = IN y] + Suc n) ∉ tags_aux cs vs s f x"
    using B by blast
  thus ?thesis
    using A by simp
qed

lemma tags_ubound_2:
  assumes
    A: "(y, Suc (length [c←cs. c = IN y] + n)) ∈ tags cs vs s f x" and
    B: "⋀z n. y = z ⟹ z ≠ x ⟹
      (z, length [c←cs. c = IN z] + n) ∉ tags cs vs s f x" and
    C: "y ≠ x"
  shows False
proof -
  have "(y, length [c←cs. c = IN y] + Suc n) ∉ tags cs vs s f x"
    using B and C by blast
  thus ?thesis
    using A by simp
qed

lemma tags_ubound:
 "(y, length [c←cs. c = IN y] + n) ∉ tags cs vs s f x"
and tags_aux_ubound:
 "(y, length [c←cs. c = IN y] + n) ∉ tags_aux cs vs s f x"
by (induction cs vs s f x and cs vs s f x arbitrary: n and n
 rule: tags_induct, auto intro: tags_ubound_1 tags_ubound_2
 split: if_split_asm com_flow.split_asm)


lemma tags_out_ubound_1:
  assumes
    A: "(y, Suc (length [c←cs. c = IN y] + n)) ∈ tags_out cs vs s f x" and
    B: "⋀z n. y = z ⟹
      (z, length [c←cs. c = IN z] + n) ∉ tags_out cs vs s f x"
  shows False
proof -
  have "(y, length [c←cs. c = IN y] + Suc n) ∉ tags_out cs vs s f x"
    using B by blast
  thus ?thesis
    using A by simp
qed

lemma tags_out_ubound:
 "(y, length [c←cs. c = IN y] + n) ∉ tags_out cs vs s f x"
by (induction cs vs s f x arbitrary: n rule: tags_out.induct, auto
 intro: notE [OF tags_ubound] tags_out_ubound_1
 split: if_split_asm com_flow.split_asm)


lemma tags_less:
 "(y, n) ∈ tags cs vs s f x ⟹ n < length [c←cs. c = IN y]"
  apply (rule ccontr)
  apply (drule add_diff_inverse_nat)
  apply (drule ssubst, assumption)
by (simp add: tags_ubound)

lemma tags_aux_less:
 "(y, n) ∈ tags_aux cs vs s f x ⟹ n < length [c←cs. c = IN y]"
  apply (rule ccontr)
  apply (drule add_diff_inverse_nat)
  apply (drule ssubst, assumption)
by (simp add: tags_aux_ubound)

lemma tags_out_less:
 "(y, n) ∈ tags_out cs vs s f x ⟹ n < length [c←cs. c = IN y]"
  apply (rule ccontr)
  apply (drule add_diff_inverse_nat)
  apply (drule ssubst, assumption)
by (simp add: tags_out_ubound)


lemma sources_observe_tl_1:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹ z = x ⟹
      sources_aux cs vs s f x ⊆ sources_aux (⟨X⟩ # cs) vs s f x" and
    B: "⋀z a b w. c = (z ::= a :: com_flow) ⟹ z = x ⟹
      sources cs vs s f w ⊆ sources (⟨X⟩ # cs) vs s f w" and
    C: "⋀z a. c = (z ::= a :: com_flow) ⟹ z ≠ x ⟹
      sources cs vs s f x ⊆ sources (⟨X⟩ # cs) vs s f x" and
    D: "⋀z. c = (IN z :: com_flow) ⟹ z = x ⟹
      sources_aux cs vs s f x ⊆ sources_aux (⟨X⟩ # cs) vs s f x" and
    E: "⋀z. c = (IN z :: com_flow) ⟹ z ≠ x ⟹
      sources cs vs s f x ⊆ sources (⟨X⟩ # cs) vs s f x" and
    F: "⋀z. c = (OUT z :: com_flow) ⟹
      sources cs vs s f x ⊆ sources (⟨X⟩ # cs) vs s f x" and
    G: "⋀Y b w. c = ⟨Y⟩ ⟹
      sources cs vs s f w ⊆ sources (⟨X⟩ # cs) vs s f w"
  shows "sources (cs @ [c]) vs s f x ⊆ sources (⟨X⟩ # cs @ [c]) vs s f x"
    (is "_ ⊆ ?F c")
  apply (subst sources.simps)
  apply (split com_flow.split)
  apply (rule conjI)
  subgoal
  proof -
    show "∀z a. c = z ::= a ⟶ (if z = x
      then sources_aux cs vs s f x ∪ ⋃ {sources cs vs s f y | y.
        run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ avars a}
      else sources cs vs s f x) ⊆ ?F c"
      (is "∀_ a. _ ⟶ (if _ then ?A ∪ ?G a else ?B) ⊆ _")
    proof (clarify, split if_split_asm)
      fix y z a
      assume H: "c = z ::= a" and I: "z = x"
      hence "?F (z ::= a) = sources_aux (⟨X⟩ # cs) vs s f x ∪
        ⋃ {sources (⟨X⟩ # cs) vs s f y | y.
          run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ avars a}"
        (is "_ = ?A' ∪ ?G' a")
        by (simp only: append_Cons [symmetric] sources.simps,
         simp add: run_flow_observe)
      moreover assume "y ∈ ?A ∪ ?G a"
      moreover {
        assume "y ∈ ?A"
        hence "y ∈ ?A'"
          using A and H and I by blast
      }
      moreover {
        assume "y ∈ ?G a"
        hence "y ∈ ?G' a"
          using B and H and I by blast
      }
      ultimately show "y ∈ ?F (z ::= a)"
        by blast
    next
      fix y z a
      assume "c = z ::= a" and "z ≠ x"
      moreover from this have "?F (z ::= a) = sources (⟨X⟩ # cs) vs s f x"
        by (simp only: append_Cons [symmetric] sources.simps, simp)
      moreover assume "y ∈ ?B"
      ultimately show "y ∈ ?F (z ::= a)"
        using C by blast
    qed
  qed
  apply (rule conjI)
  subgoal
  proof -
    show "∀z. c = IN z ⟶ (if z = x
      then sources_aux cs vs s f x else sources cs vs s f x) ⊆ ?F c"
      (is "∀_. _ ⟶ (if _ then ?A else ?B) ⊆ _")
    proof (clarify, split if_split_asm)
      fix y z
      assume "c = IN z" and "z = x"
      moreover from this have "?F (IN z) = sources_aux (⟨X⟩ # cs) vs s f x"
        by (simp only: append_Cons [symmetric] sources.simps, simp)
      moreover assume "y ∈ ?A"
      ultimately show "y ∈ ?F (IN z)"
        using D by blast
    next
      fix y z
      assume "c = IN z" and "z ≠ x"
      moreover from this have "?F (IN z) = sources (⟨X⟩ # cs) vs s f x"
        by (simp only: append_Cons [symmetric] sources.simps, simp)
      moreover assume "y ∈ ?B"
      ultimately show "y ∈ ?F (IN z)"
        using E by blast
    qed
  qed
  apply (rule conjI)
  subgoal by (simp only: append_Cons [symmetric] sources.simps, simp add: F)
  subgoal
  proof -
    show "∀Y. c = ⟨Y⟩ ⟶ sources cs vs s f x ∪
      ⋃ {sources cs vs s f y | y.
        run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ Y} ⊆ ?F c"
      (is "∀Y. _ ⟶ ?A ∪ ?G Y ⊆ _")
    proof clarify
      fix y Y
      assume H: "c = ⟨Y⟩"
      hence "?F (⟨Y⟩) = sources (⟨X⟩ # cs) vs s f x ∪
        ⋃ {sources (⟨X⟩ # cs) vs s f y | y.
          run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ Y}"
        (is "_ = ?A' ∪ ?G' Y")
        by (simp only: append_Cons [symmetric] sources.simps,
         simp add: run_flow_observe)
      moreover assume "y ∈ ?A ∪ ?G Y"
      moreover {
        assume "y ∈ ?A"
        hence "y ∈ ?A'"
          using G and H by blast
      }
      moreover {
        assume "y ∈ ?G Y"
        hence "y ∈ ?G' Y"
          using G and H by blast
      }
      ultimately show "y ∈ ?F (⟨Y⟩)"
        by blast
    qed
  qed
  done 

lemma sources_observe_tl_2:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      sources_aux cs vs s f x ⊆ sources_aux (⟨X⟩ # cs) vs s f x" and
    B: "⋀z. c = (IN z :: com_flow) ⟹
      sources_aux cs vs s f x ⊆ sources_aux (⟨X⟩ # cs) vs s f x" and
    C: "⋀z. c = (OUT z :: com_flow) ⟹
      sources_aux cs vs s f x ⊆ sources_aux (⟨X⟩ # cs) vs s f x" and
    D: "⋀Y. c = ⟨Y⟩ ⟹
      sources_aux cs vs s f x ⊆ sources_aux (⟨X⟩ # cs) vs s f x" and
    E: "⋀Y b w. c = ⟨Y⟩ ⟹
      sources cs vs s f w ⊆ sources (⟨X⟩ # cs) vs s f w"
  shows "sources_aux (cs @ [c]) vs s f x ⊆
    sources_aux (⟨X⟩ # cs @ [c]) vs s f x"
    (is "_ ⊆ ?F c")
  apply (subst sources_aux.simps)
  apply (split com_flow.split)
  apply (rule conjI)
   defer
   apply (rule conjI)
    defer
    apply (rule conjI)
     defer
  subgoal
  proof -
    show "∀Y. c = ⟨Y⟩ ⟶ sources_aux cs vs s f x ∪
      ⋃ {sources cs vs s f y | y.
        run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ Y} ⊆ ?F c"
      (is "∀Y. _ ⟶ ?A ∪ ?G Y ⊆ _")
    proof clarify
      fix y Y
      assume F: "c = ⟨Y⟩"
      hence "?F (⟨Y⟩) = sources_aux (⟨X⟩ # cs) vs s f x ∪
        ⋃ {sources (⟨X⟩ # cs) vs s f y | y.
          run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ Y}"
        (is "_ = ?A' ∪ ?G' Y")
        by (simp only: append_Cons [symmetric] sources_aux.simps,
         simp add: run_flow_observe)
      moreover assume "y ∈ ?A ∪ ?G Y"
      moreover {
        assume "y ∈ ?A"
        hence "y ∈ ?A'"
          using D and F by blast
      }
      moreover {
        assume "y ∈ ?G Y"
        hence "y ∈ ?G' Y"
          using E and F by blast
      }
      ultimately show "y ∈ ?F (⟨Y⟩)"
        by blast
    qed
  qed
by (simp only: append_Cons [symmetric] sources_aux.simps, simp add: A B C)+

lemma sources_observe_tl:
 "sources cs vs s f x ⊆ sources (⟨X⟩ # cs) vs s f x"
and sources_aux_observe_tl:
 "sources_aux cs vs s f x ⊆ sources_aux (⟨X⟩ # cs) vs s f x"
   apply (induction cs vs s f x and cs vs s f x rule: sources_induct)
  subgoal by (erule sources_observe_tl_1, assumption+)
  subgoal by (simp, subst append_Nil [symmetric], subst sources.simps, simp)
  subgoal by (erule sources_observe_tl_2, assumption+)
  by simp


lemma sources_out_observe_tl_1:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      sources_out cs vs s f x ⊆ sources_out (⟨X⟩ # cs) vs s f x" and
    B: "⋀z. c = (IN z :: com_flow) ⟹
      sources_out cs vs s f x ⊆ sources_out (⟨X⟩ # cs) vs s f x" and
    C: "⋀z. c = (OUT z :: com_flow) ⟹
      sources_out cs vs s f x ⊆ sources_out (⟨X⟩ # cs) vs s f x" and
    D: "⋀Y. c = ⟨Y⟩ ⟹
      sources_out cs vs s f x ⊆ sources_out (⟨X⟩ # cs) vs s f x"
  shows "sources_out (cs @ [c]) vs s f x ⊆
    sources_out (⟨X⟩ # cs @ [c]) vs s f x"
    (is "_ ⊆ ?F c")
  apply (subst sources_out.simps)
  apply (split com_flow.split)
  apply (rule conjI)
   defer
   apply (rule conjI)
    defer
  subgoal
  proof
    show "∀z. c = OUT z ⟶ sources_out cs vs s f x ∪
      (if z = x then sources cs vs s f x else {}) ⊆ ?F c"
      (is "∀_. _ ⟶ ?A ∪ (if _ then ?B else _) ⊆ _")
    proof (clarify, split if_split_asm)
      fix y z
      assume E: "c = OUT z" and F: "z = x"
      assume "y ∈ ?A ∪ ?B"
      moreover {
        assume "y ∈ ?A"
        hence "y ∈ sources_out (⟨X⟩ # cs) vs s f x"
          using C and E by blast
      }
      moreover {
        assume "y ∈ ?B"
        hence "y ∈ sources (⟨X⟩ # cs) vs s f x"
          by (rule subsetD [OF sources_observe_tl])
      }
      ultimately show "y ∈ ?F (OUT z)"
        using F by (simp only: append_Cons [symmetric] sources_out.simps,
         auto)
    next
      fix y z
      assume "c = OUT z" and "y ∈ sources_out cs vs s f x ∪ {}"
      hence "y ∈ sources_out (⟨X⟩ # cs) vs s f x"
        using C by blast
      thus "y ∈ ?F (OUT z)"
        by (simp only: append_Cons [symmetric] sources_out.simps, simp)
    qed
  next
    show "∀Y. c = ⟨Y⟩ ⟶ sources_out cs vs s f x ∪
      ⋃ {sources cs vs s f y | y.
        run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ Y} ⊆ ?F c"
      (is "∀Y. _ ⟶ ?A ∪ ?G Y ⊆ _")
    proof clarify
      fix y Y
      assume E: "c = ⟨Y⟩"
      assume "y ∈ ?A ∪ ?G Y"
      moreover {
        assume "y ∈ ?A"
        hence "y ∈ sources_out (⟨X⟩ # cs) vs s f x"
          using D and E by blast
      }
      moreover {
        assume "y ∈ ?G Y"
        hence "y ∈ ⋃ {sources (⟨X⟩ # cs) vs s f y | y.
          run_flow (⟨X⟩ # cs) vs s f: dom y ↝ dom x ∧ y ∈ Y}"
          by (auto intro: subsetD [OF sources_observe_tl]
           simp: run_flow_observe)
      }
      ultimately show "y ∈ ?F (⟨Y⟩)"
        by (simp only: append_Cons [symmetric] sources_out.simps, auto)
    qed
  qed
by (simp only: append_Cons [symmetric] sources_out.simps, simp add: A B)+

lemma sources_out_observe_tl:
 "sources_out cs vs s f x ⊆ sources_out (⟨X⟩ # cs) vs s f x"
by (induction cs vs s f x rule: sources_out.induct,
 erule sources_out_observe_tl_1, simp_all)


lemma tags_observe_tl_1:
 "⟦⋀z a. c = z ::= a ⟹ z = x ⟹
    tags_aux (⟨X⟩ # cs) vs s f x = tags_aux cs vs s f x;
  ⋀z a b w. c = z ::= a ⟹ z = x ⟹
    tags (⟨X⟩ # cs) vs s f w = tags cs vs s f w;
  ⋀z a. c = z ::= a ⟹ z ≠ x ⟹
    tags (⟨X⟩ # cs) vs s f x = tags cs vs s f x;
  ⋀z. c = IN z ⟹ z = x ⟹
    tags_aux (⟨X⟩ # cs) vs s f x = tags_aux cs vs s f x;
  ⋀z. c = IN z ⟹ z ≠ x ⟹
    tags (⟨X⟩ # cs) vs s f x = tags cs vs s f x;
  ⋀z. c = OUT z ⟹
    tags (⟨X⟩ # cs) vs s f x = tags cs vs s f x;
  ⋀Y b w. c = ⟨Y⟩ ⟹
    tags (⟨X⟩ # cs) vs s f w = tags cs vs s f w⟧ ⟹
  tags (⟨X⟩ # cs @ [c]) vs s f x = tags (cs @ [c]) vs s f x"
by (subst tags.simps, split com_flow.split, simp_all only: append_Cons
 [symmetric] tags.simps, simp_all add: run_flow_observe)

lemma tags_observe_tl_2:
 "⟦⋀z a. c = z ::= a ⟹
    tags_aux (⟨X⟩ # cs) vs s f x = tags_aux cs vs s f x;
  ⋀z. c = IN z ⟹
    tags_aux (⟨X⟩ # cs) vs s f x = tags_aux cs vs s f x;
  ⋀z. c = OUT z ⟹
    tags_aux (⟨X⟩ # cs) vs s f x = tags_aux cs vs s f x;
  ⋀Y. c = ⟨Y⟩ ⟹
    tags_aux (⟨X⟩ # cs) vs s f x = tags_aux cs vs s f x;
  ⋀Y b w. c = ⟨Y⟩ ⟹
    tags (⟨X⟩ # cs) vs s f w = tags cs vs s f w⟧ ⟹
  tags_aux (⟨X⟩ # cs @ [c]) vs s f x = tags_aux (cs @ [c]) vs s f x"
by (subst tags_aux.simps, split com_flow.split, simp_all only: append_Cons
 [symmetric] tags_aux.simps, simp_all add: run_flow_observe)

lemma tags_observe_tl:
 "tags (⟨X⟩ # cs) vs s f x = tags cs vs s f x"
and tags_aux_observe_tl:
 "tags_aux (⟨X⟩ # cs) vs s f x = tags_aux cs vs s f x"
   apply (induction cs vs s f x and cs vs s f x rule: tags_induct)
  subgoal by (erule tags_observe_tl_1, assumption+)
  subgoal by (subst append_Nil [symmetric], subst tags.simps tags_aux.simps, simp)
  subgoal by (erule tags_observe_tl_2, assumption+)
  subgoal by (subst append_Nil [symmetric], subst tags.simps tags_aux.simps, simp)
  done

lemma tags_out_observe_tl_1:
 "⟦⋀z a. c = z ::= a ⟹
    tags_out (⟨X⟩ # cs) vs s f x = tags_out cs vs s f x;
  ⋀z. c = IN z ⟹
    tags_out (⟨X⟩ # cs) vs s f x = tags_out cs vs s f x;
  ⋀z. c = OUT z ⟹
    tags_out (⟨X⟩ # cs) vs s f x = tags_out cs vs s f x;
  ⋀Y. c = ⟨Y⟩ ⟹
    tags_out (⟨X⟩ # cs) vs s f x = tags_out cs vs s f x⟧ ⟹
  tags_out (⟨X⟩ # cs @ [c]) vs s f x = tags_out (cs @ [c]) vs s f x"
by (subst tags_out.simps, split com_flow.split, simp_all only: append_Cons
 [symmetric] tags_out.simps, simp_all add: run_flow_observe tags_observe_tl)

lemma tags_out_observe_tl:
 "tags_out (⟨X⟩ # cs) vs s f x = tags_out cs vs s f x"
  apply (induction cs vs s f x rule: tags_out.induct)
   apply (erule tags_out_observe_tl_1, assumption+)
by (subst append_Nil [symmetric], subst tags_out.simps, simp)


lemma tags_sources_1:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹ z = x ⟹
      (y, n) ∈ tags_aux cs vs s f x ⟹
        let m = Suc (Max {k. k ≤ length cs ∧
          length [c←take k cs. c = IN y] ≤ n})
        in y ∈ sources_aux (drop m cs) (vs @ in_flow (take m cs) vs f)
          (run_flow (take m cs) vs s f) f x"
      (is "⋀_ _. _ ⟹ _ ⟹ _ ⟹ let m = Suc (Max (?F cs)) in
        _ ∈ sources_aux _ (?G m cs) (?H m cs) _ _")
  assumes
    B: "⋀z a b w. c = (z ::= a :: com_flow) ⟹ z = x ⟹
      (y, n) ∈ tags cs vs s f w ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources (drop m cs) (?G m cs) (?H m cs) f w" and
    C: "⋀z a. c = (z ::= a :: com_flow) ⟹ z ≠ x ⟹
      (y, n) ∈ tags cs vs s f x ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources (drop m cs) (?G m cs) (?H m cs) f x" and
    D: "⋀z. c = (IN z :: com_flow) ⟹ z = x ⟹
      (y, n) ∈ tags_aux cs vs s f x ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources_aux (drop m cs) (?G m cs) (?H m cs) f x" and
    E: "⋀z. c = (IN z :: com_flow) ⟹ z ≠ x ⟹
      (y, n) ∈ tags cs vs s f x ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources (drop m cs) (?G m cs) (?H m cs) f x" and
    F: "⋀z. c = (OUT z :: com_flow) ⟹
      (y, n) ∈ tags cs vs s f x ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources (drop m cs) (?G m cs) (?H m cs) f x" and
    G: "⋀X b w. c = ⟨X⟩ ⟹
      (y, n) ∈ tags cs vs s f w ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources (drop m cs) (?G m cs) (?H m cs) f w" and
    H: "(y, n) ∈ tags (cs @ [c]) vs s f x"
  shows "let m = Suc (Max (?F (cs @ [c]))) in
    y ∈ sources (drop m (cs @ [c])) (?G m (cs @ [c])) (?H m (cs @ [c])) f x"
proof -
  have I: "n < length [c←cs @ [c]. c = IN y]"
    using H by (rule tags_less)
  hence "?F (cs @ [c]) = ?F cs"
    using le_Suc_eq by auto
  moreover have "c ≠ IN y ∨ n < length [c←cs. c = IN y] ⟹
    Suc (Max (?F cs)) ≤ length cs"
    (is "_ ⟹ ?m ≤ _")
    using I by (subst Suc_le_eq, subst Max_less_iff,
     auto elim: le_neq_implies_less)
  ultimately have J: "c ≠ IN y ∨ n < length [c←cs. c = IN y] ⟹
    take (Suc (Max (?F (cs @ [c])))) (cs @ [c]) = take ?m cs ∧
    drop (Suc (Max (?F (cs @ [c])))) (cs @ [c]) = drop ?m cs @ [c]"
    by simp
  from H show ?thesis
  proof (subst (asm) tags.simps, split com_flow.split_asm)
    fix z a
    assume K: "c = z ::= a"
    show "(y, n) ∈ (if z = x
      then tags_aux cs vs s f x ∪ ⋃ {tags cs vs s f y | y.
        run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ avars a}
      else tags cs vs s f x) ⟹ ?thesis"
      (is "_ ∈ (if _ then ?A ∪ ?B else ?C) ⟹ _")
    proof (split if_split_asm)
      assume L: "z = x" and "(y, n) ∈ ?A ∪ ?B"
      moreover {
        assume "(y, n) ∈ ?A"
        hence "y ∈ sources_aux (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
          using A and K and L by simp
      }
      moreover {
        assume "(y, n) ∈ ?B"
        hence "y ∈ ⋃ {sources (drop ?m cs) (?G ?m cs) (?H ?m cs) f y | y.
          run_flow (drop ?m cs) (?G ?m cs) (?H ?m cs) f:
            dom y ↝ dom x ∧ y ∈ avars a}"
          using B and K and L by (auto simp: run_flow_append [symmetric])
      }
      ultimately show ?thesis
        using J and K by auto
    next
      assume "z ≠ x" and "(y, n) ∈ ?C"
      moreover from this have
       "y ∈ sources (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
        using C and K by simp
      ultimately show ?thesis
        using J and K by simp
    qed
  next
    fix z
    assume K: "c = IN z"
    show "(y, n) ∈ (if z = x
      then insert (x, length [c←cs. c = IN x]) (tags_aux cs vs s f x)
      else tags cs vs s f x) ⟹ ?thesis"
      (is "_ ∈ (if _ then insert _ ?A else ?B) ⟹ _")
    proof (split if_split_asm, erule insertE)
      assume "(y, n) = (x, length [c←cs. c = IN x])" and "z = x"
      moreover from this have "Max (?F (cs @ [c])) = length cs"
        using K by (subst Max_eq_iff, auto elim: le_SucE)
      ultimately show ?thesis
        by simp
    next
      assume L: "(y, n) ∈ tags_aux cs vs s f x" and "z = x"
      moreover from this have
       "y ∈ sources_aux (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
        using D and K by simp
      moreover have "n < length [c←cs. c = IN y]"
        using L by (rule tags_aux_less)
      ultimately show ?thesis
        using J and K by simp
    next
      assume L: "(y, n) ∈ tags cs vs s f x" and "z ≠ x"
      moreover from this have
       "y ∈ sources (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
        using E and K by simp
      moreover have "n < length [c←cs. c = IN y]"
        using L by (rule tags_less)
      ultimately show ?thesis
        using J and K by simp
    qed
  next
    fix z
    assume "c = OUT z" and "(y, n) ∈ tags cs vs s f x"
    moreover from this have
     "y ∈ sources (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
      using F by simp
    ultimately show ?thesis
      using J by simp
  next
    fix X
    assume K: "c = ⟨X⟩"
    assume "(y, n) ∈ tags cs vs s f x ∪ ⋃ {tags cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ X}"
      (is "_ ∈ ?A ∪ ?B")
    moreover {
      assume "(y, n) ∈ ?A"
      hence "y ∈ sources (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
        using G and K by simp
    }
    moreover {
      assume "(y, n) ∈ ?B"
      hence "y ∈ ⋃ {sources (drop ?m cs) (?G ?m cs) (?H ?m cs) f y | y.
        run_flow (drop ?m cs) (?G ?m cs) (?H ?m cs) f:
          dom y ↝ dom x ∧ y ∈ X}"
        using G and K by (auto simp: run_flow_append [symmetric])
    }
    ultimately show ?thesis
      using J and K by auto
  qed
qed

lemma tags_sources_2:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      (y, n) ∈ tags_aux cs vs s f x ⟹
        let m = Suc (Max {k. k ≤ length cs ∧
          length [c←take k cs. c = IN y] ≤ n})
        in y ∈ sources_aux (drop m cs) (vs @ in_flow (take m cs) vs f)
          (run_flow (take m cs) vs s f) f x"
      (is "⋀_ _. _ ⟹ _ ⟹ let m = Suc (Max (?F cs)) in
        _ ∈ sources_aux _ (?G m cs) (?H m cs) _ _")
  assumes
    B: "⋀z. c = (IN z :: com_flow) ⟹
      (y, n) ∈ tags_aux cs vs s f x ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources_aux (drop m cs) (?G m cs) (?H m cs) f x" and
    C: "⋀z. c = (OUT z :: com_flow) ⟹
      (y, n) ∈ tags_aux cs vs s f x ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources_aux (drop m cs) (?G m cs) (?H m cs) f x" and
    D: "⋀X. c = ⟨X⟩ ⟹
      (y, n) ∈ tags_aux cs vs s f x ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources_aux (drop m cs) (?G m cs) (?H m cs) f x" and
    E: "⋀X b w. c = ⟨X⟩ ⟹
      (y, n) ∈ tags cs vs s f w ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources (drop m cs) (?G m cs) (?H m cs) f w" and
    F: "(y, n) ∈ tags_aux (cs @ [c]) vs s f x"
  shows "let m = Suc (Max (?F (cs @ [c]))) in
    y ∈ sources_aux (drop m (cs @ [c])) (?G m (cs @ [c])) (?H m (cs @ [c])) f x"
proof -
  have G: "n < length [c←cs @ [c]. c = IN y]"
    using F by (rule tags_aux_less)
  hence "?F (cs @ [c]) = ?F cs"
    using le_Suc_eq by auto
  moreover have "c ≠ IN y ∨ n < length [c←cs. c = IN y] ⟹
    Suc (Max (?F cs)) ≤ length cs"
    (is "_ ⟹ ?m ≤ _")
    using G by (subst Suc_le_eq, subst Max_less_iff,
     auto elim: le_neq_implies_less)
  ultimately have H: "c ≠ IN y ∨ n < length [c←cs. c = IN y] ⟹
    take (Suc (Max (?F (cs @ [c])))) (cs @ [c]) = take ?m cs ∧
    drop (Suc (Max (?F (cs @ [c])))) (cs @ [c]) = drop ?m cs @ [c]"
    by simp
  from F show ?thesis
  proof (subst (asm) tags_aux.simps, split com_flow.split_asm)
    fix z a
    assume "c = z ::= a" and "(y, n) ∈ tags_aux cs vs s f x"
    moreover from this have
     "y ∈ sources_aux (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
      using A by simp
    ultimately show ?thesis
      using H by simp
  next
    fix z
    assume "c = IN z" and I: "(y, n) ∈ tags_aux cs vs s f x"
    moreover from this have
     "y ∈ sources_aux (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
      using B by simp
    moreover have "n < length [c←cs. c = IN y]"
      using I by (rule tags_aux_less)
    ultimately show ?thesis
      using H by simp
  next
    fix z
    assume "c = OUT z" and "(y, n) ∈ tags_aux cs vs s f x"
    moreover from this have
     "y ∈ sources_aux (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
      using C by simp
    ultimately show ?thesis
      using H by simp
  next
    fix X
    assume I: "c = ⟨X⟩"
    assume "(y, n) ∈ tags_aux cs vs s f x ∪ ⋃ {tags cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ X}"
      (is "_ ∈ ?A ∪ ?B")
    moreover {
      assume "(y, n) ∈ ?A"
      hence "y ∈ sources_aux (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
        using D and I by simp
    }
    moreover {
      assume "(y, n) ∈ ?B"
      hence "y ∈ ⋃ {sources (drop ?m cs) (?G ?m cs) (?H ?m cs) f y | y.
        run_flow (drop ?m cs) (?G ?m cs) (?H ?m cs) f:
          dom y ↝ dom x ∧ y ∈ X}"
        using E and I by (auto simp: run_flow_append [symmetric])
    }
    ultimately show ?thesis
      using H and I by auto
  qed
qed

lemma tags_sources:
 "(y, n) ∈ tags cs vs s f x ⟹
    let m = Suc (Max {k. k ≤ length cs ∧
      length [c←take k cs. c = IN y] ≤ n})
    in y ∈ sources (drop m cs) (vs @ in_flow (take m cs) vs f)
      (run_flow (take m cs) vs s f) f x"
and tags_aux_sources_aux:
 "(y, n) ∈ tags_aux cs vs s f x ⟹
    let m = Suc (Max {k. k ≤ length cs ∧
      length [c←take k cs. c = IN y] ≤ n})
    in y ∈ sources_aux (drop m cs) (vs @ in_flow (take m cs) vs f)
      (run_flow (take m cs) vs s f) f x"
by (induction cs vs s f x and cs vs s f x rule: tags_induct,
 erule_tac [3] tags_sources_2, erule tags_sources_1, simp_all)


lemma tags_out_sources_out_1:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      (y, n) ∈ tags_out cs vs s f x ⟹
        let m = Suc (Max {k. k ≤ length cs ∧
          length [c←take k cs. c = IN y] ≤ n})
        in y ∈ sources_out (drop m cs) (vs @ in_flow (take m cs) vs f)
          (run_flow (take m cs) vs s f) f x"
      (is "⋀_ _. _ ⟹ _ ⟹ let m = Suc (Max (?F cs)) in
        _ ∈ sources_out _ (?G m cs) (?H m cs) _ _")
  assumes
    B: "⋀z. c = (IN z :: com_flow) ⟹
      (y, n) ∈ tags_out cs vs s f x ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources_out (drop m cs) (?G m cs) (?H m cs) f x" and
    C: "⋀z. c = (OUT z :: com_flow) ⟹
      (y, n) ∈ tags_out cs vs s f x ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources_out (drop m cs) (?G m cs) (?H m cs) f x" and
    D: "⋀X. c = ⟨X⟩ ⟹
      (y, n) ∈ tags_out cs vs s f x ⟹ let m = Suc (Max (?F cs)) in
        y ∈ sources_out (drop m cs) (?G m cs) (?H m cs) f x" and
    E: "(y, n) ∈ tags_out (cs @ [c]) vs s f x"
  shows "let m = Suc (Max (?F (cs @ [c]))) in
    y ∈ sources_out (drop m (cs @ [c])) (?G m (cs @ [c])) (?H m (cs @ [c])) f x"
proof -
  have F: "n < length [c←cs @ [c]. c = IN y]"
    using E by (rule tags_out_less)
  hence "?F (cs @ [c]) = ?F cs"
    using le_Suc_eq by auto
  moreover have "c ≠ IN y ∨ n < length [c←cs. c = IN y] ⟹
    Suc (Max (?F cs)) ≤ length cs"
    (is "_ ⟹ ?m ≤ _")
    using F by (subst Suc_le_eq, subst Max_less_iff,
     auto elim: le_neq_implies_less)
  ultimately have G: "c ≠ IN y ∨ n < length [c←cs. c = IN y] ⟹
    take (Suc (Max (?F (cs @ [c])))) (cs @ [c]) = take ?m cs ∧
    drop (Suc (Max (?F (cs @ [c])))) (cs @ [c]) = drop ?m cs @ [c]"
    by simp
  from E show ?thesis
  proof (subst (asm) tags_out.simps, split com_flow.split_asm)
    fix z a
    assume "c = z ::= a" and "(y, n) ∈ tags_out cs vs s f x"
    moreover from this have
     "y ∈ sources_out (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
      using A by simp
    ultimately show ?thesis
      using G by simp
  next
    fix z
    assume "c = IN z" and H: "(y, n) ∈ tags_out cs vs s f x"
    moreover from this have
     "y ∈ sources_out (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
      using B by simp
    moreover have "n < length [c←cs. c = IN y]"
      using H by (rule tags_out_less)
    ultimately show ?thesis
      using G by simp
  next
    fix z
    assume H: "c = OUT z"
    show "(y, n) ∈ tags_out cs vs s f x ∪
      (if z = x then tags cs vs s f x else {}) ⟹ ?thesis"
      (is "_ ∈ ?A ∪ (if _ then ?B else _) ⟹ _")
    proof (split if_split_asm)
      assume "z = x" and "(y, n) ∈ ?A ∪ ?B"
      moreover {
        assume "(y, n) ∈ ?A"
        hence "y ∈ sources_out (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
          using C and H by simp
      }
      moreover {
        assume "(y, n) ∈ ?B"
        hence "y ∈ sources (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
          by (auto dest: tags_sources)
      }
      ultimately show ?thesis
        using G and H by auto
    next
      assume "(y, n) ∈ ?A ∪ {}"
      moreover from this have
       "y ∈ sources_out (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
        using C and H by simp
      ultimately show ?thesis
        using G and H by simp
    qed
  next
    fix X
    assume H: "c = ⟨X⟩"
    assume "(y, n) ∈ tags_out cs vs s f x ∪ ⋃ {tags cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ X}"
      (is "_ ∈ ?A ∪ ?B")
    moreover {
      assume "(y, n) ∈ ?A"
      hence "y ∈ sources_out (drop ?m cs) (?G ?m cs) (?H ?m cs) f x"
        using D and H by simp
    }
    moreover {
      assume "(y, n) ∈ ?B"
      hence "y ∈ ⋃ {sources (drop ?m cs) (?G ?m cs) (?H ?m cs) f y | y.
        run_flow (drop ?m cs) (?G ?m cs) (?H ?m cs) f:
          dom y ↝ dom x ∧ y ∈ X}"
        by (fastforce dest: tags_sources simp: run_flow_append [symmetric])
    }
    ultimately show ?thesis
      using G and H by auto
  qed
qed

lemma tags_out_sources_out:
 "(y, n) ∈ tags_out cs vs s f x ⟹
    let m = Suc (Max {k. k ≤ length cs ∧
      length [c←take k cs. c = IN y] ≤ n})
    in y ∈ sources_out (drop m cs) (vs @ in_flow (take m cs) vs f)
      (run_flow (take m cs) vs s f) f x"
by (induction cs vs s f x rule: tags_out.induct,
 erule tags_out_sources_out_1, simp_all)


lemma sources_member_1:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹ z = x ⟹
      y ∈ sources_aux cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
        sources cs vs s f y ⊆ sources_aux (cs @ cs') vs s f x"
      (is "⋀_ _. _ ⟹ _ ⟹ _ ∈ sources_aux _ ?vs' ?s' _ _ ⟹
        _ ⊆ sources_aux ?cs _ _ _ _")
  assumes
    B: "⋀z a b w. c = (z ::= a :: com_flow) ⟹ z = x ⟹
      y ∈ sources cs' ?vs' ?s' f w ⟹
        sources cs vs s f y ⊆ sources ?cs vs s f w" and
    C: "⋀z a. c = (z ::= a :: com_flow) ⟹ z ≠ x ⟹
      y ∈ sources cs' ?vs' ?s' f x ⟹
        sources cs vs s f y ⊆ sources ?cs vs s f x" and
    D: "⋀z. c = (IN z :: com_flow) ⟹ z = x ⟹
      y ∈ sources_aux cs' ?vs' ?s' f x ⟹
        sources cs vs s f y ⊆ sources_aux ?cs vs s f x" and
    E: "⋀z. c = (IN z :: com_flow) ⟹ z ≠ x ⟹
      y ∈ sources cs' ?vs' ?s' f x ⟹
        sources cs vs s f y ⊆ sources ?cs vs s f x" and
    F: "⋀z. c = (OUT z :: com_flow) ⟹
      y ∈ sources cs' ?vs' ?s' f x ⟹
        sources cs vs s f y ⊆ sources ?cs vs s f x" and
    G: "⋀X b w. c = ⟨X⟩ ⟹
      y ∈ sources cs' ?vs' ?s' f w ⟹
        sources cs vs s f y ⊆ sources ?cs vs s f w"
  shows "y ∈ sources (cs' @ [c]) ?vs' ?s' f x ⟹
    sources cs vs s f y ⊆ sources (cs @ cs' @ [c]) vs s f x"
proof (subst (asm) sources.simps, split com_flow.split_asm)
  fix z a
  assume H: "c = z ::= a"
  show "y ∈ (if z = x
    then sources_aux cs' ?vs' ?s' f x ∪ ⋃ {sources cs' ?vs' ?s' f w | w.
      run_flow cs' ?vs' ?s' f: dom w ↝ dom x ∧ w ∈ avars a}
    else sources cs' ?vs' ?s' f x) ⟹ ?thesis"
    (is "_ ∈ (if _ then ?A ∪ ?B else ?C) ⟹ _")
  proof (split if_split_asm)
    assume I: "z = x" and "y ∈ ?A ∪ ?B"
    moreover {
      assume "y ∈ ?A"
      hence "sources cs vs s f y ⊆ sources_aux ?cs vs s f x"
        using A and H and I by simp
    }
    moreover {
      assume "y ∈ ?B"
      hence "sources cs vs s f y ⊆ ⋃ {sources ?cs vs s f w | w.
        run_flow ?cs vs s f: dom w ↝ dom x ∧ w ∈ avars a}"
        using B and H and I by (fastforce simp: run_flow_append)
    }
    ultimately show ?thesis
      using H by (simp only: append_assoc [symmetric] sources.simps, auto)
  next
    assume "z ≠ x" and "y ∈ ?C"
    moreover from this have "sources cs vs s f y ⊆ sources ?cs vs s f x"
      using C and H by simp
    ultimately show ?thesis
      using H by (simp only: append_assoc [symmetric] sources.simps, auto)
  qed
next
  fix z
  assume H: "c = IN z"
  show "y ∈ (if z = x
    then sources_aux cs' ?vs' ?s' f x
    else sources cs' ?vs' ?s' f x) ⟹ ?thesis"
    (is "_ ∈ (if _ then ?A else ?B) ⟹ _")
  proof (split if_split_asm)
    assume "z = x" and "y ∈ ?A"
    moreover from this have "sources cs vs s f y ⊆ sources_aux ?cs vs s f x"
      using D and H by simp
    ultimately show ?thesis
      using H by (simp only: append_assoc [symmetric] sources.simps, auto)
  next
    assume "z ≠ x" and "y ∈ ?B"
    moreover from this have "sources cs vs s f y ⊆ sources ?cs vs s f x"
      using E and H by simp
    ultimately show ?thesis
      using H by (simp only: append_assoc [symmetric] sources.simps, auto)
  qed
next
  fix z
  assume "c = OUT z" and "y ∈ sources cs' ?vs' ?s' f x"
  moreover from this have "sources cs vs s f y ⊆ sources ?cs vs s f x"
    using F by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] sources.simps, auto)
next
  fix X
  assume H: "c = ⟨X⟩"
  assume "y ∈ sources cs' ?vs' ?s' f x ∪ ⋃ {sources cs' ?vs' ?s' f w | w.
    run_flow cs' ?vs' ?s' f: dom w ↝ dom x ∧ w ∈ X}"
    (is "_ ∈ ?A ∪ ?B")
  moreover {
    assume "y ∈ ?A"
    hence "sources cs vs s f y ⊆ sources ?cs vs s f x"
      using G and H by simp
  }
  moreover {
    assume "y ∈ ?B"
    hence "sources cs vs s f y ⊆ ⋃ {sources ?cs vs s f w | w.
      run_flow ?cs vs s f: dom w ↝ dom x ∧ w ∈ X}"
      using G and H by (auto simp: run_flow_append)
  }
  ultimately show ?thesis
    using H by (simp only: append_assoc [symmetric] sources.simps, auto)
qed

lemma sources_member_2:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      y ∈ sources_aux cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
        sources cs vs s f y ⊆ sources_aux (cs @ cs') vs s f x"
      (is "⋀_ _. _ ⟹ _ ∈ sources_aux _ ?vs' ?s' _ _ ⟹
        _ ⊆ sources_aux ?cs _ _ _ _")
  assumes
    B: "⋀z. c = (IN z :: com_flow) ⟹
      y ∈ sources_aux cs' ?vs' ?s' f x ⟹
        sources cs vs s f y ⊆ sources_aux ?cs vs s f x" and
    C: "⋀z. c = (OUT z :: com_flow) ⟹
      y ∈ sources_aux cs' ?vs' ?s' f x ⟹
        sources cs vs s f y ⊆ sources_aux ?cs vs s f x" and
    D: "⋀X. c = ⟨X⟩ ⟹
      y ∈ sources_aux cs' ?vs' ?s' f x ⟹
        sources cs vs s f y ⊆ sources_aux ?cs vs s f x" and
    E: "⋀X b w. c = ⟨X⟩ ⟹
      y ∈ sources cs' ?vs' ?s' f w ⟹
        sources cs vs s f y ⊆ sources ?cs vs s f w"
  shows "y ∈ sources_aux (cs' @ [c]) ?vs' ?s' f x ⟹
    sources cs vs s f y ⊆ sources_aux (cs @ cs' @ [c]) vs s f x"
proof (subst (asm) sources_aux.simps, split com_flow.split_asm)
  fix z a
  assume "c = z ::= a" and "y ∈ sources_aux cs' ?vs' ?s' f x"
  moreover from this have "sources cs vs s f y ⊆ sources_aux ?cs vs s f x"
    using A by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] sources_aux.simps, auto)
next
  fix z
  assume "c = IN z" and "y ∈ sources_aux cs' ?vs' ?s' f x"
  moreover from this have "sources cs vs s f y ⊆ sources_aux ?cs vs s f x"
    using B by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] sources_aux.simps, auto)
next
  fix z
  assume "c = OUT z" and "y ∈ sources_aux cs' ?vs' ?s' f x"
  moreover from this have "sources cs vs s f y ⊆ sources_aux ?cs vs s f x"
    using C by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] sources_aux.simps, auto)
next
  fix X
  assume F: "c = ⟨X⟩"
  assume "y ∈ sources_aux cs' ?vs' ?s' f x ∪ ⋃ {sources cs' ?vs' ?s' f w | w.
    run_flow cs' ?vs' ?s' f: dom w ↝ dom x ∧ w ∈ X}"
    (is "_ ∈ ?A ∪ ?B")
  moreover {
    assume "y ∈ ?A"
    hence "sources cs vs s f y ⊆ sources_aux ?cs vs s f x"
      using D and F by simp
  }
  moreover {
    assume "y ∈ ?B"
    hence "sources cs vs s f y ⊆ ⋃ {sources ?cs vs s f w | w.
      run_flow ?cs vs s f: dom w ↝ dom x ∧ w ∈ X}"
      using E and F by (auto simp: run_flow_append)
  }
  ultimately show ?thesis
    using F by (simp only: append_assoc [symmetric] sources_aux.simps, auto)
qed

lemma sources_member:
 "y ∈ sources cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
    sources cs vs s f y ⊆ sources (cs @ cs') vs s f x"
and sources_aux_member:
 "y ∈ sources_aux cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
    sources cs vs s f y ⊆ sources_aux (cs @ cs') vs s f x"
by (induction cs' vs s f x and cs' vs s f x rule: sources_induct,
 erule_tac [3] sources_member_2, erule sources_member_1, simp_all)


lemma sources_out_member_1:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      y ∈ sources_out cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
        sources cs vs s f y ⊆ sources_out (cs @ cs') vs s f x"
      (is "⋀_ _. _ ⟹ _ ∈ sources_out _ ?vs' ?s' _ _ ⟹
        _ ⊆ sources_out ?cs _ _ _ _")
  assumes
    B: "⋀z. c = (IN z :: com_flow) ⟹
      y ∈ sources_out cs' ?vs' ?s' f x ⟹
        sources cs vs s f y ⊆ sources_out ?cs vs s f x" and
    C: "⋀z. c = (OUT z :: com_flow) ⟹
      y ∈ sources_out cs' ?vs' ?s' f x ⟹
        sources cs vs s f y ⊆ sources_out ?cs vs s f x" and
    D: "⋀X. c = ⟨X⟩ ⟹
      y ∈ sources_out cs' ?vs' ?s' f x ⟹
        sources cs vs s f y ⊆ sources_out ?cs vs s f x"
  shows "y ∈ sources_out (cs' @ [c]) ?vs' ?s' f x ⟹
    sources cs vs s f y ⊆ sources_out (cs @ cs' @ [c]) vs s f x"
proof (subst (asm) sources_out.simps, split com_flow.split_asm)
  fix z a
  assume "c = z ::= a" and "y ∈ sources_out cs' ?vs' ?s' f x"
  moreover from this have "sources cs vs s f y ⊆ sources_out ?cs vs s f x"
    using A by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] sources_out.simps, auto)
next
  fix z
  assume "c = IN z" and "y ∈ sources_out cs' ?vs' ?s' f x"
  moreover from this have "sources cs vs s f y ⊆ sources_out ?cs vs s f x"
    using B by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] sources_out.simps, auto)
next
  fix z
  assume E: "c = OUT z"
  show "y ∈ sources_out cs' ?vs' ?s' f x ∪
    (if z = x then sources cs' ?vs' ?s' f x else {}) ⟹ ?thesis"
    (is "_ ∈ ?A ∪ (if _ then ?B else _) ⟹ _")
  proof (split if_split_asm)
    assume "z = x" and "y ∈ ?A ∪ ?B"
    moreover {
      assume "y ∈ ?A"
      hence "sources cs vs s f y ⊆ sources_out ?cs vs s f x"
        using C and E by simp
    }
    moreover {
      assume "y ∈ ?B"
      hence "sources cs vs s f y ⊆ sources ?cs vs s f x"
        by (rule sources_member)
    }
    ultimately show ?thesis
      using E by (simp only: append_assoc [symmetric] sources_out.simps, auto)
  next
    assume "y ∈ ?A ∪ {}"
    moreover from this have "sources cs vs s f y ⊆ sources_out ?cs vs s f x"
      using C and E by simp
    ultimately show ?thesis
      using E by (simp only: append_assoc [symmetric] sources_out.simps, auto)
  qed
next
  fix X
  assume E: "c = ⟨X⟩"
  assume "y ∈ sources_out cs' ?vs' ?s' f x ∪ ⋃ {sources cs' ?vs' ?s' f w | w.
    run_flow cs' ?vs' ?s' f: dom w ↝ dom x ∧ w ∈ X}"
    (is "_ ∈ ?A ∪ ?B")
  moreover {
    assume "y ∈ ?A"
    hence "sources cs vs s f y ⊆ sources_out ?cs vs s f x"
      using D and E by simp
  }
  moreover {
    assume "y ∈ ?B"
    hence "sources cs vs s f y ⊆ ⋃ {sources ?cs vs s f w | w.
      run_flow ?cs vs s f: dom w ↝ dom x ∧ w ∈ X}"
      by (auto dest: sources_member simp: run_flow_append)
  }
  ultimately show ?thesis
    using E by (simp only: append_assoc [symmetric] sources_out.simps, auto)
qed

lemma sources_out_member:
 "y ∈ sources_out cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
    sources cs vs s f y ⊆ sources_out (cs @ cs') vs s f x"
by (induction cs' vs s f x rule: sources_out.induct,
 erule sources_out_member_1, simp_all)


lemma tags_member_1:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹ z = x ⟹
      y ∈ sources_aux cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
        tags cs vs s f y ⊆ tags_aux (cs @ cs') vs s f x"
      (is "⋀_ _. _ ⟹ _ ⟹ _ ∈ sources_aux _ ?vs' ?s' _ _ ⟹
        _ ⊆ tags_aux ?cs _ _ _ _")
  assumes
    B: "⋀z a b w. c = (z ::= a :: com_flow) ⟹ z = x ⟹
      y ∈ sources cs' ?vs' ?s' f w ⟹
        tags cs vs s f y ⊆ tags ?cs vs s f w" and
    C: "⋀z a. c = (z ::= a :: com_flow) ⟹ z ≠ x ⟹
      y ∈ sources cs' ?vs' ?s' f x ⟹
        tags cs vs s f y ⊆ tags ?cs vs s f x" and
    D: "⋀z. c = (IN z :: com_flow) ⟹ z = x ⟹
      y ∈ sources_aux cs' ?vs' ?s' f x ⟹
        tags cs vs s f y ⊆ tags_aux ?cs vs s f x" and
    E: "⋀z. c = (IN z :: com_flow) ⟹ z ≠ x ⟹
      y ∈ sources cs' ?vs' ?s' f x ⟹
        tags cs vs s f y ⊆ tags ?cs vs s f x" and
    F: "⋀z. c = (OUT z :: com_flow) ⟹
      y ∈ sources cs' ?vs' ?s' f x ⟹
        tags cs vs s f y ⊆ tags ?cs vs s f x" and
    G: "⋀X b w. c = ⟨X⟩ ⟹
      y ∈ sources cs' ?vs' ?s' f w ⟹
        tags cs vs s f y ⊆ tags ?cs vs s f w"
  shows "y ∈ sources (cs' @ [c]) ?vs' ?s' f x ⟹
    tags cs vs s f y ⊆ tags (cs @ cs' @ [c]) vs s f x"
proof (subst (asm) sources.simps, split com_flow.split_asm)
  fix z a
  assume H: "c = z ::= a"
  show "y ∈ (if z = x
    then sources_aux cs' ?vs' ?s' f x ∪ ⋃ {sources cs' ?vs' ?s' f w | w.
      run_flow cs' ?vs' ?s' f: dom w ↝ dom x ∧ w ∈ avars a}
    else sources cs' ?vs' ?s' f x) ⟹ ?thesis"
    (is "_ ∈ (if _ then ?A ∪ ?B else ?C) ⟹ _")
  proof (split if_split_asm)
    assume I: "z = x" and "y ∈ ?A ∪ ?B"
    moreover {
      assume "y ∈ ?A"
      hence "tags cs vs s f y ⊆ tags_aux ?cs vs s f x"
        using A and H and I by simp
    }
    moreover {
      assume "y ∈ ?B"
      hence "tags cs vs s f y ⊆ ⋃ {tags ?cs vs s f w | w.
        run_flow ?cs vs s f: dom w ↝ dom x ∧ w ∈ avars a}"
        using B and H and I by (fastforce simp: run_flow_append)
    }
    ultimately show ?thesis
      using H by (simp only: append_assoc [symmetric] tags.simps, auto)
  next
    assume "z ≠ x" and "y ∈ ?C"
    moreover from this have "tags cs vs s f y ⊆ tags ?cs vs s f x"
      using C and H by simp
    ultimately show ?thesis
      using H by (simp only: append_assoc [symmetric] tags.simps, auto)
  qed
next
  fix z
  assume H: "c = IN z"
  show "y ∈ (if z = x
    then sources_aux cs' ?vs' ?s' f x
    else sources cs' ?vs' ?s' f x) ⟹ ?thesis"
    (is "_ ∈ (if _ then ?A else ?B) ⟹ _")
  proof (split if_split_asm)
    assume "z = x" and "y ∈ ?A"
    moreover from this have "tags cs vs s f y ⊆ tags_aux ?cs vs s f x"
      using D and H by simp
    ultimately show ?thesis
      using H by (simp only: append_assoc [symmetric] tags.simps, auto)
  next
    assume "z ≠ x" and "y ∈ ?B"
    moreover from this have "tags cs vs s f y ⊆ tags ?cs vs s f x"
      using E and H by simp
    ultimately show ?thesis
      using H by (simp only: append_assoc [symmetric] tags.simps, auto)
  qed
next
  fix z
  assume "c = OUT z" and "y ∈ sources cs' ?vs' ?s' f x"
  moreover from this have "tags cs vs s f y ⊆ tags ?cs vs s f x"
    using F by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] tags.simps, auto)
next
  fix X
  assume H: "c = ⟨X⟩"
  assume "y ∈ sources cs' ?vs' ?s' f x ∪ ⋃ {sources cs' ?vs' ?s' f w | w.
    run_flow cs' ?vs' ?s' f: dom w ↝ dom x ∧ w ∈ X}"
    (is "_ ∈ ?A ∪ ?B")
  moreover {
    assume "y ∈ ?A"
    hence "tags cs vs s f y ⊆ tags ?cs vs s f x"
      using G and H by simp
  }
  moreover {
    assume "y ∈ ?B"
    hence "tags cs vs s f y ⊆ ⋃ {tags ?cs vs s f w | w.
      run_flow ?cs vs s f: dom w ↝ dom x ∧ w ∈ X}"
      using G and H by (auto simp: run_flow_append)
  }
  ultimately show ?thesis
    using H by (simp only: append_assoc [symmetric] tags.simps, auto)
qed

lemma tags_member_2:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      y ∈ sources_aux cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
        tags cs vs s f y ⊆ tags_aux (cs @ cs') vs s f x"
      (is "⋀_ _. _ ⟹ _ ∈ sources_aux _ ?vs' ?s' _ _ ⟹
        _ ⊆ tags_aux ?cs _ _ _ _")
  assumes
    B: "⋀z. c = (IN z :: com_flow) ⟹
      y ∈ sources_aux cs' ?vs' ?s' f x ⟹
        tags cs vs s f y ⊆ tags_aux ?cs vs s f x" and
    C: "⋀z. c = (OUT z :: com_flow) ⟹
      y ∈ sources_aux cs' ?vs' ?s' f x ⟹
        tags cs vs s f y ⊆ tags_aux ?cs vs s f x" and
    D: "⋀X. c = ⟨X⟩ ⟹
      y ∈ sources_aux cs' ?vs' ?s' f x ⟹
        tags cs vs s f y ⊆ tags_aux ?cs vs s f x" and
    E: "⋀X b w. c = ⟨X⟩ ⟹
      y ∈ sources cs' ?vs' ?s' f w ⟹
        tags cs vs s f y ⊆ tags ?cs vs s f w"
  shows "y ∈ sources_aux (cs' @ [c]) ?vs' ?s' f x ⟹
    tags cs vs s f y ⊆ tags_aux (cs @ cs' @ [c]) vs s f x"
proof (subst (asm) sources_aux.simps, split com_flow.split_asm)
  fix z a
  assume "c = z ::= a" and "y ∈ sources_aux cs' ?vs' ?s' f x"
  moreover from this have "tags cs vs s f y ⊆ tags_aux ?cs vs s f x"
    using A by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] tags_aux.simps, auto)
next
  fix z
  assume "c = IN z" and "y ∈ sources_aux cs' ?vs' ?s' f x"
  moreover from this have "tags cs vs s f y ⊆ tags_aux ?cs vs s f x"
    using B by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] tags_aux.simps, auto)
next
  fix z
  assume "c = OUT z" and "y ∈ sources_aux cs' ?vs' ?s' f x"
  moreover from this have "tags cs vs s f y ⊆ tags_aux ?cs vs s f x"
    using C by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] tags_aux.simps, auto)
next
  fix X
  assume F: "c = ⟨X⟩"
  assume "y ∈ sources_aux cs' ?vs' ?s' f x ∪ ⋃ {sources cs' ?vs' ?s' f w | w.
    run_flow cs' ?vs' ?s' f: dom w ↝ dom x ∧ w ∈ X}"
    (is "_ ∈ ?A ∪ ?B")
  moreover {
    assume "y ∈ ?A"
    hence "tags cs vs s f y ⊆ tags_aux ?cs vs s f x"
      using D and F by simp
  }
  moreover {
    assume "y ∈ ?B"
    hence "tags cs vs s f y ⊆ ⋃ {tags ?cs vs s f w | w.
      run_flow ?cs vs s f: dom w ↝ dom x ∧ w ∈ X}"
      using E and F by (auto simp: run_flow_append)
  }
  ultimately show ?thesis
    using F by (simp only: append_assoc [symmetric] tags_aux.simps, auto)
qed

lemma tags_member:
 "y ∈ sources cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
    tags cs vs s f y ⊆ tags (cs @ cs') vs s f x"
and tags_aux_member:
 "y ∈ sources_aux cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
    tags cs vs s f y ⊆ tags_aux (cs @ cs') vs s f x"
by (induction cs' vs s f x and cs' vs s f x rule: tags_induct,
 erule_tac [3] tags_member_2, erule tags_member_1, simp_all)


lemma tags_out_member_1:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      y ∈ sources_out cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
        tags cs vs s f y ⊆ tags_out (cs @ cs') vs s f x"
      (is "⋀_ _. _ ⟹ _ ∈ sources_out _ ?vs' ?s' _ _ ⟹
        _ ⊆ tags_out ?cs _ _ _ _")
  assumes
    B: "⋀z. c = (IN z :: com_flow) ⟹
      y ∈ sources_out cs' ?vs' ?s' f x ⟹
        tags cs vs s f y ⊆ tags_out ?cs vs s f x" and
    C: "⋀z. c = (OUT z :: com_flow) ⟹
      y ∈ sources_out cs' ?vs' ?s' f x ⟹
        tags cs vs s f y ⊆ tags_out ?cs vs s f x" and
    D: "⋀X. c = ⟨X⟩ ⟹
      y ∈ sources_out cs' ?vs' ?s' f x ⟹
        tags cs vs s f y ⊆ tags_out ?cs vs s f x"
  shows "y ∈ sources_out (cs' @ [c]) ?vs' ?s' f x ⟹
    tags cs vs s f y ⊆ tags_out (cs @ cs' @ [c]) vs s f x"
proof (subst (asm) sources_out.simps, split com_flow.split_asm)
  fix z a
  assume "c = z ::= a" and "y ∈ sources_out cs' ?vs' ?s' f x"
  moreover from this have "tags cs vs s f y ⊆ tags_out ?cs vs s f x"
    using A by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] tags_out.simps, auto)
next
  fix z
  assume "c = IN z" and "y ∈ sources_out cs' ?vs' ?s' f x"
  moreover from this have "tags cs vs s f y ⊆ tags_out ?cs vs s f x"
    using B by simp
  ultimately show ?thesis
    by (simp only: append_assoc [symmetric] tags_out.simps, auto)
next
  fix z
  assume E: "c = OUT z"
  show "y ∈ sources_out cs' ?vs' ?s' f x ∪
    (if z = x then sources cs' ?vs' ?s' f x else {}) ⟹ ?thesis"
    (is "_ ∈ ?A ∪ (if _ then ?B else _) ⟹ _")
  proof (split if_split_asm)
    assume "z = x" and "y ∈ ?A ∪ ?B"
    moreover {
      assume "y ∈ ?A"
      hence "tags cs vs s f y ⊆ tags_out ?cs vs s f x"
        using C and E by simp
    }
    moreover {
      assume "y ∈ ?B"
      hence "tags cs vs s f y ⊆ tags ?cs vs s f x"
        by (rule tags_member)
    }
    ultimately show ?thesis
      using E by (simp only: append_assoc [symmetric] tags_out.simps, auto)
  next
    assume "y ∈ ?A ∪ {}"
    moreover from this have "tags cs vs s f y ⊆ tags_out ?cs vs s f x"
      using C and E by simp
    ultimately show ?thesis
      using E by (simp only: append_assoc [symmetric] tags_out.simps, auto)
  qed
next
  fix X
  assume E: "c = ⟨X⟩"
  assume "y ∈ sources_out cs' ?vs' ?s' f x ∪ ⋃ {sources cs' ?vs' ?s' f w | w.
    run_flow cs' ?vs' ?s' f: dom w ↝ dom x ∧ w ∈ X}"
    (is "_ ∈ ?A ∪ ?B")
  moreover {
    assume "y ∈ ?A"
    hence "tags cs vs s f y ⊆ tags_out ?cs vs s f x"
      using D and E by simp
  }
  moreover {
    assume "y ∈ ?B"
    hence "tags cs vs s f y ⊆ ⋃ {tags ?cs vs s f w | w.
      run_flow ?cs vs s f: dom w ↝ dom x ∧ w ∈ X}"
      by (auto dest: tags_member simp: run_flow_append)
  }
  ultimately show ?thesis
    using E by (simp only: append_assoc [symmetric] tags_out.simps, auto)
qed

lemma tags_out_member:
 "y ∈ sources_out cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x ⟹
    tags cs vs s f y ⊆ tags_out (cs @ cs') vs s f x"
by (induction cs' vs s f x rule: tags_out.induct,
 erule tags_out_member_1, simp_all)


lemma tags_suffix_1:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹ z = x ⟹
      tags_aux cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags_aux (cs @ cs') vs s f x}"
      (is "⋀_ _. _ ⟹ _ ⟹ tags_aux _ ?vs' ?s' _ _ = _")
  assumes
    B: "⋀z a b y. c = (z ::= a :: com_flow) ⟹ z = x ⟹
      tags cs' ?vs' ?s' f y =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags (cs @ cs') vs s f y}" and
    C: "⋀z a. c = (z ::= a :: com_flow) ⟹ z ≠ x ⟹
      tags cs' ?vs' ?s' f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags (cs @ cs') vs s f x}" and
    D: "⋀z. c = (IN z :: com_flow) ⟹ z = x ⟹
      tags_aux cs' ?vs' ?s' f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags_aux (cs @ cs') vs s f x}" and
    E: "⋀z. c = (IN z :: com_flow) ⟹ z ≠ x ⟹
      tags cs' ?vs' ?s' f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags (cs @ cs') vs s f x}" and
    F: "⋀z. c = (OUT z :: com_flow) ⟹
      tags cs' ?vs' ?s' f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags (cs @ cs') vs s f x}" and
    G: "⋀X b y. c = ⟨X⟩ ⟹
      tags cs' ?vs' ?s' f y =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags (cs @ cs') vs s f y}"
  shows "tags (cs' @ [c]) ?vs' ?s' f x =
    {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
      ∈ tags (cs @ cs' @ [c]) vs s f x}"
    (is "_ = {p. case p of (w, n) ⇒ ?P w n c}")
  apply (subst tags.simps)
  apply (split com_flow.split)
  apply (rule conjI)
  subgoal
  proof -
    show "∀z a. c = z ::= a ⟶ (if z = x
      then tags_aux cs' ?vs' ?s' f x ∪ ⋃ {tags cs' ?vs' ?s' f y | y.
        run_flow cs' ?vs' ?s' f: dom y ↝ dom x ∧ y ∈ avars a}
      else tags cs' ?vs' ?s' f x) =
      {(w, n). ?P w n c}"
      (is "∀_ a. _ ⟶ (if _ then ?A ∪ ?F a else ?B) = _")
      apply clarify
      apply (split if_split)
      apply (rule conjI)
      subgoal for z a
      proof
        assume H: "z = x" and I: "c = z ::= a"
        hence "?A = {(w, n). (w, length [c←cs. c = IN w] + n)
          ∈ tags_aux (cs @ cs') vs s f x}"
          using A by simp
        moreover have "∀y. tags cs' ?vs' ?s' f y = {(w, n).
          (w, length [c←cs. c = IN w] + n) ∈ tags (cs @ cs') vs s f y}"
          using B and H and I by simp
        hence "?F a = {(w, n). (w, length [c←cs. c = IN w] + n)
          ∈ ⋃ {tags (cs @ cs') vs s f y | y.
            run_flow cs' ?vs' ?s' f: dom y ↝ dom x ∧ y ∈ avars a}}"
          by blast
        ultimately show "?A ∪ ?F a = {(w, n). ?P w n (z ::= a)}"
          using H by (subst append_assoc [symmetric], subst tags.simps,
           auto simp: run_flow_append)
      qed
      subgoal for z a
      proof
        assume "z ≠ x" and "c = z ::= a"
        moreover from this have "?B = {(w, n).
          (w, length [c←cs. c = IN w] + n) ∈ tags (cs @ cs') vs s f x}"
          using C by simp
        ultimately show "?B = {(w, n). ?P w n (z ::= a)}"
          by (subst append_assoc [symmetric], subst tags.simps, simp)
      qed
      done
  qed
  apply (rule conjI)
  subgoal
  proof -
    show "∀z. c = IN z ⟶ (if z = x
      then insert (x, length [c←cs'. c = IN x]) (tags_aux cs' ?vs' ?s' f x)
      else tags cs' ?vs' ?s' f x) =
      {(w, n). ?P w n c}"
      (is "∀_. _ ⟶ (if _ then insert ?p ?A else ?B) = _")
      apply clarify
      apply (split if_split)
      apply (rule conjI)
      subgoal for z
      proof
        assume "z = x" and "c = IN z"
        moreover from this have "?A = {(w, n).
          (w, length [c←cs. c = IN w] + n) ∈ tags_aux (cs @ cs') vs s f x}"
          using D by simp
        ultimately show "insert ?p ?A = {(w, n). ?P w n (IN z)}"
          by (subst append_assoc [symmetric], subst tags.simps, auto)
      qed
      subgoal for z
      proof
        assume "z ≠ x" and "c = IN z"
        moreover from this have "?B = {(w, n).
          (w, length [c←cs. c = IN w] + n) ∈ tags (cs @ cs') vs s f x}"
          using E by simp
        ultimately show "?B = {(w, n). ?P w n (IN z)}"
          by (subst append_assoc [symmetric], subst tags.simps, simp)
      qed
      done
  qed
  apply (rule conjI)
  subgoal by (subst append_assoc [symmetric], subst tags.simps, simp add: F)
  subgoal
  proof -
    show "∀X. c = ⟨X⟩ ⟶
      tags cs' ?vs' ?s' f x ∪ ⋃ {tags cs' ?vs' ?s' f y | y.
        run_flow cs' ?vs' ?s' f: dom y ↝ dom x ∧ y ∈ X} =
      {(w, n). ?P w n c}"
      (is "∀X. _ ⟶ ?A ∪ ?F X = _")
    proof clarify
      fix X
      assume H: "c = ⟨X⟩"
      hence "?A = {(w, n). (w, length [c←cs. c = IN w] + n)
        ∈ tags (cs @ cs') vs s f x}"
        using G by simp
      moreover have "∀y. tags cs' ?vs' ?s' f y = {(w, n).
        (w, length [c←cs. c = IN w] + n) ∈ tags (cs @ cs') vs s f y}"
        using G and H by simp
      hence "?F X = {(w, n). (w, length [c←cs. c = IN w] + n)
        ∈ ⋃ {tags (cs @ cs') vs s f y | y.
          run_flow cs' ?vs' ?s' f: dom y ↝ dom x ∧ y ∈ X}}"
        by blast
      ultimately show "?A ∪ ?F X = {(w, n). ?P w n (⟨X⟩)}"
        by (subst append_assoc [symmetric], subst tags.simps,
         auto simp: run_flow_append)
    qed
  qed
  done

lemma tags_suffix_2:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      tags_aux cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags_aux (cs @ cs') vs s f x}"
      (is "⋀_ _. _ ⟹ tags_aux _ ?vs' ?s' _ _ = _")
  assumes
    B: "⋀z. c = (IN z :: com_flow) ⟹
      tags_aux cs' ?vs' ?s' f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags_aux (cs @ cs') vs s f x}" and
    C: "⋀z. c = (OUT z :: com_flow) ⟹
      tags_aux cs' ?vs' ?s' f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags_aux (cs @ cs') vs s f x}" and
    D: "⋀X. c = ⟨X⟩ ⟹
      tags_aux cs' ?vs' ?s' f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags_aux (cs @ cs') vs s f x}" and
    E: "⋀X b y. c = ⟨X⟩ ⟹
      tags cs' ?vs' ?s' f y =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags (cs @ cs') vs s f y}"
  shows "tags_aux (cs' @ [c]) ?vs' ?s' f x =
    {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
      ∈ tags_aux (cs @ cs' @ [c]) vs s f x}"
    (is "_ = {p. case p of (w, n) ⇒ ?P w n c}")
  apply (subst tags_aux.simps)
  apply (split com_flow.split)
  apply (rule conjI)
   defer
   apply (rule conjI)
    defer
    apply (rule conjI)
     defer
  subgoal
  proof -
    show "∀X. c = ⟨X⟩ ⟶
      tags_aux cs' ?vs' ?s' f x ∪ ⋃ {tags cs' ?vs' ?s' f y | y.
        run_flow cs' ?vs' ?s' f: dom y ↝ dom x ∧ y ∈ X} =
      {(w, n). ?P w n c}"
      (is "∀X. _ ⟶ ?A ∪ ?F X = _")
    proof clarify
      fix X
      assume F: "c = ⟨X⟩"
      hence "?A = {(w, n). (w, length [c←cs. c = IN w] + n)
        ∈ tags_aux (cs @ cs') vs s f x}"
        using D by simp
      moreover have "∀y. tags cs' ?vs' ?s' f y = {(w, n).
        (w, length [c←cs. c = IN w] + n) ∈ tags (cs @ cs') vs s f y}"
        using E and F by simp
      hence "?F X = {(w, n). (w, length [c←cs. c = IN w] + n)
        ∈ ⋃ {tags (cs @ cs') vs s f y | y.
          run_flow cs' ?vs' ?s' f: dom y ↝ dom x ∧ y ∈ X}}"
        by blast
      ultimately show "?A ∪ ?F X = {(w, n). ?P w n (⟨X⟩)}"
        by (subst append_assoc [symmetric], subst tags_aux.simps,
         auto simp: run_flow_append)
    qed
  qed
by (subst append_assoc [symmetric], subst tags_aux.simps, simp add: A B C)+

lemma tags_suffix:
 "tags cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x = {(w, n).
    (w, length [c←cs. c = IN w] + n) ∈ tags (cs @ cs') vs s f x}"
and tags_aux_suffix:
 "tags_aux cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x = {(w, n).
    (w, length [c←cs. c = IN w] + n) ∈ tags_aux (cs @ cs') vs s f x}"
by (induction cs' vs s f x and cs' vs s f x rule: tags_induct,
 erule_tac [3] tags_suffix_2, erule tags_suffix_1, simp_all
 add: tags_ubound tags_aux_ubound)


lemma tags_out_suffix_1:
  assumes
    A: "⋀z a. c = (z ::= a :: com_flow) ⟹
      tags_out cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags_out (cs @ cs') vs s f x}"
      (is "⋀_ _. _ ⟹ tags_out _ ?vs' ?s' _ _ = _")
  assumes
    B: "⋀z. c = (IN z :: com_flow) ⟹
      tags_out cs' ?vs' ?s' f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags_out (cs @ cs') vs s f x}" and
    C: "⋀z. c = (OUT z :: com_flow) ⟹
      tags_out cs' ?vs' ?s' f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags_out (cs @ cs') vs s f x}" and
    D: "⋀X. c = ⟨X⟩ ⟹
      tags_out cs' ?vs' ?s' f x =
      {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
        ∈ tags_out (cs @ cs') vs s f x}"
  shows "tags_out (cs' @ [c]) ?vs' ?s' f x =
    {p. case p of (w, n) ⇒ (w, length [c←cs. c = IN w] + n)
      ∈ tags_out (cs @ cs' @ [c]) vs s f x}"
    (is "_ = {p. case p of (w, n) ⇒ ?P w n c}")
  apply (subst tags_out.simps)
  apply (split com_flow.split)
  apply (rule conjI)
   defer
   apply (rule conjI)
    defer
  subgoal
  proof
    show "∀z. c = OUT z ⟶
      tags_out cs' ?vs' ?s' f x ∪
        (if z = x then tags cs' ?vs' ?s' f x else {}) =
      {(w, n). ?P w n c}"
      (is "∀_. _ ⟶ ?A ∪ (if _ then ?B else _) = _")
      apply clarify
      apply (split if_split)
      apply (rule conjI)
      subgoal for z
      proof
        assume "c = OUT z" and "z = x"
        moreover from this have "?A = {p. case p of (w, n) ⇒
          (w, length [c←cs. c = IN w] + n) ∈ tags_out (cs @ cs') vs s f x}"
          using C by simp
        moreover have "?B = {(w, n).
          (w, length [c←cs. c = IN w] + n) ∈ tags (cs @ cs') vs s f x}"
          by (rule tags_suffix)
        ultimately show "?A ∪ ?B = {(w, n). ?P w n (OUT z)}"
          by (subst append_assoc [symmetric], subst tags_out.simps, auto)
      qed
      subgoal for z
      proof
        assume "c = OUT z" and "z ≠ x"
        moreover from this have "?A = {p. case p of (w, n) ⇒
          (w, length [c←cs. c = IN w] + n) ∈ tags_out (cs @ cs') vs s f x}"
          using C by simp
        ultimately show "?A ∪ {} = {(w, n). ?P w n (OUT z)}"
          by (subst append_assoc [symmetric], subst tags_out.simps, simp)
      qed
      done
  next
    show "∀X. c = ⟨X⟩ ⟶
      tags_out cs' ?vs' ?s' f x ∪ ⋃ {tags cs' ?vs' ?s' f y | y.
        run_flow cs' ?vs' ?s' f: dom y ↝ dom x ∧ y ∈ X} =
      {(w, n). ?P w n c}"
      (is "∀X. _ ⟶ ?A ∪ ?F X = _")
    proof clarify
      fix X
      assume "c = ⟨X⟩"
      hence "?A = {(w, n). (w, length [c←cs. c = IN w] + n)
        ∈ tags_out (cs @ cs') vs s f x}"
        using D by simp
      moreover have "∀y. tags cs' ?vs' ?s' f y = {(w, n).
        (w, length [c←cs. c = IN w] + n) ∈ tags (cs @ cs') vs s f y}"
        by (blast intro!: tags_suffix)
      hence "?F X = {(w, n). (w, length [c←cs. c = IN w] + n)
        ∈ ⋃ {tags (cs @ cs') vs s f y | y.
          run_flow cs' ?vs' ?s' f: dom y ↝ dom x ∧ y ∈ X}}"
        by blast
      ultimately show "?A ∪ ?F X = {(w, n). ?P w n (⟨X⟩)}"
        by (subst append_assoc [symmetric], subst tags_out.simps,
         auto simp: run_flow_append)
    qed
  qed
by (subst append_assoc [symmetric], subst tags_out.simps, simp add: A B)+

lemma tags_out_suffix:
 "tags_out cs' (vs @ in_flow cs vs f) (run_flow cs vs s f) f x = {(w, n).
    (w, length [c←cs. c = IN w] + n) ∈ tags_out (cs @ cs') vs s f x}"
by (induction cs' vs s f x rule: tags_out.induct,
 erule tags_out_suffix_1, simp_all add: tags_out_ubound)


lemma sources_aux_rhs:
  assumes
    A: "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_aux (flow cfs @ cs') vs⇩1 s⇩1 f x)}"
      (is "_ ⊆ {_. _ = _ (⊆ sources_aux (?cs @ _) _ _ _ _)}")
  assumes
    B: "f = f' (⊆ vs⇩1, vs⇩1',
      ⋃ {tags_aux (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S})" and
    C: "(c⇩1, s⇩1, f, vs⇩1, ws⇩1) →*{cfs} (c⇩2, s⇩2, f, vs⇩2, ws⇩2)" and
    D: "ok_flow_aux_2 s⇩1 s⇩2 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' ?cs"
  shows "S ⊆ {x. s⇩2 = t⇩2 (⊆ sources_aux cs' vs⇩2 s⇩2 f x)}"
proof clarify
  fix x y
  assume E: "y ∈ sources_aux cs' vs⇩2 s⇩2 f x"
  moreover have F: "s⇩2 = run_flow ?cs vs⇩1 s⇩1 f"
    using C by (rule small_stepsl_run_flow)
  moreover have G: "vs⇩2 = vs⇩1 @ in_flow ?cs vs⇩1 f"
    using C by (rule small_stepsl_in_flow)
  ultimately have "sources ?cs vs⇩1 s⇩1 f y ⊆ sources_aux (?cs @ cs') vs⇩1 s⇩1 f x"
    by (blast dest: sources_aux_member)
  moreover assume H: "x ∈ S"
  ultimately have "s⇩1 = t⇩1 (⊆ sources ?cs vs⇩1 s⇩1 f y)"
    using A by blast
  moreover have "tags ?cs vs⇩1 s⇩1 f y ⊆ tags_aux (?cs @ cs') vs⇩1 s⇩1 f x"
    using E and F and G by (blast dest: tags_aux_member)
  hence "tags ?cs vs⇩1 s⇩1 f y ⊆ ⋃ {tags_aux (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S}"
    using H by blast
  with B have "f = f' (⊆ vs⇩1, vs⇩1', tags ?cs vs⇩1 s⇩1 f y)"
    by (rule eq_streams_subset)
  ultimately show "s⇩2 y = t⇩2 y"
    using D [rule_format, of "{y}"] by simp
qed

lemma sources_rhs:
  assumes
    A: "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources (flow cfs @ cs') vs⇩1 s⇩1 f x)}"
      (is "_ ⊆ {_. _ = _ (⊆ sources (?cs @ _) _ _ _ _)}")
  assumes
    B: "f = f' (⊆ vs⇩1, vs⇩1',
      ⋃ {tags (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S})" and
    C: "(c⇩1, s⇩1, f, vs⇩1, ws⇩1) →*{cfs} (c⇩2, s⇩2, f, vs⇩2, ws⇩2)" and
    D: "ok_flow_aux_2 s⇩1 s⇩2 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' ?cs"
  shows "S ⊆ {x. s⇩2 = t⇩2 (⊆ sources cs' vs⇩2 s⇩2 f x)}"
proof clarify
  fix x y
  assume E: "y ∈ sources cs' vs⇩2 s⇩2 f x"
  moreover have F: "s⇩2 = run_flow ?cs vs⇩1 s⇩1 f"
    using C by (rule small_stepsl_run_flow)
  moreover have G: "vs⇩2 = vs⇩1 @ in_flow ?cs vs⇩1 f"
    using C by (rule small_stepsl_in_flow)
  ultimately have "sources ?cs vs⇩1 s⇩1 f y ⊆ sources (?cs @ cs') vs⇩1 s⇩1 f x"
    by (blast dest: sources_member)
  moreover assume H: "x ∈ S"
  ultimately have "s⇩1 = t⇩1 (⊆ sources ?cs vs⇩1 s⇩1 f y)"
    using A by blast
  moreover have "tags ?cs vs⇩1 s⇩1 f y ⊆ tags (?cs @ cs') vs⇩1 s⇩1 f x"
    using E and F and G by (blast dest: tags_member)
  hence "tags ?cs vs⇩1 s⇩1 f y ⊆ ⋃ {tags (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S}"
    using H by blast
  with B have "f = f' (⊆ vs⇩1, vs⇩1', tags ?cs vs⇩1 s⇩1 f y)"
    by (rule eq_streams_subset)
  ultimately show "s⇩2 y = t⇩2 y"
    using D [rule_format, of "{y}"] by simp
qed

lemma sources_out_rhs:
  assumes
    A: "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_out (flow cfs @ cs') vs⇩1 s⇩1 f x)}"
      (is "_ ⊆ {_. _ = _ (⊆ sources_out (?cs @ _) _ _ _ _)}")
  assumes
    B: "f = f' (⊆ vs⇩1, vs⇩1',
      ⋃ {tags_out (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S})" and
    C: "(c⇩1, s⇩1, f, vs⇩1, ws⇩1) →*{cfs} (c⇩2, s⇩2, f, vs⇩2, ws⇩2)" and
    D: "ok_flow_aux_2 s⇩1 s⇩2 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' ?cs"
  shows "S ⊆ {x. s⇩2 = t⇩2 (⊆ sources_out cs' vs⇩2 s⇩2 f x)}"
proof clarify
  fix x y
  assume E: "y ∈ sources_out cs' vs⇩2 s⇩2 f x"
  moreover have F: "s⇩2 = run_flow ?cs vs⇩1 s⇩1 f"
    using C by (rule small_stepsl_run_flow)
  moreover have G: "vs⇩2 = vs⇩1 @ in_flow ?cs vs⇩1 f"
    using C by (rule small_stepsl_in_flow)
  ultimately have "sources ?cs vs⇩1 s⇩1 f y ⊆ sources_out (?cs @ cs') vs⇩1 s⇩1 f x"
    by (blast dest: sources_out_member)
  moreover assume H: "x ∈ S"
  ultimately have "s⇩1 = t⇩1 (⊆ sources ?cs vs⇩1 s⇩1 f y)"
    using A by blast
  moreover have "tags ?cs vs⇩1 s⇩1 f y ⊆ tags_out (?cs @ cs') vs⇩1 s⇩1 f x"
    using E and F and G by (blast dest: tags_out_member)
  hence "tags ?cs vs⇩1 s⇩1 f y ⊆ ⋃ {tags_out (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S}"
    using H by blast
  with B have "f = f' (⊆ vs⇩1, vs⇩1', tags ?cs vs⇩1 s⇩1 f y)"
    by (rule eq_streams_subset)
  ultimately show "s⇩2 y = t⇩2 y"
    using D [rule_format, of "{y}"] by simp
qed


lemma tags_aux_rhs:
  assumes
    A: "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_aux (flow cfs @ cs') vs⇩1 s⇩1 f x)}"
      (is "_ ⊆ {_. _ = _ (⊆ sources_aux (?cs @ _) _ _ _ _)}")
  assumes
    B: "f = f' (⊆ vs⇩1, vs⇩1',
      ⋃ {tags_aux (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S})" and
    C: "(c⇩1, s⇩1, f, vs⇩1, ws⇩1) →*{cfs} (c⇩2, s⇩2, f, vs⇩2, ws⇩2)" and
    D: "(c⇩1', t⇩1, f', vs⇩1', ws⇩1') →* (c⇩2', t⇩2, f', vs⇩2', ws⇩2')" and
    E: "ok_flow_aux_1 c⇩1 c⇩2 c⇩2' s⇩1 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' vs⇩2 vs⇩2' ws⇩1' ws⇩2' ?cs"
  shows "f = f' (⊆ vs⇩2, vs⇩2', ⋃ {tags_aux cs' vs⇩2 s⇩2 f x | x. x ∈ S})"
proof (subst eq_streams_def, clarify)
  fix x y n
  have F: "vs⇩2 = vs⇩1 @ drop (length vs⇩1) vs⇩2"
    using small_stepsl_steps [OF C] by (rule small_steps_in_flow)
  have G: "vs⇩2' = vs⇩1' @ drop (length vs⇩1') vs⇩2'"
    using D by (rule small_steps_in_flow)
  assume "(y, n) ∈ tags_aux cs' vs⇩2 s⇩2 f x"
  moreover have "s⇩2 = run_flow ?cs vs⇩1 s⇩1 f"
    using C by (rule small_stepsl_run_flow)
  moreover have H: "vs⇩2 = vs⇩1 @ in_flow ?cs vs⇩1 f"
    using C by (rule small_stepsl_in_flow)
  ultimately have I: "(y, length [c←?cs. c = IN y] + n)
    ∈ tags_aux (?cs @ cs') vs⇩1 s⇩1 f x"
    (is "(_, ?k + _) ∈ _")
    by (simp add: tags_aux_suffix)
  let ?m = "Suc (Max {k. k ≤ length (?cs @ cs') ∧
    length [c←take k (?cs @ cs'). c = IN y] ≤ ?k + n})"
  have J: "y ∈ sources_aux (drop ?m (?cs @ cs'))
    (vs⇩1 @ in_flow (take ?m (?cs @ cs')) vs⇩1 f)
    (run_flow (take ?m (?cs @ cs')) vs⇩1 s⇩1 f) f x"
    using I by (auto dest: tags_aux_sources_aux)
  hence "sources (take ?m (?cs @ cs')) vs⇩1 s⇩1 f y ⊆
    sources_aux (take ?m (?cs @ cs') @ drop ?m (?cs @ cs')) vs⇩1 s⇩1 f x"
    by (rule sources_aux_member)
  moreover have K: "length ?cs ≤ ?m"
    by (rule le_SucI, rule Max_ge, simp_all)
  ultimately have
   "sources (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    sources_aux (?cs @ cs') vs⇩1 s⇩1 f x"
    by simp
  moreover have
   "sources_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    sources (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule sources_aux_sources)
  moreover have "sources_aux ?cs vs⇩1 s⇩1 f y ⊆
    sources_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule sources_aux_append)
  moreover assume L: "x ∈ S"
  hence "s⇩1 = t⇩1 (⊆ sources_aux (?cs @ cs') vs⇩1 s⇩1 f x)"
    using A by blast
  ultimately have M: "s⇩1 = t⇩1 (⊆ sources_aux ?cs vs⇩1 s⇩1 f y)"
    by blast
  have "tags (take ?m (?cs @ cs')) vs⇩1 s⇩1 f y ⊆
    tags_aux (take ?m (?cs @ cs') @ drop ?m (?cs @ cs')) vs⇩1 s⇩1 f x"
    using J by (rule tags_aux_member)
  hence "tags (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    tags_aux (?cs @ cs') vs⇩1 s⇩1 f x"
    using K by simp
  moreover have
   "tags_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    tags (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule tags_aux_tags)
  moreover have "tags_aux ?cs vs⇩1 s⇩1 f y ⊆
    tags_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule tags_aux_append)
  ultimately have "tags_aux ?cs vs⇩1 s⇩1 f y ⊆
    ⋃ {tags_aux (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S}"
    using L by blast
  with B have "f = f' (⊆ vs⇩1, vs⇩1', tags_aux ?cs vs⇩1 s⇩1 f y)"
    by (rule eq_streams_subset)
  hence "map fst [p←drop (length vs⇩1) vs⇩2. fst p = y] =
    map fst [p←drop (length vs⇩1') vs⇩2'. fst p = y]"
    using E [rule_format, of "{y}"] and M by simp
  hence "length [p←drop (length vs⇩1) vs⇩2. fst p = y] =
    length [p←drop (length vs⇩1') vs⇩2'. fst p = y]"
    by (drule_tac arg_cong [where f = length],
     subst (asm) (1 2) length_map)
  hence "length [p←drop (length vs⇩1) vs⇩2. fst p = y] = ?k ∧
    length [p←drop (length vs⇩1') vs⇩2'. fst p = y] = ?k"
    using H by (simp add: in_flow_length)
  moreover have "f y (length [p←vs⇩1. fst p = y] + ?k + n) =
    f' y (length [p←vs⇩1'. fst p = y] + ?k + n)"
    using B and I and L by (fastforce simp: eq_streams_def ac_simps)
  ultimately show "f y (length [p←vs⇩2. fst p = y] + n) =
    f' y (length [p←vs⇩2'. fst p = y] + n)"
    by (subst F, subst G, simp)
qed

lemma tags_rhs:
  assumes
    A: "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources (flow cfs @ cs') vs⇩1 s⇩1 f x)}"
      (is "_ ⊆ {_. _ = _ (⊆ sources (?cs @ _) _ _ _ _)}")
  assumes
    B: "f = f' (⊆ vs⇩1, vs⇩1',
      ⋃ {tags (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S})" and
    C: "(c⇩1, s⇩1, f, vs⇩1, ws⇩1) →*{cfs} (c⇩2, s⇩2, f, vs⇩2, ws⇩2)" and
    D: "(c⇩1', t⇩1, f', vs⇩1', ws⇩1') →* (c⇩2', t⇩2, f', vs⇩2', ws⇩2')" and
    E: "ok_flow_aux_1 c⇩1 c⇩2 c⇩2' s⇩1 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' vs⇩2 vs⇩2' ws⇩1' ws⇩2' ?cs"
  shows "f = f' (⊆ vs⇩2, vs⇩2', ⋃ {tags cs' vs⇩2 s⇩2 f x | x. x ∈ S})"
proof (subst eq_streams_def, clarify)
  fix x y n
  have F: "vs⇩2 = vs⇩1 @ drop (length vs⇩1) vs⇩2"
    using small_stepsl_steps [OF C] by (rule small_steps_in_flow)
  have G: "vs⇩2' = vs⇩1' @ drop (length vs⇩1') vs⇩2'"
    using D by (rule small_steps_in_flow)
  assume "(y, n) ∈ tags cs' vs⇩2 s⇩2 f x"
  moreover have "s⇩2 = run_flow ?cs vs⇩1 s⇩1 f"
    using C by (rule small_stepsl_run_flow)
  moreover have H: "vs⇩2 = vs⇩1 @ in_flow ?cs vs⇩1 f"
    using C by (rule small_stepsl_in_flow)
  ultimately have I: "(y, length [c←?cs. c = IN y] + n)
    ∈ tags (?cs @ cs') vs⇩1 s⇩1 f x"
    (is "(_, ?k + _) ∈ _")
    by (simp add: tags_suffix)
  let ?m = "Suc (Max {k. k ≤ length (?cs @ cs') ∧
    length [c←take k (?cs @ cs'). c = IN y] ≤ ?k + n})"
  have J: "y ∈ sources (drop ?m (?cs @ cs'))
    (vs⇩1 @ in_flow (take ?m (?cs @ cs')) vs⇩1 f)
    (run_flow (take ?m (?cs @ cs')) vs⇩1 s⇩1 f) f x"
    using I by (auto dest: tags_sources)
  hence "sources (take ?m (?cs @ cs')) vs⇩1 s⇩1 f y ⊆
    sources (take ?m (?cs @ cs') @ drop ?m (?cs @ cs')) vs⇩1 s⇩1 f x"
    by (rule sources_member)
  moreover have K: "length ?cs ≤ ?m"
    by (rule le_SucI, rule Max_ge, simp_all)
  ultimately have
   "sources (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    sources (?cs @ cs') vs⇩1 s⇩1 f x"
    by simp
  moreover have
   "sources_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    sources (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule sources_aux_sources)
  moreover have "sources_aux ?cs vs⇩1 s⇩1 f y ⊆
    sources_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule sources_aux_append)
  moreover assume L: "x ∈ S"
  hence "s⇩1 = t⇩1 (⊆ sources (?cs @ cs') vs⇩1 s⇩1 f x)"
    using A by blast
  ultimately have M: "s⇩1 = t⇩1 (⊆ sources_aux ?cs vs⇩1 s⇩1 f y)"
    by blast
  have "tags (take ?m (?cs @ cs')) vs⇩1 s⇩1 f y ⊆
    tags (take ?m (?cs @ cs') @ drop ?m (?cs @ cs')) vs⇩1 s⇩1 f x"
    using J by (rule tags_member)
  hence "tags (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    tags (?cs @ cs') vs⇩1 s⇩1 f x"
    using K by simp
  moreover have
   "tags_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    tags (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule tags_aux_tags)
  moreover have "tags_aux ?cs vs⇩1 s⇩1 f y ⊆
    tags_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule tags_aux_append)
  ultimately have "tags_aux ?cs vs⇩1 s⇩1 f y ⊆
    ⋃ {tags (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S}"
    using L by blast
  with B have "f = f' (⊆ vs⇩1, vs⇩1', tags_aux ?cs vs⇩1 s⇩1 f y)"
    by (rule eq_streams_subset)
  hence "map fst [p←drop (length vs⇩1) vs⇩2. fst p = y] =
    map fst [p←drop (length vs⇩1') vs⇩2'. fst p = y]"
    using E [rule_format, of "{y}"] and M by simp
  hence "length [p←drop (length vs⇩1) vs⇩2. fst p = y] =
    length [p←drop (length vs⇩1') vs⇩2'. fst p = y]"
    by (drule_tac arg_cong [where f = length],
     subst (asm) (1 2) length_map)
  hence "length [p←drop (length vs⇩1) vs⇩2. fst p = y] = ?k ∧
    length [p←drop (length vs⇩1') vs⇩2'. fst p = y] = ?k"
    using H by (simp add: in_flow_length)
  moreover have "f y (length [p←vs⇩1. fst p = y] + ?k + n) =
    f' y (length [p←vs⇩1'. fst p = y] + ?k + n)"
    using B and I and L by (fastforce simp: eq_streams_def ac_simps)
  ultimately show "f y (length [p←vs⇩2. fst p = y] + n) =
    f' y (length [p←vs⇩2'. fst p = y] + n)"
    by (subst F, subst G, simp)
qed

lemma tags_out_rhs:
  assumes
    A: "S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_out (flow cfs @ cs') vs⇩1 s⇩1 f x)}"
      (is "_ ⊆ {_. _ = _ (⊆ sources_out (?cs @ _) _ _ _ _)}")
  assumes
    B: "f = f' (⊆ vs⇩1, vs⇩1',
      ⋃ {tags_out (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S})" and
    C: "(c⇩1, s⇩1, f, vs⇩1, ws⇩1) →*{cfs} (c⇩2, s⇩2, f, vs⇩2, ws⇩2)" and
    D: "(c⇩1', t⇩1, f', vs⇩1', ws⇩1') →* (c⇩2', t⇩2, f', vs⇩2', ws⇩2')" and
    E: "ok_flow_aux_1 c⇩1 c⇩2 c⇩2' s⇩1 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' vs⇩2 vs⇩2' ws⇩1' ws⇩2' ?cs"
  shows "f = f' (⊆ vs⇩2, vs⇩2', ⋃ {tags_out cs' vs⇩2 s⇩2 f x | x. x ∈ S})"
proof (subst eq_streams_def, clarify)
  fix x y n
  have F: "vs⇩2 = vs⇩1 @ drop (length vs⇩1) vs⇩2"
    using small_stepsl_steps [OF C] by (rule small_steps_in_flow)
  have G: "vs⇩2' = vs⇩1' @ drop (length vs⇩1') vs⇩2'"
    using D by (rule small_steps_in_flow)
  assume "(y, n) ∈ tags_out cs' vs⇩2 s⇩2 f x"
  moreover have "s⇩2 = run_flow ?cs vs⇩1 s⇩1 f"
    using C by (rule small_stepsl_run_flow)
  moreover have H: "vs⇩2 = vs⇩1 @ in_flow ?cs vs⇩1 f"
    using C by (rule small_stepsl_in_flow)
  ultimately have I: "(y, length [c←?cs. c = IN y] + n)
    ∈ tags_out (?cs @ cs') vs⇩1 s⇩1 f x"
    (is "(_, ?k + _) ∈ _")
    by (simp add: tags_out_suffix)
  let ?m = "Suc (Max {k. k ≤ length (?cs @ cs') ∧
    length [c←take k (?cs @ cs'). c = IN y] ≤ ?k + n})"
  have J: "y ∈ sources_out (drop ?m (?cs @ cs'))
    (vs⇩1 @ in_flow (take ?m (?cs @ cs')) vs⇩1 f)
    (run_flow (take ?m (?cs @ cs')) vs⇩1 s⇩1 f) f x"
    using I by (auto dest: tags_out_sources_out)
  hence "sources (take ?m (?cs @ cs')) vs⇩1 s⇩1 f y ⊆
    sources_out (take ?m (?cs @ cs') @ drop ?m (?cs @ cs')) vs⇩1 s⇩1 f x"
    by (rule sources_out_member)
  moreover have K: "length ?cs ≤ ?m"
    by (rule le_SucI, rule Max_ge, simp_all)
  ultimately have
   "sources (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    sources_out (?cs @ cs') vs⇩1 s⇩1 f x"
    by simp
  moreover have
   "sources_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    sources (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule sources_aux_sources)
  moreover have "sources_aux ?cs vs⇩1 s⇩1 f y ⊆
    sources_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule sources_aux_append)
  moreover assume L: "x ∈ S"
  hence "s⇩1 = t⇩1 (⊆ sources_out (?cs @ cs') vs⇩1 s⇩1 f x)"
    using A by blast
  ultimately have M: "s⇩1 = t⇩1 (⊆ sources_aux ?cs vs⇩1 s⇩1 f y)"
    by blast
  have "tags (take ?m (?cs @ cs')) vs⇩1 s⇩1 f y ⊆
    tags_out (take ?m (?cs @ cs') @ drop ?m (?cs @ cs')) vs⇩1 s⇩1 f x"
    using J by (rule tags_out_member)
  hence "tags (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    tags_out (?cs @ cs') vs⇩1 s⇩1 f x"
    using K by simp
  moreover have
   "tags_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y ⊆
    tags (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule tags_aux_tags)
  moreover have "tags_aux ?cs vs⇩1 s⇩1 f y ⊆
    tags_aux (?cs @ take (?m - length ?cs) cs') vs⇩1 s⇩1 f y"
    by (rule tags_aux_append)
  ultimately have "tags_aux ?cs vs⇩1 s⇩1 f y ⊆
    ⋃ {tags_out (?cs @ cs') vs⇩1 s⇩1 f x | x. x ∈ S}"
    using L by blast
  with B have "f = f' (⊆ vs⇩1, vs⇩1', tags_aux ?cs vs⇩1 s⇩1 f y)"
    by (rule eq_streams_subset)
  hence "map fst [p←drop (length vs⇩1) vs⇩2. fst p = y] =
    map fst [p←drop (length vs⇩1') vs⇩2'. fst p = y]"
    using E [rule_format, of "{y}"] and M by simp
  hence "length [p←drop (length vs⇩1) vs⇩2. fst p = y] =
    length [p←drop (length vs⇩1') vs⇩2'. fst p = y]"
    by (drule_tac arg_cong [where f = length],
     subst (asm) (1 2) length_map)
  hence "length [p←drop (length vs⇩1) vs⇩2. fst p = y] = ?k ∧
    length [p←drop (length vs⇩1') vs⇩2'. fst p = y] = ?k"
    using H by (simp add: in_flow_length)
  moreover have "f y (length [p←vs⇩1. fst p = y] + ?k + n) =
    f' y (length [p←vs⇩1'. fst p = y] + ?k + n)"
    using B and I and L by (fastforce simp: eq_streams_def ac_simps)
  ultimately show "f y (length [p←vs⇩2. fst p = y] + n) =
    f' y (length [p←vs⇩2'. fst p = y] + n)"
    by (subst F, subst G, simp)
qed


lemma ctyping2_term_seq:
  assumes
    A: "⋀B Y p. (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV ⟹ ∃p'. (c⇩1, p) ⇒ p'" and
    B: "⋀q B Y B' Y' p. (U, v) ⊨ c⇩1 (⊆ A, X) = Some q ⟹ (B, Y) = q ⟹
      (U, v) ⊨ c⇩2 (⊆ B, Y) = Some (B', Y') ⟹
        ∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV ⟹ ∃p'. (c⇩2, p) ⇒ p'" and
    C: "(U, v) ⊨ c⇩1;; c⇩2 (⊆ A, X) = Some (B', Y')" and
    D: "∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV"
  shows "∃p'. (c⇩1;; c⇩2, p) ⇒ p'"
proof -
  obtain B and Y where
    E: "(U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y)" and
    F: "(U, v) ⊨ c⇩2 (⊆ B, Y) = Some (B', Y')"
    using C by (auto split: option.split_asm)
  obtain p' where "(c⇩1, p) ⇒ p'"
    using A [OF E D] by blast
  moreover obtain p'' where "(c⇩2, p') ⇒ p''"
    using B [OF E _ F D] by blast
  ultimately show ?thesis
    by blast
qed

lemma ctyping2_term_or:
  assumes
    A: "⋀B Y p. (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV ⟹ ∃p'. (c⇩1, p) ⇒ p'" and
    B: "(U, v) ⊨ c⇩1 OR c⇩2 (⊆ A, X) = Some (B', Y')" and
    C: "∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV"
  shows "∃p'. (c⇩1 OR c⇩2, p) ⇒ p'"
proof -
  obtain B and Y where "(U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y)"
    using B by (auto split: option.split_asm)
  thus ?thesis
    using A and C by blast
qed

lemma ctyping2_term_if:
  assumes
    A: "⋀U' q B⇩1 B⇩2 B Y p.
      (U', q) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B⇩1, B⇩2) = q ⟹ (U', v) ⊨ c⇩1 (⊆ B⇩1, X) = Some (B, Y) ⟹
          ∃(C, Z) ∈ U'. ¬ C: Z ↝ UNIV ⟹ ∃p'. (c⇩1, p) ⇒ p'" and
    B: "⋀U' q B⇩1 B⇩2 B Y p.
      (U', q) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B⇩1, B⇩2) = q ⟹ (U', v) ⊨ c⇩2 (⊆ B⇩2, X) = Some (B, Y) ⟹
          ∃(C, Z) ∈ U'. ¬ C: Z ↝ UNIV ⟹ ∃p'. (c⇩2, p) ⇒ p'" and
    C: "(U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X) = Some (B, Y)" and
    D: "∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV"
  shows "∃p'. (IF b THEN c⇩1 ELSE c⇩2, p) ⇒ p'"
proof -
  let ?U' = "insert (Univ? A X, bvars b) U"
  obtain B⇩1 and B⇩1' and Y⇩1 and B⇩2 and B⇩2' and Y⇩2 where
    E: "⊨ b (⊆ A, X) = (B⇩1, B⇩2)" and
    F: "(?U', v) ⊨ c⇩1 (⊆ B⇩1, X) = Some (B⇩1', Y⇩1)" and
    G: "(?U', v) ⊨ c⇩2 (⊆ B⇩2, X) = Some (B⇩2', Y⇩2)"
    using C by (auto split: option.split_asm prod.split_asm)
  obtain s and q where "p = (s, q)"
    by (cases p)
  moreover {
    assume "bval b s"
    moreover obtain p' where "(c⇩1, s, q) ⇒ p'"
      using A [OF _ _ F, of _ B⇩2 "(s, q)"] and D and E by auto
    ultimately have "∃p'. (IF b THEN c⇩1 ELSE c⇩2, s, q) ⇒ p'"
      by blast
  }
  moreover {
    assume "¬ bval b s"
    moreover obtain p' where "(c⇩2, s, q) ⇒ p'"
      using B [OF _ _ G, of _ B⇩1 "(s, q)"] and D and E by auto
    ultimately have "∃p'. (IF b THEN c⇩1 ELSE c⇩2, s, q) ⇒ p'"
      by blast
  }
  ultimately show ?thesis
    by blast
qed

lemma ctyping2_term:
 "⟦(U, v) ⊨ c (⊆ A, X) = Some (B, Y); ∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV⟧ ⟹
    ∃p'. (c, p) ⇒ p'"
proof (induction "(U, v)" c A X arbitrary: B Y U v p rule: ctyping2.induct,
 blast)
  fix A X B Y U v c⇩1 c⇩2 p
  show
   "⟦⋀B Y p. (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV ⟹ ∃p'. (c⇩1, p) ⇒ p';
    ⋀q B Y B' Y' p. (U, v) ⊨ c⇩1 (⊆ A, X) = Some q ⟹ (B, Y) = q ⟹
      (U, v) ⊨ c⇩2 (⊆ B, Y) = Some (B', Y') ⟹
        ∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV ⟹ ∃p'. (c⇩2, p) ⇒ p';
    (U, v) ⊨ c⇩1;; c⇩2 (⊆ A, X) = Some (B, Y);
    ∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV⟧ ⟹
      ∃p'. (c⇩1;; c⇩2, p) ⇒ p'"
    by (rule ctyping2_term_seq)
next
  fix A X B Y U v c⇩1 c⇩2 p
  show
   "⟦⋀B Y p. (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV ⟹ ∃p'. (c⇩1, p) ⇒ p';
    (U, v) ⊨ c⇩1 OR c⇩2 (⊆ A, X) = Some (B, Y);
    ∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV⟧ ⟹
      ∃p'. (c⇩1 OR c⇩2, p) ⇒ p'"
    by (rule ctyping2_term_or)
next
  fix A X B Y U v b c⇩1 c⇩2 p
  show
   "⟦⋀U' q B⇩1 B⇩2 B Y p.
      (U', q) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B⇩1, B⇩2) = q ⟹ (U', v) ⊨ c⇩1 (⊆ B⇩1, X) = Some (B, Y) ⟹
          ∃(C, Z) ∈ U'. ¬ C: Z ↝ UNIV ⟹ ∃p'. (c⇩1, p) ⇒ p';
    ⋀U' q B⇩1 B⇩2 B Y p.
      (U', q) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B⇩1, B⇩2) = q ⟹ (U', v) ⊨ c⇩2 (⊆ B⇩2, X) = Some (B, Y) ⟹
          ∃(C, Z) ∈ U'. ¬ C: Z ↝ UNIV ⟹ ∃p'. (c⇩2, p) ⇒ p';
    (U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X) = Some (B, Y);
    ∃(C, Z) ∈ U. ¬ C: Z ↝ UNIV⟧ ⟹
      ∃p'. (IF b THEN c⇩1 ELSE c⇩2, p) ⇒ p'"
    by (rule ctyping2_term_if)
qed (fastforce split: if_split_asm prod.split_asm)+


lemma ctyping2_confine_seq:
  assumes
    A: "⋀s' f' vs' ws' A B X Y U v. p = (s', f', vs', ws') ⟹
      (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹ ∃(C, Z) ∈ U. C: Z ↝| S ⟹
        s = s' (⊆ S) ∧
        [p←drop (length vs) vs'. fst p ∈ S] = [] ∧
        [p←drop (length ws) ws'. fst p ∈ S] = []"
      (is "⋀s' _ vs' ws' _ _ _ _ _ _. _ ⟹ _ ⟹ _ ⟹
        ?P s s' vs vs' ws ws'")
  assumes
    B: "⋀s' f' vs' ws' A B X Y U v. p = (s', f', vs', ws') ⟹
      (U, v) ⊨ c⇩2 (⊆ A, X) = Some (B, Y) ⟹ ∃(C, Z) ∈ U. C: Z ↝| S ⟹
        ?P s' s'' vs' vs'' ws' ws''" and
    C: "(c⇩1, s, f, vs, ws) ⇒ p" and
    D: "(c⇩2, p) ⇒ (s'', f'', vs'', ws'')" and
    E: "(U, v) ⊨ c⇩1;; c⇩2 (⊆ A, X) = Some (B', Y')" and
    F: "∃(C, Z) ∈ U. C: Z ↝| S"
  shows "?P s s'' vs vs'' ws ws''"
proof -
  obtain s' and f' and vs' and ws' where G: "p = (s', f', vs', ws')"
    by (cases p)
  have H: "(c⇩1, s, f, vs, ws) →* (SKIP, s', f', vs', ws')"
    using C and G by (simp add: big_iff_small)
  have I: "(c⇩2, s', f', vs', ws') →* (SKIP, s'', f'', vs'', ws'')"
    using D and G by (simp add: big_iff_small)
  have J: "vs' = vs @ drop (length vs) vs'"
    using H by (rule small_steps_in_flow)
  have "vs'' = vs' @ drop (length vs') vs''"
    using I by (rule small_steps_in_flow)
  hence K: "vs'' = vs @ drop (length vs) vs' @ drop (length vs') vs''"
    by (subst (asm) J, simp)
  have L: "ws' = ws @ drop (length ws) ws'"
    using H by (rule small_steps_out_flow)
  have "ws'' = ws' @ drop (length ws') ws''"
    using I by (rule small_steps_out_flow)
  hence M: "ws'' = ws @ drop (length ws) ws' @ drop (length ws') ws''"
    by (subst (asm) L, simp)
  obtain B and Y where
    N: "(U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y)" and
    O: "(U, v) ⊨ c⇩2 (⊆ B, Y) = Some (B', Y')"
    using E by (auto split: option.split_asm)
  from A [OF G N F] and B [OF G O F] show ?thesis
    by (subst K, subst M, simp)
qed

lemma ctyping2_confine_or_lhs:
  assumes
    A: "⋀A B X Y U v. (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. C: Z ↝| S ⟹
        s = s' (⊆ S) ∧
        [p←drop (length vs) vs'. fst p ∈ S] = [] ∧
        [p←drop (length ws) ws'. fst p ∈ S] = []"
      (is "⋀_ _ _ _ _ _. _ ⟹ _ ⟹ ?P")
  assumes
    B: "(U, v) ⊨ c⇩1 OR c⇩2 (⊆ A, X) = Some (B', Y')" and
    C: "∃(C, Z) ∈ U. C: Z ↝| S"
  shows ?P
proof -
  obtain B and Y where "(U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y)"
    using B by (auto split: option.split_asm)
  with A and C show ?thesis
    by simp
qed

lemma ctyping2_confine_or_rhs:
  assumes
    A: "⋀A B X Y U v. (U, v) ⊨ c⇩2 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. C: Z ↝| S ⟹
        s = s' (⊆ S) ∧
        [p←drop (length vs) vs'. fst p ∈ S] = [] ∧
        [p←drop (length ws) ws'. fst p ∈ S] = []"
      (is "⋀_ _ _ _ _ _. _ ⟹ _ ⟹ ?P")
  assumes
    B: "(U, v) ⊨ c⇩1 OR c⇩2 (⊆ A, X) = Some (B', Y')" and
    C: "∃(C, Z) ∈ U. C: Z ↝| S"
  shows ?P
proof -
  obtain B and Y where "(U, v) ⊨ c⇩2 (⊆ A, X) = Some (B, Y)"
    using B by (auto split: option.split_asm)
  with A and C show ?thesis
    by simp
qed

lemma ctyping2_confine_if_true:
  assumes
    A: "⋀A B X Y U v. (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. C: Z ↝| S ⟹
        s = s' (⊆ S) ∧
        [p←drop (length vs) vs'. fst p ∈ S] = [] ∧
        [p←drop (length ws) ws'. fst p ∈ S] = []"
      (is "⋀_ _ _ _ _ _. _ ⟹ _ ⟹ ?P")
  assumes
    B: "(U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X) = Some (B, Y)" and
    C: "∃(C, Z) ∈ U. C: Z ↝| S"
  shows ?P
proof -
  obtain B⇩1 and B⇩1' and Y⇩1 where
   "(insert (Univ? A X, bvars b) U, v) ⊨ c⇩1 (⊆ B⇩1, X) = Some (B⇩1', Y⇩1)"
    using B by (auto split: option.split_asm prod.split_asm)
  with A and C show ?thesis
    by simp
qed

lemma ctyping2_confine_if_false:
  assumes
    A: "⋀A B X Y U v. (U, v) ⊨ c⇩2 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. C: Z ↝| S ⟹
        s = s' (⊆ S) ∧
        [p←drop (length vs) vs'. fst p ∈ S] = [] ∧
        [p←drop (length ws) ws'. fst p ∈ S] = []"
      (is "⋀_ _ _ _ _ _. _ ⟹ _ ⟹ ?P")
  assumes
    B: "(U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X) = Some (B, Y)" and
    C: "∃(C, Z) ∈ U. C: Z ↝| S"
  shows ?P
proof -
  obtain B⇩2 and B⇩2' and Y⇩2 where
   "(insert (Univ? A X, bvars b) U, v) ⊨ c⇩2 (⊆ B⇩2, X) = Some (B⇩2', Y⇩2)"
    using B by (auto split: option.split_asm prod.split_asm)
  with A and C show ?thesis
    by simp
qed

lemma ctyping2_confine:
 "⟦(c, s, f, vs, ws) ⇒ (s', f', vs', ws');
    (U, v) ⊨ c (⊆ A, X) = Some (B, Y); ∃(C, Z) ∈ U. C: Z ↝| S⟧ ⟹
  s = s' (⊆ S) ∧
  [p←drop (length vs) vs'. fst p ∈ S] = [] ∧
  [p←drop (length ws) ws'. fst p ∈ S] = []"
  (is "⟦_; _; _⟧ ⟹ ?P s s' vs vs' ws ws'")
proof (induction "(c, s, f, vs, ws)" "(s', f', vs', ws')" arbitrary:
 c s f vs ws s' f' vs' ws' A B X Y U v rule: big_step.induct)
  fix A B X Y U v c⇩1 c⇩2 p s f vs ws s' f' vs' ws'
  show
   "⟦⋀s' f' vs' ws' A B X Y U v. p = (s', f', vs', ws') ⟹
      (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
        ∃(C, Z) ∈ U. C: Z ↝| S ⟹ ?P s s' vs vs' ws ws';
    ⋀s f vs ws A B X Y U v. p = (s, f, vs, ws) ⟹
      (U, v) ⊨ c⇩2 (⊆ A, X) = Some (B, Y) ⟹
        ∃(C, Z) ∈ U. C: Z ↝| S ⟹ ?P s s' vs vs' ws ws';
    (c⇩1, s, f, vs, ws) ⇒ p;
    (c⇩2, p) ⇒ (s', f', vs', ws');
    (U, v) ⊨ c⇩1;; c⇩2 (⊆ A, X) = Some (B, Y);
    ∃(C, Z) ∈ U. C: Z ↝| S⟧ ⟹
      ?P s s' vs vs' ws ws'"
    by (rule ctyping2_confine_seq)
next
  fix A B X Y U v c⇩1 c⇩2 s vs ws s' vs' ws'
  show
   "⟦⋀A B X Y U v. (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. C: Z ↝| S ⟹ ?P s s' vs vs' ws ws';
    (U, v) ⊨ c⇩1 OR c⇩2 (⊆ A, X) = Some (B, Y);
    ∃(C, Z) ∈ U. C: Z ↝| S⟧ ⟹
      ?P s s' vs vs' ws ws'"
    by (rule ctyping2_confine_or_lhs)
next
  fix A B X Y U v c⇩1 c⇩2 s vs ws s' vs' ws'
  show
   "⟦⋀A B X Y U v. (U, v) ⊨ c⇩2 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. C: Z ↝| S ⟹ ?P s s' vs vs' ws ws';
    (U, v) ⊨ c⇩1 OR c⇩2 (⊆ A, X) = Some (B, Y);
    ∃(C, Z) ∈ U. C: Z ↝| S⟧ ⟹
      ?P s s' vs vs' ws ws'"
    by (rule ctyping2_confine_or_rhs)
next
  fix A B X Y U v b c⇩1 c⇩2 s vs ws s' vs' ws'
  show
   "⟦⋀A B X Y U v. (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. C: Z ↝| S ⟹ ?P s s' vs vs' ws ws';
    (U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X) = Some (B, Y);
    ∃(C, Z) ∈ U. C: Z ↝| S⟧ ⟹
      ?P s s' vs vs' ws ws'"
    by (rule ctyping2_confine_if_true)
next
  fix A B X Y U v b c⇩1 c⇩2 s vs ws s' vs' ws'
  show
   "⟦⋀A B X Y U v. (U, v) ⊨ c⇩2 (⊆ A, X) = Some (B, Y) ⟹
      ∃(C, Z) ∈ U. C: Z ↝| S ⟹ ?P s s' vs vs' ws ws';
    (U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X) = Some (B, Y);
    ∃(C, Z) ∈ U. C: Z ↝| S⟧ ⟹
      ?P s s' vs vs' ws ws'"
    by (rule ctyping2_confine_if_false)
qed (force split: if_split_asm prod.split_asm)+


lemma eq_states_assign:
  assumes
    A: "S ⊆ {y. s = t (⊆ sources [x ::= a] vs s f y)}" and
    B: "x ∈ S" and
    C: "s ∈ Univ A (⊆ state ∩ X)" and
    D: "Univ? A X: avars a ↝ {x}"
  shows "s = t (⊆ avars a)"
proof -
  obtain r where E: "r ∈ A" and F: "s = r (⊆ state ∩ X)"
    using C by blast
  have "avars a ⊆ {y. s: dom y ↝ dom x}"
  proof (cases "state ⊆ X")
    case True
    with F have "interf s = interf r"
      by (blast intro: interf_state)
    with D and E show ?thesis
      by (auto simp: univ_states_if_def split: if_split_asm)
  next
    case False
    with D and E show ?thesis
      by (auto simp: univ_states_if_def split: if_split_asm)
  qed
  moreover have "s = t (⊆ sources [x ::= a] vs s f x)"
    using A and B by blast
  hence "s = t (⊆ {y. s: dom y ↝ dom x ∧ y ∈ avars a})"
    by (subst (asm) append_Nil [symmetric],
     simp only: sources.simps, auto)
  ultimately show ?thesis
    by blast
qed

lemma eq_states_while:
  assumes
    A: "S ⊆ {x. s = t (⊆ sources_aux (⟨bvars b⟩ # cs) vs s f x)}" and
    B: "S ≠ {}" and
    C: "s ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y)" and
    D: "Univ? A X ∪ Univ? C Y: bvars b ↝ UNIV"
  shows "s = t (⊆ bvars b)"
proof -
  from C have "{s}: bvars b ↝ UNIV"
  proof
    assume "s ∈ Univ A (⊆ state ∩ X)"
    then obtain r where E: "r ∈ A" and F: "s = r (⊆ state ∩ X)"
      by blast
    show ?thesis
    proof (cases "state ⊆ X")
      case True
      with F have "interf s = interf r"
        by (blast intro: interf_state)
      with D and E show ?thesis
        by (auto simp: univ_states_if_def split: if_split_asm)
    qed (insert D E, auto simp: univ_states_if_def split: if_split_asm)
  next
    assume "s ∈ Univ C (⊆ state ∩ Y)"
    then obtain r where E: "r ∈ C" and F: "s = r (⊆ state ∩ Y)"
      by blast
    show ?thesis
    proof (cases "state ⊆ Y")
      case True
      with F have "interf s = interf r"
        by (blast intro: interf_state)
      with D and E show ?thesis
        by (auto simp: univ_states_if_def split: if_split_asm)
    qed (insert D E, auto simp: univ_states_if_def split: if_split_asm)
  qed
  hence "∀x. bvars b ⊆ sources_aux (⟨bvars b⟩ # cs) vs s f x"
    by (blast intro!: sources_aux_observe_hd)
  thus ?thesis
    using A and B by blast
qed

lemma univ_states_while:
  assumes
    A: "(c, s, p) ⇒ (s', p')" and
    B: "⊨ b (⊆ A, X) = (B⇩1, B⇩2)" and
    C: "⊢ c (⊆ B⇩1, X) = (C, Y)" and
    D: "⊨ b (⊆ C, Y) = (B⇩1', B⇩2')" and
    E: "({}, False) ⊨ c (⊆ B⇩1, X) = Some (D, Z)" and
    F: "({}, False) ⊨ c (⊆ B⇩1', Y) = Some (D', Z')" and
    G: "bval b s"
  shows "s ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y) ⟹
    s' ∈ Univ A (⊆ state ∩ X) ∪ Univ C (⊆ state ∩ Y)"
proof (erule UnE)
  assume H: "s ∈ Univ A (⊆ state ∩ X)"
  have "s ∈ Univ B⇩1 (⊆ state ∩ X)"
    using G by (insert btyping2_approx [OF B H], simp)
  with A and E have "s' ∈ Univ D (⊆ state ∩ Z)"
    by (rule ctyping2_approx)
  moreover have "D ⊆ C ∧ Y ⊆ Z"
    using C and E by (rule ctyping1_ctyping2)
  ultimately show ?thesis
    by blast
next
  assume H: "s ∈ Univ C (⊆ state ∩ Y)"
  have "s ∈ Univ B⇩1' (⊆ state ∩ Y)"
    using G by (insert btyping2_approx [OF D H], simp)
  with A and F have "s' ∈ Univ D' (⊆ state ∩ Z')"
    by (rule ctyping2_approx)
  moreover obtain C' and Y' where I: "⊢ c (⊆ B⇩1', Y) = (C', Y')"
    by (cases "⊢ c (⊆ B⇩1', Y)", simp)
  hence "D' ⊆ C' ∧ Y' ⊆ Z'"
    using F by (rule ctyping1_ctyping2)
  ultimately have "s' ∈ Univ C' (⊆ state ∩ Y')"
    by blast
  moreover have J: "⊢ c (⊆ C, Y) = (C, Y)"
    using C by (rule ctyping1_idem)
  have "B⇩1' ⊆ C"
    using D by (blast dest: btyping2_un_eq)
  with J and I have "C' ⊆ C ∧ Y ⊆ Y'"
    by (rule ctyping1_mono, simp)
  ultimately show ?thesis
    by blast
qed

end

end