src/HOL/Bali/DefiniteAssignment.thy
 author wenzelm Wed Nov 01 20:46:23 2017 +0100 (22 months ago) changeset 66983 df83b66f1d94 parent 62042 6c6ccf573479 child 67443 3abf6a722518 permissions -rw-r--r--
proper merge (amending fb46c031c841);
     1 subsection \<open>Definite Assignment\<close>

     2

     3 theory DefiniteAssignment imports WellType begin

     4

     5 text \<open>Definite Assignment Analysis (cf. 16)

     6

     7 The definite assignment analysis approximates the sets of local

     8 variables that will be assigned at a certain point of evaluation, and ensures

     9 that we will only read variables which previously were assigned.

    10 It should conform to the following idea:

    11  If the evaluation of a term completes normally (no abruption (exception,

    12 break, continue, return) appeared) , the set of local variables calculated

    13 by the analysis is a subset of the

    14 variables that were actually assigned during evaluation.

    15

    16 To get more precise information about the sets of assigned variables the

    17 analysis includes the following optimisations:

    18 \begin{itemize}

    19   \item Inside of a while loop we also take care of the variables assigned

    20         before break statements, since the break causes the while loop to

    21         continue normally.

    22   \item For conditional statements we take care of constant conditions to

    23         statically determine the path of evaluation.

    24   \item Inside a distinct path of a conditional statements we know to which

    25         boolean value the condition has evaluated to, and so can retrieve more

    26         information about the variables assigned during evaluation of the

    27         boolean condition.

    28 \end{itemize}

    29

    30 Since in our model of Java the return values of methods are stored in a local

    31 variable we also ensure that every path of (normal) evaluation will assign the

    32 result variable, or in the sense of real Java every path ends up in and

    33 return instruction.

    34

    35 Not covered yet:

    36 \begin{itemize}

    37   \item analysis of definite unassigned

    38   \item special treatment of final fields

    39 \end{itemize}

    40 \<close>

    41

    42 subsubsection \<open>Correct nesting of jump statements\<close>

    43

    44 text \<open>For definite assignment it becomes crucial, that jumps (break,

    45 continue, return) are nested correctly i.e. a continue jump is nested in a

    46 matching while statement, a break jump is nested in a proper label statement,

    47 a class initialiser does not terminate abruptly with a return. With this we

    48 can for example ensure that evaluation of an expression will never end up

    49 with a jump, since no breaks, continues or returns are allowed in an

    50 expression.\<close>

    51

    52 primrec jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"

    53 where

    54   "jumpNestingOkS jmps (Skip)   = True"

    55 | "jumpNestingOkS jmps (Expr e) = True"

    56 | "jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"

    57 | "jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and>

    58                                    jumpNestingOkS jmps c2)"

    59 | "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>

    60                                              jumpNestingOkS jmps c2)"

    61 | "jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"

    62 \<comment>\<open>The label of the while loop only handles continue jumps. Breaks are only

    63      handled by @{term Lab}\<close>

    64 | "jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"

    65 | "jumpNestingOkS jmps (Throw e) = True"

    66 | "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and>

    67                                                   jumpNestingOkS jmps c2)"

    68 | "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and>

    69                                           jumpNestingOkS jmps c2)"

    70 | "jumpNestingOkS jmps (Init C) = True"

    71  \<comment>\<open>wellformedness of the program must enshure that for all initializers

    72       jumpNestingOkS {} holds\<close>

    73 \<comment>\<open>Dummy analysis for intermediate smallstep term @{term  FinA}\<close>

    74 | "jumpNestingOkS jmps (FinA a c) = False"

    75

    76

    77 definition jumpNestingOk :: "jump set \<Rightarrow> term \<Rightarrow> bool" where

    78 "jumpNestingOk jmps t = (case t of

    79                       In1 se \<Rightarrow> (case se of

    80                                    Inl e \<Rightarrow> True

    81                                  | Inr s \<Rightarrow> jumpNestingOkS jmps s)

    82                     | In2  v \<Rightarrow> True

    83                     | In3  es \<Rightarrow> True)"

    84

    85 lemma jumpNestingOk_expr_simp [simp]: "jumpNestingOk jmps (In1l e) = True"

    86 by (simp add: jumpNestingOk_def)

    87

    88 lemma jumpNestingOk_expr_simp1 [simp]: "jumpNestingOk jmps \<langle>e::expr\<rangle> = True"

    89 by (simp add: inj_term_simps)

    90

    91 lemma jumpNestingOk_stmt_simp [simp]:

    92   "jumpNestingOk jmps (In1r s) = jumpNestingOkS jmps s"

    93 by (simp add: jumpNestingOk_def)

    94

    95 lemma jumpNestingOk_stmt_simp1 [simp]:

    96    "jumpNestingOk jmps \<langle>s::stmt\<rangle> = jumpNestingOkS jmps s"

    97 by (simp add: inj_term_simps)

    98

    99 lemma jumpNestingOk_var_simp [simp]: "jumpNestingOk jmps (In2 v) = True"

   100 by (simp add: jumpNestingOk_def)

   101

   102 lemma jumpNestingOk_var_simp1 [simp]: "jumpNestingOk jmps \<langle>v::var\<rangle> = True"

   103 by (simp add: inj_term_simps)

   104

   105 lemma jumpNestingOk_expr_list_simp [simp]: "jumpNestingOk jmps (In3 es) = True"

   106 by (simp add: jumpNestingOk_def)

   107

   108 lemma jumpNestingOk_expr_list_simp1 [simp]:

   109   "jumpNestingOk jmps \<langle>es::expr list\<rangle> = True"

   110 by (simp add: inj_term_simps)

   111

   112

   113

   114 subsubsection \<open>Calculation of assigned variables for boolean expressions\<close>

   115

   116

   117 subsection \<open>Very restricted calculation fallback calculation\<close>

   118

   119 primrec the_LVar_name :: "var \<Rightarrow> lname"

   120   where "the_LVar_name (LVar n) = n"

   121

   122 primrec assignsE :: "expr \<Rightarrow> lname set"

   123   and assignsV :: "var \<Rightarrow> lname set"

   124   and assignsEs:: "expr list \<Rightarrow> lname set"

   125 where

   126   "assignsE (NewC c)            = {}"

   127 | "assignsE (NewA t e)          = assignsE e"

   128 | "assignsE (Cast t e)          = assignsE e"

   129 | "assignsE (e InstOf r)        = assignsE e"

   130 | "assignsE (Lit val)           = {}"

   131 | "assignsE (UnOp unop e)       = assignsE e"

   132 | "assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr

   133                                        then (assignsE e1)

   134                                        else (assignsE e1) \<union> (assignsE e2))"

   135 | "assignsE (Super)             = {}"

   136 | "assignsE (Acc v)             = assignsV v"

   137 | "assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union>

   138                                    (if \<exists> n. v=(LVar n) then {the_LVar_name v}

   139                                                        else {})"

   140 | "assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"

   141 | "assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args))

   142                             = (assignsE objRef) \<union> (assignsEs args)"

   143 \<comment> \<open>Only dummy analysis for intermediate expressions

   144       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee}\<close>

   145 | "assignsE (Methd C sig)   = {}"

   146 | "assignsE (Body  C s)     = {}"

   147 | "assignsE (InsInitE s e)  = {}"

   148 | "assignsE (Callee l e)    = {}"

   149

   150 | "assignsV (LVar n)       = {}"

   151 | "assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"

   152 | "assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"

   153

   154 | "assignsEs     [] = {}"

   155 | "assignsEs (e#es) = assignsE e \<union> assignsEs es"

   156

   157 definition assigns :: "term \<Rightarrow> lname set" where

   158 "assigns t = (case t of

   159                 In1 se \<Rightarrow> (case se of

   160                              Inl e \<Rightarrow> assignsE e

   161                            | Inr s \<Rightarrow> {})

   162               | In2  v \<Rightarrow> assignsV v

   163               | In3  es \<Rightarrow> assignsEs es)"

   164

   165 lemma assigns_expr_simp [simp]: "assigns (In1l e) = assignsE e"

   166 by (simp add: assigns_def)

   167

   168 lemma assigns_expr_simp1 [simp]: "assigns (\<langle>e\<rangle>) = assignsE e"

   169 by (simp add: inj_term_simps)

   170

   171 lemma assigns_stmt_simp [simp]: "assigns (In1r s) = {}"

   172 by (simp add: assigns_def)

   173

   174 lemma assigns_stmt_simp1 [simp]: "assigns (\<langle>s::stmt\<rangle>) = {}"

   175 by (simp add: inj_term_simps)

   176

   177 lemma assigns_var_simp [simp]: "assigns (In2 v) = assignsV v"

   178 by (simp add: assigns_def)

   179

   180 lemma assigns_var_simp1 [simp]: "assigns (\<langle>v\<rangle>) = assignsV v"

   181 by (simp add: inj_term_simps)

   182

   183 lemma assigns_expr_list_simp [simp]: "assigns (In3 es) = assignsEs es"

   184 by (simp add: assigns_def)

   185

   186 lemma assigns_expr_list_simp1 [simp]: "assigns (\<langle>es\<rangle>) = assignsEs es"

   187 by (simp add: inj_term_simps)

   188

   189 subsection "Analysis of constant expressions"

   190

   191 primrec constVal :: "expr \<Rightarrow> val option"

   192 where

   193   "constVal (NewC c)      = None"

   194 | "constVal (NewA t e)    = None"

   195 | "constVal (Cast t e)    = None"

   196 | "constVal (Inst e r)    = None"

   197 | "constVal (Lit val)     = Some val"

   198 | "constVal (UnOp unop e) = (case (constVal e) of

   199                                None   \<Rightarrow> None

   200                              | Some v \<Rightarrow> Some (eval_unop unop v))"

   201 | "constVal (BinOp binop e1 e2) = (case (constVal e1) of

   202                                      None    \<Rightarrow> None

   203                                    | Some v1 \<Rightarrow> (case (constVal e2) of

   204                                                   None    \<Rightarrow> None

   205                                                 | Some v2 \<Rightarrow> Some (eval_binop

   206                                                                    binop v1 v2)))"

   207 | "constVal (Super)         = None"

   208 | "constVal (Acc v)         = None"

   209 | "constVal (Ass v e)       = None"

   210 | "constVal (Cond b e1 e2)  = (case (constVal b) of

   211                                  None   \<Rightarrow> None

   212                                | Some bv\<Rightarrow> (case the_Bool bv of

   213                                               True \<Rightarrow> (case (constVal e2) of

   214                                                          None   \<Rightarrow> None

   215                                                        | Some v \<Rightarrow> constVal e1)

   216                                             | False\<Rightarrow> (case (constVal e1) of

   217                                                          None   \<Rightarrow> None

   218                                                        | Some v \<Rightarrow> constVal e2)))"

   219 \<comment>\<open>Note that \<open>constVal (Cond b e1 e2)\<close> is stricter as it could be.

   220      It requires that all tree expressions are constant even if we can decide

   221      which branch to choose, provided the constant value of @{term b}\<close>

   222 | "constVal (Call accC statT mode objRef mn pTs args) = None"

   223 | "constVal (Methd C sig)   = None"

   224 | "constVal (Body  C s)     = None"

   225 | "constVal (InsInitE s e)  = None"

   226 | "constVal (Callee l e)    = None"

   227

   228 lemma constVal_Some_induct [consumes 1, case_names Lit UnOp BinOp CondL CondR]:

   229   assumes const: "constVal e = Some v" and

   230         hyp_Lit: "\<And> v. P (Lit v)" and

   231        hyp_UnOp: "\<And> unop e'. P e' \<Longrightarrow> P (UnOp unop e')" and

   232       hyp_BinOp: "\<And> binop e1 e2. \<lbrakk>P e1; P e2\<rbrakk> \<Longrightarrow> P (BinOp binop e1 e2)" and

   233       hyp_CondL: "\<And> b bv e1 e2. \<lbrakk>constVal b = Some bv; the_Bool bv; P b; P e1\<rbrakk>

   234                               \<Longrightarrow> P (b? e1 : e2)" and

   235       hyp_CondR: "\<And> b bv e1 e2. \<lbrakk>constVal b = Some bv; \<not>the_Bool bv; P b; P e2\<rbrakk>

   236                               \<Longrightarrow> P (b? e1 : e2)"

   237   shows "P e"

   238 proof -

   239   have "\<And> v. constVal e = Some v \<Longrightarrow> P e"

   240   proof (induct e)

   241     case Lit

   242     show ?case by (rule hyp_Lit)

   243   next

   244     case UnOp

   245     thus ?case

   246       by (auto intro: hyp_UnOp)

   247   next

   248     case BinOp

   249     thus ?case

   250       by (auto intro: hyp_BinOp)

   251   next

   252     case (Cond b e1 e2)

   253     then obtain v where   v: "constVal (b ? e1 : e2) = Some v"

   254       by blast

   255     then obtain bv where bv: "constVal b = Some bv"

   256       by simp

   257     show ?case

   258     proof (cases "the_Bool bv")

   259       case True

   260       with Cond show ?thesis using v bv

   261         by (auto intro: hyp_CondL)

   262     next

   263       case False

   264       with Cond show ?thesis using v bv

   265         by (auto intro: hyp_CondR)

   266     qed

   267   qed (simp_all add: hyp_Lit)

   268   with const

   269   show ?thesis

   270     by blast

   271 qed

   272

   273 lemma assignsE_const_simp: "constVal e = Some v \<Longrightarrow> assignsE e = {}"

   274   by (induct rule: constVal_Some_induct) simp_all

   275

   276

   277 subsection \<open>Main analysis for boolean expressions\<close>

   278

   279 text \<open>Assigned local variables after evaluating the expression if it evaluates

   280 to a specific boolean value. If the expression cannot evaluate to a

   281 @{term Boolean} value UNIV is returned. If we expect true/false the opposite

   282 constant false/true will also lead to UNIV.\<close>

   283 primrec assigns_if :: "bool \<Rightarrow> expr \<Rightarrow> lname set"

   284 where

   285   "assigns_if b (NewC c)            = UNIV" \<comment>\<open>can never evaluate to Boolean\<close>

   286 | "assigns_if b (NewA t e)          = UNIV" \<comment>\<open>can never evaluate to Boolean\<close>

   287 | "assigns_if b (Cast t e)          = assigns_if b e"

   288 | "assigns_if b (Inst e r)          = assignsE e" \<comment>\<open>Inst has type Boolean but

   289                                                        e is a reference type\<close>

   290 | "assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"

   291 | "assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of

   292                                            None   \<Rightarrow> (if unop = UNot

   293                                                          then assigns_if (\<not>b) e

   294                                                          else UNIV)

   295                                          | Some v \<Rightarrow> (if v=Bool b

   296                                                          then {}

   297                                                          else UNIV))"

   298 | "assigns_if b (BinOp binop e1 e2)

   299     = (case constVal (BinOp binop e1 e2) of

   300          None \<Rightarrow> (if binop=CondAnd then

   301                      (case b of

   302                          True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2

   303                       |  False \<Rightarrow> assigns_if False e1 \<inter>

   304                                   (assigns_if True e1 \<union> assigns_if False e2))

   305                   else

   306                  (if binop=CondOr then

   307                      (case b of

   308                          True  \<Rightarrow> assigns_if True e1 \<inter>

   309                                   (assigns_if False e1 \<union> assigns_if True e2)

   310                       |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)

   311                   else assignsE e1 \<union> assignsE e2))

   312        | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"

   313

   314 | "assigns_if b (Super)      = UNIV" \<comment>\<open>can never evaluate to Boolean\<close>

   315 | "assigns_if b (Acc v)      = (assignsV v)"

   316 | "assigns_if b (v := e)     = (assignsE (Ass v e))"

   317 | "assigns_if b (c? e1 : e2) = (assignsE c) \<union>

   318                                  (case (constVal c) of

   319                                     None    \<Rightarrow> (assigns_if b e1) \<inter>

   320                                                (assigns_if b e2)

   321                                   | Some bv \<Rightarrow> (case the_Bool bv of

   322                                                   True  \<Rightarrow> assigns_if b e1

   323                                                 | False \<Rightarrow> assigns_if b e2))"

   324 | "assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))

   325             = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "

   326 \<comment> \<open>Only dummy analysis for intermediate expressions

   327       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee}\<close>

   328 | "assigns_if b (Methd C sig)   = {}"

   329 | "assigns_if b (Body  C s)     = {}"

   330 | "assigns_if b (InsInitE s e)  = {}"

   331 | "assigns_if b (Callee l e)    = {}"

   332

   333 lemma assigns_if_const_b_simp:

   334   assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")

   335   shows   "assigns_if b e = {}" (is "?Ass b e")

   336 proof -

   337   have "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e"

   338   proof (induct e)

   339     case Lit

   340     thus ?case by simp

   341   next

   342     case UnOp

   343     thus ?case by simp

   344   next

   345     case (BinOp binop)

   346     thus ?case

   347       by (cases binop) (simp_all)

   348   next

   349     case (Cond c e1 e2 b)

   350     note hyp_c = \<open>\<And> b. ?Const b c \<Longrightarrow> ?Ass b c\<close>

   351     note hyp_e1 = \<open>\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1\<close>

   352     note hyp_e2 = \<open>\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2\<close>

   353     note const = \<open>constVal (c ? e1 : e2) = Some (Bool b)\<close>

   354     then obtain bv where bv: "constVal c = Some bv"

   355       by simp

   356     hence emptyC: "assignsE c = {}" by (rule assignsE_const_simp)

   357     show ?case

   358     proof (cases "the_Bool bv")

   359       case True

   360       with const bv

   361       have "?Const b e1" by simp

   362       hence "?Ass b e1" by (rule hyp_e1)

   363       with emptyC bv True

   364       show ?thesis

   365         by simp

   366     next

   367       case False

   368       with const bv

   369       have "?Const b e2" by simp

   370       hence "?Ass b e2" by (rule hyp_e2)

   371       with emptyC bv False

   372       show ?thesis

   373         by simp

   374     qed

   375   qed (simp_all)

   376   with boolConst

   377   show ?thesis

   378     by blast

   379 qed

   380

   381 lemma assigns_if_const_not_b_simp:

   382   assumes boolConst: "constVal e = Some (Bool b)"        (is "?Const b e")

   383   shows "assigns_if (\<not>b) e = UNIV"                  (is "?Ass b e")

   384 proof -

   385   have "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e"

   386   proof (induct e)

   387     case Lit

   388     thus ?case by simp

   389   next

   390     case UnOp

   391     thus ?case by simp

   392   next

   393     case (BinOp binop)

   394     thus ?case

   395       by (cases binop) (simp_all)

   396   next

   397     case (Cond c e1 e2 b)

   398     note hyp_c = \<open>\<And> b. ?Const b c \<Longrightarrow> ?Ass b c\<close>

   399     note hyp_e1 = \<open>\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1\<close>

   400     note hyp_e2 = \<open>\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2\<close>

   401     note const = \<open>constVal (c ? e1 : e2) = Some (Bool b)\<close>

   402     then obtain bv where bv: "constVal c = Some bv"

   403       by simp

   404     show ?case

   405     proof (cases "the_Bool bv")

   406       case True

   407       with const bv

   408       have "?Const b e1" by simp

   409       hence "?Ass b e1" by (rule hyp_e1)

   410       with bv True

   411       show ?thesis

   412         by simp

   413     next

   414       case False

   415       with const bv

   416       have "?Const b e2" by simp

   417       hence "?Ass b e2" by (rule hyp_e2)

   418       with bv False

   419       show ?thesis

   420         by simp

   421     qed

   422   qed (simp_all)

   423   with boolConst

   424   show ?thesis

   425     by blast

   426 qed

   427

   428 subsection \<open>Lifting set operations to range of tables (map to a set)\<close>

   429

   430 definition

   431   union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65)

   432   where "A \<Rightarrow>\<union> B = (\<lambda> k. A k \<union> B k)"

   433

   434 definition

   435   intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter>  _" [72,72] 71)

   436   where "A \<Rightarrow>\<inter>  B = (\<lambda>k. A k \<inter> B k)"

   437

   438 definition

   439   all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40)

   440   where "(A \<Rightarrow>\<union>\<^sub>\<forall> B) = (\<lambda> k. A k \<union> B)"

   441

   442 subsubsection \<open>Binary union of tables\<close>

   443

   444 lemma union_ts_iff [simp]: "(c \<in> (A \<Rightarrow>\<union> B) k) = (c \<in> A k \<or>  c \<in> B k)"

   445   by (unfold union_ts_def) blast

   446

   447 lemma union_tsI1 [elim?]: "c \<in> A k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k"

   448   by simp

   449

   450 lemma union_tsI2 [elim?]: "c \<in> B k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k"

   451   by simp

   452

   453 lemma union_tsCI [intro!]: "(c \<notin> B k \<Longrightarrow> c \<in> A k) \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k"

   454   by auto

   455

   456 lemma union_tsE [elim!]:

   457  "\<lbrakk>c \<in> (A \<Rightarrow>\<union> B) k; (c \<in> A k \<Longrightarrow> P); (c \<in> B k \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"

   458   by (unfold union_ts_def) blast

   459

   460 subsubsection \<open>Binary intersection of tables\<close>

   461

   462 lemma intersect_ts_iff [simp]: "c \<in> (A \<Rightarrow>\<inter> B) k = (c \<in> A k \<and> c \<in> B k)"

   463   by (unfold intersect_ts_def) blast

   464

   465 lemma intersect_tsI [intro!]: "\<lbrakk>c \<in> A k; c \<in> B k\<rbrakk> \<Longrightarrow> c \<in>  (A \<Rightarrow>\<inter> B) k"

   466   by simp

   467

   468 lemma intersect_tsD1: "c \<in> (A \<Rightarrow>\<inter> B) k \<Longrightarrow> c \<in> A k"

   469   by simp

   470

   471 lemma intersect_tsD2: "c \<in> (A \<Rightarrow>\<inter> B) k \<Longrightarrow> c \<in> B k"

   472   by simp

   473

   474 lemma intersect_tsE [elim!]:

   475    "\<lbrakk>c \<in> (A \<Rightarrow>\<inter> B) k; \<lbrakk>c \<in> A k; c \<in> B k\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"

   476   by simp

   477

   478

   479 subsubsection \<open>All-Union of tables and set\<close>

   480

   481 lemma all_union_ts_iff [simp]: "(c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k) = (c \<in> A k \<or>  c \<in> B)"

   482   by (unfold all_union_ts_def) blast

   483

   484 lemma all_union_tsI1 [elim?]: "c \<in> A k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k"

   485   by simp

   486

   487 lemma all_union_tsI2 [elim?]: "c \<in> B \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k"

   488   by simp

   489

   490 lemma all_union_tsCI [intro!]: "(c \<notin> B \<Longrightarrow> c \<in> A k) \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k"

   491   by auto

   492

   493 lemma all_union_tsE [elim!]:

   494  "\<lbrakk>c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k; (c \<in> A k \<Longrightarrow> P); (c \<in> B \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"

   495   by (unfold all_union_ts_def) blast

   496

   497

   498 subsubsection "The rules of definite assignment"

   499

   500

   501 type_synonym breakass = "(label, lname) tables"

   502 \<comment>\<open>Mapping from a break label, to the set of variables that will be assigned

   503      if the evaluation terminates with this break\<close>

   504

   505 record assigned =

   506          nrm :: "lname set" \<comment>\<open>Definetly assigned variables

   507                                  for normal completion\<close>

   508          brk :: "breakass" \<comment>\<open>Definetly assigned variables for

   509                                 abrupt completion with a break\<close>

   510

   511 definition

   512   rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"

   513   where "rmlab k A = (\<lambda>x. if x=k then UNIV else A x)"

   514

   515 (*

   516 definition

   517   setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where

   518   "setbrk b A = {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"

   519 *)

   520

   521 definition

   522   range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80)

   523   where "\<Rightarrow>\<Inter>A = {x |x. \<forall> k. x \<in> A k}"

   524

   525 text \<open>

   526 In \<open>E\<turnstile> B \<guillemotright>t\<guillemotright> A\<close>,

   527 \<open>B\<close> denotes the ''assigned'' variables before evaluating term \<open>t\<close>,

   528 whereas \<open>A\<close> denotes the ''assigned'' variables after evaluating term \<open>t\<close>.

   529 The environment @{term E} is only needed for the conditional \<open>_ ? _ : _\<close>.

   530 The definite assignment rules refer to the typing rules here to

   531 distinguish boolean and other expressions.

   532 \<close>

   533

   534 inductive

   535   da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71)

   536 where

   537   Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"

   538

   539 | Expr: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A

   540          \<Longrightarrow>

   541          Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"

   542 | Lab:  "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; nrm A = nrm C \<inter> (brk C) l; brk A = rmlab l (brk C)\<rbrakk>

   543          \<Longrightarrow>

   544          Env\<turnstile> B \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A"

   545

   546 | Comp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;

   547          nrm A = nrm C2; brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)\<rbrakk>

   548          \<Longrightarrow>

   549          Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A"

   550

   551 | If:   "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E;

   552           Env\<turnstile> (B \<union> assigns_if True  e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;

   553           Env\<turnstile> (B \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;

   554           nrm A = nrm C1 \<inter> nrm C2;

   555           brk A = brk C1 \<Rightarrow>\<inter> brk C2 \<rbrakk>

   556           \<Longrightarrow>

   557           Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A"

   558

   559 \<comment>\<open>Note that @{term E} is not further used, because we take the specialized

   560      sets that also consider if the expression evaluates to true or false.

   561      Inside of @{term e} there is no {\tt break} or {\tt finally}, so the break

   562      map of @{term E} will be the trivial one. So

   563      @{term "Env\<turnstile>B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"} is just used to ensure the definite assignment in

   564      expression @{term e}.

   565      Notice the implicit analysis of a constant boolean expression @{term e}

   566      in this rule. For example, if @{term e} is constantly @{term True} then

   567      @{term "assigns_if False e = UNIV"} and therefor @{term "nrm C2=UNIV"}.

   568      So finally @{term "nrm A = nrm C1"}. For the break maps this trick

   569      workd too, because the trival break map will map all labels to

   570      @{term UNIV}. In the example, if no break occurs in @{term c2} the break

   571      maps will trivially map to @{term UNIV} and if a break occurs it will map

   572      to @{term UNIV} too, because @{term "assigns_if False e = UNIV"}. So

   573      in the intersection of the break maps the path @{term c2} will have no

   574      contribution.

   575 \<close>

   576

   577 | Loop: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E;

   578           Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;

   579           nrm A = nrm C \<inter> (B \<union> assigns_if False e);

   580           brk A = brk C\<rbrakk>

   581           \<Longrightarrow>

   582           Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"

   583 \<comment>\<open>The \<open>Loop\<close> rule resembles some of the ideas of the \<open>If\<close> rule.

   584      For the @{term "nrm A"} the set @{term "B \<union> assigns_if False e"}

   585      will be @{term UNIV} if the condition is constantly true. To normally exit

   586      the while loop, we must consider the body @{term c} to be completed

   587      normally (@{term "nrm C"}) or with a break. But in this model,

   588      the label @{term l} of the loop

   589      only handles continue labels, not break labels. The break label will be

   590      handled by an enclosing @{term Lab} statement. So we don't have to

   591      handle the breaks specially.

   592 \<close>

   593

   594 | Jmp: "\<lbrakk>jump=Ret \<longrightarrow> Result \<in> B;

   595          nrm A = UNIV;

   596          brk A = (case jump of

   597                     Break l \<Rightarrow> \<lambda> k. if k=l then B else UNIV

   598                   | Cont l  \<Rightarrow> \<lambda> k. UNIV

   599                   | Ret     \<Rightarrow> \<lambda> k. UNIV)\<rbrakk>

   600         \<Longrightarrow>

   601         Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A"

   602 \<comment>\<open>In case of a break to label @{term l} the corresponding break set is all

   603      variables assigned before the break. The assigned variables for normal

   604      completion of the @{term Jmp} is @{term UNIV}, because the statement will

   605      never complete normally. For continue and return the break map is the

   606      trivial one. In case of a return we enshure that the result value is

   607      assigned.

   608 \<close>

   609

   610 | Throw: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = UNIV; brk A = (\<lambda> l. UNIV)\<rbrakk>

   611          \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"

   612

   613 | Try:  "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;

   614           Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;

   615           nrm A = nrm C1 \<inter> nrm C2;

   616           brk A = brk C1 \<Rightarrow>\<inter> brk C2\<rbrakk>

   617          \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A"

   618

   619 | Fin:  "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;

   620           Env\<turnstile> B \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;

   621           nrm A = nrm C1 \<union> nrm C2;

   622           brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)\<rbrakk>

   623           \<Longrightarrow>

   624           Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A"

   625 \<comment>\<open>The set of assigned variables before execution @{term c2} are the same

   626      as before execution @{term c1}, because @{term c1} could throw an exception

   627      and so we can't guarantee that any variable will be assigned in @{term c1}.

   628      The \<open>Finally\<close> statement completes

   629      normally if both @{term c1} and @{term c2} complete normally. If @{term c1}

   630      completes abruptly with a break, then @{term c2} also will be executed

   631      and may terminate normally or with a break. The overall break map then is

   632      the intersection of the maps of both paths. If @{term c2} terminates

   633      normally we have to extend all break sets in @{term "brk C1"} with

   634      @{term "nrm C2"} (\<open>\<Rightarrow>\<union>\<^sub>\<forall>\<close>). If @{term c2} exits with a break this

   635      break will appear in the overall result state. We don't know if

   636      @{term c1} completed normally or abruptly (maybe with an exception not only

   637      a break) so @{term c1} has no contribution to the break map following this

   638      path.

   639 \<close>

   640

   641 \<comment>\<open>Evaluation of expressions and the break sets of definite assignment:

   642      Thinking of a Java expression we assume that we can never have

   643      a break statement inside of a expression. So for all expressions the

   644      break sets could be set to the trivial one: @{term "\<lambda> l. UNIV"}.

   645      But we can't

   646      trivially proof, that evaluating an expression will never result in a

   647      break, allthough Java expressions allready syntactically don't allow

   648      nested stetements in them. The reason are the nested class initialzation

   649      statements which are inserted by the evaluation rules. So to proof the

   650      absence of a break we need to ensure, that the initialization statements

   651      will never end up in a break. In a wellfromed initialization statement,

   652      of course, were breaks are nested correctly inside of @{term Lab}

   653      or @{term Loop} statements evaluation of the whole initialization

   654      statement will never result in a break, because this break will be

   655      handled inside of the statement. But for simplicity we haven't added

   656      the analysis of the correct nesting of breaks in the typing judgments

   657      right now. So we have decided to adjust the rules of definite assignment

   658      to fit to these circumstances. If an initialization is involved during

   659      evaluation of the expression (evaluation rules \<open>FVar\<close>, \<open>NewC\<close>

   660      and \<open>NewA\<close>

   661 \<close>

   662

   663 | Init: "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"

   664 \<comment>\<open>Wellformedness of a program will ensure, that every static initialiser

   665      is definetly assigned and the jumps are nested correctly. The case here

   666      for @{term Init} is just for convenience, to get a proper precondition

   667      for the induction hypothesis in various proofs, so that we don't have to

   668      expand the initialisation on every point where it is triggerred by the

   669      evaluation rules.

   670 \<close>

   671 | NewC: "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"

   672

   673 | NewA: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A

   674          \<Longrightarrow>

   675          Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A"

   676

   677 | Cast: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A

   678          \<Longrightarrow>

   679          Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A"

   680

   681 | Inst: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A

   682          \<Longrightarrow>

   683          Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A"

   684

   685 | Lit:  "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"

   686

   687 | UnOp: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A

   688          \<Longrightarrow>

   689          Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A"

   690

   691 | CondAnd: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if True e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;

   692              nrm A = B \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter>

   693                              assigns_if False (BinOp CondAnd e1 e2));

   694              brk A = (\<lambda> l. UNIV) \<rbrakk>

   695             \<Longrightarrow>

   696             Env\<turnstile> B \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A"

   697

   698 | CondOr: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if False e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;

   699             nrm A = B \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter>

   700                               assigns_if False (BinOp CondOr e1 e2));

   701             brk A = (\<lambda> l. UNIV) \<rbrakk>

   702             \<Longrightarrow>

   703             Env\<turnstile> B \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A"

   704

   705 | BinOp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A;

   706            binop \<noteq> CondAnd; binop \<noteq> CondOr\<rbrakk>

   707           \<Longrightarrow>

   708           Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A"

   709

   710 | Super: "This \<in> B

   711           \<Longrightarrow>

   712           Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"

   713

   714 | AccLVar: "\<lbrakk>vn \<in> B;

   715              nrm A = B; brk A = (\<lambda> k. UNIV)\<rbrakk>

   716              \<Longrightarrow>

   717              Env\<turnstile> B \<guillemotright>\<langle>Acc (LVar vn)\<rangle>\<guillemotright> A"

   718 \<comment>\<open>To properly access a local variable we have to test the definite

   719      assignment here. The variable must occur in the set @{term B}

   720 \<close>

   721

   722 | Acc: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn;

   723          Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> A\<rbrakk>

   724          \<Longrightarrow>

   725          Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A"

   726

   727 | AssLVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = nrm E \<union> {vn}; brk A = brk E\<rbrakk>

   728             \<Longrightarrow>

   729             Env\<turnstile> B \<guillemotright>\<langle>(LVar vn) := e\<rangle>\<guillemotright> A"

   730

   731 | Ass: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn; Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V; Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A\<rbrakk>

   732          \<Longrightarrow>

   733          Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A"

   734

   735 | CondBool: "\<lbrakk>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean);

   736               Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;

   737               Env\<turnstile> (B \<union> assigns_if True  c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1;

   738               Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;

   739               nrm A = B \<union> (assigns_if True  (c ? e1 : e2) \<inter>

   740                                assigns_if False (c ? e1 : e2));

   741               brk A = (\<lambda> l. UNIV)\<rbrakk>

   742               \<Longrightarrow>

   743               Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A"

   744

   745 | Cond: "\<lbrakk>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean);

   746           Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;

   747           Env\<turnstile> (B \<union> assigns_if True  c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1;

   748           Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;

   749           nrm A = nrm E1 \<inter> nrm E2; brk A = (\<lambda> l. UNIV)\<rbrakk>

   750           \<Longrightarrow>

   751           Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A"

   752

   753 | Call: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A\<rbrakk>

   754          \<Longrightarrow>

   755          Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A"

   756

   757 \<comment> \<open>The interplay of @{term Call}, @{term Methd} and @{term Body}:

   758       Why rules for @{term Methd} and @{term Body} at all? Note that a

   759       Java source program will not include bare  @{term Methd} or @{term Body}

   760       terms. These terms are just introduced during evaluation. So definite

   761       assignment of @{term Call} does not consider @{term Methd} or

   762       @{term Body} at all. So for definite assignment alone we could omit the

   763       rules for @{term Methd} and @{term Body}.

   764       But since evaluation of the method invocation is

   765       split up into three rules we must ensure that we have enough information

   766       about the call even in the @{term Body} term to make sure that we can

   767       proof type safety. Also we must be able transport this information

   768       from @{term Call} to @{term Methd} and then further to @{term Body}

   769       during evaluation to establish the definite assignment of @{term Methd}

   770       during evaluation of @{term Call}, and of @{term Body} during evaluation

   771       of @{term Methd}. This is necessary since definite assignment will be

   772       a precondition for each induction hypothesis coming out of the evaluation

   773       rules, and therefor we have to establish the definite assignment of the

   774       sub-evaluation during the type-safety proof. Note that well-typedness is

   775       also a precondition for type-safety and so we can omit some assertion

   776       that are already ensured by well-typedness.

   777 \<close>

   778 | Methd: "\<lbrakk>methd (prg Env) D sig = Some m;

   779            Env\<turnstile> B \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A

   780           \<rbrakk>

   781           \<Longrightarrow>

   782           Env\<turnstile> B \<guillemotright>\<langle>Methd D sig\<rangle>\<guillemotright> A"

   783

   784 | Body: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; jumpNestingOkS {Ret} c; Result \<in> nrm C;

   785           nrm A = B; brk A = (\<lambda> l. UNIV)\<rbrakk>

   786          \<Longrightarrow>

   787          Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A"

   788 \<comment> \<open>Note that @{term A} is not correlated to  @{term C}. If the body

   789       statement returns abruptly with return, evaluation of  @{term Body}

   790       will absorb this return and complete normally. So we cannot trivially

   791       get the assigned variables of the body statement since it has not

   792       completed normally or with a break.

   793       If the body completes normally we guarantee that the result variable

   794       is set with this rule. But if the body completes abruptly with a return

   795       we can't guarantee that the result variable is set here, since

   796       definite assignment only talks about normal completion and breaks. So

   797       for a return the @{term Jump} rule ensures that the result variable is

   798       set and then this information must be carried over to the @{term Body}

   799       rule by the conformance predicate of the state.

   800 \<close>

   801 | LVar: "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>"

   802

   803 | FVar: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A

   804          \<Longrightarrow>

   805          Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A"

   806

   807 | AVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A\<rbrakk>

   808           \<Longrightarrow>

   809           Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A"

   810

   811 | Nil: "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>"

   812

   813 | Cons: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e::expr\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A\<rbrakk>

   814          \<Longrightarrow>

   815          Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A"

   816

   817

   818 declare inj_term_sym_simps [simp]

   819 declare assigns_if.simps [simp del]

   820 declare split_paired_All [simp del] split_paired_Ex [simp del]

   821 setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>

   822

   823 inductive_cases da_elim_cases [cases set]:

   824   "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"

   825   "Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A"

   826   "Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"

   827   "Env\<turnstile> B \<guillemotright>In1r (Expr e)\<guillemotright> A"

   828   "Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> c\<rangle>\<guillemotright> A"

   829   "Env\<turnstile> B \<guillemotright>In1r (l\<bullet> c)\<guillemotright> A"

   830   "Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A"

   831   "Env\<turnstile> B \<guillemotright>In1r (c1;; c2)\<guillemotright> A"

   832   "Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A"

   833   "Env\<turnstile> B \<guillemotright>In1r (If(e) c1 Else c2)\<guillemotright> A"

   834   "Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"

   835   "Env\<turnstile> B \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A"

   836   "Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A"

   837   "Env\<turnstile> B \<guillemotright>In1r (Jmp jump)\<guillemotright> A"

   838   "Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"

   839   "Env\<turnstile> B \<guillemotright>In1r (Throw e)\<guillemotright> A"

   840   "Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A"

   841   "Env\<turnstile> B \<guillemotright>In1r (Try c1 Catch(C vn) c2)\<guillemotright> A"

   842   "Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A"

   843   "Env\<turnstile> B \<guillemotright>In1r (c1 Finally c2)\<guillemotright> A"

   844   "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> A"

   845   "Env\<turnstile> B \<guillemotright>In1r (Init C)\<guillemotright> A"

   846   "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> A"

   847   "Env\<turnstile> B \<guillemotright>In1l (NewC C)\<guillemotright> A"

   848   "Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A"

   849   "Env\<turnstile> B \<guillemotright>In1l (New T[e])\<guillemotright> A"

   850   "Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A"

   851   "Env\<turnstile> B \<guillemotright>In1l (Cast T e)\<guillemotright> A"

   852   "Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A"

   853   "Env\<turnstile> B \<guillemotright>In1l (e InstOf T)\<guillemotright> A"

   854   "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> A"

   855   "Env\<turnstile> B \<guillemotright>In1l (Lit v)\<guillemotright> A"

   856   "Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A"

   857   "Env\<turnstile> B \<guillemotright>In1l (UnOp unop e)\<guillemotright> A"

   858   "Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A"

   859   "Env\<turnstile> B \<guillemotright>In1l (BinOp binop e1 e2)\<guillemotright> A"

   860   "Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> A"

   861   "Env\<turnstile> B \<guillemotright>In1l (Super)\<guillemotright> A"

   862   "Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A"

   863   "Env\<turnstile> B \<guillemotright>In1l (Acc v)\<guillemotright> A"

   864   "Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A"

   865   "Env\<turnstile> B \<guillemotright>In1l (v := e)\<guillemotright> A"

   866   "Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A"

   867   "Env\<turnstile> B \<guillemotright>In1l (c ? e1 : e2)\<guillemotright> A"

   868   "Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A"

   869   "Env\<turnstile> B \<guillemotright>In1l ({accC,statT,mode}e\<cdot>mn({pTs}args))\<guillemotright> A"

   870   "Env\<turnstile> B \<guillemotright>\<langle>Methd C sig\<rangle>\<guillemotright> A"

   871   "Env\<turnstile> B \<guillemotright>In1l (Methd C sig)\<guillemotright> A"

   872   "Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A"

   873   "Env\<turnstile> B \<guillemotright>In1l (Body D c)\<guillemotright> A"

   874   "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> A"

   875   "Env\<turnstile> B \<guillemotright>In2 (LVar vn)\<guillemotright> A"

   876   "Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A"

   877   "Env\<turnstile> B \<guillemotright>In2 ({accC,statDeclC,stat}e..fn)\<guillemotright> A"

   878   "Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A"

   879   "Env\<turnstile> B \<guillemotright>In2 (e1.[e2])\<guillemotright> A"

   880   "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> A"

   881   "Env\<turnstile> B \<guillemotright>In3 ([]::expr list)\<guillemotright> A"

   882   "Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A"

   883   "Env\<turnstile> B \<guillemotright>In3 (e#es)\<guillemotright> A"

   884 declare inj_term_sym_simps [simp del]

   885 declare assigns_if.simps [simp]

   886 declare split_paired_All [simp] split_paired_Ex [simp]

   887 setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>

   888

   889 (* To be able to eliminate both the versions with the overloaded brackets:

   890    (B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A),

   891    every rule appears in both versions

   892  *)

   893

   894 lemma da_Skip: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"

   895   by (auto intro: da.Skip)

   896

   897 lemma da_NewC: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> A"

   898   by (auto intro: da.NewC)

   899

   900 lemma da_Lit:  "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> A"

   901   by (auto intro: da.Lit)

   902

   903 lemma da_Super: "\<lbrakk>This \<in> B;A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>\<rbrakk> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> A"

   904   by (auto intro: da.Super)

   905

   906 lemma da_Init: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> A"

   907   by (auto intro: da.Init)

   908

   909

   910 (*

   911 For boolean expressions:

   912

   913 The following holds: "assignsE e \<subseteq> assigns_if True e \<inter> assigns_if False e"

   914 but not vice versa:

   915  "assigns_if True e \<inter> assigns_if False e \<subseteq> assignsE e"

   916

   917 Example:

   918  e = ((x < 5) || (y = true)) && (y = true)

   919

   920    =  (   a    ||    b     ) &&    c

   921

   922 assigns_if True  a = {}

   923 assigns_if False a = {}

   924

   925 assigns_if True  b = {y}

   926 assigns_if False b = {y}

   927

   928 assigns_if True  c = {y}

   929 assigns_if False c = {y}

   930

   931 assigns_if True (a || b) = assigns_if True a \<inter>

   932                                 (assigns_if False a \<union> assigns_if True b)

   933                            = {} \<inter> ({} \<union> {y}) = {}

   934 assigns_if False (a || b) = assigns_if False a \<union> assigns_if False b

   935                             = {} \<union> {y} = {y}

   936

   937

   938

   939 assigns_ifE True e =  assigns_if True (a || b) \<union> assigns_if True c

   940                     = {} \<union> {y} = {y}

   941 assigns_ifE False e = assigns_if False (a || b) \<inter>

   942                        (assigns_if True (a || b) \<union> assigns_if False c)

   943                      = {y} \<inter> ({} \<union> {y}) = {y}

   944

   945 assignsE e = {}

   946 *)

   947

   948 lemma assignsE_subseteq_assigns_ifs:

   949  assumes boolEx: "E\<turnstile>e\<Colon>-PrimT Boolean" (is "?Boolean e")

   950    shows "assignsE e \<subseteq> assigns_if True e \<inter> assigns_if False e" (is "?Incl e")

   951 proof -

   952   obtain vv where ex_lit: "E\<turnstile>Lit vv\<Colon>- PrimT Boolean"

   953     using typeof.simps(2) wt.Lit by blast

   954   have "?Boolean e \<Longrightarrow> ?Incl e"

   955   proof (induct e)

   956     case (Cast T e)

   957     have "E\<turnstile>e\<Colon>- (PrimT Boolean)"

   958     proof -

   959       from \<open>E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)\<close>

   960       obtain Te where "E\<turnstile>e\<Colon>-Te"

   961                            "prg E\<turnstile>Te\<preceq>? PrimT Boolean"

   962         by cases simp

   963       thus ?thesis

   964         by - (drule cast_Boolean2,simp)

   965     qed

   966     with Cast.hyps

   967     show ?case

   968       by simp

   969   next

   970     case (Lit val)

   971     thus ?case

   972       by - (erule wt_elim_cases, cases "val", auto simp add: empty_dt_def)

   973   next

   974     case (UnOp unop e)

   975     thus ?case

   976       by - (erule wt_elim_cases,cases unop,

   977             (fastforce simp add: assignsE_const_simp)+)

   978   next

   979     case (BinOp binop e1 e2)

   980     from BinOp.prems obtain e1T e2T

   981       where "E\<turnstile>e1\<Colon>-e1T" and "E\<turnstile>e2\<Colon>-e2T" and "wt_binop (prg E) binop e1T e2T"

   982             and "(binop_type binop) = Boolean"

   983       by (elim wt_elim_cases) simp

   984     with BinOp.hyps

   985     show ?case

   986       by - (cases binop, auto simp add: assignsE_const_simp)

   987   next

   988     case (Cond c e1 e2)

   989     note hyp_c = \<open>?Boolean c \<Longrightarrow> ?Incl c\<close>

   990     note hyp_e1 = \<open>?Boolean e1 \<Longrightarrow> ?Incl e1\<close>

   991     note hyp_e2 = \<open>?Boolean e2 \<Longrightarrow> ?Incl e2\<close>

   992     note wt = \<open>E\<turnstile>(c ? e1 : e2)\<Colon>-PrimT Boolean\<close>

   993     then obtain

   994       boolean_c:  "E\<turnstile>c\<Colon>-PrimT Boolean" and

   995       boolean_e1: "E\<turnstile>e1\<Colon>-PrimT Boolean" and

   996       boolean_e2: "E\<turnstile>e2\<Colon>-PrimT Boolean"

   997       by (elim wt_elim_cases) (auto dest: widen_Boolean2)

   998     show ?case

   999     proof (cases "constVal c")

  1000       case None

  1001       with boolean_e1 boolean_e2

  1002       show ?thesis

  1003         using hyp_e1 hyp_e2

  1004         by (auto)

  1005     next

  1006       case (Some bv)

  1007       show ?thesis

  1008       proof (cases "the_Bool bv")

  1009         case True

  1010         with Some show ?thesis using hyp_e1 boolean_e1 by auto

  1011       next

  1012         case False

  1013         with Some show ?thesis using hyp_e2 boolean_e2 by auto

  1014       qed

  1015     qed

  1016   next

  1017     show "\<And>x. E\<turnstile>Lit vv\<Colon>-PrimT Boolean"

  1018       by (rule ex_lit)

  1019   qed (simp_all add: ex_lit)

  1020   with boolEx

  1021   show ?thesis

  1022     by blast

  1023 qed

  1024

  1025

  1026 (* Trick:

  1027    If you have a rule with the abstract term injections:

  1028    e.g:  da.Skip "B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"

  1029    and the current goal state as an concrete injection:

  1030    e.g: "B \<guillemotright>In1r Skip\<guillemotright> A"

  1031    you can convert the rule by: da.Skip [simplified]

  1032    if inj_term_simps is in the simpset

  1033

  1034 *)

  1035

  1036 lemma rmlab_same_label [simp]: "(rmlab l A) l = UNIV"

  1037   by (simp add: rmlab_def)

  1038

  1039 lemma rmlab_same_label1 [simp]: "l=l' \<Longrightarrow> (rmlab l A) l' = UNIV"

  1040   by (simp add: rmlab_def)

  1041

  1042 lemma rmlab_other_label [simp]: "l\<noteq>l'\<Longrightarrow> (rmlab l A) l' = A l'"

  1043   by (auto simp add: rmlab_def)

  1044

  1045 lemma range_inter_ts_subseteq [intro]: "\<forall> k. A k \<subseteq> B k \<Longrightarrow> \<Rightarrow>\<Inter>A \<subseteq> \<Rightarrow>\<Inter>B"

  1046   by (auto simp add: range_inter_ts_def)

  1047

  1048 lemma range_inter_ts_subseteq': "\<forall> k. A k \<subseteq> B k \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>A \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>B"

  1049   by (auto simp add: range_inter_ts_def)

  1050

  1051 lemma da_monotone:

  1052   assumes da: "Env\<turnstile> B  \<guillemotright>t\<guillemotright> A" and

  1053     "B \<subseteq> B'" and

  1054     da': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'"

  1055   shows "(nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"

  1056 proof -

  1057   from da

  1058   have "\<And> B' A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; B \<subseteq> B'\<rbrakk>

  1059                   \<Longrightarrow> (nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"

  1060        (is "PROP ?Hyp Env B t A")

  1061   proof (induct)

  1062     case Skip

  1063     then show ?case by cases simp

  1064   next

  1065     case Expr

  1066     from Expr.prems Expr.hyps

  1067     show ?case by cases simp

  1068   next

  1069     case (Lab Env B c C A l B' A')

  1070     note A = \<open>nrm A = nrm C \<inter> brk C l\<close> \<open>brk A = rmlab l (brk C)\<close>

  1071     note \<open>PROP ?Hyp Env B \<langle>c\<rangle> C\<close>

  1072     moreover

  1073     note \<open>B \<subseteq> B'\<close>

  1074     moreover

  1075     obtain C'

  1076       where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"

  1077         and A': "nrm A' = nrm C' \<inter> brk C' l" "brk A' = rmlab l (brk C')"

  1078       using Lab.prems

  1079       by cases simp

  1080     ultimately

  1081     have "nrm C \<subseteq> nrm C'" and hyp_brk: "(\<forall>l. brk C l \<subseteq> brk C' l)" by auto

  1082     then

  1083     have "nrm C \<inter> brk C l \<subseteq> nrm C' \<inter> brk C' l" by auto

  1084     moreover

  1085     {

  1086       fix l'

  1087       from hyp_brk

  1088       have "rmlab l (brk C) l'  \<subseteq> rmlab l (brk C') l'"

  1089         by  (cases "l=l'") simp_all

  1090     }

  1091     moreover note A A'

  1092     ultimately show ?case

  1093       by simp

  1094   next

  1095     case (Comp Env B c1 C1 c2 C2 A B' A')

  1096     note A = \<open>nrm A = nrm C2\<close> \<open>brk A = brk C1 \<Rightarrow>\<inter>  brk C2\<close>

  1097     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'\<close>

  1098     obtain  C1' C2'

  1099       where da_c1: "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and

  1100             da_c2: "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"  and

  1101             A': "nrm A' = nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'"

  1102       by cases auto

  1103     note \<open>PROP ?Hyp Env B \<langle>c1\<rangle> C1\<close>

  1104     moreover note \<open>B \<subseteq> B'\<close>

  1105     moreover note da_c1

  1106     ultimately have C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"

  1107       by auto

  1108     note \<open>PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle> C2\<close>

  1109     with da_c2 C1'

  1110     have C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"

  1111       by auto

  1112     with A A' C1'

  1113     show ?case

  1114       by auto

  1115   next

  1116     case (If Env B e E c1 C1 c2 C2 A B' A')

  1117     note A = \<open>nrm A = nrm C1 \<inter> nrm C2\<close> \<open>brk A = brk C1 \<Rightarrow>\<inter>  brk C2\<close>

  1118     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'\<close>

  1119     obtain C1' C2'

  1120       where da_c1: "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and

  1121             da_c2: "Env\<turnstile> B' \<union> assigns_if False e \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

  1122                A': "nrm A' = nrm C1' \<inter> nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'"

  1123       by cases auto

  1124     note \<open>PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1\<close>

  1125     moreover note B' = \<open>B \<subseteq> B'\<close>

  1126     moreover note da_c1

  1127     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"

  1128       by blast

  1129     note \<open>PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle> C2\<close>

  1130     with da_c2 B'

  1131     obtain C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"

  1132       by blast

  1133     with A A' C1'

  1134     show ?case

  1135       by auto

  1136   next

  1137     case (Loop Env B e E c C A l B' A')

  1138     note A = \<open>nrm A = nrm C \<inter> (B \<union> assigns_if False e)\<close> \<open>brk A = brk C\<close>

  1139     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'\<close>

  1140     obtain C'

  1141       where

  1142        da_c': "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and

  1143           A': "nrm A' = nrm C' \<inter> (B' \<union> assigns_if False e)"

  1144               "brk A' = brk C'"

  1145       by cases auto

  1146     note \<open>PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C\<close>

  1147     moreover note B' = \<open>B \<subseteq> B'\<close>

  1148     moreover note da_c'

  1149     ultimately obtain C': "nrm C \<subseteq> nrm C'" "(\<forall>l. brk C l \<subseteq> brk C' l)"

  1150       by blast

  1151     with A A' B'

  1152     have "nrm A \<subseteq> nrm A'"

  1153       by blast

  1154     moreover

  1155     { fix l'

  1156       have  "brk A l' \<subseteq> brk A' l'"

  1157       proof (cases "constVal e")

  1158         case None

  1159         with A A' C'

  1160         show ?thesis

  1161            by (cases "l=l'") auto

  1162       next

  1163         case (Some bv)

  1164         with A A' C'

  1165         show ?thesis

  1166           by (cases "the_Bool bv", cases "l=l'") auto

  1167       qed

  1168     }

  1169     ultimately show ?case

  1170       by auto

  1171   next

  1172     case (Jmp jump B A Env B' A')

  1173     thus ?case by (elim da_elim_cases) (auto split: jump.splits)

  1174   next

  1175     case Throw thus ?case by (elim da_elim_cases) auto

  1176   next

  1177     case (Try Env B c1 C1 vn C c2 C2 A B' A')

  1178     note A = \<open>nrm A = nrm C1 \<inter> nrm C2\<close> \<open>brk A = brk C1 \<Rightarrow>\<inter>  brk C2\<close>

  1179     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'\<close>

  1180     obtain C1' C2'

  1181       where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and

  1182             da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn}

  1183                       \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

  1184             A': "nrm A' = nrm C1' \<inter> nrm C2'"

  1185                 "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'"

  1186       by cases auto

  1187     note \<open>PROP ?Hyp Env B \<langle>c1\<rangle> C1\<close>

  1188     moreover note B' = \<open>B \<subseteq> B'\<close>

  1189     moreover note da_c1'

  1190     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"

  1191       by blast

  1192     note \<open>PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)

  1193                     (B \<union> {VName vn}) \<langle>c2\<rangle> C2\<close>

  1194     with B' da_c2'

  1195     obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"

  1196       by blast

  1197     with C1' A A'

  1198     show ?case

  1199       by auto

  1200   next

  1201     case (Fin Env B c1 C1 c2 C2 A B' A')

  1202     note A = \<open>nrm A = nrm C1 \<union> nrm C2\<close>

  1203       \<open>brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)\<close>

  1204     from \<open>Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'\<close>

  1205     obtain C1' C2'

  1206       where  da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and

  1207              da_c2': "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and

  1208              A':  "nrm A' = nrm C1' \<union> nrm C2'"

  1209                   "brk A' = (brk C1' \<Rightarrow>\<union>\<^sub>\<forall> nrm C2') \<Rightarrow>\<inter> (brk C2')"

  1210       by cases auto

  1211     note \<open>PROP ?Hyp Env B \<langle>c1\<rangle> C1\<close>

  1212     moreover note B' = \<open>B \<subseteq> B'\<close>

  1213     moreover note da_c1'

  1214     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"

  1215       by blast

  1216     note hyp_c2 = \<open>PROP ?Hyp Env B \<langle>c2\<rangle> C2\<close>

  1217     from da_c2' B'

  1218      obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"

  1219        by - (drule hyp_c2,auto)

  1220      with A A' C1'

  1221      show ?case

  1222        by auto

  1223    next

  1224      case Init thus ?case by (elim da_elim_cases) auto

  1225    next

  1226      case NewC thus ?case by (elim da_elim_cases) auto

  1227    next

  1228      case NewA thus ?case by (elim da_elim_cases) auto

  1229    next

  1230      case Cast thus ?case by (elim da_elim_cases) auto

  1231    next

  1232      case Inst thus ?case by (elim da_elim_cases) auto

  1233    next

  1234      case Lit thus ?case by (elim da_elim_cases) auto

  1235    next

  1236      case UnOp thus ?case by (elim da_elim_cases) auto

  1237    next

  1238      case (CondAnd Env B e1 E1 e2 E2 A B' A')

  1239      note A = \<open>nrm A = B \<union>

  1240                        assigns_if True (BinOp CondAnd e1 e2) \<inter>

  1241                        assigns_if False (BinOp CondAnd e1 e2)\<close>

  1242              \<open>brk A = (\<lambda>l. UNIV)\<close>

  1243      from \<open>Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'\<close>

  1244      obtain  A': "nrm A' = B' \<union>

  1245                                  assigns_if True (BinOp CondAnd e1 e2) \<inter>

  1246                                  assigns_if False (BinOp CondAnd e1 e2)"

  1247                       "brk A' = (\<lambda>l. UNIV)"

  1248        by cases auto

  1249      note B' = \<open>B \<subseteq> B'\<close>

  1250      with A A' show ?case

  1251        by auto

  1252    next

  1253      case CondOr thus ?case by (elim da_elim_cases) auto

  1254    next

  1255      case BinOp thus ?case by (elim da_elim_cases) auto

  1256    next

  1257      case Super thus ?case by (elim da_elim_cases) auto

  1258    next

  1259      case AccLVar thus ?case by (elim da_elim_cases) auto

  1260    next

  1261      case Acc thus ?case by (elim da_elim_cases) auto

  1262    next

  1263      case AssLVar thus ?case by (elim da_elim_cases) auto

  1264    next

  1265      case Ass thus ?case by (elim da_elim_cases) auto

  1266    next

  1267      case (CondBool Env c e1 e2 B C E1 E2 A B' A')

  1268      note A = \<open>nrm A = B \<union>

  1269                         assigns_if True (c ? e1 : e2) \<inter>

  1270                         assigns_if False (c ? e1 : e2)\<close>

  1271              \<open>brk A = (\<lambda>l. UNIV)\<close>

  1272      note \<open>Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)\<close>

  1273      moreover

  1274      note \<open>Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'\<close>

  1275      ultimately

  1276      obtain A': "nrm A' = B' \<union>

  1277                                   assigns_if True (c ? e1 : e2) \<inter>

  1278                                   assigns_if False (c ? e1 : e2)"

  1279                      "brk A' = (\<lambda>l. UNIV)"

  1280        by (elim da_elim_cases) (auto simp add: inj_term_simps)

  1281        (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)

  1282      note B' = \<open>B \<subseteq> B'\<close>

  1283      with A A' show ?case

  1284        by auto

  1285    next

  1286      case (Cond Env c e1 e2 B C E1 E2 A B' A')

  1287      note A = \<open>nrm A = nrm E1 \<inter> nrm E2\<close> \<open>brk A = (\<lambda>l. UNIV)\<close>

  1288      note not_bool = \<open>\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)\<close>

  1289      from \<open>Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'\<close>

  1290      obtain E1' E2'

  1291        where da_e1': "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and

  1292              da_e2': "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and

  1293                  A': "nrm A' = nrm E1' \<inter> nrm E2'"

  1294                      "brk A' = (\<lambda>l. UNIV)"

  1295        using not_bool

  1296        by (elim da_elim_cases) (auto simp add: inj_term_simps)

  1297        (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)

  1298      note \<open>PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1\<close>

  1299      moreover note B' = \<open>B \<subseteq> B'\<close>

  1300      moreover note da_e1'

  1301      ultimately obtain E1': "nrm E1 \<subseteq> nrm E1'" "(\<forall>l. brk E1 l \<subseteq> brk E1' l)"

  1302        by blast

  1303      note \<open>PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle> E2\<close>

  1304      with B' da_e2'

  1305      obtain "nrm E2 \<subseteq> nrm E2'" "(\<forall>l. brk E2 l \<subseteq> brk E2' l)"

  1306        by blast

  1307     with E1' A A'

  1308     show ?case

  1309       by auto

  1310   next

  1311     case Call

  1312     from Call.prems and Call.hyps

  1313     show ?case by cases auto

  1314   next

  1315     case Methd thus ?case by (elim da_elim_cases) auto

  1316   next

  1317     case Body thus ?case by (elim da_elim_cases) auto

  1318   next

  1319     case LVar thus ?case by (elim da_elim_cases) auto

  1320   next

  1321     case FVar thus ?case by (elim da_elim_cases) auto

  1322   next

  1323     case AVar thus ?case by (elim da_elim_cases) auto

  1324   next

  1325     case Nil thus ?case by (elim da_elim_cases) auto

  1326   next

  1327     case Cons thus ?case by (elim da_elim_cases) auto

  1328   qed

  1329   from this [OF da' \<open>B \<subseteq> B'\<close>] show ?thesis .

  1330 qed

  1331

  1332 lemma da_weaken:

  1333   assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and "B \<subseteq> B'"

  1334   shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'"

  1335 proof -

  1336   note assigned.select_convs [Pure.intro]

  1337   from da

  1338   have "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")

  1339   proof (induct)

  1340     case Skip thus ?case by (iprover intro: da.Skip)

  1341   next

  1342     case Expr thus ?case by (iprover intro: da.Expr)

  1343   next

  1344     case (Lab Env B c C A l B')

  1345     note \<open>PROP ?Hyp Env B \<langle>c\<rangle>\<close>

  1346     moreover

  1347     note B' = \<open>B \<subseteq> B'\<close>

  1348     ultimately obtain C' where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"

  1349       by iprover

  1350     then obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A'"

  1351       by (iprover intro: da.Lab)

  1352     thus ?case ..

  1353   next

  1354     case (Comp Env B c1 C1 c2 C2 A B')

  1355     note da_c1 = \<open>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1\<close>

  1356     note \<open>PROP ?Hyp Env B \<langle>c1\<rangle>\<close>

  1357     moreover

  1358     note B' = \<open>B \<subseteq> B'\<close>

  1359     ultimately obtain C1' where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"

  1360       by iprover

  1361     with da_c1 B'

  1362     have

  1363       "nrm C1 \<subseteq> nrm C1'"

  1364       by (rule da_monotone [elim_format]) simp

  1365     moreover

  1366     note \<open>PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>\<close>

  1367     ultimately obtain C2' where "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"

  1368       by iprover

  1369     with da_c1' obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'"

  1370       by (iprover intro: da.Comp)

  1371     thus ?case ..

  1372   next

  1373     case (If Env B e E c1 C1 c2 C2 A B')

  1374     note B' = \<open>B \<subseteq> B'\<close>

  1375     obtain  E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"

  1376     proof -

  1377       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule If.hyps)

  1378       with B'

  1379       show ?thesis using that by iprover

  1380     qed

  1381     moreover

  1382     obtain C1' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"

  1383     proof -

  1384       from B'

  1385       have "(B \<union> assigns_if True e) \<subseteq> (B' \<union> assigns_if True e)"

  1386         by blast

  1387       moreover

  1388       have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle>" by (rule If.hyps)

  1389       ultimately

  1390       show ?thesis using that by iprover

  1391     qed

  1392     moreover

  1393     obtain C2' where "Env\<turnstile> (B' \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"

  1394     proof -

  1395       from B' have "(B \<union> assigns_if False e) \<subseteq> (B' \<union> assigns_if False e)"

  1396         by blast

  1397       moreover

  1398       have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle>" by (rule If.hyps)

  1399       ultimately

  1400       show ?thesis using that by iprover

  1401     qed

  1402     ultimately

  1403     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'"

  1404       by (iprover intro: da.If)

  1405     thus ?case ..

  1406   next

  1407     case (Loop Env B e E c C A l B')

  1408     note B' = \<open>B \<subseteq> B'\<close>

  1409     obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"

  1410     proof -

  1411       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Loop.hyps)

  1412       with B'

  1413       show ?thesis using that by iprover

  1414     qed

  1415     moreover

  1416     obtain C' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"

  1417     proof -

  1418       from B'

  1419       have "(B \<union> assigns_if True e) \<subseteq> (B' \<union> assigns_if True e)"

  1420         by blast

  1421       moreover

  1422       have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle>" by (rule Loop.hyps)

  1423       ultimately

  1424       show ?thesis using that by iprover

  1425     qed

  1426     ultimately

  1427     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'"

  1428       by (iprover intro: da.Loop )

  1429     thus ?case ..

  1430   next

  1431     case (Jmp jump B A Env B')

  1432     note B' = \<open>B \<subseteq> B'\<close>

  1433     with Jmp.hyps have "jump = Ret \<longrightarrow> Result \<in> B' "

  1434       by auto

  1435     moreover

  1436     obtain A'::assigned

  1437               where  "nrm A' = UNIV"

  1438                      "brk A' = (case jump of

  1439                                   Break l \<Rightarrow> \<lambda>k. if k = l then B' else UNIV

  1440                                 | Cont l \<Rightarrow> \<lambda>k. UNIV

  1441                                 | Ret \<Rightarrow> \<lambda>k. UNIV)"

  1442

  1443       by  iprover

  1444     ultimately have "Env\<turnstile> B' \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A'"

  1445       by (rule da.Jmp)

  1446     thus ?case ..

  1447   next

  1448     case Throw thus ?case by (iprover intro: da.Throw )

  1449   next

  1450     case (Try Env B c1 C1 vn C c2 C2 A B')

  1451     note B' = \<open>B \<subseteq> B'\<close>

  1452     obtain C1' where "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"

  1453     proof -

  1454       have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Try.hyps)

  1455       with B'

  1456       show ?thesis using that by iprover

  1457     qed

  1458     moreover

  1459     obtain C2' where

  1460       "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"

  1461     proof -

  1462       from B' have "B \<union> {VName vn} \<subseteq> B' \<union> {VName vn}" by blast

  1463       moreover

  1464       have "PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)

  1465                       (B \<union> {VName vn}) \<langle>c2\<rangle>"

  1466         by (rule Try.hyps)

  1467       ultimately

  1468       show ?thesis using that by iprover

  1469     qed

  1470     ultimately

  1471     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'"

  1472       by (iprover intro: da.Try )

  1473     thus ?case ..

  1474   next

  1475     case (Fin Env B c1 C1 c2 C2 A B')

  1476     note B' = \<open>B \<subseteq> B'\<close>

  1477     obtain C1' where C1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"

  1478     proof -

  1479       have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Fin.hyps)

  1480       with B'

  1481       show ?thesis using that by iprover

  1482     qed

  1483     moreover

  1484     obtain C2' where "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"

  1485     proof -

  1486       have "PROP ?Hyp Env B \<langle>c2\<rangle>" by (rule Fin.hyps)

  1487       with B'

  1488       show ?thesis using that by iprover

  1489     qed

  1490     ultimately

  1491     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'"

  1492       by (iprover intro: da.Fin )

  1493     thus ?case ..

  1494   next

  1495     case Init thus ?case by (iprover intro: da.Init)

  1496   next

  1497     case NewC thus ?case by (iprover intro: da.NewC)

  1498   next

  1499     case NewA thus ?case by (iprover intro: da.NewA)

  1500   next

  1501     case Cast thus ?case by (iprover intro: da.Cast)

  1502   next

  1503     case Inst thus ?case by (iprover intro: da.Inst)

  1504   next

  1505     case Lit thus ?case by (iprover intro: da.Lit)

  1506   next

  1507     case UnOp thus ?case by (iprover intro: da.UnOp)

  1508   next

  1509     case (CondAnd Env B e1 E1 e2 E2 A B')

  1510     note B' = \<open>B \<subseteq> B'\<close>

  1511     obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"

  1512     proof -

  1513       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondAnd.hyps)

  1514       with B'

  1515       show ?thesis using that by iprover

  1516     qed

  1517     moreover

  1518     obtain E2' where "Env\<turnstile> B' \<union>  assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"

  1519     proof -

  1520       from B' have "B \<union> assigns_if True e1 \<subseteq> B' \<union>  assigns_if True e1"

  1521         by blast

  1522       moreover

  1523       have "PROP ?Hyp Env (B \<union> assigns_if True e1) \<langle>e2\<rangle>" by (rule CondAnd.hyps)

  1524       ultimately show ?thesis using that by iprover

  1525     qed

  1526     ultimately

  1527     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'"

  1528       by (iprover intro: da.CondAnd)

  1529     thus ?case ..

  1530   next

  1531     case (CondOr Env B e1 E1 e2 E2 A B')

  1532     note B' = \<open>B \<subseteq> B'\<close>

  1533     obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"

  1534     proof -

  1535       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondOr.hyps)

  1536       with B'

  1537       show ?thesis using that by iprover

  1538     qed

  1539     moreover

  1540     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"

  1541     proof -

  1542       from B' have "B \<union> assigns_if False e1 \<subseteq> B' \<union>  assigns_if False e1"

  1543         by blast

  1544       moreover

  1545       have "PROP ?Hyp Env (B \<union> assigns_if False e1) \<langle>e2\<rangle>" by (rule CondOr.hyps)

  1546       ultimately show ?thesis using that by iprover

  1547     qed

  1548     ultimately

  1549     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A'"

  1550       by (iprover intro: da.CondOr)

  1551     thus ?case ..

  1552   next

  1553     case (BinOp Env B e1 E1 e2 A binop B')

  1554     note B' = \<open>B \<subseteq> B'\<close>

  1555     obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"

  1556     proof -

  1557       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule BinOp.hyps)

  1558       with B'

  1559       show ?thesis using that by iprover

  1560     qed

  1561     moreover

  1562     obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"

  1563     proof -

  1564       have "Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" by (rule BinOp.hyps)

  1565       from this B' E1'

  1566       have "nrm E1 \<subseteq> nrm E1'"

  1567         by (rule da_monotone [THEN conjE])

  1568       moreover

  1569       have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule BinOp.hyps)

  1570       ultimately show ?thesis using that by iprover

  1571     qed

  1572     ultimately

  1573     have "Env\<turnstile> B' \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A'"

  1574       using BinOp.hyps by (iprover intro: da.BinOp)

  1575     thus ?case ..

  1576   next

  1577     case (Super B Env B')

  1578     note B' = \<open>B \<subseteq> B'\<close>

  1579     with Super.hyps have "This \<in> B'"

  1580       by auto

  1581     thus ?case by (iprover intro: da.Super)

  1582   next

  1583     case (AccLVar vn B A Env B')

  1584     note \<open>vn \<in> B\<close>

  1585     moreover

  1586     note \<open>B \<subseteq> B'\<close>

  1587     ultimately have "vn \<in> B'" by auto

  1588     thus ?case by (iprover intro: da.AccLVar)

  1589   next

  1590     case Acc thus ?case by (iprover intro: da.Acc)

  1591   next

  1592     case (AssLVar Env B e E A vn B')

  1593     note B' = \<open>B \<subseteq> B'\<close>

  1594     then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"

  1595       by (rule AssLVar.hyps [elim_format]) iprover

  1596     then obtain A' where

  1597       "Env\<turnstile> B' \<guillemotright>\<langle>LVar vn:=e\<rangle>\<guillemotright> A'"

  1598       by (iprover intro: da.AssLVar)

  1599     thus ?case ..

  1600   next

  1601     case (Ass v Env B V e A B')

  1602     note B' = \<open>B \<subseteq> B'\<close>

  1603     note \<open>\<forall>vn. v \<noteq> LVar vn\<close>

  1604     moreover

  1605     obtain V' where V': "Env\<turnstile> B' \<guillemotright>\<langle>v\<rangle>\<guillemotright> V'"

  1606     proof -

  1607       have "PROP ?Hyp Env B \<langle>v\<rangle>" by (rule Ass.hyps)

  1608       with B'

  1609       show ?thesis using that by iprover

  1610     qed

  1611     moreover

  1612     obtain A' where "Env\<turnstile> nrm V' \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"

  1613     proof -

  1614       have "Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V" by (rule Ass.hyps)

  1615       from this B' V'

  1616       have "nrm V \<subseteq> nrm V'"

  1617         by (rule da_monotone [THEN conjE])

  1618       moreover

  1619       have "PROP ?Hyp Env (nrm V) \<langle>e\<rangle>" by (rule Ass.hyps)

  1620       ultimately show ?thesis using that by iprover

  1621     qed

  1622     ultimately

  1623     have "Env\<turnstile> B' \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A'"

  1624       by (iprover intro: da.Ass)

  1625     thus ?case ..

  1626   next

  1627     case (CondBool Env c e1 e2 B C E1 E2 A B')

  1628     note B' = \<open>B \<subseteq> B'\<close>

  1629     note \<open>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)\<close>

  1630     moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"

  1631     proof -

  1632       have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule CondBool.hyps)

  1633       with B'

  1634       show ?thesis using that by iprover

  1635     qed

  1636     moreover

  1637     obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"

  1638     proof -

  1639       from B'

  1640       have "(B \<union> assigns_if True c) \<subseteq> (B' \<union> assigns_if True c)"

  1641         by blast

  1642       moreover

  1643       have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule CondBool.hyps)

  1644       ultimately

  1645       show ?thesis using that by iprover

  1646     qed

  1647     moreover

  1648     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"

  1649     proof -

  1650       from B'

  1651       have "(B \<union> assigns_if False c) \<subseteq> (B' \<union> assigns_if False c)"

  1652         by blast

  1653       moreover

  1654       have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by(rule CondBool.hyps)

  1655       ultimately

  1656       show ?thesis using that by iprover

  1657     qed

  1658     ultimately

  1659     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"

  1660       by (iprover intro: da.CondBool)

  1661     thus ?case ..

  1662   next

  1663     case (Cond Env c e1 e2 B C E1 E2 A B')

  1664     note B' = \<open>B \<subseteq> B'\<close>

  1665     note \<open>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)\<close>

  1666     moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"

  1667     proof -

  1668       have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule Cond.hyps)

  1669       with B'

  1670       show ?thesis using that by iprover

  1671     qed

  1672     moreover

  1673     obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"

  1674     proof -

  1675       from B'

  1676       have "(B \<union> assigns_if True c) \<subseteq> (B' \<union> assigns_if True c)"

  1677         by blast

  1678       moreover

  1679       have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule Cond.hyps)

  1680       ultimately

  1681       show ?thesis using that by iprover

  1682     qed

  1683     moreover

  1684     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"

  1685     proof -

  1686       from B'

  1687       have "(B \<union> assigns_if False c) \<subseteq> (B' \<union> assigns_if False c)"

  1688         by blast

  1689       moreover

  1690       have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by (rule Cond.hyps)

  1691       ultimately

  1692       show ?thesis using that by iprover

  1693     qed

  1694     ultimately

  1695     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"

  1696       by (iprover intro: da.Cond)

  1697     thus ?case ..

  1698   next

  1699     case (Call Env B e E args A accC statT mode mn pTs B')

  1700     note B' = \<open>B \<subseteq> B'\<close>

  1701     obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"

  1702     proof -

  1703       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Call.hyps)

  1704       with B'

  1705       show ?thesis using that by iprover

  1706     qed

  1707     moreover

  1708     obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'"

  1709     proof -

  1710       have "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" by (rule Call.hyps)

  1711       from this B' E'

  1712       have "nrm E \<subseteq> nrm E'"

  1713         by (rule da_monotone [THEN conjE])

  1714       moreover

  1715       have "PROP ?Hyp Env (nrm E) \<langle>args\<rangle>" by (rule Call.hyps)

  1716       ultimately show ?thesis using that by iprover

  1717     qed

  1718     ultimately

  1719     have "Env\<turnstile> B' \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs}args)\<rangle>\<guillemotright> A'"

  1720       by (iprover intro: da.Call)

  1721     thus ?case ..

  1722   next

  1723     case Methd thus ?case by (iprover intro: da.Methd)

  1724   next

  1725     case (Body Env B c C A D B')

  1726     note B' = \<open>B \<subseteq> B'\<close>

  1727     obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and nrm_C': "nrm C \<subseteq> nrm C'"

  1728     proof -

  1729       have "Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" by (rule Body.hyps)

  1730       moreover note B'

  1731       moreover

  1732       from B' obtain C' where da_c: "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"

  1733         by (rule Body.hyps [elim_format]) blast

  1734       ultimately

  1735       have "nrm C \<subseteq> nrm C'"

  1736         by (rule da_monotone [THEN conjE])

  1737       with da_c that show ?thesis by iprover

  1738     qed

  1739     moreover

  1740     note \<open>Result \<in> nrm C\<close>

  1741     with nrm_C' have "Result \<in> nrm C'"

  1742       by blast

  1743     moreover note \<open>jumpNestingOkS {Ret} c\<close>

  1744     ultimately obtain A' where

  1745       "Env\<turnstile> B' \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A'"

  1746       by (iprover intro: da.Body)

  1747     thus ?case ..

  1748   next

  1749     case LVar thus ?case by (iprover intro: da.LVar)

  1750   next

  1751     case FVar thus ?case by (iprover intro: da.FVar)

  1752   next

  1753     case (AVar Env B e1 E1 e2 A B')

  1754     note B' = \<open>B \<subseteq> B'\<close>

  1755     obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"

  1756     proof -

  1757       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule AVar.hyps)

  1758       with B'

  1759       show ?thesis using that by iprover

  1760     qed

  1761     moreover

  1762     obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"

  1763     proof -

  1764       have "Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" by (rule AVar.hyps)

  1765       from this B' E1'

  1766       have "nrm E1 \<subseteq> nrm E1'"

  1767         by (rule da_monotone [THEN conjE])

  1768       moreover

  1769       have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule AVar.hyps)

  1770       ultimately show ?thesis using that by iprover

  1771     qed

  1772     ultimately

  1773     have "Env\<turnstile> B' \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A'"

  1774       by (iprover intro: da.AVar)

  1775     thus ?case ..

  1776   next

  1777     case Nil thus ?case by (iprover intro: da.Nil)

  1778   next

  1779     case (Cons Env B e E es A B')

  1780     note B' = \<open>B \<subseteq> B'\<close>

  1781     obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"

  1782     proof -

  1783       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Cons.hyps)

  1784       with B'

  1785       show ?thesis using that by iprover

  1786     qed

  1787     moreover

  1788     obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'"

  1789     proof -

  1790       have "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" by (rule Cons.hyps)

  1791       from this B' E'

  1792       have "nrm E \<subseteq> nrm E'"

  1793         by (rule da_monotone [THEN conjE])

  1794       moreover

  1795       have "PROP ?Hyp Env (nrm E) \<langle>es\<rangle>" by (rule Cons.hyps)

  1796       ultimately show ?thesis using that by iprover

  1797     qed

  1798     ultimately

  1799     have "Env\<turnstile> B' \<guillemotright>\<langle>e # es\<rangle>\<guillemotright> A'"

  1800       by (iprover intro: da.Cons)

  1801     thus ?case ..

  1802   qed

  1803   from this [OF \<open>B \<subseteq> B'\<close>] show ?thesis .

  1804 qed

  1805

  1806 (* Remarks about the proof style:

  1807

  1808    "by (rule <Case>.hyps)" vs "."

  1809    --------------------------

  1810

  1811    with <Case>.hyps you state more precise were the rule comes from

  1812

  1813    . takes all assumptions into account, but looks more "light"

  1814    and is more resistent for cut and paste proof in different

  1815    cases.

  1816

  1817   "intro: da.intros" vs "da.<Case>"

  1818   ---------------------------------

  1819   The first ist more convinient for cut and paste between cases,

  1820   the second is more informativ for the reader

  1821 *)

  1822

  1823 corollary da_weakenE [consumes 2]:

  1824   assumes          da: "Env\<turnstile> B  \<guillemotright>t\<guillemotright> A"   and

  1825                    B': "B \<subseteq> B'"          and

  1826               ex_mono: "\<And> A'.  \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; nrm A \<subseteq> nrm A';

  1827                                \<And> l. brk A l \<subseteq> brk A' l\<rbrakk> \<Longrightarrow> P"

  1828   shows "P"

  1829 proof -

  1830   from da B'

  1831   obtain A' where A': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'"

  1832     by (rule da_weaken [elim_format]) iprover

  1833   with da B'

  1834   have "nrm A \<subseteq> nrm A' \<and> (\<forall> l. brk A l \<subseteq> brk A' l)"

  1835     by (rule da_monotone)

  1836   with A' ex_mono

  1837   show ?thesis

  1838     by iprover

  1839 qed

  1840

  1841 end