# Theory DefiniteAssignment

Up to index of Isabelle/HOL/Bali

theory DefiniteAssignment
imports WellType
begin

    header {* Definite Assignment *}

    theory DefiniteAssignment imports WellType begin

    text {* Definite Assignment Analysis (cf. 16)

    The definite assignment analysis approximates the sets of local
    variables that will be assigned at a certain point of evaluation, and ensures
    that we will only read variables which previously were assigned.
    It should conform to the following idea:
     If the evaluation of a term completes normally (no abruption (exception,
    break, continue, return) appeared) , the set of local variables calculated
    by the analysis is a subset of the
    variables that were actually assigned during evaluation.

    To get more precise information about the sets of assigned variables the
    analysis includes the following optimisations:
    \begin{itemize}
      \item Inside of a while loop we also take care of the variables assigned
            before break statements, since the break causes the while loop to
            continue normally.
      \item For conditional statements we take care of constant conditions to
            statically determine the path of evaluation.
      \item Inside a distinct path of a conditional statements we know to which
            boolean value the condition has evaluated to, and so can retrieve more
            information about the variables assigned during evaluation of the
            boolean condition.
    \end{itemize}

    Since in our model of Java the return values of methods are stored in a local
    variable we also ensure that every path of (normal) evaluation will assign the
    result variable, or in the sense of real Java every path ends up in and
    return instruction.

    Not covered yet:
    \begin{itemize}
      \item analysis of definite unassigned
      \item special treatment of final fields
    \end{itemize}
    *}

    section {* Correct nesting of jump statements *}

    text {* For definite assignment it becomes crucial, that jumps (break,
    continue, return) are nested correctly i.e. a continue jump is nested in a
    matching while statement, a break jump is nested in a proper label statement,
    a class initialiser does not terminate abruptly with a return. With this we
    can for example ensure that evaluation of an expression will never end up
    with a jump, since no breaks, continues or returns are allowed in an
    expression. *}

    consts jumpNestingOkS :: "jump set => stmt => bool"
    primrec
    "jumpNestingOkS jmps (Skip)   = True"
    "jumpNestingOkS jmps (Expr e) = True"
    "jumpNestingOkS jmps (j• s) = jumpNestingOkS ({j} ∪ jmps) s"
    "jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 ∧
                                     jumpNestingOkS jmps c2)"
    "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 ∧
                                               jumpNestingOkS jmps c2)"
    "jumpNestingOkS jmps (l• While(e) c) = jumpNestingOkS ({Cont l} ∪ jmps) c"
    --{* The label of the while loop only handles continue jumps. Breaks are only
         handled by @{term Lab} *}
    "jumpNestingOkS jmps (Jmp j) = (j ∈ jmps)"
    "jumpNestingOkS jmps (Throw e) = True"
    "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 ∧
                                                    jumpNestingOkS jmps c2)"
    "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 ∧
                                            jumpNestingOkS jmps c2)"
    "jumpNestingOkS jmps (Init C) = True"
     --{* wellformedness of the program must enshure that for all initializers
          jumpNestingOkS {} holds *}
    --{* Dummy analysis for intermediate smallstep term @{term  FinA} *}
    "jumpNestingOkS jmps (FinA a c) = False"

    constdefs jumpNestingOk :: "jump set => term => bool"
    "jumpNestingOk jmps t ≡ (case t of
                          In1 se => (case se of
                                       Inl e => True
                                     | Inr s => jumpNestingOkS jmps s)
                        | In2  v => True
                        | In3  es => True)"

    lemma jumpNestingOk_expr_simp [simp]: "jumpNestingOk jmps (In1l e) = True"
    by (simp add: jumpNestingOk_def)

    lemma jumpNestingOk_expr_simp1 [simp]: "jumpNestingOk jmps ⟨e::expr⟩ = True"
    by (simp add: inj_term_simps)

    lemma jumpNestingOk_stmt_simp [simp]:
      "jumpNestingOk jmps (In1r s) = jumpNestingOkS jmps s"
    by (simp add: jumpNestingOk_def)

    lemma jumpNestingOk_stmt_simp1 [simp]:
       "jumpNestingOk jmps ⟨s::stmt⟩ = jumpNestingOkS jmps s"
    by (simp add: inj_term_simps)

    lemma jumpNestingOk_var_simp [simp]: "jumpNestingOk jmps (In2 v) = True"
    by (simp add: jumpNestingOk_def)

    lemma jumpNestingOk_var_simp1 [simp]: "jumpNestingOk jmps ⟨v::var⟩ = True"
    by (simp add: inj_term_simps)

    lemma jumpNestingOk_expr_list_simp [simp]: "jumpNestingOk jmps (In3 es) = True"
    by (simp add: jumpNestingOk_def)

    lemma jumpNestingOk_expr_list_simp1 [simp]:
      "jumpNestingOk jmps ⟨es::expr list⟩ = True"
    by (simp add: inj_term_simps)

    section {* Calculation of assigned variables for boolean expressions*}

    subsection {* Very restricted calculation fallback calculation *}

    consts the_LVar_name:: "var => lname"
    primrec
    "the_LVar_name (LVar n) = n"

    consts assignsE :: "expr      => lname set"
           assignsV :: "var       => lname set"
           assignsEs:: "expr list => lname set"
    text {* *}
    primrec
    "assignsE (NewC c)            = {}"
    "assignsE (NewA t e)          = assignsE e"
    "assignsE (Cast t e)          = assignsE e"
    "assignsE (e InstOf r)        = assignsE e"
    "assignsE (Lit val)           = {}"
    "assignsE (UnOp unop e)       = assignsE e"
    "assignsE (BinOp binop e1 e2) = (if binop=CondAnd ∨ binop=CondOr
                                         then (assignsE e1)
                                         else (assignsE e1) ∪ (assignsE e2))"
    "assignsE (Super)             = {}"
    "assignsE (Acc v)             = assignsV v"
    "assignsE (v:=e)              = (assignsV v) ∪ (assignsE e) ∪
                                     (if ∃ n. v=(LVar n) then {the_LVar_name v}
                                                         else {})"
    "assignsE (b? e1 : e2) = (assignsE b) ∪ ((assignsE e1) ∩ (assignsE e2))"
    "assignsE ({accC,statT,mode}objRef·mn({pTs}args))
                              = (assignsE objRef) ∪ (assignsEs args)"
    -- {* Only dummy analysis for intermediate expressions
          @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
    "assignsE (Methd C sig)   = {}"
    "assignsE (Body  C s)     = {}"
    "assignsE (InsInitE s e)  = {}"
    "assignsE (Callee l e)    = {}"

    "assignsV (LVar n)       = {}"
    "assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
    "assignsV (e1.[e2])      = assignsE e1 ∪ assignsE e2"

    "assignsEs     [] = {}"
    "assignsEs (e#es) = assignsE e ∪ assignsEs es"

    constdefs assigns:: "term => lname set"
    "assigns t ≡ (case t of
                    In1 se => (case se of
                                 Inl e => assignsE e
                               | Inr s => {})
                  | In2  v => assignsV v
                  | In3  es => assignsEs es)"

    lemma assigns_expr_simp [simp]: "assigns (In1l e) = assignsE e"
    by (simp add: assigns_def)

    lemma assigns_expr_simp1 [simp]: "assigns (⟨e⟩) = assignsE e"
    by (simp add: inj_term_simps)

    lemma assigns_stmt_simp [simp]: "assigns (In1r s) = {}"
    by (simp add: assigns_def)

    lemma assigns_stmt_simp1 [simp]: "assigns (⟨s::stmt⟩) = {}"
    by (simp add: inj_term_simps)

    lemma assigns_var_simp [simp]: "assigns (In2 v) = assignsV v"
    by (simp add: assigns_def)

    lemma assigns_var_simp1 [simp]: "assigns (⟨v⟩) = assignsV v"
    by (simp add: inj_term_simps)

    lemma assigns_expr_list_simp [simp]: "assigns (In3 es) = assignsEs es"
    by (simp add: assigns_def)

    lemma assigns_expr_list_simp1 [simp]: "assigns (⟨es⟩) = assignsEs es"
    by (simp add: inj_term_simps)

    subsection "Analysis of constant expressions"

    consts constVal :: "expr => val option"
    primrec
    "constVal (NewC c)      = None"
    "constVal (NewA t e)    = None"
    "constVal (Cast t e)    = None"
    "constVal (Inst e r)    = None"
    "constVal (Lit val)     = Some val"
    "constVal (UnOp unop e) = (case (constVal e) of
                                 None   => None
                               | Some v => Some (eval_unop unop v))"
    "constVal (BinOp binop e1 e2) = (case (constVal e1) of
                                       None    => None
                                     | Some v1 => (case (constVal e2) of
                                                    None    => None
                                                  | Some v2 => Some (eval_binop
                                                                     binop v1 v2)))"
    "constVal (Super)         = None"
    "constVal (Acc v)         = None"
    "constVal (Ass v e)       = None"
    "constVal (Cond b e1 e2)  = (case (constVal b) of
                                   None   => None
                                 | Some bv=> (case the_Bool bv of
                                                True => (case (constVal e2) of
                                                           None   => None
                                                         | Some v => constVal e1)
                                              | False=> (case (constVal e1) of
                                                           None   => None
                                                         | Some v => constVal e2)))"
    --{* Note that @{text "constVal (Cond b e1 e2)"} is stricter as it could be.
         It requires that all tree expressions are constant even if we can decide
         which branch to choose, provided the constant value of @{term b} *}
    "constVal (Call accC statT mode objRef mn pTs args) = None"
    "constVal (Methd C sig)   = None"
    "constVal (Body  C s)     = None"
    "constVal (InsInitE s e)  = None"
    "constVal (Callee l e)    = None"

    lemma constVal_Some_induct [consumes 1, case_names Lit UnOp BinOp CondL CondR]:
      assumes const: "constVal e = Some v" and
            hyp_Lit: "!! v. P (Lit v)" and
           hyp_UnOp: "!! unop e'. P e' ==> P (UnOp unop e')" and
          hyp_BinOp: "!! binop e1 e2. [|P e1; P e2|] ==> P (BinOp binop e1 e2)" and
          hyp_CondL: "!! b bv e1 e2. [|constVal b = Some bv; the_Bool bv; P b; P e1|]
                                  ==> P (b? e1 : e2)" and
          hyp_CondR: "!! b bv e1 e2. [|constVal b = Some bv; ¬the_Bool bv; P b; P e2|]
                                  ==> P (b? e1 : e2)"
      shows "P e"
    proof -
      have "True" and "!! v. constVal e = Some v ==> P e" and "True" and "True"
      proof (induct "x::var" and e and "s::stmt" and "es::expr list")
        case Lit
        show ?case by (rule hyp_Lit)
      next
        case UnOp
        thus ?case
          by (auto intro: hyp_UnOp)
      next
        case BinOp
        thus ?case
          by (auto intro: hyp_BinOp)
      next
        case (Cond b e1 e2)
        then obtain v where   v: "constVal (b ? e1 : e2) = Some v"
          by blast
        then obtain bv where bv: "constVal b = Some bv"
          by simp
        show ?case
        proof (cases "the_Bool bv")
          case True
          with Cond show ?thesis using v bv
            by (auto intro: hyp_CondL)
        next
          case False
          with Cond show ?thesis using v bv
            by (auto intro: hyp_CondR)
        qed
      qed (simp_all)
      with const
      show ?thesis
        by blast
    qed

    lemma assignsE_const_simp: "constVal e = Some v ==> assignsE e = {}"
      by (induct rule: constVal_Some_induct) simp_all

    subsection {* Main analysis for boolean expressions *}

    text {* Assigned local variables after evaluating the expression if it evaluates
    to a specific boolean value. If the expression cannot evaluate to a
    @{term Boolean} value UNIV is returned. If we expect true/false the opposite
    constant false/true will also lead to UNIV. *}
    consts assigns_if:: "bool => expr => lname set"
    primrec
    "assigns_if b (NewC c)            = UNIV" --{*can never evaluate to Boolean*}
    "assigns_if b (NewA t e)          = UNIV" --{*can never evaluate to Boolean*}
    "assigns_if b (Cast t e)          = assigns_if b e"
    "assigns_if b (Inst e r)          = assignsE e" --{*Inst has type Boolean but
                                                         e is a reference type*}
    "assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"
    "assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
                                             None   => (if unop = UNot
                                                           then assigns_if (¬b) e
                                                           else UNIV)
                                           | Some v => (if v=Bool b
                                                           then {}
                                                           else UNIV))"
    "assigns_if b (BinOp binop e1 e2)
      = (case constVal (BinOp binop e1 e2) of
           None => (if binop=CondAnd then
                       (case b of
                           True  => assigns_if True  e1 ∪ assigns_if True e2
                        |  False => assigns_if False e1 ∩
                                    (assigns_if True e1 ∪ assigns_if False e2))
                    else
                   (if binop=CondOr then
                       (case b of
                           True  => assigns_if True e1 ∩
                                    (assigns_if False e1 ∪ assigns_if True e2)
                        |  False => assigns_if False  e1 ∪ assigns_if False e2)
                    else assignsE e1 ∪ assignsE e2))
         | Some v => (if v=Bool b then {} else UNIV))"

    "assigns_if b (Super)      = UNIV" --{*can never evaluate to Boolean*}
    "assigns_if b (Acc v)      = (assignsV v)"
    "assigns_if b (v := e)     = (assignsE (Ass v e))"
    "assigns_if b (c? e1 : e2) = (assignsE c) ∪
                                   (case (constVal c) of
                                      None    => (assigns_if b e1) ∩
                                                 (assigns_if b e2)
                                    | Some bv => (case the_Bool bv of
                                                    True  => assigns_if b e1
                                                  | False => assigns_if b e2))"
    "assigns_if b ({accC,statT,mode}objRef·mn({pTs}args))
              = assignsE ({accC,statT,mode}objRef·mn({pTs}args)) "
    -- {* Only dummy analysis for intermediate expressions
          @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
    "assigns_if b (Methd C sig)   = {}"
    "assigns_if b (Body  C s)     = {}"
    "assigns_if b (InsInitE s e)  = {}"
    "assigns_if b (Callee l e)    = {}"

    lemma assigns_if_const_b_simp:
      assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")
      shows   "assigns_if b e = {}" (is "?Ass b e")
    proof -
      have "True" and "!! b. ?Const b e ==> ?Ass b e" and "True" and "True"
      proof (induct _ and e and _ and _ rule: var_expr_stmt.induct)
        case Lit
        thus ?case by simp
      next
        case UnOp
        thus ?case by simp
      next
        case (BinOp binop)
        thus ?case
          by (cases binop) (simp_all)
      next
        case (Cond c e1 e2 b)
        have hyp_c:  "!! b. ?Const b c ==> ?Ass b c" .
        have hyp_e1: "!! b. ?Const b e1 ==> ?Ass b e1" .
        have hyp_e2: "!! b. ?Const b e2 ==> ?Ass b e2" .
        have const: "constVal (c ? e1 : e2) = Some (Bool b)" .
        then obtain bv where bv: "constVal c = Some bv"
          by simp
        hence emptyC: "assignsE c = {}" by (rule assignsE_const_simp)
        show ?case
        proof (cases "the_Bool bv")
          case True
          with const bv
          have "?Const b e1" by simp
          hence "?Ass b e1" by (rule hyp_e1)
          with emptyC bv True
          show ?thesis
            by simp
        next
          case False
          with const bv
          have "?Const b e2" by simp
          hence "?Ass b e2" by (rule hyp_e2)
          with emptyC bv False
          show ?thesis
            by simp
        qed
      qed (simp_all)
      with boolConst
      show ?thesis
        by blast
    qed

    lemma assigns_if_const_not_b_simp:
      assumes boolConst: "constVal e = Some (Bool b)"        (is "?Const b e")
        shows "assigns_if (¬b) e = UNIV"                    (is "?Ass b e")
    proof -
      have True and "!! b. ?Const b e ==> ?Ass b e" and True and True
      proof (induct _ and e and _ and _ rule: var_expr_stmt.induct)
        case Lit
        thus ?case by simp
      next
        case UnOp
        thus ?case by simp
      next
        case (BinOp binop)
        thus ?case
          by (cases binop) (simp_all)
      next
        case (Cond c e1 e2 b)
        have hyp_c:  "!! b. ?Const b c ==> ?Ass b c" .
        have hyp_e1: "!! b. ?Const b e1 ==> ?Ass b e1" .
        have hyp_e2: "!! b. ?Const b e2 ==> ?Ass b e2" .
        have const: "constVal (c ? e1 : e2) = Some (Bool b)" .
        then obtain bv where bv: "constVal c = Some bv"
          by simp
        show ?case
        proof (cases "the_Bool bv")
          case True
          with const bv
          have "?Const b e1" by simp
          hence "?Ass b e1" by (rule hyp_e1)
          with bv True
          show ?thesis
            by simp
        next
          case False
          with const bv
          have "?Const b e2" by simp
          hence "?Ass b e2" by (rule hyp_e2)
          with bv False
          show ?thesis
            by simp
        qed
      qed (simp_all)
      with boolConst
      show ?thesis
        by blast
    qed

    subsection {* Lifting set operations to range of tables (map to a set) *}

    constdefs
     union_ts:: "('a,'b) tables => ('a,'b) tables => ('a,'b) tables"
                        ("_ =>∪ _" [67,67] 65)
     "A =>∪ B ≡ λ k. A k ∪ B k"

    constdefs
     intersect_ts:: "('a,'b) tables => ('a,'b) tables => ('a,'b) tables"
                        ("_ =>∩  _" [72,72] 71)
     "A =>∩  B ≡ λ k. A k ∩ B k"

    constdefs
     all_union_ts:: "('a,'b) tables => 'b set => ('a,'b) tables"
                                                         (infixl "=>∪∀" 40)
    "A =>∪∀ B ≡ λ k. A k ∪ B"

    subsubsection {* Binary union of tables *}

    lemma union_ts_iff [simp]: "(c ∈ (A =>∪ B) k) = (c ∈ A k ∨  c ∈ B k)"
      by (unfold union_ts_def) blast

    lemma union_tsI1 [elim?]: "c ∈ A k ==> c ∈ (A =>∪ B) k"
      by simp

    lemma union_tsI2 [elim?]: "c ∈ B k ==> c ∈ (A =>∪ B) k"
      by simp

    lemma union_tsCI [intro!]: "(c ∉ B k ==> c ∈ A k) ==> c ∈ (A =>∪ B) k"
      by auto

    lemma union_tsE [elim!]:
     "[|c ∈ (A =>∪ B) k; (c ∈ A k ==> P); (c ∈ B k ==> P)|] ==> P"
      by (unfold union_ts_def) blast

    subsubsection {* Binary intersection of tables *}

    lemma intersect_ts_iff [simp]: "c ∈ (A =>∩ B) k = (c ∈ A k ∧ c ∈ B k)"
      by (unfold intersect_ts_def) blast

    lemma intersect_tsI [intro!]: "[|c ∈ A k; c ∈ B k|] ==> c ∈  (A =>∩ B) k"
      by simp

    lemma intersect_tsD1: "c ∈ (A =>∩ B) k ==> c ∈ A k"
      by simp

    lemma intersect_tsD2: "c ∈ (A =>∩ B) k ==> c ∈ B k"
      by simp

    lemma intersect_tsE [elim!]:
       "[|c ∈ (A =>∩ B) k; [|c ∈ A k; c ∈ B k|] ==> P|] ==> P"
      by simp

    subsubsection {* All-Union of tables and set *}

    lemma all_union_ts_iff [simp]: "(c ∈ (A =>∪∀ B) k) = (c ∈ A k ∨  c ∈ B)"
      by (unfold all_union_ts_def) blast

    lemma all_union_tsI1 [elim?]: "c ∈ A k ==> c ∈ (A =>∪∀ B) k"
      by simp

    lemma all_union_tsI2 [elim?]: "c ∈ B ==> c ∈ (A =>∪∀ B) k"
      by simp

    lemma all_union_tsCI [intro!]: "(c ∉ B ==> c ∈ A k) ==> c ∈ (A =>∪∀ B) k"
      by auto

    lemma all_union_tsE [elim!]:
     "[|c ∈ (A =>∪∀ B) k; (c ∈ A k ==> P); (c ∈ B ==> P)|] ==> P"
      by (unfold all_union_ts_def) blast

    section "The rules of definite assignment"

    types breakass = "(label, lname) tables"
    --{* Mapping from a break label, to the set of variables that will be assigned
         if the evaluation terminates with this break *}

    record assigned =
             nrm :: "lname set" --{* Definetly assigned variables
                                     for normal completion*}
             brk :: "breakass" --{* Definetly assigned variables for
                                    abrupt completion with a break *}

    consts da :: "(env × lname set × term × assigned) set"
    text {* The environment @{term env} is only needed for the
            conditional @{text "_ ? _ : _"}.
            The definite assignment rules refer to the typing rules here to
            distinguish boolean and other expressions.
          *}

    syntax
    da :: "env => lname set => term => assigned => bool"
                               ("_\<turnstile> _ »_» _" [65,65,65,65] 71)

    translations
      "E\<turnstile> B »t» A" == "(E,B,t,A) ∈ da"

    text {* @{text B}: the ''assigned'' variables before evaluating term @{text t};
            @{text A}: the ''assigned'' variables after evaluating term @{text t}
    *}

    constdefs rmlab :: "'a => ('a,'b) tables => ('a,'b) tables"
    "rmlab k A ≡ λ x. if x=k then UNIV else A x"

    (*
    constdefs setbrk :: "breakass => assigned => breakass set"
    "setbrk b A ≡ {b} ∪ {a| a. a∈ brk A ∧ lab a ≠ lab b}"
    *)

    constdefs range_inter_ts :: "('a,'b) tables => 'b set" ("=>\<Inter>_" 80)
     "=>\<Inter>A ≡ {x |x. ∀ k. x ∈ A k}"

    inductive "da" intros

     Skip: "Env\<turnstile> B »⟨Skip⟩» (|nrm=B,brk=λ l. UNIV|)),"

     Expr: "Env\<turnstile> B »⟨e⟩» A
            ==>
            Env\<turnstile> B »⟨Expr e⟩» A"
     Lab:  "[|Env\<turnstile> B »⟨c⟩» C; nrm A = nrm C ∩ (brk C) l; brk A = rmlab l (brk C)|]
            ==>
            Env\<turnstile> B »⟨Break l• c⟩» A"

     Comp: "[|Env\<turnstile> B »⟨c1⟩» C1; Env\<turnstile> nrm C1 »⟨c2⟩» C2;
            nrm A = nrm C2; brk A = (brk C1) =>∩ (brk C2)|]
            ==>
            Env\<turnstile> B »⟨c1;; c2⟩» A"

     If:   "[|Env\<turnstile> B »⟨e⟩» E;
             Env\<turnstile> (B ∪ assigns_if True  e) »⟨c1⟩» C1;
             Env\<turnstile> (B ∪ assigns_if False e) »⟨c2⟩» C2;
             nrm A = nrm C1 ∩ nrm C2;
             brk A = brk C1 =>∩ brk C2 |]
             ==>
             Env\<turnstile> B »⟨If(e) c1 Else c2⟩» A"

    --{* Note that @{term E} is not further used, because we take the specialized
         sets that also consider if the expression evaluates to true or false.
         Inside of @{term e} there is no {\tt break} or {\tt finally}, so the break
         map of @{term E} will be the trivial one. So
         @{term "Env\<turnstile>B »⟨e⟩» E"} is just used to enshure the definite assignment in
         expression @{term e}.
         Notice the implicit analysis of a constant boolean expression @{term e}
         in this rule. For example, if @{term e} is constantly @{term True} then
         @{term "assigns_if False e = UNIV"} and therefor @{term "nrm C2=UNIV"}.
         So finally @{term "nrm A = nrm C1"}. For the break maps this trick
         workd too, because the trival break map will map all labels to
         @{term UNIV}. In the example, if no break occurs in @{term c2} the break
         maps will trivially map to @{term UNIV} and if a break occurs it will map
         to @{term UNIV} too, because @{term "assigns_if False e = UNIV"}. So
         in the intersection of the break maps the path @{term c2} will have no
         contribution.
      *}

     Loop: "[|Env\<turnstile> B »⟨e⟩» E;
             Env\<turnstile> (B ∪ assigns_if True e) »⟨c⟩» C;
             nrm A = nrm C ∩ (B ∪ assigns_if False e);
             brk A = brk C|]
             ==>
             Env\<turnstile> B »⟨l• While(e) c⟩» A"
    --{* The @{text Loop} rule resembles some of the ideas of the @{text If} rule.
         For the @{term "nrm A"} the set @{term "B ∪ assigns_if False e"}
         will be @{term UNIV} if the condition is constantly true. To normally exit
         the while loop, we must consider the body @{term c} to be completed
         normally (@{term "nrm C"}) or with a break. But in this model,
         the label @{term l} of the loop
         only handles continue labels, not break labels. The break label will be
         handled by an enclosing @{term Lab} statement. So we don't have to
         handle the breaks specially.
      *}

     Jmp: "[|jump=Ret --> Result ∈ B;
            nrm A = UNIV;
            brk A = (case jump of
                       Break l => λ k. if k=l then B else UNIV
                     | Cont l  => λ k. UNIV
                     | Ret     => λ k. UNIV)|]
           ==>
           Env\<turnstile> B »⟨Jmp jump⟩» A"
    --{* In case of a break to label @{term l} the corresponding break set is all
         variables assigned before the break. The assigned variables for normal
         completion of the @{term Jmp} is @{term UNIV}, because the statement will
         never complete normally. For continue and return the break map is the
         trivial one. In case of a return we enshure that the result value is
         assigned.
      *}

     Throw: "[|Env\<turnstile> B »⟨e⟩» E; nrm A = UNIV; brk A = (λ l. UNIV)|]
            ==> Env\<turnstile> B »⟨Throw e⟩» A"

     Try:  "[|Env\<turnstile> B »⟨c1⟩» C1;
             Env(|lcl := lcl Env(VName vn\<mapsto>Class C)|)),\<turnstile> (B ∪ {VName vn}) »⟨c2⟩» C2;
             nrm A = nrm C1 ∩ nrm C2;
             brk A = brk C1 =>∩ brk C2|]
            ==> Env\<turnstile> B »⟨Try c1 Catch(C vn) c2⟩» A"

     Fin:  "[|Env\<turnstile> B »⟨c1⟩» C1;
             Env\<turnstile> B »⟨c2⟩» C2;
             nrm A = nrm C1 ∪ nrm C2;
             brk A = ((brk C1) =>∪∀ (nrm C2)) =>∩ (brk C2)|]
             ==>
             Env\<turnstile> B »⟨c1 Finally c2⟩» A"
    --{* The set of assigned variables before execution @{term c2} are the same
         as before execution @{term c1}, because @{term c1} could throw an exception
         and so we can't guarantee that any variable will be assigned in @{term c1}.
         The @{text Finally} statement completes
         normally if both @{term c1} and @{term c2} complete normally. If @{term c1}
         completes abruptly with a break, then @{term c2} also will be executed
         and may terminate normally or with a break. The overall break map then is
         the intersection of the maps of both paths. If @{term c2} terminates
         normally we have to extend all break sets in @{term "brk C1"} with
         @{term "nrm C2"} (@{text "=>∪∀"}). If @{term c2} exits with a break this
         break will appear in the overall result state. We don't know if
         @{term c1} completed normally or abruptly (maybe with an exception not only
         a break) so @{term c1} has no contribution to the break map following this
         path.
      *}

    --{* Evaluation of expressions and the break sets of definite assignment:
         Thinking of a Java expression we assume that we can never have
         a break statement inside of a expression. So for all expressions the
         break sets could be set to the trivial one: @{term "λ l. UNIV"}.
         But we can't
         trivially proof, that evaluating an expression will never result in a
         break, allthough Java expressions allready syntactically don't allow
         nested stetements in them. The reason are the nested class initialzation
         statements which are inserted by the evaluation rules. So to proof the
         absence of a break we need to ensure, that the initialization statements
         will never end up in a break. In a wellfromed initialization statement,
         of course, were breaks are nested correctly inside of @{term Lab}
         or @{term Loop} statements evaluation of the whole initialization
         statement will never result in a break, because this break will be
         handled inside of the statement. But for simplicity we haven't added
         the analysis of the correct nesting of breaks in the typing judgments
         right now. So we have decided to adjust the rules of definite assignment
         to fit to these circumstances. If an initialization is involved during
         evaluation of the expression (evaluation rules @{text FVar}, @{text NewC}
         and @{text NewA}
    *}

     Init: "Env\<turnstile> B »⟨Init C⟩» (|nrm=B,brk=λ l. UNIV|)),"
    --{* Wellformedness of a program will ensure, that every static initialiser
         is definetly assigned and the jumps are nested correctly. The case here
         for @{term Init} is just for convenience, to get a proper precondition
         for the induction hypothesis in various proofs, so that we don't have to
         expand the initialisation on every point where it is triggerred by the
         evaluation rules.
      *}
     NewC: "Env\<turnstile> B »⟨NewC C⟩» (|nrm=B,brk=λ l. UNIV|)),"

     NewA: "Env\<turnstile> B »⟨e⟩» A
            ==>
            Env\<turnstile> B »⟨New T[e]⟩» A"

     Cast: "Env\<turnstile> B »⟨e⟩» A
            ==>
            Env\<turnstile> B »⟨Cast T e⟩» A"

     Inst: "Env\<turnstile> B »⟨e⟩» A
            ==>
            Env\<turnstile> B »⟨e InstOf T⟩» A"

     Lit:  "Env\<turnstile> B »⟨Lit v⟩» (|nrm=B,brk=λ l. UNIV|)),"

     UnOp: "Env\<turnstile> B »⟨e⟩» A
            ==>
            Env\<turnstile> B »⟨UnOp unop e⟩» A"

     CondAnd: "[|Env\<turnstile> B »⟨e1⟩» E1; Env\<turnstile> (B ∪ assigns_if True e1) »⟨e2⟩» E2;
                nrm A = B ∪ (assigns_if True (BinOp CondAnd e1 e2) ∩
                                assigns_if False (BinOp CondAnd e1 e2));
                brk A = (λ l. UNIV) |]
               ==>
               Env\<turnstile> B »⟨BinOp CondAnd e1 e2⟩» A"

     CondOr: "[|Env\<turnstile> B »⟨e1⟩» E1; Env\<turnstile> (B ∪ assigns_if False e1) »⟨e2⟩» E2;
               nrm A = B ∪ (assigns_if True (BinOp CondOr e1 e2) ∩
                                 assigns_if False (BinOp CondOr e1 e2));
               brk A = (λ l. UNIV) |]
               ==>
               Env\<turnstile> B »⟨BinOp CondOr e1 e2⟩» A"

     BinOp: "[|Env\<turnstile> B »⟨e1⟩» E1; Env\<turnstile> nrm E1 »⟨e2⟩» A;
              binop ≠ CondAnd; binop ≠ CondOr|]
             ==>
             Env\<turnstile> B »⟨BinOp binop e1 e2⟩» A"

     Super: "This ∈ B
             ==>
             Env\<turnstile> B »⟨Super⟩» (|nrm=B,brk=λ l. UNIV|)),"

     AccLVar: "[|vn ∈ B;
                nrm A = B; brk A = (λ k. UNIV)|]
                ==>
                Env\<turnstile> B »⟨Acc (LVar vn)⟩» A"
    --{* To properly access a local variable we have to test the definite
         assignment here. The variable must occur in the set @{term B}
      *}

     Acc: "[|∀ vn. v ≠ LVar vn;
            Env\<turnstile> B »⟨v⟩» A|]
            ==>
            Env\<turnstile> B »⟨Acc v⟩» A"

     AssLVar: "[|Env\<turnstile> B »⟨e⟩» E; nrm A = nrm E ∪ {vn}; brk A = brk E|]
               ==>
               Env\<turnstile> B »⟨(LVar vn) := e⟩» A"

     Ass: "[|∀ vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» V; Env\<turnstile> nrm V »⟨e⟩» A|]
            ==>
            Env\<turnstile> B »⟨v := e⟩» A"

     CondBool: "[|Env\<turnstile>(c ? e1 : e2)::-(PrimT Boolean);
                 Env\<turnstile> B »⟨c⟩» C;
                 Env\<turnstile> (B ∪ assigns_if True  c) »⟨e1⟩» E1;
                 Env\<turnstile> (B ∪ assigns_if False c) »⟨e2⟩» E2;
                 nrm A = B ∪ (assigns_if True  (c ? e1 : e2) ∩
                                  assigns_if False (c ? e1 : e2));
                 brk A = (λ l. UNIV)|]
                 ==>
                 Env\<turnstile> B »⟨c ? e1 : e2⟩» A"

     Cond: "[|¬ Env\<turnstile>(c ? e1 : e2)::-(PrimT Boolean);
             Env\<turnstile> B »⟨c⟩» C;
             Env\<turnstile> (B ∪ assigns_if True  c) »⟨e1⟩» E1;
             Env\<turnstile> (B ∪ assigns_if False c) »⟨e2⟩» E2;
            nrm A = nrm E1 ∩ nrm E2; brk A = (λ l. UNIV)|]
            ==>
            Env\<turnstile> B »⟨c ? e1 : e2⟩» A"

     Call: "[|Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> nrm E »⟨args⟩» A|]
            ==>
            Env\<turnstile> B »⟨{accC,statT,mode}e·mn({pTs}args)⟩» A"

    -- {* The interplay of @{term Call}, @{term Methd} and @{term Body}:
          Why rules for @{term Methd} and @{term Body} at all? Note that a
          Java source program will not include bare  @{term Methd} or @{term Body}
          terms. These terms are just introduced during evaluation. So definite
          assignment of @{term Call} does not consider @{term Methd} or
          @{term Body} at all. So for definite assignment alone we could omit the
          rules for @{term Methd} and @{term Body}.
          But since evaluation of the method invocation is
          split up into three rules we must ensure that we have enough information
          about the call even in the @{term Body} term to make sure that we can
          proof type safety. Also we must be able transport this information
          from @{term Call} to @{term Methd} and then further to @{term Body}
          during evaluation to establish the definite assignment of @{term Methd}
          during evaluation of @{term Call}, and of @{term Body} during evaluation
          of @{term Methd}. This is necessary since definite assignment will be
          a precondition for each induction hypothesis coming out of the evaluation
          rules, and therefor we have to establish the definite assignment of the
          sub-evaluation during the type-safety proof. Note that well-typedness is
          also a precondition for type-safety and so we can omit some assertion
          that are already ensured by well-typedness.
       *}
     Methd: "[|methd (prg Env) D sig = Some m;
              Env\<turnstile> B »⟨Body (declclass m) (stmt (mbody (mthd m)))⟩» A
             |]
             ==>
             Env\<turnstile> B »⟨Methd D sig⟩» A"

     Body: "[|Env\<turnstile> B »⟨c⟩» C; jumpNestingOkS {Ret} c; Result ∈ nrm C;
             nrm A = B; brk A = (λ l. UNIV)|]
            ==>
            Env\<turnstile> B »⟨Body D c⟩» A"
    -- {* Note that @{term A} is not correlated to  @{term C}. If the body
          statement returns abruptly with return, evaluation of  @{term Body}
          will absorb this return and complete normally. So we cannot trivially
          get the assigned variables of the body statement since it has not
          completed normally or with a break.
          If the body completes normally we guarantee that the result variable
          is set with this rule. But if the body completes abruptly with a return
          we can't guarantee that the result variable is set here, since
          definite assignment only talks about normal completion and breaks. So
          for a return the @{term Jump} rule ensures that the result variable is
          set and then this information must be carried over to the @{term Body}
          rule by the conformance predicate of the state.
       *}
     LVar: "Env\<turnstile> B »⟨LVar vn⟩» (|nrm=B, brk=λ l. UNIV|)),"

     FVar: "Env\<turnstile> B »⟨e⟩» A
            ==>
            Env\<turnstile> B »⟨{accC,statDeclC,stat}e..fn⟩» A"

     AVar: "[|Env\<turnstile> B »⟨e1⟩» E1; Env\<turnstile> nrm E1 »⟨e2⟩» A|]
             ==>
             Env\<turnstile> B »⟨e1.[e2]⟩» A"

     Nil: "Env\<turnstile> B »⟨[]::expr list⟩» (|nrm=B, brk=λ l. UNIV|)),"

     Cons: "[|Env\<turnstile> B »⟨e::expr⟩» E; Env\<turnstile> nrm E »⟨es⟩» A|]
            ==>
            Env\<turnstile> B »⟨e#es⟩» A"

    declare inj_term_sym_simps [simp]
    declare assigns_if.simps [simp del]
    declare split_paired_All [simp del] split_paired_Ex [simp del]
    ML_setup {*
    simpset_ref() := simpset() delloop "split_all_tac"
    *}
    inductive_cases da_elim_cases [cases set]:
      "Env\<turnstile> B »⟨Skip⟩» A"
      "Env\<turnstile> B »In1r Skip» A"
      "Env\<turnstile> B »⟨Expr e⟩» A"
      "Env\<turnstile> B »In1r (Expr e)» A"
      "Env\<turnstile> B »⟨l• c⟩» A"
      "Env\<turnstile> B »In1r (l• c)» A"
      "Env\<turnstile> B »⟨c1;; c2⟩» A"
      "Env\<turnstile> B »In1r (c1;; c2)» A"
      "Env\<turnstile> B »⟨If(e) c1 Else c2⟩» A"
      "Env\<turnstile> B »In1r (If(e) c1 Else c2)» A"
      "Env\<turnstile> B »⟨l• While(e) c⟩» A"
      "Env\<turnstile> B »In1r (l• While(e) c)» A"
      "Env\<turnstile> B »⟨Jmp jump⟩» A"
      "Env\<turnstile> B »In1r (Jmp jump)» A"
      "Env\<turnstile> B »⟨Throw e⟩» A"
      "Env\<turnstile> B »In1r (Throw e)» A"
      "Env\<turnstile> B »⟨Try c1 Catch(C vn) c2⟩» A"
      "Env\<turnstile> B »In1r (Try c1 Catch(C vn) c2)» A"
      "Env\<turnstile> B »⟨c1 Finally c2⟩» A"
      "Env\<turnstile> B »In1r (c1 Finally c2)» A"
      "Env\<turnstile> B »⟨Init C⟩» A"
      "Env\<turnstile> B »In1r (Init C)» A"
      "Env\<turnstile> B »⟨NewC C⟩» A"
      "Env\<turnstile> B »In1l (NewC C)» A"
      "Env\<turnstile> B »⟨New T[e]⟩» A"
      "Env\<turnstile> B »In1l (New T[e])» A"
      "Env\<turnstile> B »⟨Cast T e⟩» A"
      "Env\<turnstile> B »In1l (Cast T e)» A"
      "Env\<turnstile> B »⟨e InstOf T⟩» A"
      "Env\<turnstile> B »In1l (e InstOf T)» A"
      "Env\<turnstile> B »⟨Lit v⟩» A"
      "Env\<turnstile> B »In1l (Lit v)» A"
      "Env\<turnstile> B »⟨UnOp unop e⟩» A"
      "Env\<turnstile> B »In1l (UnOp unop e)» A"
      "Env\<turnstile> B »⟨BinOp binop e1 e2⟩» A"
      "Env\<turnstile> B »In1l (BinOp binop e1 e2)» A"
      "Env\<turnstile> B »⟨Super⟩» A"
      "Env\<turnstile> B »In1l (Super)» A"
      "Env\<turnstile> B »⟨Acc v⟩» A"
      "Env\<turnstile> B »In1l (Acc v)» A"
      "Env\<turnstile> B »⟨v := e⟩» A"
      "Env\<turnstile> B »In1l (v := e)» A"
      "Env\<turnstile> B »⟨c ? e1 : e2⟩» A"
      "Env\<turnstile> B »In1l (c ? e1 : e2)» A"
      "Env\<turnstile> B »⟨{accC,statT,mode}e·mn({pTs}args)⟩» A"
      "Env\<turnstile> B »In1l ({accC,statT,mode}e·mn({pTs}args))» A"
      "Env\<turnstile> B »⟨Methd C sig⟩» A"
      "Env\<turnstile> B »In1l (Methd C sig)» A"
      "Env\<turnstile> B »⟨Body D c⟩» A"
      "Env\<turnstile> B »In1l (Body D c)» A"
      "Env\<turnstile> B »⟨LVar vn⟩» A"
      "Env\<turnstile> B »In2 (LVar vn)» A"
      "Env\<turnstile> B »⟨{accC,statDeclC,stat}e..fn⟩» A"
      "Env\<turnstile> B »In2 ({accC,statDeclC,stat}e..fn)» A"
      "Env\<turnstile> B »⟨e1.[e2]⟩» A"
      "Env\<turnstile> B »In2 (e1.[e2])» A"
      "Env\<turnstile> B »⟨[]::expr list⟩» A"
      "Env\<turnstile> B »In3 ([]::expr list)» A"
      "Env\<turnstile> B »⟨e#es⟩» A"
      "Env\<turnstile> B »In3 (e#es)» A"
    declare inj_term_sym_simps [simp del]
    declare assigns_if.simps [simp]
    declare split_paired_All [simp] split_paired_Ex [simp]
    ML_setup {*
    simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    *}
    (* To be able to eliminate both the versions with the overloaded brackets:
       (B »⟨Skip⟩» A) and with the explicit constructor (B »In1r Skip» A),
       every rule appears in both versions
     *)

    lemma da_Skip: "A = (|nrm=B,brk=λ l. UNIV|)), ==> Env\<turnstile> B »⟨Skip⟩» A"
      by (auto intro: da.Skip)

    lemma da_NewC: "A = (|nrm=B,brk=λ l. UNIV|)), ==> Env\<turnstile> B »⟨NewC C⟩» A"
      by (auto intro: da.NewC)

    lemma da_Lit:  "A = (|nrm=B,brk=λ l. UNIV|)), ==> Env\<turnstile> B »⟨Lit v⟩» A"
      by (auto intro: da.Lit)

    lemma da_Super: "[|This ∈ B;A = (|nrm=B,brk=λ l. UNIV|)),|] ==> Env\<turnstile> B »⟨Super⟩» A"
      by (auto intro: da.Super)

    lemma da_Init: "A = (|nrm=B,brk=λ l. UNIV|)), ==> Env\<turnstile> B »⟨Init C⟩» A"
      by (auto intro: da.Init)

    (*
    For boolean expressions:

    The following holds: "assignsE e ⊆ assigns_if True e ∩ assigns_if False e"
    but not vice versa:
     "assigns_if True e ∩ assigns_if False e ⊆ assignsE e"

    Example:
     e = ((x < 5) || (y = true)) && (y = true)

       =  (   a    ||    b     ) &&    c

    assigns_if True  a = {}
    assigns_if False a = {}

    assigns_if True  b = {y}
    assigns_if False b = {y}

    assigns_if True  c = {y}
    assigns_if False c = {y}

    assigns_if True (a || b) = assigns_if True a ∩
                                    (assigns_if False a ∪ assigns_if True b)
                               = {} ∩ ({} ∪ {y}) = {}
    assigns_if False (a || b) = assigns_if False a ∪ assigns_if False b
                                = {} ∪ {y} = {y}

    assigns_ifE True e =  assigns_if True (a || b) ∪ assigns_if True c
                        = {} ∪ {y} = {y}
    assigns_ifE False e = assigns_if False (a || b) ∩
                           (assigns_if True (a || b) ∪ assigns_if False c)
                         = {y} ∩ ({} ∪ {y}) = {y}

    assignsE e = {}
    *)

    lemma assignsE_subseteq_assigns_ifs:
     assumes boolEx: "E\<turnstile>e::-PrimT Boolean" (is "?Boolean e")
       shows "assignsE e ⊆ assigns_if True e ∩ assigns_if False e" (is "?Incl e")
    proof -
      have True and "?Boolean e ==> ?Incl e" and True and True
      proof (induct _ and e and _ and _ rule: var_expr_stmt.induct)
        case (Cast T e)
        have "E\<turnstile>e::- (PrimT Boolean)"
        proof -
          have "E\<turnstile>(Cast T e)::- (PrimT Boolean)" .
          then obtain Te where "E\<turnstile>e::-Te"
                               "prg E\<turnstile>Te\<preceq>? PrimT Boolean"
            by cases simp
          thus ?thesis
            by - (drule cast_Boolean2,simp)
        qed
        with Cast.hyps
        show ?case
          by simp
      next
        case (Lit val)
        thus ?case
          by - (erule wt_elim_cases, cases "val", auto simp add: empty_dt_def)
      next
        case (UnOp unop e)
        thus ?case
          by - (erule wt_elim_cases,cases unop,
                (fastsimp simp add: assignsE_const_simp)+)
      next
        case (BinOp binop e1 e2)
        from BinOp.prems obtain e1T e2T
          where "E\<turnstile>e1::-e1T" and "E\<turnstile>e2::-e2T" and "wt_binop (prg E) binop e1T e2T"
                and "(binop_type binop) = Boolean"
          by (elim wt_elim_cases) simp
        with BinOp.hyps
        show ?case
          by - (cases binop, auto simp add: assignsE_const_simp)
      next
        case (Cond c e1 e2)
        have hyp_c: "?Boolean c ==> ?Incl c" .
        have hyp_e1: "?Boolean e1 ==> ?Incl e1" .
        have hyp_e2: "?Boolean e2 ==> ?Incl e2" .
        have wt: "E\<turnstile>(c ? e1 : e2)::-PrimT Boolean" .
        then obtain
          boolean_c:  "E\<turnstile>c::-PrimT Boolean" and
          boolean_e1: "E\<turnstile>e1::-PrimT Boolean" and
          boolean_e2: "E\<turnstile>e2::-PrimT Boolean"
          by (elim wt_elim_cases) (auto dest: widen_Boolean2)
        show ?case
        proof (cases "constVal c")
          case None
          with boolean_e1 boolean_e2
          show ?thesis
            using hyp_e1 hyp_e2
            by (auto)
        next
          case (Some bv)
          show ?thesis
          proof (cases "the_Bool bv")
            case True
            with Some show ?thesis using hyp_e1 boolean_e1 by auto
          next
            case False
            with Some show ?thesis using hyp_e2 boolean_e2 by auto
          qed
        qed
      qed simp_all
      with boolEx
      show ?thesis
        by blast
    qed

    (* Trick:
       If you have a rule with the abstract term injections:
       e.g:  da.Skip "B »⟨Skip⟩» A"
       and the current goal state as an concrete injection:
       e.g: "B »In1r Skip» A"
       you can convert the rule by: da.Skip [simplified]
       if inj_term_simps is in the simpset

    *)

    lemma rmlab_same_label [simp]: "(rmlab l A) l = UNIV"
      by (simp add: rmlab_def)

    lemma rmlab_same_label1 [simp]: "l=l' ==> (rmlab l A) l' = UNIV"
      by (simp add: rmlab_def)

    lemma rmlab_other_label [simp]: "l≠l'==> (rmlab l A) l' = A l'"
      by (auto simp add: rmlab_def)

    lemma range_inter_ts_subseteq [intro]: "∀ k. A k  ⊆ B k ==>  =>\<Inter>A ⊆ =>\<Inter>B"
      by (auto simp add: range_inter_ts_def)

    lemma range_inter_ts_subseteq':
      "[|∀ k. A k  ⊆ B k; x ∈ =>\<Inter>A|] ==> x ∈ =>\<Inter>B"
      by (auto simp add: range_inter_ts_def)

    lemma da_monotone:
          assumes      da: "Env\<turnstile> B  »t» A"   and
            subseteq_B_B': "B ⊆ B'"          and
                      da': "Env\<turnstile> B' »t» A'"
      shows "(nrm A ⊆ nrm A') ∧ (∀ l. (brk A l ⊆ brk A' l))"
    proof -
      from da
      show "!! B' A'. [|Env\<turnstile> B' »t» A'; B ⊆ B'|]
                      ==> (nrm A ⊆ nrm A') ∧ (∀ l. (brk A l ⊆ brk A' l))"
           (is "PROP ?Hyp Env B t A")
      proof (induct)
        case Skip
        from Skip.prems Skip.hyps
        show ?case by cases simp
      next
        case Expr
        from Expr.prems Expr.hyps
        show ?case by cases simp
      next
        case (Lab A B C Env c l B' A')
        have A: "nrm A = nrm C ∩ brk C l" "brk A = rmlab l (brk C)" .
        have "PROP ?Hyp Env B ⟨c⟩ C" .
        moreover
        have "B ⊆ B'" .
        moreover
        obtain C'
          where "Env\<turnstile> B' »⟨c⟩» C'"
            and A': "nrm A' = nrm C' ∩ brk C' l" "brk A' = rmlab l (brk C')"
          using Lab.prems
          by - (erule da_elim_cases,simp)
        ultimately
        have "nrm C ⊆ nrm C'" and hyp_brk: "(∀l. brk C l ⊆ brk C' l)" by auto
        then
        have "nrm C ∩ brk C l ⊆ nrm C' ∩ brk C' l" by auto
        moreover
        {
          fix l'
          from hyp_brk
          have "rmlab l (brk C) l'  ⊆ rmlab l (brk C') l'"
            by  (cases "l=l'") simp_all
        }
        moreover note A A'
        ultimately show ?case
          by simp
      next
        case (Comp A B C1 C2 Env c1 c2 B' A')
        have A: "nrm A = nrm C2" "brk A = brk C1 =>∩  brk C2" .
        have "Env\<turnstile> B' »⟨c1;; c2⟩» A'" .
        then obtain  C1' C2'
          where da_c1: "Env\<turnstile> B' »⟨c1⟩» C1'" and
                da_c2: "Env\<turnstile> nrm C1' »⟨c2⟩» C2'"  and
                A': "nrm A' = nrm C2'" "brk A' = brk C1' =>∩  brk C2'"
          by (rule da_elim_cases) auto
        have "PROP ?Hyp Env B ⟨c1⟩ C1" .
        moreover have "B ⊆ B'" .
        moreover note da_c1
        ultimately have C1': "nrm C1 ⊆ nrm C1'" "(∀l. brk C1 l ⊆ brk C1' l)"
          by (auto)
        have "PROP ?Hyp Env (nrm C1) ⟨c2⟩ C2" .
        with da_c2 C1'
        have C2': "nrm C2 ⊆ nrm C2'" "(∀l. brk C2 l ⊆ brk C2' l)"
          by (auto)
        with A A' C1'
        show ?case
          by auto
      next
        case (If A B C1 C2 E Env c1 c2 e B' A')
        have A: "nrm A = nrm C1 ∩ nrm C2" "brk A = brk C1 =>∩  brk C2" .
        have "Env\<turnstile> B' »⟨If(e) c1 Else c2⟩» A'" .
        then obtain C1' C2'
          where da_c1: "Env\<turnstile> B' ∪ assigns_if True e »⟨c1⟩» C1'" and
                da_c2: "Env\<turnstile> B' ∪ assigns_if False e »⟨c2⟩» C2'" and
                   A': "nrm A' = nrm C1' ∩ nrm C2'" "brk A' = brk C1' =>∩  brk C2'"
          by (rule da_elim_cases) auto
        have "PROP ?Hyp Env (B ∪ assigns_if True e) ⟨c1⟩ C1" .
        moreover have B': "B ⊆ B'" .
        moreover note da_c1
        ultimately obtain C1': "nrm C1 ⊆ nrm C1'" "(∀l. brk C1 l ⊆ brk C1' l)"
          by blast
        have "PROP ?Hyp Env (B ∪ assigns_if False e) ⟨c2⟩ C2" .
        with da_c2 B'
        obtain C2': "nrm C2 ⊆ nrm C2'" "(∀l. brk C2 l ⊆ brk C2' l)"
          by blast
        with A A' C1'
        show ?case
          by auto
      next
        case (Loop A B C E Env c e l B' A')
        have A: "nrm A = nrm C ∩ (B ∪ assigns_if False e)"
                "brk A = brk C" .
        have "Env\<turnstile> B' »⟨l• While(e) c⟩» A'" .
        then obtain C'
          where
           da_c': "Env\<turnstile> B' ∪ assigns_if True e »⟨c⟩» C'" and
              A': "nrm A' = nrm C' ∩ (B' ∪ assigns_if False e)"
                  "brk A' = brk C'"
          by (rule da_elim_cases) auto
        have "PROP ?Hyp Env (B ∪ assigns_if True e) ⟨c⟩ C" .
        moreover have B': "B ⊆ B'" .
        moreover note da_c'
        ultimately obtain C': "nrm C ⊆ nrm C'" "(∀l. brk C l ⊆ brk C' l)"
          by blast
        with A A' B'
        have "nrm A ⊆ nrm A'"
          by blast
        moreover
        { fix l'
          have  "brk A l' ⊆ brk A' l'"
          proof (cases "constVal e")
            case None
            with A A' C'
            show ?thesis
               by (cases "l=l'") auto
          next
            case (Some bv)
            with A A' C'
            show ?thesis
              by (cases "the_Bool bv", cases "l=l'") auto
          qed
        }
        ultimately show ?case
          by auto
      next
        case (Jmp A B Env jump B' A')
        thus ?case by (elim da_elim_cases) (auto split: jump.splits)
      next
        case Throw thus ?case by -  (erule da_elim_cases, auto)
      next
        case (Try A B C C1 C2 Env c1 c2 vn B' A')
        have A: "nrm A = nrm C1 ∩ nrm C2"
                "brk A = brk C1 =>∩  brk C2" .
        have "Env\<turnstile> B' »⟨Try c1 Catch(C vn) c2⟩» A'" .
        then obtain C1' C2'
          where da_c1': "Env\<turnstile> B' »⟨c1⟩» C1'" and
                da_c2': "Env(|lcl := lcl Env(VName vn\<mapsto>Class C)|)),\<turnstile> B' ∪ {VName vn}
                          »⟨c2⟩» C2'" and
                A': "nrm A' = nrm C1' ∩ nrm C2'"
                    "brk A' = brk C1' =>∩  brk C2'"
          by (rule da_elim_cases) auto
        have "PROP ?Hyp Env B ⟨c1⟩ C1" .
        moreover have B': "B ⊆ B'" .
        moreover note da_c1'
        ultimately obtain C1': "nrm C1 ⊆ nrm C1'" "(∀l. brk C1 l ⊆ brk C1' l)"
          by blast
        have "PROP ?Hyp (Env(|lcl := lcl Env(VName vn\<mapsto>Class C)|)),)
                        (B ∪ {VName vn}) ⟨c2⟩ C2" .
        with B' da_c2'
        obtain "nrm C2 ⊆ nrm C2'" "(∀l. brk C2 l ⊆ brk C2' l)"
          by blast
        with C1' A A'
        show ?case
          by auto
      next
        case (Fin A B C1 C2 Env c1 c2 B' A')
        have A: "nrm A = nrm C1 ∪ nrm C2"
                "brk A = (brk C1 =>∪∀ nrm C2) =>∩ (brk C2)" .
        have "Env\<turnstile> B' »⟨c1 Finally c2⟩» A'" .
        then obtain C1' C2'
          where  da_c1': "Env\<turnstile> B' »⟨c1⟩» C1'" and
                 da_c2': "Env\<turnstile> B' »⟨c2⟩» C2'" and
                 A':  "nrm A' = nrm C1' ∪ nrm C2'"
                      "brk A' = (brk C1' =>∪∀ nrm C2') =>∩ (brk C2')"
          by (rule da_elim_cases) auto
        have "PROP ?Hyp Env B ⟨c1⟩ C1" .
        moreover have B': "B ⊆ B'" .
        moreover note da_c1'
        ultimately obtain C1': "nrm C1 ⊆ nrm C1'" "(∀l. brk C1 l ⊆ brk C1' l)"
          by blast
        have hyp_c2: "PROP ?Hyp Env B ⟨c2⟩ C2" .
        from da_c2' B'
         obtain "nrm C2 ⊆ nrm C2'" "(∀l. brk C2 l ⊆ brk C2' l)"
           by - (drule hyp_c2,auto)
         with A A' C1'
         show ?case
           by auto
       next
         case Init thus ?case by -  (erule da_elim_cases, auto)
       next
         case NewC thus ?case by -  (erule da_elim_cases, auto)
       next
         case NewA thus ?case by -  (erule da_elim_cases, auto)
       next
         case Cast thus ?case by -  (erule da_elim_cases, auto)
       next
         case Inst thus ?case by -  (erule da_elim_cases, auto)
       next
         case Lit thus ?case by -  (erule da_elim_cases, auto)
       next
         case UnOp thus ?case by -  (erule da_elim_cases, auto)
       next
         case (CondAnd A B E1 E2 Env e1 e2 B' A')
         have A: "nrm A = B ∪
                           assigns_if True (BinOp CondAnd e1 e2) ∩
                           assigns_if False (BinOp CondAnd e1 e2)"
                 "brk A = (λl. UNIV)" .
         have "Env\<turnstile> B' »⟨BinOp CondAnd e1 e2⟩» A'" .
         then obtain  A': "nrm A' = B' ∪
                                     assigns_if True (BinOp CondAnd e1 e2) ∩
                                     assigns_if False (BinOp CondAnd e1 e2)"
                          "brk A' = (λl. UNIV)"
           by (rule da_elim_cases) auto
         have B': "B ⊆ B'" .
         with A A' show ?case
           by auto
       next
         case CondOr thus ?case by - (erule da_elim_cases, auto)
       next
         case BinOp thus ?case by -  (erule da_elim_cases, auto)
       next
         case Super thus ?case by -  (erule da_elim_cases, auto)
       next
         case AccLVar thus ?case by -  (erule da_elim_cases, auto)
       next
         case Acc thus ?case by -  (erule da_elim_cases, auto)
       next
         case AssLVar thus ?case by - (erule da_elim_cases, auto)
       next
         case Ass thus ?case by -  (erule da_elim_cases, auto)
       next
         case (CondBool A B C E1 E2 Env c e1 e2 B' A')
         have A: "nrm A = B ∪
                            assigns_if True (c ? e1 : e2) ∩
                            assigns_if False (c ? e1 : e2)"
                 "brk A = (λl. UNIV)" .
         have "Env\<turnstile> (c ? e1 : e2)::- (PrimT Boolean)" .
         moreover
         have "Env\<turnstile> B' »⟨c ? e1 : e2⟩» A'" .
         ultimately
         obtain A': "nrm A' = B' ∪
                                      assigns_if True (c ? e1 : e2) ∩
                                      assigns_if False (c ? e1 : e2)"
                         "brk A' = (λl. UNIV)"
           by - (erule da_elim_cases,auto simp add: inj_term_simps)
           (* inj_term_simps needed to handle wt (defined without ⟨⟩) *)
         have B': "B ⊆ B'" .
         with A A' show ?case
           by auto
       next
         case (Cond A B C E1 E2 Env c e1 e2 B' A')
         have A: "nrm A = nrm E1 ∩ nrm E2"
                 "brk A = (λl. UNIV)" .
         have not_bool: "¬ Env\<turnstile> (c ? e1 : e2)::- (PrimT Boolean)" .
         have "Env\<turnstile> B' »⟨c ? e1 : e2⟩» A'" .
         then obtain E1' E2'
           where da_e1': "Env\<turnstile> B' ∪ assigns_if True c »⟨e1⟩» E1'" and
                 da_e2': "Env\<turnstile> B' ∪ assigns_if False c »⟨e2⟩» E2'" and
                     A': "nrm A' = nrm E1' ∩ nrm E2'"
                         "brk A' = (λl. UNIV)"
           using not_bool
           by  - (erule da_elim_cases, auto simp add: inj_term_simps)
           (* inj_term_simps needed to handle wt (defined without ⟨⟩) *)
         have "PROP ?Hyp Env (B ∪ assigns_if True c) ⟨e1⟩ E1" .
         moreover have B': "B ⊆ B'" .
         moreover note da_e1'
         ultimately obtain E1': "nrm E1 ⊆ nrm E1'" "(∀l. brk E1 l ⊆ brk E1' l)"
          by blast
         have "PROP ?Hyp Env (B ∪ assigns_if False c) ⟨e2⟩ E2" .
         with B' da_e2'
         obtain "nrm E2 ⊆ nrm E2'" "(∀l. brk E2 l ⊆ brk E2' l)"
           by blast
        with E1' A A'
        show ?case
          by auto
      next
        case Call
        from Call.prems and Call.hyps
        show ?case by cases auto
      next
        case Methd thus ?case by -  (erule da_elim_cases, auto)
      next
        case Body thus ?case by -  (erule da_elim_cases, auto)
      next
        case LVar thus ?case by -  (erule da_elim_cases, auto)
      next
        case FVar thus ?case by -  (erule da_elim_cases, auto)
      next
        case AVar thus ?case by -  (erule da_elim_cases, auto)
      next
        case Nil thus ?case by -  (erule da_elim_cases, auto)
      next
        case Cons thus ?case by -  (erule da_elim_cases, auto)
      qed
    qed

    lemma da_weaken:
          assumes            da: "Env\<turnstile> B »t» A" and
                  subseteq_B_B': "B ⊆ B'"
            shows "∃ A'. Env \<turnstile> B' »t» A'"
    proof -
      note assigned.select_convs [Pure.intro]
      from da
      show "!! B'. B ⊆ B' ==> ∃ A'. Env\<turnstile> B' »t» A'" (is "PROP ?Hyp Env B t")
      proof (induct)
        case Skip thus ?case by (iprover intro: da.Skip)
      next
        case Expr thus ?case by (iprover intro: da.Expr)
      next
        case (Lab A B C Env c l B')
        have "PROP ?Hyp Env B ⟨c⟩" .
        moreover
        have B': "B ⊆ B'" .
        ultimately obtain C' where "Env\<turnstile> B' »⟨c⟩» C'"
          by iprover
        then obtain A' where "Env\<turnstile> B' »⟨Break l• c⟩» A'"
          by (iprover intro: da.Lab)
        thus ?case ..
      next
        case (Comp A B C1 C2 Env c1 c2 B')
        have da_c1: "Env\<turnstile> B »⟨c1⟩» C1" .
        have "PROP ?Hyp Env B ⟨c1⟩" .
        moreover
        have B': "B ⊆ B'" .
        ultimately obtain C1' where da_c1': "Env\<turnstile> B' »⟨c1⟩» C1'"
          by iprover
        with da_c1 B'
        have
          "nrm C1 ⊆ nrm C1'"
          by (rule da_monotone [elim_format]) simp
        moreover
        have "PROP ?Hyp Env (nrm C1) ⟨c2⟩" .
        ultimately obtain C2' where "Env\<turnstile> nrm C1' »⟨c2⟩» C2'"
          by iprover
        with da_c1' obtain A' where "Env\<turnstile> B' »⟨c1;; c2⟩» A'"
          by (iprover intro: da.Comp)
        thus ?case ..
      next
        case (If A B C1 C2 E Env c1 c2 e B')
        have B': "B ⊆ B'" .
        obtain  E' where "Env\<turnstile> B' »⟨e⟩» E'"
        proof -
          have "PROP ?Hyp Env B ⟨e⟩" by (rule If.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain C1' where "Env\<turnstile> (B' ∪ assigns_if True e) »⟨c1⟩» C1'"
        proof -
          from B'
          have "(B ∪ assigns_if True e) ⊆ (B' ∪ assigns_if True e)"
            by blast
          moreover
          have "PROP ?Hyp Env (B ∪ assigns_if True e) ⟨c1⟩" by (rule If.hyps)
          ultimately
          show ?thesis using that by iprover
        qed
        moreover
        obtain C2' where "Env\<turnstile> (B' ∪ assigns_if False e) »⟨c2⟩» C2'"
        proof -
          from B' have "(B ∪ assigns_if False e) ⊆ (B' ∪ assigns_if False e)"
            by blast
          moreover
          have "PROP ?Hyp Env (B ∪ assigns_if False e) ⟨c2⟩" by (rule If.hyps)
          ultimately
          show ?thesis using that by iprover
        qed
        ultimately
        obtain A' where "Env\<turnstile> B' »⟨If(e) c1 Else c2⟩» A'"
          by (iprover intro: da.If)
        thus ?case ..
      next
        case (Loop A B C E Env c e l B')
        have B': "B ⊆ B'" .
        obtain  E' where "Env\<turnstile> B' »⟨e⟩» E'"
        proof -
          have "PROP ?Hyp Env B ⟨e⟩" by (rule Loop.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain C' where "Env\<turnstile> (B' ∪ assigns_if True e) »⟨c⟩» C'"
        proof -
          from B'
          have "(B ∪ assigns_if True e) ⊆ (B' ∪ assigns_if True e)"
            by blast
          moreover
          have "PROP ?Hyp Env (B ∪ assigns_if True e) ⟨c⟩" by (rule Loop.hyps)
          ultimately
          show ?thesis using that by iprover
        qed
        ultimately
        obtain A' where "Env\<turnstile> B' »⟨l• While(e) c⟩» A'"
          by (iprover intro: da.Loop )
        thus ?case ..
      next
        case (Jmp A B Env jump B')
        have B': "B ⊆ B'" .
        with Jmp.hyps have "jump = Ret --> Result ∈ B' "
          by auto
        moreover
        obtain A'::assigned
                  where  "nrm A' = UNIV"
                         "brk A' = (case jump of
                                      Break l => λk. if k = l then B' else UNIV
                                    | Cont l => λk. UNIV
                                    | Ret => λk. UNIV)"

          by  iprover
        ultimately have "Env\<turnstile> B' »⟨Jmp jump⟩» A'"
          by (rule da.Jmp)
        thus ?case ..
      next
        case Throw thus ?case by (iprover intro: da.Throw )
      next
        case (Try A B C C1 C2 Env c1 c2 vn B')
        have B': "B ⊆ B'" .
        obtain C1' where "Env\<turnstile> B' »⟨c1⟩» C1'"
        proof -
          have "PROP ?Hyp Env B ⟨c1⟩" by (rule Try.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain C2' where
          "Env(|lcl := lcl Env(VName vn\<mapsto>Class C)|)),\<turnstile> B' ∪ {VName vn} »⟨c2⟩» C2'"
        proof -
          from B' have "B ∪ {VName vn} ⊆ B' ∪ {VName vn}" by blast
          moreover
          have "PROP ?Hyp (Env(|lcl := lcl Env(VName vn\<mapsto>Class C)|)),)
                          (B ∪ {VName vn}) ⟨c2⟩"
            by (rule Try.hyps)
          ultimately
          show ?thesis using that by iprover
        qed
        ultimately
        obtain A' where "Env\<turnstile> B' »⟨Try c1 Catch(C vn) c2⟩» A'"
          by (iprover intro: da.Try )
        thus ?case ..
      next
        case (Fin A B C1 C2 Env c1 c2 B')
        have B': "B ⊆ B'" .
        obtain C1' where C1': "Env\<turnstile> B' »⟨c1⟩» C1'"
        proof -
          have "PROP ?Hyp Env B ⟨c1⟩" by (rule Fin.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain C2' where "Env\<turnstile> B' »⟨c2⟩» C2'"
        proof -
          have "PROP ?Hyp Env B ⟨c2⟩" by (rule Fin.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        ultimately
        obtain A' where "Env\<turnstile> B' »⟨c1 Finally c2⟩» A'"
          by (iprover intro: da.Fin )
        thus ?case ..
      next
        case Init thus ?case by (iprover intro: da.Init)
      next
        case NewC thus ?case by (iprover intro: da.NewC)
      next
        case NewA thus ?case by (iprover intro: da.NewA)
      next
        case Cast thus ?case by (iprover intro: da.Cast)
      next
        case Inst thus ?case by (iprover intro: da.Inst)
      next
        case Lit thus ?case by (iprover intro: da.Lit)
      next
        case UnOp thus ?case by (iprover intro: da.UnOp)
      next
        case (CondAnd A B E1 E2 Env e1 e2 B')
        have B': "B ⊆ B'" .
        obtain E1' where "Env\<turnstile> B' »⟨e1⟩» E1'"
        proof -
          have "PROP ?Hyp Env B ⟨e1⟩" by (rule CondAnd.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain E2' where "Env\<turnstile> B' ∪  assigns_if True e1 »⟨e2⟩» E2'"
        proof -
          from B' have "B ∪ assigns_if True e1 ⊆ B' ∪  assigns_if True e1"
            by blast
          moreover
          have "PROP ?Hyp Env (B ∪ assigns_if True e1) ⟨e2⟩" by (rule CondAnd.hyps)
          ultimately show ?thesis using that by iprover
        qed
        ultimately
        obtain A' where "Env\<turnstile> B' »⟨BinOp CondAnd e1 e2⟩» A'"
          by (iprover intro: da.CondAnd)
        thus ?case ..
      next
        case (CondOr A B E1 E2 Env e1 e2 B')
        have B': "B ⊆ B'" .
        obtain E1' where "Env\<turnstile> B' »⟨e1⟩» E1'"
        proof -
          have "PROP ?Hyp Env B ⟨e1⟩" by (rule CondOr.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain E2' where "Env\<turnstile> B' ∪ assigns_if False e1 »⟨e2⟩» E2'"
        proof -
          from B' have "B ∪ assigns_if False e1 ⊆ B' ∪  assigns_if False e1"
            by blast
          moreover
          have "PROP ?Hyp Env (B ∪ assigns_if False e1) ⟨e2⟩" by (rule CondOr.hyps)
          ultimately show ?thesis using that by iprover
        qed
        ultimately
        obtain A' where "Env\<turnstile> B' »⟨BinOp CondOr e1 e2⟩» A'"
          by (iprover intro: da.CondOr)
        thus ?case ..
      next
        case (BinOp A B E1 Env binop e1 e2 B')
        have B': "B ⊆ B'" .
        obtain E1' where E1': "Env\<turnstile> B' »⟨e1⟩» E1'"
        proof -
          have "PROP ?Hyp Env B ⟨e1⟩" by (rule BinOp.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain A' where "Env\<turnstile> nrm E1' »⟨e2⟩» A'"
        proof -
          have "Env\<turnstile> B »⟨e1⟩» E1" by (rule BinOp.hyps)
          from this B' E1'
          have "nrm E1 ⊆ nrm E1'"
            by (rule da_monotone [THEN conjE])
          moreover
          have "PROP ?Hyp Env (nrm E1) ⟨e2⟩" by (rule BinOp.hyps)
          ultimately show ?thesis using that by iprover
        qed
        ultimately
        have "Env\<turnstile> B' »⟨BinOp binop e1 e2⟩» A'"
          using BinOp.hyps by (iprover intro: da.BinOp)
        thus ?case ..
      next
        case (Super B Env B')
        have B': "B ⊆ B'" .
        with Super.hyps have "This ∈ B' "
          by auto
        thus ?case by (iprover intro: da.Super)
      next
        case (AccLVar A B Env vn B')
        have "vn ∈ B" .
        moreover
        have "B ⊆ B'" .
        ultimately have "vn ∈ B'" by auto
        thus ?case by (iprover intro: da.AccLVar)
      next
        case Acc thus ?case by (iprover intro: da.Acc)
      next
        case (AssLVar A B E Env e vn B')
        have B': "B ⊆ B'" .
        then obtain E' where "Env\<turnstile> B' »⟨e⟩» E'"
          by (rule AssLVar.hyps [elim_format]) iprover
        then obtain A' where
          "Env\<turnstile> B' »⟨LVar vn:=e⟩» A'"
          by (iprover intro: da.AssLVar)
        thus ?case ..
      next
        case (Ass A B Env V e v B')
        have B': "B ⊆ B'" .
        have "∀vn. v ≠ LVar vn".
        moreover
        obtain V' where V': "Env\<turnstile> B' »⟨v⟩» V'"
        proof -
          have "PROP ?Hyp Env B ⟨v⟩" by (rule Ass.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain A' where "Env\<turnstile> nrm V' »⟨e⟩» A'"
        proof -
          have "Env\<turnstile> B »⟨v⟩» V" by (rule Ass.hyps)
          from this B' V'
          have "nrm V ⊆ nrm V'"
            by (rule da_monotone [THEN conjE])
          moreover
          have "PROP ?Hyp Env (nrm V) ⟨e⟩" by (rule Ass.hyps)
          ultimately show ?thesis using that by iprover
        qed
        ultimately
        have "Env\<turnstile> B' »⟨v := e⟩» A'"
          by (iprover intro: da.Ass)
        thus ?case ..
      next
        case (CondBool A B C E1 E2 Env c e1 e2 B')
        have B': "B ⊆ B'" .
        have "Env\<turnstile>(c ? e1 : e2)::-(PrimT Boolean)" .
        moreover obtain C' where C': "Env\<turnstile> B' »⟨c⟩» C'"
        proof -
          have "PROP ?Hyp Env B ⟨c⟩" by (rule CondBool.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain E1' where "Env\<turnstile> B' ∪ assigns_if True c »⟨e1⟩» E1'"
        proof -
          from B'
          have "(B ∪ assigns_if True c) ⊆ (B' ∪ assigns_if True c)"
            by blast
          moreover
          have "PROP ?Hyp Env (B ∪ assigns_if True c) ⟨e1⟩" by (rule CondBool.hyps)
          ultimately
          show ?thesis using that by iprover
        qed
        moreover
        obtain E2' where "Env\<turnstile> B' ∪ assigns_if False c »⟨e2⟩» E2'"
        proof -
          from B'
          have "(B ∪ assigns_if False c) ⊆ (B' ∪ assigns_if False c)"
            by blast
          moreover
          have "PROP ?Hyp Env (B ∪ assigns_if False c) ⟨e2⟩" by(rule CondBool.hyps)
          ultimately
          show ?thesis using that by iprover
        qed
        ultimately
        obtain A' where "Env\<turnstile> B' »⟨c ? e1 : e2⟩» A'"
          by (iprover intro: da.CondBool)
        thus ?case ..
      next
        case (Cond A B C E1 E2 Env c e1 e2 B')
        have B': "B ⊆ B'" .
        have "¬ Env\<turnstile>(c ? e1 : e2)::-(PrimT Boolean)" .
        moreover obtain C' where C': "Env\<turnstile> B' »⟨c⟩» C'"
        proof -
          have "PROP ?Hyp Env B ⟨c⟩" by (rule Cond.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain E1' where "Env\<turnstile> B' ∪ assigns_if True c »⟨e1⟩» E1'"
        proof -
          from B'
          have "(B ∪ assigns_if True c) ⊆ (B' ∪ assigns_if True c)"
            by blast
          moreover
          have "PROP ?Hyp Env (B ∪ assigns_if True c) ⟨e1⟩" by (rule Cond.hyps)
          ultimately
          show ?thesis using that by iprover
        qed
        moreover
        obtain E2' where "Env\<turnstile> B' ∪ assigns_if False c »⟨e2⟩» E2'"
        proof -
          from B'
          have "(B ∪ assigns_if False c) ⊆ (B' ∪ assigns_if False c)"
            by blast
          moreover
          have "PROP ?Hyp Env (B ∪ assigns_if False c) ⟨e2⟩" by (rule Cond.hyps)
          ultimately
          show ?thesis using that by iprover
        qed
        ultimately
        obtain A' where "Env\<turnstile> B' »⟨c ? e1 : e2⟩» A'"
          by (iprover intro: da.Cond)
        thus ?case ..
      next
        case (Call A B E Env accC args e mn mode pTs statT B')
        have B': "B ⊆ B'" .
        obtain E' where E': "Env\<turnstile> B' »⟨e⟩» E'"
        proof -
          have "PROP ?Hyp Env B ⟨e⟩" by (rule Call.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain A' where "Env\<turnstile> nrm E' »⟨args⟩» A'"
        proof -
          have "Env\<turnstile> B »⟨e⟩» E" by (rule Call.hyps)
          from this B' E'
          have "nrm E ⊆ nrm E'"
            by (rule da_monotone [THEN conjE])
          moreover
          have "PROP ?Hyp Env (nrm E) ⟨args⟩" by (rule Call.hyps)
          ultimately show ?thesis using that by iprover
        qed
        ultimately
        have "Env\<turnstile> B' »⟨{accC,statT,mode}e·mn( {pTs}args)⟩» A'"
          by (iprover intro: da.Call)
        thus ?case ..
      next
        case Methd thus ?case by (iprover intro: da.Methd)
      next
        case (Body A B C D Env c B')
        have B': "B ⊆ B'" .
        obtain C' where C': "Env\<turnstile> B' »⟨c⟩» C'" and nrm_C': "nrm C ⊆ nrm C'"
        proof -
          have "Env\<turnstile> B »⟨c⟩» C" by (rule Body.hyps)
          moreover note B'
          moreover
          from B' obtain C' where da_c: "Env\<turnstile> B' »⟨c⟩» C'"
            by (rule Body.hyps [elim_format]) blast
          ultimately
          have "nrm C ⊆ nrm C'"
            by (rule da_monotone [THEN conjE])
          with da_c that show ?thesis by iprover
        qed
        moreover
        have "Result ∈ nrm C" .
        with nrm_C' have "Result ∈ nrm C'"
          by blast
        moreover have "jumpNestingOkS {Ret} c" .
        ultimately obtain A' where
          "Env\<turnstile> B' »⟨Body D c⟩» A'"
          by (iprover intro: da.Body)
        thus ?case ..
      next
        case LVar thus ?case by (iprover intro: da.LVar)
      next
        case FVar thus ?case by (iprover intro: da.FVar)
      next
        case (AVar A B E1 Env e1 e2 B')
        have B': "B ⊆ B'" .
        obtain E1' where E1': "Env\<turnstile> B' »⟨e1⟩» E1'"
        proof -
          have "PROP ?Hyp Env B ⟨e1⟩" by (rule AVar.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain A' where "Env\<turnstile> nrm E1' »⟨e2⟩» A'"
        proof -
          have "Env\<turnstile> B »⟨e1⟩» E1" by (rule AVar.hyps)
          from this B' E1'
          have "nrm E1 ⊆ nrm E1'"
            by (rule da_monotone [THEN conjE])
          moreover
          have "PROP ?Hyp Env (nrm E1) ⟨e2⟩" by (rule AVar.hyps)
          ultimately show ?thesis using that by iprover
        qed
        ultimately
        have "Env\<turnstile> B' »⟨e1.[e2]⟩» A'"
          by (iprover intro: da.AVar)
        thus ?case ..
      next
        case Nil thus ?case by (iprover intro: da.Nil)
      next
        case (Cons A B E Env e es B')
        have B': "B ⊆ B'" .
        obtain E' where E': "Env\<turnstile> B' »⟨e⟩» E'"
        proof -
          have "PROP ?Hyp Env B ⟨e⟩" by (rule Cons.hyps)
          with B'
          show ?thesis using that by iprover
        qed
        moreover
        obtain A' where "Env\<turnstile> nrm E' »⟨es⟩» A'"
        proof -
          have "Env\<turnstile> B »⟨e⟩» E" by (rule Cons.hyps)
          from this B' E'
          have "nrm E ⊆ nrm E'"
            by (rule da_monotone [THEN conjE])
          moreover
          have "PROP ?Hyp Env (nrm E) ⟨es⟩" by (rule Cons.hyps)
          ultimately show ?thesis using that by iprover
        qed
        ultimately
        have "Env\<turnstile> B' »⟨e # es⟩» A'"
          by (iprover intro: da.Cons)
        thus ?case ..
      qed
    qed

    (* Remarks about the proof style:

       "by (rule <Case>.hyps)" vs "."
       --------------------------

       with <Case>.hyps you state more precise were the rule comes from

       . takes all assumptions into account, but looks more "light"
       and is more resistent for cut and paste proof in different
       cases.

      "intro: da.intros" vs "da.<Case>"
      ---------------------------------
      The first ist more convinient for cut and paste between cases,
      the second is more informativ for the reader
    *)

    corollary da_weakenE [consumes 2]:
      assumes          da: "Env\<turnstile> B  »t» A"   and
                       B': "B ⊆ B'"          and
                  ex_mono: "!! A'.  [|Env\<turnstile> B' »t» A'; nrm A ⊆ nrm A';
                                   !! l. brk A l ⊆ brk A' l|] ==> P"
      shows "P"
    proof -
      from da B'
      obtain A' where A': "Env\<turnstile> B' »t» A'"
        by (rule da_weaken [elim_format]) iprover
      with da B'
      have "nrm A ⊆ nrm A' ∧ (∀ l. brk A l ⊆ brk A' l)"
        by (rule da_monotone)
      with A' ex_mono
      show ?thesis
        by iprover
    qed

    end

## Correct nesting of jump statements

lemma jumpNestingOk_expr_simp:

      jumpNestingOk jmps (In1l e) = True

lemma jumpNestingOk_expr_simp1:

      jumpNestingOk jmps ⟨e⟩ = True

lemma jumpNestingOk_stmt_simp:

      jumpNestingOk jmps (In1r s) = jumpNestingOkS jmps s

lemma jumpNestingOk_stmt_simp1:

      jumpNestingOk jmps ⟨s⟩ = jumpNestingOkS jmps s

lemma jumpNestingOk_var_simp:

      jumpNestingOk jmps (In2 v) = True

lemma jumpNestingOk_var_simp1:

      jumpNestingOk jmps ⟨v⟩ = True

lemma jumpNestingOk_expr_list_simp:

      jumpNestingOk jmps (In3 es) = True

lemma jumpNestingOk_expr_list_simp1:

      jumpNestingOk jmps ⟨es⟩ = True

## Calculation of assigned variables for boolean expressions

### Very restricted calculation fallback calculation

lemma assigns_expr_simp:

      assigns (In1l e) = assignsE e

lemma assigns_expr_simp1:

      assigns ⟨e⟩ = assignsE e

lemma assigns_stmt_simp:

      assigns (In1r s) = {}

lemma assigns_stmt_simp1:

      assigns ⟨s⟩ = {}

lemma assigns_var_simp:

      assigns (In2 v) = assignsV v

lemma assigns_var_simp1:

      assigns ⟨v⟩ = assignsV v

lemma assigns_expr_list_simp:

      assigns (In3 es) = assignsEs es

lemma assigns_expr_list_simp1:

      assigns ⟨es⟩ = assignsEs es

### Analysis of constant expressions

lemma constVal_Some_induct:

      [| constVal e = Some v; !!v. P (Lit v); !!unop e'. P e' ==> P (UnOp unop e');
         !!binop e1 e2. [| P e1; P e2 |] ==> P (BinOp binop e1 e2);
         !!b bv e1 e2.
            [| constVal b = Some bv; the_Bool bv; P b; P e1 |] ==> P (b ? e1 : e2);
         !!b bv e1 e2.
            [| constVal b = Some bv; ¬ the_Bool bv; P b; P e2 |]
            ==> P (b ? e1 : e2) |]
      ==> P e

lemma assignsE_const_simp:

      constVal e = Some v ==> assignsE e = {}

### Main analysis for boolean expressions

lemma assigns_if_const_b_simp:

      constVal e = Some (Bool b) ==> assigns_if b e = {}

lemma assigns_if_const_not_b_simp:

      constVal e = Some (Bool b) ==> assigns_if (¬ b) e = UNIV

### Lifting set operations to range of tables (map to a set)

#### Binary union of tables

lemma union_ts_iff:

      (c ∈ (A =>∪ B) k) = (c ∈ A k ∨ c ∈ B k)

lemma union_tsI1:

      c ∈ A k ==> c ∈ (A =>∪ B) k

lemma union_tsI2:

      c ∈ B k ==> c ∈ (A =>∪ B) k

lemma union_tsCI:

      (c ∉ B k ==> c ∈ A k) ==> c ∈ (A =>∪ B) k

lemma union_tsE:

      [| c ∈ (A =>∪ B) k; c ∈ A k ==> P; c ∈ B k ==> P |] ==> P

#### Binary intersection of tables

lemma intersect_ts_iff:

      (c ∈ (A =>∩  B) k) = (c ∈ A k ∧ c ∈ B k)

lemma intersect_tsI:

      [| c ∈ A k; c ∈ B k |] ==> c ∈ (A =>∩  B) k

lemma intersect_tsD1:

      c ∈ (A =>∩  B) k ==> c ∈ A k

lemma intersect_tsD2:

      c ∈ (A =>∩  B) k ==> c ∈ B k

lemma intersect_tsE:

      [| c ∈ (A =>∩  B) k; [| c ∈ A k; c ∈ B k |] ==> P |] ==> P

#### All-Union of tables and set

lemma all_union_ts_iff:

      (c ∈ (A =>∪∀ B) k) = (c ∈ A k ∨ c ∈ B)

lemma all_union_tsI1:

      c ∈ A k ==> c ∈ (A =>∪∀ B) k

lemma all_union_tsI2:

      c ∈ B ==> c ∈ (A =>∪∀ B) k

lemma all_union_tsCI:

      (c ∉ B ==> c ∈ A k) ==> c ∈ (A =>∪∀ B) k

lemma all_union_tsE:

      [| c ∈ (A =>∪∀ B) k; c ∈ A k ==> P; c ∈ B ==> P |] ==> P

## The rules of definite assignment

lemmas da_elim_cases:

      [| Env\<turnstile> B »⟨Skip⟩» A; A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »In1r Skip» A; A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Expr e⟩» A; Env\<turnstile> B »⟨e⟩» A ==> P |] ==> P

      [| Env\<turnstile> B »In1r (Expr e)» A; Env\<turnstile> B »⟨e⟩» A ==> P |] ==> P

      [| Env\<turnstile> B »⟨l• c⟩» A;
         !!C l. [| Env\<turnstile> B »⟨c⟩» C; nrm A = nrm C ∩ brk C l;
                   brk A = rmlab l (brk C); l = Break l |]
                ==> P |]
      ==> P

      [| Env\<turnstile> B »In1r (l• c)» A;
         !!C l. [| Env\<turnstile> B »⟨c⟩» C; nrm A = nrm C ∩ brk C l;
                   brk A = rmlab l (brk C); l = Break l |]
                ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨c1.0;; c2.0⟩» A;
         !!C1 C2.
            [| Env\<turnstile> B »⟨c1.0⟩» C1; Env\<turnstile> nrm C1 »⟨c2.0⟩» C2;
               nrm A = nrm C2; brk A = brk C1 =>∩  brk C2 |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »In1r (c1.0;; c2.0)» A;
         !!C1 C2.
            [| Env\<turnstile> B »⟨c1.0⟩» C1; Env\<turnstile> nrm C1 »⟨c2.0⟩» C2;
               nrm A = nrm C2; brk A = brk C1 =>∩  brk C2 |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨If(e) c1.0 Else c2.0⟩» A;
         !!C1 C2 E.
            [| Env\<turnstile> B »⟨e⟩» E;
               Env\<turnstile> B ∪ assigns_if True e »⟨c1.0⟩» C1;
               Env\<turnstile> B ∪ assigns_if False e »⟨c2.0⟩» C2;
               nrm A = nrm C1 ∩ nrm C2; brk A = brk C1 =>∩  brk C2 |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »In1r (If(e) c1.0 Else c2.0)» A;
         !!C1 C2 E.
            [| Env\<turnstile> B »⟨e⟩» E;
               Env\<turnstile> B ∪ assigns_if True e »⟨c1.0⟩» C1;
               Env\<turnstile> B ∪ assigns_if False e »⟨c2.0⟩» C2;
               nrm A = nrm C1 ∩ nrm C2; brk A = brk C1 =>∩  brk C2 |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨l• While(e) c⟩» A;
         !!C E. [| Env\<turnstile> B »⟨e⟩» E;
                   Env\<turnstile> B ∪ assigns_if True e »⟨c⟩» C;
                   nrm A = nrm C ∩ (B ∪ assigns_if False e); brk A = brk C |]
                ==> P |]
      ==> P

      [| Env\<turnstile> B »In1r (l• While(e) c)» A;
         !!C E. [| Env\<turnstile> B »⟨e⟩» E;
                   Env\<turnstile> B ∪ assigns_if True e »⟨c⟩» C;
                   nrm A = nrm C ∩ (B ∪ assigns_if False e); brk A = brk C |]
                ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Jmp jump⟩» A;
         [| jump = Ret --> Result ∈ B; nrm A = UNIV;
            brk A =
            (case jump of Break l => %k. if k = l then B else UNIV | _ => %k. UNIV) |]
         ==> P |]
      ==> P

      [| Env\<turnstile> B »In1r (Jmp jump)» A;
         [| jump = Ret --> Result ∈ B; nrm A = UNIV;
            brk A =
            (case jump of Break l => %k. if k = l then B else UNIV | _ => %k. UNIV) |]
         ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Throw e⟩» A;
         !!E. [| Env\<turnstile> B »⟨e⟩» E; nrm A = UNIV; brk A = (%l. UNIV) |]
              ==> P |]
      ==> P

      [| Env\<turnstile> B »In1r (Throw e)» A;
         !!E. [| Env\<turnstile> B »⟨e⟩» E; nrm A = UNIV; brk A = (%l. UNIV) |]
              ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Try c1.0 Catch(C vn) c2.0⟩» A;
         !!C1 C2.
            [| Env\<turnstile> B »⟨c1.0⟩» C1;
               Env(| lcl := lcl Env(VName vn |->
                       Class C) |)\<turnstile> insert (VName vn) B »⟨c2.0⟩» C2;
               nrm A = nrm C1 ∩ nrm C2; brk A = brk C1 =>∩  brk C2 |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »In1r (Try c1.0 Catch(C vn) c2.0)» A;
         !!C1 C2.
            [| Env\<turnstile> B »⟨c1.0⟩» C1;
               Env(| lcl := lcl Env(VName vn |->
                       Class C) |)\<turnstile> insert (VName vn) B »⟨c2.0⟩» C2;
               nrm A = nrm C1 ∩ nrm C2; brk A = brk C1 =>∩  brk C2 |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨c1.0 Finally c2.0⟩» A;
         !!C1 C2.
            [| Env\<turnstile> B »⟨c1.0⟩» C1; Env\<turnstile> B »⟨c2.0⟩» C2;
               nrm A = nrm C1 ∪ nrm C2; brk A = (brk C1 =>∪∀ nrm C2) =>∩  brk C2 |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »In1r (c1.0 Finally c2.0)» A;
         !!C1 C2.
            [| Env\<turnstile> B »⟨c1.0⟩» C1; Env\<turnstile> B »⟨c2.0⟩» C2;
               nrm A = nrm C1 ∪ nrm C2; brk A = (brk C1 =>∪∀ nrm C2) =>∩  brk C2 |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Init C⟩» A; A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »In1r (Init C)» A;
         A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨NewC C⟩» A; A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »In1l (NewC C)» A;
         A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨New T[e]⟩» A; Env\<turnstile> B »⟨e⟩» A ==> P |] ==> P

      [| Env\<turnstile> B »In1l (New T[e])» A; Env\<turnstile> B »⟨e⟩» A ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Cast T e⟩» A; Env\<turnstile> B »⟨e⟩» A ==> P |] ==> P

      [| Env\<turnstile> B »In1l (Cast T e)» A; Env\<turnstile> B »⟨e⟩» A ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨e InstOf T⟩» A; Env\<turnstile> B »⟨e⟩» A ==> P |] ==> P

      [| Env\<turnstile> B »In1l (e InstOf T)» A; Env\<turnstile> B »⟨e⟩» A ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Lit v⟩» A; A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »In1l (Lit v)» A;
         A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨UnOp unop e⟩» A; Env\<turnstile> B »⟨e⟩» A ==> P |] ==> P

      [| Env\<turnstile> B »In1l (UnOp unop e)» A; Env\<turnstile> B »⟨e⟩» A ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨BinOp binop e1.0 e2.0⟩» A;
         !!E1 E2.
            [| Env\<turnstile> B »⟨e1.0⟩» E1;
               Env\<turnstile> B ∪ assigns_if True e1.0 »⟨e2.0⟩» E2;
               nrm A =
               B ∪ assigns_if True (BinOp CondAnd e1.0 e2.0) ∩
                   assigns_if False (BinOp CondAnd e1.0 e2.0);
               brk A = (%l. UNIV); binop = CondAnd |]
            ==> P;
         !!E1 E2.
            [| Env\<turnstile> B »⟨e1.0⟩» E1;
               Env\<turnstile> B ∪ assigns_if False e1.0 »⟨e2.0⟩» E2;
               nrm A =
               B ∪ assigns_if True (BinOp CondOr e1.0 e2.0) ∩
                   assigns_if False (BinOp CondOr e1.0 e2.0);
               brk A = (%l. UNIV); binop = CondOr |]
            ==> P;
         !!E1. [| Env\<turnstile> B »⟨e1.0⟩» E1; Env\<turnstile> nrm E1 »⟨e2.0⟩» A;
                  binop ≠ CondAnd; binop ≠ CondOr |]
               ==> P |]
      ==> P

      [| Env\<turnstile> B »In1l (BinOp binop e1.0 e2.0)» A;
         !!E1 E2.
            [| Env\<turnstile> B »⟨e1.0⟩» E1;
               Env\<turnstile> B ∪ assigns_if True e1.0 »⟨e2.0⟩» E2;
               nrm A =
               B ∪ assigns_if True (BinOp CondAnd e1.0 e2.0) ∩
                   assigns_if False (BinOp CondAnd e1.0 e2.0);
               brk A = (%l. UNIV); binop = CondAnd |]
            ==> P;
         !!E1 E2.
            [| Env\<turnstile> B »⟨e1.0⟩» E1;
               Env\<turnstile> B ∪ assigns_if False e1.0 »⟨e2.0⟩» E2;
               nrm A =
               B ∪ assigns_if True (BinOp CondOr e1.0 e2.0) ∩
                   assigns_if False (BinOp CondOr e1.0 e2.0);
               brk A = (%l. UNIV); binop = CondOr |]
            ==> P;
         !!E1. [| Env\<turnstile> B »⟨e1.0⟩» E1; Env\<turnstile> nrm E1 »⟨e2.0⟩» A;
                  binop ≠ CondAnd; binop ≠ CondOr |]
               ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Super⟩» A;
         [| This ∈ B; A = (| nrm = B, brk = %l. UNIV |) |] ==> P |]
      ==> P

      [| Env\<turnstile> B »In1l Super» A;
         [| This ∈ B; A = (| nrm = B, brk = %l. UNIV |) |] ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Acc v⟩» A;
         !!vn. [| vn ∈ nrm A; brk A = (%k. UNIV); B = nrm A; v = LVar vn |] ==> P;
         [| ∀vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» A |] ==> P |]
      ==> P

      [| Env\<turnstile> B »In1l (Acc v)» A;
         !!vn. [| vn ∈ nrm A; brk A = (%k. UNIV); B = nrm A; v = LVar vn |] ==> P;
         [| ∀vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» A |] ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨v:=e⟩» A;
         !!E vn.
            [| Env\<turnstile> B »⟨e⟩» E; nrm A = insert vn (nrm E); brk A = brk E;
               v = LVar vn |]
            ==> P;
         !!V. [| ∀vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» V;
                 Env\<turnstile> nrm V »⟨e⟩» A |]
              ==> P |]
      ==> P

      [| Env\<turnstile> B »In1l (v:=e)» A;
         !!E vn.
            [| Env\<turnstile> B »⟨e⟩» E; nrm A = insert vn (nrm E); brk A = brk E;
               v = LVar vn |]
            ==> P;
         !!V. [| ∀vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» V;
                 Env\<turnstile> nrm V »⟨e⟩» A |]
              ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨c ? e1.0 : e2.0⟩» A;
         !!C E1 E2.
            [| Env|-⟨c ? e1.0 : e2.0⟩::Inl (PrimT Boolean); Env\<turnstile> B »⟨c⟩» C;
               Env\<turnstile> B ∪ assigns_if True c »⟨e1.0⟩» E1;
               Env\<turnstile> B ∪ assigns_if False c »⟨e2.0⟩» E2;
               nrm A =
               B ∪ assigns_if True (c ? e1.0 : e2.0) ∩
                   assigns_if False (c ? e1.0 : e2.0);
               brk A = (%l. UNIV) |]
            ==> P;
         !!C E1 E2.
            [| (Env, empty_dt, ⟨c ? e1.0 : e2.0⟩, Inl (PrimT Boolean)) ∉ wt;
               Env\<turnstile> B »⟨c⟩» C;
               Env\<turnstile> B ∪ assigns_if True c »⟨e1.0⟩» E1;
               Env\<turnstile> B ∪ assigns_if False c »⟨e2.0⟩» E2;
               nrm A = nrm E1 ∩ nrm E2; brk A = (%l. UNIV) |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »In1l (c ? e1.0 : e2.0)» A;
         !!C E1 E2.
            [| Env|-⟨c ? e1.0 : e2.0⟩::Inl (PrimT Boolean); Env\<turnstile> B »⟨c⟩» C;
               Env\<turnstile> B ∪ assigns_if True c »⟨e1.0⟩» E1;
               Env\<turnstile> B ∪ assigns_if False c »⟨e2.0⟩» E2;
               nrm A =
               B ∪ assigns_if True (c ? e1.0 : e2.0) ∩
                   assigns_if False (c ? e1.0 : e2.0);
               brk A = (%l. UNIV) |]
            ==> P;
         !!C E1 E2.
            [| (Env, empty_dt, ⟨c ? e1.0 : e2.0⟩, Inl (PrimT Boolean)) ∉ wt;
               Env\<turnstile> B »⟨c⟩» C;
               Env\<turnstile> B ∪ assigns_if True c »⟨e1.0⟩» E1;
               Env\<turnstile> B ∪ assigns_if False c »⟨e2.0⟩» E2;
               nrm A = nrm E1 ∩ nrm E2; brk A = (%l. UNIV) |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨{accC,statT,mode}e·mn( {pTs}args)⟩» A;
         !!E. [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> nrm E »⟨args⟩» A |]
              ==> P |]
      ==> P

      [| Env\<turnstile> B »In1l ({accC,statT,mode}e·mn( {pTs}args))» A;
         !!E. [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> nrm E »⟨args⟩» A |]
              ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Methd C sig⟩» A;
         !!m. [| methd (prg Env) C sig = Some m;
                 Env\<turnstile> B »⟨Body (declclass m) (stmt (mbody (mthd m)))⟩» A |]
              ==> P |]
      ==> P

      [| Env\<turnstile> B »In1l (Methd C sig)» A;
         !!m. [| methd (prg Env) C sig = Some m;
                 Env\<turnstile> B »⟨Body (declclass m) (stmt (mbody (mthd m)))⟩» A |]
              ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨Body D c⟩» A;
         !!C. [| Env\<turnstile> nrm A »⟨c⟩» C; jumpNestingOkS {Ret} c;
                 Result ∈ nrm C; brk A = (%l. UNIV); B = nrm A |]
              ==> P |]
      ==> P

      [| Env\<turnstile> B »In1l (Body D c)» A;
         !!C. [| Env\<turnstile> nrm A »⟨c⟩» C; jumpNestingOkS {Ret} c;
                 Result ∈ nrm C; brk A = (%l. UNIV); B = nrm A |]
              ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨LVar vn⟩» A; A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »In2 (LVar vn)» A;
         A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨{accC,statDeclC,stat}e..fn⟩» A;
         Env\<turnstile> B »⟨e⟩» A ==> P |]
      ==> P

      [| Env\<turnstile> B »In2 ({accC,statDeclC,stat}e..fn)» A;
         Env\<turnstile> B »⟨e⟩» A ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨e1.0.[e2.0]⟩» A;
         !!E1. [| Env\<turnstile> B »⟨e1.0⟩» E1; Env\<turnstile> nrm E1 »⟨e2.0⟩» A |]
               ==> P |]
      ==> P

      [| Env\<turnstile> B »In2 (e1.0.[e2.0])» A;
         !!E1. [| Env\<turnstile> B »⟨e1.0⟩» E1; Env\<turnstile> nrm E1 »⟨e2.0⟩» A |]
               ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨[]⟩» A; A = (| nrm = B, brk = %l. UNIV |) ==> P |] ==> P

      [| Env\<turnstile> B »In3 []» A; A = (| nrm = B, brk = %l. UNIV |) ==> P |]
      ==> P

      [| Env\<turnstile> B »⟨e # es⟩» A;
         [| ⟨e # es⟩ = ⟨Skip⟩; A = (| nrm = B, brk = %l. UNIV |) |] ==> P;
         !!e. [| Env\<turnstile> B »⟨e⟩» A; ⟨e # es⟩ = ⟨Expr e⟩ |] ==> P;
         !!C c l.
            [| Env\<turnstile> B »⟨c⟩» C; nrm A = nrm C ∩ brk C l;
               brk A = rmlab l (brk C); ⟨e # es⟩ = ⟨Break l• c⟩ |]
            ==> P;
         !!C1 C2 c1 c2.
            [| Env\<turnstile> B »⟨c1⟩» C1; Env\<turnstile> nrm C1 »⟨c2⟩» C2;
               nrm A = nrm C2; brk A = brk C1 =>∩  brk C2; ⟨e # es⟩ = ⟨c1;; c2⟩ |]
            ==> P;
         !!C1 C2 E c1 c2 e.
            [| Env\<turnstile> B »⟨e⟩» E;
               Env\<turnstile> B ∪ assigns_if True e »⟨c1⟩» C1;
               Env\<turnstile> B ∪ assigns_if False e »⟨c2⟩» C2;
               nrm A = nrm C1 ∩ nrm C2; brk A = brk C1 =>∩  brk C2;
               ⟨e # es⟩ = ⟨If(e) c1 Else c2⟩ |]
            ==> P;
         !!C E c e l.
            [| Env\<turnstile> B »⟨e⟩» E;
               Env\<turnstile> B ∪ assigns_if True e »⟨c⟩» C;
               nrm A = nrm C ∩ (B ∪ assigns_if False e); brk A = brk C;
               ⟨e # es⟩ = ⟨l• While(e) c⟩ |]
            ==> P;
         !!jump.
            [| jump = Ret --> Result ∈ B; nrm A = UNIV;
               brk A =
               (case jump of Break l => %k. if k = l then B else UNIV
                | _ => %k. UNIV);
               ⟨e # es⟩ = ⟨Jmp jump⟩ |]
            ==> P;
         !!E e. [| Env\<turnstile> B »⟨e⟩» E; nrm A = UNIV; brk A = (%l. UNIV);
                   ⟨e # es⟩ = ⟨Throw e⟩ |]
                ==> P;
         !!C C1 C2 c1 c2 vn.
            [| Env\<turnstile> B »⟨c1⟩» C1;
               Env(| lcl := lcl Env(VName vn |->
                       Class C) |)\<turnstile> insert (VName vn) B »⟨c2⟩» C2;
               nrm A = nrm C1 ∩ nrm C2; brk A = brk C1 =>∩  brk C2;
               ⟨e # es⟩ = ⟨Try c1 Catch(C vn) c2⟩ |]
            ==> P;
         !!C1 C2 c1 c2.
            [| Env\<turnstile> B »⟨c1⟩» C1; Env\<turnstile> B »⟨c2⟩» C2;
               nrm A = nrm C1 ∪ nrm C2; brk A = (brk C1 =>∪∀ nrm C2) =>∩  brk C2;
               ⟨e # es⟩ = ⟨c1 Finally c2⟩ |]
            ==> P;
         !!C. [| ⟨e # es⟩ = ⟨Init C⟩; A = (| nrm = B, brk = %l. UNIV |) |] ==> P;
         !!C. [| ⟨e # es⟩ = ⟨NewC C⟩; A = (| nrm = B, brk = %l. UNIV |) |] ==> P;
         !!T e. [| Env\<turnstile> B »⟨e⟩» A; ⟨e # es⟩ = ⟨New T[e]⟩ |] ==> P;
         !!T e. [| Env\<turnstile> B »⟨e⟩» A; ⟨e # es⟩ = ⟨Cast T e⟩ |] ==> P;
         !!T e. [| Env\<turnstile> B »⟨e⟩» A; ⟨e # es⟩ = ⟨e InstOf T⟩ |] ==> P;
         !!v. [| ⟨e # es⟩ = ⟨Lit v⟩; A = (| nrm = B, brk = %l. UNIV |) |] ==> P;
         !!e unop. [| Env\<turnstile> B »⟨e⟩» A; ⟨e # es⟩ = ⟨UnOp unop e⟩ |] ==> P;
         !!E1 E2 e1 e2.
            [| Env\<turnstile> B »⟨e1⟩» E1;
               Env\<turnstile> B ∪ assigns_if True e1 »⟨e2⟩» E2;
               nrm A =
               B ∪ assigns_if True (BinOp CondAnd e1 e2) ∩
                   assigns_if False (BinOp CondAnd e1 e2);
               brk A = (%l. UNIV); ⟨e # es⟩ = ⟨BinOp CondAnd e1 e2⟩ |]
            ==> P;
         !!E1 E2 e1 e2.
            [| Env\<turnstile> B »⟨e1⟩» E1;
               Env\<turnstile> B ∪ assigns_if False e1 »⟨e2⟩» E2;
               nrm A =
               B ∪ assigns_if True (BinOp CondOr e1 e2) ∩
                   assigns_if False (BinOp CondOr e1 e2);
               brk A = (%l. UNIV); ⟨e # es⟩ = ⟨BinOp CondOr e1 e2⟩ |]
            ==> P;
         !!E1 binop e1 e2.
            [| Env\<turnstile> B »⟨e1⟩» E1; Env\<turnstile> nrm E1 »⟨e2⟩» A;
               binop ≠ CondAnd; binop ≠ CondOr; ⟨e # es⟩ = ⟨BinOp binop e1 e2⟩ |]
            ==> P;
         [| This ∈ B; ⟨e # es⟩ = ⟨Super⟩; A = (| nrm = B, brk = %l. UNIV |) |] ==> P;
         !!vn. [| vn ∈ nrm A; brk A = (%k. UNIV); B = nrm A;
                  ⟨e # es⟩ = ⟨Acc (LVar vn)⟩ |]
               ==> P;
         !!v. [| ∀vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» A; ⟨e # es⟩ = ⟨Acc v⟩ |]
              ==> P;
         !!E e vn.
            [| Env\<turnstile> B »⟨e⟩» E; nrm A = insert vn (nrm E); brk A = brk E;
               ⟨e # es⟩ = ⟨LVar vn:=e⟩ |]
            ==> P;
         !!V e v.
            [| ∀vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» V;
               Env\<turnstile> nrm V »⟨e⟩» A; ⟨e # es⟩ = ⟨v:=e⟩ |]
            ==> P;
         !!C E1 E2 c e1 e2.
            [| Env|-⟨c ? e1 : e2⟩::Inl (PrimT Boolean); Env\<turnstile> B »⟨c⟩» C;
               Env\<turnstile> B ∪ assigns_if True c »⟨e1⟩» E1;
               Env\<turnstile> B ∪ assigns_if False c »⟨e2⟩» E2;
               nrm A =
               B ∪ assigns_if True (c ? e1 : e2) ∩ assigns_if False (c ? e1 : e2);
               brk A = (%l. UNIV); ⟨e # es⟩ = ⟨c ? e1 : e2⟩ |]
            ==> P;
         !!C E1 E2 c e1 e2.
            [| (Env, empty_dt, ⟨c ? e1 : e2⟩, Inl (PrimT Boolean)) ∉ wt;
               Env\<turnstile> B »⟨c⟩» C;
               Env\<turnstile> B ∪ assigns_if True c »⟨e1⟩» E1;
               Env\<turnstile> B ∪ assigns_if False c »⟨e2⟩» E2;
               nrm A = nrm E1 ∩ nrm E2; brk A = (%l. UNIV);
               ⟨e # es⟩ = ⟨c ? e1 : e2⟩ |]
            ==> P;
         !!E accC args e mn mode pTs statT.
            [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> nrm E »⟨args⟩» A;
               ⟨e # es⟩ = ⟨{accC,statT,mode}e·mn( {pTs}args)⟩ |]
            ==> P;
         !!D m sig.
            [| methd (prg Env) D sig = Some m;
               Env\<turnstile> B »⟨Body (declclass m) (stmt (mbody (mthd m)))⟩» A;
               ⟨e # es⟩ = ⟨Methd D sig⟩ |]
            ==> P;
         !!C D c.
            [| Env\<turnstile> nrm A »⟨c⟩» C; jumpNestingOkS {Ret} c; Result ∈ nrm C;
               brk A = (%l. UNIV); B = nrm A; ⟨e # es⟩ = ⟨Body D c⟩ |]
            ==> P;
         !!vn. [| ⟨e # es⟩ = ⟨LVar vn⟩; A = (| nrm = B, brk = %l. UNIV |) |] ==> P;
         !!accC e fn stat statDeclC.
            [| Env\<turnstile> B »⟨e⟩» A; ⟨e # es⟩ = ⟨{accC,statDeclC,stat}e..fn⟩ |]
            ==> P;
         !!E1 e1 e2.
            [| Env\<turnstile> B »⟨e1⟩» E1; Env\<turnstile> nrm E1 »⟨e2⟩» A;
               ⟨e # es⟩ = ⟨e1.[e2]⟩ |]
            ==> P;
         [| ⟨e # es⟩ = ⟨[]⟩; A = (| nrm = B, brk = %l. UNIV |) |] ==> P;
         !!E e es.
            [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> nrm E »⟨es⟩» A;
               ⟨e # es⟩ = ⟨e # es⟩ |]
            ==> P |]
      ==> P

      [| Env\<turnstile> B »In3 (e # es)» A;
         !!E. [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> nrm E »⟨es⟩» A |] ==> P |]
      ==> P

lemma da_Skip:

      A = (| nrm = B, brk = %l. UNIV |) ==> Env\<turnstile> B »⟨Skip⟩» A

lemma da_NewC:

      A = (| nrm = B, brk = %l. UNIV |) ==> Env\<turnstile> B »⟨NewC C⟩» A

lemma da_Lit:

      A = (| nrm = B, brk = %l. UNIV |) ==> Env\<turnstile> B »⟨Lit v⟩» A

lemma da_Super:

      [| This ∈ B; A = (| nrm = B, brk = %l. UNIV |) |]
      ==> Env\<turnstile> B »⟨Super⟩» A

lemma da_Init:

      A = (| nrm = B, brk = %l. UNIV |) ==> Env\<turnstile> B »⟨Init C⟩» A

lemma assignsE_subseteq_assigns_ifs:

      E|-e:-PrimT Boolean ==> assignsE e ⊆ assigns_if True e ∩ assigns_if False e

lemma rmlab_same_label:

      rmlab l A l = UNIV

lemma rmlab_same_label1:

      l = l' ==> rmlab l A l' = UNIV

lemma rmlab_other_label:

      l ≠ l' ==> rmlab l A l' = A l'

lemma range_inter_ts_subseteq:

      ∀k. A k ⊆ B k ==> =>\<Inter>A ⊆ =>\<Inter>B

lemma range_inter_ts_subseteq':

      [| ∀k. A k ⊆ B k; x ∈ =>\<Inter>A |] ==> x ∈ =>\<Inter>B

lemma da_monotone:

      [| Env\<turnstile> B »t» A; B ⊆ B'; Env\<turnstile> B' »t» A' |]
      ==> nrm A ⊆ nrm A' ∧ (∀l. brk A l ⊆ brk A' l)

lemma da_weaken:

      [| Env\<turnstile> B »t» A; B ⊆ B' |] ==> ∃A'. Env\<turnstile> B' »t» A'

corollary da_weakenE:

      [| Env\<turnstile> B »t» A; B ⊆ B';
         !!A'. [| Env\<turnstile> B' »t» A'; nrm A ⊆ nrm A';
                  !!l. brk A l ⊆ brk A' l |]
               ==> P |]
      ==> P