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