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