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