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