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