Theory Overapproximation

(*  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 "Overapproximation of program semantics by the main type system"

theory Overapproximation
  imports Idempotence
begin

text ‹
\null

As in my previous paper cite‹"Noce24"›, the purpose of this section is to prove that type system
@{const [names_short] noninterf.ctyping2} overapproximates program semantics, namely that if (a)
@{prop "(c, s, p) ⇒ (t, q)"}, (b) the type system outputs a @{typ "state set"} @{term B} and a
@{typ "vname set"} @{term Y} when it is input program @{term c}, @{typ "state set"} @{term A}, and
@{typ "vname set"} @{term X}, and (c) state @{term s} agrees with some state in @{term A} on the
value of each state variable in @{term X}, then @{term t} must agree with some state in @{term B} on
the value of each state variable in @{term Y} (lemma @{text ctyping2_approx}).

This proof makes use of the lemma @{text ctyping1_idem} proven in the previous section.
›


subsection "Global context proofs"

lemma avars_aval:
 "s = t (⊆ avars a) ⟹ aval a s = aval a t"
by (induction a, simp_all)


subsection "Local context proofs"

context noninterf
begin


lemma interf_set_mono:
 "⟦A' ⊆ A; X ⊆ X'; ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y;
    ∀(B, Y) ∈ insert (Univ? A X, Z) U. B: Y ↝ W⟧ ⟹
  ∀(B, Y) ∈ insert (Univ? A' X', Z) U'. B: Y ↝ W"
by (subgoal_tac "Univ? A' X' ⊆ Univ? A X", fastforce,
 auto simp: univ_states_if_def)


lemma btyping1_btyping2_aux_1 [elim]:
  assumes
    A: "avars a1 = {}" and
    B: "avars a2 = {}" and
    C: "aval a1 (λx. 0) < aval a2 (λx. 0)"
  shows "aval a1 s < aval a2 s"
proof -
  have "aval a1 s = aval a1 (λx. 0) ∧ aval a2 s = aval a2 (λx. 0)"
    using A and B by (blast intro: avars_aval)
  thus ?thesis
    using C by simp
qed

lemma btyping1_btyping2_aux_2 [elim]:
  assumes
    A: "avars a1 = {}" and
    B: "avars a2 = {}" and
    C: "¬ aval a1 (λx. 0) < aval a2 (λx. 0)" and
    D: "aval a1 s < aval a2 s"
  shows False
proof -
  have "aval a1 s = aval a1 (λx. 0) ∧ aval a2 s = aval a2 (λx. 0)"
    using A and B by (blast intro: avars_aval)
  thus ?thesis
    using C and D by simp
qed

lemma btyping1_btyping2_aux:
 "⊢ b = Some v ⟹ ⊫ b (⊆ A, X) = Some (if v then A else {})"
by (induction b arbitrary: v, auto split: if_split_asm option.split_asm)

lemma btyping1_btyping2:
 "⊢ b = Some v ⟹ ⊨ b (⊆ A, X) = (if v then (A, {}) else ({}, A))"
by (simp add: btyping2_def btyping1_btyping2_aux)

lemma btyping2_aux_subset:
 "⊫ b (⊆ A, X) = Some A' ⟹ A' = {s. s ∈ A ∧ bval b s}"
by (induction b arbitrary: A', auto split: if_split_asm option.split_asm)

lemma btyping2_aux_diff:
 "⟦⊫ b (⊆ A, X) = Some B; ⊫ b (⊆ A', X') = Some B'; A' ⊆ A; B' ⊆ B⟧ ⟹
    A' - B' ⊆ A - B"
by (blast dest: btyping2_aux_subset)

lemma btyping2_aux_mono:
 "⟦⊫ b (⊆ A, X) = Some B; A' ⊆ A; X ⊆ X'⟧ ⟹
    ∃B'. ⊫ b (⊆ A', X') = Some B' ∧ B' ⊆ B"
by (induction b arbitrary: B, auto dest: btyping2_aux_diff split:
 if_split_asm option.split_asm)

lemma btyping2_mono:
 "⟦⊨ b (⊆ A, X) = (B1, B2); ⊨ b (⊆ A', X') = (B1', B2'); A' ⊆ A; X ⊆ X'⟧ ⟹
    B1' ⊆ B1 ∧ B2' ⊆ B2"
by (simp add: btyping2_def split: option.split_asm,
 frule_tac [3-4] btyping2_aux_mono, auto dest: btyping2_aux_subset)

lemma btyping2_un_eq:
 "⊨ b (⊆ A, X) = (B1, B2) ⟹ B1 ∪ B2 = A"
by (auto simp: btyping2_def dest: btyping2_aux_subset split: option.split_asm)

lemma btyping2_aux_eq:
 "⟦⊫ b (⊆ A, X) = Some A'; s = t (⊆ state ∩ X)⟧ ⟹ bval b s = bval b t"
proof (induction b arbitrary: A')
  fix A' v
  show
   "⟦⊫ Bc v (⊆ A, X) = Some A'; s = t (⊆ state ∩ X)⟧ ⟹
      bval (Bc v) s = bval (Bc v) t"
    by simp
next
  fix A' b
  show
   "⟦⋀A'. ⊫ b (⊆ A, X) = Some A' ⟹ s = t (⊆ state ∩ X) ⟹
      bval b s = bval b t;
    ⊫ Not b (⊆ A, X) = Some A'; s = t (⊆ state ∩ X)⟧ ⟹
      bval (Not b) s = bval (Not b) t"
    by (simp split: option.split_asm)
next
  fix A' b1 b2
  show
   "⟦⋀A'. ⊫ b1 (⊆ A, X) = Some A' ⟹ s = t (⊆ state ∩ X) ⟹
      bval b1 s = bval b1 t;
    ⋀A'. ⊫ b2 (⊆ A, X) = Some A' ⟹ s = t (⊆ state ∩ X) ⟹
      bval b2 s = bval b2 t;
    ⊫ And b1 b2 (⊆ A, X) = Some A'; s = t (⊆ state ∩ X)⟧ ⟹
      bval (And b1 b2) s = bval (And b1 b2) t"
    by (simp split: option.split_asm)
next
  fix A' a1 a2
  show
   "⟦⊫ Less a1 a2 (⊆ A, X) = Some A'; s = t (⊆ state ∩ X)⟧ ⟹
      bval (Less a1 a2) s = bval (Less a1 a2) t"
    by (subgoal_tac "aval a1 s = aval a1 t",
     subgoal_tac "aval a2 s = aval a2 t",
     auto intro!: avars_aval split: if_split_asm)
qed


lemma ctyping1_mono_fst:
 "⟦⊢ c (⊆ A, X) = (B, Y); ⊢ c (⊆ A', X') = (B', Y'); A' ⊆ A⟧ ⟹
    B' ⊆ B"
by (fastforce simp: ctyping1_def)

lemma ctyping1_mono:
  assumes
    A: "⊢ c (⊆ A, X) = (B, Y)" and
    B: "⊢ c (⊆ A', X') = (B', Y')" and
    C: "A' ⊆ A" and
    D: "X ⊆ X'"
  shows "B' ⊆ B ∧ Y ⊆ Y'"
proof (rule conjI, rule ctyping1_mono_fst [OF A B C])
  {
    fix x
    assume "x ∉ Univ?? A' {x. ∀f ∈ {λx. [y←ys. fst y = x] | ys. ys ∈ ⊢ c}.
      if f x = [] then x ∈ X' else snd (last (f x)) ≠ None}"
    moreover from this have "A' ≠ {}"
      by (simp split: if_split_asm)
    ultimately have "¬ (∀f.
      (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c) ⟶
        (if f x = [] then x ∈ X' else snd (last (f x)) ≠ None))"
      (is "¬ ?P X'")
      by (auto split: if_split_asm)
    moreover assume "?P X"
    hence "?P X'"
      using D by fastforce
    ultimately have False
      by contradiction
  }
  with A and B and C show "Y ⊆ Y'"
    by (cases "A = {}", auto simp: ctyping1_def)
qed


lemma ctyping2_mono_skip [elim!]:
 "⟦(U, False) ⊨ SKIP (⊆ A, X) = Some (C, Z); A' ⊆ A; X ⊆ X'⟧ ⟹
    ∃C' Z'. (U', False) ⊨ SKIP (⊆ A', X') = Some (C', Z') ∧
      C' ⊆ C ∧ Z ⊆ Z'"
by (clarsimp, subgoal_tac "Univ?? C X = X", force+)

lemma ctyping2_mono_assign [elim!]:
 "⟦(U, False) ⊨ x ::= a (⊆ A, X) = Some (C, Z); A' ⊆ A; X ⊆ X';
    ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y⟧ ⟹
  ∃C' Z'. (U', False) ⊨ x ::= a (⊆ A', X') = Some (C', Z') ∧
    C' ⊆ C ∧ Z ⊆ Z'"
by (frule interf_set_mono [where W = "{x}"], auto split: if_split_asm)

lemma ctyping2_mono_input [elim!]:
 "⟦(U, False) ⊨ IN x (⊆ A, X) = Some (C, Z); A' ⊆ A; X ⊆ X';
    ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y⟧ ⟹
  ∃C' Z'. (U', False) ⊨ IN x (⊆ A', X') = Some (C', Z') ∧
    C' ⊆ C ∧ Z ⊆ Z'"
by (frule interf_set_mono [where W = "{x}"], auto split: if_split_asm)

lemma ctyping2_mono_output [elim!]:
 "⟦(U, False) ⊨ OUT x (⊆ A, X) = Some (C, Z); A' ⊆ A; X ⊆ X';
    ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y⟧ ⟹
  ∃C' Z'. (U', False) ⊨ OUT x (⊆ A', X') = Some (C', Z') ∧
    C' ⊆ C ∧ Z ⊆ Z'"
by (frule interf_set_mono [where W = "{x}"], auto split: if_split_asm)

lemma ctyping2_mono_seq:
  assumes
    A: "⋀A' B X' Y U'.
      (U, False) ⊨ c1 (⊆ A, X) = Some (B, Y) ⟹ A' ⊆ A ⟹ X ⊆ X' ⟹
        ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y ⟹
          ∃B' Y'. (U', False) ⊨ c1 (⊆ A', X') = Some (B', Y') ∧
            B' ⊆ B ∧ Y ⊆ Y'" and
    B: "⋀p B Y B' C Y' Z U'.
      (U, False) ⊨ c1 (⊆ A, X) = Some p ⟹ (B, Y) = p ⟹
        (U, False) ⊨ c2 (⊆ B, Y) = Some (C, Z) ⟹ B' ⊆ B ⟹ Y ⊆ Y' ⟹
          ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y ⟹
            ∃C' Z'. (U', False) ⊨ c2 (⊆ B', Y') = Some (C', Z') ∧
              C' ⊆ C ∧ Z ⊆ Z'" and
    C: "(U, False) ⊨ c1;; c2 (⊆ A, X) = Some (C, Z)" and
    D: "A' ⊆ A" and
    E: "X ⊆ X'" and
    F: "∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y"
  shows "∃C' Z'. (U', False) ⊨ c1;; c2 (⊆ A', X') = Some (C', Z') ∧
    C' ⊆ C ∧ Z ⊆ Z'"
proof -
  obtain B Y where "(U, False) ⊨ c1 (⊆ A, X) = Some (B, Y) ∧
    (U, False) ⊨ c2 (⊆ B, Y) = Some (C, Z)"
    using C by (auto split: option.split_asm)
  moreover from this obtain B' Y' where
    G: "(U', False) ⊨ c1 (⊆ A', X') = Some (B', Y') ∧ B' ⊆ B ∧ Y ⊆ Y'"
    using A and D and E and F by fastforce
  ultimately obtain C' Z' where
   "(U', False) ⊨ c2 (⊆ B', Y') = Some (C', Z') ∧ C' ⊆ C ∧ Z ⊆ Z'"
    using B and F by fastforce
  thus ?thesis
    using G by simp
qed

lemma ctyping2_mono_or:
  assumes
    A: "⋀A' C1 X' Y1 U'.
      (U, False) ⊨ c1 (⊆ A, X) = Some (C1, Y1) ⟹ A' ⊆ A ⟹ X ⊆ X' ⟹
        ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y ⟹
          ∃C1' Y1'. (U', False) ⊨ c1 (⊆ A', X') = Some (C1', Y1') ∧
            C1' ⊆ C1 ∧ Y1 ⊆ Y1'" and
    B: "⋀A' C2 X' Y2 U'.
      (U, False) ⊨ c2 (⊆ A, X) = Some (C2, Y2) ⟹ A' ⊆ A ⟹ X ⊆ X' ⟹
        ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y ⟹
          ∃C2' Y2'. (U', False) ⊨ c2 (⊆ A', X') = Some (C2', Y2') ∧
            C2' ⊆ C2 ∧ Y2 ⊆ Y2'" and
    C: "(U, False) ⊨ c1 OR c2 (⊆ A, X) = Some (C, Y)" and
    D: "A' ⊆ A" and
    E: "X ⊆ X'" and
    F: "∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y"
  shows "∃C' Y'. (U', False) ⊨ c1 OR c2 (⊆ A', X') = Some (C', Y') ∧
    C' ⊆ C ∧ Y ⊆ Y'"
proof -
  obtain C1 C2 Y1 Y2 where
    G: "(C, Y) = (C1 ∪ C2, Y1 ∩ Y2) ∧
      Some (C1, Y1) = (U, False) ⊨ c1 (⊆ A, X) ∧
      Some (C2, Y2) = (U, False) ⊨ c2 (⊆ A, X)"
    using C by (simp split: option.split_asm prod.split_asm)
  moreover have H: "∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y"
    using F by simp
  ultimately have "∃C1' Y1'.
    (U', False) ⊨ c1 (⊆ A', X') = Some (C1', Y1') ∧ C1' ⊆ C1 ∧ Y1 ⊆ Y1'"
    using A and D and E by simp
  moreover have "∃C2' Y2'.
    (U', False) ⊨ c2 (⊆ A', X') = Some (C2', Y2') ∧ C2' ⊆ C2 ∧ Y2 ⊆ Y2'"
    using B and D and E and G and H by simp
  ultimately show ?thesis
    using G by auto
qed

lemma ctyping2_mono_if:
  assumes
    A: "⋀W p B1 B2 B1' C1 X' Y1 W'. (W, p) =
      (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹ (B1, B2) = p ⟹
        (W, False) ⊨ c1 (⊆ B1, X) = Some (C1, Y1) ⟹ B1' ⊆ B1 ⟹
          X ⊆ X' ⟹ ∀(B', Y') ∈ W'. ∃(B, Y) ∈ W. B' ⊆ B ∧ Y' ⊆ Y ⟹
            ∃C1' Y1'. (W', False) ⊨ c1 (⊆ B1', X') = Some (C1', Y1') ∧
              C1' ⊆ C1 ∧ Y1 ⊆ Y1'" and
    B: "⋀W p B1 B2 B2' C2 X' Y2 W'. (W, p) =
      (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹ (B1, B2) = p ⟹
        (W, False) ⊨ c2 (⊆ B2, X) = Some (C2, Y2) ⟹ B2' ⊆ B2 ⟹
          X ⊆ X' ⟹ ∀(B', Y') ∈ W'. ∃(B, Y) ∈ W. B' ⊆ B ∧ Y' ⊆ Y ⟹
            ∃C2' Y2'. (W', False) ⊨ c2 (⊆ B2', X') = Some (C2', Y2') ∧
              C2' ⊆ C2 ∧ Y2 ⊆ Y2'" and
    C: "(U, False) ⊨ IF b THEN c1 ELSE c2 (⊆ A, X) = Some (C, Y)" and
    D: "A' ⊆ A" and
    E: "X ⊆ X'" and
    F: "∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y"
  shows "∃C' Y'. (U', False) ⊨ IF b THEN c1 ELSE c2 (⊆ A', X') =
    Some (C', Y') ∧ C' ⊆ C ∧ Y ⊆ Y'"
proof -
  let ?W = "insert (Univ? A X, bvars b) U"
  let ?W' = "insert (Univ? A' X', bvars b) U'"
  obtain B1 B2 C1 C2 Y1 Y2 where
    G: "(C, Y) = (C1 ∪ C2, Y1 ∩ Y2) ∧ (B1, B2) = ⊨ b (⊆ A, X) ∧
      Some (C1, Y1) = (?W, False) ⊨ c1 (⊆ B1, X) ∧
      Some (C2, Y2) = (?W, False) ⊨ c2 (⊆ B2, X)"
    using C by (simp split: option.split_asm prod.split_asm)
  moreover obtain B1' B2' where H: "(B1', B2') = ⊨ b (⊆ A', X')"
    by (cases "⊨ b (⊆ A', X')", simp)
  ultimately have I: "B1' ⊆ B1 ∧ B2' ⊆ B2"
    by (metis btyping2_mono D E)
  moreover have J: "∀(B', Y') ∈ ?W'. ∃(B, Y) ∈ ?W. B' ⊆ B ∧ Y' ⊆ Y"
    using D and E and F by (auto simp: univ_states_if_def)
  ultimately have "∃C1' Y1'.
    (?W', False) ⊨ c1 (⊆ B1', X') = Some (C1', Y1') ∧ C1' ⊆ C1 ∧ Y1 ⊆ Y1'"
    using A and E and G by force
  moreover have "∃C2' Y2'.
    (?W', False) ⊨ c2 (⊆ B2', X') = Some (C2', Y2') ∧ C2' ⊆ C2 ∧ Y2 ⊆ Y2'"
    using B and E and G and I and J by force
  ultimately show ?thesis
    using G and H by (auto split: prod.split)
qed

lemma ctyping2_mono_while:
  assumes
    A: "⋀B1 B2 C Y B1' B2' D1 E X' V U'. (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹ (B1', B2') = ⊨ b (⊆ C, Y) ⟹
        ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
          B: W ↝ UNIV ⟹
          ({}, False) ⊨ c (⊆ B1, X) = Some (E, V) ⟹ D1 ⊆ B1 ⟹
            X ⊆ X' ⟹ ∀(B', Y') ∈ U'. ∃(B, Y) ∈ {}. B' ⊆ B ∧ Y' ⊆ Y ⟹
              ∃E' V'. (U', False) ⊨ c (⊆ D1, X') = Some (E', V') ∧
                E' ⊆ E ∧ V ⊆ V'" and
    B: "⋀B1 B2 C Y B1' B2' D1' F Y' W U'. (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹ (B1', B2') = ⊨ b (⊆ C, Y) ⟹
        ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
          B: W ↝ UNIV ⟹
          ({}, False) ⊨ c (⊆ B1', Y) = Some (F, W) ⟹ D1' ⊆ B1' ⟹
            Y ⊆ Y' ⟹ ∀(B', Y') ∈ U'. ∃(B, Y) ∈ {}. B' ⊆ B ∧ Y' ⊆ Y ⟹
              ∃F' W'. (U', False) ⊨ c (⊆ D1', Y') = Some (F', W') ∧
                F' ⊆ F ∧ W ⊆ W'" and
    C: "(U, False) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Z)" and
    D: "A' ⊆ A" and
    E: "X ⊆ X'" and
    F: "∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y"
  shows "∃B' Z'. (U', False) ⊨ WHILE b DO c (⊆ A', X') = Some (B', Z') ∧
    B' ⊆ B ∧ Z ⊆ Z'"
proof -
  obtain B1 B1' B2 B2' C E F V W Y where G: "(B1, B2) = ⊨ b (⊆ A, X) ∧
    (C, Y) = ⊢ c (⊆ B1, X) ∧ (B1', B2') = ⊨ b (⊆ C, Y) ∧
    (∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U. B: W ↝ UNIV) ∧
    Some (E, V) = ({}, False) ⊨ c (⊆ B1, X) ∧
    Some (F, W) = ({}, False) ⊨ c (⊆ B1', Y) ∧
    (B, Z) = (B2 ∪ B2', Univ?? B2 X ∩ Y)"
    using C by (force split: if_split_asm option.split_asm prod.split_asm)
  moreover obtain D1 D2 where H: "⊨ b (⊆ A', X') = (D1, D2)"
    by (cases "⊨ b (⊆ A', X')", simp)
  ultimately have I: "D1 ⊆ B1 ∧ D2 ⊆ B2"
    by (smt (verit) btyping2_mono D E)
  moreover obtain C' Y' where J: "⊢ c (⊆ D1, X') = (C', Y')"
    by (cases "⊢ c (⊆ D1, X')", simp)
  ultimately have K: "C' ⊆ C ∧ Y ⊆ Y'"
    by (smt (verit) ctyping1_mono E G)
  moreover obtain D1' D2' where L: "⊨ b (⊆ C', Y') = (D1', D2')"
    by (cases "⊨ b (⊆ C', Y')", simp)
  ultimately have M: "D1' ⊆ B1' ∧ D2' ⊆ B2'"
    by (smt (verit) btyping2_mono G)
  then obtain F' W' where
   "({}, False) ⊨ c (⊆ D1', Y') = Some (F', W') ∧ F' ⊆ F ∧ W ⊆ W'"
    using B and F and G and K by force
  moreover obtain E' V' where
   "({}, False) ⊨ c (⊆ D1, X') = Some (E', V') ∧ E' ⊆ E ∧ V ⊆ V'"
    using A and E and F and G and I by force
  moreover have "Univ? A' X' ⊆ Univ? A X"
    using D and E by (auto simp: univ_states_if_def)
  moreover have "Univ? C' Y' ⊆ Univ? C Y"
    using K by (auto simp: univ_states_if_def)
  ultimately have "(U', False) ⊨ WHILE b DO c (⊆ A', X') =
    Some (D2 ∪ D2', Univ?? D2 X' ∩ Y')"
    using F and G and H and J and L by force
  moreover have "D2 ∪ D2' ⊆ B"
    using G and I and M by auto
  moreover have "Z ⊆ Univ?? D2 X' ∩ Y'"
    using E and G and I and K by auto
  ultimately show ?thesis
    by simp
qed

lemma ctyping2_mono:
 "⟦(U, False) ⊨ c (⊆ A, X) = Some (C, Z); A' ⊆ A; X ⊆ X';
    ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y⟧ ⟹
  ∃C' Z'. (U', False) ⊨ c (⊆ A', X') = Some (C', Z') ∧ C' ⊆ C ∧ Z ⊆ Z'"
  apply (induction "(U, False)" c A X arbitrary: A' C X' Z U U'
   rule: ctyping2.induct)
         apply fastforce
        apply fastforce
       apply fastforce
      apply fastforce
     apply (erule ctyping2_mono_seq, assumption+)
    apply (erule ctyping2_mono_or, assumption+)
   apply (erule ctyping2_mono_if, assumption+)
  apply (erule ctyping2_mono_while, assumption+)
  done


lemma ctyping1_ctyping2_fst_assign [elim!]:
  assumes
    A: "⊢ x ::= a (⊆ A, X) = (C, Z)" and
    B: "(U, False) ⊨ x ::= a (⊆ A, X) = Some (C', Z')"
  shows "C' ⊆ C"
proof -
  let ?F = "λx' w. if x = x'
    then (x, w) # [y←[]. fst y = x']
    else [y←[]. fst y = x']"
  {
    fix s'
    assume "s' ∈ C'"
    moreover assume "x ∈ state" and C: "avars a = {}"
    ultimately obtain s where D: "s ∈ A" and E: "s' = s(x := aval a s)"
      using B by (auto split: if_split_asm)
    have "∃s.
      (∃t. s' = (λx'. if ?F x' (Some (aval a (λx. 0))) = []
        then s x'
        else case snd (last (?F x' (Some (aval a (λx. 0))))) of
          None ⇒ t x' | Some i ⇒ i)) ∧
      s ∈ A"
      apply (insert C E)
      apply (rule exI [of _ s])
      apply (rule conjI [OF _ D])
      apply (rule exI [of _ "λx. 0"])
      by (fastforce intro: avars_aval)
  }
  moreover {
    fix s'
    assume "s' ∈ C'"
    moreover assume "x ∈ state" and "avars a ≠ {}"
    ultimately obtain s where C: "s ∈ A" and D: "s' = s"
      using B by (simp split: if_split_asm)
    have "∃s.
      (∃t. s' = (λx'. if ?F x' None = []
        then s x'
        else case snd (last (?F x' None)) of
          None ⇒ t x' | Some i ⇒ i)) ∧
      s ∈ A"
      apply (insert D)
      apply (rule exI [of _ s])
      apply (rule conjI [OF _ C])
      apply (rule exI [of _ s])
      by auto
  }
  moreover {
    fix s'
    assume "s' ∈ C'" and "x ∉ state"
    hence "s' ∈ A"
      using B by (simp split: if_split_asm)
  }
  ultimately show ?thesis
    using A by (fastforce simp: ctyping1_def)
qed

lemma ctyping1_ctyping2_fst_input [elim!]:
  assumes
    A: "⊢ IN x (⊆ A, X) = (C, Z)" and
    B: "(U, False) ⊨ IN x (⊆ A, X) = Some (C', Z')"
  shows "C' ⊆ C"
proof -
  let ?F = "λx'. if x = x'
    then (x, None) # [y←[]. fst y = x']
    else [y←[]. fst y = x']"
  {
    fix s'
    assume "s' ∈ C'"
    moreover assume "x ∈ state"
    ultimately obtain s where C: "s ∈ A" and D: "s' = s"
      using B by (simp split: if_split_asm)
    have "∃s.
      (∃t. s' = (λx'. if ?F x' = []
        then s x'
        else case snd (last (?F x')) of
          None ⇒ t x' | Some i ⇒ i)) ∧
      s ∈ A"
      apply (insert D)
      apply (rule exI [of _ s])
      apply (rule conjI [OF _ C])
      apply (rule exI [of _ s])
      by auto
  }
  moreover {
    fix s'
    assume "s' ∈ C'" and "x ∉ state"
    hence "s' ∈ A"
      using B by (simp split: if_split_asm)
  }
  ultimately show ?thesis
    using A by (fastforce simp: ctyping1_def)
qed

lemma ctyping1_ctyping2_fst_output [elim!]:
 "⟦⊢ OUT x (⊆ A, X) = (C, Z);
    (U, False) ⊨ OUT x (⊆ A, X) = Some (C', Z')⟧ ⟹
  C' ⊆ C"
by (simp add: ctyping1_def split: if_split_asm)

lemma ctyping1_ctyping2_fst_seq:
  assumes
    A: "⊢ c1;; c2 (⊆ A, X) = (C, Z)" and
    B: "(U, False) ⊨ c1;; c2 (⊆ A, X) = Some (C', Z')" and
    C: "⋀B B' Y Y'. ⊢ c1 (⊆ A, X) = (B, Y) ⟹
      (U, False) ⊨ c1 (⊆ A, X) = Some (B', Y') ⟹ B' ⊆ B" and
    D: "⋀p B' Y' D' C' W' Z'.
      (U, False) ⊨ c1 (⊆ A, X) = Some p ⟹ (B', Y') = p ⟹
        ⊢ c2 (⊆ B', Y') = (D', W') ⟹
          (U, False) ⊨ c2 (⊆ B', Y') = Some (C', Z') ⟹ C' ⊆ D'"
  shows "C' ⊆ C"
proof -
  obtain B' Y' where E: "(U, False) ⊨ c1 (⊆ A, X) = Some (B', Y')" and
   "(U, False) ⊨ c2 (⊆ B', Y') = Some (C', Z')"
    using B by (auto split: option.split_asm)
  moreover obtain D' W' where F: "⊢ c2 (⊆ B', Y') = (D', W')"
    by (cases "⊢ c2 (⊆ B', Y')", simp)
  ultimately have G: "C' ⊆ D'"
    using D by simp
  obtain B Y where H: "⊢ c1 (⊆ A, X) = (B, Y)"
    by (cases "⊢ c1 (⊆ A, X)", simp)
  hence "B' ⊆ B"
    using C and E by simp
  moreover obtain D W where I: "⊢ c2 (⊆ B, Y) = (D, W)"
    by (cases "⊢ c2 (⊆ B, Y)", simp)
  ultimately have "D' ⊆ D"
    using F by (blast dest: ctyping1_mono_fst)
  moreover {
    fix ys ys' s t and t' :: state
    assume K: "s ∈ A"
    assume "ys ∈ ⊢ c1" and "ys' ∈ ⊢ c2"
    hence L: "ys @ ys' ∈ ⊢ c1 ⊔@ ⊢ c2"
      by (force simp: ctyping1_merge_append_def
       ctyping1_append_def ctyping1_merge_def)
    let ?f = "λx. [y←ys @ ys'. fst y = x]"
    let ?t = "λx. if [y←ys'. fst y = x] = [] then t x else t' x"
    have "∃f s'.
      (∃t''.
        (λx. if [y←ys'. fst y = x] = []
          then if [y←ys. fst y = x] = []
            then s x
            else case snd (last [y←ys. fst y = x]) of
              None ⇒ t x | Some i ⇒ i
          else case snd (last [y←ys'. fst y = x]) of
            None ⇒ t' x | Some i ⇒ i) =
        (λx. if f x = []
          then s' x
          else case snd (last (f x)) of None ⇒ t'' x | Some i ⇒ i)) ∧
      (∃ys''. f = (λx. [y←ys''. fst y = x]) ∧ ys'' ∈ ⊢ c1 ⊔@ ⊢ c2) ∧ s' ∈ A"
      apply (insert K L)
      apply (rule exI [of _ ?f])
      apply (rule exI [of _ s])
      apply (rule conjI)
       apply (rule exI [of _ ?t])
       apply fastforce
      apply (rule conjI)
       apply (rule exI [of _ "ys @ ys'"])
      by simp_all
  }
  hence "D ⊆ C"
    using A and H and I by (auto simp: ctyping1_def)
  ultimately show ?thesis
    using G by simp
qed

lemma ctyping1_ctyping2_fst_or:
  assumes
    A: "⊢ c1 OR c2 (⊆ A, X) = (C, Y)" and
    B: "(U, False) ⊨ c1 OR c2 (⊆ A, X) = Some (C', Y')" and
    C: "⋀C C' Y Y'. ⊢ c1 (⊆ A, X) = (C, Y) ⟹
      (U, False) ⊨ c1 (⊆ A, X) = Some (C', Y') ⟹ C' ⊆ C" and
    D: "⋀C C' Y Y'. ⊢ c2 (⊆ A, X) = (C, Y) ⟹
      (U, False) ⊨ c2 (⊆ A, X) = Some (C', Y') ⟹ C' ⊆ C"
  shows "C' ⊆ C"
proof -
  obtain C1' C2' Y1' Y2' where
    E: "(C', Y') = (C1' ∪ C2', Y1' ∩ Y2')" and
    F: "(U, False) ⊨ c1 (⊆ A, X) = Some (C1', Y1')" and
    G: "(U, False) ⊨ c2 (⊆ A, X) = Some (C2', Y2')"
    using B by (auto split: option.split_asm prod.split_asm)
  obtain C1 Y1 where H: "⊢ c1 (⊆ A, X) = (C1, Y1)"
    by (cases "⊢ c1 (⊆ A, X)", simp)
  hence "C1' ⊆ C1"
    using C and F by simp
  moreover obtain C2 Y2 where I: "⊢ c2 (⊆ A, X) = (C2, Y2)"
    by (cases "⊢ c2 (⊆ A, X)", simp)
  hence "C2' ⊆ C2"
    using D and G by simp
  ultimately have "C' ⊆ C1 ∪ C2"
    using E by blast
  moreover {
    fix ys s t
    assume "s ∈ A"
    moreover assume "ys ∈ ⊢ c1"
    hence "ys ∈ ⊢ c1 ⊔ ⊢ c2"
      by (force simp: ctyping1_merge_def)
    ultimately have "∃f s'.
      (∃t'.
        (λx. if [y←ys. fst y = x] = []
          then s x
          else case snd (last [y←ys. fst y = x]) of
            None ⇒ t x | Some i ⇒ i) =
        (λx. if f x = []
          then s' x
          else case snd (last (f x)) of None ⇒ t' x | Some i ⇒ i)) ∧
      (∃ys'. f = (λx. [y←ys'. fst y = x]) ∧ ys' ∈ ⊢ c1 ⊔ ⊢ c2) ∧ s' ∈ A"
      by fastforce
  }
  hence "C1 ⊆ C"
    using A and H by (auto simp: ctyping1_def)
  moreover {
    fix ys s t
    assume "s ∈ A"
    moreover assume "ys ∈ ⊢ c2"
    hence "ys ∈ ⊢ c1 ⊔ ⊢ c2"
      by (force simp: ctyping1_merge_def)
    ultimately have "∃f s'.
      (∃t'.
        (λx. if [y←ys. fst y = x] = []
          then s x
          else case snd (last [y←ys. fst y = x]) of
            None ⇒ t x | Some i ⇒ i) =
        (λx. if f x = []
          then s' x
          else case snd (last (f x)) of None ⇒ t' x | Some i ⇒ i)) ∧
      (∃ys'. f = (λx. [y←ys'. fst y = x]) ∧ ys' ∈ ⊢ c1 ⊔ ⊢ c2) ∧ s' ∈ A"
      by fastforce
  }
  hence "C2 ⊆ C"
    using A and I by (auto simp: ctyping1_def)
  ultimately show ?thesis
    by blast
qed

lemma ctyping1_ctyping2_fst_if:
  assumes
    A: "⊢ IF b THEN c1 ELSE c2 (⊆ A, X) = (C, Y)" and
    B: "(U, False) ⊨ IF b THEN c1 ELSE c2 (⊆ A, X) = Some (C', Y')" and
    C: "⋀U' p B1 B2 C C' Y Y'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B1, B2) = p ⟹ ⊢ c1 (⊆ B1, X) = (C, Y) ⟹
          (U', False) ⊨ c1 (⊆ B1, X) = Some (C', Y') ⟹ C' ⊆ C" and
    D: "⋀U' p B1 B2 C C' Y Y'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B1, B2) = p ⟹ ⊢ c2 (⊆ B2, X) = (C, Y) ⟹
          (U', False) ⊨ c2 (⊆ B2, X) = Some (C', Y') ⟹ C' ⊆ C"
  shows "C' ⊆ C"
proof -
  let ?U' = "insert (Univ? A X, bvars b) U"
  obtain B1 B2 C1' C2' Y1' Y2' where
    E: "(C', Y') = (C1' ∪ C2', Y1' ∩ Y2')" and
    F: "⊨ b (⊆ A, X) = (B1, B2)" and
    G: "(?U', False) ⊨ c1 (⊆ B1, X) = Some (C1', Y1')" and
    H: "(?U', False) ⊨ c2 (⊆ B2, X) = Some (C2', Y2')"
    using B by (auto split: option.split_asm prod.split_asm)
  obtain C1 Y1 where I: "⊢ c1 (⊆ B1, X) = (C1, Y1)"
    by (cases "⊢ c1 (⊆ B1, X)", simp)
  hence "C1' ⊆ C1"
    using C and F and G by simp
  moreover obtain C2 Y2 where J: "⊢ c2 (⊆ B2, X) = (C2, Y2)"
    by (cases "⊢ c2 (⊆ B2, X)", simp)
  hence "C2' ⊆ C2"
    using D and F and H by simp
  ultimately have K: "C' ⊆ C1 ∪ C2"
    using E by blast
  {
    fix ys s t
    assume "s ∈ B1"
    hence "s ∈ A"
      using F by (blast dest: btyping2_un_eq)
    moreover assume "ys ∈ ⊢ c1"
    hence "ys ∈ ⊢ c1 ⊔ ⊢ c2"
      by (force simp: ctyping1_merge_def)
    ultimately have "∃f s'.
      (∃t'.
        (λx. if [y←ys. fst y = x] = []
          then s x
          else case snd (last [y←ys. fst y = x]) of
            None ⇒ t x | Some i ⇒ i) =
        (λx. if f x = []
          then s' x
          else case snd (last (f x)) of None ⇒ t' x | Some i ⇒ i)) ∧
      (∃ys'. f = (λx. [y←ys'. fst y = x]) ∧ ys' ∈ ⊢ c1 ⊔ ⊢ c2) ∧ s' ∈ A"
      by fastforce
  }
  moreover {
    fix ys s t
    assume "s ∈ B1"
    moreover assume "ys ∈ ⊢ c1"
    hence "ys ∈ ⊢ c1 ⊔ {}"
      by (force simp: ctyping1_merge_def)
    ultimately have "∃f s'.
      (∃t'.
        (λx. if [y←ys. fst y = x] = []
          then s x
          else case snd (last [y←ys. fst y = x]) of
            None ⇒ t x | Some i ⇒ i) =
        (λx. if f x = []
          then s' x
          else case snd (last (f x)) of None ⇒ t' x | Some i ⇒ i)) ∧
      (∃ys'. f = (λx. [y←ys'. fst y = x]) ∧ ys' ∈ ⊢ c1 ⊔ {}) ∧ s' ∈ B1"
      by fastforce
  }
  ultimately have L: "C1 ⊆ C"
    using A and F and I by (cases "⊢ b", auto
     dest!: btyping1_btyping2 [of _ _ A X] simp: ctyping1_def)
  {
    fix ys s t
    assume "s ∈ B2"
    hence "s ∈ A"
      using F by (blast dest: btyping2_un_eq)
    moreover assume "ys ∈ ⊢ c2"
    hence "ys ∈ ⊢ c1 ⊔ ⊢ c2"
      by (force simp: ctyping1_merge_def)
    ultimately have "∃f s'.
      (∃t'.
        (λx. if [y←ys. fst y = x] = []
          then s x
          else case snd (last [y←ys. fst y = x]) of
            None ⇒ t x | Some i ⇒ i) =
        (λx. if f x = []
          then s' x
          else case snd (last (f x)) of None ⇒ t' x | Some i ⇒ i)) ∧
      (∃ys'. f = (λx. [y←ys'. fst y = x]) ∧ ys' ∈ ⊢ c1 ⊔ ⊢ c2) ∧ s' ∈ A"
      by fastforce
  }
  moreover {
    fix ys s t
    assume "s ∈ B2"
    moreover assume "ys ∈ ⊢ c2"
    hence "ys ∈ {} ⊔ ⊢ c2"
      by (force simp: ctyping1_merge_def)
    ultimately have "∃f s'.
      (∃t'.
        (λx. if [y←ys. fst y = x] = []
          then s x
          else case snd (last [y←ys. fst y = x]) of
            None ⇒ t x | Some i ⇒ i) =
        (λx. if f x = []
          then s' x
          else case snd (last (f x)) of None ⇒ t' x | Some i ⇒ i)) ∧
      (∃ys'. f = (λx. [y←ys'. fst y = x]) ∧ ys' ∈ {} ⊔ ⊢ c2) ∧ s' ∈ B2"
      by fastforce
  }
  ultimately have "C2 ⊆ C"
    using A and F and J by (cases "⊢ b", auto
     dest!: btyping1_btyping2 [of _ _ A X] simp: ctyping1_def)
  with K and L show ?thesis
    by blast
qed

lemma ctyping1_ctyping2_fst_while:
  assumes
    A: "⊢ WHILE b DO c (⊆ A, X) = (B, Z)" and
    B: "(U, False) ⊨ WHILE b DO c (⊆ A, X) = Some (B', Z')"
  shows "B' ⊆ B"
proof -
  obtain B1 B1' B2 B2' C Y where
    C: "⊨ b (⊆ A, X) = (B1, B2)" and
    D: "⊢ c (⊆ B1, X) = (C, Y)" and
    E: "⊨ b (⊆ C, Y) = (B1', B2')" and
    F: "(B', Z') = (B2 ∪ B2', Univ?? B2 X ∩ Y)"
    using B by (force split: if_split_asm option.split_asm prod.split_asm)
  {
    fix s
    assume "s ∈ B2"
    hence "s ∈ A"
      using C by (blast dest: btyping2_un_eq)
    hence "∃f s'.
      (∃t. s = (λx. if f x = []
        then s' x
        else case snd (last (f x)) of None ⇒ t x | Some i ⇒ i)) ∧
      (∃ys. f = (λx. [y←ys. fst y = x]) ∧ (ys = [] ∨ ys ∈ ⊢ c)) ∧ s' ∈ A"
      by force
  }
  with A and C have G: "B2 ⊆ B"
    by (cases "⊢ b", auto dest!: btyping1_btyping2 [of _ _ A X]
     simp: ctyping1_def)
  {
    fix s
    assume "s ∈ B2'"
    hence "s ∈ C"
      using E by (blast dest: btyping2_un_eq)
    then obtain f s' where H:
     "(∃t. s = (λx. if f x = []
        then s' x
        else case snd (last (f x)) of None ⇒ t x | Some i ⇒ i)) ∧
      (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c) ∧ s' ∈ B1"
      using D by (fastforce simp: ctyping1_def)
    hence I: "s' ∈ A"
      using C by (blast dest: btyping2_un_eq)
    have "∃f s'.
      (∃t. s = (λx. if f x = []
        then s' x
        else case snd (last (f x)) of None ⇒ t x | Some i ⇒ i)) ∧
      (∃ys. f = (λx. [y←ys. fst y = x]) ∧ (ys = [] ∨ ys ∈ ⊢ c)) ∧ s' ∈ A"
      by (rule exI [of _ f], insert H I, auto)
  }
  moreover {
    fix s
    assume "s ∈ B2'"
    moreover assume "⊢ b = Some True"
    ultimately have "∃f s'.
      (∃t. s = (λx. if f x = []
        then s' x
        else case snd (last (f x)) of None ⇒ t x | Some i ⇒ i)) ∧
      (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c) ∧ s' ∈ A"
      using E by (auto dest: btyping1_btyping2 [of _ _ C Y])
  }
  moreover {
    fix s
    assume "s ∈ B2'"
    hence "C ≠ {}"
      using E by (blast dest: btyping2_un_eq) 
    hence "B1 ≠ {}"
      using D by (auto simp: ctyping1_def)
    moreover assume "⊢ b = Some False"
    ultimately have "s ∈ A"
      using C by (auto dest: btyping1_btyping2 [of _ _ A X])
  }
  ultimately have "B2' ⊆ B"
    using A by (cases "⊢ b", auto simp: ctyping1_def)
  with F and G show ?thesis
    by simp
qed

lemma ctyping1_ctyping2_fst:
 "⟦⊢ c (⊆ A, X) = (C, Z); (U, False) ⊨ c (⊆ A, X) = Some (C', Z')⟧ ⟹
    C' ⊆ C"
  apply (induction "(U, False)" c A X arbitrary: C C' Z Z' U
   rule: ctyping2.induct)
         apply (fastforce simp: ctyping1_def)
        apply fastforce
       apply fastforce
      apply fastforce
     apply (erule ctyping1_ctyping2_fst_seq, assumption+)
    apply (erule ctyping1_ctyping2_fst_or, assumption+)
   apply (erule ctyping1_ctyping2_fst_if, assumption+)
  apply (erule ctyping1_ctyping2_fst_while, assumption+)
  done


lemma ctyping1_ctyping2_snd_skip [elim!]:
 "⟦⊢ SKIP (⊆ A, X) = (C, Z);
    (U, False) ⊨ SKIP (⊆ A, X) = Some (C', Z')⟧ ⟹
  Z ⊆ Z'"
by (simp add: ctyping1_def split: if_split_asm)

lemma ctyping1_ctyping2_snd_assign [elim!]:
 "⟦⊢ x ::= a (⊆ A, X) = (C, Z);
    (U, False) ⊨ x ::= a (⊆ A, X) = Some (C', Z')⟧ ⟹
  Z ⊆ Z'"
by (auto simp: ctyping1_def split: if_split_asm)

lemma ctyping1_ctyping2_snd_input [elim!]:
 "⟦⊢ IN x (⊆ A, X) = (C, Z);
    (U, False) ⊨ IN x (⊆ A, X) = Some (C', Z')⟧ ⟹
  Z ⊆ Z'"
by (auto simp: ctyping1_def split: if_split_asm)

lemma ctyping1_ctyping2_snd_output [elim!]:
 "⟦⊢ OUT x (⊆ A, X) = (C, Z);
    (U, False) ⊨ OUT x (⊆ A, X) = Some (C', Z')⟧ ⟹
  Z ⊆ Z'"
by (simp add: ctyping1_def split: if_split_asm)

lemma ctyping1_ctyping2_snd_seq:
  assumes
    A: "⊢ c1;; c2 (⊆ A, X) = (C, Z)" and
    B: "(U, False) ⊨ c1;; c2 (⊆ A, X) = Some (C', Z')" and
    C: "⋀B B' Y Y'. ⊢ c1 (⊆ A, X) = (B, Y) ⟹
      (U, False) ⊨ c1 (⊆ A, X) = Some (B', Y') ⟹ Y ⊆ Y'" and
    D: "⋀p B' Y' D' C' W' Z'.
      (U, False) ⊨ c1 (⊆ A, X) = Some p ⟹ (B', Y') = p ⟹
        ⊢ c2 (⊆ B', Y') = (D', W') ⟹
          (U, False) ⊨ c2 (⊆ B', Y') = Some (C', Z') ⟹ W' ⊆ Z'"
  shows "Z ⊆ Z'"
proof -
  obtain B' Y' where E: "(U, False) ⊨ c1 (⊆ A, X) = Some (B', Y')" and
   "(U, False) ⊨ c2 (⊆ B', Y') = Some (C', Z')"
    using B by (auto split: option.split_asm)
  moreover obtain D' W' where F: "⊢ c2 (⊆ B', Y') = (D', W')"
    by (cases "⊢ c2 (⊆ B', Y')", simp)
  ultimately have G: "W' ⊆ Z'"
    using D by simp
  obtain B Y where H: "⊢ c1 (⊆ A, X) = (B, Y)"
    by (cases "⊢ c1 (⊆ A, X)", simp)
  hence "Y ⊆ Y'"
    using C and E by simp
  moreover have "B' ⊆ B"
    using H and E by (rule ctyping1_ctyping2_fst)
  moreover obtain D W where I: "⊢ c2 (⊆ B, Y) = (D, W)"
    by (cases "⊢ c2 (⊆ B, Y)", simp)
  ultimately have "W ⊆ W'"
    using F by (blast dest: ctyping1_mono)
  moreover {
    fix x
    assume J: "∀f. (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c1 ⊔@ ⊢ c2) ⟶
      (if f x = [] then x ∈ X else snd (last (f x)) ≠ None)"
    {
      fix ys' ys
      assume "ys ∈ ⊢ c1" and "ys' ∈ ⊢ c2"
      hence "ys @ ys' ∈ ⊢ c1 ⊔@ ⊢ c2"
        by (force simp: ctyping1_merge_append_def
         ctyping1_append_def ctyping1_merge_def)
      moreover assume "[y←ys. fst y = x] = []" and "[y←ys'. fst y = x] = []"
      ultimately have "x ∈ X"
        using J by auto
    }
    moreover {
      fix ys ys'
      assume "ys ∈ ⊢ c1" and "ys' ∈ ⊢ c2"
      hence "ys @ ys' ∈ ⊢ c1 ⊔@ ⊢ c2"
        by (force simp: ctyping1_merge_append_def
         ctyping1_append_def ctyping1_merge_def)
      moreover assume "[y←ys. fst y = x] ≠ []" and "[y←ys'. fst y = x] = []"
      ultimately have "∃i. snd (last [y←ys. fst y = x]) = Some i"
        using J by auto
    }
    moreover {
      fix ys'
      assume "ys' ∈ ⊢ c2"
      moreover obtain ys where "ys ∈ ⊢ c1"
        by (insert ctyping1_aux_nonempty, blast)
      ultimately have "ys @ ys' ∈ ⊢ c1 ⊔@ ⊢ c2"
        by (force simp: ctyping1_merge_append_def
         ctyping1_append_def ctyping1_merge_def)
      moreover assume "[y←ys'. fst y = x] ≠ []"
      ultimately have "∃i. snd (last [y←ys'. fst y = x]) = Some i"
        using J by auto
    }
    ultimately have "x ∈ {x. ∀f ∈ {λx. [y←ys. fst y = x] | ys. ys ∈ ⊢ c2}.
      if f x = []
      then x ∈ {x. ∀f. (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c1) ⟶
        (if f x = [] then x ∈ X else snd (last (f x)) ≠ None)}
      else snd (last (f x)) ≠ None}"
      (is "_ ∈ ?X")
      by auto
    moreover assume "x ∉ (if ∀x f s.
      (∀t. x ≠ (λx. if f x = [] then s x else case snd (last (f x)) of
        None ⇒ t x | Some i ⇒ i)) ∨
      (∀ys. f = (λx. [y←ys. fst y = x]) ⟶ ys ∉ ⊢ c1) ∨ s ∉ A
        then UNIV else ?X)"
    hence "x ∉ ?X"
      by (auto split: if_split_asm)
    ultimately have False
      by contradiction
  }
  hence "Z ⊆ W"
    using A and H and I by (cases "A = {}", auto simp: ctyping1_def)
  ultimately show ?thesis
    using G by simp
qed

lemma ctyping1_ctyping2_snd_or:
  assumes
    A: "⊢ c1 OR c2 (⊆ A, X) = (C, Y)" and
    B: "(U, False) ⊨ c1 OR c2 (⊆ A, X) = Some (C', Y')" and
    C: "⋀C C' Y Y'. ⊢ c1 (⊆ A, X) = (C, Y) ⟹
      (U, False) ⊨ c1 (⊆ A, X) = Some (C', Y') ⟹ Y ⊆ Y'" and
    D: "⋀C C' Y Y'. ⊢ c2 (⊆ A, X) = (C, Y) ⟹
      (U, False) ⊨ c2 (⊆ A, X) = Some (C', Y') ⟹ Y ⊆ Y'"
  shows "Y ⊆ Y'"
proof -
  obtain C1' C2' Y1' Y2' where
    E: "(C', Y') = (C1' ∪ C2', Y1' ∩ Y2')" and
    F: "(U, False) ⊨ c1 (⊆ A, X) = Some (C1', Y1')" and
    G: "(U, False) ⊨ c2 (⊆ A, X) = Some (C2', Y2')"
    using B by (auto split: option.split_asm prod.split_asm)
  obtain C1 Y1 where H: "⊢ c1 (⊆ A, X) = (C1, Y1)"
    by (cases "⊢ c1 (⊆ A, X)", simp)
  hence "Y1 ⊆ Y1'"
    using C and F by simp
  moreover obtain C2 Y2 where I: "⊢ c2 (⊆ A, X) = (C2, Y2)"
    by (cases "⊢ c2 (⊆ A, X)", simp)
  hence "Y2 ⊆ Y2'"
    using D and G by simp
  ultimately have "Y1 ∩ Y2 ⊆ Y'"
    using E by blast
  moreover {
    fix x ys
    assume "∀f. (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c1 ⊔ ⊢ c2) ⟶
      (if f x = [] then x ∈ X else snd (last (f x)) ≠ None)"
    moreover assume "ys ∈ ⊢ c1"
    hence "ys ∈ ⊢ c1 ⊔ ⊢ c2"
      by (force simp: ctyping1_merge_def)
    ultimately have "if [y←ys. fst y = x] = []
      then x ∈ X else snd (last [y←ys. fst y = x]) ≠ None"
      (is ?P)
      by blast
    moreover assume "¬ ?P"
    ultimately have False
      by contradiction
  }
  hence "Y ⊆ Y1"
    using A and H by (cases "A = {}", auto simp: ctyping1_def)
  moreover {
    fix x ys
    assume "∀f. (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c1 ⊔ ⊢ c2) ⟶
      (if f x = [] then x ∈ X else snd (last (f x)) ≠ None)"
    moreover assume "ys ∈ ⊢ c2"
    hence "ys ∈ ⊢ c1 ⊔ ⊢ c2"
      by (force simp: ctyping1_merge_def)
    ultimately have "if [y←ys. fst y = x] = []
      then x ∈ X else snd (last [y←ys. fst y = x]) ≠ None"
      (is ?P)
      by blast
    moreover assume "¬ ?P"
    ultimately have False
      by contradiction
  }
  hence "Y ⊆ Y2"
    using A and I by (cases "A = {}", auto simp: ctyping1_def)
  ultimately show ?thesis
    by blast
qed

lemma ctyping1_ctyping2_snd_if:
  assumes
    A: "⊢ IF b THEN c1 ELSE c2 (⊆ A, X) = (C, Y)" and
    B: "(U, False) ⊨ IF b THEN c1 ELSE c2 (⊆ A, X) = Some (C', Y')" and
    C: "⋀U' p B1 B2 C C' Y Y'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B1, B2) = p ⟹ ⊢ c1 (⊆ B1, X) = (C, Y) ⟹
          (U', False) ⊨ c1 (⊆ B1, X) = Some (C', Y') ⟹ Y ⊆ Y'" and
    D: "⋀U' p B1 B2 C C' Y Y'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B1, B2) = p ⟹ ⊢ c2 (⊆ B2, X) = (C, Y) ⟹
          (U', False) ⊨ c2 (⊆ B2, X) = Some (C', Y') ⟹ Y ⊆ Y'"
  shows "Y ⊆ Y'"
proof -
  let ?U' = "insert (Univ? A X, bvars b) U"
  obtain B1 B2 C1' C2' Y1' Y2' where
    E: "(C', Y') = (C1' ∪ C2', Y1' ∩ Y2')" and
    F: "⊨ b (⊆ A, X) = (B1, B2)" and
    G: "(?U', False) ⊨ c1 (⊆ B1, X) = Some (C1', Y1')" and
    H: "(?U', False) ⊨ c2 (⊆ B2, X) = Some (C2', Y2')"
    using B by (auto split: option.split_asm prod.split_asm)
  obtain C1 Y1 where I: "⊢ c1 (⊆ B1, X) = (C1, Y1)"
    by (cases "⊢ c1 (⊆ B1, X)", simp)
  hence "Y1 ⊆ Y1'"
    using C and F and G by simp
  moreover obtain C2 Y2 where J: "⊢ c2 (⊆ B2, X) = (C2, Y2)"
    by (cases "⊢ c2 (⊆ B2, X)", simp)
  hence "Y2 ⊆ Y2'"
    using D and F and H by simp
  ultimately have "Y1 ∩ Y2 ⊆ Y'"
    using E by blast
  moreover have K: "B1 ∪ B2 = A"
    using F by (rule btyping2_un_eq)
  {
    fix x x' ys
    assume "x ∈ (if B1 = {} ∧ B2 = {} then UNIV else
      {x. ∀f ∈ {λx. [y←ys. fst y = x] | ys. ys ∈ ⊢ c1 ⊔ ⊢ c2}.
        if f x = [] then x ∈ X else snd (last (f x)) ≠ None})" and
     "x' ∈ B1"
    hence "∀f. (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c1 ⊔ ⊢ c2) ⟶
      (if f x = [] then x ∈ X else snd (last (f x)) ≠ None)"
      by (auto split: if_split_asm)
    moreover assume "ys ∈ ⊢ c1"
    hence "ys ∈ ⊢ c1 ⊔ ⊢ c2"
      by (force simp: ctyping1_merge_def)
    ultimately have "if [y←ys. fst y = x] = []
      then x ∈ X else snd (last [y←ys. fst y = x]) ≠ None"
      (is ?P)
      by blast
    moreover assume "¬ ?P"
    ultimately have False
      by contradiction
  }
  note L = this
  {
    fix x x' ys v
    assume "x ∈ (if B1 = {} ∧ B2 = {} then UNIV else
      {x. ∀f ∈ {λx. [y←ys. fst y = x] | ys.
        ys ∈ (if v then ⊢ c1 else {}) ⊔ (if ¬ v then ⊢ c2 else {})}.
          if f x = [] then x ∈ X else snd (last (f x)) ≠ None})"
    moreover assume M: "x' ∈ B1" and
     "(if v then (B1 ∪ B2, {}) else ({}, B1 ∪ B2)) = (B1, B2)"
    hence v
      by (simp split: if_split_asm)
    ultimately have
     "∀f. (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c1 ⊔ {}) ⟶
        (if f x = [] then x ∈ X else snd (last (f x)) ≠ None)"
      using M by (auto split: if_split_asm)
    moreover assume "ys ∈ ⊢ c1"
    hence "ys ∈ ⊢ c1 ⊔ {}"
      by (force simp: ctyping1_merge_def)
    ultimately have "if [y←ys. fst y = x] = []
      then x ∈ X else snd (last [y←ys. fst y = x]) ≠ None"
      (is ?P)
      by blast
    moreover assume "¬ ?P"
    ultimately have False
      by contradiction
  }
  note M = this
  from A and F and I and K have "Y ⊆ Y1"
    apply (cases "B1 = {}")
     apply (fastforce simp: ctyping1_def)
    apply (cases "⊢ b")
    by (auto dest!: btyping1_btyping2 [of _ _ A X] L M simp: ctyping1_def)
  moreover {
    fix x x' ys
    assume "x ∈ (if B1 = {} ∧ B2 = {} then UNIV else
      {x. ∀f ∈ {λx. [y←ys. fst y = x] | ys. ys ∈ ⊢ c1 ⊔ ⊢ c2}.
        if f x = [] then x ∈ X else snd (last (f x)) ≠ None})" and
     "x' ∈ B2"
    hence "∀f. (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c1 ⊔ ⊢ c2) ⟶
      (if f x = [] then x ∈ X else snd (last (f x)) ≠ None)"
      by (auto split: if_split_asm)
    moreover assume "ys ∈ ⊢ c2"
    hence "ys ∈ ⊢ c1 ⊔ ⊢ c2"
      by (force simp: ctyping1_merge_def)
    ultimately have "if [y←ys. fst y = x] = []
      then x ∈ X else snd (last [y←ys. fst y = x]) ≠ None"
      (is ?P)
      by blast
    moreover assume "¬ ?P"
    ultimately have False
      by contradiction
  }
  note N = this
  {
    fix x x' ys v
    assume "x ∈ (if B1 = {} ∧ B2 = {} then UNIV else
      {x. ∀f ∈ {λx. [y←ys. fst y = x] | ys.
        ys ∈ (if v then ⊢ c1 else {}) ⊔ (if ¬ v then ⊢ c2 else {})}.
          if f x = [] then x ∈ X else snd (last (f x)) ≠ None})"
    moreover assume O: "x' ∈ B2" and
     "(if v then (B1 ∪ B2, {}) else ({}, B1 ∪ B2)) = (B1, B2)"
    hence "¬ v"
      by (simp split: if_split_asm)
    ultimately have
     "∀f. (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ {} ⊔ ⊢ c2) ⟶
        (if f x = [] then x ∈ X else snd (last (f x)) ≠ None)"
      using O by (auto split: if_split_asm)
    moreover assume "ys ∈ ⊢ c2"
    hence "ys ∈ {} ⊔ ⊢ c2"
      by (force simp: ctyping1_merge_def)
    ultimately have "if [y←ys. fst y = x] = []
      then x ∈ X else snd (last [y←ys. fst y = x]) ≠ None"
      (is ?P)
      by blast
    moreover assume "¬ ?P"
    ultimately have False
      by contradiction
  }
  note O = this
  from A and F and J and K have "Y ⊆ Y2"
    apply (cases "B2 = {}")
     apply (fastforce simp: ctyping1_def)
    apply (cases "⊢ b")
    by (auto dest!: btyping1_btyping2 [of _ _ A X] N O simp: ctyping1_def)
  ultimately show ?thesis
    by blast
qed

lemma ctyping1_ctyping2_snd_while:
  assumes
    A: "⊢ WHILE b DO c (⊆ A, X) = (B, Z)" and
    B: "(U, False) ⊨ WHILE b DO c (⊆ A, X) = Some (B', Z')"
  shows "Z ⊆ Z'"
proof -
  obtain B1 B1' B2 B2' C Y where
    C: "⊨ b (⊆ A, X) = (B1, B2)" and
    D: "⊢ c (⊆ B1, X) = (C, Y)" and
    E: "⊨ b (⊆ C, Y) = (B1', B2')" and
    F: "(B', Z') = (B2 ∪ B2', Univ?? B2 X ∩ Y)"
    using B by (force split: if_split_asm option.split_asm prod.split_asm)
  have G: "B1 ∪ B2 = A"
    using C by (rule btyping2_un_eq)
  {
    fix x x'
    assume "x ∈ (if B1 = {} ∧ B2 = {} then UNIV else
      {x. ∀f ∈ {λx. [y←ys. fst y = x] | ys. ys = [] ∨ ys ∈ ⊢ c}.
        if f x = [] then x ∈ X else snd (last (f x)) ≠ None})" and
     "x' ∈ B2"
    hence "∀f ∈ {λx. [y←ys. fst y = x] | ys. ys = [] ∨ ys ∈ ⊢ c}.
      (if f x = [] then x ∈ X else snd (last (f x)) ≠ None)"
      by (auto split: if_split_asm)
    hence "x ∈ X"
      by fastforce
    moreover assume "x ∉ X"
    ultimately have False
      by contradiction
  }
  note H = this
  {
    fix x x' v
    assume "x ∈ (if B1 = {} ∧ B2 = {} then UNIV else
      {x. ∀f ∈ {λx. [y←ys. fst y = x] | ys.
        ys ∈ (if ¬ v then {[]} else {}) ∨ ys ∈ (if v then ⊢ c else {})}.
          if f x = [] then x ∈ X else snd (last (f x)) ≠ None})"
    moreover assume H: "x' ∈ B2" and
     "(if v then (B1 ∪ B2, {}) else ({}, B1 ∪ B2)) = (B1, B2)"
    hence "¬ v"
      by (simp split: if_split_asm)
    ultimately have "x ∈ X"
      using H by (auto split: if_split_asm)
    moreover assume "x ∉ X"
    ultimately have False
      by contradiction
  }
  note I = this
  from A and C and G have "Z ⊆ Univ?? B2 X"
    apply (cases "B2 = {}")
     apply fastforce
    apply (cases "⊢ b")
    by (auto dest!: btyping1_btyping2 [of _ _ A X] H I simp: ctyping1_def)
  moreover {
    fix x
    assume "x ∉ Univ?? B1 {x. ∀f ∈ {λx. [y←ys. fst y = x] | ys. ys ∈ ⊢ c}.
      if f x = [] then x ∈ X else snd (last (f x)) ≠ None}"
    moreover from this have "B1 ≠ {}"
      by (simp split: if_split_asm)
    ultimately have "¬ (∀f.
      (∃ys. f = (λx. [y←ys. fst y = x]) ∧ (ys = [] ∨ ys ∈ ⊢ c)) ⟶
        (if f x = [] then x ∈ X else snd (last (f x)) ≠ None))"
      (is "¬ ?P")
      by (auto split: if_split_asm)
    moreover assume ?P
    ultimately have False
      by contradiction
  }
  note J = this
  {
    fix x v
    assume "x ∉ Univ?? B1 {x. ∀f ∈ {λx. [y←ys. fst y = x] | ys. ys ∈ ⊢ c}.
      if f x = [] then x ∈ X else snd (last (f x)) ≠ None}"
    moreover from this have K: "B1 ≠ {}"
      by (simp split: if_split_asm)
    ultimately have L: "¬ (∀f.
      (∃ys. f = (λx. [y←ys. fst y = x]) ∧ ys ∈ ⊢ c) ⟶
        (if f x = [] then x ∈ X else snd (last (f x)) ≠ None))"
      (is "¬ ?P")
      by (auto split: if_split_asm)
    assume "⊢ b = Some v"
    with C and K have v
      by (auto dest: btyping1_btyping2 [of _ _ A X])
    moreover assume "∀f. (∃ys. f = (λx. [y←ys. fst y = x]) ∧
      (ys ∈ (if ¬ v then {[]} else {}) ∨ ys ∈ (if v then ⊢ c else {}))) ⟶
        (if f x = [] then x ∈ X else snd (last (f x)) ≠ None)"
    ultimately have ?P
      by simp
    with L have False
      by contradiction
  }
  note K = this
  from A and D and G have "Z ⊆ Y"
    apply (cases "A = {}")
     apply (fastforce simp: ctyping1_def)
    apply (cases "⊢ b")
    by (auto dest: J K simp: ctyping1_def)
  ultimately show ?thesis
    using F by simp
qed

lemma ctyping1_ctyping2_snd:
 "⟦⊢ c (⊆ A, X) = (C, Z); (U, False) ⊨ c (⊆ A, X) = Some (C', Z')⟧ ⟹
    Z ⊆ Z'"
  apply (induction "(U, False)" c A X arbitrary: C C' Z Z' U
   rule: ctyping2.induct)
         apply fastforce
        apply fastforce
       apply fastforce
      apply fastforce
     apply (erule ctyping1_ctyping2_snd_seq, assumption+)
    apply (erule ctyping1_ctyping2_snd_or, assumption+)
   apply (erule ctyping1_ctyping2_snd_if, assumption+)
  apply (erule ctyping1_ctyping2_snd_while, assumption+)
  done


lemma ctyping1_ctyping2:
 "⟦⊢ c (⊆ A, X) = (C, Z); (U, False) ⊨ c (⊆ A, X) = Some (C', Z')⟧ ⟹
    C' ⊆ C ∧ Z ⊆ Z'"
by (blast dest: ctyping1_ctyping2_fst ctyping1_ctyping2_snd)


lemma btyping2_aux_approx_1 [elim]:
  assumes
    A: "⊫ b1 (⊆ A, X) = Some B1" and
    B: "⊫ b2 (⊆ A, X) = Some B2" and
    C: "bval b1 s" and
    D: "bval b2 s" and
    E: "r ∈ A" and
    F: "s = r (⊆ state ∩ X)"
  shows "∃r' ∈ B1 ∩ B2. r = r' (⊆ state ∩ X)"
proof -
  from A and C and E and F have "r ∈ B1"
    by (frule_tac btyping2_aux_subset, drule_tac btyping2_aux_eq, auto)
  moreover from B and D and E and F have "r ∈ B2"
    by (frule_tac btyping2_aux_subset, drule_tac btyping2_aux_eq, auto)
  ultimately show ?thesis
    by blast
qed

lemma btyping2_aux_approx_2 [elim]:
  assumes
    A: "avars a1 ⊆ state" and
    B: "avars a2 ⊆ state" and
    C: "avars a1 ⊆ X" and
    D: "avars a2 ⊆ X" and
    E: "aval a1 s < aval a2 s" and
    F: "r ∈ A" and
    G: "s = r (⊆ state ∩ X)"
  shows "∃r'. r' ∈ A ∧ aval a1 r' < aval a2 r' ∧ r = r' (⊆ state ∩ X)"
proof -
  have "aval a1 s = aval a1 r ∧ aval a2 s = aval a2 r"
    using A and B and C and D and G by (blast intro: avars_aval)
  thus ?thesis
    using E and F by auto
qed

lemma btyping2_aux_approx_3 [elim]:
  assumes
    A: "avars a1 ⊆ state" and
    B: "avars a2 ⊆ state" and
    C: "avars a1 ⊆ X" and
    D: "avars a2 ⊆ X" and
    E: "¬ aval a1 s < aval a2 s" and
    F: "r ∈ A" and
    G: "s = r (⊆ state ∩ X)"
  shows "∃r' ∈ A - {s ∈ A. aval a1 s < aval a2 s}. r = r' (⊆ state ∩ X)"
proof -
  have "aval a1 s = aval a1 r ∧ aval a2 s = aval a2 r"
    using A and B and C and D and G by (blast intro: avars_aval)
  thus ?thesis
    using E and F by auto
qed

lemma btyping2_aux_approx:
 "⟦⊫ b (⊆ A, X) = Some A'; s ∈ Univ A (⊆ state ∩ X)⟧ ⟹
    s ∈ Univ (if bval b s then A' else A - A') (⊆ state ∩ X)"
by (induction b arbitrary: A', auto dest: btyping2_aux_subset
 split: if_split_asm option.split_asm)

lemma btyping2_approx:
 "⟦⊨ b (⊆ A, X) = (B1, B2); s ∈ Univ A (⊆ state ∩ X)⟧ ⟹
    s ∈ Univ (if bval b s then B1 else B2) (⊆ state ∩ X)"
by (drule sym, simp add: btyping2_def split: option.split_asm,
 drule btyping2_aux_approx, auto)


lemma ctyping2_approx_assign [elim!]:
 "⟦∀t'. aval a s = t' x ⟶ (∀s. t' = s(x := aval a s) ⟶ s ∉ A) ∨
    (∃y ∈ state ∩ X. y ≠ x ∧ t y ≠ t' y);
  v ⊨ a (⊆ X); t ∈ A; s = t (⊆ state ∩ X)⟧ ⟹ False"
by (drule spec [of _ "t(x := aval a t)"], cases a,
 (fastforce simp del: aval.simps(3) intro: avars_aval)+)

lemma ctyping2_approx_if_1:
 "⟦bval b s; ⊨ b (⊆ A, X) = (B1, B2); r ∈ A; s = r (⊆ state ∩ X);
    (insert (Univ? A X, bvars b) U, v) ⊨ c1 (⊆ B1, X) = Some (C1, Y1);
    ⋀A B X Y U v. (U, v) ⊨ c1 (⊆ A, X) = Some (B, Y) ⟹
      ∃r ∈ A. s = r (⊆ state ∩ X) ⟹ ∃r' ∈ B. t = r' (⊆ state ∩ Y)⟧ ⟹
  ∃r' ∈ C1 ∪ C2. t = r' (⊆ state ∩ (Y1 ∩ Y2))"
by (drule btyping2_approx, blast, fastforce)

lemma ctyping2_approx_if_2:
 "⟦¬ bval b s; ⊨ b (⊆ A, X) = (B1, B2); r ∈ A; s = r (⊆ state ∩ X);
    (insert (Univ? A X, bvars b) U, v) ⊨ c2 (⊆ B2, X) = Some (C2, Y2);
    ⋀A B X Y U v. (U, v) ⊨ c2 (⊆ A, X) = Some (B, Y) ⟹
      ∃r ∈ A. s = r (⊆ state ∩ X) ⟹ ∃r' ∈ B. t = r' (⊆ state ∩ Y)⟧ ⟹
  ∃r' ∈ C1 ∪ C2. t = r' (⊆ state ∩ (Y1 ∩ Y2))"
by (drule btyping2_approx, blast, fastforce)

lemma ctyping2_approx_while_1 [elim]:
 "⟦¬ bval b s; r ∈ A; s = r (⊆ state ∩ X); ⊨ b (⊆ A, X) = (B, {})⟧ ⟹
    ∃t ∈ C. s = t (⊆ state ∩ Y)"
by (drule btyping2_approx, blast, simp)

lemma ctyping2_approx_while_2 [elim]:
 "⟦∀t ∈ B2 ∪ B2'. ∃x ∈ state ∩ (X ∩ Y). r x ≠ t x; ¬ bval b s;
    r ∈ A; s = r (⊆ state ∩ X); ⊨ b (⊆ A, X) = (B1, B2)⟧ ⟹ False"
by (drule btyping2_approx, blast, auto)

lemma ctyping2_approx_while_aux:
  assumes
    A: "⊨ b (⊆ A, X) = (B1, B2)" and
    B: "⊢ c (⊆ B1, X) = (C, Y)" and
    C: "⊨ b (⊆ C, Y) = (B1', B2')" and
    D: "({}, False) ⊨ c (⊆ B1, X) = Some (D, Z)" and
    E: "({}, False) ⊨ c (⊆ B1', Y) = Some (D', Z')" and
    F: "r1 ∈ A" and
    G: "s1 = r1 (⊆ state ∩ X)" and
    H: "bval b s1" and
    I: "⋀C B Y W U. (case ⊨ b (⊆ C, Y) of (B1', B2') ⇒
      case ⊢ c (⊆ B1', Y) of (C', Y') ⇒
      case ⊨ b (⊆ C', Y') of (B1'', B2'') ⇒ if
        (∀s ∈ Univ? C Y ∪ Univ? C' Y'. ∀x ∈ bvars b. ∀y. s: dom x ↝ dom y) ∧
        (∀p ∈ U. case p of (B, W) ⇒ ∀s ∈ B. ∀x ∈ W. ∀y. s: dom x ↝ dom y)
        then case ({}, False) ⊨ c (⊆ B1', Y) of
          None ⇒ None | Some _ ⇒ case ({}, False) ⊨ c (⊆ B1'', Y') of
            None ⇒ None | Some _ ⇒ Some (B2' ∪ B2'', Univ?? B2' Y ∩ Y')
        else None) = Some (B, W) ⟹
          ∃r ∈ C. s2 = r (⊆ state ∩ Y) ⟹ ∃r ∈ B. s3 = r (⊆ state ∩ W)"
      (is "⋀C B Y W U. ?P C B Y W U ⟹ _ ⟹ _") and
    J: "⋀A B X Y U v. (U, v) ⊨ c (⊆ A, X) = Some (B, Y) ⟹
      ∃r ∈ A. s1 = r (⊆ state ∩ X) ⟹ ∃r ∈ B. s2 = r (⊆ state ∩ Y)" and
    K: "∀s ∈ Univ? A X ∪ Univ? C Y. ∀x ∈ bvars b. ∀y. s: dom x ↝ dom y" and
    L: "∀p ∈ U. ∀B W. p = (B, W) ⟶
      (∀s ∈ B. ∀x ∈ W. ∀y. s: dom x ↝ dom y)"
  shows "∃r ∈ B2 ∪ B2'. s3 = r (⊆ state ∩ Univ?? B2 X ∩ Y)"
proof -
  obtain C' Y' where M: "⊢ c (⊆ B1', Y) = (C', Y')"
    by (cases "⊢ c (⊆ B1', Y)", simp)
  obtain B1'' B2'' where N: "(B1'', B2'') = ⊨ b (⊆ C', Y')"
    by (cases "⊨ b (⊆ C', Y')", simp)
  let ?B = "B2' ∪ B2''"
  let ?W = "Univ?? B2' Y ∩ Y'"
  have "⊢ c (⊆ C, Y) = (C, Y)"
    using ctyping1_idem and B by auto
  moreover have "B1' ⊆ C"
    using C by (blast dest: btyping2_un_eq)
  ultimately have O: "C' ⊆ C ∧ Y ⊆ Y'"
    by (rule ctyping1_mono [OF _ M], simp)
  hence "Univ? C' Y' ⊆ Univ? C Y"
    by (auto simp: univ_states_if_def)
  moreover from I have "?P C ?B Y ?W U ⟹
    ∃r ∈ C. s2 = r (⊆ state ∩ Y) ⟹ ∃r ∈ ?B. s3 = r (⊆ state ∩ ?W)" .
  ultimately have "(case ({}, False) ⊨ c (⊆ B1'', Y') of
    None ⇒ None | Some _ ⇒ Some (?B, ?W)) = Some (?B, ?W) ⟹
      ∃r ∈ C. s2 = r (⊆ state ∩ Y) ⟹ ∃r ∈ ?B. s3 = r (⊆ state ∩ ?W)"
    using C and E and K and L and M and N
     by (fastforce split: if_split_asm prod.split_asm)
  moreover have P: "B1'' ⊆ B1' ∧ B2'' ⊆ B2'"
    by (metis btyping2_mono C N O)
  hence "∃D'' Z''. ({}, False) ⊨ c (⊆ B1'', Y') =
    Some (D'', Z'') ∧ D'' ⊆ D' ∧ Z' ⊆ Z''"
    using E and O by (auto intro: ctyping2_mono)
  ultimately have
   "∃r ∈ C. s2 = r (⊆ state ∩ Y) ⟹ ∃r ∈ ?B. s3 = r (⊆ state ∩ ?W)"
    by fastforce
  moreover from A and D and F and G and H and J obtain r2 where
   "r2 ∈ D" and "s2 = r2 (⊆ state ∩ Z)"
    by (drule_tac btyping2_approx, blast, force)
  moreover have "D ⊆ C ∧ Y ⊆ Z"
    using B and D by (rule ctyping1_ctyping2)
  ultimately obtain r3 where Q: "r3 ∈ ?B" and R: "s3 = r3 (⊆ state ∩ ?W)"
    by blast
  show ?thesis
  proof (rule bexI [of _ r3])
    show "s3 = r3 (⊆ state ∩ Univ?? B2 X ∩ Y)"
      using O and R by auto
  next
    show "r3 ∈ B2 ∪ B2'"
      using P and Q by blast
  qed
qed

lemmas ctyping2_approx_while_3 =
  ctyping2_approx_while_aux [where B2 = "{}", simplified]

lemma ctyping2_approx_while_4:
 "⟦⊨ b (⊆ A, X) = (B1, B2);
  ⊢ c (⊆ B1, X) = (C, Y);
  ⊨ b (⊆ C, Y) = (B1', B2');
  ({}, False) ⊨ c (⊆ B1, X) = Some (D, Z);
  ({}, False) ⊨ c (⊆ B1', Y) = Some (D', Z');
  r1 ∈ A; s1 = r1 (⊆ state ∩ X); bval b s1;
  ⋀C B Y W U. (case ⊨ b (⊆ C, Y) of (B1', B2') ⇒
    case ⊢ c (⊆ B1', Y) of (C', Y') ⇒
    case ⊨ b (⊆ C', Y') of (B1'', B2'') ⇒
      if (∀s ∈ Univ? C Y ∪ Univ? C' Y'. ∀x ∈ bvars b. ∀y. s: dom x ↝ dom y) ∧
        (∀p ∈ U. case p of (B, W) ⇒ ∀s ∈ B. ∀x ∈ W. ∀y. s: dom x ↝ dom y)
      then case ({}, False) ⊨ c (⊆ B1', Y) of
        None ⇒ None | Some _ ⇒ case ({}, False) ⊨ c (⊆ B1'', Y') of
          None ⇒ None | Some _ ⇒ Some (B2' ∪ B2'', Univ?? B2' Y ∩ Y')
      else None) = Some (B, W) ⟹
    ∃r ∈ C. s2 = r (⊆ state ∩ Y) ⟹ ∃r ∈ B. s3 = r (⊆ state ∩ W);
  ⋀A B X Y U v. (U, v) ⊨ c (⊆ A, X) = Some (B, Y) ⟹
    ∃r ∈ A. s1 = r (⊆ state ∩ X) ⟹ ∃r ∈ B. s2 = r (⊆ state ∩ Y);
  ∀s ∈ Univ? A X ∪ Univ? C Y. ∀x ∈ bvars b. ∀y. s: dom x ↝ dom y;
  ∀p ∈ U. ∀B W. p = (B, W) ⟶ (∀s ∈ B. ∀x ∈ W. ∀y. s: dom x ↝ dom y);
  ∀r ∈ B2 ∪ B2'. ∃x ∈ state ∩ (X ∩ Y). s3 x ≠ r x⟧ ⟹
    False"
by (drule ctyping2_approx_while_aux, assumption+, auto)

lemma ctyping2_approx:
 "⟦(c, s, p) ⇒ (t, q); (U, v) ⊨ c (⊆ A, X) = Some (B, Y);
    s ∈ Univ A (⊆ state ∩ X)⟧ ⟹ t ∈ Univ B (⊆ state ∩ Y)"
proof (induction "(c, s, p)" "(t, q)" arbitrary: A B X Y U v c s p t q
 rule: big_step.induct)
  fix A C X Z U v c1 c2 s p t q and p' :: stage
  show
   "⟦⋀r q A B X Y U v. p' = (r, q) ⟹
      (U, v) ⊨ c1 (⊆ A, X) = Some (B, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹ r ∈ Univ B (⊆ state ∩ Y);
    ⋀r q B C Y Z U v. p' = (r, q) ⟹
      (U, v) ⊨ c2 (⊆ B, Y) = Some (C, Z) ⟹
      r ∈ Univ B (⊆ state ∩ Y) ⟹ t ∈ Univ C (⊆ state ∩ Z);
    (U, v) ⊨ c1;; c2 (⊆ A, X) = Some (C, Z);
    s ∈ Univ A (⊆ state ∩ X)⟧ ⟹
      t ∈ Univ C (⊆ state ∩ Z)"
    by (cases p', auto split: option.split_asm prod.split_asm)
next
  fix A C X Y U v c1 c2 s p t q
  show
   "⟦⋀A C X Y U v. (U, v) ⊨ c1 (⊆ A, X) = Some (C, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹ t ∈ Univ C (⊆ state ∩ Y);
    (U, v) ⊨ c1 OR c2 (⊆ A, X) = Some (C, Y);
    s ∈ Univ A (⊆ state ∩ X)⟧ ⟹
      t ∈ Univ C (⊆ state ∩ Y)"
    by (fastforce split: option.split_asm)
next
  fix A C X Y U v c1 c2 s p t q
  show
   "⟦⋀A C X Y U v. (U, v) ⊨ c2 (⊆ A, X) = Some (C, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹ t ∈ Univ C (⊆ state ∩ Y);
    (U, v) ⊨ c1 OR c2 (⊆ A, X) = Some (C, Y);
    s ∈ Univ A (⊆ state ∩ X)⟧ ⟹
      t ∈ Univ C (⊆ state ∩ Y)"
    by (fastforce split: option.split_asm)
next
  fix A B X Y U v b c1 c2 s p t q
  show
   "⟦bval b s; (c1, s, p) ⇒ (t, q);
    ⋀A C X Y U v. (U, v) ⊨ c1 (⊆ A, X) = Some (C, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹ t ∈ Univ C (⊆ state ∩ Y);
    (U, v) ⊨ IF b THEN c1 ELSE c2 (⊆ A, X) = Some (B, Y);
    s ∈ Univ A (⊆ state ∩ X)⟧ ⟹
      t ∈ Univ B (⊆ state ∩ Y)"
    by (auto split: option.split_asm prod.split_asm,
     rule ctyping2_approx_if_1)
next
  fix A B X Y U v b c1 c2 s p t q
  show
   "⟦¬ bval b s; (c2, s, p) ⇒ (t, q);
    ⋀A C X Y U v. (U, v) ⊨ c2 (⊆ A, X) = Some (C, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹ t ∈ Univ C (⊆ state ∩ Y);
    (U, v) ⊨ IF b THEN c1 ELSE c2 (⊆ A, X) = Some (B, Y);
    s ∈ Univ A (⊆ state ∩ X)⟧ ⟹
      t ∈ Univ B (⊆ state ∩ Y)"
    by (auto split: option.split_asm prod.split_asm,
     rule ctyping2_approx_if_2)
next
  fix A B X Y U v b c s1 p1 s2 p2 s3 p3
  show
   "⟦bval b s1; (c, s1, p1) ⇒ (s2, p2);
    ⋀A B X Y U v. (U, v) ⊨ c (⊆ A, X) = Some (B, Y) ⟹
      s1 ∈ Univ A (⊆ state ∩ X) ⟹ s2 ∈ Univ B (⊆ state ∩ Y);
    (WHILE b DO c, s2, p2) ⇒ (s3, p3);
    ⋀A B X Y U v. (U, v) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Y) ⟹
      s2 ∈ Univ A (⊆ state ∩ X) ⟹ s3 ∈ Univ B (⊆ state ∩ Y);
    (U, v) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Y);
    s1 ∈ Univ A (⊆ state ∩ X)⟧ ⟹
      s3 ∈ Univ B (⊆ state ∩ Y)"
  by (auto split: if_split_asm option.split_asm prod.split_asm,
   erule_tac [2] ctyping2_approx_while_4,
   erule ctyping2_approx_while_3)
qed (auto split: if_split_asm option.split_asm prod.split_asm)

end

end