Theory DefiniteAssignment

subsection ‹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}
›

subsubsection ‹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.›

primrec jumpNestingOkS :: "jump set  stmt  bool"
where
  "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 termLab
| "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 termFinA
| "jumpNestingOkS jmps (FinA a c) = False"


definition jumpNestingOk :: "jump set  term  bool" where
"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)



subsubsection ‹Calculation of assigned variables for boolean expressions›


subsection ‹Very restricted calculation fallback calculation›

primrec the_LVar_name :: "var  lname"
  where "the_LVar_name (LVar n) = n"

primrec assignsE :: "expr  lname set" 
  and assignsV :: "var  lname set"
  and assignsEs:: "expr list  lname set"
where
  "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}objRefmn({pTs}args)) 
                            = (assignsE objRef)  (assignsEs args)"
― ‹Only dummy analysis for intermediate expressions  
      termMethd, termBody, termInsInitE and termCallee
| "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"

definition assigns :: "term  lname set" where
"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"

primrec constVal :: "expr  val option"
where
  "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 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 termb
| "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 " v. constVal e = Some v  P e"
  proof (induct e)
    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 add: hyp_Lit)
  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 
termBoolean value UNIV is returned. If we expect true/false the opposite 
constant false/true will also lead to UNIV.›
primrec assigns_if :: "bool  expr  lname set"
where
  "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}objRefmn({pTs}args))  
            = assignsE ({accC,statT,mode}objRefmn({pTs}args)) "
― ‹Only dummy analysis for intermediate expressions  
      termMethd, termBody, termInsInitE and termCallee
| "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 " b. ?Const b e  ?Ass b e"
  proof (induct e)
    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)
    note hyp_c =  b. ?Const b c  ?Ass b c
    note hyp_e1 =  b. ?Const b e1  ?Ass b e1
    note hyp_e2 =  b. ?Const b e2  ?Ass b e2
    note 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 " b. ?Const b e  ?Ass b e"
  proof (induct e)
    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)
    note hyp_c =  b. ?Const b c  ?Ass b c
    note hyp_e1 =  b. ?Const b e1  ?Ass b e1
    note hyp_e2 =  b. ?Const b e2  ?Ass b e2
    note 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)›

definition
  union_ts :: "('a,'b) tables  ('a,'b) tables  ('a,'b) tables" ("_ ⇒∪ _" [67,67] 65)
  where "A ⇒∪ B = (λ k. A k  B k)"

definition
  intersect_ts :: "('a,'b) tables  ('a,'b) tables  ('a,'b) tables" ("_ ⇒∩  _" [72,72] 71)
  where "A ⇒∩  B = (λk. A k  B k)"

definition
  all_union_ts :: "('a,'b) tables  'b set  ('a,'b) tables" (infixl "⇒∪" 40)
  where "(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


subsubsection "The rules of definite assignment"

 
type_synonym 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›

definition
  rmlab :: "'a  ('a,'b) tables  ('a,'b) tables"
  where "rmlab k A = (λx. if x=k then UNIV else A x)"
 
(*
definition
  setbrk :: "breakass ⇒ assigned ⇒ breakass set" where
  "setbrk b A = {b} ∪ {a| a. a∈ brk A ∧ lab a ≠ lab b}"
*)

definition
  range_inter_ts :: "('a,'b) tables  'b set" ("⇒⋂_" 80)
  where "⇒⋂A = {x |x.  k. x  A k}"

text ‹
In E⊢ B »t» A›,
B› denotes the ''assigned'' variables before evaluating term t›,
whereas A› denotes the ''assigned'' variables after evaluating term t›.
The environment termE is only needed for the conditional _ ? _ : _›.
The definite assignment rules refer to the typing rules here to
distinguish boolean and other expressions.
›

inductive
  da :: "env  lname set  term  assigned  bool" ("_ _ »_» _" [65,65,65,65] 71)
where
  Skip: "Env B »Skip» nrm=B,brk=λ l. UNIV"

| Expr: "Env B »e» A 
           
         Env B »Expr e» A"
