Theory Idempotence

(*  Title:       Information Flow Control via Stateful Intransitive Noninterference 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 "Idempotence of the auxiliary type system meant for loop bodies"

theory Idempotence
  imports Definitions
begin

text ‹
\null

The purpose of this section is to prove that the auxiliary type system @{const [names_short]
noninterf.ctyping1} used to simulate the execution of loop bodies is idempotent, namely that if its
output for a given input is the pair composed of @{typ "state set"} @{term B} and @{typ "vname set"}
@{term Y}, then the same output is returned if @{term B} and @{term Y} are fed back into the type
system (lemma @{text ctyping1_idem}).
›


subsection "Global context proofs"

lemma remdups_filter_last:
 "last [x←remdups xs. P x] = last [x←xs. P x]"
by (induction xs, auto simp: filter_empty_conv)

lemma remdups_append:
 "set xs ⊆ set ys ⟹ remdups (xs @ ys) = remdups ys"
by (induction xs, simp_all)

lemma remdups_concat_1:
 "remdups (concat (remdups [])) = remdups (concat [])"
by simp

lemma remdups_concat_2:
 "remdups (concat (remdups xs)) = remdups (concat xs) ⟹
    remdups (concat (remdups (x # xs))) = remdups (concat (x # xs))"
by (simp, subst (2 3) remdups_append2 [symmetric], clarsimp,
 subst remdups_append, auto)

lemma remdups_concat:
 "remdups (concat (remdups xs)) = remdups (concat xs)"
by (induction xs, rule remdups_concat_1, rule remdups_concat_2)


subsection "Local context proofs"

context noninterf
begin


lemma ctyping1_seq_last:
 "foldl (;;) S xs = (λx. let xs' = [T←xs. T x ≠ None] in
    if xs' = [] then S x else last xs' x)"
by (rule ext, induction xs rule: rev_induct, auto simp: ctyping1_seq_def)

lemma ctyping1_seq_remdups:
 "foldl (;;) S (remdups xs) = foldl (;;) S xs"
by (simp add: Let_def ctyping1_seq_last, subst remdups_filter_last,
 simp add: remdups_filter [symmetric])

lemma ctyping1_seq_remdups_concat:
 "foldl (;;) S (concat (remdups xs)) = foldl (;;) S (concat xs)"
by (subst (1 2) ctyping1_seq_remdups [symmetric], simp add: remdups_concat)

lemma ctyping1_seq_eq:
  assumes A: "foldl (;;) (λx. None) xs = foldl (;;) (λx. None) ys"
  shows "foldl (;;) S xs = foldl (;;) S ys"
proof -
  have "∀x. ([T←xs. T x ≠ None] = [] ⟷ [T←ys. T x ≠ None] = []) ∧
    last [T←xs. T x ≠ None] x = last [T←ys. T x ≠ None] x"
    (is "∀x. (?xs' x = [] ⟷ ?ys' x = []) ∧ _")
  proof
    fix x
    from A have "(if ?xs' x = [] then None else last (?xs' x) x) =
      (if ?ys' x = [] then None else last (?ys' x) x)"
      by (drule_tac fun_cong [where x = x], auto simp: ctyping1_seq_last)
    moreover have "?xs' x ≠ [] ⟹ last (?xs' x) x ≠ None"
      by (drule last_in_set, simp)
    moreover have "?ys' x ≠ [] ⟹ last (?ys' x) x ≠ None"
      by (drule last_in_set, simp)
    ultimately show "(?xs' x = [] ⟷ ?ys' x = []) ∧
      last (?xs' x) x = last (?ys' x) x"
      by (auto split: if_split_asm)
  qed
  thus ?thesis
    by (auto simp: ctyping1_seq_last)
qed


lemma ctyping1_merge_aux_butlast:
 "⟦ws ∈ A ⨆ B; butlast ws ≠ []⟧ ⟹
    snd (last (butlast ws)) = (¬ snd (last ws))"
by (erule ctyping1_merge_aux.cases, simp_all)

lemma ctyping1_merge_aux_distinct:
 "ws ∈ A ⨆ B ⟹ distinct ws"
by (induction rule: ctyping1_merge_aux.induct, simp_all)

lemma ctyping1_merge_aux_nonempty:
 "ws ∈ A ⨆ B ⟹ ws ≠ []"
by (induction rule: ctyping1_merge_aux.induct, simp_all)

lemma ctyping1_merge_aux_item:
 "⟦ws ∈ A ⨆ B; w ∈ set ws⟧ ⟹ fst w ∈ (if snd w then A else B)"
by (induction rule: ctyping1_merge_aux.induct, auto)

lemma ctyping1_merge_aux_take_1 [elim]:
 "⟦take n ws ∈ A ⨆ B; ¬ snd (last ws); xs ∈ A; (xs, True) ∉ set ws⟧ ⟹
    take n ws @ take (n - length ws) [(xs, True)] ∈ A ⨆ B"
by (cases "n ≤ length ws", auto)

lemma ctyping1_merge_aux_take_2 [elim]:
 "⟦take n ws ∈ A ⨆ B; snd (last ws); ys ∈ B; (ys, False) ∉ set ws⟧ ⟹
    take n ws @ take (n - length ws) [(ys, False)] ∈ A ⨆ B"
by (cases "n ≤ length ws", auto)

lemma ctyping1_merge_aux_take:
 "⟦ws ∈ A ⨆ B; 0 < n⟧ ⟹ take n ws ∈ A ⨆ B"
by (induction rule: ctyping1_merge_aux.induct, auto)


lemma ctyping1_merge_aux_drop_1 [elim]:
  assumes
    A: "xs ∈ A" and
    B: "ys ∈ B"
  shows "drop n [(xs, True)] @ [(ys, False)] ∈ A ⨆ B"
proof -
  from A have "[(xs, True)] ∈ A ⨆ B" ..
  with B have "[(xs, True)] @ [(ys, False)] ∈ A ⨆ B"
    by fastforce
  with B show ?thesis
    by (cases n, auto)
qed

lemma ctyping1_merge_aux_drop_2 [elim]:
  assumes
    A: "xs ∈ A" and
    B: "ys ∈ B"
  shows "drop n [(ys, False)] @ [(xs, True)] ∈ A ⨆ B"
proof -
  from B have "[(ys, False)] ∈ A ⨆ B" ..
  with A have "[(ys, False)] @ [(xs, True)] ∈ A ⨆ B"
    by fastforce
  with A show ?thesis
    by (cases n, auto)
qed

lemma ctyping1_merge_aux_drop_3:
  assumes
    A: "⋀xs v. (xs, True) ∉ set (drop n ws) ⟹
      xs ∈ A ⟹ v ⟹ drop n ws @ [(xs, True)] ∈ A ⨆ B" and
    B: "xs ∈ A" and
    C: "ys ∈ B" and
    D: "(xs, True) ∉ set ws" and
    E: "(ys, False) ∉ set (drop n ws)"
  shows "drop n ws @ drop (n - length ws) [(xs, True)] @
    [(ys, False)] ∈ A ⨆ B"
proof -
  have "set (drop n ws) ⊆ set ws"
    by (rule set_drop_subset)
  hence "drop n ws @ [(xs, True)] ∈ A ⨆ B"
    using A and B and D by blast
  hence "(drop n ws @ [(xs, True)]) @ [(ys, False)] ∈ A ⨆ B"
    using C and E by fastforce
  thus ?thesis
    using C by (cases "n ≤ length ws", auto)
qed

lemma ctyping1_merge_aux_drop_4:
  assumes
    A: "⋀ys v. (ys, False) ∉ set (drop n ws) ⟹
      ys ∈ B ⟹ ¬ v ⟹ drop n ws @ [(ys, False)] ∈ A ⨆ B" and
    B: "ys ∈ B" and
    C: "xs ∈ A" and
    D: "(ys, False) ∉ set ws" and
    E: "(xs, True) ∉ set (drop n ws)"
  shows "drop n ws @ drop (n - length ws) [(ys, False)] @
    [(xs, True)] ∈ A ⨆ B"
proof -
  have "set (drop n ws) ⊆ set ws"
    by (rule set_drop_subset)
  hence "drop n ws @ [(ys, False)] ∈ A ⨆ B"
    using A and B and D by blast
  hence "(drop n ws @ [(ys, False)]) @ [(xs, True)] ∈ A ⨆ B"
    using C and E by fastforce
  thus ?thesis
    using C by (cases "n ≤ length ws", auto)
qed

lemma ctyping1_merge_aux_drop:
 "⟦ws ∈ A ⨆ B; w ∉ set (drop n ws);
    fst w ∈ (if snd w then A else B); snd w = (¬ snd (last ws))⟧ ⟹
  drop n ws @ [w] ∈ A ⨆ B"
proof (induction arbitrary: w rule: ctyping1_merge_aux.induct)
  fix xs ws w
  show
   "⟦ws ∈ A ⨆ B;
    ⋀w. w ∉ set (drop n ws) ⟹
      fst w ∈ (if snd w then A else B) ⟹
      snd w = (¬ snd (last ws)) ⟹
      drop n ws @ [w] ∈ A ⨆ B;
    ¬ snd (last ws);
    xs ∈ A;
    (xs, True) ∉ set ws;
    w ∉ set (drop n (ws @ [(xs, True)]));
    fst w ∈ (if snd w then A else B);
    snd w = (¬ snd (last (ws @ [(xs, True)])))⟧ ⟹
      drop n (ws @ [(xs, True)]) @ [w] ∈ A ⨆ B"
    by (cases w, auto intro: ctyping1_merge_aux_drop_3)
next
  fix ys ws w
  show
   "⟦ws ∈ A ⨆ B;
    ⋀w. w ∉ set (drop n ws) ⟹
      fst w ∈ (if snd w then A else B) ⟹
      snd w = (¬ snd (last ws)) ⟹
      drop n ws @ [w] ∈ A ⨆ B;
    snd (last ws);
    ys ∈ B;
    (ys, False) ∉ set ws;
    w ∉ set (drop n (ws @ [(ys, False)]));
    fst w ∈ (if snd w then A else B);
    snd w = (¬ snd (last (ws @ [(ys, False)])))⟧ ⟹
      drop n (ws @ [(ys, False)]) @ [w] ∈ A ⨆ B"
    by (cases w, auto intro: ctyping1_merge_aux_drop_4)
qed auto


lemma ctyping1_merge_aux_closed_1:
  assumes
    A: "∀vs. length vs ≤ length us ⟶
      (∀ls rs. vs = ls @ rs ⟶ ls ∈ A ⨆ B ⟶ rs ∈ A ⨆ B ⟶
        (∃ws ∈ A ⨆ B. foldl (;;) (λx. None) (concat (map fst ws)) =
          foldl (;;) (λx. None) (concat (map fst (ls @ rs))) ∧
        length ws ≤ length (ls @ rs) ∧ snd (last ws) = snd (last rs)))"
      (is "∀_. _ ⟶ (∀ls rs. _ ⟶ _ ⟶ _ ⟶ (∃ws ∈ _. ?P ws ls rs))") and
    B: "us ∈ A ⨆ B" and
    C: "fst v ∈ (if snd v then A else B)" and
    D: "snd v = (¬ snd (last us))"
  shows "∃ws ∈ A ⨆ B. foldl (;;) (λx. None) (concat (map fst ws)) =
    foldl (;;) (λx. None) (concat (map fst (us @ [v]))) ∧
    length ws ≤ Suc (length us) ∧ snd (last ws) = snd v"
proof (cases "v ∈ set us", cases "hd us = v")
  assume E: "hd us = v"
  moreover have "distinct us"
    using B by (rule ctyping1_merge_aux_distinct)
  ultimately have "v ∉ set (drop (Suc 0) us)"
    by (cases us, simp_all)
  with B have "drop (Suc 0) us @ [v] ∈ A ⨆ B"
    (is "?ws ∈ _")
    using C and D by (rule ctyping1_merge_aux_drop)
  moreover have "foldl (;;) (λx. None) (concat (map fst ?ws)) =
    foldl (;;) (λx. None) (concat (map fst (us @ [v])))"
    using E by (cases us, simp, subst (1 2) ctyping1_seq_remdups_concat
     [symmetric], simp)
  ultimately show ?thesis
    by fastforce
next
  assume "v ∈ set us"
  then obtain ls and rs where E: "us = ls @ v # rs ∧ v ∉ set rs"
    by (blast dest: split_list_last)
  moreover assume "hd us ≠ v"
  ultimately have "ls ≠ []"
    by (cases ls, simp_all)
  hence "take (length ls) us ∈ A ⨆ B"
    by (simp add: ctyping1_merge_aux_take B)
  moreover have "v ∉ set (drop (Suc (length ls)) us)"
    using E by simp
  with B have "drop (Suc (length ls)) us @ [v] ∈ A ⨆ B"
    using C and D by (rule ctyping1_merge_aux_drop)
  ultimately have "∃ws ∈ A ⨆ B. ?P ws ls (rs @ [v])"
    using A and E by (drule_tac spec [of _ "ls @ rs @ [v]"],
     simp, drule_tac spec [of _ ls], simp)
  moreover have "foldl (;;) (λx. None) (concat (map fst (ls @ rs @ [v]))) =
    foldl (;;) (λx. None) (concat (map fst (us @ [v])))"
    using E by (subst (1 2) ctyping1_seq_remdups_concat [symmetric],
     simp, subst (1 2) remdups_append2 [symmetric], simp)
  ultimately show ?thesis
    using E by auto
next
  assume E: "v ∉ set us"
  show ?thesis
  proof (rule bexI [of _ "us @ [v]"])
    show "foldl (;;) (λx. None) (concat (map fst (us @ [v]))) =
      foldl (;;) (λx. None) (concat (map fst (us @ [v]))) ∧
      length (us @ [v]) ≤ Suc (length us) ∧
      snd (last (us @ [v])) = snd v"
      by simp
  next
    from B and C and D and E show "us @ [v] ∈ A ⨆ B"
      by (cases v, cases "snd (last us)", auto)
  qed
qed

lemma ctyping1_merge_aux_closed:
  assumes
    A: "∀xs ∈ A. ∀ys ∈ A. ∃zs ∈ A.
      foldl (;;) (λx. None) zs = foldl (;;) (λx. None) (xs @ ys)" and
    B: "∀xs ∈ B. ∀ys ∈ B. ∃zs ∈ B.
      foldl (;;) (λx. None) zs = foldl (;;) (λx. None) (xs @ ys)"
  shows "⟦us ∈ A ⨆ B; vs ∈ A ⨆ B⟧ ⟹
    ∃ws ∈ A ⨆ B. foldl (;;) (λx. None) (concat (map fst ws)) =
      foldl (;;) (λx. None) (concat (map fst (us @ vs))) ∧
    length ws ≤ length (us @ vs) ∧ snd (last ws) = snd (last vs)"
    (is "⟦_; _⟧ ⟹ ∃ws ∈ _. ?P ws us vs")
proof (induction "us @ vs" arbitrary: us vs rule: length_induct)
  fix us vs
  let ?f = "foldl (;;) (λx. None)"
  assume
    C: "∀ts. length ts < length (us @ vs) ⟶
      (∀ls rs. ts = ls @ rs ⟶ ls ∈ A ⨆ B ⟶ rs ∈ A ⨆ B ⟶
        (∃ws ∈ A ⨆ B. ?f (concat (map fst ws)) =
          ?f (concat (map fst (ls @ rs))) ∧
        length ws ≤ length (ls @ rs) ∧ snd (last ws) = snd (last rs)))"
      (is "∀_. _ ⟶ (∀ls rs. _ ⟶ _ ⟶ _ ⟶ (∃ws ∈ _. ?Q ws ls rs))") and
    D: "us ∈ A ⨆ B" and
    E: "vs ∈ A ⨆ B"
  {
    fix vs' v
    assume F: "vs = vs' @ [v]"
    have "∃ws ∈ A ⨆ B. ?f (concat (map fst ws)) =
      ?f (concat (map fst (us @ vs' @ [v]))) ∧
      length ws ≤ Suc (length us + length vs') ∧ snd (last ws) = snd v"
    proof (cases vs', cases "(¬ snd (last us)) = snd v")
      assume "vs' = []" and "(¬ snd (last us)) = snd v"
      thus ?thesis
        using ctyping1_merge_aux_closed_1 [OF _ D] and
         ctyping1_merge_aux_item [OF E] and C and F
         by (auto simp: less_Suc_eq_le)
    next
      have G: "us ≠ []"
        using D by (rule ctyping1_merge_aux_nonempty)
      hence "fst (last us) ∈ (if snd (last us) then A else B)"
        using ctyping1_merge_aux_item and D by auto
      moreover assume H: "(¬ snd (last us)) ≠ snd v"
      ultimately have "fst (last us) ∈ (if snd v then A else B)"
        by simp
      moreover have "fst v ∈ (if snd v then A else B)"
        using ctyping1_merge_aux_item and E and F by auto
      ultimately have "∃zs ∈ if snd v
        then A else B. ?f zs = ?f (concat (map fst [last us, v]))"
        (is "∃zs ∈ _. ?R zs")
        using A and B by auto
      then obtain zs where
        I: "zs ∈ (if snd v then A else B)" and J: "?R zs" ..
      let ?w = "(zs, snd v)"
      assume K: "vs' = []"
      {
        fix us' u
        assume Cons: "butlast us = u # us'"
        hence L: "snd v = (¬ snd (last (butlast us)))"
          using D and H by (drule_tac ctyping1_merge_aux_butlast, simp_all)
        let ?S = "?f (concat (map fst (butlast us)))"
        have "take (length (butlast us)) us ∈ A ⨆ B"
          using Cons by (auto intro: ctyping1_merge_aux_take [OF D])
        hence M: "butlast us ∈ A ⨆ B"
          by (subst (asm) (2) append_butlast_last_id [OF G, symmetric], simp)
        have N: "∀ts. length ts < length (butlast us @ [last us, v]) ⟶
          (∀ls rs. ts = ls @ rs ⟶ ls ∈ A ⨆ B ⟶ rs ∈ A ⨆ B ⟶
            (∃ws ∈ A ⨆ B. ?Q ws ls rs))"
          using C and F and K by (subst (asm) append_butlast_last_id
           [OF G, symmetric], simp)
        have "∃ws ∈ A ⨆ B. ?f (concat (map fst ws)) =
          ?f (concat (map fst (butlast us @ [?w]))) ∧
          length ws ≤ Suc (length (butlast us)) ∧ snd (last ws) = snd ?w"
        proof (rule ctyping1_merge_aux_closed_1)
          show "∀ts. length ts ≤ length (butlast us) ⟶
            (∀ls rs. ts = ls @ rs ⟶ ls ∈ A ⨆ B ⟶ rs ∈ A ⨆ B ⟶
              (∃ws ∈ A ⨆ B. ?Q ws ls rs))"
            using N by force
        next
          from M show "butlast us ∈ A ⨆ B" .
        next
          show "fst (zs, snd v) ∈ (if snd (zs, snd v) then A else B)"
            using I by simp
        next
          show "snd (zs, snd v) = (¬ snd (last (butlast us)))"
            using L by simp
        qed
        moreover have "foldl (;;) ?S zs =
          foldl (;;) ?S (concat (map fst [last us, v]))"
          using J by (rule ctyping1_seq_eq)
        ultimately have "∃ws ∈ A ⨆ B. ?f (concat (map fst ws)) =
          ?f (concat (map fst ((butlast us @ [last us]) @ [v]))) ∧
          length ws ≤ Suc (length us) ∧ snd (last ws) = snd v"
          by auto
      }
      with K and I and J show ?thesis
        by (simp, subst append_butlast_last_id [OF G, symmetric],
         cases "butlast us", (force split: if_split_asm)+)
    next
      case Cons
      hence "take (length vs') vs ∈ A ⨆ B"
        by (auto intro: ctyping1_merge_aux_take [OF E])
      hence "vs' ∈ A ⨆ B"
        using F by simp
      then obtain ws where G: "ws ∈ A ⨆ B" and H: "?Q ws us vs'"
        using C and D and F by force
      have I: "∀ts. length ts ≤ length ws ⟶
          (∀ls rs. ts = ls @ rs ⟶ ls ∈ A ⨆ B ⟶ rs ∈ A ⨆ B ⟶
            (∃ws ∈ A ⨆ B. ?Q ws ls rs))"
      proof (rule allI, rule impI)
        fix ts :: "(state_upd list × bool) list"
        assume J: "length ts ≤ length ws"
        show "∀ls rs. ts = ls @ rs ⟶ ls ∈ A ⨆ B ⟶ rs ∈ A ⨆ B ⟶
          (∃ws ∈ A ⨆ B. ?Q ws ls rs)"
        proof (rule spec [OF C, THEN mp])
          show "length ts < length (us @ vs)"
            using F and H and J by simp
        qed
      qed
      hence J: "snd (last (butlast vs)) = (¬ snd (last vs))"
        by (metis E F Cons butlast_snoc ctyping1_merge_aux_butlast
         list.distinct(1))
      have "∃ws' ∈ A ⨆ B. ?f (concat (map fst ws')) =
        ?f (concat (map fst (ws @ [v]))) ∧
        length ws' ≤ Suc (length ws) ∧ snd (last ws') = snd v"
      proof (rule ctyping1_merge_aux_closed_1 [OF I G])
        show "fst v ∈ (if snd v then A else B)"
          by (rule ctyping1_merge_aux_item [OF E], simp add: F)
      next
        show "snd v = (¬ snd (last ws))"
          using F and H and J by simp
      qed
      thus ?thesis
        using H by auto
    qed
  }
  note F = this
  show "∃ws ∈ A ⨆ B. ?P ws us vs"
  proof (rule rev_cases [of vs])
    assume "vs = []"
    thus ?thesis
      by (simp add: ctyping1_merge_aux_nonempty [OF E])
  next
    fix vs' v
    assume "vs = vs' @ [v]"
    thus ?thesis
      using F by simp
  qed
qed


lemma ctyping1_merge_closed:
  assumes
    A: "∀xs ∈ A. ∀ys ∈ A. ∃zs ∈ A.
      foldl (;;) (λx. None) zs = foldl (;;) (λx. None) (xs @ ys)" and
    B: "∀xs ∈ B. ∀ys ∈ B. ∃zs ∈ B.
      foldl (;;) (λx. None) zs = foldl (;;) (λx. None) (xs @ ys)" and
    C: "xs ∈ A ⊔ B" and
    D: "ys ∈ A ⊔ B"
  shows "∃zs ∈ A ⊔ B. foldl (;;) (λx. None) zs =
    foldl (;;) (λx. None) (xs @ ys)"
proof -
  let ?f = "foldl (;;) (λx. None)"
  obtain us where "us ∈ A ⨆ B" and
    E: "xs = concat (map fst us)"
    using C by (auto simp: ctyping1_merge_def)
  moreover obtain vs where "vs ∈ A ⨆ B" and
    F: "ys = concat (map fst vs)"
    using D by (auto simp: ctyping1_merge_def)
  ultimately have "∃ws ∈ A ⨆ B. ?f (concat (map fst ws)) =
    ?f (concat (map fst (us @ vs))) ∧
    length ws ≤ length (us @ vs) ∧ snd (last ws) = snd (last vs)"
    using A and B by (blast intro: ctyping1_merge_aux_closed)
  then obtain ws where "ws ∈ A ⨆ B" and
   "?f (concat (map fst ws)) = ?f (xs @ ys)"
    using E and F by auto
  thus ?thesis
    by (auto simp: ctyping1_merge_def)
qed

lemma ctyping1_merge_append_closed:
  assumes
    A: "∀xs ∈ A. ∀ys ∈ A. ∃zs ∈ A.
      foldl (;;) (λx. None) zs = foldl (;;) (λx. None) (xs @ ys)" and
    B: "∀xs ∈ B. ∀ys ∈ B. ∃zs ∈ B.
      foldl (;;) (λx. None) zs = foldl (;;) (λx. None) (xs @ ys)" and
    C: "xs ∈ A ⊔⇩@ B" and
    D: "ys ∈ A ⊔⇩@ B"
  shows "∃zs ∈ A ⊔⇩@ B. foldl (;;) (λx. None) zs =
    foldl (;;) (λx. None) (xs @ ys)"
proof -
  let ?f = "foldl (;;) (λx. None)"
  {
    assume E: "card B = Suc 0"
    moreover from C and this obtain as bs where
     "xs = as @ bs ∧ as ∈ A ∧ bs ∈ B"
      by (auto simp: ctyping1_append_def ctyping1_merge_append_def)
    moreover from D and E obtain as' bs' where
     "ys = as' @ bs' ∧ as' ∈ A ∧ bs' ∈ B"
      by (auto simp: ctyping1_append_def ctyping1_merge_append_def)
    ultimately have F: "xs @ ys = as @ bs @ as' @ bs ∧
      {as, as'} ⊆ A ∧ bs ∈ B"
      by (auto simp: card_1_singleton_iff)
    hence "?f (xs @ ys) = ?f (remdups (as @ remdups (bs @ as' @ bs)))"
      by (simp add: ctyping1_seq_remdups)
    also have "… = ?f (remdups (as @ remdups (as' @ bs)))"
      by (simp add: remdups_append)
    finally have G: "?f (xs @ ys) = ?f (as @ as' @ bs)"
      by (simp add: ctyping1_seq_remdups)
    obtain as'' where H: "as'' ∈ A" and I: "?f as'' = ?f (as @ as')"
      using A and F by auto
    have "∃zs ∈ A @ B. ?f zs = ?f (xs @ ys)"
    proof (rule bexI [of _ "as'' @ bs"])
      show "foldl (;;) (λx. None) (as'' @ bs) =
        foldl (;;) (λx. None) (xs @ ys)"
        using G and I by simp
    next
      show "as'' @ bs ∈ A @ B"
        using F and H by (auto simp: ctyping1_append_def)
    qed
  }
  moreover {
    fix n
    assume E: "card B ≠ Suc 0"
    moreover from C and this obtain ws bs where
     "xs = ws @ bs ∧ ws ∈ A ⊔ B ∧ bs ∈ B"
      by (auto simp: ctyping1_append_def ctyping1_merge_append_def)
    moreover from D and E obtain ws' bs' where
     "ys = ws' @ bs' ∧ ws' ∈ A ⊔ B ∧ bs' ∈ B"
      by (auto simp: ctyping1_append_def ctyping1_merge_append_def)
    ultimately have F: "xs @ ys = ws @ bs @ ws' @ bs' ∧
      {ws, ws'} ⊆ A ⊔ B ∧ {bs, bs'} ⊆ B"
      by simp
    hence "[(bs, False)] ∈ A ⨆ B"
      by blast
    hence G: "bs ∈ A ⊔ B"
      by (force simp: ctyping1_merge_def)
    have "∃vs ∈ A ⊔ B. ?f vs = ?f (ws @ bs)"
      (is "∃vs ∈ _. ?P vs ws bs")
    proof (rule ctyping1_merge_closed)
      show "∀xs ∈ A. ∀ys ∈ A. ∃zs ∈ A. foldl (;;) (λx. None) zs =
        foldl (;;) (λx. None) (xs @ ys)"
        using A by simp
    next
      show "∀xs ∈ B. ∀ys ∈ B. ∃zs ∈ B. foldl (;;) (λx. None) zs =
        foldl (;;) (λx. None) (xs @ ys)"
        using B by simp
    next
      show "ws ∈ A ⊔ B"
        using F by simp
    next
      from G show "bs ∈ A ⊔ B" .
    qed
    then obtain vs where H: "vs ∈ A ⊔ B" and I: "?P vs ws bs" ..
    have "∃vs' ∈ A ⊔ B. ?P vs' vs ws'"
    proof (rule ctyping1_merge_closed)
      show "∀xs ∈ A. ∀ys ∈ A. ∃zs ∈ A. foldl (;;) (λx. None) zs =
        foldl (;;) (λx. None) (xs @ ys)"
        using A by simp
    next
      show "∀xs ∈ B. ∀ys ∈ B. ∃zs ∈ B. foldl (;;) (λx. None) zs =
        foldl (;;) (λx. None) (xs @ ys)"
        using B by simp
    next
      from H show "vs ∈ A ⊔ B" .
    next
      show "ws' ∈ A ⊔ B"
        using F by simp
    qed
    then obtain vs' where J: "vs' ∈ A ⊔ B" and K: "?P vs' vs ws'" ..
    have "∃zs ∈ A ⊔ B @ B. ?f zs = ?f (xs @ ys)"
    proof (rule bexI [of _ "vs' @ bs'"])
      show "foldl (;;) (λx. None) (vs' @ bs') =
        foldl (;;) (λx. None) (xs @ ys)"
        using F and I and K by simp
    next
      show "vs' @ bs' ∈ A ⊔ B @ B"
        using F and J by (auto simp: ctyping1_append_def)
    qed
  }
  ultimately show ?thesis
    using A and B and C and D by (auto simp: ctyping1_merge_append_def)
qed

lemma ctyping1_aux_closed:
 "⟦xs ∈ ⊢ c; ys ∈ ⊢ c⟧ ⟹ ∃zs ∈ ⊢ c. foldl (;;) (λx. None) zs =
    foldl (;;) (λx. None) (xs @ ys)"
by (induction c arbitrary: xs ys, auto
 intro: ctyping1_merge_closed ctyping1_merge_append_closed
 simp: Let_def ctyping1_seq_def simp del: foldl_append)


lemma ctyping1_idem_1:
  assumes
    A: "s ∈ A" and
    B: "xs ∈ ⊢ c" and
    C: "ys ∈ ⊢ c"
  shows "∃f r.
    (∃t.
      (λx. case foldl (;;) (λx. None) ys x of
        None ⇒ case foldl (;;) (λx. None) xs x of
          None ⇒ s x | Some None ⇒ t' x | Some (Some i) ⇒ i |
        Some None ⇒ t'' x | Some (Some i) ⇒ i) =
      (λx. case f x of
        None ⇒ r x | Some None ⇒ t x | Some (Some i) ⇒ i)) ∧
    (∃zs. f = foldl (;;) (λx. None) zs ∧ zs ∈ ⊢ c) ∧
    r ∈ A"
proof -
  let ?f = "foldl (;;) (λx. None)"
  let ?t = "λx. case ?f ys x of
    None ⇒ case ?f xs x of Some None ⇒ t' x | _ ⇒ (0 :: val) |
    Some None ⇒ t'' x | _ ⇒ 0"
  have "∃zs ∈ ⊢ c. ?f zs = ?f (xs @ ys)"
    using B and C by (rule ctyping1_aux_closed)
  then obtain zs where "zs ∈ ⊢ c" and "?f zs = ?f (xs @ ys)" ..
  with A show ?thesis
    by (rule_tac exI [of _ "?f zs"], rule_tac exI [of _ s],
     rule_tac conjI, rule_tac exI [of _ ?t], fastforce dest: last_in_set
     simp: Let_def ctyping1_seq_last split: option.split, blast)
qed

lemma ctyping1_idem_2:
  assumes
    A: "s ∈ A" and
    B: "xs ∈ ⊢ c"
  shows "∃f r.
    (∃t.
      (λx. case foldl (;;) (λx. None) xs x of
        None ⇒ s x | Some None ⇒ t' x | Some (Some i) ⇒ i) =
      (λx. case f x of
        None ⇒ r x | Some None ⇒ t x | Some (Some i) ⇒ i)) ∧
    (∃xs. f = foldl (;;) (λx. None) xs ∧ xs ∈ ⊢ c) ∧
    (∃f s.
      (∃t. r = (λx. case f x of
        None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i)) ∧
      (∃xs. f = foldl (;;) (λx. None) xs ∧ xs ∈ ⊢ c) ∧
      s ∈ A)"
proof -
  let ?f = "foldl (;;) (λx. None)"
  let ?g = "λf s t x. case f x of
    None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i"
  show ?thesis
    by (rule exI [of _ "?f xs"], rule exI [of _ "?g (?f xs) s t'"],
     (fastforce simp: A B split: option.split)+)
qed

lemma ctyping1_idem:
 "⊢ c (⊆ A, X) = (B, Y) ⟹ ⊢ c (⊆ B, Y) = (B, Y)"
by (cases "A = {}", auto simp: ctyping1_def
 intro: ctyping1_idem_1 ctyping1_idem_2)

end

end