schirmer@13688: header {* Definite Assignment *}
schirmer@13688: 
haftmann@16417: theory DefiniteAssignment imports WellType begin 
schirmer@13688: 
schirmer@13688: text {* Definite Assignment Analysis (cf. 16)
schirmer@13688: 
schirmer@13688: The definite assignment analysis approximates the sets of local 
schirmer@13688: variables that will be assigned at a certain point of evaluation, and ensures
schirmer@13688: that we will only read variables which previously were assigned.
schirmer@13688: It should conform to the following idea:
schirmer@13688:  If the evaluation of a term completes normally (no abruption (exception, 
schirmer@13688: break, continue, return) appeared) , the set of local variables calculated 
schirmer@13688: by the analysis is a subset of the
schirmer@13688: variables that were actually assigned during evaluation.
schirmer@13688: 
schirmer@13688: To get more precise information about the sets of assigned variables the 
schirmer@13688: analysis includes the following optimisations:
schirmer@13688: \begin{itemize}
schirmer@13688:   \item Inside of a while loop we also take care of the variables assigned
schirmer@13688:         before break statements, since the break causes the while loop to
schirmer@13688:         continue normally.
schirmer@13688:   \item For conditional statements we take care of constant conditions to 
schirmer@13688:         statically determine the path of evaluation.
schirmer@13688:   \item Inside a distinct path of a conditional statements we know to which
schirmer@13688:         boolean value the condition has evaluated to, and so can retrieve more
schirmer@13688:         information about the variables assigned during evaluation of the
schirmer@13688:         boolean condition.
schirmer@13688: \end{itemize}
schirmer@13688: 
schirmer@13688: Since in our model of Java the return values of methods are stored in a local
schirmer@13688: variable we also ensure that every path of (normal) evaluation will assign the
schirmer@13688: result variable, or in the sense of real Java every path ends up in and 
schirmer@13688: return instruction. 
schirmer@13688: 
schirmer@13688: Not covered yet:
schirmer@13688: \begin{itemize} 
schirmer@13688:   \item analysis of definite unassigned
schirmer@13688:   \item special treatment of final fields
schirmer@13688: \end{itemize}
schirmer@13688: *}
schirmer@13688: 
schirmer@13688: section {* Correct nesting of jump statements *}
schirmer@13688: 
schirmer@13688: text {* For definite assignment it becomes crucial, that jumps (break, 
schirmer@13688: continue, return) are nested correctly i.e. a continue jump is nested in a
schirmer@13688: matching while statement, a break jump is nested in a proper label statement,
schirmer@13688: a class initialiser does not terminate abruptly with a return. With this we 
schirmer@13688: can for example ensure that evaluation of an expression will never end up 
schirmer@13688: with a jump, since no breaks, continues or returns are allowed in an 
schirmer@13688: expression. *}
schirmer@13688: 
schirmer@13688: consts jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
schirmer@13688: primrec
schirmer@13688: "jumpNestingOkS jmps (Skip)   = True"
schirmer@13688: "jumpNestingOkS jmps (Expr e) = True"
schirmer@13688: "jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
schirmer@13688: "jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> 
schirmer@13688:                                  jumpNestingOkS jmps c2)"
schirmer@13688: "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>  
schirmer@13688:                                            jumpNestingOkS jmps c2)"
schirmer@13688: "jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
schirmer@13688: --{* The label of the while loop only handles continue jumps. Breaks are only
schirmer@13688:      handled by @{term Lab} *}
schirmer@13688: "jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
schirmer@13688: "jumpNestingOkS jmps (Throw e) = True"
schirmer@13688: "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> 
schirmer@13688:                                                 jumpNestingOkS jmps c2)"
schirmer@13688: "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> 
schirmer@13688:                                         jumpNestingOkS jmps c2)"
schirmer@13688: "jumpNestingOkS jmps (Init C) = True" 
schirmer@13688:  --{* wellformedness of the program must enshure that for all initializers 
schirmer@13688:       jumpNestingOkS {} holds *} 
schirmer@13688: --{* Dummy analysis for intermediate smallstep term @{term  FinA} *}
schirmer@13688: "jumpNestingOkS jmps (FinA a c) = False"
schirmer@13688: 
schirmer@13688: 
schirmer@13688: constdefs jumpNestingOk :: "jump set \<Rightarrow> term \<Rightarrow> bool"
schirmer@13688: "jumpNestingOk jmps t \<equiv> (case t of
schirmer@13688:                       In1 se \<Rightarrow> (case se of
schirmer@13688:                                    Inl e \<Rightarrow> True
schirmer@13688:                                  | Inr s \<Rightarrow> jumpNestingOkS jmps s)
schirmer@13688:                     | In2  v \<Rightarrow> True
schirmer@13688:                     | In3  es \<Rightarrow> True)"
schirmer@13688: 
schirmer@13688: lemma jumpNestingOk_expr_simp [simp]: "jumpNestingOk jmps (In1l e) = True"
schirmer@13688: by (simp add: jumpNestingOk_def)
schirmer@13688: 
schirmer@13688: lemma jumpNestingOk_expr_simp1 [simp]: "jumpNestingOk jmps \<langle>e::expr\<rangle> = True"
schirmer@13688: by (simp add: inj_term_simps)
schirmer@13688: 
schirmer@13688: lemma jumpNestingOk_stmt_simp [simp]: 
schirmer@13688:   "jumpNestingOk jmps (In1r s) = jumpNestingOkS jmps s"
schirmer@13688: by (simp add: jumpNestingOk_def)
schirmer@13688: 
schirmer@13688: lemma jumpNestingOk_stmt_simp1 [simp]: 
schirmer@13688:    "jumpNestingOk jmps \<langle>s::stmt\<rangle> = jumpNestingOkS jmps s"
schirmer@13688: by (simp add: inj_term_simps)
schirmer@13688: 
schirmer@13688: lemma jumpNestingOk_var_simp [simp]: "jumpNestingOk jmps (In2 v) = True"
schirmer@13688: by (simp add: jumpNestingOk_def)
schirmer@13688: 
schirmer@13688: lemma jumpNestingOk_var_simp1 [simp]: "jumpNestingOk jmps \<langle>v::var\<rangle> = True"
schirmer@13688: by (simp add: inj_term_simps)
schirmer@13688: 
schirmer@13688: lemma jumpNestingOk_expr_list_simp [simp]: "jumpNestingOk jmps (In3 es) = True"
schirmer@13688: by (simp add: jumpNestingOk_def)
schirmer@13688: 
schirmer@13688: lemma jumpNestingOk_expr_list_simp1 [simp]: 
schirmer@13688:   "jumpNestingOk jmps \<langle>es::expr list\<rangle> = True"
schirmer@13688: by (simp add: inj_term_simps)
schirmer@13688: 
schirmer@13688: 
schirmer@13688: 
schirmer@13688: section {* Calculation of assigned variables for boolean expressions*}
schirmer@13688: 
schirmer@13688: 
schirmer@13688: subsection {* Very restricted calculation fallback calculation *}
schirmer@13688: 
schirmer@13688: consts the_LVar_name:: "var \<Rightarrow> lname"
schirmer@13688: primrec 
schirmer@13688: "the_LVar_name (LVar n) = n"
schirmer@13688: 
schirmer@13688: consts assignsE :: "expr      \<Rightarrow> lname set" 
schirmer@13688:        assignsV :: "var       \<Rightarrow> lname set"
schirmer@13688:        assignsEs:: "expr list \<Rightarrow> lname set"
schirmer@13688: text {* *}
schirmer@13688: primrec
schirmer@13688: "assignsE (NewC c)            = {}" 
schirmer@13688: "assignsE (NewA t e)          = assignsE e"
schirmer@13688: "assignsE (Cast t e)          = assignsE e"
schirmer@13688: "assignsE (e InstOf r)        = assignsE e"
schirmer@13688: "assignsE (Lit val)           = {}"
schirmer@13688: "assignsE (UnOp unop e)       = assignsE e"
schirmer@13688: "assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
schirmer@13688:                                      then (assignsE e1)
schirmer@13688:                                      else (assignsE e1) \<union> (assignsE e2))" 
schirmer@13688: "assignsE (Super)             = {}"
schirmer@13688: "assignsE (Acc v)             = assignsV v"
schirmer@13688: "assignsE (v:=e)              = (assignsV v) \<union> (assignsE e) \<union> 
schirmer@13688:                                  (if \<exists> n. v=(LVar n) then {the_LVar_name v} 
schirmer@13688:                                                      else {})"
schirmer@13688: "assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
schirmer@13688: "assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) 
schirmer@13688:                           = (assignsE objRef) \<union> (assignsEs args)"
schirmer@13688: -- {* Only dummy analysis for intermediate expressions  
schirmer@13688:       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
schirmer@13688: "assignsE (Methd C sig)   = {}" 
schirmer@13688: "assignsE (Body  C s)     = {}"   
schirmer@13688: "assignsE (InsInitE s e)  = {}"  
schirmer@13688: "assignsE (Callee l e)    = {}" 
schirmer@13688: 
schirmer@13688: "assignsV (LVar n)       = {}"
schirmer@13688: "assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
schirmer@13688: "assignsV (e1.[e2])      = assignsE e1 \<union> assignsE e2"
schirmer@13688: 
schirmer@13688: "assignsEs     [] = {}"
schirmer@13688: "assignsEs (e#es) = assignsE e \<union> assignsEs es"
schirmer@13688: 
schirmer@13688: constdefs assigns:: "term \<Rightarrow> lname set"
schirmer@13688: "assigns t \<equiv> (case t of
schirmer@13688:                 In1 se \<Rightarrow> (case se of
schirmer@13688:                              Inl e \<Rightarrow> assignsE e
schirmer@13688:                            | Inr s \<Rightarrow> {})
schirmer@13688:               | In2  v \<Rightarrow> assignsV v
schirmer@13688:               | In3  es \<Rightarrow> assignsEs es)"
schirmer@13688: 
schirmer@13688: lemma assigns_expr_simp [simp]: "assigns (In1l e) = assignsE e"
schirmer@13688: by (simp add: assigns_def)
schirmer@13688: 
schirmer@13688: lemma assigns_expr_simp1 [simp]: "assigns (\<langle>e\<rangle>) = assignsE e"
schirmer@13688: by (simp add: inj_term_simps)
schirmer@13688: 
schirmer@13688: lemma assigns_stmt_simp [simp]: "assigns (In1r s) = {}"
schirmer@13688: by (simp add: assigns_def)
schirmer@13688: 
schirmer@13688: lemma assigns_stmt_simp1 [simp]: "assigns (\<langle>s::stmt\<rangle>) = {}"
schirmer@13688: by (simp add: inj_term_simps)
schirmer@13688: 
schirmer@13688: lemma assigns_var_simp [simp]: "assigns (In2 v) = assignsV v"
schirmer@13688: by (simp add: assigns_def)
schirmer@13688: 
schirmer@13688: lemma assigns_var_simp1 [simp]: "assigns (\<langle>v\<rangle>) = assignsV v"
schirmer@13688: by (simp add: inj_term_simps)
schirmer@13688: 
schirmer@13688: lemma assigns_expr_list_simp [simp]: "assigns (In3 es) = assignsEs es"
schirmer@13688: by (simp add: assigns_def)
schirmer@13688: 
schirmer@13688: lemma assigns_expr_list_simp1 [simp]: "assigns (\<langle>es\<rangle>) = assignsEs es"
schirmer@13688: by (simp add: inj_term_simps)
schirmer@13688: 
schirmer@13688: subsection "Analysis of constant expressions"
schirmer@13688: 
schirmer@13688: consts constVal :: "expr \<Rightarrow> val option"
schirmer@13688: primrec 
schirmer@13688: "constVal (NewC c)      = None"
schirmer@13688: "constVal (NewA t e)    = None"
schirmer@13688: "constVal (Cast t e)    = None"
schirmer@13688: "constVal (Inst e r)    = None"
schirmer@13688: "constVal (Lit val)     = Some val"
schirmer@13688: "constVal (UnOp unop e) = (case (constVal e) of
schirmer@13688:                              None   \<Rightarrow> None
schirmer@13688:                            | Some v \<Rightarrow> Some (eval_unop unop v))" 
schirmer@13688: "constVal (BinOp binop e1 e2) = (case (constVal e1) of
schirmer@13688:                                    None    \<Rightarrow> None
schirmer@13688:                                  | Some v1 \<Rightarrow> (case (constVal e2) of 
schirmer@13688:                                                 None    \<Rightarrow> None
schirmer@13688:                                               | Some v2 \<Rightarrow> Some (eval_binop 
schirmer@13688:                                                                  binop v1 v2)))"
schirmer@13688: "constVal (Super)         = None"
schirmer@13688: "constVal (Acc v)         = None"
schirmer@13688: "constVal (Ass v e)       = None"
schirmer@13688: "constVal (Cond b e1 e2)  = (case (constVal b) of
schirmer@13688:                                None   \<Rightarrow> None
schirmer@13688:                              | Some bv\<Rightarrow> (case the_Bool bv of
schirmer@13688:                                             True \<Rightarrow> (case (constVal e2) of
schirmer@13688:                                                        None   \<Rightarrow> None
schirmer@13688:                                                      | Some v \<Rightarrow> constVal e1)
schirmer@13688:                                           | False\<Rightarrow> (case (constVal e1) of
schirmer@13688:                                                        None   \<Rightarrow> None
schirmer@13688:                                                      | Some v \<Rightarrow> constVal e2)))"
schirmer@13688: --{* Note that @{text "constVal (Cond b e1 e2)"} is stricter as it could be.
schirmer@13688:      It requires that all tree expressions are constant even if we can decide
schirmer@13688:      which branch to choose, provided the constant value of @{term b} *}
schirmer@13688: "constVal (Call accC statT mode objRef mn pTs args) = None"
schirmer@13688: "constVal (Methd C sig)   = None" 
schirmer@13688: "constVal (Body  C s)     = None"   
schirmer@13688: "constVal (InsInitE s e)  = None"  
schirmer@13688: "constVal (Callee l e)    = None" 
schirmer@13688: 
schirmer@13688: lemma constVal_Some_induct [consumes 1, case_names Lit UnOp BinOp CondL CondR]: 
schirmer@13688:   assumes const: "constVal e = Some v" and
schirmer@13688:         hyp_Lit: "\<And> v. P (Lit v)" and
schirmer@13688:        hyp_UnOp: "\<And> unop e'. P e' \<Longrightarrow> P (UnOp unop e')" and
schirmer@13688:       hyp_BinOp: "\<And> binop e1 e2. \<lbrakk>P e1; P e2\<rbrakk> \<Longrightarrow> P (BinOp binop e1 e2)" and
schirmer@13688:       hyp_CondL: "\<And> b bv e1 e2. \<lbrakk>constVal b = Some bv; the_Bool bv; P b; P e1\<rbrakk> 
schirmer@13688:                               \<Longrightarrow> P (b? e1 : e2)" and
schirmer@13688:       hyp_CondR: "\<And> b bv e1 e2. \<lbrakk>constVal b = Some bv; \<not>the_Bool bv; P b; P e2\<rbrakk>
schirmer@13688:                               \<Longrightarrow> P (b? e1 : e2)"
schirmer@13688:   shows "P e"
schirmer@13688: proof -
schirmer@13688:   have "True" and "\<And> v. constVal e = Some v \<Longrightarrow> P e" and "True" and "True"
schirmer@13688:   proof (induct "x::var" and e and "s::stmt" and "es::expr list")
schirmer@13688:     case Lit
schirmer@13688:     show ?case by (rule hyp_Lit)
schirmer@13688:   next
schirmer@13688:     case UnOp
schirmer@13688:     thus ?case
schirmer@13688:       by (auto intro: hyp_UnOp)
schirmer@13688:   next
schirmer@13688:     case BinOp
schirmer@13688:     thus ?case
schirmer@13688:       by (auto intro: hyp_BinOp)
schirmer@13688:   next
schirmer@13688:     case (Cond b e1 e2)
schirmer@13688:     then obtain v where   v: "constVal (b ? e1 : e2) = Some v"
schirmer@13688:       by blast
schirmer@13688:     then obtain bv where bv: "constVal b = Some bv"
schirmer@13688:       by simp
schirmer@13688:     show ?case
schirmer@13688:     proof (cases "the_Bool bv")
schirmer@13688:       case True
schirmer@13688:       with Cond show ?thesis using v bv
schirmer@13688: 	by (auto intro: hyp_CondL)
schirmer@13688:     next
schirmer@13688:       case False
schirmer@13688:       with Cond show ?thesis using v bv
schirmer@13688: 	by (auto intro: hyp_CondR)
schirmer@13688:     qed
schirmer@13688:   qed (simp_all)
schirmer@13688:   with const 
schirmer@13688:   show ?thesis
schirmer@13688:     by blast  
schirmer@13688: qed
schirmer@13688: 
schirmer@13688: lemma assignsE_const_simp: "constVal e = Some v \<Longrightarrow> assignsE e = {}"
schirmer@13688:   by (induct rule: constVal_Some_induct) simp_all
schirmer@13688: 
schirmer@13688: 
schirmer@13688: subsection {* Main analysis for boolean expressions *}
schirmer@13688: 
schirmer@13688: text {* Assigned local variables after evaluating the expression if it evaluates
schirmer@13688: to a specific boolean value. If the expression cannot evaluate to a 
schirmer@13688: @{term Boolean} value UNIV is returned. If we expect true/false the opposite 
schirmer@13688: constant false/true will also lead to UNIV. *}
schirmer@13688: consts assigns_if:: "bool \<Rightarrow> expr \<Rightarrow> lname set" 
schirmer@13688: primrec
schirmer@13688: "assigns_if b (NewC c)            = UNIV" --{*can never evaluate to Boolean*} 
schirmer@13688: "assigns_if b (NewA t e)          = UNIV" --{*can never evaluate to Boolean*}
schirmer@13688: "assigns_if b (Cast t e)          = assigns_if b e" 
schirmer@13688: "assigns_if b (Inst e r)          = assignsE e" --{*Inst has type Boolean but
schirmer@13688:                                                      e is a reference type*}
schirmer@13688: "assigns_if b (Lit val)           = (if val=Bool b then {} else UNIV)"  
schirmer@13688: "assigns_if b (UnOp unop e)       = (case constVal (UnOp unop e) of
schirmer@13688:                                          None   \<Rightarrow> (if unop = UNot 
schirmer@13688:                                                        then assigns_if (\<not>b) e
schirmer@13688:                                                        else UNIV)
schirmer@13688:                                        | Some v \<Rightarrow> (if v=Bool b 
schirmer@13688:                                                        then {} 
schirmer@13688:                                                        else UNIV))"
schirmer@13688: "assigns_if b (BinOp binop e1 e2) 
schirmer@13688:   = (case constVal (BinOp binop e1 e2) of
schirmer@13688:        None \<Rightarrow> (if binop=CondAnd then
schirmer@13688:                    (case b of 
schirmer@13688:                        True  \<Rightarrow> assigns_if True  e1 \<union> assigns_if True e2
schirmer@13688:                     |  False \<Rightarrow> assigns_if False e1 \<inter> 
schirmer@13688:                                 (assigns_if True e1 \<union> assigns_if False e2))
schirmer@13688:                 else
schirmer@13688:                (if binop=CondOr then
schirmer@13688:                    (case b of 
schirmer@13688:                        True  \<Rightarrow> assigns_if True e1 \<inter> 
schirmer@13688:                                 (assigns_if False e1 \<union> assigns_if True e2)
schirmer@13688:                     |  False \<Rightarrow> assigns_if False  e1 \<union> assigns_if False e2)
schirmer@13688:                 else assignsE e1 \<union> assignsE e2))
schirmer@13688:      | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
schirmer@13688: 
schirmer@13688: "assigns_if b (Super)      = UNIV" --{*can never evaluate to Boolean*}
schirmer@13688: "assigns_if b (Acc v)      = (assignsV v)"
schirmer@13688: "assigns_if b (v := e)     = (assignsE (Ass v e))"
schirmer@13688: "assigns_if b (c? e1 : e2) = (assignsE c) \<union>
schirmer@13688:                                (case (constVal c) of
schirmer@13688:                                   None    \<Rightarrow> (assigns_if b e1) \<inter> 
schirmer@13688:                                              (assigns_if b e2)
schirmer@13688:                                 | Some bv \<Rightarrow> (case the_Bool bv of
schirmer@13688:                                                 True  \<Rightarrow> assigns_if b e1
schirmer@13688:                                               | False \<Rightarrow> assigns_if b e2))"
schirmer@13688: "assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))  
schirmer@13688:           = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
schirmer@13688: -- {* Only dummy analysis for intermediate expressions  
schirmer@13688:       @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
schirmer@13688: "assigns_if b (Methd C sig)   = {}" 
schirmer@13688: "assigns_if b (Body  C s)     = {}"   
schirmer@13688: "assigns_if b (InsInitE s e)  = {}"  
schirmer@13688: "assigns_if b (Callee l e)    = {}" 
schirmer@13688: 
schirmer@13688: lemma assigns_if_const_b_simp:
schirmer@13688:   assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")
schirmer@13688:   shows   "assigns_if b e = {}" (is "?Ass b e")
schirmer@13688: proof -
schirmer@13688:   have "True" and "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e" and "True" and "True"
wenzelm@18459:   proof (induct _ and e and _ and _ rule: var_expr_stmt.inducts)
schirmer@13688:     case Lit
schirmer@13688:     thus ?case by simp
schirmer@13688:   next
schirmer@13688:     case UnOp 
schirmer@13688:     thus ?case by simp
schirmer@13688:   next 
schirmer@13688:     case (BinOp binop)
schirmer@13688:     thus ?case
schirmer@13688:       by (cases binop) (simp_all)
schirmer@13688:   next
schirmer@13688:     case (Cond c e1 e2 b)
wenzelm@23350:     note hyp_c = `\<And> b. ?Const b c \<Longrightarrow> ?Ass b c`
wenzelm@23350:     note hyp_e1 = `\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1`
wenzelm@23350:     note hyp_e2 = `\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2`
wenzelm@23350:     note const = `constVal (c ? e1 : e2) = Some (Bool b)`
schirmer@13688:     then obtain bv where bv: "constVal c = Some bv"
schirmer@13688:       by simp
schirmer@13688:     hence emptyC: "assignsE c = {}" by (rule assignsE_const_simp)
schirmer@13688:     show ?case
schirmer@13688:     proof (cases "the_Bool bv")
schirmer@13688:       case True
schirmer@13688:       with const bv  
schirmer@13688:       have "?Const b e1" by simp
schirmer@13688:       hence "?Ass b e1" by (rule hyp_e1)
schirmer@13688:       with emptyC bv True
schirmer@13688:       show ?thesis
schirmer@13688: 	by simp
schirmer@13688:     next
schirmer@13688:       case False
schirmer@13688:       with const bv  
schirmer@13688:       have "?Const b e2" by simp
schirmer@13688:       hence "?Ass b e2" by (rule hyp_e2)
schirmer@13688:       with emptyC bv False
schirmer@13688:       show ?thesis
schirmer@13688: 	by simp
schirmer@13688:     qed
schirmer@13688:   qed (simp_all)
schirmer@13688:   with boolConst
schirmer@13688:   show ?thesis
schirmer@13688:     by blast
schirmer@13688: qed
schirmer@13688: 
schirmer@13688: lemma assigns_if_const_not_b_simp:
schirmer@13688:   assumes boolConst: "constVal e = Some (Bool b)"        (is "?Const b e")  
wenzelm@18459:   shows "assigns_if (\<not>b) e = UNIV"                  (is "?Ass b e")
schirmer@13688: proof -
schirmer@13688:   have True and "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e" and True and True
wenzelm@18459:   proof (induct _ and e and _ and _ rule: var_expr_stmt.inducts) 
schirmer@13688:     case Lit
schirmer@13688:     thus ?case by simp
schirmer@13688:   next
schirmer@13688:     case UnOp 
schirmer@13688:     thus ?case by simp
schirmer@13688:   next 
schirmer@13688:     case (BinOp binop)
schirmer@13688:     thus ?case
schirmer@13688:       by (cases binop) (simp_all)
schirmer@13688:   next
schirmer@13688:     case (Cond c e1 e2 b)
wenzelm@23350:     note hyp_c = `\<And> b. ?Const b c \<Longrightarrow> ?Ass b c`
wenzelm@23350:     note hyp_e1 = `\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1`
wenzelm@23350:     note hyp_e2 = `\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2`
wenzelm@23350:     note const = `constVal (c ? e1 : e2) = Some (Bool b)`
schirmer@13688:     then obtain bv where bv: "constVal c = Some bv"
schirmer@13688:       by simp
schirmer@13688:     show ?case
schirmer@13688:     proof (cases "the_Bool bv")
schirmer@13688:       case True
schirmer@13688:       with const bv  
schirmer@13688:       have "?Const b e1" by simp
schirmer@13688:       hence "?Ass b e1" by (rule hyp_e1)
schirmer@13688:       with bv True
schirmer@13688:       show ?thesis
schirmer@13688: 	by simp
schirmer@13688:     next
schirmer@13688:       case False
schirmer@13688:       with const bv  
schirmer@13688:       have "?Const b e2" by simp
schirmer@13688:       hence "?Ass b e2" by (rule hyp_e2)
schirmer@13688:       with bv False 
schirmer@13688:       show ?thesis
schirmer@13688: 	by simp
schirmer@13688:     qed
schirmer@13688:   qed (simp_all)
schirmer@13688:   with boolConst
schirmer@13688:   show ?thesis
schirmer@13688:     by blast
schirmer@13688: qed
schirmer@13688: 
schirmer@13688: subsection {* Lifting set operations to range of tables (map to a set) *}
schirmer@13688: 
schirmer@13688: constdefs 
schirmer@13688:  union_ts:: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
schirmer@13688:                     ("_ \<Rightarrow>\<union> _" [67,67] 65)
schirmer@13688:  "A \<Rightarrow>\<union> B \<equiv> \<lambda> k. A k \<union> B k"
schirmer@13688: 
schirmer@13688: constdefs
schirmer@13688:  intersect_ts:: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
schirmer@13688:                     ("_ \<Rightarrow>\<inter>  _" [72,72] 71)
schirmer@13688:  "A \<Rightarrow>\<inter>  B \<equiv> \<lambda> k. A k \<inter> B k"
schirmer@13688: 
schirmer@13688: constdefs
schirmer@13688:  all_union_ts:: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" 
schirmer@13688:                                                      (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40)
schirmer@13688: "A \<Rightarrow>\<union>\<^sub>\<forall> B \<equiv> \<lambda> k. A k \<union> B"
schirmer@13688:   
schirmer@13688: subsubsection {* Binary union of tables *}
schirmer@13688: 
schirmer@13688: lemma union_ts_iff [simp]: "(c \<in> (A \<Rightarrow>\<union> B) k) = (c \<in> A k \<or>  c \<in> B k)"
schirmer@13688:   by (unfold union_ts_def) blast
schirmer@13688: 
schirmer@13688: lemma union_tsI1 [elim?]: "c \<in> A k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k"
schirmer@13688:   by simp
schirmer@13688: 
schirmer@13688: lemma union_tsI2 [elim?]: "c \<in> B k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k"
schirmer@13688:   by simp
schirmer@13688: 
schirmer@13688: lemma union_tsCI [intro!]: "(c \<notin> B k \<Longrightarrow> c \<in> A k) \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k"
schirmer@13688:   by auto
schirmer@13688: 
schirmer@13688: lemma union_tsE [elim!]: 
schirmer@13688:  "\<lbrakk>c \<in> (A \<Rightarrow>\<union> B) k; (c \<in> A k \<Longrightarrow> P); (c \<in> B k \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
schirmer@13688:   by (unfold union_ts_def) blast
schirmer@13688: 
schirmer@13688: subsubsection {* Binary intersection of tables *}
schirmer@13688: 
schirmer@13688: lemma intersect_ts_iff [simp]: "c \<in> (A \<Rightarrow>\<inter> B) k = (c \<in> A k \<and> c \<in> B k)"
schirmer@13688:   by (unfold intersect_ts_def) blast
schirmer@13688: 
schirmer@13688: lemma intersect_tsI [intro!]: "\<lbrakk>c \<in> A k; c \<in> B k\<rbrakk> \<Longrightarrow> c \<in>  (A \<Rightarrow>\<inter> B) k"
schirmer@13688:   by simp
schirmer@13688: 
schirmer@13688: lemma intersect_tsD1: "c \<in> (A \<Rightarrow>\<inter> B) k \<Longrightarrow> c \<in> A k"
schirmer@13688:   by simp
schirmer@13688: 
schirmer@13688: lemma intersect_tsD2: "c \<in> (A \<Rightarrow>\<inter> B) k \<Longrightarrow> c \<in> B k"
schirmer@13688:   by simp
schirmer@13688: 
schirmer@13688: lemma intersect_tsE [elim!]: 
schirmer@13688:    "\<lbrakk>c \<in> (A \<Rightarrow>\<inter> B) k; \<lbrakk>c \<in> A k; c \<in> B k\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
schirmer@13688:   by simp
schirmer@13688: 
schirmer@13688: 
schirmer@13688: subsubsection {* All-Union of tables and set *}
schirmer@13688: 
schirmer@13688: lemma all_union_ts_iff [simp]: "(c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k) = (c \<in> A k \<or>  c \<in> B)"
schirmer@13688:   by (unfold all_union_ts_def) blast
schirmer@13688: 
schirmer@13688: lemma all_union_tsI1 [elim?]: "c \<in> A k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k"
schirmer@13688:   by simp
schirmer@13688: 
schirmer@13688: lemma all_union_tsI2 [elim?]: "c \<in> B \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k"
schirmer@13688:   by simp
schirmer@13688: 
schirmer@13688: lemma all_union_tsCI [intro!]: "(c \<notin> B \<Longrightarrow> c \<in> A k) \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k"
schirmer@13688:   by auto
schirmer@13688: 
schirmer@13688: lemma all_union_tsE [elim!]: 
schirmer@13688:  "\<lbrakk>c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k; (c \<in> A k \<Longrightarrow> P); (c \<in> B \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
schirmer@13688:   by (unfold all_union_ts_def) blast
schirmer@13688: 
schirmer@13688: 
schirmer@13688: section "The rules of definite assignment"
schirmer@13688: 
schirmer@13688:  
schirmer@13688: types breakass = "(label, lname) tables" 
schirmer@13688: --{* Mapping from a break label, to the set of variables that will be assigned 
schirmer@13688:      if the evaluation terminates with this break *}
schirmer@13688:     
schirmer@13688: record assigned = 
schirmer@13688:          nrm :: "lname set" --{* Definetly assigned variables 
schirmer@13688:                                  for normal completion*}
schirmer@13688:          brk :: "breakass" --{* Definetly assigned variables for 
schirmer@14030:                                 abrupt completion with a break *}
schirmer@13688: 
schirmer@13688: constdefs rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
schirmer@13688: "rmlab k A \<equiv> \<lambda> x. if x=k then UNIV else A x"
schirmer@13688:  
schirmer@13688: (*
schirmer@13688: constdefs setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set"
schirmer@13688: "setbrk b A \<equiv> {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
schirmer@13688: *)
schirmer@13688: 
schirmer@13688: constdefs range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80)
schirmer@13688:  "\<Rightarrow>\<Inter>A \<equiv> {x |x. \<forall> k. x \<in> A k}"
schirmer@13688: 
berghofe@21765: text {*
berghofe@21765: In @{text "E\<turnstile> B \<guillemotright>t\<guillemotright> A"},
berghofe@21765: @{text B} denotes the ''assigned'' variables before evaluating term @{text t},
berghofe@21765: whereas @{text A} denotes the ''assigned'' variables after evaluating term @{text t}.
berghofe@21765: The environment @{term E} is only needed for the conditional @{text "_ ? _ : _"}.
berghofe@21765: The definite assignment rules refer to the typing rules here to
berghofe@21765: distinguish boolean and other expressions.
berghofe@21765: *}
schirmer@13688: 
berghofe@23747: inductive
berghofe@21765:   da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71)
berghofe@21765: where
berghofe@21765:   Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
schirmer@13688: 
berghofe@21765: | Expr: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A 
berghofe@21765:          \<Longrightarrow>  
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"
berghofe@21765: | Lab:  "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; nrm A = nrm C \<inter> (brk C) l; brk A = rmlab l (brk C)\<rbrakk>
berghofe@21765:          \<Longrightarrow> 
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A" 
schirmer@13688: 
berghofe@21765: | Comp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; 
berghofe@21765:          nrm A = nrm C2; brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)\<rbrakk> 
berghofe@21765:          \<Longrightarrow>  
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A"
berghofe@21765: 
berghofe@21765: | If:   "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E;
berghofe@21765:           Env\<turnstile> (B \<union> assigns_if True  e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
berghofe@21765:           Env\<turnstile> (B \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
berghofe@21765:           nrm A = nrm C1 \<inter> nrm C2;
berghofe@21765:           brk A = brk C1 \<Rightarrow>\<inter> brk C2 \<rbrakk>  
berghofe@21765:           \<Longrightarrow>
berghofe@21765:           Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A"
schirmer@13688: 
schirmer@13688: --{* Note that @{term E} is not further used, because we take the specialized
schirmer@13688:      sets that also consider if the expression evaluates to true or false. 
schirmer@13688:      Inside of @{term e} there is no {\tt break} or {\tt finally}, so the break
schirmer@13688:      map of @{term E} will be the trivial one. So 
berghofe@21765:      @{term "Env\<turnstile>B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"} is just used to ensure the definite assignment in
schirmer@13688:      expression @{term e}.
schirmer@13688:      Notice the implicit analysis of a constant boolean expression @{term e}
schirmer@13688:      in this rule. For example, if @{term e} is constantly @{term True} then 
schirmer@13688:      @{term "assigns_if False e = UNIV"} and therefor @{term "nrm C2=UNIV"}.
schirmer@13688:      So finally @{term "nrm A = nrm C1"}. For the break maps this trick 
schirmer@13688:      workd too, because the trival break map will map all labels to 
schirmer@13688:      @{term UNIV}. In the example, if no break occurs in @{term c2} the break
schirmer@13688:      maps will trivially map to @{term UNIV} and if a break occurs it will map
schirmer@13688:      to @{term UNIV} too, because @{term "assigns_if False e = UNIV"}. So
schirmer@13688:      in the intersection of the break maps the path @{term c2} will have no
schirmer@13688:      contribution.
schirmer@13688:   *}
schirmer@13688: 
berghofe@21765: | Loop: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; 
berghofe@21765:           Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
berghofe@21765:           nrm A = nrm C \<inter> (B \<union> assigns_if False e);
berghofe@21765:           brk A = brk C\<rbrakk>  
berghofe@21765:           \<Longrightarrow>
berghofe@21765:           Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"
schirmer@13688: --{* The @{text Loop} rule resembles some of the ideas of the @{text If} rule.
schirmer@13688:      For the @{term "nrm A"} the set @{term "B \<union> assigns_if False e"} 
schirmer@13688:      will be @{term UNIV} if the condition is constantly true. To normally exit
schirmer@13688:      the while loop, we must consider the body @{term c} to be completed 
schirmer@13688:      normally (@{term "nrm C"}) or with a break. But in this model, 
schirmer@13688:      the label @{term l} of the loop
schirmer@13688:      only handles continue labels, not break labels. The break label will be
schirmer@13688:      handled by an enclosing @{term Lab} statement. So we don't have to
schirmer@13688:      handle the breaks specially. 
schirmer@13688:   *}
schirmer@13688: 
berghofe@21765: | Jmp: "\<lbrakk>jump=Ret \<longrightarrow> Result \<in> B;
berghofe@21765:          nrm A = UNIV;
berghofe@21765:          brk A = (case jump of
berghofe@21765:                     Break l \<Rightarrow> \<lambda> k. if k=l then B else UNIV     
berghofe@21765:                   | Cont l  \<Rightarrow> \<lambda> k. UNIV
berghofe@21765:                   | Ret     \<Rightarrow> \<lambda> k. UNIV)\<rbrakk> 
berghofe@21765:         \<Longrightarrow> 
berghofe@21765:         Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A"
schirmer@13688: --{* In case of a break to label @{term l} the corresponding break set is all
schirmer@13688:      variables assigned before the break. The assigned variables for normal
schirmer@13688:      completion of the @{term Jmp} is @{term UNIV}, because the statement will
schirmer@13688:      never complete normally. For continue and return the break map is the 
schirmer@13688:      trivial one. In case of a return we enshure that the result value is
schirmer@13688:      assigned.
schirmer@13688:   *}
schirmer@13688: 
berghofe@21765: | Throw: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = UNIV; brk A = (\<lambda> l. UNIV)\<rbrakk> 
berghofe@21765:          \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | Try:  "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; 
berghofe@21765:           Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;  
berghofe@21765:           nrm A = nrm C1 \<inter> nrm C2;
berghofe@21765:           brk A = brk C1 \<Rightarrow>\<inter> brk C2\<rbrakk> 
berghofe@21765:          \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | Fin:  "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
berghofe@21765:           Env\<turnstile> B \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
berghofe@21765:           nrm A = nrm C1 \<union> nrm C2;
berghofe@21765:           brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)\<rbrakk>  
berghofe@21765:           \<Longrightarrow>
berghofe@21765:           Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A" 
schirmer@13688: --{* The set of assigned variables before execution @{term c2} are the same
schirmer@13688:      as before execution @{term c1}, because @{term c1} could throw an exception
schirmer@13688:      and so we can't guarantee that any variable will be assigned in @{term c1}.
schirmer@13688:      The @{text Finally} statement completes
schirmer@13688:      normally if both @{term c1} and @{term c2} complete normally. If @{term c1}
schirmer@14030:      completes abruptly with a break, then @{term c2} also will be executed 
schirmer@13688:      and may terminate normally or with a break. The overall break map then is
schirmer@13688:      the intersection of the maps of both paths. If @{term c2} terminates 
schirmer@13688:      normally we have to extend all break sets in @{term "brk C1"} with 
schirmer@13688:      @{term "nrm C2"} (@{text "\<Rightarrow>\<union>\<^sub>\<forall>"}). If @{term c2} exits with a break this
schirmer@13688:      break will appear in the overall result state. We don't know if 
schirmer@13688:      @{term c1} completed normally or abruptly (maybe with an exception not only
schirmer@13688:      a break) so @{term c1} has no contribution to the break map following this
schirmer@13688:      path.
schirmer@13688:   *}
schirmer@13688: 
schirmer@13688: --{* Evaluation of expressions and the break sets of definite assignment:
schirmer@13688:      Thinking of a Java expression we assume that we can never have
schirmer@13688:      a break statement inside of a expression. So for all expressions the
schirmer@13688:      break sets could be set to the trivial one: @{term "\<lambda> l. UNIV"}. 
schirmer@13688:      But we can't
schirmer@13688:      trivially proof, that evaluating an expression will never result in a 
schirmer@13688:      break, allthough Java expressions allready syntactically don't allow
schirmer@13688:      nested stetements in them. The reason are the nested class initialzation 
schirmer@13688:      statements which are inserted by the evaluation rules. So to proof the
schirmer@13688:      absence of a break we need to ensure, that the initialization statements
schirmer@13688:      will never end up in a break. In a wellfromed initialization statement, 
schirmer@13688:      of course, were breaks are nested correctly inside of @{term Lab} 
schirmer@13688:      or @{term Loop} statements evaluation of the whole initialization 
schirmer@13688:      statement will never result in a break, because this break will be 
schirmer@13688:      handled inside of the statement. But for simplicity we haven't added
schirmer@13688:      the analysis of the correct nesting of breaks in the typing judgments 
schirmer@13688:      right now. So we have decided to adjust the rules of definite assignment
schirmer@13688:      to fit to these circumstances. If an initialization is involved during
schirmer@13688:      evaluation of the expression (evaluation rules @{text FVar}, @{text NewC} 
schirmer@13688:      and @{text NewA}
schirmer@13688: *}
schirmer@13688: 
berghofe@21765: | Init: "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
schirmer@13688: --{* Wellformedness of a program will ensure, that every static initialiser 
schirmer@13688:      is definetly assigned and the jumps are nested correctly. The case here
schirmer@13688:      for @{term Init} is just for convenience, to get a proper precondition 
schirmer@13688:      for the induction hypothesis in various proofs, so that we don't have to
schirmer@13688:      expand the initialisation on every point where it is triggerred by the
schirmer@13688:      evaluation rules.
schirmer@13688:   *}   
berghofe@21765: | NewC: "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" 
berghofe@21765: 
berghofe@21765: | NewA: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A 
berghofe@21765:          \<Longrightarrow>
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | Cast: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
berghofe@21765:          \<Longrightarrow>
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | Inst: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A 
berghofe@21765:          \<Longrightarrow> 
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | Lit:  "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
schirmer@13688: 
berghofe@21765: | UnOp: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
berghofe@21765:          \<Longrightarrow> 
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | CondAnd: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if True e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; 
berghofe@21765:              nrm A = B \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter> 
berghofe@21765:                              assigns_if False (BinOp CondAnd e1 e2));
berghofe@21765:              brk A = (\<lambda> l. UNIV) \<rbrakk>
berghofe@21765:             \<Longrightarrow>
berghofe@21765:             Env\<turnstile> B \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | CondOr: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if False e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; 
berghofe@21765:             nrm A = B \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter> 
berghofe@21765:                               assigns_if False (BinOp CondOr e1 e2));
schirmer@13688:             brk A = (\<lambda> l. UNIV) \<rbrakk>
berghofe@21765:             \<Longrightarrow>
berghofe@21765:             Env\<turnstile> B \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | BinOp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A; 
berghofe@21765:            binop \<noteq> CondAnd; binop \<noteq> CondOr\<rbrakk>
berghofe@21765:           \<Longrightarrow>
berghofe@21765:           Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | Super: "This \<in> B 
berghofe@21765:           \<Longrightarrow> 
berghofe@21765:           Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
schirmer@13688: 
berghofe@21765: | AccLVar: "\<lbrakk>vn \<in> B;
berghofe@21765:              nrm A = B; brk A = (\<lambda> k. UNIV)\<rbrakk> 
berghofe@21765:              \<Longrightarrow> 
berghofe@21765:              Env\<turnstile> B \<guillemotright>\<langle>Acc (LVar vn)\<rangle>\<guillemotright> A"
schirmer@13688: --{* To properly access a local variable we have to test the definite 
schirmer@13688:      assignment here. The variable must occur in the set @{term B} 
schirmer@13688:   *}
schirmer@13688: 
berghofe@21765: | Acc: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn;
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> A\<rbrakk>
berghofe@21765:          \<Longrightarrow>
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | AssLVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = nrm E \<union> {vn}; brk A = brk E\<rbrakk> 
berghofe@21765:             \<Longrightarrow> 
berghofe@21765:             Env\<turnstile> B \<guillemotright>\<langle>(LVar vn) := e\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | Ass: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn; Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V; Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A\<rbrakk>
berghofe@21765:          \<Longrightarrow>
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A"
schirmer@13688: 
berghofe@21765: | CondBool: "\<lbrakk>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean);
berghofe@21765:               Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
berghofe@21765:               Env\<turnstile> (B \<union> assigns_if True  c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1;
berghofe@21765:               Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
berghofe@21765:               nrm A = B \<union> (assigns_if True  (c ? e1 : e2) \<inter> 
berghofe@21765:                                assigns_if False (c ? e1 : e2));
berghofe@21765:               brk A = (\<lambda> l. UNIV)\<rbrakk>
berghofe@21765:               \<Longrightarrow> 
berghofe@21765:               Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" 
schirmer@13688: 
berghofe@21765: | Cond: "\<lbrakk>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean);
berghofe@21765:           Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
berghofe@21765:           Env\<turnstile> (B \<union> assigns_if True  c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1;
berghofe@21765:           Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2;
berghofe@21765:           nrm A = nrm E1 \<inter> nrm E2; brk A = (\<lambda> l. UNIV)\<rbrakk>
berghofe@21765:           \<Longrightarrow> 
berghofe@21765:           Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" 
schirmer@13688: 
berghofe@21765: | Call: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A\<rbrakk> 
berghofe@21765:          \<Longrightarrow>  
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A"
schirmer@13688: 
schirmer@13688: -- {* The interplay of @{term Call}, @{term Methd} and @{term Body}:
schirmer@13688:       Why rules for @{term Methd} and @{term Body} at all? Note that a
schirmer@13688:       Java source program will not include bare  @{term Methd} or @{term Body}
schirmer@13688:       terms. These terms are just introduced during evaluation. So definite
schirmer@13688:       assignment of @{term Call} does not consider @{term Methd} or 
schirmer@13688:       @{term Body} at all. So for definite assignment alone we could omit the
schirmer@13688:       rules for @{term Methd} and @{term Body}. 
schirmer@13688:       But since evaluation of the method invocation is
schirmer@13688:       split up into three rules we must ensure that we have enough information
schirmer@13688:       about the call even in the @{term Body} term to make sure that we can
schirmer@13688:       proof type safety. Also we must be able transport this information 
schirmer@13688:       from @{term Call} to @{term Methd} and then further to @{term Body} 
schirmer@13688:       during evaluation to establish the definite assignment of @{term Methd}
schirmer@13688:       during evaluation of @{term Call}, and of @{term Body} during evaluation
schirmer@13688:       of @{term Methd}. This is necessary since definite assignment will be
schirmer@13688:       a precondition for each induction hypothesis coming out of the evaluation
schirmer@13688:       rules, and therefor we have to establish the definite assignment of the
schirmer@13688:       sub-evaluation during the type-safety proof. Note that well-typedness is
schirmer@13688:       also a precondition for type-safety and so we can omit some assertion 
schirmer@13688:       that are already ensured by well-typedness. 
schirmer@13688:    *}
berghofe@21765: | Methd: "\<lbrakk>methd (prg Env) D sig = Some m;
berghofe@21765:            Env\<turnstile> B \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A
berghofe@21765:           \<rbrakk>
berghofe@21765:           \<Longrightarrow>
berghofe@21765:           Env\<turnstile> B \<guillemotright>\<langle>Methd D sig\<rangle>\<guillemotright> A" 
berghofe@21765: 
berghofe@21765: | Body: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; jumpNestingOkS {Ret} c; Result \<in> nrm C;
berghofe@21765:           nrm A = B; brk A = (\<lambda> l. UNIV)\<rbrakk>
schirmer@13688:          \<Longrightarrow>
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A"
schirmer@13688: -- {* Note that @{term A} is not correlated to  @{term C}. If the body
schirmer@13688:       statement returns abruptly with return, evaluation of  @{term Body}
schirmer@13688:       will absorb this return and complete normally. So we cannot trivially
schirmer@13688:       get the assigned variables of the body statement since it has not 
schirmer@13688:       completed normally or with a break.
schirmer@13688:       If the body completes normally we guarantee that the result variable
schirmer@13688:       is set with this rule. But if the body completes abruptly with a return
schirmer@13688:       we can't guarantee that the result variable is set here, since 
schirmer@13688:       definite assignment only talks about normal completion and breaks. So
schirmer@13688:       for a return the @{term Jump} rule ensures that the result variable is
schirmer@13688:       set and then this information must be carried over to the @{term Body}
schirmer@13688:       rule by the conformance predicate of the state.
schirmer@13688:    *}
berghofe@21765: | LVar: "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>" 
schirmer@13688: 
berghofe@21765: | FVar: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A 
schirmer@13688:          \<Longrightarrow> 
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A" 
schirmer@13688: 
berghofe@21765: | AVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A\<rbrakk>
berghofe@21765:           \<Longrightarrow> 
berghofe@21765:           Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A" 
schirmer@13688: 
berghofe@21765: | Nil: "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>" 
berghofe@21765: 
berghofe@21765: | Cons: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e::expr\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A\<rbrakk>
berghofe@21765:          \<Longrightarrow> 
berghofe@21765:          Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A" 
schirmer@13688: 
schirmer@13688: 
schirmer@13688: declare inj_term_sym_simps [simp]
schirmer@13688: declare assigns_if.simps [simp del]
schirmer@13688: declare split_paired_All [simp del] split_paired_Ex [simp del]
schirmer@13688: ML_setup {*
wenzelm@17876: change_simpset (fn ss => ss delloop "split_all_tac");
schirmer@13688: *}
berghofe@23747: inductive_cases da_elim_cases [cases set]:
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r (Expr e)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> c\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r (l\<bullet> c)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r (c1;; c2)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r (If(e) c1 Else c2)\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A"  
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r (Jmp jump)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r (Throw e)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r (Try c1 Catch(C vn) c2)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r (c1 Finally c2)\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1r (Init C)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (NewC C)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (New T[e])\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (Cast T e)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (e InstOf T)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (Lit v)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (UnOp unop e)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (BinOp binop e1 e2)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (Super)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (Acc v)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (v := e)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (c ? e1 : e2)\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l ({accC,statT,mode}e\<cdot>mn({pTs}args))\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Methd C sig\<rangle>\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (Methd C sig)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In1l (Body D c)\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In2 (LVar vn)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In2 ({accC,statDeclC,stat}e..fn)\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In2 (e1.[e2])\<guillemotright> A" 
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In3 ([]::expr list)\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A"
schirmer@13688:   "Env\<turnstile> B \<guillemotright>In3 (e#es)\<guillemotright> A"
schirmer@13688: declare inj_term_sym_simps [simp del]
schirmer@13688: declare assigns_if.simps [simp]
schirmer@13688: declare split_paired_All [simp] split_paired_Ex [simp]
schirmer@13688: ML_setup {*
wenzelm@17876: change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
schirmer@13688: *}
schirmer@13688: (* To be able to eliminate both the versions with the overloaded brackets: 
schirmer@13688:    (B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A), 
schirmer@13688:    every rule appears in both versions
schirmer@13688:  *)
schirmer@13688: 
schirmer@13688: lemma da_Skip: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
schirmer@13688:   by (auto intro: da.Skip)
schirmer@13688: 
schirmer@13688: lemma da_NewC: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> A"
schirmer@13688:   by (auto intro: da.NewC)
schirmer@13688:  
schirmer@13688: lemma da_Lit:  "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> A"
schirmer@13688:   by (auto intro: da.Lit)
schirmer@13688: 
schirmer@13688: lemma da_Super: "\<lbrakk>This \<in> B;A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>\<rbrakk> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> A"
schirmer@13688:   by (auto intro: da.Super)
schirmer@13688: 
schirmer@13688: lemma da_Init: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> A"
schirmer@13688:   by (auto intro: da.Init)
schirmer@13688: 
schirmer@13688: 
schirmer@13688: (*
schirmer@13688: For boolean expressions:
schirmer@13688: 
schirmer@13688: The following holds: "assignsE e \<subseteq> assigns_if True e \<inter> assigns_if False e"
schirmer@13688: but not vice versa:
schirmer@13688:  "assigns_if True e \<inter> assigns_if False e \<subseteq> assignsE e"
schirmer@13688: 
schirmer@13688: Example: 
schirmer@13688:  e = ((x < 5) || (y = true)) && (y = true)
schirmer@13688: 
schirmer@13688:    =  (   a    ||    b     ) &&    c
schirmer@13688: 
schirmer@13688: assigns_if True  a = {}
schirmer@13688: assigns_if False a = {}
schirmer@13688: 
schirmer@13688: assigns_if True  b = {y}
schirmer@13688: assigns_if False b = {y}
schirmer@13688: 
schirmer@13688: assigns_if True  c = {y}
schirmer@13688: assigns_if False c = {y}
schirmer@13688: 
schirmer@13688: assigns_if True (a || b) = assigns_if True a \<inter> 
schirmer@13688:                                 (assigns_if False a \<union> assigns_if True b)
schirmer@13688:                            = {} \<inter> ({} \<union> {y}) = {}
schirmer@13688: assigns_if False (a || b) = assigns_if False a \<union> assigns_if False b
schirmer@13688:                             = {} \<union> {y} = {y}
schirmer@13688: 
schirmer@13688: 
schirmer@13688: 
schirmer@13688: assigns_ifE True e =  assigns_if True (a || b) \<union> assigns_if True c
schirmer@13688:                     = {} \<union> {y} = {y}
schirmer@13688: assigns_ifE False e = assigns_if False (a || b) \<inter> 
schirmer@13688:                        (assigns_if True (a || b) \<union> assigns_if False c)
schirmer@13688:                      = {y} \<inter> ({} \<union> {y}) = {y}
schirmer@13688: 
schirmer@13688: assignsE e = {}
schirmer@13688: *)  
schirmer@13688: 
schirmer@13688: lemma assignsE_subseteq_assigns_ifs:
schirmer@13688:  assumes boolEx: "E\<turnstile>e\<Colon>-PrimT Boolean" (is "?Boolean e")
schirmer@13688:    shows "assignsE e \<subseteq> assigns_if True e \<inter> assigns_if False e" (is "?Incl e")
schirmer@13688: proof -
schirmer@13688:   have True and "?Boolean e \<Longrightarrow> ?Incl e" and True and True
wenzelm@18459:   proof (induct _ and e and _ and _ rule: var_expr_stmt.inducts)
schirmer@13688:     case (Cast T e)
schirmer@13688:     have "E\<turnstile>e\<Colon>- (PrimT Boolean)"
schirmer@13688:     proof -
wenzelm@23350:       from `E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)`
wenzelm@23350:       obtain Te where "E\<turnstile>e\<Colon>-Te"
schirmer@13688:                            "prg E\<turnstile>Te\<preceq>? PrimT Boolean"
schirmer@13688: 	by cases simp
schirmer@13688:       thus ?thesis
schirmer@13688: 	by - (drule cast_Boolean2,simp)
schirmer@13688:     qed
schirmer@13688:     with Cast.hyps
schirmer@13688:     show ?case
schirmer@13688:       by simp
schirmer@13688:   next	
schirmer@13688:     case (Lit val) 
schirmer@13688:     thus ?case
schirmer@13688:       by - (erule wt_elim_cases, cases "val", auto simp add: empty_dt_def)
schirmer@13688:   next
schirmer@13688:     case (UnOp unop e) 
schirmer@13688:     thus ?case
schirmer@13688:       by - (erule wt_elim_cases,cases unop,
schirmer@13688:             (fastsimp simp add: assignsE_const_simp)+)
schirmer@13688:   next
schirmer@13688:     case (BinOp binop e1 e2)
schirmer@13688:     from BinOp.prems obtain e1T e2T
schirmer@13688:       where "E\<turnstile>e1\<Colon>-e1T" and "E\<turnstile>e2\<Colon>-e2T" and "wt_binop (prg E) binop e1T e2T"
schirmer@13688:             and "(binop_type binop) = Boolean"
schirmer@13688:       by (elim wt_elim_cases) simp
schirmer@13688:     with BinOp.hyps
schirmer@13688:     show ?case
schirmer@13688:       by - (cases binop, auto simp add: assignsE_const_simp)
schirmer@13688:   next
schirmer@13688:     case (Cond c e1 e2)
wenzelm@23350:     note hyp_c = `?Boolean c \<Longrightarrow> ?Incl c`
wenzelm@23350:     note hyp_e1 = `?Boolean e1 \<Longrightarrow> ?Incl e1`
wenzelm@23350:     note hyp_e2 = `?Boolean e2 \<Longrightarrow> ?Incl e2`
wenzelm@23350:     note wt = `E\<turnstile>(c ? e1 : e2)\<Colon>-PrimT Boolean`
schirmer@13688:     then obtain
schirmer@13688:       boolean_c:  "E\<turnstile>c\<Colon>-PrimT Boolean" and
schirmer@13688:       boolean_e1: "E\<turnstile>e1\<Colon>-PrimT Boolean" and
schirmer@13688:       boolean_e2: "E\<turnstile>e2\<Colon>-PrimT Boolean"
schirmer@13688:       by (elim wt_elim_cases) (auto dest: widen_Boolean2)
schirmer@13688:     show ?case
schirmer@13688:     proof (cases "constVal c")
schirmer@13688:       case None
schirmer@13688:       with boolean_e1 boolean_e2
schirmer@13688:       show ?thesis
schirmer@13688: 	using hyp_e1 hyp_e2 
schirmer@13688: 	by (auto)
schirmer@13688:     next
schirmer@13688:       case (Some bv)
schirmer@13688:       show ?thesis
schirmer@13688:       proof (cases "the_Bool bv")
schirmer@13688: 	case True
schirmer@13688: 	with Some show ?thesis using hyp_e1 boolean_e1 by auto
schirmer@13688:       next
schirmer@13688: 	case False
schirmer@13688: 	with Some show ?thesis using hyp_e2 boolean_e2 by auto
schirmer@13688:       qed
schirmer@13688:     qed
schirmer@13688:   qed simp_all
schirmer@13688:   with boolEx 
schirmer@13688:   show ?thesis
schirmer@13688:     by blast
schirmer@13688: qed
schirmer@13688:   
schirmer@13688: 
schirmer@13688: (* Trick:
schirmer@13688:    If you have a rule with the abstract term injections:
schirmer@13688:    e.g:  da.Skip "B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
schirmer@13688:    and the current goal state as an concrete injection:
schirmer@13688:    e.g: "B \<guillemotright>In1r Skip\<guillemotright> A"
schirmer@13688:    you can convert the rule by: da.Skip [simplified]
schirmer@13688:    if inj_term_simps is in the simpset
schirmer@13688: 
schirmer@13688: *)
schirmer@13688: 
schirmer@13688: lemma rmlab_same_label [simp]: "(rmlab l A) l = UNIV"
schirmer@13688:   by (simp add: rmlab_def)
schirmer@13688: 
schirmer@13688: lemma rmlab_same_label1 [simp]: "l=l' \<Longrightarrow> (rmlab l A) l' = UNIV"
schirmer@13688:   by (simp add: rmlab_def)
schirmer@13688: 
schirmer@13688: lemma rmlab_other_label [simp]: "l\<noteq>l'\<Longrightarrow> (rmlab l A) l' = A l'"
schirmer@13688:   by (auto simp add: rmlab_def)
schirmer@13688: 
schirmer@13688: lemma range_inter_ts_subseteq [intro]: "\<forall> k. A k  \<subseteq> B k \<Longrightarrow>  \<Rightarrow>\<Inter>A \<subseteq> \<Rightarrow>\<Inter>B"
schirmer@13688:   by (auto simp add: range_inter_ts_def)
schirmer@13688: 
schirmer@13688: lemma range_inter_ts_subseteq': 
schirmer@13688:   "\<lbrakk>\<forall> k. A k  \<subseteq> B k; x \<in> \<Rightarrow>\<Inter>A\<rbrakk> \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>B"
schirmer@13688:   by (auto simp add: range_inter_ts_def)
schirmer@13688: 
schirmer@13688: lemma da_monotone: 
wenzelm@23350:   assumes da: "Env\<turnstile> B  \<guillemotright>t\<guillemotright> A" and
wenzelm@23350:     "B \<subseteq> B'" and
wenzelm@23350:     da': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" 
schirmer@13688:   shows "(nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"
schirmer@13688: proof -
schirmer@13688:   from da
schirmer@13688:   show "\<And> B' A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; B \<subseteq> B'\<rbrakk> 
schirmer@13688:                   \<Longrightarrow> (nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"
schirmer@13688:        (is "PROP ?Hyp Env B t A")  
schirmer@13688:   proof (induct)
schirmer@13688:     case Skip 
schirmer@13688:     from Skip.prems Skip.hyps 
schirmer@13688:     show ?case by cases simp
schirmer@13688:   next
schirmer@13688:     case Expr 
schirmer@13688:     from Expr.prems Expr.hyps 
schirmer@13688:     show ?case by cases simp
schirmer@13688:   next
berghofe@21765:     case (Lab Env B c C A l B' A')
wenzelm@23350:     note A = `nrm A = nrm C \<inter> brk C l` `brk A = rmlab l (brk C)`
wenzelm@23350:     note `PROP ?Hyp Env B \<langle>c\<rangle> C`
schirmer@13688:     moreover
wenzelm@23350:     note `B \<subseteq> B'`
schirmer@13688:     moreover
schirmer@13688:     obtain C'
schirmer@13688:       where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
schirmer@13688:         and A': "nrm A' = nrm C' \<inter> brk C' l" "brk A' = rmlab l (brk C')"
schirmer@13688:       using Lab.prems
schirmer@13688:       by - (erule da_elim_cases,simp)
schirmer@13688:     ultimately
schirmer@13688:     have "nrm C \<subseteq> nrm C'" and hyp_brk: "(\<forall>l. brk C l \<subseteq> brk C' l)" by auto
schirmer@13688:     then 
schirmer@13688:     have "nrm C \<inter> brk C l \<subseteq> nrm C' \<inter> brk C' l" by auto
schirmer@13688:     moreover
schirmer@13688:     {
schirmer@13688:       fix l'
schirmer@13688:       from hyp_brk
schirmer@13688:       have "rmlab l (brk C) l'  \<subseteq> rmlab l (brk C') l'"
schirmer@13688: 	by  (cases "l=l'") simp_all
schirmer@13688:     }
schirmer@13688:     moreover note A A'
schirmer@13688:     ultimately show ?case
schirmer@13688:       by simp
schirmer@13688:   next
berghofe@21765:     case (Comp Env B c1 C1 c2 C2 A B' A')
wenzelm@23350:     note A = `nrm A = nrm C2` `brk A = brk C1 \<Rightarrow>\<inter>  brk C2`
wenzelm@23350:     from `Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'`
wenzelm@23350:     obtain  C1' C2'
schirmer@13688:       where da_c1: "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
schirmer@13688:             da_c2: "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"  and
schirmer@13688:             A': "nrm A' = nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'"
schirmer@13688:       by (rule da_elim_cases) auto
wenzelm@23350:     note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
wenzelm@23350:     moreover note `B \<subseteq> B'`
schirmer@13688:     moreover note da_c1
schirmer@13688:     ultimately have C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
wenzelm@23350:       by auto
wenzelm@23350:     note `PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle> C2`
schirmer@13688:     with da_c2 C1' 
schirmer@13688:     have C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
wenzelm@23350:       by auto
schirmer@13688:     with A A' C1'
schirmer@13688:     show ?case
schirmer@13688:       by auto
schirmer@13688:   next
berghofe@21765:     case (If Env B e E c1 C1 c2 C2 A B' A')
wenzelm@23350:     note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter>  brk C2`
wenzelm@23350:     from `Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'`
wenzelm@23350:     obtain C1' C2'
schirmer@13688:       where da_c1: "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
schirmer@13688:             da_c2: "Env\<turnstile> B' \<union> assigns_if False e \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
schirmer@13688:                A': "nrm A' = nrm C1' \<inter> nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'"
schirmer@13688:       by (rule da_elim_cases) auto
wenzelm@23350:     note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1`
wenzelm@23350:     moreover note B' = `B \<subseteq> B'`
schirmer@13688:     moreover note da_c1 
schirmer@13688:     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
schirmer@13688:       by blast
wenzelm@23350:     note `PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle> C2`
schirmer@13688:     with da_c2 B'
schirmer@13688:     obtain C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
schirmer@13688:       by blast
schirmer@13688:     with A A' C1'
schirmer@13688:     show ?case
schirmer@13688:       by auto
schirmer@13688:   next
berghofe@21765:     case (Loop Env B e E c C A l B' A')
wenzelm@23350:     note A = `nrm A = nrm C \<inter> (B \<union> assigns_if False e)` `brk A = brk C`
wenzelm@23350:     from `Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'`
wenzelm@23350:     obtain C'
schirmer@13688:       where 
schirmer@13688:        da_c': "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
schirmer@13688:           A': "nrm A' = nrm C' \<inter> (B' \<union> assigns_if False e)"
schirmer@13688:               "brk A' = brk C'" 
schirmer@13688:       by (rule da_elim_cases) auto
wenzelm@23350:     note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C`
wenzelm@23350:     moreover note B' = `B \<subseteq> B'`
schirmer@13688:     moreover note da_c'
schirmer@13688:     ultimately obtain C': "nrm C \<subseteq> nrm C'" "(\<forall>l. brk C l \<subseteq> brk C' l)"
schirmer@13688:       by blast
schirmer@13688:     with A A' B'
schirmer@13688:     have "nrm A \<subseteq> nrm A'"
schirmer@13688:       by blast
schirmer@13688:     moreover
schirmer@13688:     { fix l'
schirmer@13688:       have  "brk A l' \<subseteq> brk A' l'"
schirmer@13688:       proof (cases "constVal e")
schirmer@13688: 	case None
schirmer@13688: 	with A A' C' 
schirmer@13688: 	show ?thesis
schirmer@13688: 	   by (cases "l=l'") auto
schirmer@13688:       next
schirmer@13688: 	case (Some bv)
schirmer@13688: 	with A A' C'
schirmer@13688: 	show ?thesis
schirmer@13688: 	  by (cases "the_Bool bv", cases "l=l'") auto
schirmer@13688:       qed
schirmer@13688:     }
schirmer@13688:     ultimately show ?case
schirmer@13688:       by auto
schirmer@13688:   next
berghofe@21765:     case (Jmp jump B A Env B' A')
schirmer@13688:     thus ?case by (elim da_elim_cases) (auto split: jump.splits)
schirmer@13688:   next
schirmer@13688:     case Throw thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:   next
berghofe@21765:     case (Try Env B c1 C1 vn C c2 C2 A B' A')
wenzelm@23350:     note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter>  brk C2`
wenzelm@23350:     from `Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'`
wenzelm@23350:     obtain C1' C2'
schirmer@13688:       where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
schirmer@13688:             da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} 
schirmer@13688:                       \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
schirmer@13688:             A': "nrm A' = nrm C1' \<inter> nrm C2'"
schirmer@13688:                 "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'" 
schirmer@13688:       by (rule da_elim_cases) auto
wenzelm@23350:     note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
wenzelm@23350:     moreover note B' = `B \<subseteq> B'`
schirmer@13688:     moreover note da_c1'
schirmer@13688:     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
schirmer@13688:       by blast
wenzelm@23350:     note `PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
wenzelm@23350:                     (B \<union> {VName vn}) \<langle>c2\<rangle> C2`
schirmer@13688:     with B' da_c2'
schirmer@13688:     obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
schirmer@13688:       by blast
schirmer@13688:     with C1' A A'
schirmer@13688:     show ?case
schirmer@13688:       by auto
schirmer@13688:   next
berghofe@21765:     case (Fin Env B c1 C1 c2 C2 A B' A')
wenzelm@23350:     note A = `nrm A = nrm C1 \<union> nrm C2`
wenzelm@23350:       `brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)`
wenzelm@23350:     from `Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'`
wenzelm@23350:     obtain C1' C2'
schirmer@13688:       where  da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
schirmer@13688:              da_c2': "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
schirmer@13688:              A':  "nrm A' = nrm C1' \<union> nrm C2'"
schirmer@13688:                   "brk A' = (brk C1' \<Rightarrow>\<union>\<^sub>\<forall> nrm C2') \<Rightarrow>\<inter> (brk C2')"
schirmer@13688:       by (rule da_elim_cases) auto
wenzelm@23350:     note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
wenzelm@23350:     moreover note B' = `B \<subseteq> B'`
schirmer@13688:     moreover note da_c1'
schirmer@13688:     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
schirmer@13688:       by blast
wenzelm@23350:     note hyp_c2 = `PROP ?Hyp Env B \<langle>c2\<rangle> C2`
schirmer@13688:     from da_c2' B' 
schirmer@13688:      obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
schirmer@13688:        by - (drule hyp_c2,auto)
schirmer@13688:      with A A' C1'
schirmer@13688:      show ?case
schirmer@13688:        by auto
schirmer@13688:    next
schirmer@13688:      case Init thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case NewC thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case NewA thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case Cast thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case Inst thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case Lit thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case UnOp thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
berghofe@21765:      case (CondAnd Env B e1 E1 e2 E2 A B' A')
wenzelm@23350:      note A = `nrm A = B \<union>
schirmer@13688:                        assigns_if True (BinOp CondAnd e1 e2) \<inter>
wenzelm@23350:                        assigns_if False (BinOp CondAnd e1 e2)`
wenzelm@23350:              `brk A = (\<lambda>l. UNIV)`
wenzelm@23350:      from `Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'`
wenzelm@23350:      obtain  A': "nrm A' = B' \<union>
schirmer@13688:                                  assigns_if True (BinOp CondAnd e1 e2) \<inter>
schirmer@13688:                                  assigns_if False (BinOp CondAnd e1 e2)"
schirmer@13688:                       "brk A' = (\<lambda>l. UNIV)" 
schirmer@13688:        by (rule da_elim_cases) auto
wenzelm@23350:      note B' = `B \<subseteq> B'`
schirmer@13688:      with A A' show ?case 
schirmer@13688:        by auto 
schirmer@13688:    next
schirmer@13688:      case CondOr thus ?case by - (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case BinOp thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case Super thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case AccLVar thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case Acc thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case AssLVar thus ?case by - (erule da_elim_cases, auto)
schirmer@13688:    next
schirmer@13688:      case Ass thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:    next
berghofe@21765:      case (CondBool Env c e1 e2 B C E1 E2 A B' A')
wenzelm@23350:      note A = `nrm A = B \<union> 
schirmer@13688:                         assigns_if True (c ? e1 : e2) \<inter> 
wenzelm@23350:                         assigns_if False (c ? e1 : e2)`
wenzelm@23350:              `brk A = (\<lambda>l. UNIV)`
wenzelm@23350:      note `Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)`
schirmer@13688:      moreover
wenzelm@23350:      note `Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'`
schirmer@13688:      ultimately
schirmer@13688:      obtain A': "nrm A' = B' \<union> 
schirmer@13688:                                   assigns_if True (c ? e1 : e2) \<inter> 
schirmer@13688:                                   assigns_if False (c ? e1 : e2)"
schirmer@13688:                      "brk A' = (\<lambda>l. UNIV)"
schirmer@13688:        by - (erule da_elim_cases,auto simp add: inj_term_simps) 
schirmer@13688:        (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
wenzelm@23350:      note B' = `B \<subseteq> B'`
schirmer@13688:      with A A' show ?case 
schirmer@13688:        by auto 
schirmer@13688:    next
berghofe@21765:      case (Cond Env c e1 e2 B C E1 E2 A B' A')  
wenzelm@23350:      note A = `nrm A = nrm E1 \<inter> nrm E2` `brk A = (\<lambda>l. UNIV)`
wenzelm@23350:      note not_bool = `\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)`
wenzelm@23350:      from `Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'`
wenzelm@23350:      obtain E1' E2'
schirmer@13688:        where da_e1': "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and
schirmer@13688:              da_e2': "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and
schirmer@13688:                  A': "nrm A' = nrm E1' \<inter> nrm E2'"
schirmer@13688:                      "brk A' = (\<lambda>l. UNIV)"
schirmer@13688:        using not_bool
schirmer@13688:        by  - (erule da_elim_cases, auto simp add: inj_term_simps)
schirmer@13688:        (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
wenzelm@23350:      note `PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1`
wenzelm@23350:      moreover note B' = `B \<subseteq> B'`
schirmer@13688:      moreover note da_e1'
schirmer@13688:      ultimately obtain E1': "nrm E1 \<subseteq> nrm E1'" "(\<forall>l. brk E1 l \<subseteq> brk E1' l)"
wenzelm@23350:        by blast
wenzelm@23350:      note `PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle> E2`
schirmer@13688:      with B' da_e2'
schirmer@13688:      obtain "nrm E2 \<subseteq> nrm E2'" "(\<forall>l. brk E2 l \<subseteq> brk E2' l)"
schirmer@13688:        by blast
schirmer@13688:     with E1' A A'
schirmer@13688:     show ?case
schirmer@13688:       by auto
schirmer@13688:   next
schirmer@13688:     case Call
schirmer@13688:     from Call.prems and Call.hyps
schirmer@13688:     show ?case by cases auto
schirmer@13688:   next
schirmer@13688:     case Methd thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:   next
schirmer@13688:     case Body thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:   next
schirmer@13688:     case LVar thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:   next
schirmer@13688:     case FVar thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:   next
schirmer@13688:     case AVar thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:   next
schirmer@13688:     case Nil thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:   next
schirmer@13688:     case Cons thus ?case by -  (erule da_elim_cases, auto)
schirmer@13688:   qed
wenzelm@23350: qed (rule da', rule `B \<subseteq> B'`)
schirmer@13688:   
schirmer@13688: lemma da_weaken:     
wenzelm@23350:   assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and "B \<subseteq> B'" 
wenzelm@23350:   shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'"
schirmer@13688: proof -
wenzelm@15801:   note assigned.select_convs [Pure.intro]
schirmer@13688:   from da  
schirmer@13688:   show "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
schirmer@13688:   proof (induct) 
nipkow@17589:     case Skip thus ?case by (iprover intro: da.Skip)
schirmer@13688:   next
nipkow@17589:     case Expr thus ?case by (iprover intro: da.Expr)
schirmer@13688:   next
berghofe@21765:     case (Lab Env B c C A l B')  
wenzelm@23350:     note `PROP ?Hyp Env B \<langle>c\<rangle>`
schirmer@13688:     moreover
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     ultimately obtain C' where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
nipkow@17589:       by iprover
schirmer@13688:     then obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.Lab)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
berghofe@21765:     case (Comp Env B c1 C1 c2 C2 A B')
wenzelm@23350:     note da_c1 = `Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1`
wenzelm@23350:     note `PROP ?Hyp Env B \<langle>c1\<rangle>`
schirmer@13688:     moreover
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     ultimately obtain C1' where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
nipkow@17589:       by iprover
schirmer@13688:     with da_c1 B'
schirmer@13688:     have
schirmer@13688:       "nrm C1 \<subseteq> nrm C1'"
schirmer@13688:       by (rule da_monotone [elim_format]) simp
schirmer@13688:     moreover
wenzelm@23350:     note `PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>`
schirmer@13688:     ultimately obtain C2' where "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
nipkow@17589:       by iprover
schirmer@13688:     with da_c1' obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.Comp)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
berghofe@21765:     case (If Env B e E c1 C1 c2 C2 A B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     obtain  E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule If.hyps)
schirmer@13688:       with B'  
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain C1' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
schirmer@13688:     proof -
schirmer@13688:       from B'
schirmer@13688:       have "(B \<union> assigns_if True e) \<subseteq> (B' \<union> assigns_if True e)"
schirmer@13688: 	by blast
schirmer@13688:       moreover
schirmer@13688:       have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle>" by (rule If.hyps)
schirmer@13688:       ultimately 
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain C2' where "Env\<turnstile> (B' \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
schirmer@13688:     proof - 
schirmer@13688:       from B' have "(B \<union> assigns_if False e) \<subseteq> (B' \<union> assigns_if False e)"
schirmer@13688: 	by blast
schirmer@13688:       moreover
schirmer@13688:       have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle>" by (rule If.hyps)
schirmer@13688:       ultimately
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     ultimately
schirmer@13688:     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.If)
schirmer@13688:     thus ?case ..
schirmer@13688:   next  
berghofe@21765:     case (Loop Env B e E c C A l B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
wenzelm@23350:     obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Loop.hyps)
schirmer@13688:       with B'  
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain C' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
schirmer@13688:     proof -
schirmer@13688:       from B'
schirmer@13688:       have "(B \<union> assigns_if True e) \<subseteq> (B' \<union> assigns_if True e)"
schirmer@13688: 	by blast
schirmer@13688:       moreover
schirmer@13688:       have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle>" by (rule Loop.hyps)
schirmer@13688:       ultimately 
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     ultimately
schirmer@13688:     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.Loop )
schirmer@13688:     thus ?case ..
schirmer@13688:   next
berghofe@21765:     case (Jmp jump B A Env B') 
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     with Jmp.hyps have "jump = Ret \<longrightarrow> Result \<in> B' "
schirmer@13688:       by auto
schirmer@13688:     moreover
schirmer@13688:     obtain A'::assigned 
schirmer@13688:               where  "nrm A' = UNIV"
schirmer@13688:                      "brk A' = (case jump of 
schirmer@13688:                                   Break l \<Rightarrow> \<lambda>k. if k = l then B' else UNIV 
schirmer@13688:                                 | Cont l \<Rightarrow> \<lambda>k. UNIV
schirmer@13688:                                 | Ret \<Rightarrow> \<lambda>k. UNIV)"
schirmer@13688:                      
nipkow@17589:       by  iprover
schirmer@13688:     ultimately have "Env\<turnstile> B' \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A'"
schirmer@13688:       by (rule da.Jmp)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
nipkow@17589:     case Throw thus ?case by (iprover intro: da.Throw )
schirmer@13688:   next
berghofe@21765:     case (Try Env B c1 C1 vn C c2 C2 A B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     obtain C1' where "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Try.hyps)
schirmer@13688:       with B'  
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain C2' where 
schirmer@13688:       "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
schirmer@13688:     proof -
schirmer@13688:       from B' have "B \<union> {VName vn} \<subseteq> B' \<union> {VName vn}" by blast
schirmer@13688:       moreover
schirmer@13688:       have "PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) 
schirmer@13688:                       (B \<union> {VName vn}) \<langle>c2\<rangle>" 
schirmer@13688: 	by (rule Try.hyps)
schirmer@13688:       ultimately
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     ultimately
schirmer@13688:     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.Try )
schirmer@13688:     thus ?case ..
schirmer@13688:   next
berghofe@21765:     case (Fin Env B c1 C1 c2 C2 A B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     obtain C1' where C1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Fin.hyps)
schirmer@13688:       with B'  
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain C2' where "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>c2\<rangle>" by (rule Fin.hyps)
schirmer@13688:       with B'
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     ultimately
schirmer@13688:     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.Fin )
schirmer@13688:     thus ?case ..
schirmer@13688:   next
nipkow@17589:     case Init thus ?case by (iprover intro: da.Init)
schirmer@13688:   next
nipkow@17589:     case NewC thus ?case by (iprover intro: da.NewC)
schirmer@13688:   next
nipkow@17589:     case NewA thus ?case by (iprover intro: da.NewA)
schirmer@13688:   next
nipkow@17589:     case Cast thus ?case by (iprover intro: da.Cast)
schirmer@13688:   next
nipkow@17589:     case Inst thus ?case by (iprover intro: da.Inst)
schirmer@13688:   next
nipkow@17589:     case Lit thus ?case by (iprover intro: da.Lit)
schirmer@13688:   next
nipkow@17589:     case UnOp thus ?case by (iprover intro: da.UnOp)
schirmer@13688:   next
berghofe@21765:     case (CondAnd Env B e1 E1 e2 E2 A B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondAnd.hyps)
wenzelm@23350:       with B'
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain E2' where "Env\<turnstile> B' \<union>  assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
schirmer@13688:     proof -
schirmer@13688:       from B' have "B \<union> assigns_if True e1 \<subseteq> B' \<union>  assigns_if True e1"
schirmer@13688: 	by blast
schirmer@13688:       moreover
schirmer@13688:       have "PROP ?Hyp Env (B \<union> assigns_if True e1) \<langle>e2\<rangle>" by (rule CondAnd.hyps)
nipkow@17589:       ultimately show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     ultimately
schirmer@13688:     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.CondAnd)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
berghofe@21765:     case (CondOr Env B e1 E1 e2 E2 A B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondOr.hyps)
schirmer@13688:       with B'  
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
schirmer@13688:     proof -
schirmer@13688:       from B' have "B \<union> assigns_if False e1 \<subseteq> B' \<union>  assigns_if False e1"
schirmer@13688: 	by blast
schirmer@13688:       moreover
schirmer@13688:       have "PROP ?Hyp Env (B \<union> assigns_if False e1) \<langle>e2\<rangle>" by (rule CondOr.hyps)
nipkow@17589:       ultimately show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     ultimately
schirmer@13688:     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.CondOr)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
berghofe@21765:     case (BinOp Env B e1 E1 e2 A binop B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule BinOp.hyps)
wenzelm@23350:       with B'
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"
schirmer@13688:     proof -
schirmer@13688:       have "Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" by (rule BinOp.hyps)
schirmer@13688:       from this B' E1'
schirmer@13688:       have "nrm E1 \<subseteq> nrm E1'"
schirmer@13688: 	by (rule da_monotone [THEN conjE])
schirmer@13688:       moreover 
schirmer@13688:       have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule BinOp.hyps)
nipkow@17589:       ultimately show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     ultimately
schirmer@13688:     have "Env\<turnstile> B' \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A'"
nipkow@17589:       using BinOp.hyps by (iprover intro: da.BinOp)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
schirmer@13688:     case (Super B Env B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
wenzelm@23350:     with Super.hyps have "This \<in> B'"
schirmer@13688:       by auto
nipkow@17589:     thus ?case by (iprover intro: da.Super)
schirmer@13688:   next
berghofe@21765:     case (AccLVar vn B A Env B')
wenzelm@23350:     note `vn \<in> B`
schirmer@13688:     moreover
wenzelm@23350:     note `B \<subseteq> B'`
schirmer@13688:     ultimately have "vn \<in> B'" by auto
nipkow@17589:     thus ?case by (iprover intro: da.AccLVar)
schirmer@13688:   next
nipkow@17589:     case Acc thus ?case by (iprover intro: da.Acc)
schirmer@13688:   next 
berghofe@21765:     case (AssLVar Env B e E A vn B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
nipkow@17589:       by (rule AssLVar.hyps [elim_format]) iprover
schirmer@13688:     then obtain A' where  
schirmer@13688:       "Env\<turnstile> B' \<guillemotright>\<langle>LVar vn:=e\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.AssLVar)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
berghofe@21765:     case (Ass v Env B V e A B') 
wenzelm@23350:     note B' = `B \<subseteq> B'`
wenzelm@23350:     note `\<forall>vn. v \<noteq> LVar vn`
schirmer@13688:     moreover
schirmer@13688:     obtain V' where V': "Env\<turnstile> B' \<guillemotright>\<langle>v\<rangle>\<guillemotright> V'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>v\<rangle>" by (rule Ass.hyps)
schirmer@13688:       with B'  
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain A' where "Env\<turnstile> nrm V' \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"
schirmer@13688:     proof -
schirmer@13688:       have "Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V" by (rule Ass.hyps)
schirmer@13688:       from this B' V'
schirmer@13688:       have "nrm V \<subseteq> nrm V'"
schirmer@13688: 	by (rule da_monotone [THEN conjE])
schirmer@13688:       moreover 
schirmer@13688:       have "PROP ?Hyp Env (nrm V) \<langle>e\<rangle>" by (rule Ass.hyps)
nipkow@17589:       ultimately show ?thesis using that by iprover
schirmer@13688:     qed  
schirmer@13688:     ultimately
schirmer@13688:     have "Env\<turnstile> B' \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.Ass)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
berghofe@21765:     case (CondBool Env c e1 e2 B C E1 E2 A B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
wenzelm@23350:     note `Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)`
schirmer@13688:     moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule CondBool.hyps)
schirmer@13688:       with B'  
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover 
schirmer@13688:     obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
schirmer@13688:     proof -
schirmer@13688:       from B'
schirmer@13688:       have "(B \<union> assigns_if True c) \<subseteq> (B' \<union> assigns_if True c)"
schirmer@13688: 	by blast
schirmer@13688:       moreover
schirmer@13688:       have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule CondBool.hyps)
schirmer@13688:       ultimately 
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
schirmer@13688:     proof -
schirmer@13688:       from B'
schirmer@13688:       have "(B \<union> assigns_if False c) \<subseteq> (B' \<union> assigns_if False c)"
schirmer@13688: 	by blast
schirmer@13688:       moreover
schirmer@13688:       have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by(rule CondBool.hyps)
schirmer@13688:       ultimately 
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     ultimately 
schirmer@13688:     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.CondBool)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
berghofe@21765:     case (Cond Env c e1 e2 B C E1 E2 A B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
wenzelm@23350:     note `\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)`
schirmer@13688:     moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule Cond.hyps)
schirmer@13688:       with B'  
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover 
schirmer@13688:     obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
schirmer@13688:     proof -
schirmer@13688:       from B'
schirmer@13688:       have "(B \<union> assigns_if True c) \<subseteq> (B' \<union> assigns_if True c)"
schirmer@13688: 	by blast
schirmer@13688:       moreover
schirmer@13688:       have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule Cond.hyps)
schirmer@13688:       ultimately 
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
schirmer@13688:     proof -
schirmer@13688:       from B'
schirmer@13688:       have "(B \<union> assigns_if False c) \<subseteq> (B' \<union> assigns_if False c)"
schirmer@13688: 	by blast
schirmer@13688:       moreover
schirmer@13688:       have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by (rule Cond.hyps)
schirmer@13688:       ultimately 
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     ultimately 
schirmer@13688:     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.Cond)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
berghofe@21765:     case (Call Env B e E args A accC statT mode mn pTs B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Call.hyps)
schirmer@13688:       with B'  
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'"
schirmer@13688:     proof -
schirmer@13688:       have "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" by (rule Call.hyps)
schirmer@13688:       from this B' E'
schirmer@13688:       have "nrm E \<subseteq> nrm E'"
schirmer@13688: 	by (rule da_monotone [THEN conjE])
schirmer@13688:       moreover 
schirmer@13688:       have "PROP ?Hyp Env (nrm E) \<langle>args\<rangle>" by (rule Call.hyps)
nipkow@17589:       ultimately show ?thesis using that by iprover
schirmer@13688:     qed  
schirmer@13688:     ultimately
schirmer@13688:     have "Env\<turnstile> B' \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs}args)\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.Call)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
nipkow@17589:     case Methd thus ?case by (iprover intro: da.Methd)
schirmer@13688:   next
berghofe@21765:     case (Body Env B c C A D B')  
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and nrm_C': "nrm C \<subseteq> nrm C'"
schirmer@13688:     proof -
schirmer@13688:       have "Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" by (rule Body.hyps)
schirmer@13688:       moreover note B'
schirmer@13688:       moreover
schirmer@13688:       from B' obtain C' where da_c: "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
schirmer@13688: 	by (rule Body.hyps [elim_format]) blast
schirmer@13688:       ultimately
schirmer@13688:       have "nrm C \<subseteq> nrm C'"
schirmer@13688: 	by (rule da_monotone [THEN conjE])
nipkow@17589:       with da_c that show ?thesis by iprover
schirmer@13688:     qed
schirmer@13688:     moreover 
wenzelm@23350:     note `Result \<in> nrm C`
schirmer@13688:     with nrm_C' have "Result \<in> nrm C'"
schirmer@13688:       by blast
wenzelm@23350:     moreover note `jumpNestingOkS {Ret} c`
schirmer@13688:     ultimately obtain A' where
schirmer@13688:       "Env\<turnstile> B' \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.Body)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
nipkow@17589:     case LVar thus ?case by (iprover intro: da.LVar)
schirmer@13688:   next
nipkow@17589:     case FVar thus ?case by (iprover intro: da.FVar)
schirmer@13688:   next
berghofe@21765:     case (AVar Env B e1 E1 e2 A B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule AVar.hyps)
wenzelm@23350:       with B'
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"
schirmer@13688:     proof -
schirmer@13688:       have "Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" by (rule AVar.hyps)
schirmer@13688:       from this B' E1'
schirmer@13688:       have "nrm E1 \<subseteq> nrm E1'"
schirmer@13688: 	by (rule da_monotone [THEN conjE])
schirmer@13688:       moreover 
schirmer@13688:       have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule AVar.hyps)
nipkow@17589:       ultimately show ?thesis using that by iprover
schirmer@13688:     qed  
schirmer@13688:     ultimately
schirmer@13688:     have "Env\<turnstile> B' \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.AVar)
schirmer@13688:     thus ?case ..
schirmer@13688:   next
nipkow@17589:     case Nil thus ?case by (iprover intro: da.Nil)
schirmer@13688:   next
berghofe@21765:     case (Cons Env B e E es A B')
wenzelm@23350:     note B' = `B \<subseteq> B'`
schirmer@13688:     obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
schirmer@13688:     proof -
schirmer@13688:       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Cons.hyps)
schirmer@13688:       with B'  
nipkow@17589:       show ?thesis using that by iprover
schirmer@13688:     qed
schirmer@13688:     moreover
schirmer@13688:     obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'"
schirmer@13688:     proof -
schirmer@13688:       have "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" by (rule Cons.hyps)
schirmer@13688:       from this B' E'
schirmer@13688:       have "nrm E \<subseteq> nrm E'"
schirmer@13688: 	by (rule da_monotone [THEN conjE])
schirmer@13688:       moreover 
schirmer@13688:       have "PROP ?Hyp Env (nrm E) \<langle>es\<rangle>" by (rule Cons.hyps)
nipkow@17589:       ultimately show ?thesis using that by iprover
schirmer@13688:     qed  
schirmer@13688:     ultimately
schirmer@13688:     have "Env\<turnstile> B' \<guillemotright>\<langle>e # es\<rangle>\<guillemotright> A'"
nipkow@17589:       by (iprover intro: da.Cons)
schirmer@13688:     thus ?case ..
schirmer@13688:   qed
wenzelm@23350: qed (rule `B \<subseteq> B'`)
schirmer@13688: 
schirmer@13688: (* Remarks about the proof style:
schirmer@13688: 
schirmer@13688:    "by (rule <Case>.hyps)" vs "."
schirmer@13688:    --------------------------
schirmer@13688:   
schirmer@13688:    with <Case>.hyps you state more precise were the rule comes from
schirmer@13688: 
schirmer@13688:    . takes all assumptions into account, but looks more "light"
schirmer@13688:    and is more resistent for cut and paste proof in different 
schirmer@13688:    cases.
schirmer@13688: 
schirmer@13688:   "intro: da.intros" vs "da.<Case>"
schirmer@13688:   ---------------------------------
schirmer@13688:   The first ist more convinient for cut and paste between cases,
schirmer@13688:   the second is more informativ for the reader
schirmer@13688: *)
schirmer@13688: 
schirmer@13688: corollary da_weakenE [consumes 2]:
schirmer@13688:   assumes          da: "Env\<turnstile> B  \<guillemotright>t\<guillemotright> A"   and
schirmer@13688:                    B': "B \<subseteq> B'"          and
schirmer@13688:               ex_mono: "\<And> A'.  \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; nrm A \<subseteq> nrm A'; 
schirmer@13688:                                \<And> l. brk A l \<subseteq> brk A' l\<rbrakk> \<Longrightarrow> P" 
schirmer@13688:   shows "P"
schirmer@13688: proof -
schirmer@13688:   from da B'
schirmer@13688:   obtain A' where A': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'"
nipkow@17589:     by (rule da_weaken [elim_format]) iprover
schirmer@13688:   with da B'
schirmer@13688:   have "nrm A \<subseteq> nrm A' \<and> (\<forall> l. brk A l \<subseteq> brk A' l)"
schirmer@13688:     by (rule da_monotone)
schirmer@13688:   with A' ex_mono
schirmer@13688:   show ?thesis
nipkow@17589:     by iprover
schirmer@13688: qed
schirmer@13688: 
nipkow@17589: end