| Lab:  "Env B »c» C; nrm A = nrm C  (brk C) l; brk A = rmlab l (brk C)
          
         Env B »Break l c» A" 

| Comp: "Env B »c1» C1; Env nrm C1 »c2» C2; 
         nrm A = nrm C2; brk A = (brk C1) ⇒∩ (brk C2) 
           
         Env B »c1;; c2» A"

| If:   "Env B »e» E;
          Env (B  assigns_if True  e) »c1» C1;
          Env (B  assigns_if False e) »c2» C2;
          nrm A = nrm C1  nrm C2;
          brk A = brk C1 ⇒∩ brk C2   
          
          Env B »If(e) c1 Else c2» A"

― ‹Note that termE is not further used, because we take the specialized
     sets that also consider if the expression evaluates to true or false. 
     Inside of terme there is no {\tt break} or {\tt finally}, so the break
     map of termE will be the trivial one. So 
     termEnvB »e» E is just used to ensure the definite assignment in
     expression terme.
     Notice the implicit analysis of a constant boolean expression terme
     in this rule. For example, if terme is constantly termTrue then 
     termassigns_if False e = UNIV and therefor termnrm C2=UNIV.
     So finally termnrm A = nrm C1. For the break maps this trick 
     workd too, because the trivial break map will map all labels to 
     termUNIV. In the example, if no break occurs in termc2 the break
     maps will trivially map to termUNIV and if a break occurs it will map
     to termUNIV too, because termassigns_if False e = UNIV. So
     in the intersection of the break maps the path termc2 will have no
     contribution.›

| Loop: "Env B »e» E; 
          Env (B  assigns_if True e) »c» C;
          nrm A = nrm C  (B  assigns_if False e);
          brk A = brk C  
          
          Env B »l While(e) c» A"
― ‹The Loop› rule resembles some of the ideas of the If› rule.
     For the termnrm A the set termB  assigns_if False e 
     will be termUNIV if the condition is constantly true. To normally exit
     the while loop, we must consider the body termc to be completed 
     normally (termnrm C) or with a break. But in this model, 
     the label terml of the loop
     only handles continue labels, not break labels. The break label will be
     handled by an enclosing termLab 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 B »Jmp jump» A"
― ‹In case of a break to label terml the corresponding break set is all
     variables assigned before the break. The assigned variables for normal
     completion of the termJmp is termUNIV, 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 B »e» E; nrm A = UNIV; brk A = (λ l. UNIV) 
          Env B »Throw e» A"

| Try:  "Env B »c1» C1; 
          Envlcl := (lcl Env)(VName vnClass C) (B  {VName vn}) »c2» C2;  
          nrm A = nrm C1  nrm C2;
          brk A = brk C1 ⇒∩ brk C2 
          Env B »Try c1 Catch(C vn) c2» A"

| Fin:  "Env B »c1» C1;
          Env B »c2» C2;
          nrm A = nrm C1  nrm C2;
          brk A = ((brk C1) ⇒∪ (nrm C2)) ⇒∩ (brk C2)  
          
          Env B »c1 Finally c2» A" 
― ‹The set of assigned variables before execution termc2 are the same
     as before execution termc1, because termc1 could throw an exception
     and so we can't guarantee that any variable will be assigned in termc1.
     The Finally› statement completes
     normally if both termc1 and termc2 complete normally. If termc1
     completes abruptly with a break, then termc2 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 termc2 terminates 
     normally we have to extend all break sets in termbrk C1 with 
     termnrm C2 (⇒∪). If termc2 exits with a break this
     break will appear in the overall result state. We don't know if 
     termc1 completed normally or abruptly (maybe with an exception not only
     a break) so termc1 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 termLab 
     or termLoop 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 FVar›, NewC› 
     and NewA›

| Init: "Env 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 termInit 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 B »NewC C» nrm=B,brk=λ l. UNIV" 

| NewA: "Env B »e» A 
         
         Env B »New T[e]» A"

| Cast: "Env B »e» A
         
         Env B »Cast T e» A"

| Inst: "Env B »e» A 
          
         Env B »e InstOf T» A"

