src/HOL/Bali/TypeSafe.thy
changeset 14030 cd928c0ac225
parent 13690 ac335b2f4a39
child 14700 2f885b7e5ba7
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Wed May 14 15:22:37 2003 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Wed May 14 20:29:18 2003 +0200
     1.3 @@ -1230,54 +1230,23 @@
     1.4    case Nil thus ?case by simp
     1.5  next
     1.6    case (Cons x xs tab tab' ys)
     1.7 -  have "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z"
     1.8 -    by (rule Cons.hyps) (rule map_upd_cong_ext)
     1.9 -  thus ?case
    1.10 -    by simp
    1.11 +  note Hyps = this
    1.12 +  show ?case
    1.13 +  proof (cases ys)
    1.14 +    case Nil
    1.15 +    thus ?thesis by simp
    1.16 +  next
    1.17 +    case (Cons y ys')
    1.18 +    have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
    1.19 +      by (rules intro: Hyps map_upd_cong_ext)
    1.20 +    with Cons show ?thesis
    1.21 +      by simp
    1.22 +  qed
    1.23  qed
    1.24     
    1.25  lemma map_upd_override: "(tab(x\<mapsto>y)) x = (tab'(x\<mapsto>y)) x"
    1.26    by simp
    1.27  
    1.28 -
    1.29 -lemma map_upds_override_cong:
    1.30 -"\<And> tab tab' zs. x\<in> set ws \<Longrightarrow> 
    1.31 - (tab(ws[\<mapsto>]zs)) x = (tab'(ws[\<mapsto>]zs)) x"
    1.32 -proof (induct ws)
    1.33 -  case Nil thus ?case by simp
    1.34 -next
    1.35 -  case (Cons w ws tab tab' zs)
    1.36 -  have x: "x \<in> set (w#ws)" .
    1.37 -  show ?case
    1.38 -  proof (cases "x=w")
    1.39 -    case True thus ?thesis
    1.40 -      by simp (rule map_upds_cong_ext, rule map_upd_override)
    1.41 -  next
    1.42 -    case False
    1.43 -    with x have "x \<in> set ws"
    1.44 -      by simp
    1.45 -    with Cons.hyps show ?thesis
    1.46 -      by simp
    1.47 -  qed
    1.48 -qed
    1.49 -
    1.50 -lemma map_upds_in_suffix: assumes x: "x \<in> set xs" 
    1.51 - shows "\<And> tab qs. (tab(ps @ xs[\<mapsto>]qs)) x = (tab(xs[\<mapsto>]drop (length ps) qs)) x"
    1.52 -proof (induct ps)
    1.53 -  case Nil thus ?case by simp
    1.54 -next
    1.55 -  case (Cons p ps tab qs)
    1.56 -  have "(tab(p\<mapsto>hd qs)(ps @ xs[\<mapsto>](tl qs))) x
    1.57 -          =(tab(p\<mapsto>hd qs)(xs[\<mapsto>]drop (length ps) (tl qs))) x"
    1.58 -    by (rule Cons.hyps)
    1.59 -  moreover
    1.60 -  have "drop (Suc (length ps)) qs=drop (length ps) (tl qs)"
    1.61 -    by (cases qs) simp+
    1.62 -  ultimately show ?case
    1.63 -    by simp (rule map_upds_override_cong)
    1.64 -qed
    1.65 - 
    1.66 -
    1.67  lemma map_upds_eq_length_suffix: "\<And> tab qs. 
    1.68          length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
    1.69  proof (induct ps)
    1.70 @@ -1327,13 +1296,21 @@
    1.71    case Nil thus ?case by simp
    1.72  next
    1.73    case (Cons x xs tab ys z)
    1.74 -  have "tab vn = Some z" .
    1.75 -  then obtain z' where "(tab(x\<mapsto>hd ys)) vn = Some z'" 
    1.76 -    by (rule map_upd_Some_expand [of tab,elim_format]) blast
    1.77 -  hence "\<exists> z. (tab (x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
    1.78 -    by (rule Cons.hyps)
    1.79 -  thus ?case
    1.80 -    by simp
    1.81 +  have z: "tab vn = Some z" .
    1.82 +  show ?case
    1.83 +  proof (cases ys)
    1.84 +    case Nil
    1.85 +    with z show ?thesis by simp
    1.86 +  next
    1.87 +    case (Cons y ys')
    1.88 +    have ys: "ys = y#ys'".
    1.89 +    from z obtain z' where "(tab(x\<mapsto>y)) vn = Some z'"
    1.90 +      by (rule map_upd_Some_expand [of tab,elim_format]) blast
    1.91 +    hence "\<exists>z. ((tab(x\<mapsto>y))(xs[\<mapsto>]ys')) vn = Some z"
    1.92 +      by (rule Cons.hyps)
    1.93 +    with ys show ?thesis
    1.94 +      by simp
    1.95 +  qed
    1.96  qed
    1.97  
    1.98  
    1.99 @@ -1349,22 +1326,6 @@
   1.100  lemma map_eq_upd_eq: "tab vn = tab' vn \<Longrightarrow> (tab(x\<mapsto>y)) vn = (tab'(x\<mapsto>y)) vn"
   1.101  by (simp add: fun_upd_def)
   1.102  
   1.103 -lemma map_eq_upds_eq: 
   1.104 -  "\<And> tab tab' ys. 
   1.105 -   tab vn = tab' vn \<Longrightarrow> (tab(xs[\<mapsto>]ys)) vn = (tab'(xs[\<mapsto>]ys)) vn"
   1.106 -proof (induct xs)
   1.107 -  case Nil thus ?case by simp 
   1.108 -next
   1.109 -  case (Cons x xs tab tab' ys)
   1.110 -  have "tab vn = tab' vn" .
   1.111 -  hence "(tab(x\<mapsto>hd ys)) vn = (tab'(x\<mapsto>hd ys)) vn"
   1.112 -    by (rule map_eq_upd_eq)
   1.113 -  hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
   1.114 -    by (rule Cons.hyps)
   1.115 -  thus ?case 
   1.116 -    by simp
   1.117 -qed
   1.118 -
   1.119  lemma map_upd_in_expansion_map_swap:
   1.120   "\<lbrakk>(tab(x\<mapsto>y)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
   1.121                   \<Longrightarrow>  (tab'(x\<mapsto>y)) vn = Some z"
   1.122 @@ -1377,32 +1338,37 @@
   1.123    case Nil thus ?case by simp
   1.124  next
   1.125    case (Cons x xs tab tab' ys z)
   1.126 -  from Cons.prems obtain 
   1.127 -    some: "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z" and
   1.128 -    tab_not_z: "tab vn \<noteq> Some z"
   1.129 -    by simp
   1.130 +  have some: "(tab(x # xs[\<mapsto>]ys)) vn = Some z" .
   1.131 +  have tab_not_z: "tab vn \<noteq> Some z".
   1.132    show ?case
   1.133 -  proof (cases "(tab(x\<mapsto>hd ys)) vn \<noteq> Some z")
   1.134 -    case True
   1.135 -    with some have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
   1.136 -      by (rule Cons.hyps)
   1.137 -    thus ?thesis 
   1.138 -      by simp
   1.139 +  proof (cases "ys")
   1.140 +    case Nil with some tab_not_z show ?thesis by simp
   1.141    next
   1.142 -    case False
   1.143 -    hence tabx_z: "(tab(x\<mapsto>hd ys)) vn = Some z" by blast
   1.144 -    moreover
   1.145 -    from tabx_z tab_not_z
   1.146 -    have "(tab'(x\<mapsto>hd ys)) vn = Some z" 
   1.147 -      by (rule map_upd_in_expansion_map_swap)
   1.148 -    ultimately
   1.149 -    have "(tab(x\<mapsto>hd ys)) vn =(tab'(x\<mapsto>hd ys)) vn"
   1.150 -      by simp
   1.151 -    hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
   1.152 -      by (rule map_eq_upds_eq)
   1.153 -    with some 
   1.154 -    show ?thesis 
   1.155 -      by simp
   1.156 +    case (Cons y tl)
   1.157 +    have ys: "ys = y#tl".
   1.158 +    show ?thesis
   1.159 +    proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
   1.160 +      case True
   1.161 +      with some ys have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = Some z"
   1.162 +	by (fastsimp intro: Cons.hyps)
   1.163 +      with ys show ?thesis 
   1.164 +	by simp
   1.165 +    next
   1.166 +      case False
   1.167 +      hence tabx_z: "(tab(x\<mapsto>y)) vn = Some z" by blast
   1.168 +      moreover
   1.169 +      from tabx_z tab_not_z
   1.170 +      have "(tab'(x\<mapsto>y)) vn = Some z" 
   1.171 +	by (rule map_upd_in_expansion_map_swap)
   1.172 +      ultimately
   1.173 +      have "(tab(x\<mapsto>y)) vn =(tab'(x\<mapsto>y)) vn"
   1.174 +	by simp
   1.175 +      hence "(tab(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn"
   1.176 +	by (rule map_upds_cong_ext)
   1.177 +      with some ys
   1.178 +      show ?thesis 
   1.179 +	by simp
   1.180 +    qed
   1.181    qed
   1.182  qed
   1.183     
   1.184 @@ -1464,17 +1430,28 @@
   1.185    case Nil thus ?case by simp
   1.186  next
   1.187    case (Cons x xs tab tab' ys)
   1.188 -  from Cons.prems
   1.189 -  have "(tab(x\<mapsto>hd ys)) vn = Some el"
   1.190 -    by - (rule Cons.hyps,auto)
   1.191 -  moreover from Cons.prems 
   1.192 -  have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = None" 
   1.193 -    by simp
   1.194 -  hence "(tab'(x\<mapsto>hd ys)) vn = None"
   1.195 -    by (rule map_upds_None_cut)
   1.196 -  ultimately show "tab vn = Some el" 
   1.197 -    by (rule map_upd_cut_irrelevant)
   1.198 +  have tab_vn: "(tab(x # xs[\<mapsto>]ys)) vn = Some el".
   1.199 +  have tab'_vn: "(tab'(x # xs[\<mapsto>]ys)) vn = None".
   1.200 +  show ?case
   1.201 +  proof (cases ys)
   1.202 +    case Nil
   1.203 +    with tab_vn show ?thesis by simp
   1.204 +  next
   1.205 +    case (Cons y tl)
   1.206 +    have ys: "ys=y#tl".
   1.207 +    with tab_vn tab'_vn 
   1.208 +    have "(tab(x\<mapsto>y)) vn = Some el"
   1.209 +      by - (rule Cons.hyps,auto)
   1.210 +    moreover from tab'_vn ys
   1.211 +    have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = None" 
   1.212 +      by simp
   1.213 +    hence "(tab'(x\<mapsto>y)) vn = None"
   1.214 +      by (rule map_upds_None_cut)
   1.215 +    ultimately show "tab vn = Some el" 
   1.216 +      by (rule map_upd_cut_irrelevant)
   1.217 +  qed
   1.218  qed
   1.219 +
   1.220     
   1.221  lemma dom_vname_split:
   1.222   "dom (lname_case (ename_case (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
   1.223 @@ -1531,22 +1508,30 @@
   1.224  lemma dom_map_upd: "\<And> tab. dom (tab(x\<mapsto>y)) = dom tab \<union> {x}"
   1.225  by (auto simp add: dom_def fun_upd_def)
   1.226  
   1.227 -lemma dom_map_upds: "\<And> tab ys. dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
   1.228 +lemma dom_map_upds: "\<And> tab ys. length xs = length ys 
   1.229 +  \<Longrightarrow> dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
   1.230  proof (induct xs)
   1.231    case Nil thus ?case by (simp add: dom_def)
   1.232  next
   1.233    case (Cons x xs tab ys)
   1.234 -  have "dom (tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) = dom (tab(x\<mapsto>hd ys)) \<union> set xs" .
   1.235 -  moreover 
   1.236 -  have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
   1.237 -    by (rule dom_map_upd)
   1.238 -  ultimately
   1.239 +  note Hyp = Cons.hyps
   1.240 +  have len: "length (x#xs)=length ys".
   1.241    show ?case
   1.242 -    by simp
   1.243 +  proof (cases ys)
   1.244 +    case Nil with len show ?thesis by simp
   1.245 +  next
   1.246 +    case (Cons y tl)
   1.247 +    with len have "dom (tab(x\<mapsto>y)(xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
   1.248 +      by - (rule Hyp,simp)
   1.249 +    moreover 
   1.250 +    have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
   1.251 +      by (rule dom_map_upd)
   1.252 +    ultimately
   1.253 +    show ?thesis using Cons
   1.254 +      by simp
   1.255 +  qed
   1.256  qed
   1.257   
   1.258 -
   1.259 -
   1.260  lemma dom_ename_case_None_simp:
   1.261   "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)"
   1.262    apply (auto simp add: dom_def image_def )
   1.263 @@ -1583,14 +1568,17 @@
   1.264   "f ` g ` A = (f \<circ> g) ` A"
   1.265  by (auto simp add: image_def)
   1.266  
   1.267 +
   1.268  lemma dom_locals_init_lvars: 
   1.269    assumes m: "m=(mthd (the (methd G C sig)))"  
   1.270 +  assumes len: "length (pars m) = length pvs"
   1.271    shows "dom (locals (store (init_lvars G C sig (invmode m e) a pvs s)))  
   1.272             = parameters m"
   1.273  proof -
   1.274    from m
   1.275    have static_m': "is_static m = static m"
   1.276      by simp
   1.277 +  from len
   1.278    have dom_vnames: "dom (empty(pars m[\<mapsto>]pvs))=set (pars m)"
   1.279      by (simp add: dom_map_upds)
   1.280    show ?thesis
   1.281 @@ -1609,6 +1597,7 @@
   1.282    qed
   1.283  qed
   1.284  
   1.285 +
   1.286  lemma da_e2_BinOp:
   1.287    assumes da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.288                    \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A"
   1.289 @@ -3283,10 +3272,25 @@
   1.290  	      from is_static_eq 
   1.291  	      have "(invmode (mthd dynM) e) = (invmode statM e)"
   1.292  		by (simp add: invmode_def)
   1.293 -	      with init_lvars dynM' is_static_eq normal_s2 mode 
   1.294 +	      moreover
   1.295 +	      have "length (pars (mthd dynM)) = length vs" 
   1.296 +	      proof -
   1.297 +		from normal_s2 conf_args
   1.298 +		have "length vs = length pTs"
   1.299 +		  by (simp add: list_all2_def)
   1.300 +		also from pTs_widen
   1.301 +		have "\<dots> = length pTs'"
   1.302 +		  by (simp add: widens_def list_all2_def)
   1.303 +		also from wf_dynM
   1.304 +		have "\<dots> = length (pars (mthd dynM))"
   1.305 +		  by (simp add: wf_mdecl_def wf_mhead_def)
   1.306 +		finally show ?thesis ..
   1.307 +	      qed
   1.308 +	      moreover note init_lvars dynM' is_static_eq normal_s2 mode 
   1.309 +	      ultimately
   1.310  	      have "parameters (mthd dynM) = dom (locals (store s3))"
   1.311  		using dom_locals_init_lvars 
   1.312 -                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" e a vs s2]
   1.313 +                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" vs e a s2]
   1.314  		by simp
   1.315  	      also from check
   1.316  	      have "dom (locals (store s3)) \<subseteq>  dom (locals (store s3'))"