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