| Lit:  "Env B »Lit v» nrm=B,brk=λ l. UNIV"

| UnOp: "Env B »e» A
          
         Env B »UnOp unop e» A"

| CondAnd: "Env B »e1» E1; Env (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 B »BinOp CondAnd e1 e2» A"

| CondOr: "Env B »e1» E1; Env (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 B »BinOp CondOr e1 e2» A"

| BinOp: "Env B »e1» E1; Env nrm E1 »e2» A; 
           binop  CondAnd; binop  CondOr
          
          Env B »BinOp binop e1 e2» A"

| Super: "This  B 
           
          Env B »Super» nrm=B,brk=λ l. UNIV"

| AccLVar: "vn  B;
             nrm A = B; brk A = (λ k. UNIV) 
              
             Env 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 termB

| Acc: " vn. v  LVar vn;
         Env B »v» A
         
         Env B »Acc v» A"

| AssLVar: "Env B »e» E; nrm A = nrm E  {vn}; brk A = brk E 
             
            Env B »(LVar vn) := e» A"

| Ass: " vn. v  LVar vn; Env B »v» V; Env nrm V »e» A
         
         Env B »v := e» A"

| CondBool: "Env(c ? e1 : e2)∷-(PrimT Boolean);
              Env B »c» C;
              Env (B  assigns_if True  c) »e1» E1;
              Env (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 B »c ? e1 : e2» A" 

| Cond: "¬ Env(c ? e1 : e2)∷-(PrimT Boolean);
          Env B »c» C;
          Env (B  assigns_if True  c) »e1» E1;
          Env (B  assigns_if False c) »e2» E2;
          nrm A = nrm E1  nrm E2; brk A = (λ l. UNIV)
           
          Env B »c ? e1 : e2» A" 

| Call: "Env B »e» E; Env nrm E »args» A 
           
         Env B »{accC,statT,mode}emn({pTs}args)» A"

― ‹The interplay of termCall, termMethd and termBody:
      Why rules for termMethd and termBody at all? Note that a
      Java source program will not include bare  termMethd or termBody
      terms. These terms are just introduced during evaluation. So definite
      assignment of termCall does not consider termMethd or 
      termBody at all. So for definite assignment alone we could omit the
      rules for termMethd and termBody. 
      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 termBody term to make sure that we can
      proof type safety. Also we must be able transport this information 
      from termCall to termMethd and then further to termBody 
      during evaluation to establish the definite assignment of termMethd
      during evaluation of termCall, and of termBody during evaluation
      of termMethd. 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 B »Body (declclass m) (stmt (mbody (mthd m)))» A
          
          
          Env B »Methd D sig» A" 

| Body: "Env B »c» C; jumpNestingOkS {Ret} c; Result  nrm C;
          nrm A = B; brk A = (λ l. UNIV)
         
         Env B »Body D c» A"
― ‹Note that termA is not correlated to  termC. If the body
      statement returns abruptly with return, evaluation of  termBody
      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 termJump rule ensures that the result variable is
      set and then this information must be carried over to the termBody
      rule by the conformance predicate of the state.›
| LVar: "Env B »LVar vn» nrm=B, brk=λ l. UNIV" 

| FVar: "Env B »e» A 
          
         Env B »{accC,statDeclC,stat}e..fn» A" 

| AVar: "Env B »e1» E1; Env nrm E1 »e2» A
           
          Env B »e1.[e2]» A" 

| Nil: "Env B »[]::expr list» nrm=B, brk=λ l. UNIV" 

| Cons: "Env B »e::expr» E; Env nrm E »es» A
          
         Env 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]
setup map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")

