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