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