inductive_cases da_elim_cases [cases set]:
  "Env B »Skip» A" 
  "Env B »In1r Skip» A" 
  "Env B »Expr e» A"
  "Env B »In1r (Expr e)» A"
  "Env B »l c» A"
  "Env B »In1r (l c)» A"
  "Env B »c1;; c2» A"
  "Env B »In1r (c1;; c2)» A"
  "Env B »If(e) c1 Else c2» A" 
  "Env B »In1r (If(e) c1 Else c2)» A" 
  "Env B »l While(e) c» A"
  "Env B »In1r (l While(e) c)» A"  
  "Env B »Jmp jump» A"
  "Env B »In1r (Jmp jump)» A"
  "Env B »Throw e» A"
  "Env B »In1r (Throw e)» A"
  "Env B »Try c1 Catch(C vn) c2» A"
  "Env B »In1r (Try c1 Catch(C vn) c2)» A"
  "Env B »c1 Finally c2» A" 
  "Env B »In1r (c1 Finally c2)» A" 
  "Env B »Init C» A"
  "Env B »In1r (Init C)» A"
  "Env B »NewC C» A"
  "Env B »In1l (NewC C)» A"
  "Env B »New T[e]» A"
  "Env B »In1l (New T[e])» A"
  "Env B »Cast T e» A"
  "Env B »In1l (Cast T e)» A"
  "Env B »e InstOf T» A"
  "Env B »In1l (e InstOf T)» A"
  "Env B »Lit v» A"
  "Env B »In1l (Lit v)» A"
  "Env B »UnOp unop e» A"
  "Env B »In1l (UnOp unop e)» A"
  "Env B »BinOp binop e1 e2» A"
  "Env B »In1l (BinOp binop e1 e2)» A"
  "Env B »Super» A"
  "Env B »In1l (Super)» A"
  "Env B »Acc v» A"
  "Env B »In1l (Acc v)» A"
  "Env B »v := e» A"
  "Env B »In1l (v := e)» A"
  "Env B »c ? e1 : e2» A" 
  "Env B »In1l (c ? e1 : e2)» A" 
  "Env B »{accC,statT,mode}emn({pTs}args)» A"
  "Env B »In1l ({accC,statT,mode}emn({pTs}args))» A"
  "Env B »Methd C sig» A" 
  "Env B »In1l (Methd C sig)» A"
  "Env B »Body D c» A" 
  "Env B »In1l (Body D c)» A" 
  "Env B »LVar vn» A"
  "Env B »In2 (LVar vn)» A"
  "Env B »{accC,statDeclC,stat}e..fn» A" 
  "Env B »In2 ({accC,statDeclC,stat}e..fn)» A" 
  "Env B »e1.[e2]» A" 
  "Env B »In2 (e1.[e2])» A" 
  "Env B »[]::expr list» A"
  "Env B »In3 ([]::expr list)» A"
  "Env B »e#es» A"
  "Env 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]
setup map_theory_simpset (fn ctxt => ctxt 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 B »Skip» A"
  by (auto intro: da.Skip)

lemma da_NewC: "A = nrm=B,brk=λ l. UNIV  Env B »NewC C» A"
  by (auto intro: da.NewC)
 
lemma da_Lit:  "A = nrm=B,brk=λ l. UNIV  Env B »Lit v» A"
  by (auto intro: da.Lit)

lemma da_Super: "This  B;A = nrm=B,brk=λ l. UNIV  Env B »Super» A"
  by (auto intro: da.Super)

lemma da_Init: "A = nrm=B,brk=λ l. UNIV  Env 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: "Ee∷-PrimT Boolean" (is "?Boolean e")
   shows "assignsE e  assigns_if True e  assigns_if False e" (is "?Incl e")
proof -
  obtain vv where ex_lit: "ELit vv∷- PrimT Boolean"
    using typeof.simps(2) wt.Lit by blast
  have "?Boolean e  ?Incl e"
  proof (induct e)
    case (Cast T e)
    have "Ee∷- (PrimT Boolean)"
    proof -
      from E(Cast T e)∷- (PrimT Boolean)
      obtain Te where "Ee∷-Te"
                           "prg ETe≼? 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,
            (fastforce simp add: assignsE_const_simp)+)
  next
    case (BinOp binop e1 e2)
    from BinOp.prems obtain e1T e2T
      where "Ee1∷-e1T" and "Ee2∷-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)
    note hyp_c = ?Boolean c  ?Incl c
    note hyp_e1 = ?Boolean e1  ?Incl e1
    note hyp_e2 = ?Boolean e2  ?Incl e2
    note wt = E(c ? e1 : e2)∷-PrimT Boolean
    then obtain
      boolean_c:  "Ec∷-PrimT Boolean" and
      boolean_e1: "Ee1∷-PrimT Boolean" and
      boolean_e2: "Ee2∷-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
  next
    show "x. ELit vv∷-PrimT Boolean"
      by (rule ex_lit)
  qed (simp_all add: ex_lit)
  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]: "ll' (rmlab l A) l' = A l'"
  by (auto simp add: rmlab_def)

