src/HOL/Bali/DefiniteAssignment.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62042 6c6ccf573479
child 67443 3abf6a722518
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 subsection \<open>Definite Assignment\<close>
     2 
     3 theory DefiniteAssignment imports WellType begin 
     4 
     5 text \<open>Definite Assignment Analysis (cf. 16)
     6 
     7 The definite assignment analysis approximates the sets of local 
     8 variables that will be assigned at a certain point of evaluation, and ensures
     9 that we will only read variables which previously were assigned.
    10 It should conform to the following idea:
    11  If the evaluation of a term completes normally (no abruption (exception, 
    12 break, continue, return) appeared) , the set of local variables calculated 
    13 by the analysis is a subset of the
    14 variables that were actually assigned during evaluation.
    15 
    16 To get more precise information about the sets of assigned variables the 
    17 analysis includes the following optimisations:
    18 \begin{itemize}
    19   \item Inside of a while loop we also take care of the variables assigned
    20         before break statements, since the break causes the while loop to
    21         continue normally.
    22   \item For conditional statements we take care of constant conditions to 
    23         statically determine the path of evaluation.
    24   \item Inside a distinct path of a conditional statements we know to which
    25         boolean value the condition has evaluated to, and so can retrieve more
    26         information about the variables assigned during evaluation of the
    27         boolean condition.
    28 \end{itemize}
    29 
    30 Since in our model of Java the return values of methods are stored in a local
    31 variable we also ensure that every path of (normal) evaluation will assign the
    32 result variable, or in the sense of real Java every path ends up in and 
    33 return instruction. 
    34 
    35 Not covered yet:
    36 \begin{itemize} 
    37   \item analysis of definite unassigned
    38   \item special treatment of final fields
    39 \end{itemize}
    40 \<close>
    41 
    42 subsubsection \<open>Correct nesting of jump statements\<close>
    43 
    44 text \<open>For definite assignment it becomes crucial, that jumps (break, 
    45 continue, return) are nested correctly i.e. a continue jump is nested in a
    46 matching while statement, a break jump is nested in a proper label statement,
    47 a class initialiser does not terminate abruptly with a return. With this we 
    48 can for example ensure that evaluation of an expression will never end up 
    49 with a jump, since no breaks, continues or returns are allowed in an 
    50 expression.\<close>
    51 
    52 primrec jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
    53 where
    54   "jumpNestingOkS jmps (Skip)   = True"
    55 | "jumpNestingOkS jmps (Expr e) = True"
    56 | "jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
    57 | "jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> 
    58                                    jumpNestingOkS jmps c2)"
    59 | "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>  
    60                                              jumpNestingOkS jmps c2)"
    61 | "jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
    62 \<comment>\<open>The label of the while loop only handles continue jumps. Breaks are only
    63      handled by @{term Lab}\<close>
    64 | "jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
    65 | "jumpNestingOkS jmps (Throw e) = True"
    66 | "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> 
    67                                                   jumpNestingOkS jmps c2)"
    68 | "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> 
    69                                           jumpNestingOkS jmps c2)"
    70 | "jumpNestingOkS jmps (Init C) = True" 
    71  \<comment>\<open>wellformedness of the program must enshure that for all initializers 
    72       jumpNestingOkS {} holds\<close> 
    73 \<comment>\<open>Dummy analysis for intermediate smallstep term @{term  FinA}\<close>
    74 | "jumpNestingOkS jmps (FinA a c) = False"
    75 
    76 
    77 definition jumpNestingOk :: "jump set \<Rightarrow> term \<Rightarrow> bool" where
    78 "jumpNestingOk jmps t = (case t of
    79                       In1 se \<Rightarrow> (case se of
    80                                    Inl e \<Rightarrow> True
    81                                  | Inr s \<Rightarrow> jumpNestingOkS jmps s)
    82                     | In2  v \<Rightarrow> True
    83                     | In3  es \<Rightarrow> True)"
    84 
    85 lemma jumpNestingOk_expr_simp [simp]: "jumpNestingOk jmps (In1l e) = True"
    86 by (simp add: jumpNestingOk_def)
    87 
    88 lemma jumpNestingOk_expr_simp1 [simp]: "jumpNestingOk jmps \<langle>e::expr\<rangle> = True"
    89 by (simp add: inj_term_simps)
    90 
    91 lemma jumpNestingOk_stmt_simp [simp]: 
    92   "jumpNestingOk jmps (In1r s) = jumpNestingOkS jmps s"
    93 by (simp add: jumpNestingOk_def)
    94 
    95 lemma jumpNestingOk_stmt_simp1 [simp]: 
    96    "jumpNestingOk jmps \<langle>s::stmt\<rangle> = jumpNestingOkS jmps s"
    97 by (simp add: inj_term_simps)
    98 
    99 lemma jumpNestingOk_var_simp [simp]: "jumpNestingOk jmps (In2 v) = True"
   100 by (simp add: jumpNestingOk_def)
   101 
   102 lemma jumpNestingOk_var_simp1 [simp]: "jumpNestingOk jmps \<langle>v::var\<rangle> = True"
   103 by (simp add: inj_term_simps)
   104 
   105 lemma jumpNestingOk_expr_list_simp [simp]: "jumpNestingOk jmps (In3 es) = True"
   106 by (simp add: jumpNestingOk_def)
   107 
   108 lemma jumpNestingOk_expr_list_simp1 [simp]: 
   109   "jumpNestingOk jmps \<langle>es::expr list\<rangle> = True"
   110 by (simp add: inj_term_simps)
   111 
   112 
   113 
   114 subsubsection \<open>Calculation of assigned variables for boolean expressions\<close>
   115 
   116 
   117 subsection \<open>Very restricted calculation fallback calculation\<close>
   118 
   119 primrec the_LVar_name :: "var \<Rightarrow> lname"
   120   where "the_LVar_name (LVar n) = n"
   121 
   122 primrec assignsE :: "expr \<Rightarrow> lname set" 
   123   and assignsV :: "var \<Rightarrow> lname set"
   124   and assignsEs:: "expr list \<Rightarrow> lname set"
   125 where
   126   "assignsE (NewC c)            = {}" 
   127 | "assignsE (NewA t e)          = assignsE e"
   128 | "assignsE (Cast t e)          = assignsE e"
   129 | "assignsE (e InstOf r)        = assignsE e"
   130 | "assignsE (Lit val)           = {}"
   131 | "assignsE (UnOp unop e)       = assignsE e"
   132 | "assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
   133                                        then (assignsE e1)
   134                                        else (assignsE e1) \<union> (assignsE e2))" 
   135 | "assignsE (Super)             = {}"
   136 | "assignsE (Acc v)             = assignsV v"
   137 | "assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union> 
   138                                    (if \<exists> n. v=(LVar n) then {the_LVar_name v} 
   139                                                        else {})"
   140 | "assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
   141 | "assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) 
   142                             = (assignsE objRef) \<union> (assignsEs args)"
   143 \<comment> \<open>Only dummy analysis for intermediate expressions  
   144       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee}\<close>
   145 | "assignsE (Methd C sig)   = {}" 
   146 | "assignsE (Body  C s)     = {}"   
   147 | "assignsE (InsInitE s e)  = {}"  
   148 | "assignsE (Callee l e)    = {}" 
   149 
   150 | "assignsV (LVar n)       = {}"
   151 | "assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
   152 | "assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"
   153 
   154 | "assignsEs     [] = {}"
   155 | "assignsEs (e#es) = assignsE e \<union> assignsEs es"
   156 
   157 definition assigns :: "term \<Rightarrow> lname set" where
   158 "assigns t = (case t of
   159                 In1 se \<Rightarrow> (case se of
   160                              Inl e \<Rightarrow> assignsE e
   161                            | Inr s \<Rightarrow> {})
   162               | In2  v \<Rightarrow> assignsV v
   163               | In3  es \<Rightarrow> assignsEs es)"
   164 
   165 lemma assigns_expr_simp [simp]: "assigns (In1l e) = assignsE e"
   166 by (simp add: assigns_def)
   167 
   168 lemma assigns_expr_simp1 [simp]: "assigns (\<langle>e\<rangle>) = assignsE e"
   169 by (simp add: inj_term_simps)
   170 
   171 lemma assigns_stmt_simp [simp]: "assigns (In1r s) = {}"
   172 by (simp add: assigns_def)
   173 
   174 lemma assigns_stmt_simp1 [simp]: "assigns (\<langle>s::stmt\<rangle>) = {}"
   175 by (simp add: inj_term_simps)
   176 
   177 lemma assigns_var_simp [simp]: "assigns (In2 v) = assignsV v"
   178 by (simp add: assigns_def)
   179 
   180 lemma assigns_var_simp1 [simp]: "assigns (\<langle>v\<rangle>) = assignsV v"
   181 by (simp add: inj_term_simps)
   182 
   183 lemma assigns_expr_list_simp [simp]: "assigns (In3 es) = assignsEs es"
   184 by (simp add: assigns_def)
   185 
   186 lemma assigns_expr_list_simp1 [simp]: "assigns (\<langle>es\<rangle>) = assignsEs es"
   187 by (simp add: inj_term_simps)
   188 
   189 subsection "Analysis of constant expressions"
   190 
   191 primrec constVal :: "expr \<Rightarrow> val option"
   192 where
   193   "constVal (NewC c)      = None"
   194 | "constVal (NewA t e)    = None"
   195 | "constVal (Cast t e)    = None"
   196 | "constVal (Inst e r)    = None"
   197 | "constVal (Lit val)     = Some val"
   198 | "constVal (UnOp unop e) = (case (constVal e) of
   199                                None   \<Rightarrow> None
   200                              | Some v \<Rightarrow> Some (eval_unop unop v))" 
   201 | "constVal (BinOp binop e1 e2) = (case (constVal e1) of
   202                                      None    \<Rightarrow> None
   203                                    | Some v1 \<Rightarrow> (case (constVal e2) of 
   204                                                   None    \<Rightarrow> None
   205                                                 | Some v2 \<Rightarrow> Some (eval_binop 
   206                                                                    binop v1 v2)))"
   207 | "constVal (Super)         = None"
   208 | "constVal (Acc v)         = None"
   209 | "constVal (Ass v e)       = None"
   210 | "constVal (Cond b e1 e2)  = (case (constVal b) of
   211                                  None   \<Rightarrow> None
   212                                | Some bv\<Rightarrow> (case the_Bool bv of
   213                                               True \<Rightarrow> (case (constVal e2) of
   214                                                          None   \<Rightarrow> None
   215                                                        | Some v \<Rightarrow> constVal e1)
   216                                             | False\<Rightarrow> (case (constVal e1) of
   217                                                          None   \<Rightarrow> None
   218                                                        | Some v \<Rightarrow> constVal e2)))"
   219 \<comment>\<open>Note that \<open>constVal (Cond b e1 e2)\<close> is stricter as it could be.
   220      It requires that all tree expressions are constant even if we can decide
   221      which branch to choose, provided the constant value of @{term b}\<close>
   222 | "constVal (Call accC statT mode objRef mn pTs args) = None"
   223 | "constVal (Methd C sig)   = None" 
   224 | "constVal (Body  C s)     = None"   
   225 | "constVal (InsInitE s e)  = None"  
   226 | "constVal (Callee l e)    = None" 
   227 
   228 lemma constVal_Some_induct [consumes 1, case_names Lit UnOp BinOp CondL CondR]: 
   229   assumes const: "constVal e = Some v" and
   230         hyp_Lit: "\<And> v. P (Lit v)" and
   231        hyp_UnOp: "\<And> unop e'. P e' \<Longrightarrow> P (UnOp unop e')" and
   232       hyp_BinOp: "\<And> binop e1 e2. \<lbrakk>P e1; P e2\<rbrakk> \<Longrightarrow> P (BinOp binop e1 e2)" and
   233       hyp_CondL: "\<And> b bv e1 e2. \<lbrakk>constVal b = Some bv; the_Bool bv; P b; P e1\<rbrakk> 
   234                               \<Longrightarrow> P (b? e1 : e2)" and
   235       hyp_CondR: "\<And> b bv e1 e2. \<lbrakk>constVal b = Some bv; \<not>the_Bool bv; P b; P e2\<rbrakk>
   236                               \<Longrightarrow> P (b? e1 : e2)"
   237   shows "P e"
   238 proof -
   239   have "\<And> v. constVal e = Some v \<Longrightarrow> P e"
   240   proof (induct e)
   241     case Lit
   242     show ?case by (rule hyp_Lit)
   243   next
   244     case UnOp
   245     thus ?case
   246       by (auto intro: hyp_UnOp)
   247   next
   248     case BinOp
   249     thus ?case
   250       by (auto intro: hyp_BinOp)
   251   next
   252     case (Cond b e1 e2)
   253     then obtain v where   v: "constVal (b ? e1 : e2) = Some v"
   254       by blast
   255     then obtain bv where bv: "constVal b = Some bv"
   256       by simp
   257     show ?case
   258     proof (cases "the_Bool bv")
   259       case True
   260       with Cond show ?thesis using v bv
   261         by (auto intro: hyp_CondL)
   262     next
   263       case False
   264       with Cond show ?thesis using v bv
   265         by (auto intro: hyp_CondR)
   266     qed
   267   qed (simp_all add: hyp_Lit)
   268   with const 
   269   show ?thesis
   270     by blast  
   271 qed
   272 
   273 lemma assignsE_const_simp: "constVal e = Some v \<Longrightarrow> assignsE e = {}"
   274   by (induct rule: constVal_Some_induct) simp_all
   275 
   276 
   277 subsection \<open>Main analysis for boolean expressions\<close>
   278 
   279 text \<open>Assigned local variables after evaluating the expression if it evaluates
   280 to a specific boolean value. If the expression cannot evaluate to a 
   281 @{term Boolean} value UNIV is returned. If we expect true/false the opposite 
   282 constant false/true will also lead to UNIV.\<close>
   283 primrec assigns_if :: "bool \<Rightarrow> expr \<Rightarrow> lname set"
   284 where
   285   "assigns_if b (NewC c)            = UNIV" \<comment>\<open>can never evaluate to Boolean\<close> 
   286 | "assigns_if b (NewA t e)          = UNIV" \<comment>\<open>can never evaluate to Boolean\<close>
   287 | "assigns_if b (Cast t e)          = assigns_if b e" 
   288 | "assigns_if b (Inst e r)          = assignsE e" \<comment>\<open>Inst has type Boolean but
   289                                                        e is a reference type\<close>
   290 | "assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"  
   291 | "assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
   292                                            None   \<Rightarrow> (if unop = UNot 
   293                                                          then assigns_if (\<not>b) e
   294                                                          else UNIV)
   295                                          | Some v \<Rightarrow> (if v=Bool b 
   296                                                          then {} 
   297                                                          else UNIV))"
   298 | "assigns_if b (BinOp binop e1 e2) 
   299     = (case constVal (BinOp binop e1 e2) of
   300          None \<Rightarrow> (if binop=CondAnd then
   301                      (case b of 
   302                          True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2
   303                       |  False \<Rightarrow> assigns_if False e1 \<inter> 
   304                                   (assigns_if True e1 \<union> assigns_if False e2))
   305                   else
   306                  (if binop=CondOr then
   307                      (case b of 
   308                          True  \<Rightarrow> assigns_if True e1 \<inter> 
   309                                   (assigns_if False e1 \<union> assigns_if True e2)
   310                       |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)
   311                   else assignsE e1 \<union> assignsE e2))
   312        | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
   313 
   314 | "assigns_if b (Super)      = UNIV" \<comment>\<open>can never evaluate to Boolean\<close>
   315 | "assigns_if b (Acc v)      = (assignsV v)"
   316 | "assigns_if b (v := e)     = (assignsE (Ass v e))"
   317 | "assigns_if b (c? e1 : e2) = (assignsE c) \<union>
   318                                  (case (constVal c) of
   319                                     None    \<Rightarrow> (assigns_if b e1) \<inter> 
   320                                                (assigns_if b e2)
   321                                   | Some bv \<Rightarrow> (case the_Bool bv of
   322                                                   True  \<Rightarrow> assigns_if b e1
   323                                                 | False \<Rightarrow> assigns_if b e2))"
   324 | "assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))  
   325             = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
   326 \<comment> \<open>Only dummy analysis for intermediate expressions  
   327       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee}\<close>
   328 | "assigns_if b (Methd C sig)   = {}" 
   329 | "assigns_if b (Body  C s)     = {}"   
   330 | "assigns_if b (InsInitE s e)  = {}"  
   331 | "assigns_if b (Callee l e)    = {}" 
   332 
   333 lemma assigns_if_const_b_simp:
   334   assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")
   335   shows   "assigns_if b e = {}" (is "?Ass b e")
   336 proof -
   337   have "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e"
   338   proof (induct e)
   339     case Lit
   340     thus ?case by simp
   341   next
   342     case UnOp 
   343     thus ?case by simp
   344   next 
   345     case (BinOp binop)
   346     thus ?case
   347       by (cases binop) (simp_all)
   348   next
   349     case (Cond c e1 e2 b)
   350     note hyp_c = \<open>\<And> b. ?Const b c \<Longrightarrow> ?Ass b c\<close>
   351     note hyp_e1 = \<open>\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1\<close>
   352     note hyp_e2 = \<open>\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2\<close>
   353     note const = \<open>constVal (c ? e1 : e2) = Some (Bool b)\<close>
   354     then obtain bv where bv: "constVal c = Some bv"
   355       by simp
   356     hence emptyC: "assignsE c = {}" by (rule assignsE_const_simp)
   357     show ?case
   358     proof (cases "the_Bool bv")
   359       case True
   360       with const bv  
   361       have "?Const b e1" by simp
   362       hence "?Ass b e1" by (rule hyp_e1)
   363       with emptyC bv True
   364       show ?thesis
   365         by simp
   366     next
   367       case False
   368       with const bv  
   369       have "?Const b e2" by simp
   370       hence "?Ass b e2" by (rule hyp_e2)
   371       with emptyC bv False
   372       show ?thesis
   373         by simp
   374     qed
   375   qed (simp_all)
   376   with boolConst
   377   show ?thesis
   378     by blast
   379 qed
   380 
   381 lemma assigns_if_const_not_b_simp:
   382   assumes boolConst: "constVal e = Some (Bool b)"        (is "?Const b e")  
   383   shows "assigns_if (\<not>b) e = UNIV"                  (is "?Ass b e")
   384 proof -
   385   have "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e"
   386   proof (induct e)
   387     case Lit
   388     thus ?case by simp
   389   next
   390     case UnOp 
   391     thus ?case by simp
   392   next 
   393     case (BinOp binop)
   394     thus ?case
   395       by (cases binop) (simp_all)
   396   next
   397     case (Cond c e1 e2 b)
   398     note hyp_c = \<open>\<And> b. ?Const b c \<Longrightarrow> ?Ass b c\<close>
   399     note hyp_e1 = \<open>\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1\<close>
   400     note hyp_e2 = \<open>\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2\<close>
   401     note const = \<open>constVal (c ? e1 : e2) = Some (Bool b)\<close>
   402     then obtain bv where bv: "constVal c = Some bv"
   403       by simp
   404     show ?case
   405     proof (cases "the_Bool bv")
   406       case True
   407       with const bv  
   408       have "?Const b e1" by simp
   409       hence "?Ass b e1" by (rule hyp_e1)
   410       with bv True
   411       show ?thesis
   412         by simp
   413     next
   414       case False
   415       with const bv  
   416       have "?Const b e2" by simp
   417       hence "?Ass b e2" by (rule hyp_e2)
   418       with bv False 
   419       show ?thesis
   420         by simp
   421     qed
   422   qed (simp_all)
   423   with boolConst
   424   show ?thesis
   425     by blast
   426 qed
   427 
   428 subsection \<open>Lifting set operations to range of tables (map to a set)\<close>
   429 
   430 definition
   431   union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65)
   432   where "A \<Rightarrow>\<union> B = (\<lambda> k. A k \<union> B k)"
   433 
   434 definition
   435   intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter>  _" [72,72] 71)
   436   where "A \<Rightarrow>\<inter>  B = (\<lambda>k. A k \<inter> B k)"
   437 
   438 definition
   439   all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40)
   440   where "(A \<Rightarrow>\<union>\<^sub>\<forall> B) = (\<lambda> k. A k \<union> B)"
   441   
   442 subsubsection \<open>Binary union of tables\<close>
   443 
   444 lemma union_ts_iff [simp]: "(c \<in> (A \<Rightarrow>\<union> B) k) = (c \<in> A k \<or>  c \<in> B k)"
   445   by (unfold union_ts_def) blast
   446 
   447 lemma union_tsI1 [elim?]: "c \<in> A k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k"
   448   by simp
   449 
   450 lemma union_tsI2 [elim?]: "c \<in> B k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k"
   451   by simp
   452 
   453 lemma union_tsCI [intro!]: "(c \<notin> B k \<Longrightarrow> c \<in> A k) \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k"
   454   by auto
   455 
   456 lemma union_tsE [elim!]: 
   457  "\<lbrakk>c \<in> (A \<Rightarrow>\<union> B) k; (c \<in> A k \<Longrightarrow> P); (c \<in> B k \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
   458   by (unfold union_ts_def) blast
   459 
   460 subsubsection \<open>Binary intersection of tables\<close>
   461 
   462 lemma intersect_ts_iff [simp]: "c \<in> (A \<Rightarrow>\<inter> B) k = (c \<in> A k \<and> c \<in> B k)"
   463   by (unfold intersect_ts_def) blast
   464 
   465 lemma intersect_tsI [intro!]: "\<lbrakk>c \<in> A k; c \<in> B k\<rbrakk> \<Longrightarrow> c \<in>  (A \<Rightarrow>\<inter> B) k"
   466   by simp
   467 
   468 lemma intersect_tsD1: "c \<in> (A \<Rightarrow>\<inter> B) k \<Longrightarrow> c \<in> A k"
   469   by simp
   470 
   471 lemma intersect_tsD2: "c \<in> (A \<Rightarrow>\<inter> B) k \<Longrightarrow> c \<in> B k"
   472   by simp
   473 
   474 lemma intersect_tsE [elim!]: 
   475    "\<lbrakk>c \<in> (A \<Rightarrow>\<inter> B) k; \<lbrakk>c \<in> A k; c \<in> B k\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   476   by simp
   477 
   478 
   479 subsubsection \<open>All-Union of tables and set\<close>
   480 
   481 lemma all_union_ts_iff [simp]: "(c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k) = (c \<in> A k \<or>  c \<in> B)"
   482   by (unfold all_union_ts_def) blast
   483 
   484 lemma all_union_tsI1 [elim?]: "c \<in> A k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k"
   485   by simp
   486 
   487 lemma all_union_tsI2 [elim?]: "c \<in> B \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k"
   488   by simp
   489 
   490 lemma all_union_tsCI [intro!]: "(c \<notin> B \<Longrightarrow> c \<in> A k) \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k"
   491   by auto
   492 
   493 lemma all_union_tsE [elim!]: 
   494  "\<lbrakk>c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k; (c \<in> A k \<Longrightarrow> P); (c \<in> B \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
   495   by (unfold all_union_ts_def) blast
   496 
   497 
   498 subsubsection "The rules of definite assignment"
   499 
   500  
   501 type_synonym breakass = "(label, lname) tables" 
   502 \<comment>\<open>Mapping from a break label, to the set of variables that will be assigned 
   503      if the evaluation terminates with this break\<close>
   504     
   505 record assigned = 
   506          nrm :: "lname set" \<comment>\<open>Definetly assigned variables 
   507                                  for normal completion\<close>
   508          brk :: "breakass" \<comment>\<open>Definetly assigned variables for 
   509                                 abrupt completion with a break\<close>
   510 
   511 definition
   512   rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
   513   where "rmlab k A = (\<lambda>x. if x=k then UNIV else A x)"
   514  
   515 (*
   516 definition
   517   setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
   518   "setbrk b A = {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
   519 *)
   520 
   521 definition
   522   range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80)
   523   where "\<Rightarrow>\<Inter>A = {x |x. \<forall> k. x \<in> A k}"
   524 
   525 text \<open>
   526 In \<open>E\<turnstile> B \<guillemotright>t\<guillemotright> A\<close>,
   527 \<open>B\<close> denotes the ''assigned'' variables before evaluating term \<open>t\<close>,
   528 whereas \<open>A\<close> denotes the ''assigned'' variables after evaluating term \<open>t\<close>.
   529 The environment @{term E} is only needed for the conditional \<open>_ ? _ : _\<close>.
   530 The definite assignment rules refer to the typing rules here to
   531 distinguish boolean and other expressions.
   532 \<close>
   533 
   534 inductive
   535   da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71)
   536 where
   537   Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
   538 
   539 | Expr: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A 
   540          \<Longrightarrow>  
   541          Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"
   542 | Lab:  "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; nrm A = nrm C \<inter> (brk C) l; brk A = rmlab l (brk C)\<rbrakk>
   543          \<Longrightarrow> 
   544          Env\<turnstile> B \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A" 
   545 
   546 | Comp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; 
   547          nrm A = nrm C2; brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)\<rbrakk> 
   548          \<Longrightarrow>  
   549          Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A"
   550 
   551 | If:   "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E;
   552           Env\<turnstile> (B \<union> assigns_if True  e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
   553           Env\<turnstile> (B \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
   554           nrm A = nrm C1 \<inter> nrm C2;
   555           brk A = brk C1 \<Rightarrow>\<inter> brk C2 \<rbrakk>  
   556           \<Longrightarrow>
   557           Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A"
   558 
   559 \<comment>\<open>Note that @{term E} is not further used, because we take the specialized
   560      sets that also consider if the expression evaluates to true or false. 
   561      Inside of @{term e} there is no {\tt break} or {\tt finally}, so the break
   562      map of @{term E} will be the trivial one. So 
   563      @{term "Env\<turnstile>B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"} is just used to ensure the definite assignment in
   564      expression @{term e}.
   565      Notice the implicit analysis of a constant boolean expression @{term e}
   566      in this rule. For example, if @{term e} is constantly @{term True} then 
   567      @{term "assigns_if False e = UNIV"} and therefor @{term "nrm C2=UNIV"}.
   568      So finally @{term "nrm A = nrm C1"}. For the break maps this trick 
   569      workd too, because the trival break map will map all labels to 
   570      @{term UNIV}. In the example, if no break occurs in @{term c2} the break
   571      maps will trivially map to @{term UNIV} and if a break occurs it will map
   572      to @{term UNIV} too, because @{term "assigns_if False e = UNIV"}. So
   573      in the intersection of the break maps the path @{term c2} will have no
   574      contribution.
   575 \<close>
   576 
   577 | Loop: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; 
   578           Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
   579           nrm A = nrm C \<inter> (B \<union> assigns_if False e);
   580           brk A = brk C\<rbrakk>  
   581           \<Longrightarrow>
   582           Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"
   583 \<comment>\<open>The \<open>Loop\<close> rule resembles some of the ideas of the \<open>If\<close> rule.
   584      For the @{term "nrm A"} the set @{term "B \<union> assigns_if False e"} 
   585      will be @{term UNIV} if the condition is constantly true. To normally exit
   586      the while loop, we must consider the body @{term c} to be completed 
   587      normally (@{term "nrm C"}) or with a break. But in this model, 
   588      the label @{term l} of the loop
   589      only handles continue labels, not break labels. The break label will be
   590      handled by an enclosing @{term Lab} statement. So we don't have to
   591      handle the breaks specially. 
   592 \<close>
   593 
   594 | Jmp: "\<lbrakk>jump=Ret \<longrightarrow> Result \<in> B;
   595          nrm A = UNIV;
   596          brk A = (case jump of
   597                     Break l \<Rightarrow> \<lambda> k. if k=l then B else UNIV     
   598                   | Cont l  \<Rightarrow> \<lambda> k. UNIV
   599                   | Ret     \<Rightarrow> \<lambda> k. UNIV)\<rbrakk> 
   600         \<Longrightarrow> 
   601         Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A"
   602 \<comment>\<open>In case of a break to label @{term l} the corresponding break set is all
   603      variables assigned before the break. The assigned variables for normal
   604      completion of the @{term Jmp} is @{term UNIV}, because the statement will
   605      never complete normally. For continue and return the break map is the 
   606      trivial one. In case of a return we enshure that the result value is
   607      assigned.
   608 \<close>
   609 
   610 | Throw: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = UNIV; brk A = (\<lambda> l. UNIV)\<rbrakk> 
   611          \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"
   612 
   613 | Try:  "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; 
   614           Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;  
   615           nrm A = nrm C1 \<inter> nrm C2;
   616           brk A = brk C1 \<Rightarrow>\<inter> brk C2\<rbrakk> 
   617          \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A"
   618 
   619 | Fin:  "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
   620           Env\<turnstile> B \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
   621           nrm A = nrm C1 \<union> nrm C2;
   622           brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)\<rbrakk>  
   623           \<Longrightarrow>
   624           Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A" 
   625 \<comment>\<open>The set of assigned variables before execution @{term c2} are the same
   626      as before execution @{term c1}, because @{term c1} could throw an exception
   627      and so we can't guarantee that any variable will be assigned in @{term c1}.
   628      The \<open>Finally\<close> statement completes
   629      normally if both @{term c1} and @{term c2} complete normally. If @{term c1}
   630      completes abruptly with a break, then @{term c2} also will be executed 
   631      and may terminate normally or with a break. The overall break map then is
   632      the intersection of the maps of both paths. If @{term c2} terminates 
   633      normally we have to extend all break sets in @{term "brk C1"} with 
   634      @{term "nrm C2"} (\<open>\<Rightarrow>\<union>\<^sub>\<forall>\<close>). If @{term c2} exits with a break this
   635      break will appear in the overall result state. We don't know if 
   636      @{term c1} completed normally or abruptly (maybe with an exception not only
   637      a break) so @{term c1} has no contribution to the break map following this
   638      path.
   639 \<close>
   640 
   641 \<comment>\<open>Evaluation of expressions and the break sets of definite assignment:
   642      Thinking of a Java expression we assume that we can never have
   643      a break statement inside of a expression. So for all expressions the
   644      break sets could be set to the trivial one: @{term "\<lambda> l. UNIV"}. 
   645      But we can't
   646      trivially proof, that evaluating an expression will never result in a 
   647      break, allthough Java expressions allready syntactically don't allow
   648      nested stetements in them. The reason are the nested class initialzation 
   649      statements which are inserted by the evaluation rules. So to proof the
   650      absence of a break we need to ensure, that the initialization statements
   651      will never end up in a break. In a wellfromed initialization statement, 
   652      of course, were breaks are nested correctly inside of @{term Lab} 
   653      or @{term Loop} statements evaluation of the whole initialization 
   654      statement will never result in a break, because this break will be 
   655      handled inside of the statement. But for simplicity we haven't added
   656      the analysis of the correct nesting of breaks in the typing judgments 
   657      right now. So we have decided to adjust the rules of definite assignment
   658      to fit to these circumstances. If an initialization is involved during
   659      evaluation of the expression (evaluation rules \<open>FVar\<close>, \<open>NewC\<close> 
   660      and \<open>NewA\<close>
   661 \<close>
   662 
   663 | Init: "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
   664 \<comment>\<open>Wellformedness of a program will ensure, that every static initialiser 
   665      is definetly assigned and the jumps are nested correctly. The case here
   666      for @{term Init} is just for convenience, to get a proper precondition 
   667      for the induction hypothesis in various proofs, so that we don't have to
   668      expand the initialisation on every point where it is triggerred by the
   669      evaluation rules.
   670 \<close>   
   671 | NewC: "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" 
   672 
   673 | NewA: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A 
   674          \<Longrightarrow>
   675          Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A"
   676 
   677 | Cast: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
   678          \<Longrightarrow>
   679          Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A"
   680 
   681 | Inst: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A 
   682          \<Longrightarrow> 
   683          Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A"
   684 
   685 | Lit:  "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
   686 
   687 | UnOp: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
   688          \<Longrightarrow> 
   689          Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A"
   690 
   691 | CondAnd: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if True e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; 
   692              nrm A = B \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter> 
   693                              assigns_if False (BinOp CondAnd e1 e2));
   694              brk A = (\<lambda> l. UNIV) \<rbrakk>
   695             \<Longrightarrow>
   696             Env\<turnstile> B \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A"
   697 
   698 | CondOr: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if False e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; 
   699             nrm A = B \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter> 
   700                               assigns_if False (BinOp CondOr e1 e2));
   701             brk A = (\<lambda> l. UNIV) \<rbrakk>
   702             \<Longrightarrow>
   703             Env\<turnstile> B \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A"
   704 
   705 | BinOp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A; 
   706            binop \<noteq> CondAnd; binop \<noteq> CondOr\<rbrakk>
   707           \<Longrightarrow>
   708           Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A"
   709 
   710 | Super: "This \<in> B 
   711           \<Longrightarrow> 
   712           Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
   713 
   714 | AccLVar: "\<lbrakk>vn \<in> B;
   715              nrm A = B; brk A = (\<lambda> k. UNIV)\<rbrakk> 
   716              \<Longrightarrow> 
   717              Env\<turnstile> B \<guillemotright>\<langle>Acc (LVar vn)\<rangle>\<guillemotright> A"
   718 \<comment>\<open>To properly access a local variable we have to test the definite 
   719      assignment here. The variable must occur in the set @{term B} 
   720 \<close>
   721 
   722 | Acc: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn;
   723          Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> A\<rbrakk>
   724          \<Longrightarrow>
   725          Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A"
   726 
   727 | AssLVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = nrm E \<union> {vn}; brk A = brk E\<rbrakk> 
   728             \<Longrightarrow> 
   729             Env\<turnstile> B \<guillemotright>\<langle>(LVar vn) := e\<rangle>\<guillemotright> A"
   730 
   731 | Ass: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn; Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V; Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A\<rbrakk>
   732          \<Longrightarrow>
   733          Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A"
   734 
   735 | CondBool: "\<lbrakk>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean);
   736               Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
   737               Env\<turnstile> (B \<union> assigns_if True  c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1;
   738               Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
   739               nrm A = B \<union> (assigns_if True  (c ? e1 : e2) \<inter> 
   740                                assigns_if False (c ? e1 : e2));
   741               brk A = (\<lambda> l. UNIV)\<rbrakk>
   742               \<Longrightarrow> 
   743               Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" 
   744 
   745 | Cond: "\<lbrakk>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean);
   746           Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
   747           Env\<turnstile> (B \<union> assigns_if True  c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1;
   748           Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
   749           nrm A = nrm E1 \<inter> nrm E2; brk A = (\<lambda> l. UNIV)\<rbrakk>
   750           \<Longrightarrow> 
   751           Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" 
   752 
   753 | Call: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A\<rbrakk> 
   754          \<Longrightarrow>  
   755          Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A"
   756 
   757 \<comment> \<open>The interplay of @{term Call}, @{term Methd} and @{term Body}:
   758       Why rules for @{term Methd} and @{term Body} at all? Note that a
   759       Java source program will not include bare  @{term Methd} or @{term Body}
   760       terms. These terms are just introduced during evaluation. So definite
   761       assignment of @{term Call} does not consider @{term Methd} or 
   762       @{term Body} at all. So for definite assignment alone we could omit the
   763       rules for @{term Methd} and @{term Body}. 
   764       But since evaluation of the method invocation is
   765       split up into three rules we must ensure that we have enough information
   766       about the call even in the @{term Body} term to make sure that we can
   767       proof type safety. Also we must be able transport this information 
   768       from @{term Call} to @{term Methd} and then further to @{term Body} 
   769       during evaluation to establish the definite assignment of @{term Methd}
   770       during evaluation of @{term Call}, and of @{term Body} during evaluation
   771       of @{term Methd}. This is necessary since definite assignment will be
   772       a precondition for each induction hypothesis coming out of the evaluation
   773       rules, and therefor we have to establish the definite assignment of the
   774       sub-evaluation during the type-safety proof. Note that well-typedness is
   775       also a precondition for type-safety and so we can omit some assertion 
   776       that are already ensured by well-typedness. 
   777 \<close>
   778 | Methd: "\<lbrakk>methd (prg Env) D sig = Some m;
   779            Env\<turnstile> B \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A
   780           \<rbrakk>
   781           \<Longrightarrow>
   782           Env\<turnstile> B \<guillemotright>\<langle>Methd D sig\<rangle>\<guillemotright> A" 
   783 
   784 | Body: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; jumpNestingOkS {Ret} c; Result \<in> nrm C;
   785           nrm A = B; brk A = (\<lambda> l. UNIV)\<rbrakk>
   786          \<Longrightarrow>
   787          Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A"
   788 \<comment> \<open>Note that @{term A} is not correlated to  @{term C}. If the body
   789       statement returns abruptly with return, evaluation of  @{term Body}
   790       will absorb this return and complete normally. So we cannot trivially
   791       get the assigned variables of the body statement since it has not 
   792       completed normally or with a break.
   793       If the body completes normally we guarantee that the result variable
   794       is set with this rule. But if the body completes abruptly with a return
   795       we can't guarantee that the result variable is set here, since 
   796       definite assignment only talks about normal completion and breaks. So
   797       for a return the @{term Jump} rule ensures that the result variable is
   798       set and then this information must be carried over to the @{term Body}
   799       rule by the conformance predicate of the state.
   800 \<close>
   801 | LVar: "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>" 
   802 
   803 | FVar: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A 
   804          \<Longrightarrow> 
   805          Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A" 
   806 
   807 | AVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A\<rbrakk>
   808           \<Longrightarrow> 
   809           Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A" 
   810 
   811 | Nil: "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>" 
   812 
   813 | Cons: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e::expr\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A\<rbrakk>
   814          \<Longrightarrow> 
   815          Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A" 
   816 
   817 
   818 declare inj_term_sym_simps [simp]
   819 declare assigns_if.simps [simp del]
   820 declare split_paired_All [simp del] split_paired_Ex [simp del]
   821 setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
   822 
   823 inductive_cases da_elim_cases [cases set]:
   824   "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" 
   825   "Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A" 
   826   "Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"
   827   "Env\<turnstile> B \<guillemotright>In1r (Expr e)\<guillemotright> A"
   828   "Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> c\<rangle>\<guillemotright> A"
   829   "Env\<turnstile> B \<guillemotright>In1r (l\<bullet> c)\<guillemotright> A"
   830   "Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A"
   831   "Env\<turnstile> B \<guillemotright>In1r (c1;; c2)\<guillemotright> A"
   832   "Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A" 
   833   "Env\<turnstile> B \<guillemotright>In1r (If(e) c1 Else c2)\<guillemotright> A" 
   834   "Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"
   835   "Env\<turnstile> B \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A"  
   836   "Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A"
   837   "Env\<turnstile> B \<guillemotright>In1r (Jmp jump)\<guillemotright> A"
   838   "Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"
   839   "Env\<turnstile> B \<guillemotright>In1r (Throw e)\<guillemotright> A"
   840   "Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A"
   841   "Env\<turnstile> B \<guillemotright>In1r (Try c1 Catch(C vn) c2)\<guillemotright> A"
   842   "Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A" 
   843   "Env\<turnstile> B \<guillemotright>In1r (c1 Finally c2)\<guillemotright> A" 
   844   "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> A"
   845   "Env\<turnstile> B \<guillemotright>In1r (Init C)\<guillemotright> A"
   846   "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> A"
   847   "Env\<turnstile> B \<guillemotright>In1l (NewC C)\<guillemotright> A"
   848   "Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A"
   849   "Env\<turnstile> B \<guillemotright>In1l (New T[e])\<guillemotright> A"
   850   "Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A"
   851   "Env\<turnstile> B \<guillemotright>In1l (Cast T e)\<guillemotright> A"
   852   "Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A"
   853   "Env\<turnstile> B \<guillemotright>In1l (e InstOf T)\<guillemotright> A"
   854   "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> A"
   855   "Env\<turnstile> B \<guillemotright>In1l (Lit v)\<guillemotright> A"
   856   "Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A"
   857   "Env\<turnstile> B \<guillemotright>In1l (UnOp unop e)\<guillemotright> A"
   858   "Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A"
   859   "Env\<turnstile> B \<guillemotright>In1l (BinOp binop e1 e2)\<guillemotright> A"
   860   "Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> A"
   861   "Env\<turnstile> B \<guillemotright>In1l (Super)\<guillemotright> A"
   862   "Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A"
   863   "Env\<turnstile> B \<guillemotright>In1l (Acc v)\<guillemotright> A"
   864   "Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A"
   865   "Env\<turnstile> B \<guillemotright>In1l (v := e)\<guillemotright> A"
   866   "Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" 
   867   "Env\<turnstile> B \<guillemotright>In1l (c ? e1 : e2)\<guillemotright> A" 
   868   "Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A"
   869   "Env\<turnstile> B \<guillemotright>In1l ({accC,statT,mode}e\<cdot>mn({pTs}args))\<guillemotright> A"
   870   "Env\<turnstile> B \<guillemotright>\<langle>Methd C sig\<rangle>\<guillemotright> A" 
   871   "Env\<turnstile> B \<guillemotright>In1l (Methd C sig)\<guillemotright> A"
   872   "Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A" 
   873   "Env\<turnstile> B \<guillemotright>In1l (Body D c)\<guillemotright> A" 
   874   "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> A"
   875   "Env\<turnstile> B \<guillemotright>In2 (LVar vn)\<guillemotright> A"
   876   "Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A" 
   877   "Env\<turnstile> B \<guillemotright>In2 ({accC,statDeclC,stat}e..fn)\<guillemotright> A" 
   878   "Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A" 
   879   "Env\<turnstile> B \<guillemotright>In2 (e1.[e2])\<guillemotright> A" 
   880   "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> A"
   881   "Env\<turnstile> B \<guillemotright>In3 ([]::expr list)\<guillemotright> A"
   882   "Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A"
   883   "Env\<turnstile> B \<guillemotright>In3 (e#es)\<guillemotright> A"
   884 declare inj_term_sym_simps [simp del]
   885 declare assigns_if.simps [simp]
   886 declare split_paired_All [simp] split_paired_Ex [simp]
   887 setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
   888 
   889 (* To be able to eliminate both the versions with the overloaded brackets: 
   890    (B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A), 
   891    every rule appears in both versions
   892  *)
   893 
   894 lemma da_Skip: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
   895   by (auto intro: da.Skip)
   896 
   897 lemma da_NewC: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> A"
   898   by (auto intro: da.NewC)
   899  
   900 lemma da_Lit:  "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> A"
   901   by (auto intro: da.Lit)
   902 
   903 lemma da_Super: "\<lbrakk>This \<in> B;A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>\<rbrakk> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> A"
   904   by (auto intro: da.Super)
   905 
   906 lemma da_Init: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> A"
   907   by (auto intro: da.Init)
   908 
   909 
   910 (*
   911 For boolean expressions:
   912 
   913 The following holds: "assignsE e \<subseteq> assigns_if True e \<inter> assigns_if False e"
   914 but not vice versa:
   915  "assigns_if True e \<inter> assigns_if False e \<subseteq> assignsE e"
   916 
   917 Example: 
   918  e = ((x < 5) || (y = true)) && (y = true)
   919 
   920    =  (   a    ||    b     ) &&    c
   921 
   922 assigns_if True  a = {}
   923 assigns_if False a = {}
   924 
   925 assigns_if True  b = {y}
   926 assigns_if False b = {y}
   927 
   928 assigns_if True  c = {y}
   929 assigns_if False c = {y}
   930 
   931 assigns_if True (a || b) = assigns_if True a \<inter> 
   932                                 (assigns_if False a \<union> assigns_if True b)
   933                            = {} \<inter> ({} \<union> {y}) = {}
   934 assigns_if False (a || b) = assigns_if False a \<union> assigns_if False b
   935                             = {} \<union> {y} = {y}
   936 
   937 
   938 
   939 assigns_ifE True e =  assigns_if True (a || b) \<union> assigns_if True c
   940                     = {} \<union> {y} = {y}
   941 assigns_ifE False e = assigns_if False (a || b) \<inter> 
   942                        (assigns_if True (a || b) \<union> assigns_if False c)
   943                      = {y} \<inter> ({} \<union> {y}) = {y}
   944 
   945 assignsE e = {}
   946 *)  
   947 
   948 lemma assignsE_subseteq_assigns_ifs:
   949  assumes boolEx: "E\<turnstile>e\<Colon>-PrimT Boolean" (is "?Boolean e")
   950    shows "assignsE e \<subseteq> assigns_if True e \<inter> assigns_if False e" (is "?Incl e")
   951 proof -
   952   obtain vv where ex_lit: "E\<turnstile>Lit vv\<Colon>- PrimT Boolean"
   953     using typeof.simps(2) wt.Lit by blast
   954   have "?Boolean e \<Longrightarrow> ?Incl e"
   955   proof (induct e)
   956     case (Cast T e)
   957     have "E\<turnstile>e\<Colon>- (PrimT Boolean)"
   958     proof -
   959       from \<open>E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)\<close>
   960       obtain Te where "E\<turnstile>e\<Colon>-Te"
   961                            "prg E\<turnstile>Te\<preceq>? PrimT Boolean"
   962         by cases simp
   963       thus ?thesis
   964         by - (drule cast_Boolean2,simp)
   965     qed
   966     with Cast.hyps
   967     show ?case
   968       by simp
   969   next  
   970     case (Lit val) 
   971     thus ?case
   972       by - (erule wt_elim_cases, cases "val", auto simp add: empty_dt_def)
   973   next
   974     case (UnOp unop e) 
   975     thus ?case
   976       by - (erule wt_elim_cases,cases unop,
   977             (fastforce simp add: assignsE_const_simp)+)
   978   next
   979     case (BinOp binop e1 e2)
   980     from BinOp.prems obtain e1T e2T
   981       where "E\<turnstile>e1\<Colon>-e1T" and "E\<turnstile>e2\<Colon>-e2T" and "wt_binop (prg E) binop e1T e2T"
   982             and "(binop_type binop) = Boolean"
   983       by (elim wt_elim_cases) simp
   984     with BinOp.hyps
   985     show ?case
   986       by - (cases binop, auto simp add: assignsE_const_simp)
   987   next
   988     case (Cond c e1 e2)
   989     note hyp_c = \<open>?Boolean c \<Longrightarrow> ?Incl c\<close>
   990     note hyp_e1 = \<open>?Boolean e1 \<Longrightarrow> ?Incl e1\<close>
   991     note hyp_e2 = \<open>?Boolean e2 \<Longrightarrow> ?Incl e2\<close>
   992     note wt = \<open>E\<turnstile>(c ? e1 : e2)\<Colon>-PrimT Boolean\<close>
   993     then obtain
   994       boolean_c:  "E\<turnstile>c\<Colon>-PrimT Boolean" and
   995       boolean_e1: "E\<turnstile>e1\<Colon>-PrimT Boolean" and
   996       boolean_e2: "E\<turnstile>e2\<Colon>-PrimT Boolean"
   997       by (elim wt_elim_cases) (auto dest: widen_Boolean2)
   998     show ?case
   999     proof (cases "constVal c")
  1000       case None
  1001       with boolean_e1 boolean_e2
  1002       show ?thesis
  1003         using hyp_e1 hyp_e2 
  1004         by (auto)
  1005     next
  1006       case (Some bv)
  1007       show ?thesis
  1008       proof (cases "the_Bool bv")
  1009         case True
  1010         with Some show ?thesis using hyp_e1 boolean_e1 by auto
  1011       next
  1012         case False
  1013         with Some show ?thesis using hyp_e2 boolean_e2 by auto
  1014       qed
  1015     qed
  1016   next
  1017     show "\<And>x. E\<turnstile>Lit vv\<Colon>-PrimT Boolean"
  1018       by (rule ex_lit)
  1019   qed (simp_all add: ex_lit)
  1020   with boolEx 
  1021   show ?thesis
  1022     by blast
  1023 qed
  1024   
  1025 
  1026 (* Trick:
  1027    If you have a rule with the abstract term injections:
  1028    e.g:  da.Skip "B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
  1029    and the current goal state as an concrete injection:
  1030    e.g: "B \<guillemotright>In1r Skip\<guillemotright> A"
  1031    you can convert the rule by: da.Skip [simplified]
  1032    if inj_term_simps is in the simpset
  1033 
  1034 *)
  1035 
  1036 lemma rmlab_same_label [simp]: "(rmlab l A) l = UNIV"
  1037   by (simp add: rmlab_def)
  1038 
  1039 lemma rmlab_same_label1 [simp]: "l=l' \<Longrightarrow> (rmlab l A) l' = UNIV"
  1040   by (simp add: rmlab_def)
  1041 
  1042 lemma rmlab_other_label [simp]: "l\<noteq>l'\<Longrightarrow> (rmlab l A) l' = A l'"
  1043   by (auto simp add: rmlab_def)
  1044 
  1045 lemma range_inter_ts_subseteq [intro]: "\<forall> k. A k \<subseteq> B k \<Longrightarrow> \<Rightarrow>\<Inter>A \<subseteq> \<Rightarrow>\<Inter>B"
  1046   by (auto simp add: range_inter_ts_def)
  1047 
  1048 lemma range_inter_ts_subseteq': "\<forall> k. A k \<subseteq> B k \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>A \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>B"
  1049   by (auto simp add: range_inter_ts_def)
  1050 
  1051 lemma da_monotone: 
  1052   assumes da: "Env\<turnstile> B  \<guillemotright>t\<guillemotright> A" and
  1053     "B \<subseteq> B'" and
  1054     da': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" 
  1055   shows "(nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"
  1056 proof -
  1057   from da
  1058   have "\<And> B' A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; B \<subseteq> B'\<rbrakk> 
  1059                   \<Longrightarrow> (nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"
  1060        (is "PROP ?Hyp Env B t A")  
  1061   proof (induct)
  1062     case Skip 
  1063     then show ?case by cases simp
  1064   next
  1065     case Expr 
  1066     from Expr.prems Expr.hyps 
  1067     show ?case by cases simp
  1068   next
  1069     case (Lab Env B c C A l B' A')
  1070     note A = \<open>nrm A = nrm C \<inter> brk C l\<close> \<open>brk A = rmlab l (brk C)\<close>
  1071     note \<open>PROP ?Hyp Env B \<langle>c\<rangle> C\<close>
  1072     moreover
  1073     note \<open>B \<subseteq> B'\<close>
  1074     moreover
  1075     obtain C'
  1076       where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
  1077         and A': "nrm A' = nrm C' \<inter> brk C' l" "brk A' = rmlab l (brk C')"
  1078       using Lab.prems
  1079       by cases simp
  1080     ultimately
  1081     have "nrm C \<subseteq> nrm C'" and hyp_brk: "(\<forall>l. brk C l \<subseteq> brk C' l)" by auto
  1082     then 
  1083     have "nrm C \<inter> brk C l \<subseteq> nrm C' \<inter> brk C' l" by auto
  1084     moreover
  1085     {
  1086       fix l'
  1087       from hyp_brk
  1088       have "rmlab l (brk C) l'  \<subseteq> rmlab l (brk C') l'"
  1089         by  (cases "l=l'") simp_all
  1090     }
  1091     moreover note A A'
  1092     ultimately show ?case
  1093       by simp
  1094   next
  1095     case (Comp Env B c1 C1 c2 C2 A B' A')
  1096     note A = \<open>nrm A = nrm C2\<close> \<open>brk A = brk C1 \<Rightarrow>\<inter>  brk C2\<close>
  1097     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'\<close>
  1098     obtain  C1' C2'
  1099       where da_c1: "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
  1100             da_c2: "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"  and
  1101             A': "nrm A' = nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'"
  1102       by cases auto
  1103     note \<open>PROP ?Hyp Env B \<langle>c1\<rangle> C1\<close>
  1104     moreover note \<open>B \<subseteq> B'\<close>
  1105     moreover note da_c1
  1106     ultimately have C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
  1107       by auto
  1108     note \<open>PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle> C2\<close>
  1109     with da_c2 C1' 
  1110     have C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
  1111       by auto
  1112     with A A' C1'
  1113     show ?case
  1114       by auto
  1115   next
  1116     case (If Env B e E c1 C1 c2 C2 A B' A')
  1117     note A = \<open>nrm A = nrm C1 \<inter> nrm C2\<close> \<open>brk A = brk C1 \<Rightarrow>\<inter>  brk C2\<close>
  1118     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'\<close>
  1119     obtain C1' C2'
  1120       where da_c1: "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
  1121             da_c2: "Env\<turnstile> B' \<union> assigns_if False e \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
  1122                A': "nrm A' = nrm C1' \<inter> nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'"
  1123       by cases auto
  1124     note \<open>PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1\<close>
  1125     moreover note B' = \<open>B \<subseteq> B'\<close>
  1126     moreover note da_c1 
  1127     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
  1128       by blast
  1129     note \<open>PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle> C2\<close>
  1130     with da_c2 B'
  1131     obtain C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
  1132       by blast
  1133     with A A' C1'
  1134     show ?case
  1135       by auto
  1136   next
  1137     case (Loop Env B e E c C A l B' A')
  1138     note A = \<open>nrm A = nrm C \<inter> (B \<union> assigns_if False e)\<close> \<open>brk A = brk C\<close>
  1139     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'\<close>
  1140     obtain C'
  1141       where 
  1142        da_c': "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
  1143           A': "nrm A' = nrm C' \<inter> (B' \<union> assigns_if False e)"
  1144               "brk A' = brk C'" 
  1145       by cases auto
  1146     note \<open>PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C\<close>
  1147     moreover note B' = \<open>B \<subseteq> B'\<close>
  1148     moreover note da_c'
  1149     ultimately obtain C': "nrm C \<subseteq> nrm C'" "(\<forall>l. brk C l \<subseteq> brk C' l)"
  1150       by blast
  1151     with A A' B'
  1152     have "nrm A \<subseteq> nrm A'"
  1153       by blast
  1154     moreover
  1155     { fix l'
  1156       have  "brk A l' \<subseteq> brk A' l'"
  1157       proof (cases "constVal e")
  1158         case None
  1159         with A A' C' 
  1160         show ?thesis
  1161            by (cases "l=l'") auto
  1162       next
  1163         case (Some bv)
  1164         with A A' C'
  1165         show ?thesis
  1166           by (cases "the_Bool bv", cases "l=l'") auto
  1167       qed
  1168     }
  1169     ultimately show ?case
  1170       by auto
  1171   next
  1172     case (Jmp jump B A Env B' A')
  1173     thus ?case by (elim da_elim_cases) (auto split: jump.splits)
  1174   next
  1175     case Throw thus ?case by (elim da_elim_cases) auto
  1176   next
  1177     case (Try Env B c1 C1 vn C c2 C2 A B' A')
  1178     note A = \<open>nrm A = nrm C1 \<inter> nrm C2\<close> \<open>brk A = brk C1 \<Rightarrow>\<inter>  brk C2\<close>
  1179     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'\<close>
  1180     obtain C1' C2'
  1181       where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
  1182             da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} 
  1183                       \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
  1184             A': "nrm A' = nrm C1' \<inter> nrm C2'"
  1185                 "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'" 
  1186       by cases auto
  1187     note \<open>PROP ?Hyp Env B \<langle>c1\<rangle> C1\<close>
  1188     moreover note B' = \<open>B \<subseteq> B'\<close>
  1189     moreover note da_c1'
  1190     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
  1191       by blast
  1192     note \<open>PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
  1193                     (B \<union> {VName vn}) \<langle>c2\<rangle> C2\<close>
  1194     with B' da_c2'
  1195     obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
  1196       by blast
  1197     with C1' A A'
  1198     show ?case
  1199       by auto
  1200   next
  1201     case (Fin Env B c1 C1 c2 C2 A B' A')
  1202     note A = \<open>nrm A = nrm C1 \<union> nrm C2\<close>
  1203       \<open>brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)\<close>
  1204     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'\<close>
  1205     obtain C1' C2'
  1206       where  da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
  1207              da_c2': "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
  1208              A':  "nrm A' = nrm C1' \<union> nrm C2'"
  1209                   "brk A' = (brk C1' \<Rightarrow>\<union>\<^sub>\<forall> nrm C2') \<Rightarrow>\<inter> (brk C2')"
  1210       by cases auto
  1211     note \<open>PROP ?Hyp Env B \<langle>c1\<rangle> C1\<close>
  1212     moreover note B' = \<open>B \<subseteq> B'\<close>
  1213     moreover note da_c1'
  1214     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
  1215       by blast
  1216     note hyp_c2 = \<open>PROP ?Hyp Env B \<langle>c2\<rangle> C2\<close>
  1217     from da_c2' B' 
  1218      obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
  1219        by - (drule hyp_c2,auto)
  1220      with A A' C1'
  1221      show ?case
  1222        by auto
  1223    next
  1224      case Init thus ?case by (elim da_elim_cases) auto
  1225    next
  1226      case NewC thus ?case by (elim da_elim_cases) auto
  1227    next
  1228      case NewA thus ?case by (elim da_elim_cases) auto
  1229    next
  1230      case Cast thus ?case by (elim da_elim_cases) auto
  1231    next
  1232      case Inst thus ?case by (elim da_elim_cases) auto
  1233    next
  1234      case Lit thus ?case by (elim da_elim_cases) auto
  1235    next
  1236      case UnOp thus ?case by (elim da_elim_cases) auto
  1237    next
  1238      case (CondAnd Env B e1 E1 e2 E2 A B' A')
  1239      note A = \<open>nrm A = B \<union>
  1240                        assigns_if True (BinOp CondAnd e1 e2) \<inter>
  1241                        assigns_if False (BinOp CondAnd e1 e2)\<close>
  1242              \<open>brk A = (\<lambda>l. UNIV)\<close>
  1243      from \<open>Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'\<close>
  1244      obtain  A': "nrm A' = B' \<union>
  1245                                  assigns_if True (BinOp CondAnd e1 e2) \<inter>
  1246                                  assigns_if False (BinOp CondAnd e1 e2)"
  1247                       "brk A' = (\<lambda>l. UNIV)" 
  1248        by cases auto
  1249      note B' = \<open>B \<subseteq> B'\<close>
  1250      with A A' show ?case 
  1251        by auto 
  1252    next
  1253      case CondOr thus ?case by (elim da_elim_cases) auto
  1254    next
  1255      case BinOp thus ?case by (elim da_elim_cases) auto
  1256    next
  1257      case Super thus ?case by (elim da_elim_cases) auto
  1258    next
  1259      case AccLVar thus ?case by (elim da_elim_cases) auto
  1260    next
  1261      case Acc thus ?case by (elim da_elim_cases) auto
  1262    next
  1263      case AssLVar thus ?case by (elim da_elim_cases) auto
  1264    next
  1265      case Ass thus ?case by (elim da_elim_cases) auto
  1266    next
  1267      case (CondBool Env c e1 e2 B C E1 E2 A B' A')
  1268      note A = \<open>nrm A = B \<union> 
  1269                         assigns_if True (c ? e1 : e2) \<inter> 
  1270                         assigns_if False (c ? e1 : e2)\<close>
  1271              \<open>brk A = (\<lambda>l. UNIV)\<close>
  1272      note \<open>Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)\<close>
  1273      moreover
  1274      note \<open>Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'\<close>
  1275      ultimately
  1276      obtain A': "nrm A' = B' \<union> 
  1277                                   assigns_if True (c ? e1 : e2) \<inter> 
  1278                                   assigns_if False (c ? e1 : e2)"
  1279                      "brk A' = (\<lambda>l. UNIV)"
  1280        by (elim da_elim_cases) (auto simp add: inj_term_simps) 
  1281        (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
  1282      note B' = \<open>B \<subseteq> B'\<close>
  1283      with A A' show ?case 
  1284        by auto 
  1285    next
  1286      case (Cond Env c e1 e2 B C E1 E2 A B' A')  
  1287      note A = \<open>nrm A = nrm E1 \<inter> nrm E2\<close> \<open>brk A = (\<lambda>l. UNIV)\<close>
  1288      note not_bool = \<open>\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)\<close>
  1289      from \<open>Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'\<close>
  1290      obtain E1' E2'
  1291        where da_e1': "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and
  1292              da_e2': "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and
  1293                  A': "nrm A' = nrm E1' \<inter> nrm E2'"
  1294                      "brk A' = (\<lambda>l. UNIV)"
  1295        using not_bool
  1296        by (elim da_elim_cases) (auto simp add: inj_term_simps)
  1297        (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
  1298      note \<open>PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1\<close>
  1299      moreover note B' = \<open>B \<subseteq> B'\<close>
  1300      moreover note da_e1'
  1301      ultimately obtain E1': "nrm E1 \<subseteq> nrm E1'" "(\<forall>l. brk E1 l \<subseteq> brk E1' l)"
  1302        by blast
  1303      note \<open>PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle> E2\<close>
  1304      with B' da_e2'
  1305      obtain "nrm E2 \<subseteq> nrm E2'" "(\<forall>l. brk E2 l \<subseteq> brk E2' l)"
  1306        by blast
  1307     with E1' A A'
  1308     show ?case
  1309       by auto
  1310   next
  1311     case Call
  1312     from Call.prems and Call.hyps
  1313     show ?case by cases auto
  1314   next
  1315     case Methd thus ?case by (elim da_elim_cases) auto
  1316   next
  1317     case Body thus ?case by (elim da_elim_cases) auto
  1318   next
  1319     case LVar thus ?case by (elim da_elim_cases) auto
  1320   next
  1321     case FVar thus ?case by (elim da_elim_cases) auto
  1322   next
  1323     case AVar thus ?case by (elim da_elim_cases) auto
  1324   next
  1325     case Nil thus ?case by (elim da_elim_cases) auto
  1326   next
  1327     case Cons thus ?case by (elim da_elim_cases) auto
  1328   qed
  1329   from this [OF da' \<open>B \<subseteq> B'\<close>] show ?thesis .
  1330 qed
  1331   
  1332 lemma da_weaken:     
  1333   assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and "B \<subseteq> B'" 
  1334   shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'"
  1335 proof -
  1336   note assigned.select_convs [Pure.intro]
  1337   from da  
  1338   have "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
  1339   proof (induct) 
  1340     case Skip thus ?case by (iprover intro: da.Skip)
  1341   next
  1342     case Expr thus ?case by (iprover intro: da.Expr)
  1343   next
  1344     case (Lab Env B c C A l B')  
  1345     note \<open>PROP ?Hyp Env B \<langle>c\<rangle>\<close>
  1346     moreover
  1347     note B' = \<open>B \<subseteq> B'\<close>
  1348     ultimately obtain C' where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
  1349       by iprover
  1350     then obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A'"
  1351       by (iprover intro: da.Lab)
  1352     thus ?case ..
  1353   next
  1354     case (Comp Env B c1 C1 c2 C2 A B')
  1355     note da_c1 = \<open>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1\<close>
  1356     note \<open>PROP ?Hyp Env B \<langle>c1\<rangle>\<close>
  1357     moreover
  1358     note B' = \<open>B \<subseteq> B'\<close>
  1359     ultimately obtain C1' where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
  1360       by iprover
  1361     with da_c1 B'
  1362     have
  1363       "nrm C1 \<subseteq> nrm C1'"
  1364       by (rule da_monotone [elim_format]) simp
  1365     moreover
  1366     note \<open>PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>\<close>
  1367     ultimately obtain C2' where "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
  1368       by iprover
  1369     with da_c1' obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'"
  1370       by (iprover intro: da.Comp)
  1371     thus ?case ..
  1372   next
  1373     case (If Env B e E c1 C1 c2 C2 A B')
  1374     note B' = \<open>B \<subseteq> B'\<close>
  1375     obtain  E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
  1376     proof -
  1377       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule If.hyps)
  1378       with B'  
  1379       show ?thesis using that by iprover
  1380     qed
  1381     moreover
  1382     obtain C1' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
  1383     proof -
  1384       from B'
  1385       have "(B \<union> assigns_if True e) \<subseteq> (B' \<union> assigns_if True e)"
  1386         by blast
  1387       moreover
  1388       have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle>" by (rule If.hyps)
  1389       ultimately 
  1390       show ?thesis using that by iprover
  1391     qed
  1392     moreover
  1393     obtain C2' where "Env\<turnstile> (B' \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
  1394     proof - 
  1395       from B' have "(B \<union> assigns_if False e) \<subseteq> (B' \<union> assigns_if False e)"
  1396         by blast
  1397       moreover
  1398       have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle>" by (rule If.hyps)
  1399       ultimately
  1400       show ?thesis using that by iprover
  1401     qed
  1402     ultimately
  1403     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'"
  1404       by (iprover intro: da.If)
  1405     thus ?case ..
  1406   next  
  1407     case (Loop Env B e E c C A l B')
  1408     note B' = \<open>B \<subseteq> B'\<close>
  1409     obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
  1410     proof -
  1411       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Loop.hyps)
  1412       with B'  
  1413       show ?thesis using that by iprover
  1414     qed
  1415     moreover
  1416     obtain C' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
  1417     proof -
  1418       from B'
  1419       have "(B \<union> assigns_if True e) \<subseteq> (B' \<union> assigns_if True e)"
  1420         by blast
  1421       moreover
  1422       have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle>" by (rule Loop.hyps)
  1423       ultimately 
  1424       show ?thesis using that by iprover
  1425     qed
  1426     ultimately
  1427     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'"
  1428       by (iprover intro: da.Loop )
  1429     thus ?case ..
  1430   next
  1431     case (Jmp jump B A Env B') 
  1432     note B' = \<open>B \<subseteq> B'\<close>
  1433     with Jmp.hyps have "jump = Ret \<longrightarrow> Result \<in> B' "
  1434       by auto
  1435     moreover
  1436     obtain A'::assigned 
  1437               where  "nrm A' = UNIV"
  1438                      "brk A' = (case jump of 
  1439                                   Break l \<Rightarrow> \<lambda>k. if k = l then B' else UNIV 
  1440                                 | Cont l \<Rightarrow> \<lambda>k. UNIV
  1441                                 | Ret \<Rightarrow> \<lambda>k. UNIV)"
  1442                      
  1443       by  iprover
  1444     ultimately have "Env\<turnstile> B' \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A'"
  1445       by (rule da.Jmp)
  1446     thus ?case ..
  1447   next
  1448     case Throw thus ?case by (iprover intro: da.Throw )
  1449   next
  1450     case (Try Env B c1 C1 vn C c2 C2 A B')
  1451     note B' = \<open>B \<subseteq> B'\<close>
  1452     obtain C1' where "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
  1453     proof -
  1454       have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Try.hyps)
  1455       with B'  
  1456       show ?thesis using that by iprover
  1457     qed
  1458     moreover
  1459     obtain C2' where 
  1460       "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
  1461     proof -
  1462       from B' have "B \<union> {VName vn} \<subseteq> B' \<union> {VName vn}" by blast
  1463       moreover
  1464       have "PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) 
  1465                       (B \<union> {VName vn}) \<langle>c2\<rangle>" 
  1466         by (rule Try.hyps)
  1467       ultimately
  1468       show ?thesis using that by iprover
  1469     qed
  1470     ultimately
  1471     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'"
  1472       by (iprover intro: da.Try )
  1473     thus ?case ..
  1474   next
  1475     case (Fin Env B c1 C1 c2 C2 A B')
  1476     note B' = \<open>B \<subseteq> B'\<close>
  1477     obtain C1' where C1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
  1478     proof -
  1479       have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Fin.hyps)
  1480       with B'  
  1481       show ?thesis using that by iprover
  1482     qed
  1483     moreover
  1484     obtain C2' where "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
  1485     proof -
  1486       have "PROP ?Hyp Env B \<langle>c2\<rangle>" by (rule Fin.hyps)
  1487       with B'
  1488       show ?thesis using that by iprover
  1489     qed
  1490     ultimately
  1491     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'"
  1492       by (iprover intro: da.Fin )
  1493     thus ?case ..
  1494   next
  1495     case Init thus ?case by (iprover intro: da.Init)
  1496   next
  1497     case NewC thus ?case by (iprover intro: da.NewC)
  1498   next
  1499     case NewA thus ?case by (iprover intro: da.NewA)
  1500   next
  1501     case Cast thus ?case by (iprover intro: da.Cast)
  1502   next
  1503     case Inst thus ?case by (iprover intro: da.Inst)
  1504   next
  1505     case Lit thus ?case by (iprover intro: da.Lit)
  1506   next
  1507     case UnOp thus ?case by (iprover intro: da.UnOp)
  1508   next
  1509     case (CondAnd Env B e1 E1 e2 E2 A B')
  1510     note B' = \<open>B \<subseteq> B'\<close>
  1511     obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
  1512     proof -
  1513       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondAnd.hyps)
  1514       with B'
  1515       show ?thesis using that by iprover
  1516     qed
  1517     moreover
  1518     obtain E2' where "Env\<turnstile> B' \<union>  assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
  1519     proof -
  1520       from B' have "B \<union> assigns_if True e1 \<subseteq> B' \<union>  assigns_if True e1"
  1521         by blast
  1522       moreover
  1523       have "PROP ?Hyp Env (B \<union> assigns_if True e1) \<langle>e2\<rangle>" by (rule CondAnd.hyps)
  1524       ultimately show ?thesis using that by iprover
  1525     qed
  1526     ultimately
  1527     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'"
  1528       by (iprover intro: da.CondAnd)
  1529     thus ?case ..
  1530   next
  1531     case (CondOr Env B e1 E1 e2 E2 A B')
  1532     note B' = \<open>B \<subseteq> B'\<close>
  1533     obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
  1534     proof -
  1535       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondOr.hyps)
  1536       with B'  
  1537       show ?thesis using that by iprover
  1538     qed
  1539     moreover
  1540     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
  1541     proof -
  1542       from B' have "B \<union> assigns_if False e1 \<subseteq> B' \<union>  assigns_if False e1"
  1543         by blast
  1544       moreover
  1545       have "PROP ?Hyp Env (B \<union> assigns_if False e1) \<langle>e2\<rangle>" by (rule CondOr.hyps)
  1546       ultimately show ?thesis using that by iprover
  1547     qed
  1548     ultimately
  1549     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A'"
  1550       by (iprover intro: da.CondOr)
  1551     thus ?case ..
  1552   next
  1553     case (BinOp Env B e1 E1 e2 A binop B')
  1554     note B' = \<open>B \<subseteq> B'\<close>
  1555     obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
  1556     proof -
  1557       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule BinOp.hyps)
  1558       with B'
  1559       show ?thesis using that by iprover
  1560     qed
  1561     moreover
  1562     obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"
  1563     proof -
  1564       have "Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" by (rule BinOp.hyps)
  1565       from this B' E1'
  1566       have "nrm E1 \<subseteq> nrm E1'"
  1567         by (rule da_monotone [THEN conjE])
  1568       moreover 
  1569       have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule BinOp.hyps)
  1570       ultimately show ?thesis using that by iprover
  1571     qed
  1572     ultimately
  1573     have "Env\<turnstile> B' \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A'"
  1574       using BinOp.hyps by (iprover intro: da.BinOp)
  1575     thus ?case ..
  1576   next
  1577     case (Super B Env B')
  1578     note B' = \<open>B \<subseteq> B'\<close>
  1579     with Super.hyps have "This \<in> B'"
  1580       by auto
  1581     thus ?case by (iprover intro: da.Super)
  1582   next
  1583     case (AccLVar vn B A Env B')
  1584     note \<open>vn \<in> B\<close>
  1585     moreover
  1586     note \<open>B \<subseteq> B'\<close>
  1587     ultimately have "vn \<in> B'" by auto
  1588     thus ?case by (iprover intro: da.AccLVar)
  1589   next
  1590     case Acc thus ?case by (iprover intro: da.Acc)
  1591   next 
  1592     case (AssLVar Env B e E A vn B')
  1593     note B' = \<open>B \<subseteq> B'\<close>
  1594     then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
  1595       by (rule AssLVar.hyps [elim_format]) iprover
  1596     then obtain A' where  
  1597       "Env\<turnstile> B' \<guillemotright>\<langle>LVar vn:=e\<rangle>\<guillemotright> A'"
  1598       by (iprover intro: da.AssLVar)
  1599     thus ?case ..
  1600   next
  1601     case (Ass v Env B V e A B') 
  1602     note B' = \<open>B \<subseteq> B'\<close>
  1603     note \<open>\<forall>vn. v \<noteq> LVar vn\<close>
  1604     moreover
  1605     obtain V' where V': "Env\<turnstile> B' \<guillemotright>\<langle>v\<rangle>\<guillemotright> V'"
  1606     proof -
  1607       have "PROP ?Hyp Env B \<langle>v\<rangle>" by (rule Ass.hyps)
  1608       with B'  
  1609       show ?thesis using that by iprover
  1610     qed
  1611     moreover
  1612     obtain A' where "Env\<turnstile> nrm V' \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"
  1613     proof -
  1614       have "Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V" by (rule Ass.hyps)
  1615       from this B' V'
  1616       have "nrm V \<subseteq> nrm V'"
  1617         by (rule da_monotone [THEN conjE])
  1618       moreover 
  1619       have "PROP ?Hyp Env (nrm V) \<langle>e\<rangle>" by (rule Ass.hyps)
  1620       ultimately show ?thesis using that by iprover
  1621     qed  
  1622     ultimately
  1623     have "Env\<turnstile> B' \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A'"
  1624       by (iprover intro: da.Ass)
  1625     thus ?case ..
  1626   next
  1627     case (CondBool Env c e1 e2 B C E1 E2 A B')
  1628     note B' = \<open>B \<subseteq> B'\<close>
  1629     note \<open>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)\<close>
  1630     moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
  1631     proof -
  1632       have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule CondBool.hyps)
  1633       with B'  
  1634       show ?thesis using that by iprover
  1635     qed
  1636     moreover 
  1637     obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
  1638     proof -
  1639       from B'
  1640       have "(B \<union> assigns_if True c) \<subseteq> (B' \<union> assigns_if True c)"
  1641         by blast
  1642       moreover
  1643       have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule CondBool.hyps)
  1644       ultimately 
  1645       show ?thesis using that by iprover
  1646     qed
  1647     moreover
  1648     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
  1649     proof -
  1650       from B'
  1651       have "(B \<union> assigns_if False c) \<subseteq> (B' \<union> assigns_if False c)"
  1652         by blast
  1653       moreover
  1654       have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by(rule CondBool.hyps)
  1655       ultimately 
  1656       show ?thesis using that by iprover
  1657     qed
  1658     ultimately 
  1659     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"
  1660       by (iprover intro: da.CondBool)
  1661     thus ?case ..
  1662   next
  1663     case (Cond Env c e1 e2 B C E1 E2 A B')
  1664     note B' = \<open>B \<subseteq> B'\<close>
  1665     note \<open>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)\<close>
  1666     moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
  1667     proof -
  1668       have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule Cond.hyps)
  1669       with B'  
  1670       show ?thesis using that by iprover
  1671     qed
  1672     moreover 
  1673     obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
  1674     proof -
  1675       from B'
  1676       have "(B \<union> assigns_if True c) \<subseteq> (B' \<union> assigns_if True c)"
  1677         by blast
  1678       moreover
  1679       have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule Cond.hyps)
  1680       ultimately 
  1681       show ?thesis using that by iprover
  1682     qed
  1683     moreover
  1684     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
  1685     proof -
  1686       from B'
  1687       have "(B \<union> assigns_if False c) \<subseteq> (B' \<union> assigns_if False c)"
  1688         by blast
  1689       moreover
  1690       have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by (rule Cond.hyps)
  1691       ultimately 
  1692       show ?thesis using that by iprover
  1693     qed
  1694     ultimately 
  1695     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"
  1696       by (iprover intro: da.Cond)
  1697     thus ?case ..
  1698   next
  1699     case (Call Env B e E args A accC statT mode mn pTs B')
  1700     note B' = \<open>B \<subseteq> B'\<close>
  1701     obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
  1702     proof -
  1703       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Call.hyps)
  1704       with B'  
  1705       show ?thesis using that by iprover
  1706     qed
  1707     moreover
  1708     obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'"
  1709     proof -
  1710       have "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" by (rule Call.hyps)
  1711       from this B' E'
  1712       have "nrm E \<subseteq> nrm E'"
  1713         by (rule da_monotone [THEN conjE])
  1714       moreover 
  1715       have "PROP ?Hyp Env (nrm E) \<langle>args\<rangle>" by (rule Call.hyps)
  1716       ultimately show ?thesis using that by iprover
  1717     qed  
  1718     ultimately
  1719     have "Env\<turnstile> B' \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs}args)\<rangle>\<guillemotright> A'"
  1720       by (iprover intro: da.Call)
  1721     thus ?case ..
  1722   next
  1723     case Methd thus ?case by (iprover intro: da.Methd)
  1724   next
  1725     case (Body Env B c C A D B')  
  1726     note B' = \<open>B \<subseteq> B'\<close>
  1727     obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and nrm_C': "nrm C \<subseteq> nrm C'"
  1728     proof -
  1729       have "Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" by (rule Body.hyps)
  1730       moreover note B'
  1731       moreover
  1732       from B' obtain C' where da_c: "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
  1733         by (rule Body.hyps [elim_format]) blast
  1734       ultimately
  1735       have "nrm C \<subseteq> nrm C'"
  1736         by (rule da_monotone [THEN conjE])
  1737       with da_c that show ?thesis by iprover
  1738     qed
  1739     moreover 
  1740     note \<open>Result \<in> nrm C\<close>
  1741     with nrm_C' have "Result \<in> nrm C'"
  1742       by blast
  1743     moreover note \<open>jumpNestingOkS {Ret} c\<close>
  1744     ultimately obtain A' where
  1745       "Env\<turnstile> B' \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A'"
  1746       by (iprover intro: da.Body)
  1747     thus ?case ..
  1748   next
  1749     case LVar thus ?case by (iprover intro: da.LVar)
  1750   next
  1751     case FVar thus ?case by (iprover intro: da.FVar)
  1752   next
  1753     case (AVar Env B e1 E1 e2 A B')
  1754     note B' = \<open>B \<subseteq> B'\<close>
  1755     obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
  1756     proof -
  1757       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule AVar.hyps)
  1758       with B'
  1759       show ?thesis using that by iprover
  1760     qed
  1761     moreover
  1762     obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"
  1763     proof -
  1764       have "Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" by (rule AVar.hyps)
  1765       from this B' E1'
  1766       have "nrm E1 \<subseteq> nrm E1'"
  1767         by (rule da_monotone [THEN conjE])
  1768       moreover 
  1769       have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule AVar.hyps)
  1770       ultimately show ?thesis using that by iprover
  1771     qed  
  1772     ultimately
  1773     have "Env\<turnstile> B' \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A'"
  1774       by (iprover intro: da.AVar)
  1775     thus ?case ..
  1776   next
  1777     case Nil thus ?case by (iprover intro: da.Nil)
  1778   next
  1779     case (Cons Env B e E es A B')
  1780     note B' = \<open>B \<subseteq> B'\<close>
  1781     obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
  1782     proof -
  1783       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Cons.hyps)
  1784       with B'  
  1785       show ?thesis using that by iprover
  1786     qed
  1787     moreover
  1788     obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'"
  1789     proof -
  1790       have "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" by (rule Cons.hyps)
  1791       from this B' E'
  1792       have "nrm E \<subseteq> nrm E'"
  1793         by (rule da_monotone [THEN conjE])
  1794       moreover 
  1795       have "PROP ?Hyp Env (nrm E) \<langle>es\<rangle>" by (rule Cons.hyps)
  1796       ultimately show ?thesis using that by iprover
  1797     qed  
  1798     ultimately
  1799     have "Env\<turnstile> B' \<guillemotright>\<langle>e # es\<rangle>\<guillemotright> A'"
  1800       by (iprover intro: da.Cons)
  1801     thus ?case ..
  1802   qed
  1803   from this [OF \<open>B \<subseteq> B'\<close>] show ?thesis .
  1804 qed
  1805 
  1806 (* Remarks about the proof style:
  1807 
  1808    "by (rule <Case>.hyps)" vs "."
  1809    --------------------------
  1810   
  1811    with <Case>.hyps you state more precise were the rule comes from
  1812 
  1813    . takes all assumptions into account, but looks more "light"
  1814    and is more resistent for cut and paste proof in different 
  1815    cases.
  1816 
  1817   "intro: da.intros" vs "da.<Case>"
  1818   ---------------------------------
  1819   The first ist more convinient for cut and paste between cases,
  1820   the second is more informativ for the reader
  1821 *)
  1822 
  1823 corollary da_weakenE [consumes 2]:
  1824   assumes          da: "Env\<turnstile> B  \<guillemotright>t\<guillemotright> A"   and
  1825                    B': "B \<subseteq> B'"          and
  1826               ex_mono: "\<And> A'.  \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; nrm A \<subseteq> nrm A'; 
  1827                                \<And> l. brk A l \<subseteq> brk A' l\<rbrakk> \<Longrightarrow> P" 
  1828   shows "P"
  1829 proof -
  1830   from da B'
  1831   obtain A' where A': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'"
  1832     by (rule da_weaken [elim_format]) iprover
  1833   with da B'
  1834   have "nrm A \<subseteq> nrm A' \<and> (\<forall> l. brk A l \<subseteq> brk A' l)"
  1835     by (rule da_monotone)
  1836   with A' ex_mono
  1837   show ?thesis
  1838     by iprover
  1839 qed
  1840 
  1841 end