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