lemma range_inter_ts_subseteq [intro]: " k. A k  B k  ⇒⋂A  ⇒⋂B"
  by (auto simp add: range_inter_ts_def)

lemma range_inter_ts_subseteq': " k. A k  B k  x  ⇒⋂A  x  ⇒⋂B"
  by (auto simp add: range_inter_ts_def)

lemma da_monotone: 
  assumes da: "Env B  »t» A" and
    "B  B'" and
    da': "Env B' »t» A'" 
  shows "(nrm A  nrm A')  ( l. (brk A l  brk A' l))"
proof -
  from da
  have " B' A'. Env 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 
    then show ?case by cases simp
  next
    case Expr 
    from Expr.prems Expr.hyps 
    show ?case by cases simp
  next
    case (Lab Env B c C A l B' A')
    note A = nrm A = nrm C  brk C l brk A = rmlab l (brk C)
    note PROP ?Hyp Env B c C
    moreover
    note B  B'
    moreover
    obtain C'
      where "Env B' »c» C'"
        and A': "nrm A' = nrm C'  brk C' l" "brk A' = rmlab l (brk C')"
      using Lab.prems
      by 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 Env B c1 C1 c2 C2 A B' A')
    note A = nrm A = nrm C2 brk A = brk C1 ⇒∩  brk C2
    from Env B' »c1;; c2» A'
    obtain  C1' C2'
      where da_c1: "Env B' »c1» C1'" and
            da_c2: "Env nrm C1' »c2» C2'"  and
            A': "nrm A' = nrm C2'" "brk A' = brk C1' ⇒∩  brk C2'"
      by cases auto
    note PROP ?Hyp Env B c1 C1
    moreover note B  B'
    moreover note da_c1
    ultimately have C1': "nrm C1  nrm C1'" "(l. brk C1 l  brk C1' l)"
      by auto
    note 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 Env B e E c1 C1 c2 C2 A B' A')
    note A = nrm A = nrm C1  nrm C2 brk A = brk C1 ⇒∩  brk C2
    from Env B' »If(e) c1 Else c2» A'
    obtain C1' C2'
      where da_c1: "Env B'  assigns_if True e »c1» C1'" and
            da_c2: "Env B'  assigns_if False e »c2» C2'" and
               A': "nrm A' = nrm C1'  nrm C2'" "brk A' = brk C1' ⇒∩  brk C2'"
      by cases auto
    note PROP ?Hyp Env (B  assigns_if True e) c1 C1
    moreover note B' = B  B'
    moreover note da_c1 
    ultimately obtain C1': "nrm C1  nrm C1'" "(l. brk C1 l  brk C1' l)"
      by blast
    note 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 Env B e E c C A l B' A')
    note A = nrm A = nrm C  (B  assigns_if False e) brk A = brk C
    from Env B' »l While(e) c» A'
    obtain C'
      where 
       da_c': "Env B'  assigns_if True e »c» C'" and
          A': "nrm A' = nrm C'  (B'  assigns_if False e)"
              "brk A' = brk C'" 
      by cases auto
    note PROP ?Hyp Env (B  assigns_if True e) c C
    moreover note 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 jump B A Env B' A')
    thus ?case by (elim da_elim_cases) (auto split: jump.splits)
  next
    case Throw thus ?case by (elim da_elim_cases) auto
  next
    case (Try Env B c1 C1 vn C c2 C2 A B' A')
    note A = nrm A = nrm C1  nrm C2 brk A = brk C1 ⇒∩  brk C2
    from Env B' »Try c1 Catch(C vn) c2» A'
    obtain C1' C2'
      where da_c1': "Env B' »c1» C1'" and
            da_c2': "Envlcl := (lcl Env)(VName vnClass C) B'  {VName vn} 
                      »c2» C2'" and
            A': "nrm A' = nrm C1'  nrm C2'"
                "brk A' = brk C1' ⇒∩  brk C2'" 
      by cases auto
    note PROP ?Hyp Env B c1 C1
    moreover note B' = B  B'
    moreover note da_c1'
    ultimately obtain C1': "nrm C1  nrm C1'" "(l. brk C1 l  brk C1' l)"
      by blast
    note PROP ?Hyp (Envlcl := (lcl Env)(VName vnClass 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 Env B c1 C1 c2 C2 A B' A')
    note A = nrm A = nrm C1  nrm C2
      brk A = (brk C1 ⇒∪ nrm C2) ⇒∩ (brk C2)
    from Env B' »c1 Finally c2» A'
    obtain C1' C2'
      where  da_c1': "Env B' »c1» C1'" and
             da_c2': "Env B' »c2» C2'" and
             A':  "nrm A' = nrm C1'  nrm C2'"
                  "brk A' = (brk C1' ⇒∪ nrm C2') ⇒∩ (brk C2')"
      by cases auto
    note PROP ?Hyp Env B c1 C1
    moreover note B' = B  B'
    moreover note da_c1'
    ultimately obtain C1': "nrm C1  nrm C1'" "(l. brk C1 l  brk C1' l)"
      by blast
    note 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 (elim da_elim_cases) auto
   next
     case NewC thus ?case by (elim da_elim_cases) auto
   next
     case NewA thus ?case by (elim da_elim_cases) auto
   next
     case Cast thus ?case by (elim da_elim_cases) auto
   next
     case Inst thus ?case by (elim da_elim_cases) auto
   next
     case Lit thus ?case by (elim da_elim_cases) auto
   next
     case UnOp thus ?case by (elim da_elim_cases) auto
   next
     case (CondAnd Env B e1 E1 e2 E2 A B' A')
     note A = nrm A = B 
                       assigns_if True (BinOp CondAnd e1 e2) 
                       assigns_if False (BinOp CondAnd e1 e2)
             brk A = (λl. UNIV)
     from Env B' »BinOp CondAnd e1 e2» A'
     obtain  A': "nrm A' = B' 
                                 assigns_if True (BinOp CondAnd e1 e2) 
                                 assigns_if False (BinOp CondAnd e1 e2)"
                      "brk A' = (λl. UNIV)" 
       by cases auto
     note B' = B  B'
     with A A' show ?case 
       by auto 
   next
     case CondOr thus ?case by (elim da_elim_cases) auto
   next
     case BinOp thus ?case by (elim da_elim_cases) auto
   next
     case Super thus ?case by (elim da_elim_cases) auto
   next
     case AccLVar thus ?case by (elim da_elim_cases) auto
   next
     case Acc thus ?case by (elim da_elim_cases) auto
   next
     case AssLVar thus ?case by (elim da_elim_cases) auto
   next
     case Ass thus ?case by (elim da_elim_cases) auto
   next
     case (CondBool Env c e1 e2 B C E1 E2 A B' A')
     note A = nrm A = B  
                        assigns_if True (c ? e1 : e2)  
                        assigns_if False (c ? e1 : e2)
             brk A = (λl. UNIV)
     note Env (c ? e1 : e2)∷- (PrimT Boolean)
     moreover
     note Env 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 (elim da_elim_cases) (auto simp add: inj_term_simps) 
       (* inj_term_simps needed to handle wt (defined without ⟨⟩) *)
     note B' = B  B'
     with A A' show ?case 
       by auto 
   next
     case (Cond Env c e1 e2 B C E1 E2 A B' A')  
     note A = nrm A = nrm E1  nrm E2 brk A = (λl. UNIV)
     note not_bool = ¬ Env (c ? e1 : e2)∷- (PrimT Boolean)
     from Env B' »c ? e1 : e2» A'
     obtain E1' E2'
       where da_e1': "Env B'  assigns_if True c »e1» E1'" and
             da_e2': "Env B'  assigns_if False c »e2» E2'" and
                 A': "nrm A' = nrm E1'  nrm E2'"
                     "brk A' = (λl. UNIV)"
       using not_bool
       by (elim da_elim_cases) (auto simp add: inj_term_simps)
       (* inj_term_simps needed to handle wt (defined without ⟨⟩) *)
     note PROP ?Hyp Env (B  assigns_if True c) e1 E1
     moreover note B' = B  B'
     moreover note da_e1'
     ultimately obtain E1': "nrm E1  nrm E1'" "(l. brk E1 l  brk E1' l)"
       by blast
     note 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 (elim da_elim_cases) auto
  next
    case Body thus ?case by (elim da_elim_cases) auto
  next
    case LVar thus ?case by (elim da_elim_cases) auto
  next
    case FVar thus ?case by (elim da_elim_cases) auto
  next
    case AVar thus ?case by (elim da_elim_cases) auto
  next
    case Nil thus ?case by (elim da_elim_cases) auto
  next
    case Cons thus ?case by (elim da_elim_cases) auto
  qed
  from this [OF da' B  B'] show ?thesis .
qed
  
lemma da_weaken:     
  assumes da: "Env B »t» A" and "B  B'" 
  shows " A'. Env  B' »t» A'"
proof -
  note assigned.select_convs [Pure.intro]
  from da  
  have " B'. B  B'   A'. Env 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 Env B c C A l B')  
    note PROP ?Hyp Env B c
    moreover
    note B' = B  B'
    ultimately obtain C' where "Env B' »c» C'"
      by iprover
    then obtain A' where "Env B' »Break l c» A'"
      by (iprover intro: da.Lab)
    thus ?case ..
  next
    case (Comp Env B c1 C1 c2 C2 A B')
    note da_c1 = Env B »c1» C1
    note PROP ?Hyp Env B c1
    moreover
    note B' = B  B'
    ultimately obtain C1' where da_c1': "Env B' »c1» C1'"
      by iprover
    with da_c1 B'
    have
      "nrm C1  nrm C1'"
      by (rule da_monotone [elim_format]) simp
    moreover
    note PROP ?Hyp Env (nrm C1) c2
    ultimately obtain C2' where "Env nrm C1' »c2» C2'"
      by iprover
    with da_c1' obtain A' where "Env B' »c1;; c2» A'"
      by (iprover intro: da.Comp)
    thus ?case ..
  next
    case (If Env B e E c1 C1 c2 C2 A B')
    note B' = B  B'
    obtain  E' where "Env 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 (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 (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 B' »If(e) c1 Else c2» A'"
      by (iprover intro: da.If)
    thus ?case ..
  next  
    case (Loop Env B e E c C A l B')
    note B' = B  B'
    obtain E' where "Env 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 (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 B' »l While(e) c» A'"
      by (iprover intro: da.Loop )
    thus ?case ..
  next
    case (Jmp jump B A Env B') 
    note 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 B' »Jmp jump» A'"
      by (rule da.Jmp)
    thus ?case ..
  next
    case Throw thus ?case by (iprover intro: da.Throw )
  next
    case (Try Env B c1 C1 vn C c2 C2 A B')
    note B' = B  B'
    obtain C1' where "Env 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 
      "Envlcl := (lcl Env)(VName vnClass C) B'  {VName vn} »c2» C2'"
    proof -
      from B' have "B  {VName vn}  B'  {VName vn}" by blast
      moreover
      have "PROP ?Hyp (Envlcl := (lcl Env)(VName vnClass C)) 
                      (B  {VName vn}) c2" 
        by (rule Try.hyps)
      ultimately
      show ?thesis using that by iprover
    qed
    ultimately
    obtain A' where "Env B' »Try c1 Catch(C vn) c2» A'"
      by (iprover intro: da.Try )
    thus ?case ..
  next
    case (Fin Env B c1 C1 c2 C2 A B')
    note B' = B  B'
    obtain C1' where C1': "Env 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 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 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 Env B e1 E1 e2 E2 A B')
    note B' = B  B'
    obtain E1' where "Env 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 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 B' »BinOp CondAnd e1 e2» A'"
      by (iprover intro: da.CondAnd)
    thus ?case ..
  next
    case (CondOr Env B e1 E1 e2 E2 A B')
    note B' = B  B'
    obtain E1' where "Env 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 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 B' »BinOp CondOr e1 e2» A'"
      by (iprover intro: da.CondOr)
    thus ?case ..
  next
    case (BinOp Env B e1 E1 e2 A binop B')
    note B' = B  B'
    obtain E1' where E1': "Env 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 nrm E1' »e2» A'"
    proof -
      have "Env 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 B' »BinOp binop e1 e2» A'"
      using BinOp.hyps by (iprover intro: da.BinOp)
    thus ?case ..
  next
    case (Super B Env B')
    note B' = B  B'
    with Super.hyps have "This  B'"
      by auto
    thus ?case by (iprover intro: da.Super)
  next
    case (AccLVar vn B A Env B')
    note vn  B
    moreover
    note 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 Env B e E A vn B')
    note B' = B  B'
    then obtain E' where "Env B' »e» E'"
      by (rule AssLVar.hyps [elim_format]) iprover
    then obtain A' where  
      "Env B' »LVar vn:=e» A'"
      by (iprover intro: da.AssLVar)
    thus ?case ..
  next
    case (Ass v Env B V e A B') 
    note B' = B  B'
    note vn. v  LVar vn
    moreover
    obtain V' where V': "Env 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 nrm V' »e» A'"
    proof -
      have "Env 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 B' »v := e» A'"
      by (iprover intro: da.Ass)
    thus ?case ..
  next
    case (CondBool Env c e1 e2 B C E1 E2 A B')
    note B' = B  B'
    note Env(c ? e1 : e2)∷-(PrimT Boolean)
    moreover obtain C' where C': "Env 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 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 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 B' »c ? e1 : e2» A'"
      by (iprover intro: da.CondBool)
    thus ?case ..
  next
    case (Cond Env c e1 e2 B C E1 E2 A B')
    note B' = B  B'
    note ¬ Env(c ? e1 : e2)∷-(PrimT Boolean)
    moreover obtain C' where C': "Env 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 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 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 B' »c ? e1 : e2» A'"
      by (iprover intro: da.Cond)
    thus ?case ..
  next
    case (Call Env B e E args A accC statT mode mn pTs B')
    note B' = B  B'
    obtain E' where E': "Env 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 nrm E' »args» A'"
    proof -
      have "Env 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 B' »{accC,statT,mode}emn( {pTs}args)» A'"
      by (iprover intro: da.Call)
    thus ?case ..
  next
    case Methd thus ?case by (iprover intro: da.Methd)
  next
    case (Body Env B c C A D B')  
    note B' = B  B'
    obtain C' where C': "Env B' »c» C'" and nrm_C': "nrm C  nrm C'"
    proof -
      have "Env B »c» C" by (rule Body.hyps)
      moreover note B'
      moreover
      from B' obtain C' where da_c: "Env 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 
    note Result  nrm C
    with nrm_C' have "Result  nrm C'"
      by blast
    moreover note jumpNestingOkS {Ret} c
    ultimately obtain A' where
      "Env 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 Env B e1 E1 e2 A B')
    note B' = B  B'
    obtain E1' where E1': "Env 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 nrm E1' »e2» A'"
    proof -
      have "Env 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 B' »e1.[e2]» A'"
      by (iprover intro: da.AVar)
    thus ?case ..
  next
    case Nil thus ?case by (iprover intro: da.Nil)
  next
    case (Cons Env B e E es A B')
    note B' = B  B'
    obtain E' where E': "Env 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 nrm E' »es» A'"
    proof -
      have "Env 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 B' »e # es» A'"
      by (iprover intro: da.Cons)
    thus ?case ..
  qed
  from this [OF B  B'] show ?thesis .
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 B  »t» A"   and
                   B': "B  B'"          and
              ex_mono: " A'.  Env 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 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