Theory Overapproximation

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

theory Overapproximation
  imports Idempotence
begin

text ‹
\null

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) ⇒ t"}, (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 a state in @{term A} on the value of every state variable in @{term X}, then @{term t}
must agree with some state in @{term B} on the value of every 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: dom ` Y ↝ W⟧ ⟹
  ∀(B, Y) ∈ insert (Univ? A' X', Z) U'. B: dom ` 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 a⇩1 = {}" and
    B: "avars a⇩2 = {}" and
    C: "aval a⇩1 (λx. 0) < aval a⇩2 (λx. 0)"
  shows "aval a⇩1 s < aval a⇩2 s"
proof -
  have "aval a⇩1 s = aval a⇩1 (λx. 0) ∧ aval a⇩2 s = aval a⇩2 (λ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 a⇩1 = {}" and
    B: "avars a⇩2 = {}" and
    C: "¬ aval a⇩1 (λx. 0) < aval a⇩2 (λx. 0)" and
    D: "aval a⇩1 s < aval a⇩2 s"
  shows False
proof -
  have "aval a⇩1 s = aval a⇩1 (λx. 0) ∧ aval a⇩2 s = aval a⇩2 (λ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) = (B⇩1, B⇩2); ⊨ b (⊆ A', X') = (B⇩1', B⇩2'); A' ⊆ A; X ⊆ X'⟧ ⟹
    B⇩1' ⊆ B⇩1 ∧ B⇩2' ⊆ B⇩2"
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) = (B⇩1, B⇩2) ⟹ B⇩1 ∪ B⇩2 = A"
by (auto simp: btyping2_def dest: btyping2_aux_subset split: option.split_asm)

lemma btyping2_fst_empty:
 "⊨ b (⊆ {}, X) = ({}, {})"
by (auto simp: btyping2_def dest: btyping2_aux_subset split: option.split)

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' b⇩1 b⇩2
  show
   "⟦⋀A'. ⊫ b⇩1 (⊆ A, X) = Some A' ⟹ s = t (⊆ state ∩ X) ⟹
      bval b⇩1 s = bval b⇩1 t;
    ⋀A'. ⊫ b⇩2 (⊆ A, X) = Some A' ⟹ s = t (⊆ state ∩ X) ⟹
      bval b⇩2 s = bval b⇩2 t;
    ⊫ And b⇩1 b⇩2 (⊆ A, X) = Some A'; s = t (⊆ state ∩ X)⟧ ⟹
      bval (And b⇩1 b⇩2) s = bval (And b⇩1 b⇩2) t"
    by (simp split: option.split_asm)
next
  fix A' a⇩1 a⇩2
  show
   "⟦⊫ Less a⇩1 a⇩2 (⊆ A, X) = Some A'; s = t (⊆ state ∩ X)⟧ ⟹
      bval (Less a⇩1 a⇩2) s = bval (Less a⇩1 a⇩2) t"
    by (subgoal_tac "aval a⇩1 s = aval a⇩1 t",
     subgoal_tac "aval a⇩2 s = aval a⇩2 t",
     auto intro!: avars_aval split: if_split_asm)
qed


lemma ctyping1_merge_in:
 "xs ∈ A ∪ B ⟹ xs ∈ A ⊔ B"
by (force simp: ctyping1_merge_def)

lemma ctyping1_merge_append_in:
 "⟦xs ∈ A; ys ∈ B⟧ ⟹ xs @ ys ∈ A ⊔⇩@ B"
by (force simp: ctyping1_merge_append_def ctyping1_append_def ctyping1_merge_in)

lemma ctyping1_aux_nonempty:
 "⊢ c ≠ {}"
by (induction c, simp_all add: Let_def ctyping1_append_def
 ctyping1_merge_def ctyping1_merge_append_def, fastforce+)

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

lemma ctyping2_fst_empty:
 "Some (B, Y) = (U, v) ⊨ c (⊆ {}, X) ⟹ (B, Y) = ({}, UNIV)"
proof (induction "(U, v)" c "{} :: state set" X arbitrary: B Y U v
 rule: ctyping2.induct)
  fix C X Y U v b c⇩1 c⇩2
  show
   "⟦⋀U' p B⇩2 C Y.
      (U', p) = (insert (Univ? {} X, bvars b) U, ⊨ b (⊆ {}, X)) ⟹
      ({}, B⇩2) = p ⟹ Some (C, Y) = (U', v) ⊨ c⇩1 (⊆ {}, X) ⟹
      (C, Y) = ({}, UNIV);
    ⋀U' p B⇩1 C Y.
      (U', p) = (insert (Univ? {} X, bvars b) U, ⊨ b (⊆ {}, X)) ⟹
      (B⇩1, {}) = p ⟹ Some (C, Y) = (U', v) ⊨ c⇩2 (⊆ {}, X) ⟹
      (C, Y) = ({}, UNIV);
    Some (C, Y) = (U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ {}, X)⟧ ⟹
      (C, Y) = ({}, UNIV)"
    by (fastforce simp: btyping2_fst_empty split: option.split_asm)
next
  fix B X Z U v b c
  show
   "⟦⋀B⇩2 C Y B⇩1' B⇩2' B Z.
      ({}, B⇩2) = ⊨ b (⊆ {}, X) ⟹
      (C, Y) = ⊢ c (⊆ {}, X) ⟹
      (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? {} X ∪ Univ? C Y, bvars b) U.
        B: dom ` W ↝ UNIV ⟹
      Some (B, Z) = ({}, False) ⊨ c (⊆ {}, X) ⟹
      (B, Z) = ({}, UNIV);
    ⋀B⇩1 B⇩2 C Y B⇩2' B Z.
      (B⇩1, B⇩2) = ⊨ b (⊆ {}, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹
      ({}, B⇩2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? {} X ∪ Univ? C Y, bvars b) U.
        B: dom ` W ↝ UNIV ⟹
      Some (B, Z) = ({}, False) ⊨ c (⊆ {}, Y) ⟹
      (B, Z) = ({}, UNIV);
    Some (B, Z) = (U, v) ⊨ WHILE b DO c (⊆ {}, X)⟧ ⟹
      (B, Z) = ({}, UNIV)"
    by (simp split: if_split_asm option.split_asm prod.split_asm,
     (fastforce simp: btyping2_fst_empty ctyping1_def)+)
qed (simp_all split: if_split_asm option.split_asm prod.split_asm)


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 = "{dom x}"], auto split: if_split_asm)

lemma ctyping2_mono_seq:
  assumes
    A: "⋀A' B X' Y U'.
      (U, False) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹ A' ⊆ A ⟹ X ⊆ X' ⟹
        ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y ⟹
          ∃B' Y'. (U', False) ⊨ c⇩1 (⊆ A', X') = Some (B', Y') ∧
            B' ⊆ B ∧ Y ⊆ Y'" and
    B: "⋀p B Y B' C Y' Z U'.
      (U, False) ⊨ c⇩1 (⊆ A, X) = Some p ⟹ (B, Y) = p ⟹
        (U, False) ⊨ c⇩2 (⊆ B, Y) = Some (C, Z) ⟹ B' ⊆ B ⟹ Y ⊆ Y' ⟹
          ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y ⟹
            ∃C' Z'. (U', False) ⊨ c⇩2 (⊆ B', Y') = Some (C', Z') ∧
              C' ⊆ C ∧ Z ⊆ Z'" and
    C: "(U, False) ⊨ c⇩1;; c⇩2 (⊆ 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) ⊨ c⇩1;; c⇩2 (⊆ A', X') = Some (C', Z') ∧
    C' ⊆ C ∧ Z ⊆ Z'"
proof -
  obtain B Y where "(U, False) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ∧
    (U, False) ⊨ c⇩2 (⊆ B, Y) = Some (C, Z)"
    using C by (auto split: option.split_asm)
  moreover from this obtain B' Y' where
    G: "(U', False) ⊨ c⇩1 (⊆ 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) ⊨ c⇩2 (⊆ 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_if:
  assumes
    A: "⋀W p B⇩1 B⇩2 B⇩1' C⇩1 X' Y⇩1 W'. (W, p) =
      (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹ (B⇩1, B⇩2) = p ⟹
        (W, False) ⊨ c⇩1 (⊆ B⇩1, X) = Some (C⇩1, Y⇩1) ⟹ B⇩1' ⊆ B⇩1 ⟹
          X ⊆ X' ⟹ ∀(B', Y') ∈ W'. ∃(B, Y) ∈ W. B' ⊆ B ∧ Y' ⊆ Y ⟹
            ∃C⇩1' Y⇩1'. (W', False) ⊨ c⇩1 (⊆ B⇩1', X') = Some (C⇩1', Y⇩1') ∧
              C⇩1' ⊆ C⇩1 ∧ Y⇩1 ⊆ Y⇩1'" and
    B: "⋀W p B⇩1 B⇩2 B⇩2' C⇩2 X' Y⇩2 W'. (W, p) =
      (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹ (B⇩1, B⇩2) = p ⟹
        (W, False) ⊨ c⇩2 (⊆ B⇩2, X) = Some (C⇩2, Y⇩2) ⟹ B⇩2' ⊆ B⇩2 ⟹
          X ⊆ X' ⟹ ∀(B', Y') ∈ W'. ∃(B, Y) ∈ W. B' ⊆ B ∧ Y' ⊆ Y ⟹
            ∃C⇩2' Y⇩2'. (W', False) ⊨ c⇩2 (⊆ B⇩2', X') = Some (C⇩2', Y⇩2') ∧
              C⇩2' ⊆ C⇩2 ∧ Y⇩2 ⊆ Y⇩2'" and
    C: "(U, False) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ 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 c⇩1 ELSE c⇩2 (⊆ 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 B⇩1 B⇩2 C⇩1 C⇩2 Y⇩1 Y⇩2 where
    G: "(C, Y) = (C⇩1 ∪ C⇩2, Y⇩1 ∩ Y⇩2) ∧ (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ∧
      Some (C⇩1, Y⇩1) = (?W, False) ⊨ c⇩1 (⊆ B⇩1, X) ∧
      Some (C⇩2, Y⇩2) = (?W, False) ⊨ c⇩2 (⊆ B⇩2, X)"
    using C by (simp split: option.split_asm prod.split_asm)
  moreover obtain B⇩1' B⇩2' where H: "(B⇩1', B⇩2') = ⊨ b (⊆ A', X')"
    by (cases "⊨ b (⊆ A', X')", simp)
  ultimately have I: "B⇩1' ⊆ B⇩1 ∧ B⇩2' ⊆ B⇩2"
    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 "∃C⇩1' Y⇩1'.
    (?W', False) ⊨ c⇩1 (⊆ B⇩1', X') = Some (C⇩1', Y⇩1') ∧ C⇩1' ⊆ C⇩1 ∧ Y⇩1 ⊆ Y⇩1'"
    using A and E and G by force
  moreover have "∃C⇩2' Y⇩2'.
    (?W', False) ⊨ c⇩2 (⊆ B⇩2', X') = Some (C⇩2', Y⇩2') ∧ C⇩2' ⊆ C⇩2 ∧ Y⇩2 ⊆ Y⇩2'"
    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: "⋀B⇩1 B⇩2 C Y B⇩1' B⇩2' D⇩1 E X' V U'. (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹ (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
        ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
          B: dom ` W ↝ UNIV ⟹
          ({}, False) ⊨ c (⊆ B⇩1, X) = Some (E, V) ⟹ D⇩1 ⊆ B⇩1 ⟹
            X ⊆ X' ⟹ ∀(B', Y') ∈ U'. ∃(B, Y) ∈ {}. B' ⊆ B ∧ Y' ⊆ Y ⟹
              ∃E' V'. (U', False) ⊨ c (⊆ D⇩1, X') = Some (E', V') ∧
                E' ⊆ E ∧ V ⊆ V'" and
    B: "⋀B⇩1 B⇩2 C Y B⇩1' B⇩2' D⇩1' F Y' W U'. (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹ (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
        ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
          B: dom ` W ↝ UNIV ⟹
          ({}, False) ⊨ c (⊆ B⇩1', Y) = Some (F, W) ⟹ D⇩1' ⊆ B⇩1' ⟹
            Y ⊆ Y' ⟹ ∀(B', Y') ∈ U'. ∃(B, Y) ∈ {}. B' ⊆ B ∧ Y' ⊆ Y ⟹
              ∃F' W'. (U', False) ⊨ c (⊆ D⇩1', 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 B⇩1 B⇩1' B⇩2 B⇩2' C E F V W Y where G: "(B⇩1, B⇩2) = ⊨ b (⊆ A, X) ∧
    (C, Y) = ⊢ c (⊆ B⇩1, X) ∧ (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ∧
    (∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
      B: dom ` W ↝ UNIV) ∧
    Some (E, V) = ({}, False) ⊨ c (⊆ B⇩1, X) ∧
    Some (F, W) = ({}, False) ⊨ c (⊆ B⇩1', Y) ∧
    (B, Z) = (B⇩2 ∪ B⇩2', Univ?? B⇩2 X ∩ Y)"
    using C by (force split: if_split_asm option.split_asm prod.split_asm)
  moreover obtain D⇩1 D⇩2 where H: "⊨ b (⊆ A', X') = (D⇩1, D⇩2)"
    by (cases "⊨ b (⊆ A', X')", simp)
  ultimately have I: "D⇩1 ⊆ B⇩1 ∧ D⇩2 ⊆ B⇩2"
    by (smt (verit) btyping2_mono D E)
  moreover obtain C' Y' where J: "(C', Y') = ⊢ c (⊆ D⇩1, X')"
    by (cases "⊢ c (⊆ D⇩1, X')", simp)
  ultimately have K: "C' ⊆ C ∧ Y ⊆ Y'"
    by (meson ctyping1_mono E G)
  moreover obtain D⇩1' D⇩2' where L: "⊨ b (⊆ C', Y') = (D⇩1', D⇩2')"
    by (cases "⊨ b (⊆ C', Y')", simp)
  ultimately have M: "D⇩1' ⊆ B⇩1' ∧ D⇩2' ⊆ B⇩2'"
    by (smt (verit) btyping2_mono G)
  then obtain F' W' where
   "({}, False) ⊨ c (⊆ D⇩1', 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 (⊆ D⇩1, 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 (D⇩2 ∪ D⇩2', Univ?? D⇩2 X' ∩ Y')"
    using F and G and H and J [symmetric] and L by force
  moreover have "D⇩2 ∪ D⇩2' ⊆ B"
    using G and I and M by auto
  moreover have "Z ⊆ Univ?? D⇩2 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'"
proof (induction "(U, False)" c A X arbitrary: A' C X' Z U U'
 rule: ctyping2.induct)
  fix A A' X X' U U' C Z c⇩1 c⇩2
  show
   "⟦⋀A' B X' Y U'.
      (U, False) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      A' ⊆ A ⟹ X ⊆ X' ⟹
      ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y ⟹
      ∃B' Y'. (U', False) ⊨ c⇩1 (⊆ A', X') = Some (B', Y') ∧
        B' ⊆ B ∧ Y ⊆ Y';
    ⋀p B Y A' C X' Z U'. (U, False) ⊨ c⇩1 (⊆ A, X) = Some p ⟹
      (B, Y) = p ⟹ (U, False) ⊨ c⇩2 (⊆ B, Y) = Some (C, Z) ⟹
      A' ⊆ B ⟹ Y ⊆ X' ⟹
      ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y ⟹
      ∃C' Z'. (U', False) ⊨ c⇩2 (⊆ A', X') = Some (C', Z') ∧
        C' ⊆ C ∧ Z ⊆ Z';
    (U, False) ⊨ c⇩1;; c⇩2 (⊆ A, X) = Some (C, Z);
    A' ⊆ A; X ⊆ X';
    ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y⟧ ⟹
      ∃C' Z'. (U', False) ⊨ c⇩1;; c⇩2 (⊆ A', X') = Some (C', Z') ∧
        C' ⊆ C ∧ Z ⊆ Z'"
    by (rule ctyping2_mono_seq)
next
  fix A A' X X' U U' C Z b c⇩1 c⇩2
  show
   "⟦⋀U'' p B⇩1 B⇩2 A' C X' Z U'.
      (U'', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B⇩1, B⇩2) = p ⟹ (U'', False) ⊨ c⇩1 (⊆ B⇩1, X) = Some (C, Z) ⟹
      A' ⊆ B⇩1 ⟹ X ⊆ X' ⟹
      ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U''. B' ⊆ B ∧ Y' ⊆ Y ⟹
      ∃C' Z'. (U', False) ⊨ c⇩1 (⊆ A', X') = Some (C', Z') ∧
        C' ⊆ C ∧ Z ⊆ Z';
    ⋀U'' p B⇩1 B⇩2 A' C X' Z U'.
      (U'', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B⇩1, B⇩2) = p ⟹ (U'', False) ⊨ c⇩2 (⊆ B⇩2, X) = Some (C, Z) ⟹
      A' ⊆ B⇩2 ⟹ X ⊆ X' ⟹
      ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U''. B' ⊆ B ∧ Y' ⊆ Y ⟹
      ∃C' Z'. (U', False) ⊨ c⇩2 (⊆ A', X') = Some (C', Z') ∧
        C' ⊆ C ∧ Z ⊆ Z';
    (U, False) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X) = Some (C, Z);
    A' ⊆ A; X ⊆ X';
    ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y⟧ ⟹
      ∃C' Z'. (U', False) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A', X') =
        Some (C', Z') ∧ C' ⊆ C ∧ Z ⊆ Z'"
    by (rule ctyping2_mono_if)
next
  fix A A' X X' U U' B Z b c
  show
   "⟦⋀B⇩1 B⇩2 C Y B⇩1' B⇩2' A' B X' Z U'.
      (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹
      (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: dom ` W ↝ UNIV ⟹
      ({}, False) ⊨ c (⊆ B⇩1, X) = Some (B, Z) ⟹
      A' ⊆ B⇩1 ⟹ X ⊆ X' ⟹
      ∀(B', Y') ∈ U'. ∃(B, Y) ∈ {}. B' ⊆ B ∧ Y' ⊆ Y ⟹
        ∃B' Z'. (U', False) ⊨ c (⊆ A', X') = Some (B', Z') ∧
          B' ⊆ B ∧ Z ⊆ Z';
    ⋀B⇩1 B⇩2 C Y B⇩1' B⇩2' A' B X' Z U'.
      (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹
      (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: dom ` W ↝ UNIV ⟹
      ({}, False) ⊨ c (⊆ B⇩1', Y) = Some (B, Z) ⟹
      A' ⊆ B⇩1' ⟹ Y ⊆ X' ⟹
      ∀(B', Y') ∈ U'. ∃(B, Y) ∈ {}. B' ⊆ B ∧ Y' ⊆ Y ⟹
        ∃B' Z'. (U', False) ⊨ c (⊆ A', X') = Some (B', Z') ∧
          B' ⊆ B ∧ Z ⊆ Z';
    (U, False) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Z);
    A' ⊆ A; X ⊆ X';
    ∀(B', Y') ∈ U'. ∃(B, Y) ∈ U. B' ⊆ B ∧ Y' ⊆ Y⟧ ⟹
      ∃B' Z'. (U', False) ⊨ WHILE b DO c (⊆ A', X') =
        Some (B', Z') ∧ B' ⊆ B ∧ Z ⊆ Z'"
    by (rule ctyping2_mono_while)
qed fastforce+


lemma ctyping1_ctyping2_fst_assign [elim!]:
  assumes
    A: "(C, Z) = ⊢ x ::= a (⊆ A, X)" and
    B: "Some (C', Z') = (U, False) ⊨ x ::= a (⊆ A, X)"
  shows "C' ⊆ C"
proof -
  {
    fix s
    assume "s ∈ A"
    moreover assume "avars a = {}"
    hence "aval a s = aval a (λx. 0)"
      by (blast intro: avars_aval)
    ultimately have "∃s'. (∃t. s(x := aval a s) = (λx'. case case
      if x' = x then Some (Some (aval a (λx. 0))) else None of
        None ⇒ None | Some v ⇒ Some v of
          None ⇒ s' x' | Some None ⇒ t x' | Some (Some i) ⇒ i)) ∧ s' ∈ A"
      by fastforce
  }
  note C = this
  from A and B show ?thesis
    by (clarsimp simp: ctyping1_def ctyping1_seq_def split: if_split_asm,
     erule_tac C, simp, fastforce)
qed

lemma ctyping1_ctyping2_fst_seq:
  assumes
    A: "⋀B B' Y Y'. (B, Y) = ⊢ c⇩1 (⊆ A, X) ⟹
      Some (B', Y') = (U, False) ⊨ c⇩1 (⊆ A, X) ⟹ B' ⊆ B" and
    B: "⋀p B Y C C' Z Z'. (U, False) ⊨ c⇩1 (⊆ A, X) = Some p ⟹
      (B, Y) = p ⟹ (C, Z) = ⊢ c⇩2 (⊆ B, Y) ⟹
        Some (C', Z') = (U, False) ⊨ c⇩2 (⊆ B, Y) ⟹ C' ⊆ C" and
    C: "(C, Z) = ⊢ c⇩1;; c⇩2 (⊆ A, X)" and
    D: "Some (C', Z') = (U, False) ⊨ c⇩1;; c⇩2 (⊆ A, X)"
  shows "C' ⊆ C"
proof -
  let ?f = "foldl (;;) (λx. None)"
  let ?P = "λr A S. ∃f s. (∃t. r = (λx. case f x of
    None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i)) ∧
    (∃ys. f = ?f ys ∧ ys ∈ S) ∧ s ∈ A"
  let ?F = "λA S. {r. ?P r A S}"
  {
    fix s⇩3 B' Y'
    assume
      E: "⋀B'' B C C' Z'. B' = B'' ⟹ B = B'' ⟹ C = ?F B'' (⊢ c⇩2) ⟹
        Some (C', Z') = (U, False) ⊨ c⇩2 (⊆ B'', Y') ⟹
          C' ⊆ ?F B'' (⊢ c⇩2)" and
      F: "⋀B B''. B = ?F A (⊢ c⇩1) ⟹ B'' = B' ⟹ B' ⊆ ?F A (⊢ c⇩1)" and
      G: "Some (C', Z') = (U, False) ⊨ c⇩2 (⊆ B', Y')" and
      H: "s⇩3 ∈ C'"
    have "?P s⇩3 A (⊢ c⇩1 ⊔⇩@ ⊢ c⇩2)"
    proof -
      obtain s⇩2 and t⇩2 and ys⇩2 where
        I: "s⇩3 = (λx. case ?f ys⇩2 x of
          None ⇒ s⇩2 x | Some None ⇒ t⇩2 x | Some (Some i) ⇒ i) ∧
          s⇩2 ∈ B' ∧ ys⇩2 ∈ ⊢ c⇩2"
        using E and G and H by fastforce
      from this obtain s⇩1 and t⇩1 and ys⇩1 where
        J: "s⇩2 = (λx. case ?f ys⇩1 x of
          None ⇒ s⇩1 x | Some None ⇒ t⇩1 x | Some (Some i) ⇒ i) ∧
          s⇩1 ∈ A ∧ ys⇩1 ∈ ⊢ c⇩1"
        using F by fastforce
      let ?t = "λx. case ?f ys⇩2 x of
        None ⇒ case ?f ys⇩1 x of Some None ⇒ t⇩1 x | _ ⇒ 0 |
        Some None ⇒ t⇩2 x | _ ⇒ 0"
      from I and J have "s⇩3 = (λx. case ?f (ys⇩1 @ ys⇩2) x of
        None ⇒ s⇩1 x | Some None ⇒ ?t x | Some (Some i) ⇒ i)"
        by (fastforce dest: last_in_set simp: Let_def ctyping1_seq_last
         split: option.split)
      moreover have "ys⇩1 @ ys⇩2 ∈ ⊢ c⇩1 ⊔⇩@ ⊢ c⇩2"
        by (simp add: ctyping1_merge_append_in I J)
      ultimately show ?thesis
        using J by fastforce
    qed
  }
  note E = this
  from A and B and C and D show ?thesis
    by (auto simp: ctyping1_def split: option.split_asm, erule_tac E)
qed

lemma ctyping1_ctyping2_fst_if:
  assumes
    A: "⋀U' p B⇩1 B⇩2 C⇩1 C⇩1' Y⇩1 Y⇩1'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B⇩1, B⇩2) = p ⟹ (C⇩1, Y⇩1) = ⊢ c⇩1 (⊆ B⇩1, X) ⟹
          Some (C⇩1', Y⇩1') = (U', False) ⊨ c⇩1 (⊆ B⇩1, X) ⟹ C⇩1' ⊆ C⇩1" and
    B: "⋀U' p B⇩1 B⇩2 C⇩2 C⇩2' Y⇩2 Y⇩2'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B⇩1, B⇩2) = p ⟹ (C⇩2, Y⇩2) = ⊢ c⇩2 (⊆ B⇩2, X) ⟹
          Some (C⇩2', Y⇩2') = (U', False) ⊨ c⇩2 (⊆ B⇩2, X) ⟹ C⇩2' ⊆ C⇩2" and
    C: "(C, Y) = ⊢ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X)" and
    D: "Some (C', Y') = (U, False) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X)"
  shows "C' ⊆ C"
proof -
  let ?f = "foldl (;;) (λx. None)"
  let ?P = "λr A S. ∃f s. (∃t. r = (λx. case f x of
    None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i)) ∧
    (∃ys. f = ?f ys ∧ ys ∈ S) ∧ s ∈ A"
  let ?F = "λA S. {r. ?P r A S}"
  let ?S⇩1 = "λf. if f = Some True ∨ f = None then ⊢ c⇩1 else {}"
  let ?S⇩2 = "λf. if f = Some False ∨ f = None then ⊢ c⇩2 else {}"
  {
    fix s' B⇩1 B⇩2 C⇩1
    assume
      E: "⋀U' B⇩1' C⇩1' C⇩1''. U' = insert (Univ? A X, bvars b) U ⟹
        B⇩1' = B⇩1 ⟹ C⇩1' = ?F B⇩1 (⊢ c⇩1) ⟹ C⇩1'' = C⇩1 ⟹
          C⇩1 ⊆ ?F B⇩1 (⊢ c⇩1)" and
      F: "⊨ b (⊆ A, X) = (B⇩1, B⇩2)" and
      G: "s' ∈ C⇩1"
    have "?P s' A (let f = ⊢ b in ?S⇩1 f ⊔ ?S⇩2 f)"
    proof -
      obtain s and t and ys where
        H: "s' = (λx. case ?f ys x of
          None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i) ∧
          s ∈ B⇩1 ∧ ys ∈ ⊢ c⇩1"
        using E and G by fastforce
      moreover from F and this have "s ∈ A"
        by (blast dest: btyping2_un_eq)
      moreover from F and H have "⊢ b ≠ Some False"
        by (auto dest: btyping1_btyping2 [where A = A and X = X])
      hence "ys ∈ (let f = ⊢ b in ?S⇩1 f ∪ ?S⇩2 f)"
        using H by (auto simp: Let_def)
      hence "ys ∈ (let f = ⊢ b in ?S⇩1 f ⊔ ?S⇩2 f)"
        by (auto simp: Let_def intro: ctyping1_merge_in)
      ultimately show ?thesis
        by blast
    qed
  }
  note E = this
  {
    fix s' B⇩1 B⇩2 C⇩2
    assume
      F: "⋀U' B⇩2' C⇩2' C⇩2''. U' = insert (Univ? A X, bvars b) U ⟹
        B⇩2' = B⇩1 ⟹ C⇩2' = ?F B⇩2 (⊢ c⇩2) ⟹ C⇩2'' = C⇩2 ⟹
          C⇩2 ⊆ ?F B⇩2 (⊢ c⇩2)" and
      G: "⊨ b (⊆ A, X) = (B⇩1, B⇩2)" and
      H: "s' ∈ C⇩2"
    have "?P s' A (let f = ⊢ b in ?S⇩1 f ⊔ ?S⇩2 f)"
    proof -
      obtain s and t and ys where
        I: "s' = (λx. case ?f ys x of
          None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i) ∧
          s ∈ B⇩2 ∧ ys ∈ ⊢ c⇩2"
        using F and H by fastforce
      moreover from G and this have "s ∈ A"
        by (blast dest: btyping2_un_eq)
      moreover from G and I have "⊢ b ≠ Some True"
        by (auto dest: btyping1_btyping2 [where A = A and X = X])
      hence "ys ∈ (let f = ⊢ b in ?S⇩1 f ∪ ?S⇩2 f)"
        using I by (auto simp: Let_def)
      hence "ys ∈ (let f = ⊢ b in ?S⇩1 f ⊔ ?S⇩2 f)"
        by (auto simp: Let_def intro: ctyping1_merge_in)
      ultimately show ?thesis
        by blast
    qed
  }
  note F = this
  from A and B and C and D show ?thesis
    by (auto simp: ctyping1_def split: option.split_asm prod.split_asm,
     erule_tac [2] F, erule_tac E)
qed

lemma ctyping1_ctyping2_fst_while:
  assumes
    A: "(C, Y) = ⊢ WHILE b DO c (⊆ A, X)" and
    B: "Some (C', Y') = (U, False) ⊨ WHILE b DO c (⊆ A, X)"
  shows "C' ⊆ C"
proof -
  let ?f = "foldl (;;) (λx. None)"
  let ?P = "λr A S. ∃f s. (∃t. r = (λx. case f x of
    None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i)) ∧
    (∃ys. f = ?f ys ∧ ys ∈ S) ∧ s ∈ A"
  let ?F = "λA S. {r. ?P r A S}"
  let ?S⇩1 = "λf. if f = Some False ∨ f = None then {[]} else {}"
  let ?S⇩2 = "λf. if f = Some True ∨ f = None then ⊢ c else {}"
  {
    fix s' B⇩1 B⇩2 B⇩1' B⇩2'
    assume
      C: "⊨ b (⊆ A, X) = (B⇩1, B⇩2)" and
      D: "⊨ b (⊆ ?F B⇩1 (⊢ c), Univ?? B⇩1 {x. ∀f ∈ {?f ys |ys. ys ∈ ⊢ c}.
        f x ≠ Some None ∧ (f x = None ⟶ x ∈ X)}) = (B⇩1', B⇩2')"
        (is "⊨ _ (⊆ ?C, ?Y) = _")
    assume "s' ∈ C'" and "Some (C', Y') = (if (∀s ∈ Univ? A X ∪
      Univ? ?C ?Y. ∀x ∈ bvars b. All (interf s (dom x))) ∧
      (∀p ∈ U. ∀B W. p = (B, W) ⟶ (∀s ∈ B. ∀x ∈ W. All (interf s (dom x))))
        then Some (B⇩2 ∪ B⇩2', Univ?? B⇩2 X ∩ ?Y)
        else None)"
    hence "s' ∈ B⇩2 ∪ B⇩2'"
      by (simp split: if_split_asm)
    hence "?P s' A (let f = ⊢ b in ?S⇩1 f ∪ ?S⇩2 f)"
    proof
      assume E: "s' ∈ B⇩2"
      hence "s' ∈ A"
        using C by (blast dest: btyping2_un_eq)
      moreover from C and E have "⊢ b ≠ Some True"
        by (auto dest: btyping1_btyping2 [where A = A and X = X])
      hence "[] ∈ (let f = ⊢ b in ?S⇩1 f ∪ ?S⇩2 f)"
        by (auto simp: Let_def)
      ultimately show ?thesis
        by force
    next
      assume "s' ∈ B⇩2'"
      then obtain s and t and ys where
        E: "s' = (λx. case ?f ys x of
          None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i) ∧
          s ∈ B⇩1 ∧ ys ∈ ⊢ c"
        using D by (blast dest: btyping2_un_eq)
      moreover from C and this have "s ∈ A"
        by (blast dest: btyping2_un_eq)
      moreover from C and E have "⊢ b ≠ Some False"
        by (auto dest: btyping1_btyping2 [where A = A and X = X])
      hence "ys ∈ (let f = ⊢ b in ?S⇩1 f ∪ ?S⇩2 f)"
        using E by (auto simp: Let_def)
      ultimately show ?thesis
        by blast
    qed
  }
  note C = this
  from A and B show ?thesis
    by (auto intro: C simp: ctyping1_def
     split: option.split_asm prod.split_asm)
qed

lemma ctyping1_ctyping2_fst:
 "⟦(C, Z) = ⊢ c (⊆ A, X); Some (C', Z') = (U, False) ⊨ c (⊆ A, X)⟧ ⟹
    C' ⊆ C"
proof (induction "(U, False)" c A X arbitrary: C C' Z Z' U
 rule: ctyping2.induct)
  fix A X C C' Z Z' U c⇩1 c⇩2
  show
   "⟦⋀C C' Z Z'.
      (C, Z) = ⊢ c⇩1 (⊆ A, X) ⟹
      Some (C', Z') = (U, False) ⊨ c⇩1 (⊆ A, X) ⟹
      C' ⊆ C;
    ⋀p B Y C C' Z Z'. (U, False) ⊨ c⇩1 (⊆ A, X) = Some p ⟹
      (B, Y) = p ⟹ (C, Z) = ⊢ c⇩2 (⊆ B, Y) ⟹
      Some (C', Z') = (U, False) ⊨ c⇩2 (⊆ B, Y) ⟹
      C' ⊆ C;
    (C, Z) = ⊢ c⇩1;; c⇩2 (⊆ A, X);
    Some (C', Z') = (U, False) ⊨ c⇩1;; c⇩2 (⊆ A, X)⟧ ⟹
      C' ⊆ C"
    by (rule ctyping1_ctyping2_fst_seq)
next
  fix A X C C' Z Z' U b c⇩1 c⇩2
  show
   "⟦⋀U' p B⇩1 B⇩2 C C' Z Z'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B⇩1, B⇩2) = p ⟹ (C, Z) = ⊢ c⇩1 (⊆ B⇩1, X) ⟹
      Some (C', Z') = (U', False) ⊨ c⇩1 (⊆ B⇩1, X) ⟹
      C' ⊆ C;
    ⋀U' p B⇩1 B⇩2 C C' Z Z'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B⇩1, B⇩2) = p ⟹ (C, Z) = ⊢ c⇩2 (⊆ B⇩2, X) ⟹
      Some (C', Z') = (U', False) ⊨ c⇩2 (⊆ B⇩2, X) ⟹
      C' ⊆ C;
    (C, Z) = ⊢ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X);
    Some (C', Z') = (U, False) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X)⟧ ⟹
      C' ⊆ C"
    by (rule ctyping1_ctyping2_fst_if)
next
  fix A X B B' Z Z' U b c
  show
   "⟦⋀B⇩1 B⇩2 C Y B⇩1' B⇩2' B B' Z Z'.
      (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹
      (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: dom ` W ↝ UNIV ⟹
      (B, Z) = ⊢ c (⊆ B⇩1, X) ⟹
      Some (B', Z') = ({}, False) ⊨ c (⊆ B⇩1, X) ⟹
      B' ⊆ B;
    ⋀B⇩1 B⇩2 C Y B⇩1' B⇩2' B B' Z Z'.
      (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹
      (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: dom ` W ↝ UNIV ⟹
      (B, Z) = ⊢ c (⊆ B⇩1', Y) ⟹
      Some (B', Z') = ({}, False) ⊨ c (⊆ B⇩1', Y) ⟹
      B' ⊆ B;
    (B, Z) = ⊢ WHILE b DO c (⊆ A, X);
    Some (B', Z') = (U, False) ⊨ WHILE b DO c (⊆ A, X)⟧ ⟹
      B' ⊆ B"
    by (rule ctyping1_ctyping2_fst_while)
qed (simp add: ctyping1_def, auto)


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

lemma ctyping1_ctyping2_snd_seq:
  assumes
    A: "⋀B B' Y Y'. (B, Y) = ⊢ c⇩1 (⊆ A, X) ⟹
      Some (B', Y') = (U, False) ⊨ c⇩1 (⊆ A, X) ⟹ Y ⊆ Y'" and
    B: "⋀p B Y C C' Z Z'. (U, False) ⊨ c⇩1 (⊆ A, X) = Some p ⟹
      (B, Y) = p ⟹ (C, Z) = ⊢ c⇩2 (⊆ B, Y) ⟹
        Some (C', Z') = (U, False) ⊨ c⇩2 (⊆ B, Y) ⟹ Z ⊆ Z'" and
    C: "(C, Z) = ⊢ c⇩1;; c⇩2 (⊆ A, X)" and
    D: "Some (C', Z') = (U, False) ⊨ c⇩1;; c⇩2 (⊆ A, X)"
  shows "Z ⊆ Z'"
proof -
  let ?f = "foldl (;;) (λx. None)"
  let ?F = "λA S. {r. ∃f s. (∃t. r = (λx. case f x of
    None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i)) ∧
    (∃ys. f = ?f ys ∧ ys ∈ S) ∧ s ∈ A}"
  let ?G = "λX S. {x. ∀f ∈ {?f ys | ys. ys ∈ S}.
    f x ≠ Some None ∧ (f x = None ⟶ x ∈ X)}"
  {
    fix x B Y
    assume "⋀B' B'' C C' Z'. B = B' ⟹ B'' = B' ⟹ C = ?F B' (⊢ c⇩2) ⟹
      Some (C', Z') = (U, False) ⊨ c⇩2 (⊆ B', Y) ⟹
        Univ?? B' (?G Y (⊢ c⇩2)) ⊆ Z'" and
     "Some (C', Z') = (U, False) ⊨ c⇩2 (⊆ B, Y)"
    hence E: "Univ?? B (?G Y (⊢ c⇩2)) ⊆ Z'"
      by simp
    assume "⋀C B'. C = ?F A (⊢ c⇩1) ⟹ B' = B ⟹
      Univ?? A (?G X (⊢ c⇩1)) ⊆ Y"
    hence F: "Univ?? A (?G X (⊢ c⇩1)) ⊆ Y"
      by simp
    assume G: "∀f. (∃zs. f = ?f zs ∧ zs ∈ ⊢ c⇩1 ⊔⇩@ ⊢ c⇩2) ⟶
      f x ≠ Some None ∧ (f x = None ⟶ x ∈ X)"
    {
      fix ys
      have "⊢ c⇩1 ≠ {}"
        by (rule ctyping1_aux_nonempty)
      then obtain xs where "xs ∈ ⊢ c⇩1"
        by blast
      moreover assume "ys ∈ ⊢ c⇩2"
      ultimately have "xs @ ys ∈ ⊢ c⇩1 ⊔⇩@ ⊢ c⇩2"
        by (rule ctyping1_merge_append_in)
      moreover assume "?f ys x = Some None"
      hence "?f (xs @ ys) x = Some None"
        by (simp add: Let_def ctyping1_seq_last split: if_split_asm)
      ultimately have False
        using G by blast
    }
    hence H: "∀ys ∈ ⊢ c⇩2. ?f ys x ≠ Some None"
      by blast
    {
      fix xs ys
      assume "xs ∈ ⊢ c⇩1" and "ys ∈ ⊢ c⇩2"
      hence "xs @ ys ∈ ⊢ c⇩1 ⊔⇩@ ⊢ c⇩2"
        by (rule ctyping1_merge_append_in)
      moreover assume "?f xs x = Some None" and "?f ys x = None"
      hence "?f (xs @ ys) x = Some None"
        by (auto dest: last_in_set simp: Let_def ctyping1_seq_last
         split: if_split_asm)
      ultimately have "(∃ys ∈ ⊢ c⇩2. ?f ys x = None) ⟶
        (∀xs ∈ ⊢ c⇩1. ?f xs x ≠ Some None)"
        using G by blast
    }
    hence I: "(∃ys ∈ ⊢ c⇩2. ?f ys x = None) ⟶
      (∀xs ∈ ⊢ c⇩1. ?f xs x ≠ Some None)"
      by blast
    {
      fix xs ys
      assume "xs ∈ ⊢ c⇩1" and J: "ys ∈ ⊢ c⇩2"
      hence "xs @ ys ∈ ⊢ c⇩1 ⊔⇩@ ⊢ c⇩2"
        by (rule ctyping1_merge_append_in)
      moreover assume "?f xs x = None" and K: "?f ys x = None"
      hence "?f (xs @ ys) x = None"
        by (simp add: Let_def ctyping1_seq_last split: if_split_asm)
      ultimately have "x ∈ X"
        using G by blast
      moreover have "∀xs ∈ ⊢ c⇩1. ?f xs x ≠ Some None"
        using I and J and K by blast
      ultimately have "x ∈ Z'"
        using E and F and H by fastforce
    }
    moreover {
      fix ys
      assume "ys ∈ ⊢ c⇩2" and "?f ys x = None"
      hence "∀xs ∈ ⊢ c⇩1. ?f xs x ≠ Some None"
        using I by blast
      moreover assume "∀xs ∈ ⊢ c⇩1. ∃v. ?f xs x = Some v"
      ultimately have "x ∈ Z'"
        using E and F and H by fastforce
    }
    moreover {
      assume "∀ys ∈ ⊢ c⇩2. ∃v. ?f ys x = Some v"
      hence "x ∈ Z'"
        using E and H by fastforce
    }
    ultimately have "x ∈ Z'"
      by (cases "∃ys ∈ ⊢ c⇩2. ?f ys x = None",
       cases "∃xs ∈ ⊢ c⇩1. ?f xs x = None", auto)
    moreover assume "x ∉ Z'"
    ultimately have False
      by contradiction
  }
  note E = this
  from A and B and C and D show ?thesis
    by (auto dest: ctyping2_fst_empty ctyping2_fst_empty [OF sym]
     simp: ctyping1_def split: option.split_asm, erule_tac E)
qed

lemma ctyping1_ctyping2_snd_if:
  assumes
    A: "⋀U' p B⇩1 B⇩2 C⇩1 C⇩1' Y⇩1 Y⇩1'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B⇩1, B⇩2) = p ⟹ (C⇩1, Y⇩1) = ⊢ c⇩1 (⊆ B⇩1, X) ⟹
          Some (C⇩1', Y⇩1') = (U', False) ⊨ c⇩1 (⊆ B⇩1, X) ⟹ Y⇩1 ⊆ Y⇩1'" and
    B: "⋀U' p B⇩1 B⇩2 C⇩2 C⇩2' Y⇩2 Y⇩2'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
        (B⇩1, B⇩2) = p ⟹ (C⇩2, Y⇩2) = ⊢ c⇩2 (⊆ B⇩2, X) ⟹
          Some (C⇩2', Y⇩2') = (U', False) ⊨ c⇩2 (⊆ B⇩2, X) ⟹ Y⇩2 ⊆ Y⇩2'" and
    C: "(C, Y) = ⊢ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X)" and
    D: "Some (C', Y') = (U, False) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X)"
  shows "Y ⊆ Y'"
proof -
  let ?f = "foldl (;;) (λx. None)"
  let ?F = "λA S. {r. ∃f s. (∃t. r = (λx. case f x of
    None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i)) ∧
    (∃ys. f = ?f ys ∧ ys ∈ S) ∧ s ∈ A}"
  let ?G = "λX S. {x. ∀f ∈ {?f ys | ys. ys ∈ S}.
    f x ≠ Some None ∧ (f x = None ⟶ x ∈ X)}"
  let ?S⇩1 = "λf. if f = Some True ∨ f = None then ⊢ c⇩1 else {}"
  let ?S⇩2 = "λf. if f = Some False ∨ f = None then ⊢ c⇩2 else {}"
  let ?P = "λx. ∀f. (∃ys. f = ?f ys ∧ ys ∈ (let f = ⊢ b in ?S⇩1 f ⊔ ?S⇩2 f)) ⟶
    f x ≠ Some None ∧ (f x = None ⟶ x ∈ X)"
  let ?U = "insert (Univ? A X, bvars b) U"
  {
    fix B⇩1 B⇩2 Y⇩1' Y⇩2' and C⇩1' :: "state set" and C⇩2' :: "state set"
    assume "⋀U' B⇩1' C⇩1 C⇩1''. U' = ?U ⟹ B⇩1' = B⇩1 ⟹
      C⇩1 = ?F B⇩1 (⊢ c⇩1) ⟹ C⇩1'' = C⇩1' ⟹ Univ?? B⇩1 (?G X (⊢ c⇩1)) ⊆ Y⇩1'"
    hence E: "Univ?? B⇩1 (?G X (⊢ c⇩1)) ⊆ Y⇩1'"
      by simp
    moreover assume "⋀U' B⇩1' C⇩2 C⇩2''. U' = ?U ⟹ B⇩1' = B⇩1 ⟹
      C⇩2 = ?F B⇩2 (⊢ c⇩2) ⟹ C⇩2'' = C⇩2' ⟹ Univ?? B⇩2 (?G X (⊢ c⇩2)) ⊆ Y⇩2'"
    hence F: "Univ?? B⇩2 (?G X (⊢ c⇩2)) ⊆ Y⇩2'"
      by simp
    moreover assume G: "⊨ b (⊆ A, X) = (B⇩1, B⇩2)"
    moreover {
      fix x
      assume "?P x"
      have "x ∈ Y⇩1'"
      proof (cases "⊢ b = Some False")
        case True
        with E and G show ?thesis
          by (drule_tac btyping1_btyping2 [where A = A and X = X], auto)
      next
        case False
        {
          fix xs
          assume "xs ∈ ⊢ c⇩1"
          with False have "xs ∈ (let f = ⊢ b in ?S⇩1 f ⊔ ?S⇩2 f)"
            by (auto intro: ctyping1_merge_in simp: Let_def)
          hence "?f xs x ≠ Some None ∧ (?f xs x = None ⟶ x ∈ X)"
            using `?P x` by auto
        }
        hence "x ∈ Univ?? B⇩1 (?G X (⊢ c⇩1))"
          by auto
        thus ?thesis
          using E ..
      qed
    }
    moreover {
      fix x
      assume "?P x"
      have "x ∈ Y⇩2'"
      proof (cases "⊢ b = Some True")
        case True
        with F and G show ?thesis
          by (drule_tac btyping1_btyping2 [where A = A and X = X], auto)
      next
        case False
        {
          fix ys
          assume "ys ∈ ⊢ c⇩2"
          with False have "ys ∈ (let f = ⊢ b in ?S⇩1 f ⊔ ?S⇩2 f)"
            by (auto intro: ctyping1_merge_in simp: Let_def)
          hence "?f ys x ≠ Some None ∧ (?f ys x = None ⟶ x ∈ X)"
            using `?P x` by auto
        }
        hence "x ∈ Univ?? B⇩2 (?G X (⊢ c⇩2))"
          by auto
        thus ?thesis
          using F ..
      qed
    }
    ultimately have "(A = {} ⟶ UNIV ⊆ Y⇩1' ∧ UNIV ⊆ Y⇩2') ∧
      (A ≠ {} ⟶ {x. ?P x} ⊆ Y⇩1' ∧ {x. ?P x} ⊆ Y⇩2')"
      by (auto simp: btyping2_fst_empty)
  }
  note E = this
  from A and B and C and D show ?thesis
    by (clarsimp simp: ctyping1_def split: option.split_asm prod.split_asm,
     erule_tac E)
qed

lemma ctyping1_ctyping2_snd_while:
  assumes
    A: "(C, Y) = ⊢ WHILE b DO c (⊆ A, X)" and
    B: "Some (C', Y') = (U, False) ⊨ WHILE b DO c (⊆ A, X)"
  shows "Y ⊆ Y'"
proof -
  let ?f = "foldl (;;) (λx. None)"
  let ?F = "λA S. {r. ∃f s. (∃t. r = (λx. case f x of
    None ⇒ s x | Some None ⇒ t x | Some (Some i) ⇒ i)) ∧
    (∃ys. f = ?f ys ∧ ys ∈ S) ∧ s ∈ A}"
  let ?S⇩1 = "λf. if f = Some False ∨ f = None then {[]} else {}"
  let ?S⇩2 = "λf. if f = Some True ∨ f = None then ⊢ c else {}"
  let ?P = "λx. ∀f. (∃ys. f = ?f ys ∧ ys ∈ (let f = ⊢ b in ?S⇩1 f ∪ ?S⇩2 f)) ⟶
    f x ≠ Some None ∧ (f x = None ⟶ x ∈ X)"
  let ?Y = "λA. Univ?? A {x. ∀f ∈ {?f ys |ys. ys ∈ ⊢ c}.
    f x ≠ Some None ∧ (f x = None ⟶ x ∈ X)}"
  {
    fix B⇩1 B⇩2 B⇩1' B⇩2'
    assume C: "⊨ b (⊆ A, X) = (B⇩1, B⇩2)"
    assume "Some (C', Y') = (if (∀s ∈ Univ? A X ∪
      Univ? (?F B⇩1 (⊢ c)) (?Y B⇩1). ∀x ∈ bvars b. All (interf s (dom x))) ∧
      (∀p ∈ U. ∀B W. p = (B, W) ⟶ (∀s ∈ B. ∀x ∈ W. All (interf s (dom x))))
        then Some (B⇩2 ∪ B⇩2', Univ?? B⇩2 X ∩ ?Y B⇩1)
        else None)"
    hence D: "Y' = Univ?? B⇩2 X ∩ ?Y B⇩1"
      by (simp split: if_split_asm)
    {
      fix x
      assume "A = {}"
      hence "x ∈ Y'"
        using C and D by (simp add: btyping2_fst_empty)
    }
    moreover {
      fix x
      assume "?P x"
      {
        assume "⊢ b ≠ Some True"
        hence "[] ∈ (let f = ⊢ b in ?S⇩1 f ∪ ?S⇩2 f)"
          by (auto simp: Let_def)
        hence "x ∈ X"
          using `?P x` by auto
      }
      hence E: "⊢ b ≠ Some True ⟶ x ∈ Univ?? B⇩2 X"
        by auto
      {
        fix ys
        assume "⊢ b ≠ Some False" and "ys ∈ ⊢ c"
        hence "ys ∈ (let f = ⊢ b in ?S⇩1 f ∪ ?S⇩2 f)"
          by (auto simp: Let_def)
        hence "?f ys x ≠ Some None ∧ (?f ys x = None ⟶ x ∈ X)"
          using `?P x` by auto
      }
      hence F: "⊢ b ≠ Some False ⟶ x ∈ ?Y B⇩1"
        by auto
      have "x ∈ Y'"
      proof (cases "⊢ b")
        case None
        thus ?thesis
          using D and E and F by simp
      next
        case (Some v)
        show ?thesis
        proof (cases v)
          case True
          with C and D and F and Some show ?thesis
            by (drule_tac btyping1_btyping2 [where A = A and X = X], simp)
        next
          case False
          with C and D and E and Some show ?thesis
            by (drule_tac btyping1_btyping2 [where A = A and X = X], simp)
        qed
      qed
    }
    ultimately have "(A = {} ⟶ UNIV ⊆ Y') ∧ (A ≠ {} ⟶ {x. ?P x} ⊆ Y')"
      by auto
  }
  note C = this
  from A and B show ?thesis
    by (auto intro!: C simp: ctyping1_def
     split: option.split_asm prod.split_asm)
qed

lemma ctyping1_ctyping2_snd:
 "⟦(C, Z) = ⊢ c (⊆ A, X); Some (C', Z') = (U, False) ⊨ c (⊆ A, X)⟧ ⟹
    Z ⊆ Z'"
proof (induction "(U, False)" c A X arbitrary: C C' Z Z' U
 rule: ctyping2.induct)
  fix A X C C' Z Z' U c⇩1 c⇩2
  show
   "⟦⋀B B' Y Y'.
      (B, Y) = ⊢ c⇩1 (⊆ A, X) ⟹
      Some (B', Y') = (U, False) ⊨ c⇩1 (⊆ A, X) ⟹
      Y ⊆ Y';
    ⋀p B Y C C' Z Z'. (U, False) ⊨ c⇩1 (⊆ A, X) = Some p ⟹
      (B, Y) = p ⟹ (C, Z) = ⊢ c⇩2 (⊆ B, Y) ⟹
      Some (C', Z') = (U, False) ⊨ c⇩2 (⊆ B, Y) ⟹
      Z ⊆ Z';
    (C, Z) = ⊢ c⇩1;; c⇩2 (⊆ A, X);
    Some (C', Z') = (U, False) ⊨ c⇩1;; c⇩2 (⊆ A, X)⟧ ⟹
      Z ⊆ Z'"
    by (rule ctyping1_ctyping2_snd_seq)
next
  fix A X C C' Z Z' U b c⇩1 c⇩2
  show
   "⟦⋀U' p B⇩1 B⇩2 C C' Z Z'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B⇩1, B⇩2) = p ⟹ (C, Z) = ⊢ c⇩1 (⊆ B⇩1, X) ⟹
      Some (C', Z') = (U', False) ⊨ c⇩1 (⊆ B⇩1, X) ⟹
      Z ⊆ Z';
    ⋀U' p B⇩1 B⇩2 C C' Z Z'.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B⇩1, B⇩2) = p ⟹ (C, Z) = ⊢ c⇩2 (⊆ B⇩2, X) ⟹
      Some (C', Z') = (U', False) ⊨ c⇩2 (⊆ B⇩2, X) ⟹
      Z ⊆ Z';
    (C, Z) = ⊢ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X);
    Some (C', Z') = (U, False) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X)⟧ ⟹
      Z ⊆ Z'"
    by (rule ctyping1_ctyping2_snd_if)
next
  fix A X B B' Z Z' U b c
  show
   "⟦⋀B⇩1 B⇩2 C Y B⇩1' B⇩2' B B' Z Z'.
      (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹
      (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: dom ` W ↝ UNIV ⟹
      (B, Z) = ⊢ c (⊆ B⇩1, X) ⟹
      Some (B', Z') = ({}, False) ⊨ c (⊆ B⇩1, X) ⟹
      Z ⊆ Z';
    ⋀B⇩1 B⇩2 C Y B⇩1' B⇩2' B B' Z Z'.
      (B⇩1, B⇩2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B⇩1, X) ⟹
      (B⇩1', B⇩2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: dom ` W ↝ UNIV ⟹
      (B, Z) = ⊢ c (⊆ B⇩1', Y) ⟹
      Some (B', Z') = ({}, False) ⊨ c (⊆ B⇩1', Y) ⟹
      Z ⊆ Z';
    (B, Z) = ⊢ WHILE b DO c (⊆ A, X);
    Some (B', Z') = (U, False) ⊨ WHILE b DO c (⊆ A, X)⟧ ⟹
      Z ⊆ Z'"
    by (rule ctyping1_ctyping2_snd_while)
qed (simp add: ctyping1_def, auto)


lemma ctyping1_ctyping2:
 "⟦⊢ c (⊆ A, X) = (C, Z); (U, False) ⊨ c (⊆ A, X) = Some (C', Z')⟧ ⟹
    C' ⊆ C ∧ Z ⊆ Z'"
by (rule conjI, ((rule ctyping1_ctyping2_fst [OF sym sym] |
 rule ctyping1_ctyping2_snd [OF sym sym]), assumption+)+)


lemma btyping2_aux_approx_1 [elim]:
  assumes
    A: "⊫ b⇩1 (⊆ A, X) = Some B⇩1" and
    B: "⊫ b⇩2 (⊆ A, X) = Some B⇩2" and
    C: "bval b⇩1 s" and
    D: "bval b⇩2 s" and
    E: "r ∈ A" and
    F: "s = r (⊆ state ∩ X)"
  shows "∃r' ∈ B⇩1 ∩ B⇩2. r = r' (⊆ state ∩ X)"
proof -
  from A and C and E and F have "r ∈ B⇩1"
    by (frule_tac btyping2_aux_subset, drule_tac btyping2_aux_eq, auto)
  moreover from B and D and E and F have "r ∈ B⇩2"
    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 a⇩1 ⊆ state" and
    B: "avars a⇩2 ⊆ state" and
    C: "avars a⇩1 ⊆ X" and
    D: "avars a⇩2 ⊆ X" and
    E: "aval a⇩1 s < aval a⇩2 s" and
    F: "r ∈ A" and
    G: "s = r (⊆ state ∩ X)"
  shows "∃r'. r' ∈ A ∧ aval a⇩1 r' < aval a⇩2 r' ∧ r = r' (⊆ state ∩ X)"
proof -
  have "aval a⇩1 s = aval a⇩1 r ∧ aval a⇩2 s = aval a⇩2 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 a⇩1 ⊆ state" and
    B: "avars a⇩2 ⊆ state" and
    C: "avars a⇩1 ⊆ X" and
    D: "avars a⇩2 ⊆ X" and
    E: "¬ aval a⇩1 s < aval a⇩2 s" and
    F: "r ∈ A" and
    G: "s = r (⊆ state ∩ X)"
  shows "∃r' ∈ A - {s ∈ A. aval a⇩1 s < aval a⇩2 s}. r = r' (⊆ state ∩ X)"
proof -
  have "aval a⇩1 s = aval a⇩1 r ∧ aval a⇩2 s = aval a⇩2 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) = (B⇩1, B⇩2); s ∈ Univ A (⊆ state ∩ X)⟧ ⟹
    s ∈ Univ (if bval b s then B⇩1 else B⇩2) (⊆ 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) = (B⇩1, B⇩2); r ∈ A; s = r (⊆ state ∩ X);
    (insert (Univ? A X, bvars b) U, v) ⊨ c⇩1 (⊆ B⇩1, X) = Some (C⇩1, Y⇩1);
    ⋀A B X Y U v. (U, v) ⊨ c⇩1 (⊆ A, X) = Some (B, Y) ⟹
      ∃r ∈ A. s = r (⊆ state ∩ X) ⟹ ∃r' ∈ B. t = r' (⊆ state ∩ Y)⟧ ⟹
  ∃r' ∈ C⇩1 ∪ C⇩2. t = r' (⊆ state ∩ (Y⇩1 ∩ Y⇩2))"
by (drule btyping2_approx, blast, fastforce)

lemma ctyping2_approx_if_2:
 "⟦¬ bval b s; ⊨ b (⊆ A, X) = (B⇩1, B⇩2); r ∈ A; s = r (⊆ state ∩ X);
    (insert (Univ? A X, bvars b) U, v) ⊨ c⇩2 (⊆ B⇩2, X) = Some (C⇩2, Y⇩2);
    ⋀A B X Y U v. (U, v) ⊨ c⇩2 (⊆ A, X) = Some (B, Y) ⟹
      ∃r ∈ A. s = r (⊆ state ∩ X) ⟹ ∃r' ∈ B. t = r' (⊆ state ∩ Y)⟧ ⟹
  ∃r' ∈ C⇩1 ∪ C⇩2. t = r' (⊆ state ∩ (Y⇩1 ∩ Y⇩2))"
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 ∈ B⇩2 ∪ B⇩2'. ∃x ∈ state ∩ (X ∩ Y). r x ≠ t x; ¬ bval b s;
    r ∈ A; s = r (⊆ state ∩ X); ⊨ b (⊆ A, X) = (B⇩1, B⇩2)⟧ ⟹ False"
by (drule btyping2_approx, blast, auto)

lemma ctyping2_approx_while_aux:
  assumes
    A: "⊨ b (⊆ A, X) = (B⇩1, B⇩2)" and
    B: "⊢ c (⊆ B⇩1, X) = (C, Y)" and
    C: "⊨ b (⊆ C, Y) = (B⇩1', B⇩2')" and
    D: "({}, False) ⊨ c (⊆ B⇩1, X) = Some (D, Z)" and
    E: "({}, False) ⊨ c (⊆ B⇩1', Y) = Some (D', Z')" and
    F: "r⇩1 ∈ A" and
    G: "s⇩1 = r⇩1 (⊆ state ∩ X)" and
    H: "bval b s⇩1" and
    I: "⋀C B Y W U. (case ⊨ b (⊆ C, Y) of (B⇩1', B⇩2') ⇒
      case ⊢ c (⊆ B⇩1', Y) of (C', Y') ⇒
      case ⊨ b (⊆ C', Y') of (B⇩1'', B⇩2'') ⇒
        if (∀s ∈ Univ? C Y ∪ Univ? C' Y'. ∀x ∈ bvars b. All (interf s (dom x))) ∧
          (∀p ∈ U. case p of (B, W) ⇒ ∀s ∈ B. ∀x ∈ W. All (interf s (dom x)))
        then case ({}, False) ⊨ c (⊆ B⇩1', Y) of
          None ⇒ None | Some _ ⇒ case ({}, False) ⊨ c (⊆ B⇩1'', Y') of
            None ⇒ None | Some _ ⇒ Some (B⇩2' ∪ B⇩2'', Univ?? B⇩2' Y ∩ Y')
        else None) = Some (B, W) ⟹
          ∃r ∈ C. s⇩2 = r (⊆ state ∩ Y) ⟹ ∃r ∈ B. s⇩3 = 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. s⇩1 = r (⊆ state ∩ X) ⟹ ∃r ∈ B. s⇩2 = r (⊆ state ∩ Y)" and
    K: "∀s ∈ Univ? A X ∪ Univ? C Y. ∀x ∈ bvars b. All (interf s (dom x))" and
    L: "∀p ∈ U. ∀B W. p  = (B, W) ⟶
      (∀s ∈ B. ∀x ∈ W. All (interf s (dom x)))"
  shows "∃r ∈ B⇩2 ∪ B⇩2'. s⇩3 = r (⊆ state ∩ Univ?? B⇩2 X ∩ Y)"
proof -
  obtain C' Y' where M: "(C', Y') = ⊢ c (⊆ B⇩1', Y)"
    by (cases "⊢ c (⊆ B⇩1', Y)", simp)
  obtain B⇩1'' B⇩2'' where N: "(B⇩1'', B⇩2'') = ⊨ b (⊆ C', Y')"
    by (cases "⊨ b (⊆ C', Y')", simp)
  let ?B = "B⇩2' ∪ B⇩2''"
  let ?W = "Univ?? B⇩2' Y ∩ Y'"
  have "(C, Y) = ⊢ c (⊆ C, Y)"
    using ctyping1_idem and B by auto
  moreover have "B⇩1' ⊆ 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. s⇩2 = r (⊆ state ∩ Y) ⟹ ∃r ∈ ?B. s⇩3 = r (⊆ state ∩ ?W)" .
  ultimately have "(case ({}, False) ⊨ c (⊆ B⇩1'', Y') of
    None ⇒ None | Some _ ⇒ Some (?B, ?W)) = Some (?B, ?W) ⟹
      ∃r ∈ C. s⇩2 = r (⊆ state ∩ Y) ⟹ ∃r ∈ ?B. s⇩3 = 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: "B⇩1'' ⊆ B⇩1' ∧ B⇩2'' ⊆ B⇩2'"
    by (metis btyping2_mono C N O)
  hence "∃D'' Z''. ({}, False) ⊨ c (⊆ B⇩1'', Y') =
    Some (D'', Z'') ∧ D'' ⊆ D' ∧ Z' ⊆ Z''"
    using E and O by (auto intro: ctyping2_mono)
  ultimately have
   "∃r ∈ C. s⇩2 = r (⊆ state ∩ Y) ⟹ ∃r ∈ ?B. s⇩3 = r (⊆ state ∩ ?W)"
    by fastforce
  moreover from A and D and F and G and H and J obtain r⇩2 where
   "r⇩2 ∈ D" and "s⇩2 = r⇩2 (⊆ 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 r⇩3 where Q: "r⇩3 ∈ ?B" and R: "s⇩3 = r⇩3 (⊆ state ∩ ?W)"
    by blast
  show ?thesis
  proof (rule bexI [of _ r⇩3])
    show "s⇩3 = r⇩3 (⊆ state ∩ Univ?? B⇩2 X ∩ Y)"
      using O and R by auto
  next
    show "r⇩3 ∈ B⇩2 ∪ B⇩2'"
      using P and Q by blast
  qed
qed

lemmas ctyping2_approx_while_3 =
  ctyping2_approx_while_aux [where B⇩2 = "{}", simplified]

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

lemma ctyping2_approx:
 "⟦(c, s) ⇒ t; (U, v) ⊨ c (⊆ A, X) = Some (B, Y);
    s ∈ Univ A (⊆ state ∩ X)⟧ ⟹ t ∈ Univ B (⊆ state ∩ Y)"
proof (induction arbitrary: A B X Y U v rule: big_step_induct)
  fix A B X Y U v b c⇩1 c⇩2 s t
  show
   "⟦bval b s; (c⇩1, s) ⇒ t;
    ⋀A C X Y U v. (U, v) ⊨ c⇩1 (⊆ A, X) = Some (C, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹
      t ∈ Univ C (⊆ state ∩ Y);
    (U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ 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 c⇩1 c⇩2 s t
  show
   "⟦¬ bval b s; (c⇩2, s) ⇒ t;
    ⋀A C X Y U v. (U, v) ⊨ c⇩2 (⊆ A, X) = Some (C, Y) ⟹
      s ∈ Univ A (⊆ state ∩ X) ⟹
      t ∈ Univ C (⊆ state ∩ Y);
    (U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ 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 s⇩1 s⇩2 s⇩3
  show
   "⟦bval b s⇩1; (c, s⇩1) ⇒ s⇩2;
    ⋀A B X Y U v. (U, v) ⊨ c (⊆ A, X) = Some (B, Y) ⟹
      s⇩1 ∈ Univ A (⊆ state ∩ X) ⟹
      s⇩2 ∈ Univ B (⊆ state ∩ Y);
    (WHILE b DO c, s⇩2) ⇒ s⇩3;
    ⋀A B X Y U v. (U, v) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Y) ⟹
      s⇩2 ∈ Univ A (⊆ state ∩ X) ⟹
      s⇩3 ∈ Univ B (⊆ state ∩ Y);
    (U, v) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Y);
    s⇩1 ∈ Univ A (⊆ state ∩ X)⟧ ⟹
      s⇩3 ∈ 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