src/HOL/MicroJava/Comp/CorrCompTp.thy
author ballarin
Fri Aug 29 15:19:02 2003 +0200 (2003-08-29)
changeset 14174 f3cafd2929d5
parent 14045 a34d89ce6097
child 14981 e73f8140af78
permissions -rw-r--r--
Methods rule_tac etc support static (Isar) contexts.
     1 (*  Title:      HOL/MicroJava/Comp/CorrCompTp.thy
     2     ID:         $Id$
     3     Author:     Martin Strecker
     4     Copyright   GPL 2002
     5 *)
     6 
     7 theory CorrCompTp =  LemmasComp + JVM + TypeInf + Altern:
     8 
     9 declare split_paired_All [simp del]
    10 declare split_paired_Ex [simp del]
    11 
    12 
    13 (**********************************************************************)
    14 
    15 constdefs     
    16    inited_LT :: "[cname, ty list, (vname \<times> ty) list] \<Rightarrow> locvars_type"
    17   "inited_LT C pTs lvars == (OK (Class C))#((map OK pTs))@(map (Fun.comp OK snd) lvars)"
    18    is_inited_LT :: "[cname, ty list, (vname \<times> ty) list, locvars_type] \<Rightarrow> bool"
    19   "is_inited_LT C pTs lvars LT == (LT = (inited_LT C pTs lvars))"
    20 
    21   local_env :: "[java_mb prog, cname, sig, vname list,(vname \<times> ty) list] \<Rightarrow> java_mb env"
    22   "local_env G C S pns lvars == 
    23      let (mn, pTs) = S in (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C))"
    24 
    25 lemma local_env_fst [simp]: "fst (local_env G C S pns lvars) = G"
    26 by (simp add: local_env_def split_beta)
    27 
    28 
    29 lemma wt_class_expr_is_class: "\<lbrakk> ws_prog G; E \<turnstile> expr :: Class cname;
    30   E = local_env G C (mn, pTs) pns lvars\<rbrakk>
    31   \<Longrightarrow> is_class G cname "
    32 apply (subgoal_tac "((fst E), (snd E)) \<turnstile> expr :: Class cname")
    33 apply (frule ty_expr_is_type) apply simp
    34 apply simp apply (simp (no_asm_use))
    35 done
    36 
    37 
    38 
    39 (********************************************************************************)
    40 section "index"
    41 
    42 lemma local_env_snd: "
    43   snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)"
    44 by (simp add: local_env_def)
    45 
    46 
    47 
    48 lemma index_in_bounds: " length pns = length pTs \<Longrightarrow>
    49   snd (local_env G C (mn, pTs) pns lvars) vname = Some T
    50        \<Longrightarrow> index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)"
    51 apply (simp add: local_env_snd index_def split_beta)
    52 apply (case_tac "vname = This")
    53 apply (simp add: inited_LT_def)
    54 apply simp
    55 apply (drule map_of_upds_SomeD)
    56 apply (drule length_takeWhile)
    57 apply (simp add: inited_LT_def)
    58 done
    59 
    60 
    61 lemma map_upds_append [rule_format (no_asm)]: 
    62   "\<forall> x1s m. (length k1s = length x1s 
    63   \<longrightarrow> m(k1s[\<mapsto>]x1s)(k2s[\<mapsto>]x2s) = m ((k1s@k2s)[\<mapsto>](x1s@x2s)))"
    64 apply (induct k1s)
    65 apply simp
    66 apply (intro strip)
    67 apply (subgoal_tac "\<exists> x xr. x1s = x # xr")
    68 apply clarify
    69 apply simp
    70   (* subgoal *)
    71 apply (case_tac x1s)
    72 apply auto
    73 done
    74 
    75 
    76 lemma map_of_append [rule_format]: 
    77   "\<forall> ys. (map_of ((rev xs) @ ys) = (map_of ys) ((map fst xs) [\<mapsto>] (map snd xs)))"
    78 apply (induct xs)
    79 apply simp
    80 apply (rule allI)
    81 apply (drule_tac x="a # ys" in spec)
    82 apply (simp only: rev.simps append_assoc append_Cons append_Nil
    83   map.simps map_of.simps map_upds_Cons hd.simps tl.simps)
    84 done
    85 
    86 lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))"
    87 by (rule map_of_append [of _ "[]", simplified])
    88 
    89 lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs"
    90 apply (induct xs)
    91 apply simp
    92 apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym]
    93                  Map.map_of_append[symmetric] del:Map.map_of_append)
    94 done
    95 
    96 lemma map_upds_rev [rule_format]: "\<forall> xs. (distinct ks \<longrightarrow> length ks = length xs 
    97   \<longrightarrow> m (rev ks [\<mapsto>] rev xs) = m (ks [\<mapsto>] xs))"
    98 apply (induct ks)
    99 apply simp
   100 apply (intro strip)
   101 apply (subgoal_tac "\<exists> x xr. xs = x # xr")
   102 apply clarify
   103 apply (drule_tac x=xr in spec)
   104 apply (simp add: map_upds_append [THEN sym])
   105   (* subgoal *)
   106 apply (case_tac xs)
   107 apply auto
   108 done
   109 
   110 lemma map_upds_takeWhile [rule_format]:
   111   "\<forall> ks. (empty(rev ks[\<mapsto>]rev xs)) k = Some x \<longrightarrow> length ks = length xs \<longrightarrow>
   112     xs ! length (takeWhile (\<lambda>z. z \<noteq> k) ks) = x"
   113 apply (induct xs)
   114 apply simp
   115 apply (intro strip)
   116 apply (subgoal_tac "\<exists> k' kr. ks = k' # kr")
   117 apply (clarify)
   118 apply (drule_tac x=kr in spec)
   119 apply (simp only: rev.simps)
   120 apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev list @ [a])) = empty (rev kr[\<mapsto>]rev list)([k'][\<mapsto>][a])")
   121 apply (simp only:)
   122 apply (case_tac "k' = k")
   123 apply simp
   124 apply simp 
   125 apply (case_tac "k = k'")
   126 apply simp
   127 apply (simp add: empty_def)
   128 apply (simp add: map_upds_append [THEN sym])
   129 apply (case_tac ks)
   130 apply auto
   131 done
   132 
   133 
   134 lemma local_env_inited_LT: "\<lbrakk> snd (local_env G C (mn, pTs) pns lvars) vname = Some T;
   135   length pns = length pTs; distinct pns; unique lvars \<rbrakk>
   136   \<Longrightarrow> (inited_LT C pTs lvars ! index (pns, lvars, blk, res) vname) = OK T"
   137 apply (simp add: local_env_snd index_def)
   138 apply (case_tac "vname = This")
   139 apply (simp add: inited_LT_def)
   140 apply (simp add: inited_LT_def)
   141 apply (simp (no_asm_simp) only: map_compose map_append [THEN sym] map.simps [THEN sym])
   142 apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)")
   143 apply (simp (no_asm_simp) only: List.nth_map ok_val.simps)
   144 apply (subgoal_tac "map_of lvars = map_of (map (\<lambda> p. (fst p, snd p)) lvars)")
   145 apply (simp only:)
   146 apply (subgoal_tac "distinct (map fst lvars)") 
   147 apply (frule_tac g=snd in AuxLemmas.map_of_map_as_map_upd)
   148 apply (simp only:)
   149 apply (simp add: map_upds_append)
   150 apply (frule map_upds_SomeD)
   151 apply (rule map_upds_takeWhile)
   152 apply (simp (no_asm_simp))
   153 apply (simp add: map_upds_append [THEN sym])
   154 apply (simp add: map_upds_rev)
   155 
   156   (* show length (pns @ map fst lvars) = length (pTs @ map snd lvars) *)
   157 apply simp
   158 
   159   (* show distinct (map fst lvars) *)
   160 apply (simp only: unique_def Fun.comp_def)
   161 
   162   (* show map_of lvars = map_of (map (\<lambda>p. (fst p, snd p)) lvars) *)
   163 apply simp
   164 
   165   (* show length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars) *)
   166 apply (drule map_of_upds_SomeD)
   167 apply (drule length_takeWhile)
   168 apply simp
   169 done
   170 
   171 
   172 lemma inited_LT_at_index_no_err: " i < length (inited_LT C pTs lvars)
   173   \<Longrightarrow> inited_LT C pTs lvars ! i \<noteq> Err"
   174 apply (simp only: inited_LT_def)
   175 apply (simp only: map_compose map_append [THEN sym] map.simps [THEN sym] length_map)
   176 apply (simp only: nth_map)
   177 apply simp
   178 done
   179 
   180 
   181 lemma sup_loc_update_index: "
   182   \<lbrakk> G \<turnstile> T \<preceq> T'; is_type G T'; length pns = length pTs; distinct pns; unique lvars;
   183   snd (local_env G C (mn, pTs) pns lvars) vname = Some T' \<rbrakk>
   184   \<Longrightarrow> 
   185   comp G \<turnstile> 
   186   inited_LT C pTs lvars [index (pns, lvars, blk, res) vname := OK T] <=l 
   187   inited_LT C pTs lvars"
   188 apply (subgoal_tac " index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)")
   189 apply (frule_tac blk=blk and res=res in local_env_inited_LT, assumption+)
   190 apply (rule sup_loc_trans)
   191 apply (rule_tac b="OK T'" in sup_loc_update)
   192 apply (simp add: comp_widen) 
   193 apply assumption
   194 apply (rule sup_loc_refl)
   195 apply (simp add: list_update_same_conv [THEN iffD2])
   196   (* subgoal *)
   197 apply (rule index_in_bounds)
   198 apply simp+
   199 done
   200 
   201 
   202 (********************************************************************************)
   203 
   204 section "Preservation of ST and LT by compTpExpr / compTpStmt"
   205 
   206 lemma sttp_of_comb_nil [simp]: "sttp_of (comb_nil sttp) = sttp"
   207 by (simp add: comb_nil_def)
   208 
   209 lemma mt_of_comb_nil [simp]: "mt_of (comb_nil sttp) = []"
   210 by (simp add: comb_nil_def)
   211 
   212 
   213 lemma sttp_of_comb [simp]: "sttp_of ((f1 \<box> f2) sttp) = sttp_of (f2 (sttp_of (f1 sttp)))"
   214 apply (case_tac "f1 sttp")
   215 apply (case_tac "(f2 (sttp_of (f1 sttp)))")
   216 apply (simp add: comb_def)
   217 done
   218 
   219 lemma mt_of_comb: "(mt_of ((f1 \<box> f2) sttp)) = 
   220   (mt_of (f1 sttp)) @ (mt_of (f2 (sttp_of (f1 sttp))))"
   221 by (simp add: comb_def split_beta)
   222 
   223 
   224 lemma mt_of_comb_length [simp]: "\<lbrakk> n1 = length (mt_of (f1 sttp)); n1 \<le> n \<rbrakk>
   225   \<Longrightarrow> (mt_of ((f1 \<box> f2) sttp) ! n) = (mt_of (f2 (sttp_of (f1 sttp))) ! (n - n1))"
   226 by (simp add: comb_def nth_append split_beta)
   227 
   228 
   229 lemma compTpExpr_Exprs_LT_ST: "
   230   \<lbrakk>jmb = (pns, lvars, blk, res); 
   231   wf_prog wf_java_mdecl G;
   232   wf_java_mdecl G C ((mn, pTs), rT, jmb);
   233   E = local_env G C (mn, pTs) pns lvars \<rbrakk>
   234  \<Longrightarrow> 
   235   (\<forall> ST LT T. 
   236   E \<turnstile> ex :: T \<longrightarrow>
   237   is_inited_LT C pTs lvars LT \<longrightarrow>
   238   sttp_of (compTpExpr jmb G ex (ST, LT)) = (T # ST, LT))
   239  \<and>
   240  (\<forall> ST LT Ts. 
   241   E \<turnstile> exs [::] Ts \<longrightarrow>
   242   is_inited_LT C pTs lvars LT \<longrightarrow>
   243   sttp_of (compTpExprs jmb G exs (ST, LT)) = ((rev Ts) @ ST, LT))"
   244 
   245 apply (rule expr.induct)
   246 
   247 (* expresssions *)
   248 
   249 (* NewC *) 
   250 apply (intro strip)
   251 apply (drule NewC_invers)
   252 apply (simp add: pushST_def)
   253 
   254 (* Cast *)
   255 apply (intro strip)
   256 apply (drule Cast_invers, clarify)
   257 apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
   258 apply (simp add: replST_def split_beta)
   259 
   260 (* Lit *)
   261 apply (intro strip)
   262 apply (drule Lit_invers)
   263 apply (simp add: pushST_def)
   264 
   265 (* BinOp *)
   266 apply (intro strip)
   267 apply (drule BinOp_invers, clarify)
   268 apply (drule_tac x=ST in spec)
   269 apply (drule_tac x="Ta # ST" in spec)
   270 apply ((drule spec)+, (drule mp, assumption)+)
   271   apply (case_tac binop)
   272   apply (simp (no_asm_simp))
   273     apply (simp (no_asm_simp) add: popST_def pushST_def)
   274   apply (simp)
   275     apply (simp (no_asm_simp) add: replST_def)
   276 
   277 
   278 (* LAcc *)
   279 apply (intro strip)
   280 apply (drule LAcc_invers)
   281 apply (simp add: pushST_def is_inited_LT_def)
   282 apply (simp add: wf_prog_def)
   283 apply (frule wf_java_mdecl_disjoint_varnames) 
   284   apply (simp add: disjoint_varnames_def)
   285 apply (frule wf_java_mdecl_length_pTs_pns)
   286 apply (erule conjE)+
   287 apply (simp (no_asm_simp) add: local_env_inited_LT)
   288 
   289 (* LAss *)
   290 apply (intro strip)
   291 apply (drule LAss_invers, clarify)
   292 apply (drule LAcc_invers)
   293 apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
   294 apply (simp add: popST_def dupST_def)
   295 
   296 (* FAcc *)
   297 apply (intro strip)
   298 apply (drule FAcc_invers, clarify)
   299 apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
   300 apply (simp add: replST_def)
   301 
   302   (* show   snd (the (field (G, cname) vname)) = T *)
   303   apply (subgoal_tac "is_class G Ca")
   304   apply (subgoal_tac "is_class G cname \<and> field (G, cname) vname = Some (cname, T)")
   305   apply simp
   306 
   307   (* show is_class G cname \<and> field (G, cname) vname = Some (cname, T) *)
   308   apply (rule field_in_fd) apply assumption+
   309   (* show is_class G Ca *)
   310   apply (fast intro: wt_class_expr_is_class)
   311 
   312 (* FAss *)
   313 apply (intro strip)
   314 apply (drule FAss_invers, clarify)
   315 apply (drule FAcc_invers, clarify)
   316 apply (drule_tac x=ST in spec)
   317 apply (drule_tac x="Class Ca # ST" in spec)
   318 apply ((drule spec)+, (drule mp, assumption)+)
   319 apply (simp add: popST_def dup_x1ST_def)
   320 
   321 
   322 (* Call *)
   323 apply (intro strip)
   324 apply (drule Call_invers, clarify)
   325 apply (drule_tac x=ST in spec)
   326 apply (drule_tac x="Class cname # ST" in spec)
   327 apply ((drule spec)+, (drule mp, assumption)+)
   328 apply (simp add: replST_def)
   329 
   330 
   331 (* expression lists *)
   332 (* nil *) 
   333 
   334 apply (intro strip)
   335 apply (drule Nil_invers)
   336 apply (simp add: comb_nil_def)
   337 
   338 (* cons *)
   339 
   340 apply (intro strip)
   341 apply (drule Cons_invers, clarify)
   342 apply (drule_tac x=ST in spec)
   343 apply (drule_tac x="T # ST" in spec)
   344 apply ((drule spec)+, (drule mp, assumption)+)
   345 apply simp
   346 
   347 done
   348 
   349 
   350 
   351 lemmas compTpExpr_LT_ST [rule_format (no_asm)] = 
   352   compTpExpr_Exprs_LT_ST [THEN conjunct1]
   353 
   354 lemmas compTpExprs_LT_ST [rule_format (no_asm)] = 
   355   compTpExpr_Exprs_LT_ST [THEN conjunct2]
   356 
   357 lemma compTpStmt_LT_ST [rule_format (no_asm)]: "
   358   \<lbrakk> jmb = (pns,lvars,blk,res); 
   359   wf_prog wf_java_mdecl G;
   360   wf_java_mdecl G C ((mn, pTs), rT, jmb);
   361   E = (local_env G C (mn, pTs) pns lvars)\<rbrakk> 
   362 \<Longrightarrow> (\<forall> ST LT.
   363   E \<turnstile> s\<surd> \<longrightarrow>
   364   (is_inited_LT C pTs lvars LT)
   365 \<longrightarrow> sttp_of (compTpStmt jmb G s (ST, LT)) = (ST, LT))"
   366 
   367 apply (rule stmt.induct)
   368 
   369 (* Skip *) 
   370 apply (intro strip)
   371 apply simp
   372 
   373 (* Expr *)
   374 apply (intro strip)
   375 apply (drule Expr_invers, erule exE)
   376 apply (simp (no_asm_simp) add: compTpExpr_LT_ST)
   377 apply (frule_tac ST=ST in compTpExpr_LT_ST, assumption+)
   378 apply (simp add: popST_def)
   379 
   380 (* Comp *)
   381 apply (intro strip)
   382 apply (drule Comp_invers, clarify)
   383 apply (simp (no_asm_use))
   384 apply simp
   385 
   386 (* Cond *)
   387 apply (intro strip)
   388 apply (drule Cond_invers)
   389 apply (erule conjE)+
   390 apply (drule_tac x=ST in spec)
   391 apply (drule_tac x=ST in spec)
   392 apply (drule spec)+ apply (drule mp, assumption)+
   393 apply (drule_tac ST="PrimT Boolean # ST" in compTpExpr_LT_ST, assumption+)
   394 apply (simp add: popST_def pushST_def nochangeST_def)
   395 
   396 (* Loop *)
   397 apply (intro strip)
   398 apply (drule Loop_invers)
   399 apply (erule conjE)+
   400 apply (drule_tac x=ST in spec)
   401 apply (drule spec)+ apply (drule mp, assumption)+
   402 apply (drule_tac ST="PrimT Boolean # ST" in compTpExpr_LT_ST, assumption+)
   403 apply (simp add: popST_def pushST_def nochangeST_def)
   404 done
   405 
   406 
   407 
   408 lemma compTpInit_LT_ST: "
   409   sttp_of (compTpInit jmb (vn,ty) (ST, LT)) = (ST, LT[(index jmb vn):= OK ty])"
   410 by (simp add: compTpInit_def storeST_def pushST_def)
   411 
   412 
   413 lemma compTpInitLvars_LT_ST_aux [rule_format (no_asm)]:
   414   "\<forall> pre lvars_pre lvars0.
   415   jmb = (pns,lvars0,blk,res) \<and>
   416   lvars0 = (lvars_pre @ lvars) \<and>
   417   (length pns) + (length lvars_pre) + 1 = length pre \<and>
   418   disjoint_varnames pns (lvars_pre @ lvars)
   419   \<longrightarrow>
   420 sttp_of (compTpInitLvars jmb lvars (ST, pre @ replicate (length lvars) Err))
   421     = (ST, pre @ map (Fun.comp OK snd) lvars)"
   422 apply (induct lvars)
   423 apply simp
   424 
   425 apply (intro strip)
   426 apply (subgoal_tac "\<exists> vn ty. a = (vn, ty)")
   427   prefer 2 apply (simp (no_asm_simp)) 
   428   apply ((erule exE)+, simp (no_asm_simp))
   429 
   430 apply (drule_tac x="pre @ [OK ty]" in spec)
   431 apply (drule_tac x="lvars_pre @ [a]" in spec)
   432 apply (drule_tac x="lvars0" in spec)
   433 apply (simp add: compTpInit_LT_ST index_of_var2)
   434 done
   435 
   436 lemma compTpInitLvars_LT_ST: 
   437   "\<lbrakk> jmb = (pns, lvars, blk, res); wf_java_mdecl G C ((mn, pTs), rT, jmb) \<rbrakk>
   438 \<Longrightarrow>(sttp_of (compTpInitLvars jmb lvars (ST, start_LT C pTs (length lvars))))
   439   = (ST, inited_LT C pTs lvars)"
   440 apply (simp add: start_LT_def inited_LT_def)
   441 apply (simp only: append_Cons [THEN sym])
   442 apply (rule compTpInitLvars_LT_ST_aux)
   443 apply (auto dest: wf_java_mdecl_length_pTs_pns wf_java_mdecl_disjoint_varnames)
   444 done
   445 
   446 
   447 
   448 (********************************************************************************)
   449 
   450 lemma max_of_list_elem: "x \<in> set xs \<Longrightarrow> x \<le> (max_of_list xs)"
   451 by (induct xs, auto intro: le_maxI1 simp: le_max_iff_disj max_of_list_def)
   452 
   453 lemma max_of_list_sublist: "set xs \<subseteq> set ys 
   454   \<Longrightarrow> (max_of_list xs) \<le> (max_of_list ys)"
   455 by (induct xs, auto dest: max_of_list_elem simp: max_of_list_def)
   456 
   457 lemma max_of_list_append [simp]:
   458   "max_of_list (xs @ ys) = max (max_of_list xs) (max_of_list ys)" 
   459 apply (simp add: max_of_list_def)
   460 apply (induct xs)
   461 apply simp
   462 apply simp
   463 apply arith
   464 done
   465 
   466 
   467 lemma app_mono_mxs: "\<lbrakk> app i G mxs rT pc et s; mxs \<le> mxs' \<rbrakk> 
   468   \<Longrightarrow> app i G mxs' rT pc et s"
   469 apply (case_tac s)
   470 apply (simp add: app_def)
   471 apply (case_tac i)
   472 apply (auto intro: less_trans)
   473 done
   474 
   475 
   476 
   477 lemma err_mono [simp]: "A \<subseteq> B \<Longrightarrow> err A \<subseteq> err B"
   478 by (auto simp: err_def)
   479 
   480 lemma opt_mono [simp]: "A \<subseteq> B \<Longrightarrow> opt A \<subseteq> opt B"
   481 by (auto simp: opt_def)
   482 
   483 
   484 lemma states_mono: "\<lbrakk> mxs \<le> mxs' \<rbrakk>
   485   \<Longrightarrow> states G mxs mxr \<subseteq> states G mxs' mxr"
   486 apply (simp add: states_def JVMType.sl_def)
   487 apply (simp add: Product.esl_def stk_esl_def reg_sl_def 
   488   upto_esl_def Listn.sl_def Err.sl_def  JType.esl_def)
   489 apply (simp add: Err.esl_def Err.le_def Listn.le_def)
   490 apply (simp add: Product.le_def Product.sup_def Err.sup_def)
   491 apply (simp add: Opt.esl_def Listn.sup_def)
   492 apply (rule err_mono)
   493 apply (rule opt_mono)
   494 apply (rule Sigma_mono)
   495 apply (rule Union_mono)
   496 apply auto 
   497 done
   498 
   499 
   500 lemma check_type_mono: "\<lbrakk> check_type G mxs mxr s; mxs \<le> mxs' \<rbrakk> 
   501   \<Longrightarrow> check_type G mxs' mxr s"
   502 apply (simp add: check_type_def)
   503 apply (frule_tac G=G and mxr=mxr in states_mono)
   504 apply auto
   505 done
   506 
   507 
   508   (* wt is preserved when adding instructions/state-types at the end *)
   509 lemma wt_instr_prefix: "
   510  \<lbrakk> wt_instr_altern (bc ! pc) cG rT mt mxs mxr max_pc et pc; 
   511   bc' = bc @ bc_post; mt' = mt @ mt_post; 
   512   mxs \<le> mxs'; max_pc \<le> max_pc'; 
   513   pc < length bc; pc < length mt; 
   514   max_pc = (length mt)\<rbrakk>
   515 \<Longrightarrow> wt_instr_altern (bc' ! pc) cG rT mt' mxs' mxr max_pc' et pc"
   516 apply (simp add: wt_instr_altern_def nth_append)
   517 apply (auto intro: app_mono_mxs check_type_mono)
   518 done
   519 
   520 
   521 (************************************************************************)
   522 
   523 
   524 
   525 lemma pc_succs_shift: "pc'\<in>set (succs i (pc'' + n))
   526  \<Longrightarrow> ((pc' - n) \<in>set (succs i pc''))"
   527 apply (induct i)
   528 apply simp+
   529   (* case Goto *)
   530 apply arith
   531   (* case Ifcmpeq *)
   532 apply simp
   533 apply (erule disjE)
   534 apply arith
   535 apply arith
   536   (* case Throw *)
   537 apply simp
   538 done
   539 
   540 
   541 lemma pc_succs_le: "\<lbrakk> pc' \<in> set (succs i (pc'' + n));   
   542   \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc'' + b)) \<rbrakk> 
   543   \<Longrightarrow> n \<le> pc'"
   544 apply (induct i)
   545 apply simp+
   546   (* case Goto *)
   547 apply arith
   548   (* case Ifcmpeq *)
   549 apply simp
   550 apply (erule disjE)
   551 apply simp
   552 apply arith
   553   (* case Throw *)
   554 apply simp
   555 done
   556 
   557 
   558 (**********************************************************************)
   559 
   560 constdefs
   561   offset_xcentry :: "[nat, exception_entry] \<Rightarrow> exception_entry"
   562   "offset_xcentry == 
   563       \<lambda> n (start_pc, end_pc, handler_pc, catch_type).
   564           (start_pc + n, end_pc + n, handler_pc + n, catch_type)"
   565 
   566   offset_xctable :: "[nat, exception_table] \<Rightarrow> exception_table"
   567   "offset_xctable n == (map (offset_xcentry n))"
   568 
   569 lemma match_xcentry_offset [simp]: "
   570   match_exception_entry G cn (pc + n) (offset_xcentry n ee) = 
   571   match_exception_entry G cn pc ee"
   572 by (simp add: match_exception_entry_def offset_xcentry_def split_beta)
   573 
   574 lemma match_xctable_offset: "
   575   (match_exception_table G cn (pc + n) (offset_xctable n et)) =
   576   (option_map (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
   577 apply (induct et)
   578 apply (simp add: offset_xctable_def)+
   579 apply (case_tac "match_exception_entry G cn pc a")
   580 apply (simp add: offset_xcentry_def split_beta)+
   581 done
   582 
   583 
   584 lemma match_offset [simp]: "
   585   match G cn (pc + n) (offset_xctable n et) = match G cn pc et"
   586 apply (induct et)
   587 apply (simp add: offset_xctable_def)+
   588 done
   589 
   590 lemma match_any_offset [simp]: "
   591   match_any G (pc + n) (offset_xctable n et) = match_any G pc et"
   592 apply (induct et)
   593 apply (simp add: offset_xctable_def offset_xcentry_def split_beta)+
   594 done
   595 
   596 lemma app_mono_pc: "\<lbrakk> app i G mxs rT pc et s; pc'= pc + n \<rbrakk> 
   597   \<Longrightarrow> app i G mxs rT pc' (offset_xctable n et) s"
   598 apply (case_tac s)
   599 apply (simp add: app_def)
   600 apply (case_tac i)
   601 apply (auto)
   602 done
   603 
   604 (**********************************************************************)
   605 
   606   (* Currently: empty exception_table *)
   607 
   608 syntax
   609   empty_et :: exception_table
   610 translations
   611   "empty_et" => "[]"
   612 
   613 
   614 
   615   (* move into Effect.thy *)
   616 lemma xcpt_names_Nil [simp]: "(xcpt_names (i, G, pc, [])) = []"
   617 by (induct i, simp_all)
   618 
   619 lemma xcpt_eff_Nil [simp]: "(xcpt_eff i G pc s []) = []"
   620 by (simp add: xcpt_eff_def)
   621 
   622 
   623 lemma app_jumps_lem: "\<lbrakk> app i cG mxs rT pc empty_et s; s=(Some st) \<rbrakk>
   624   \<Longrightarrow>  \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc + b))"
   625 apply (simp only:)
   626 apply (induct i)
   627 apply auto
   628 done
   629 
   630 
   631 (* wt is preserved when adding instructions/state-types to the front *)
   632 lemma wt_instr_offset: "
   633  \<lbrakk> \<forall> pc'' < length mt. 
   634     wt_instr_altern ((bc@bc_post) ! pc'') cG rT (mt@mt_post) mxs mxr max_pc empty_et pc''; 
   635   bc' = bc_pre @ bc @ bc_post; mt' = mt_pre @ mt @ mt_post; 
   636   length bc_pre = length mt_pre; length bc = length mt;
   637   length mt_pre \<le> pc; pc < length (mt_pre @ mt); 
   638   mxs \<le> mxs'; max_pc + length mt_pre \<le> max_pc' \<rbrakk>
   639 \<Longrightarrow> wt_instr_altern (bc' ! pc) cG rT mt' mxs' mxr max_pc' empty_et pc"
   640 
   641 apply (simp add: wt_instr_altern_def)
   642 apply (subgoal_tac "\<exists> pc''. pc = pc'' + length mt_pre", erule exE)
   643 prefer 2 apply (rule_tac x="pc - length mt_pre" in exI, arith)
   644 
   645 apply (drule_tac x=pc'' in spec)
   646 apply (drule mp) apply arith	(* show pc'' < length mt *)
   647 apply clarify
   648 
   649 apply (rule conjI)
   650   (* app *)
   651   apply (simp add: nth_append)
   652   apply (rule app_mono_mxs)
   653   apply (frule app_mono_pc) apply (rule HOL.refl) apply (simp add: offset_xctable_def)
   654   apply assumption+
   655 
   656   (* check_type *)
   657 apply (rule conjI)
   658 apply (simp add: nth_append)
   659 apply (rule  check_type_mono) apply assumption+
   660 
   661   (* ..eff.. *)
   662 apply (intro ballI)
   663 apply (subgoal_tac "\<exists> pc' s'. x = (pc', s')", (erule exE)+, simp)
   664 
   665 apply (case_tac s')
   666   (* s' = None *)
   667 apply (simp add: eff_def nth_append norm_eff_def)
   668 apply (frule_tac x="(pc', None)" and  f=fst and b=pc' in rev_image_eqI) 
   669   apply (simp (no_asm_simp))
   670   apply (simp only: fst_conv image_compose [THEN sym] Fun.comp_def)
   671   apply simp
   672   apply (frule pc_succs_shift)
   673 apply (drule bspec, assumption)
   674 apply arith
   675 
   676   (* s' = Some a *)
   677 apply (drule_tac x="(pc' - length mt_pre, s')" in bspec)
   678 
   679   (* show  (pc' - length mt_pre, s') \<in> set (eff \<dots>) *)
   680 apply (simp add: eff_def)
   681     (* norm_eff *)
   682   apply (clarsimp simp: nth_append pc_succs_shift)
   683 
   684   (* show P x of bspec *)
   685 apply simp
   686   apply (subgoal_tac "length mt_pre \<le> pc'")
   687   apply (simp add: nth_append) apply arith
   688 
   689   (* subgoals *)
   690 apply (simp add: eff_def xcpt_eff_def)
   691 apply (clarsimp)
   692 apply (rule pc_succs_le) apply assumption+
   693 apply (subgoal_tac "\<exists> st. mt ! pc'' = Some st", erule exE)
   694  apply (rule_tac s="Some st" and st=st and cG=cG and mxs=mxs and rT=rT
   695         in app_jumps_lem)
   696   apply (simp add: nth_append)+
   697     (* subgoal \<exists> st. mt ! pc'' = Some st *)
   698   apply (simp add: norm_eff_def option_map_def nth_append)
   699   apply (case_tac "mt ! pc''")
   700 apply simp+
   701 done
   702 
   703 
   704 (**********************************************************************)
   705 
   706 
   707 constdefs
   708   start_sttp_resp_cons :: "[state_type \<Rightarrow> method_type \<times> state_type] \<Rightarrow> bool"
   709   "start_sttp_resp_cons f == 
   710      (\<forall> sttp. let (mt', sttp') = (f sttp) in (\<exists>mt'_rest. mt' = Some sttp # mt'_rest))"
   711 
   712   start_sttp_resp :: "[state_type \<Rightarrow> method_type \<times> state_type] \<Rightarrow> bool"
   713   "start_sttp_resp f == (f = comb_nil) \<or> (start_sttp_resp_cons f)"
   714 
   715 lemma start_sttp_resp_comb_nil [simp]: "start_sttp_resp comb_nil"
   716 by (simp add: start_sttp_resp_def)
   717 
   718 lemma start_sttp_resp_cons_comb_cons [simp]: "start_sttp_resp_cons f 
   719   \<Longrightarrow> start_sttp_resp_cons (f \<box> f')"
   720 apply (simp add: start_sttp_resp_cons_def comb_def split_beta)
   721 apply (rule allI)
   722 apply (drule_tac x=sttp in spec)
   723 apply auto
   724 done
   725 
   726 lemma start_sttp_resp_cons_comb_cons_r: "\<lbrakk> start_sttp_resp f; start_sttp_resp_cons f'\<rbrakk>
   727   \<Longrightarrow> start_sttp_resp_cons (f \<box> f')"
   728 apply (simp add: start_sttp_resp_def)
   729 apply (erule disjE)
   730 apply simp+
   731 done
   732 
   733 lemma start_sttp_resp_cons_comb [simp]: "start_sttp_resp_cons f 
   734   \<Longrightarrow> start_sttp_resp (f \<box> f')"
   735 by (simp add: start_sttp_resp_def)
   736 
   737 lemma start_sttp_resp_comb: "\<lbrakk> start_sttp_resp f; start_sttp_resp f' \<rbrakk>
   738   \<Longrightarrow> start_sttp_resp (f \<box> f')"
   739 apply (simp add: start_sttp_resp_def)
   740 apply (erule disjE)
   741 apply simp
   742 apply (erule disjE)
   743 apply simp+
   744 done
   745 
   746 lemma start_sttp_resp_cons_nochangeST [simp]: "start_sttp_resp_cons nochangeST"
   747 by (simp add: start_sttp_resp_cons_def nochangeST_def)
   748 
   749 lemma start_sttp_resp_cons_pushST [simp]: "start_sttp_resp_cons (pushST Ts)"
   750 by (simp add: start_sttp_resp_cons_def pushST_def split_beta)
   751 
   752 lemma start_sttp_resp_cons_dupST [simp]: "start_sttp_resp_cons dupST"
   753 by (simp add: start_sttp_resp_cons_def dupST_def split_beta)
   754 
   755 lemma start_sttp_resp_cons_dup_x1ST [simp]: "start_sttp_resp_cons dup_x1ST"
   756 by (simp add: start_sttp_resp_cons_def dup_x1ST_def split_beta)
   757 
   758 lemma start_sttp_resp_cons_popST [simp]: "start_sttp_resp_cons (popST n)"
   759 by (simp add: start_sttp_resp_cons_def popST_def split_beta)
   760 
   761 lemma start_sttp_resp_cons_replST [simp]: "start_sttp_resp_cons (replST n tp)"
   762 by (simp add: start_sttp_resp_cons_def replST_def split_beta)
   763 
   764 lemma start_sttp_resp_cons_storeST [simp]: "start_sttp_resp_cons (storeST i tp)"
   765 by (simp add: start_sttp_resp_cons_def storeST_def split_beta)
   766 
   767 lemma start_sttp_resp_cons_compTpExpr [simp]: "start_sttp_resp_cons (compTpExpr jmb G ex)"
   768 apply (induct ex)
   769 apply simp+
   770 apply (simp add: start_sttp_resp_cons_def comb_def pushST_def split_beta) (* LAcc *)
   771 apply simp+
   772 done
   773 
   774 lemma start_sttp_resp_cons_compTpInit [simp]: "start_sttp_resp_cons (compTpInit jmb lv)"
   775 by (simp add: compTpInit_def split_beta)
   776 
   777 
   778 lemma start_sttp_resp_nochangeST [simp]: "start_sttp_resp nochangeST"
   779 by (simp add: start_sttp_resp_def)
   780 
   781 lemma start_sttp_resp_pushST [simp]: "start_sttp_resp (pushST Ts)"
   782 by (simp add: start_sttp_resp_def)
   783 
   784 lemma start_sttp_resp_dupST [simp]: "start_sttp_resp dupST"
   785 by (simp add: start_sttp_resp_def)
   786 
   787 lemma start_sttp_resp_dup_x1ST [simp]: "start_sttp_resp dup_x1ST"
   788 by (simp add: start_sttp_resp_def)
   789 
   790 lemma start_sttp_resp_popST [simp]: "start_sttp_resp (popST n)"
   791 by (simp add: start_sttp_resp_def)
   792 
   793 lemma start_sttp_resp_replST [simp]: "start_sttp_resp (replST n tp)"
   794 by (simp add: start_sttp_resp_def)
   795 
   796 lemma start_sttp_resp_storeST [simp]: "start_sttp_resp (storeST i tp)"
   797 by (simp add: start_sttp_resp_def)
   798 
   799 lemma start_sttp_resp_compTpExpr [simp]: "start_sttp_resp (compTpExpr jmb G ex)"
   800 by (simp add: start_sttp_resp_def)
   801 
   802 lemma start_sttp_resp_compTpExprs [simp]: "start_sttp_resp (compTpExprs jmb G exs)"
   803 by (induct exs, (simp add: start_sttp_resp_comb)+)
   804 
   805 lemma start_sttp_resp_compTpStmt [simp]: "start_sttp_resp (compTpStmt jmb G s)"
   806 by (induct s, (simp add: start_sttp_resp_comb)+)
   807 
   808 lemma start_sttp_resp_compTpInitLvars [simp]: "start_sttp_resp (compTpInitLvars jmb lvars)"
   809 by (induct lvars, simp+)
   810 
   811 
   812 
   813 
   814   (* ********************************************************************** *)
   815 section "length of compExpr/ compTpExprs"
   816   (* ********************************************************************** *)
   817 
   818 lemma length_comb [simp]:  "length (mt_of ((f1 \<box> f2) sttp)) = 
   819   length (mt_of (f1 sttp)) + length (mt_of (f2 (sttp_of (f1 sttp))))"
   820 by (simp add: comb_def split_beta)
   821 
   822 
   823 lemma length_comb_nil [simp]: "length (mt_of (comb_nil sttp)) = 0"
   824 by (simp add: comb_nil_def)
   825 
   826 lemma length_nochangeST [simp]: "length (mt_of (nochangeST sttp)) = 1"
   827 by (simp add: nochangeST_def)
   828 
   829 lemma length_pushST [simp]: "length (mt_of (pushST Ts sttp)) = 1"
   830 by (simp add: pushST_def split_beta)
   831 
   832 lemma length_dupST [simp]: "length (mt_of (dupST sttp)) = 1"
   833 by (simp add: dupST_def split_beta)
   834 
   835 lemma length_dup_x1ST [simp]: "length (mt_of (dup_x1ST sttp)) = 1"
   836 by (simp add: dup_x1ST_def split_beta)
   837 
   838 lemma length_popST [simp]: "length (mt_of (popST n sttp)) = 1"
   839 by (simp add: popST_def split_beta)
   840 
   841 lemma length_replST [simp]: "length (mt_of (replST n tp sttp)) = 1"
   842 by (simp add: replST_def split_beta)
   843 
   844 lemma length_storeST [simp]: "length (mt_of (storeST i tp sttp)) = 1"
   845 by (simp add: storeST_def split_beta)
   846 
   847 
   848 lemma length_compTpExpr_Exprs [rule_format]: "
   849   (\<forall> sttp. (length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)))
   850   \<and> (\<forall> sttp. (length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)))"
   851 apply (rule  expr.induct)
   852 apply simp+
   853 apply (case_tac binop)
   854 apply simp+
   855 apply (simp add: pushST_def split_beta)
   856 apply simp+
   857 done
   858 
   859 lemma length_compTpExpr: "length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)"
   860 by (rule length_compTpExpr_Exprs [THEN conjunct1 [THEN spec]])
   861 
   862 lemma length_compTpExprs: "length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)"
   863 by (rule length_compTpExpr_Exprs [THEN conjunct2 [THEN spec]])
   864 
   865 lemma length_compTpStmt [rule_format]: "
   866   (\<forall> sttp. (length (mt_of (compTpStmt jmb G s sttp)) = length (compStmt jmb s)))"
   867 apply (rule stmt.induct)
   868 apply (simp add: length_compTpExpr)+
   869 done
   870 
   871 
   872 lemma length_compTpInit: "length (mt_of (compTpInit jmb lv sttp)) = length (compInit jmb lv)"
   873 by (simp add: compTpInit_def compInit_def split_beta)
   874 
   875 lemma length_compTpInitLvars [rule_format]: 
   876   "\<forall> sttp. length (mt_of (compTpInitLvars jmb lvars sttp)) = length (compInitLvars jmb lvars)"
   877 by (induct lvars,  (simp add: compInitLvars_def length_compTpInit split_beta)+)
   878 
   879 
   880   (* ********************************************************************** *)
   881 section "Correspondence bytecode - method types"
   882   (* ********************************************************************** *)
   883 
   884 syntax
   885   ST_of :: "state_type \<Rightarrow> opstack_type"
   886   LT_of :: "state_type \<Rightarrow> locvars_type"
   887 translations
   888   "ST_of" => "fst"
   889   "LT_of" => "snd"
   890 
   891 lemma states_lower:
   892   "\<lbrakk> OK (Some (ST, LT)) \<in> states cG mxs mxr; length ST \<le> mxs\<rbrakk>
   893   \<Longrightarrow> OK (Some (ST, LT)) \<in> states cG (length ST) mxr"
   894 apply (simp add: states_def JVMType.sl_def)
   895 apply (simp add: Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
   896   JType.esl_def)
   897 apply (simp add: Err.esl_def Err.le_def Listn.le_def)
   898 apply (simp add: Product.le_def Product.sup_def Err.sup_def)
   899 apply (simp add: Opt.esl_def Listn.sup_def)
   900 apply clarify
   901 apply auto
   902 done
   903 
   904 lemma check_type_lower:
   905   "\<lbrakk> check_type cG mxs mxr (OK (Some (ST, LT))); length ST \<le> mxs\<rbrakk>
   906   \<Longrightarrow>check_type cG (length ST) mxr (OK (Some (ST, LT)))"
   907 by (simp add: check_type_def states_lower)
   908 
   909 lemma max_same_iter [simp]: "max (x::'a::linorder) (max x y) = max x y"
   910 by (simp del: max_assoc add: max_assoc [THEN sym])
   911 
   912   (* ******************************************************************* *)
   913 
   914 constdefs
   915    bc_mt_corresp :: "
   916   [bytecode, state_type \<Rightarrow> method_type \<times> state_type, state_type, jvm_prog, ty, nat, p_count]
   917   \<Rightarrow> bool"
   918 
   919   "bc_mt_corresp bc f sttp0 cG rT mxr idx ==
   920   let (mt, sttp) = f sttp0 in
   921   (length bc = length mt \<and> 
   922     ((check_type cG (length (ST_of sttp0)) mxr (OK (Some sttp0))) \<longrightarrow>
   923     (\<forall>  mxs. 
   924      mxs = max_ssize (mt@[Some sttp]) \<longrightarrow>
   925      (\<forall> pc. pc < idx \<longrightarrow> 
   926       wt_instr_altern (bc ! pc) cG rT (mt@[Some sttp]) mxs mxr (length mt + 1) empty_et pc)
   927      \<and> 
   928      check_type cG mxs mxr (OK ((mt@[Some sttp]) ! idx)))))"
   929 
   930 
   931 lemma bc_mt_corresp_comb: "
   932   \<lbrakk> bc' = (bc1@bc2); l' = (length bc');
   933   bc_mt_corresp bc1 f1 sttp0 cG rT mxr (length bc1);
   934   bc_mt_corresp bc2 f2 (sttp_of (f1 sttp0)) cG rT mxr (length bc2);
   935   start_sttp_resp f2\<rbrakk>
   936 \<Longrightarrow> bc_mt_corresp bc' (f1 \<box> f2) sttp0 cG rT mxr l'"
   937 apply (subgoal_tac "\<exists> mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
   938 apply (subgoal_tac "\<exists> mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
   939 
   940   (* unfold start_sttp_resp and make case distinction *)
   941 apply (simp only: start_sttp_resp_def)
   942 apply (erule disjE)
   943   (* case f2 = comb_nil *)
   944 apply (simp add: bc_mt_corresp_def comb_nil_def start_sttp_resp_cons_def)
   945 apply (erule conjE)+
   946 apply (intro strip)
   947 apply simp
   948 
   949   (* case start_sttp_resp_cons f2 *)
   950 apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def del: all_simps)
   951 apply (intro strip)
   952 apply (erule conjE)+
   953 apply (drule mp, assumption)
   954 apply (subgoal_tac "check_type cG (length (fst sttp1)) mxr (OK (Some sttp1))")
   955 apply (erule conjE)+
   956 apply (drule mp, assumption)
   957 apply (erule conjE)+
   958 
   959 apply (rule conjI)
   960   (* show wt_instr  \<dots> *)
   961 
   962 apply (drule_tac x=sttp1 in spec, simp)
   963 apply (erule exE)
   964 apply (intro strip)
   965 apply (case_tac "pc < length mt1")
   966 
   967   (* case pc < length mt1 *)
   968 apply (drule spec, drule mp, simp)
   969 apply simp 
   970 apply (rule_tac mt="mt1 @ [Some sttp1]" in wt_instr_prefix)
   971   apply assumption+ apply (rule HOL.refl)
   972   apply (simp (no_asm_simp))
   973   apply (simp (no_asm_simp) add: max_ssize_def)
   974   apply (simp add: max_of_list_def max_ac)
   975   apply arith
   976   apply (simp (no_asm_simp))+
   977 
   978   (* case pc \<ge> length mt1 *)
   979 apply (rule_tac bc=bc2 and mt=mt2 and bc_post="[]" and mt_post="[Some sttp2]" 
   980   and mxr=mxr 
   981   in wt_instr_offset)
   982 apply simp
   983 apply (simp (no_asm_simp))+
   984 apply simp
   985 apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def)
   986 apply (simp (no_asm_simp))+
   987 
   988   (* show check_type \<dots> *)
   989 apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
   990 apply (simp only:)
   991 apply (rule check_type_mono) apply assumption
   992 apply (simp (no_asm_simp)  add: max_ssize_def max_of_list_append max_ac)
   993 apply arith
   994 apply (simp add: nth_append)
   995 
   996 apply (erule conjE)+
   997 apply (case_tac sttp1)
   998 apply (simp add: check_type_def)
   999 apply (rule states_lower, assumption)
  1000 apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append)
  1001 apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def max_def)
  1002 apply (simp (no_asm_simp))+
  1003 done
  1004 
  1005 
  1006 lemma bc_mt_corresp_zero [simp]: "\<lbrakk> length (mt_of (f sttp)) = length bc; start_sttp_resp f\<rbrakk>
  1007   \<Longrightarrow> bc_mt_corresp bc f sttp cG rT mxr 0"
  1008 apply (simp add: bc_mt_corresp_def start_sttp_resp_def split_beta)
  1009 apply (erule disjE)
  1010 apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split_beta)
  1011 apply (intro strip)
  1012 apply (simp add: start_sttp_resp_cons_def split_beta)
  1013 apply (drule_tac x=sttp in spec, erule exE)
  1014 apply simp
  1015 apply (rule check_type_mono, assumption)
  1016 apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def split_beta)
  1017 done
  1018 
  1019   (* ********************************************************************** *)
  1020 
  1021 
  1022 constdefs
  1023   mt_sttp_flatten :: "method_type \<times> state_type \<Rightarrow> method_type"
  1024   "mt_sttp_flatten mt_sttp == (mt_of mt_sttp) @ [Some (sttp_of mt_sttp)]"
  1025 
  1026 
  1027 lemma mt_sttp_flatten_length [simp]: "n = (length (mt_of (f sttp)))
  1028  \<Longrightarrow> (mt_sttp_flatten (f sttp)) ! n = Some (sttp_of (f sttp))"
  1029 by (simp add: mt_sttp_flatten_def)
  1030 
  1031 lemma mt_sttp_flatten_comb: "(mt_sttp_flatten ((f1 \<box> f2) sttp)) = 
  1032   (mt_of (f1 sttp)) @ (mt_sttp_flatten (f2 (sttp_of (f1 sttp))))"
  1033 by (simp add: mt_sttp_flatten_def comb_def split_beta)
  1034 
  1035 lemma mt_sttp_flatten_comb_length [simp]: "\<lbrakk> n1 = length (mt_of (f1 sttp)); n1 \<le> n \<rbrakk>
  1036   \<Longrightarrow> (mt_sttp_flatten ((f1 \<box> f2) sttp) ! n) = (mt_sttp_flatten (f2 (sttp_of (f1 sttp))) ! (n - n1))"
  1037 by (simp add: mt_sttp_flatten_comb nth_append)
  1038 
  1039 lemma mt_sttp_flatten_comb_zero [simp]: "start_sttp_resp f 
  1040   \<Longrightarrow> (mt_sttp_flatten (f sttp)) ! 0 = Some sttp"
  1041 apply (simp only: start_sttp_resp_def)
  1042 apply (erule disjE)
  1043 apply (simp add: comb_nil_def mt_sttp_flatten_def)
  1044 apply (simp add: start_sttp_resp_cons_def mt_sttp_flatten_def split_beta)
  1045 apply (drule_tac x=sttp in spec)
  1046 apply (erule exE)
  1047 apply simp
  1048 done
  1049 
  1050 
  1051 (* move into prelude -- compare with nat_int_length *)
  1052 lemma int_outside_right: "0 \<le> (m::int) \<Longrightarrow> m + (int n) = int ((nat m) + n)"
  1053 by simp
  1054 
  1055 lemma int_outside_left: "0 \<le> (m::int) \<Longrightarrow> (int n) + m = int (n + (nat m))"
  1056 by simp
  1057 
  1058 
  1059 
  1060 
  1061   (* ********************************************************************** *)
  1062   (* bc_mt_corresp for individual instructions                              *)
  1063   (* ---------------------------------------------------------------------- *)
  1064 
  1065 lemma less_Suc [simp] : "n \<le> k \<Longrightarrow> (k < Suc n) = (k = n)"
  1066   by arith
  1067 
  1068 lemmas check_type_simps = check_type_def states_def JVMType.sl_def
  1069    Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
  1070   JType.esl_def Err.esl_def Err.le_def Listn.le_def Product.le_def Product.sup_def Err.sup_def
  1071   Opt.esl_def Listn.sup_def
  1072 
  1073 
  1074 lemma check_type_push: "\<lbrakk> 
  1075   is_class cG cname; check_type cG (length ST) mxr (OK (Some (ST, LT))) \<rbrakk>
  1076   \<Longrightarrow> check_type cG (Suc (length ST)) mxr (OK (Some (Class cname # ST, LT)))"
  1077 apply (simp add: check_type_simps)
  1078 apply clarify
  1079 apply (rule_tac x="Suc (length ST)" in exI)
  1080 apply simp+
  1081 done
  1082 
  1083 lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
  1084   \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
  1085 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
  1086     max_ssize_def max_of_list_def ssize_sto_def max_def 
  1087     eff_def norm_eff_def)
  1088 apply (intro strip)
  1089 apply (rule conjI)
  1090 apply (rule check_type_mono, assumption, simp)
  1091 apply (simp add: check_type_push)
  1092 done
  1093 
  1094 lemma bc_mt_corresp_Pop: "
  1095   bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
  1096   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
  1097   apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
  1098   apply (simp add: max_def)
  1099   apply (simp add: check_type_simps)
  1100   apply clarify
  1101   apply (rule_tac x="(length ST)" in exI)
  1102   apply simp+
  1103   done
  1104 
  1105 lemma bc_mt_corresp_Checkcast: "\<lbrakk> is_class cG cname; sttp = (ST, LT); 
  1106   (\<exists>rT STo. ST = RefT rT # STo) \<rbrakk>
  1107   \<Longrightarrow> bc_mt_corresp [Checkcast cname] (replST (Suc 0) (Class cname)) sttp cG rT mxr (Suc 0)"
  1108   apply (erule exE)+
  1109   apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
  1110   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
  1111   apply (simp add: check_type_simps)
  1112   apply clarify
  1113   apply (rule_tac x="Suc (length STo)" in exI)
  1114   apply simp+
  1115   done
  1116 
  1117 
  1118 lemma bc_mt_corresp_LitPush: "\<lbrakk> typeof (\<lambda>v. None) val = Some T \<rbrakk>
  1119   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
  1120 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
  1121   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
  1122                  max_ssize_def max_of_list_def ssize_sto_def max_def
  1123                  eff_def norm_eff_def)
  1124   apply (intro strip)
  1125   apply (rule conjI)
  1126   apply (rule check_type_mono, assumption, simp)
  1127   apply (simp add: check_type_simps)
  1128 apply clarify
  1129 apply (rule_tac x="Suc (length ST)" in exI)
  1130 apply simp
  1131 apply (drule sym)
  1132 apply (case_tac val)
  1133 apply simp+
  1134 done
  1135 
  1136 
  1137 lemma bc_mt_corresp_LitPush_CT: "\<lbrakk> typeof (\<lambda>v. None) val = Some T \<and> cG \<turnstile> T \<preceq> T';
  1138   is_type cG T' \<rbrakk>
  1139   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
  1140 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
  1141   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
  1142                  max_ssize_def max_of_list_def ssize_sto_def max_def
  1143                  eff_def norm_eff_def)
  1144   apply (intro strip)
  1145   apply (rule conjI)
  1146   apply (rule check_type_mono, assumption, simp)
  1147   apply (simp add: check_type_simps)
  1148   apply (simp add: sup_state_Cons)
  1149 apply clarify
  1150 apply (rule_tac x="Suc (length ST)" in exI)
  1151 apply simp
  1152 apply simp+
  1153 done
  1154 
  1155 lemma bc_mt_corresp_Load: "\<lbrakk> i < length LT; LT ! i \<noteq> Err; mxr = length LT \<rbrakk>
  1156   \<Longrightarrow> bc_mt_corresp [Load i] 
  1157          (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
  1158 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
  1159                  max_ssize_def max_of_list_def ssize_sto_def max_def
  1160                  eff_def norm_eff_def)
  1161   apply (intro strip)
  1162   apply (rule conjI)
  1163   apply (rule check_type_mono, assumption, simp)
  1164 apply (simp add: check_type_simps)
  1165 apply clarify
  1166 apply (rule_tac x="Suc (length ST)" in exI)
  1167 apply (simp (no_asm_simp))
  1168   apply (simp only: err_def)
  1169   apply (frule listE_nth_in) apply assumption
  1170 apply (subgoal_tac "LT ! i \<in> {x. \<exists>y\<in>types cG. x = OK y}")
  1171 apply (drule CollectD) apply (erule bexE)
  1172 apply (simp (no_asm_simp) )
  1173 apply blast
  1174 apply blast
  1175 done
  1176 
  1177 
  1178 lemma bc_mt_corresp_Store_init: "\<lbrakk> i < length LT \<rbrakk>
  1179   \<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
  1180  apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
  1181   apply (simp add: max_ssize_def  max_of_list_def )
  1182   apply (simp add: ssize_sto_def) apply (simp add: max_def)
  1183   apply (intro strip)
  1184 apply (simp add: check_type_simps)
  1185 apply clarify
  1186 apply (rule conjI)
  1187 apply (rule_tac x="(length ST)" in exI)
  1188 apply simp+
  1189 done
  1190 
  1191 
  1192 
  1193 lemma bc_mt_corresp_Store: "\<lbrakk> i < length LT; cG  \<turnstile>  LT[i := OK T] <=l LT \<rbrakk>
  1194   \<Longrightarrow> bc_mt_corresp [Store i] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
  1195   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
  1196   apply (simp add: sup_state_conv)
  1197   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  1198   apply (simp add: max_def)
  1199  apply (intro strip)
  1200 apply (simp add: check_type_simps)
  1201 apply clarify
  1202 apply (rule_tac x="(length ST)" in exI)
  1203 apply simp+
  1204 done
  1205 
  1206 
  1207 lemma bc_mt_corresp_Dup: "
  1208   bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
  1209  apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
  1210                  max_ssize_def max_of_list_def ssize_sto_def max_def
  1211                  eff_def norm_eff_def)
  1212   apply (intro strip)
  1213   apply (rule conjI)
  1214   apply (rule check_type_mono, assumption, simp)
  1215 apply (simp add: check_type_simps)
  1216 apply clarify
  1217 apply (rule_tac x="Suc (Suc (length ST))" in exI)
  1218 apply simp+
  1219 done
  1220 
  1221 lemma bc_mt_corresp_Dup_x1: "
  1222   bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
  1223   apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
  1224                  max_ssize_def max_of_list_def ssize_sto_def max_def
  1225                  eff_def norm_eff_def)
  1226   apply (intro strip)
  1227   apply (rule conjI)
  1228   apply (rule check_type_mono, assumption, simp)
  1229 apply (simp add: check_type_simps)
  1230 apply clarify
  1231 apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)
  1232 apply simp+
  1233 done
  1234 
  1235 
  1236 
  1237 lemma bc_mt_corresp_IAdd: "
  1238   bc_mt_corresp [IAdd] (replST 2 (PrimT Integer)) 
  1239          (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
  1240   apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
  1241   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
  1242   apply (simp add: check_type_simps)
  1243   apply clarify
  1244   apply (rule_tac x="Suc (length ST)" in exI)
  1245   apply simp+
  1246   done
  1247 
  1248 lemma bc_mt_corresp_Getfield: "\<lbrakk> wf_prog wf_mb G; 
  1249   field (G, C) vname = Some (cname, T);  is_class G C \<rbrakk>
  1250   \<Longrightarrow> bc_mt_corresp [Getfield vname cname] 
  1251         (replST (Suc 0) (snd (the (field (G, cname) vname))))
  1252         (Class C # ST, LT) (comp G) rT mxr (Suc 0)"
  1253   apply (frule wf_prog_ws_prog [THEN wf_subcls1])
  1254   apply (frule field_in_fd, assumption+)
  1255   apply (frule widen_field, assumption+)
  1256   apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
  1257   apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
  1258   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  1259   apply (intro strip)
  1260 apply (simp add: check_type_simps)
  1261 apply clarify
  1262 apply (rule_tac x="Suc (length ST)" in exI)
  1263 apply simp+
  1264 apply (simp only: comp_is_type)
  1265 apply (rule_tac C=cname in fields_is_type)
  1266 apply (simp add: field_def)
  1267 apply (drule JBasis.table_of_remap_SomeD)+
  1268 apply assumption+
  1269 apply (erule wf_prog_ws_prog)
  1270 apply assumption
  1271 done
  1272 
  1273 lemma bc_mt_corresp_Putfield: "\<lbrakk> wf_prog wf_mb G; 
  1274   field (G, C) vname = Some (cname, Ta); G \<turnstile> T \<preceq> Ta; is_class G C \<rbrakk>
  1275   \<Longrightarrow> bc_mt_corresp [Putfield vname cname] (popST 2) (T # Class C # T # ST, LT)
  1276            (comp G) rT mxr (Suc 0)"
  1277   apply (frule wf_prog_ws_prog [THEN wf_subcls1])
  1278   apply (frule field_in_fd, assumption+)
  1279   apply (frule widen_field, assumption+)
  1280   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
  1281   apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
  1282   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
  1283 
  1284   apply (intro strip)
  1285 apply (simp add: check_type_simps)
  1286 apply clarify
  1287 apply (rule_tac x="Suc (length ST)" in exI)
  1288 apply simp+
  1289 done
  1290 
  1291 
  1292 
  1293 lemma Call_app: "\<lbrakk> wf_prog wf_mb G; is_class G cname;
  1294 STs = rev pTsa @ Class cname # ST;
  1295 max_spec G cname (mname, pTsa) = {((md, T), pTs')} \<rbrakk>
  1296   \<Longrightarrow> app (Invoke cname mname pTs') (comp G) (length (T # ST)) rT 0 empty_et (Some (STs, LTs))"
  1297   apply (subgoal_tac "(\<exists>mD' rT' comp_b. 
  1298     method (comp G, cname) (mname, pTs') = Some (mD', rT', comp_b))")
  1299   apply (simp add: comp_is_class)
  1300   apply (rule_tac x=pTsa in exI)
  1301   apply (rule_tac x="Class cname" in exI)
  1302   apply (simp add: max_spec_preserves_length comp_is_class)
  1303   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
  1304   apply (simp add: split_paired_all comp_widen list_all2_def)
  1305   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
  1306   apply (rule exI)+
  1307   apply (simp add: wf_prog_ws_prog [THEN comp_method])
  1308   apply auto
  1309   done
  1310 
  1311 
  1312 lemma bc_mt_corresp_Invoke: "\<lbrakk> wf_prog wf_mb G; 
  1313   max_spec G cname (mname, pTsa) = {((md, T), fpTs)};
  1314   is_class G cname \<rbrakk>
  1315  \<Longrightarrow> bc_mt_corresp [Invoke cname mname fpTs] (replST (Suc (length pTsa)) T)
  1316            (rev pTsa @ Class cname # ST, LT) (comp G) rT mxr (Suc 0)"
  1317   apply (simp add: bc_mt_corresp_def wt_instr_altern_def eff_def norm_eff_def)
  1318   apply (simp add: replST_def del: appInvoke)
  1319   apply (intro strip)
  1320   apply (rule conjI)
  1321 
  1322   -- "app"
  1323   apply (rule Call_app [THEN app_mono_mxs]) apply assumption+
  1324     apply (rule HOL.refl) apply assumption
  1325     apply (simp add: max_ssize_def max_of_list_elem ssize_sto_def)
  1326 
  1327   -- {* @{text "<=s"} *}
  1328   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
  1329   apply (simp add: wf_prog_ws_prog [THEN comp_method])
  1330   apply (simp add: max_spec_preserves_length [THEN sym])
  1331 
  1332   -- "@{text check_type}"
  1333 apply (simp add: max_ssize_def ssize_sto_def max_def)
  1334 apply (simp add: max_of_list_def)
  1335 apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)")
  1336 apply simp
  1337 apply (simp add: check_type_simps)
  1338 apply clarify
  1339 apply (rule_tac x="Suc (length ST)" in exI)
  1340 apply simp+
  1341 apply (simp only: comp_is_type)
  1342 apply (frule method_wf_mdecl) apply assumption apply assumption
  1343 apply (simp add: wf_mdecl_def wf_mhead_def)
  1344 apply (simp add: max_def)
  1345   done
  1346 
  1347 
  1348 lemma wt_instr_Ifcmpeq: "\<lbrakk>Suc pc < max_pc; 
  1349   0 \<le> (int pc + i);  nat (int pc + i) < max_pc;
  1350   (mt_sttp_flatten f ! pc = Some (ts#ts'#ST,LT)) \<and> 
  1351   ((\<exists>p. ts = PrimT p \<and> ts' = PrimT p) \<or> (\<exists>r r'. ts = RefT r \<and> ts' = RefT r'));
  1352   mt_sttp_flatten f ! Suc pc = Some (ST,LT);
  1353   mt_sttp_flatten f ! nat (int pc + i) = Some (ST,LT);
  1354   check_type (TranslComp.comp G) mxs mxr (OK (Some (ts # ts' # ST, LT))) \<rbrakk>
  1355     \<Longrightarrow>  wt_instr_altern (Ifcmpeq i) (comp G) rT  (mt_sttp_flatten f) mxs mxr max_pc empty_et pc"
  1356 by (simp  add: wt_instr_altern_def eff_def norm_eff_def)
  1357 
  1358 
  1359 lemma wt_instr_Goto: "\<lbrakk> 0 \<le> (int pc + i); nat (int pc + i) < max_pc;
  1360   mt_sttp_flatten f ! nat (int pc + i) = (mt_sttp_flatten f ! pc);
  1361   check_type (TranslComp.comp G) mxs mxr (OK (mt_sttp_flatten f ! pc)) \<rbrakk>
  1362   \<Longrightarrow> wt_instr_altern (Goto i) (comp G) rT  (mt_sttp_flatten f) mxs mxr max_pc empty_et pc"
  1363 apply (case_tac "(mt_sttp_flatten f ! pc)")
  1364 apply (simp  add: wt_instr_altern_def eff_def norm_eff_def app_def xcpt_app_def)+
  1365 done
  1366 
  1367 
  1368 
  1369 
  1370   (* ********************************************************************** *)
  1371 
  1372 
  1373 
  1374 lemma bc_mt_corresp_comb_inside: "
  1375   \<lbrakk> 
  1376   bc_mt_corresp bc' f' sttp0 cG rT mxr l1;
  1377   bc' = (bc1@bc2@bc3); f'= (f1 \<box> f2 \<box> f3); 
  1378   l1 = (length bc1); l12 = (length (bc1@bc2));
  1379   bc_mt_corresp bc2 f2 (sttp_of (f1 sttp0)) cG rT mxr (length bc2);
  1380   length bc1 = length (mt_of (f1 sttp0));
  1381   start_sttp_resp f2; start_sttp_resp f3\<rbrakk>
  1382 \<Longrightarrow> bc_mt_corresp bc' f' sttp0 cG rT mxr l12"
  1383 apply (subgoal_tac "\<exists> mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
  1384 apply (subgoal_tac "\<exists> mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
  1385 apply (subgoal_tac "\<exists> mt3 sttp3. (f3 sttp2) = (mt3, sttp3)", (erule exE)+)
  1386 
  1387   (* unfold start_sttp_resp and make case distinction *)
  1388 apply (simp only: start_sttp_resp_def)
  1389 apply (erule_tac Q="start_sttp_resp_cons f2" in disjE)
  1390   (* case f2 = comb_nil *)
  1391 apply (simp add: bc_mt_corresp_def comb_nil_def start_sttp_resp_cons_def)
  1392 
  1393   (* case start_sttp_resp_cons f2 *)
  1394 apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def)
  1395 apply (drule_tac x=sttp1 in spec, simp, erule exE)
  1396 apply (intro strip, (erule conjE)+)
  1397 
  1398 
  1399   (* get rid of all check_type info *)
  1400 apply (subgoal_tac "check_type cG (length (fst sttp1)) mxr (OK (Some sttp1))")
  1401 apply (subgoal_tac "check_type cG (max_ssize (mt2 @ [Some sttp2])) mxr (OK (Some sttp2))")
  1402 apply (subgoal_tac "check_type cG (max_ssize (mt1 @ mt2 @ mt3 @ [Some sttp3])) mxr
  1403            (OK ((mt2 @ mt3 @ [Some sttp3]) ! length mt2))")
  1404 apply simp
  1405 
  1406 
  1407 
  1408 apply (intro strip, (erule conjE)+)
  1409 apply (case_tac "pc < length mt1")
  1410 
  1411   (* case pc < length mt1 *)
  1412 apply (drule spec, drule mp, assumption)
  1413 apply assumption
  1414 
  1415   (* case pc \<ge> length mt1 *)
  1416   (* case distinction on start_sttp_resp f3 *)
  1417 apply (erule_tac P="f3 = comb_nil" in disjE)
  1418 
  1419   (* case f3 = comb_nil *)
  1420 apply (subgoal_tac "mt3 = [] \<and> sttp2 = sttp3")  apply (erule conjE)+
  1421 apply (subgoal_tac "bc3=[]")
  1422 
  1423 apply (rule_tac bc_pre=bc1 and bc=bc2 and bc_post=bc3
  1424   and mt_pre=mt1 and mt=mt2 and mt_post="mt3@ [Some sttp3]" 
  1425   and mxs="(max_ssize (mt2 @ [(Some sttp2)]))"
  1426   and max_pc="(Suc (length mt2))"
  1427   in wt_instr_offset)
  1428   apply simp
  1429   apply (rule HOL.refl)+
  1430   apply (simp (no_asm_simp))+
  1431 
  1432   apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
  1433     apply (rule max_of_list_sublist)
  1434     apply (simp (no_asm_simp) only: set_append set.simps map.simps) apply blast
  1435   apply (simp (no_asm_simp))
  1436   apply simp			(* subgoal bc3 = [] *)
  1437   apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
  1438 
  1439   (* case start_sttp_resp_cons f3 *)
  1440 apply (subgoal_tac "\<exists>mt3_rest. (mt3 = Some sttp2 # mt3_rest)", erule exE)
  1441 apply (rule_tac bc_pre=bc1 and bc=bc2 and bc_post=bc3
  1442   and mt_pre=mt1 and mt=mt2 and mt_post="mt3@ [Some sttp3]" 
  1443   and mxs="(max_ssize (mt2 @ [Some sttp2]))"
  1444   and max_pc="(Suc (length mt2))"
  1445   in wt_instr_offset)
  1446 apply (intro strip)
  1447 apply (rule_tac bc=bc2 and mt="(mt2 @ [Some sttp2])"
  1448   and mxs="(max_ssize (mt2 @ [Some sttp2]))"
  1449   and max_pc="(Suc (length mt2))"
  1450   in wt_instr_prefix)
  1451 
  1452 
  1453      (* preconditions of  wt_instr_prefix *)
  1454   apply simp
  1455   apply (rule HOL.refl)
  1456   apply (simp (no_asm_simp))+
  1457   apply simp+
  1458      (* (some) preconditions of  wt_instr_offset *)
  1459   apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
  1460   apply (rule max_of_list_sublist)
  1461     apply (simp (no_asm_simp) only: set_append set.simps map.simps) apply blast
  1462   apply (simp (no_asm_simp))
  1463 
  1464 apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)
  1465 
  1466   (* subgoals check_type*)
  1467   (* \<dots> ! length mt2 *)
  1468 apply simp
  1469 
  1470 apply (erule_tac P="f3 = comb_nil" in disjE)
  1471 
  1472   (* -- case f3 = comb_nil *)
  1473 apply (subgoal_tac "mt3 = [] \<and> sttp2 = sttp3")  apply (erule conjE)+
  1474 apply simp
  1475 apply (rule check_type_mono, assumption)
  1476 apply (simp only: max_ssize_def) apply (rule max_of_list_sublist) apply (simp (no_asm_simp))
  1477 apply blast
  1478   apply simp			(* subgoal bc3 = [] *)
  1479   apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
  1480 
  1481 
  1482   (* -- case start_sttp_resp_cons f3 *)
  1483 apply (subgoal_tac "\<exists>mt3_rest. (mt3 = Some sttp2 # mt3_rest)", erule exE)
  1484 apply (simp (no_asm_simp) add: nth_append)
  1485 apply (erule conjE)+
  1486 apply (rule check_type_mono, assumption)
  1487 apply (simp only: max_ssize_def) apply (rule max_of_list_sublist) apply (simp (no_asm_simp))
  1488 apply blast
  1489 apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)
  1490 
  1491 
  1492   (* subgoal check_type \<dots> Some sttp2 *)
  1493 apply (simp add: nth_append)
  1494 
  1495   (* subgoal check_type \<dots> Some sttp1 *)
  1496 apply (simp add: nth_append)
  1497 apply (erule conjE)+
  1498 apply (case_tac "sttp1", simp)
  1499 apply (rule check_type_lower) apply assumption
  1500 apply (simp (no_asm_simp) add: max_ssize_def ssize_sto_def)
  1501 apply (simp (no_asm_simp) add: max_of_list_def max_def)
  1502 
  1503   (* subgoals \<exists> ... *)
  1504 apply (rule surj_pair)+
  1505 done
  1506 
  1507 
  1508   (* ******************** *)
  1509 constdefs 
  1510   contracting :: "(state_type \<Rightarrow> method_type \<times> state_type) \<Rightarrow> bool"
  1511   "contracting f == (\<forall> ST LT. 
  1512                     let (ST', LT') = sttp_of (f (ST, LT)) 
  1513                     in (length ST' \<le> length ST \<and> set ST' \<subseteq> set ST  \<and>
  1514                         length LT' = length LT \<and> set LT' \<subseteq> set LT))"
  1515 
  1516 
  1517   (* ### possibly move into HOL *)
  1518 lemma set_drop_Suc [rule_format]: "\<forall> xs. set (drop (Suc n) xs) \<subseteq> set (drop n xs)"
  1519 apply (induct n)
  1520 apply simp
  1521 apply (intro strip)
  1522 apply (rule list.induct)
  1523 apply simp
  1524 apply simp apply blast
  1525 apply (intro strip)
  1526 apply (rule_tac 
  1527   P="\<lambda> xs. set (drop (Suc (Suc n)) xs) \<subseteq> set (drop (Suc n) xs)" in list.induct)
  1528 apply simp+
  1529 done
  1530 
  1531 lemma set_drop_le [rule_format,simp]: "\<forall> n xs. n \<le> m \<longrightarrow> set (drop m xs) \<subseteq> set (drop n xs)"
  1532 apply (induct m)
  1533 apply simp
  1534 apply (intro strip)
  1535 apply (subgoal_tac "na \<le> n \<or> na = Suc n")
  1536 apply (erule disjE)
  1537 apply (frule_tac x=na in spec, drule_tac x=xs in spec, drule mp, assumption)
  1538 apply (rule set_drop_Suc [THEN subset_trans], assumption)
  1539 apply auto
  1540 done
  1541 
  1542 lemma set_drop [simp] : "set (drop m xs) \<subseteq> set xs"
  1543 apply (rule_tac B="set (drop 0 xs)" in subset_trans)
  1544 apply (rule set_drop_le)
  1545 apply simp+
  1546 done
  1547 
  1548 
  1549 
  1550 lemma contracting_popST [simp]: "contracting (popST n)"
  1551 by (simp add: contracting_def popST_def)
  1552 
  1553 lemma contracting_nochangeST [simp]: "contracting nochangeST"
  1554 by (simp add: contracting_def nochangeST_def)
  1555 
  1556 
  1557 lemma check_type_contracting: "\<lbrakk> check_type cG mxs mxr (OK (Some sttp)); contracting f\<rbrakk> 
  1558   \<Longrightarrow> check_type cG mxs mxr (OK (Some (sttp_of (f sttp))))"
  1559 apply (subgoal_tac "\<exists> ST LT. sttp = (ST, LT)", (erule exE)+)
  1560 apply (simp add: check_type_simps contracting_def)
  1561 apply clarify
  1562 apply (drule_tac x=ST in spec, drule_tac x=LT in spec)
  1563 apply (case_tac "(sttp_of (f (ST, LT)))")
  1564 apply simp
  1565 apply (erule conjE)+
  1566 
  1567 apply (drule listE_set)+
  1568 apply (rule conjI)
  1569 apply (rule_tac x="length a" in exI) apply simp
  1570 apply (rule listI) apply simp apply blast
  1571 apply (rule listI) apply simp apply blast
  1572 apply auto
  1573 done
  1574 
  1575   (* ******************** *)
  1576 
  1577 
  1578 lemma bc_mt_corresp_comb_wt_instr: "
  1579   \<lbrakk> bc_mt_corresp bc' f' sttp0 cG rT mxr l1;
  1580   bc' = (bc1@[inst]@bc3); f'= (f1 \<box> f2 \<box> f3); 
  1581   l1 = (length bc1); 
  1582   length bc1 = length (mt_of (f1 sttp0));
  1583   length (mt_of (f2 (sttp_of (f1 sttp0)))) = 1;
  1584   start_sttp_resp_cons f1; start_sttp_resp_cons f2; start_sttp_resp f3;
  1585 
  1586   check_type cG (max_ssize (mt_sttp_flatten (f' sttp0))) mxr
  1587              (OK ((mt_sttp_flatten (f' sttp0)) ! (length bc1)))
  1588   \<longrightarrow>
  1589   wt_instr_altern inst cG rT 
  1590       (mt_sttp_flatten (f' sttp0)) 
  1591       (max_ssize (mt_sttp_flatten (f' sttp0)))
  1592       mxr
  1593       (Suc (length bc'))
  1594       empty_et
  1595       (length bc1);
  1596   contracting f2
  1597  \<rbrakk>
  1598 \<Longrightarrow> bc_mt_corresp bc' f' sttp0 cG rT mxr (length (bc1@[inst]))"
  1599 apply (subgoal_tac "\<exists> mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
  1600 apply (subgoal_tac "\<exists> mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
  1601 apply (subgoal_tac "\<exists> mt3 sttp3. (f3 sttp2) = (mt3, sttp3)", (erule exE)+)
  1602 
  1603 apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def
  1604   mt_sttp_flatten_def)
  1605 
  1606 apply (intro strip, (erule conjE)+)
  1607 apply (drule mp, assumption)+ apply (erule conjE)+
  1608 apply (drule mp, assumption)
  1609 apply (rule conjI)
  1610 
  1611   (* wt_instr \<dots> *)
  1612 apply (intro strip)
  1613 apply (case_tac "pc < length mt1")
  1614 
  1615   (* case pc < length mt1 *)
  1616 apply (drule spec, drule mp, assumption)
  1617 apply assumption
  1618 
  1619   (* case pc \<ge> length mt1 *)
  1620 apply (subgoal_tac "pc = length mt1") prefer 2 apply arith
  1621 apply (simp only:)
  1622 apply (simp add: nth_append mt_sttp_flatten_def)
  1623 
  1624 
  1625   (* check_type \<dots> *)
  1626 apply (simp add: start_sttp_resp_def)
  1627 apply (drule_tac x="sttp0" in spec, simp, erule exE)
  1628 apply (drule_tac x="sttp1" in spec, simp, erule exE)
  1629 
  1630 apply (subgoal_tac "check_type cG (max_ssize (mt1 @ mt2 @ mt3 @ [Some sttp3])) mxr 
  1631                     (OK (Some (sttp_of (f2 sttp1))))")
  1632 
  1633 apply (simp only:)
  1634 
  1635 apply (erule disjE)
  1636     (* case f3 = comb_nil *)
  1637 apply (subgoal_tac "((mt1 @ mt2 @ mt3 @ [Some sttp3]) ! Suc (length mt1)) = (Some (snd (f2 sttp1)))")apply (subgoal_tac "mt3 = [] \<and> sttp2 = sttp3")  apply (erule conjE)+
  1638 apply (simp add: nth_append)
  1639 apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
  1640 apply (simp add: nth_append comb_nil_def) (* subgoal \<dots> ! Suc (length mt1) *)
  1641 
  1642     (* case start_sttp_resp_cons f3 *)
  1643 apply (simp add: start_sttp_resp_cons_def)  
  1644 apply (drule_tac x="sttp2" in spec, simp, erule exE)
  1645 apply (simp  add: nth_append)
  1646 
  1647   (* subgoal check_type *)
  1648 apply (rule check_type_contracting)
  1649 apply (subgoal_tac "((mt1 @ mt2 @ mt3 @ [Some sttp3]) ! length mt1) = (Some sttp1)")
  1650 apply (simp add: nth_append)
  1651 apply (simp add: nth_append)
  1652 
  1653 apply assumption
  1654 
  1655 (* subgoals *)
  1656 apply (rule surj_pair)+
  1657 done
  1658 
  1659 
  1660 lemma compTpExpr_LT_ST_rewr [simp]: "\<lbrakk>
  1661   wf_java_prog G;
  1662   wf_java_mdecl G C ((mn, pTs), rT, (pns, lvars, blk, res));
  1663   local_env G C (mn, pTs) pns lvars \<turnstile> ex :: T;
  1664   is_inited_LT C pTs lvars LT\<rbrakk>
  1665 \<Longrightarrow> sttp_of (compTpExpr (pns, lvars, blk, res) G ex (ST, LT)) = (T # ST, LT)"
  1666 apply (rule compTpExpr_LT_ST)
  1667 apply auto
  1668 done
  1669 
  1670 
  1671 
  1672 
  1673 lemma wt_method_compTpExpr_Exprs_corresp: "
  1674   \<lbrakk> jmb = (pns,lvars,blk,res); 
  1675   wf_prog wf_java_mdecl G;
  1676   wf_java_mdecl G C ((mn, pTs), rT, jmb);
  1677   E = (local_env G C (mn, pTs) pns lvars)\<rbrakk> 
  1678 \<Longrightarrow> 
  1679  (\<forall> ST LT T bc' f'.
  1680   E \<turnstile> ex :: T \<longrightarrow>  
  1681   (is_inited_LT C pTs lvars LT) \<longrightarrow>
  1682   bc' = (compExpr jmb ex) \<longrightarrow>
  1683   f' = (compTpExpr jmb G ex)
  1684   \<longrightarrow> bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) (length bc'))
  1685  \<and>
  1686  (\<forall> ST LT Ts.
  1687   E \<turnstile> exs [::] Ts \<longrightarrow>
  1688   (is_inited_LT C pTs lvars LT) 
  1689   \<longrightarrow> bc_mt_corresp (compExprs jmb exs) (compTpExprs jmb G exs) (ST, LT) (comp G) rT (length LT) (length (compExprs jmb exs)))"
  1690 
  1691 apply (rule  expr.induct)
  1692 
  1693 
  1694 (* expresssions *)
  1695 
  1696 (* NewC *)
  1697 apply (intro allI impI)
  1698 apply (simp only:)
  1699 apply (drule NewC_invers)
  1700 apply (simp (no_asm_use))
  1701 apply (rule bc_mt_corresp_New)
  1702 apply (simp add: comp_is_class)
  1703 
  1704 (* Cast *)
  1705 apply (intro allI impI)
  1706 apply (simp only:)
  1707 apply (drule Cast_invers)
  1708 apply clarify
  1709 apply (simp (no_asm_use))
  1710 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast)
  1711 apply (simp (no_asm_simp), rule bc_mt_corresp_Checkcast)
  1712 apply (simp add: comp_is_class)
  1713 apply (simp only: compTpExpr_LT_ST)
  1714 apply (drule cast_RefT)
  1715 apply blast
  1716 apply (simp add: start_sttp_resp_def)
  1717 
  1718 (* Lit *)
  1719 apply (intro allI impI)
  1720 apply (simp only:)
  1721 apply (drule Lit_invers)
  1722 (* apply (simp (no_asm_use)) *)
  1723 apply simp
  1724 apply (rule bc_mt_corresp_LitPush)
  1725    apply assumption
  1726 
  1727 
  1728 (* BinOp *)
  1729 
  1730 apply (intro allI impI)
  1731 apply (simp (no_asm_simp) only:)
  1732 apply (drule BinOp_invers, erule exE, (erule conjE)+)
  1733 apply (case_tac binop)
  1734 apply (simp (no_asm_simp))
  1735 
  1736   (* case Eq *)
  1737 apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0")
  1738 prefer 2
  1739   apply (rule bc_mt_corresp_zero) apply (simp add: length_compTpExpr) 
  1740   apply (simp (no_asm_simp))
  1741 
  1742 apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "compExpr jmb expr1" 
  1743   and ?f1.0=comb_nil and ?f2.0 = "compTpExpr jmb G expr1" 
  1744   in bc_mt_corresp_comb_inside)
  1745   apply (simp (no_asm_simp))+
  1746   apply blast
  1747   apply (simp (no_asm_simp) add: length_compTpExpr)+
  1748 
  1749 apply (drule_tac ?bc2.0 = "compExpr jmb expr2" and ?f2.0 = "compTpExpr jmb G expr2" 
  1750   in bc_mt_corresp_comb_inside)
  1751   apply (simp (no_asm_simp))+
  1752   apply (simp only: compTpExpr_LT_ST)
  1753   apply (simp (no_asm_simp) add: length_compTpExpr)
  1754   apply (simp (no_asm_simp))
  1755   apply (simp (no_asm_simp))
  1756 
  1757 apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2" 
  1758     and inst = "Ifcmpeq 3" and ?bc3.0 = "[LitPush (Bool False),Goto 2, LitPush (Bool True)]"
  1759   and ?f1.0="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2"
  1760   and ?f2.0="popST 2" and ?f3.0="pushST [PrimT Boolean] \<box> popST 1 \<box> pushST [PrimT Boolean]"
  1761   in bc_mt_corresp_comb_wt_instr)
  1762   apply (simp (no_asm_simp) add: length_compTpExpr)+
  1763 
  1764     (* wt_instr *)
  1765   apply (intro strip)
  1766   apply (simp (no_asm_simp) add: wt_instr_altern_def length_compTpExpr eff_def)
  1767   apply (simp (no_asm_simp) add: norm_eff_def)
  1768   apply (simp (no_asm_simp) only: int_outside_left nat_int)
  1769   apply (simp (no_asm_simp) add: length_compTpExpr)
  1770   apply (simp only: compTpExpr_LT_ST)+
  1771   apply (simp add: eff_def norm_eff_def popST_def pushST_def mt_sttp_flatten_def)
  1772   apply (case_tac Ta) apply (simp (no_asm_simp)) apply (simp (no_asm_simp))
  1773   apply (rule contracting_popST)		(* contracting (popST 2)  *)
  1774 
  1775 apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3]"
  1776   and ?bc2.0 = "[LitPush (Bool False)]" 
  1777   and ?bc3.0 = "[Goto 2, LitPush (Bool True)]" 
  1778   and ?f1.0 = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2"
  1779   and ?f2.0 = "pushST [PrimT Boolean]" 
  1780   and ?f3.0 = "popST (Suc 0) \<box> pushST [PrimT Boolean]"
  1781   in bc_mt_corresp_comb_inside)
  1782   apply (simp (no_asm_simp))+
  1783   apply (simp add: compTpExpr_LT_ST_rewr popST_def)
  1784   apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp))
  1785   apply (simp (no_asm_simp) add: length_compTpExpr)
  1786   apply (simp (no_asm_simp))
  1787   apply (simp (no_asm_simp) add: start_sttp_resp_def)
  1788 
  1789 
  1790 apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False)]" 
  1791     and inst = "Goto 2" and ?bc3.0 = "[LitPush (Bool True)]"
  1792   and ?f1.0="compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> pushST [PrimT Boolean]"
  1793   and ?f2.0="popST 1" and ?f3.0="pushST [PrimT Boolean]"
  1794   in bc_mt_corresp_comb_wt_instr)
  1795   apply (simp (no_asm_simp) add: length_compTpExpr)+
  1796 
  1797     (* wt_instr *)
  1798   apply (simp (no_asm_simp) add: wt_instr_altern_def length_compTpExpr)
  1799   apply (simp (no_asm_simp) add: eff_def norm_eff_def)
  1800   apply (simp (no_asm_simp) only: int_outside_right nat_int)
  1801   apply (simp (no_asm_simp) add: length_compTpExpr)
  1802   apply (simp only: compTpExpr_LT_ST)+
  1803   apply (simp add: eff_def norm_eff_def popST_def pushST_def)
  1804   apply (rule contracting_popST)		(* contracting (popST 1) *)
  1805 
  1806 apply (drule_tac 
  1807   ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False), Goto 2]" 
  1808   and ?bc2.0 = "[LitPush (Bool True)]"
  1809   and ?bc3.0 = "[]"
  1810   and ?f1.0 = "compTpExpr jmb G expr1 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> 
  1811                 pushST [PrimT Boolean] \<box> popST (Suc 0)"
  1812   and ?f2.0 = "pushST [PrimT Boolean]"
  1813   and ?f3.0 = "comb_nil" 
  1814   in bc_mt_corresp_comb_inside)
  1815   apply (simp (no_asm_simp))+
  1816   apply (simp add: compTpExpr_LT_ST_rewr popST_def) 
  1817   apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp))
  1818   apply (simp (no_asm_simp) add: length_compTpExpr)
  1819   apply (simp (no_asm_simp) add: start_sttp_resp_def)
  1820   apply (simp (no_asm_simp))
  1821 
  1822 apply simp
  1823 
  1824   (* case Add *)
  1825 apply simp
  1826 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast
  1827 apply (rule bc_mt_corresp_comb, rule HOL.refl) 
  1828    apply (simp only: compTpExpr_LT_ST) 
  1829 apply (simp only: compTpExpr_LT_ST) apply blast
  1830 
  1831 apply (simp only: compTpExpr_LT_ST)
  1832 apply simp
  1833 apply (rule bc_mt_corresp_IAdd)
  1834 apply (simp (no_asm_simp) add: start_sttp_resp_def)
  1835 apply (simp (no_asm_simp) add: start_sttp_resp_def)
  1836 
  1837 
  1838   (* LAcc *)
  1839 apply (intro allI impI)
  1840 apply (simp only:)
  1841 apply (drule LAcc_invers)
  1842 apply (frule wf_java_mdecl_length_pTs_pns)
  1843 apply clarify
  1844 apply (simp add: is_inited_LT_def)
  1845 apply (rule bc_mt_corresp_Load)
  1846   apply (rule index_in_bounds) apply simp apply assumption
  1847   apply (rule inited_LT_at_index_no_err)
  1848   apply (rule index_in_bounds) apply simp apply assumption
  1849 apply (rule HOL.refl)
  1850 
  1851 
  1852   (* LAss *)
  1853 apply (intro allI impI)
  1854 apply (simp only:)
  1855 apply (drule LAss_invers, erule exE, (erule conjE)+)
  1856 apply (drule LAcc_invers)
  1857 apply (frule wf_java_mdecl_disjoint_varnames, simp add: disjoint_varnames_def)
  1858 apply (frule wf_java_mdecl_length_pTs_pns)
  1859 apply clarify
  1860 apply (simp (no_asm_use))
  1861 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast)
  1862 apply (rule_tac ?bc1.0="[Dup]" and ?bc2.0="[Store (index (pns, lvars, blk, res) vname)]" 
  1863        and ?f1.0="dupST" and ?f2.0="popST (Suc 0)"
  1864        in bc_mt_corresp_comb) 
  1865   apply (simp (no_asm_simp))+
  1866   apply (rule bc_mt_corresp_Dup)
  1867   apply (simp only: compTpExpr_LT_ST)
  1868   apply (simp add: dupST_def is_inited_LT_def)
  1869   apply (rule bc_mt_corresp_Store)
  1870   apply (rule index_in_bounds)
  1871     apply simp apply assumption
  1872   apply (rule sup_loc_update_index, assumption+) 
  1873     apply simp apply assumption+
  1874 apply (simp add: start_sttp_resp_def)
  1875 apply (simp add: start_sttp_resp_def)
  1876 
  1877   (* FAcc *)
  1878 apply (intro allI impI)
  1879 apply (simp only:)
  1880 apply (drule FAcc_invers)
  1881 apply clarify
  1882 apply (simp (no_asm_use))
  1883 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp), blast) 
  1884   apply (simp (no_asm_simp))
  1885   apply (rule bc_mt_corresp_Getfield) apply assumption+
  1886      apply (fast intro: wt_class_expr_is_class)
  1887 apply (simp (no_asm_simp) add: start_sttp_resp_def)
  1888 
  1889 
  1890   (* FAss *)
  1891 apply (intro allI impI)
  1892 apply (simp only:)
  1893 apply (drule FAss_invers, erule exE, (erule conjE)+)
  1894 apply (drule FAcc_invers)
  1895 apply clarify
  1896 apply (simp (no_asm_use))
  1897 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast
  1898   apply (simp only: compTpExpr_LT_ST)
  1899 apply (rule bc_mt_corresp_comb, (rule HOL.refl)+) apply blast
  1900   apply (simp only: compTpExpr_LT_ST)
  1901 apply (rule_tac ?bc1.0="[Dup_x1]" and ?bc2.0="[Putfield vname cname]" in bc_mt_corresp_comb) 
  1902   apply (simp (no_asm_simp))+
  1903 apply (rule bc_mt_corresp_Dup_x1)
  1904   apply (simp (no_asm_simp) add: dup_x1ST_def)
  1905 apply (rule bc_mt_corresp_Putfield) apply assumption+
  1906      apply (fast intro: wt_class_expr_is_class)
  1907 apply (simp (no_asm_simp) add: start_sttp_resp_def)
  1908 apply (simp (no_asm_simp) add: start_sttp_resp_def)
  1909 apply (simp (no_asm_simp) add: start_sttp_resp_def)
  1910 
  1911 (* Call *)
  1912 apply (intro allI impI)
  1913 apply (simp only:)
  1914 apply (drule Call_invers)
  1915 apply clarify
  1916 apply (simp (no_asm_use))
  1917 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast
  1918   apply (simp only: compTpExpr_LT_ST)
  1919 apply (rule bc_mt_corresp_comb, (rule HOL.refl)+) apply blast
  1920   apply (simp only: compTpExprs_LT_ST)
  1921   apply (simp (no_asm_simp))
  1922 apply (rule bc_mt_corresp_Invoke) apply assumption+
  1923      apply (fast intro: wt_class_expr_is_class)
  1924 apply (simp (no_asm_simp) add: start_sttp_resp_def)
  1925 apply (rule start_sttp_resp_comb) 
  1926   apply (simp (no_asm_simp))
  1927   apply (simp (no_asm_simp) add: start_sttp_resp_def)
  1928 
  1929 
  1930 (* expression lists *)
  1931 (* nil *) 
  1932 
  1933 apply (intro allI impI)
  1934 apply (drule Nil_invers)
  1935 apply simp
  1936 
  1937 (* cons *)
  1938 
  1939 apply (intro allI impI)
  1940 apply (drule Cons_invers, (erule exE)+, (erule conjE)+)
  1941 apply clarify
  1942 apply (simp (no_asm_use))
  1943 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) apply simp apply blast
  1944   apply (simp only: compTpExpr_LT_ST)
  1945 apply blast
  1946 apply simp
  1947 
  1948 done
  1949 
  1950 
  1951 lemmas wt_method_compTpExpr_corresp [rule_format (no_asm)] = 
  1952   wt_method_compTpExpr_Exprs_corresp [THEN conjunct1]
  1953 
  1954 
  1955   (* ********************************************************************** *)
  1956 
  1957 
  1958 
  1959 
  1960 lemma wt_method_compTpStmt_corresp [rule_format (no_asm)]: "
  1961   \<lbrakk> jmb = (pns,lvars,blk,res); 
  1962   wf_prog wf_java_mdecl G;
  1963   wf_java_mdecl G C ((mn, pTs), rT, jmb);
  1964   E = (local_env G C (mn, pTs) pns lvars)\<rbrakk> 
  1965 \<Longrightarrow> 
  1966  (\<forall> ST LT T bc' f'.
  1967   E \<turnstile> s\<surd> \<longrightarrow>
  1968   (is_inited_LT C pTs lvars LT) \<longrightarrow>
  1969   bc' = (compStmt jmb s) \<longrightarrow>
  1970   f' = (compTpStmt jmb G s)
  1971   \<longrightarrow> bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) (length bc'))"
  1972 
  1973 apply (rule stmt.induct)
  1974 
  1975 (* Skip *) 
  1976 apply (intro allI impI)
  1977 apply simp
  1978 
  1979 
  1980 (* Expr *)
  1981 apply (intro allI impI)
  1982 apply (drule Expr_invers, erule exE)
  1983 apply (simp (no_asm_simp))
  1984 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp))
  1985 apply (rule wt_method_compTpExpr_corresp) apply assumption+
  1986 apply (simp add: compTpExpr_LT_ST [of _ pns lvars blk res])+
  1987 apply (rule bc_mt_corresp_Pop)
  1988 apply (simp add: start_sttp_resp_def)
  1989 
  1990 
  1991 (* Comp *)
  1992 apply (intro allI impI)
  1993 apply (drule Comp_invers)
  1994 apply clarify
  1995 apply (simp (no_asm_use))
  1996 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl) 
  1997    apply (simp (no_asm_simp)) apply blast
  1998 apply (simp only: compTpStmt_LT_ST) 
  1999 apply (simp (no_asm_simp))
  2000 
  2001 (* Cond *)
  2002 apply (intro allI impI)
  2003 apply (simp (no_asm_simp) only:)
  2004 apply (drule Cond_invers, (erule conjE)+)
  2005 apply (simp (no_asm_simp))
  2006 
  2007 apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0")
  2008 prefer 2 
  2009 apply (rule bc_mt_corresp_zero) 
  2010   apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr)
  2011   apply (simp (no_asm_simp))
  2012 
  2013 apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "[LitPush (Bool False)]" 
  2014   and ?bc3.0="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
  2015             compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
  2016             compStmt jmb stmt2" 
  2017   and ?f1.0=comb_nil and ?f2.0 = "pushST [PrimT Boolean]" 
  2018   and ?f3.0="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt1 \<box>
  2019             nochangeST \<box> compTpStmt jmb G stmt2"
  2020   in bc_mt_corresp_comb_inside)
  2021   apply (simp (no_asm_simp))+
  2022   apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
  2023   apply (simp (no_asm_simp) add: start_sttp_resp_def)+
  2024 
  2025 apply (drule_tac ?bc1.0="[LitPush (Bool False)]" and ?bc2.0 = "compExpr jmb expr"
  2026   and ?bc3.0="Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
  2027             compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
  2028             compStmt jmb stmt2" 
  2029   and ?f1.0="pushST [PrimT Boolean]" and ?f2.0 = "compTpExpr jmb G expr"
  2030   and ?f3.0="popST 2 \<box> compTpStmt jmb G stmt1 \<box>
  2031             nochangeST \<box> compTpStmt jmb G stmt2"
  2032   in bc_mt_corresp_comb_inside)
  2033   apply (simp (no_asm_simp))+
  2034   apply (simp (no_asm_simp)  add: pushST_def)
  2035   apply (rule  wt_method_compTpExpr_corresp) apply assumption+ 
  2036       apply (simp (no_asm_simp))+
  2037 
  2038 
  2039 apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr" 
  2040     and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt1)))" 
  2041   and ?bc3.0 = "compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
  2042             compStmt jmb stmt2"
  2043   and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and ?f2.0 = "popST 2"
  2044   and ?f3.0="compTpStmt jmb G stmt1 \<box> nochangeST \<box> compTpStmt jmb G stmt2"
  2045   in bc_mt_corresp_comb_wt_instr)
  2046   apply (simp (no_asm_simp) add: length_compTpExpr)+
  2047   apply (simp (no_asm_simp) add: start_sttp_resp_comb)
  2048 
  2049     (* wt_instr *)
  2050   apply (intro strip)
  2051   apply (rule_tac ts="PrimT Boolean" and ts'="PrimT Boolean" 
  2052     and ST=ST and LT=LT 
  2053     in wt_instr_Ifcmpeq)
  2054   apply (simp (no_asm_simp))
  2055   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
  2056   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
  2057     (* current pc *)
  2058   apply (simp add: length_compTpExpr pushST_def)
  2059   apply (simp only: compTpExpr_LT_ST) 
  2060     (* Suc pc *)
  2061   apply (simp add: length_compTpExpr pushST_def)
  2062   apply (simp add: popST_def start_sttp_resp_comb)
  2063     (* jump goal *)
  2064   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
  2065   apply (simp add: length_compTpExpr pushST_def)
  2066   apply (simp add: popST_def start_sttp_resp_comb length_compTpStmt)
  2067   apply (simp only: compTpStmt_LT_ST)
  2068   apply (simp add: nochangeST_def)
  2069     (* check_type *)
  2070   apply (subgoal_tac "
  2071     (mt_sttp_flatten (f' (ST, LT)) ! length ([LitPush (Bool False)] @ compExpr jmb expr)) = 
  2072     (Some (PrimT Boolean # PrimT Boolean # ST, LT))")
  2073   apply (simp only:)
  2074   apply (simp (no_asm_simp)) apply (rule trans, rule mt_sttp_flatten_comb_length) 
  2075     apply (rule HOL.refl) apply (simp (no_asm_simp) add: length_compTpExpr)
  2076     apply (simp (no_asm_simp) add: length_compTpExpr pushST_def)
  2077     apply (simp only: compTpExpr_LT_ST_rewr) 
  2078     (* contracting\<dots> *)
  2079   apply (rule contracting_popST)
  2080 
  2081 apply (drule_tac 
  2082   ?bc1.0="[LitPush (Bool False)] @ compExpr jmb expr @ 
  2083            [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] " 
  2084   and ?bc2.0 = "compStmt jmb stmt1"
  2085   and ?bc3.0="Goto (1 + int (length (compStmt jmb stmt2))) # compStmt jmb stmt2"
  2086   and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2" 
  2087   and ?f2.0 = "compTpStmt jmb G stmt1"
  2088   and ?f3.0="nochangeST \<box> compTpStmt jmb G stmt2"
  2089   in bc_mt_corresp_comb_inside)
  2090   apply (simp (no_asm_simp))+
  2091   apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST)
  2092   apply (simp only: compTpExpr_LT_ST)
  2093   apply (simp (no_asm_simp))
  2094   apply (simp (no_asm_simp) add: length_compTpExpr)+
  2095 
  2096 
  2097 apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ compStmt jmb stmt1" 
  2098     and inst = "Goto (1 + int (length (compStmt jmb stmt2)))"
  2099   and ?bc3.0 = "compStmt jmb stmt2"
  2100   and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
  2101               compTpStmt jmb G stmt1" 
  2102   and ?f2.0 = "nochangeST"
  2103   and ?f3.0="compTpStmt jmb G stmt2"
  2104   in bc_mt_corresp_comb_wt_instr)
  2105   apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+
  2106   apply (intro strip)
  2107   apply (rule wt_instr_Goto)
  2108   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
  2109   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
  2110     (* \<dots> ! nat (int pc + i) = \<dots> ! pc *)
  2111   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
  2112   apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
  2113   apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
  2114   apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
  2115   apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
  2116   apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
  2117   apply (simp only:)
  2118   apply (simp add: length_compTpExpr length_compTpStmt)
  2119   apply (rule contracting_nochangeST)
  2120 
  2121 
  2122 apply (drule_tac 
  2123   ?bc1.0= "[LitPush (Bool False)] @ compExpr jmb expr @ 
  2124             [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ 
  2125             compStmt jmb stmt1 @ [Goto (1 + int (length (compStmt jmb stmt2)))]"
  2126   and ?bc2.0 = "compStmt jmb stmt2"
  2127   and ?bc3.0="[]"
  2128   and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
  2129               compTpStmt jmb G stmt1 \<box> nochangeST"
  2130   and ?f2.0 = "compTpStmt jmb G stmt2"
  2131   and ?f3.0="comb_nil"
  2132   in bc_mt_corresp_comb_inside)
  2133   apply (simp (no_asm_simp))+
  2134   apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def compTpExpr_LT_ST)
  2135   apply (simp only: compTpExpr_LT_ST)
  2136   apply (simp (no_asm_simp))
  2137   apply (simp only: compTpStmt_LT_ST)
  2138   apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+
  2139 
  2140 apply simp
  2141 
  2142 
  2143 (* Loop *)
  2144 apply (intro allI impI)
  2145 apply (simp (no_asm_simp) only:)
  2146 apply (drule Loop_invers, (erule conjE)+)
  2147 apply (simp (no_asm_simp))
  2148 
  2149 apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0")
  2150 prefer 2 
  2151 apply (rule bc_mt_corresp_zero) 
  2152   apply (simp (no_asm_simp) add: length_compTpStmt length_compTpExpr)
  2153   apply (simp (no_asm_simp))
  2154 
  2155 apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "[LitPush (Bool False)]" 
  2156   and ?bc3.0="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
  2157             compStmt jmb stmt @ 
  2158             [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]" 
  2159   and ?f1.0=comb_nil and ?f2.0 = "pushST [PrimT Boolean]" 
  2160   and ?f3.0="compTpExpr jmb G expr \<box> popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
  2161   in bc_mt_corresp_comb_inside)
  2162   apply (simp (no_asm_simp))+
  2163   apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
  2164   apply (simp (no_asm_simp) add: start_sttp_resp_def)+
  2165 
  2166 apply (drule_tac ?bc1.0="[LitPush (Bool False)]" and ?bc2.0 = "compExpr jmb expr"
  2167   and ?bc3.0="Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
  2168             compStmt jmb stmt @ 
  2169             [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]" 
  2170   and ?f1.0="pushST [PrimT Boolean]" and ?f2.0 = "compTpExpr jmb G expr"
  2171   and ?f3.0="popST 2 \<box> compTpStmt jmb G stmt \<box> nochangeST"
  2172   in bc_mt_corresp_comb_inside)
  2173   apply (simp (no_asm_simp))+
  2174   apply (simp (no_asm_simp)  add: pushST_def)
  2175   apply (rule  wt_method_compTpExpr_corresp) apply assumption+ 
  2176       apply (simp (no_asm_simp))+
  2177 
  2178 
  2179 apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr" 
  2180     and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt)))" 
  2181   and ?bc3.0 = "compStmt jmb stmt @ 
  2182        [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
  2183   and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr" and ?f2.0 = "popST 2"
  2184   and ?f3.0="compTpStmt jmb G stmt \<box> nochangeST"
  2185   in bc_mt_corresp_comb_wt_instr)
  2186   apply (simp (no_asm_simp) add: length_compTpExpr)+
  2187   apply (simp (no_asm_simp) add: start_sttp_resp_comb)
  2188 
  2189     (* wt_instr *)
  2190   apply (intro strip)
  2191   apply (rule_tac ts="PrimT Boolean" and ts'="PrimT Boolean" 
  2192     and ST=ST and LT=LT 
  2193     in wt_instr_Ifcmpeq)
  2194   apply (simp (no_asm_simp))
  2195   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
  2196   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
  2197     (* current pc *)
  2198   apply (simp add: length_compTpExpr pushST_def)
  2199   apply (simp only: compTpExpr_LT_ST) 
  2200     (* Suc pc *)
  2201   apply (simp add: length_compTpExpr pushST_def)
  2202   apply (simp add: popST_def start_sttp_resp_comb)
  2203     (* jump goal *)
  2204   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
  2205   apply (simp add: length_compTpExpr pushST_def)
  2206   apply (simp add: popST_def start_sttp_resp_comb length_compTpStmt)
  2207   apply (simp only: compTpStmt_LT_ST)
  2208   apply (simp add: nochangeST_def)
  2209     (* check_type *)
  2210   apply (subgoal_tac "
  2211     (mt_sttp_flatten (f' (ST, LT)) ! length ([LitPush (Bool False)] @ compExpr jmb expr)) = 
  2212     (Some (PrimT Boolean # PrimT Boolean # ST, LT))")
  2213   apply (simp only:)
  2214   apply (simp (no_asm_simp)) apply (rule trans, rule mt_sttp_flatten_comb_length) 
  2215     apply (rule HOL.refl) apply (simp (no_asm_simp) add: length_compTpExpr)
  2216     apply (simp (no_asm_simp) add: length_compTpExpr pushST_def)
  2217     apply (simp only: compTpExpr_LT_ST_rewr) 
  2218     (* contracting\<dots> *)
  2219   apply (rule contracting_popST)
  2220 
  2221 apply (drule_tac 
  2222   ?bc1.0="[LitPush (Bool False)] @ compExpr jmb expr @ 
  2223            [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] " 
  2224   and ?bc2.0 = "compStmt jmb stmt"
  2225   and ?bc3.0="[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
  2226   and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2" 
  2227   and ?f2.0 = "compTpStmt jmb G stmt"
  2228   and ?f3.0="nochangeST"
  2229   in bc_mt_corresp_comb_inside)
  2230   apply (simp (no_asm_simp))+
  2231   apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST)
  2232   apply (simp only: compTpExpr_LT_ST)
  2233   apply (simp (no_asm_simp))
  2234   apply (simp (no_asm_simp) add: length_compTpExpr)+
  2235 
  2236 
  2237 apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] @ compStmt jmb stmt" 
  2238     and inst = "Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))"
  2239   and ?bc3.0 = "[]"
  2240   and ?f1.0="pushST [PrimT Boolean] \<box> compTpExpr jmb G expr \<box> popST 2 \<box> 
  2241               compTpStmt jmb G stmt" 
  2242   and ?f2.0 = "nochangeST"
  2243   and ?f3.0="comb_nil"
  2244   in bc_mt_corresp_comb_wt_instr)
  2245   apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+ 
  2246   apply (intro strip)
  2247   apply (rule wt_instr_Goto)
  2248   apply arith
  2249   apply arith
  2250     (* \<dots> ! nat (int pc + i) = \<dots> ! pc *)
  2251   apply (simp (no_asm_simp))
  2252   apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
  2253   apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
  2254   apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
  2255   apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
  2256   apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
  2257   apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
  2258   apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
  2259   apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
  2260 
  2261   apply (simp add: length_compTpExpr length_compTpStmt) (* check_type *)
  2262     apply (simp add: pushST_def popST_def compTpExpr_LT_ST compTpStmt_LT_ST)
  2263   apply (rule contracting_nochangeST)
  2264 apply simp
  2265 
  2266 done
  2267 
  2268 
  2269   (**********************************************************************************)
  2270 
  2271 
  2272 
  2273 lemma wt_method_compTpInit_corresp: "\<lbrakk> jmb = (pns,lvars,blk,res); 
  2274   wf_java_mdecl G C ((mn, pTs), rT, jmb); mxr = length LT;
  2275   length LT = (length pns) + (length lvars) + 1;  vn \<in> set (map fst lvars);
  2276   bc = (compInit jmb (vn,ty)); f = (compTpInit jmb (vn,ty));
  2277   is_type G ty \<rbrakk>
  2278   \<Longrightarrow> bc_mt_corresp bc f (ST, LT) (comp G) rT mxr (length bc)"
  2279 apply (simp add: compInit_def compTpInit_def split_beta)
  2280 apply (rule_tac ?bc1.0="[load_default_val ty]" and ?bc2.0="[Store (index jmb vn)]" 
  2281   in bc_mt_corresp_comb) 
  2282   apply simp+
  2283   apply (simp add: load_default_val_def)
  2284    apply (rule typeof_default_val [THEN exE]) 
  2285 
  2286   apply (rule bc_mt_corresp_LitPush_CT) apply assumption
  2287     apply (simp add: comp_is_type)
  2288 apply (simp add: pushST_def)
  2289   apply (rule bc_mt_corresp_Store_init)
  2290   apply simp
  2291   apply (rule index_length_lvars [THEN conjunct2])
  2292 apply auto
  2293 done
  2294 
  2295 
  2296 lemma wt_method_compTpInitLvars_corresp_aux [rule_format (no_asm)]: "
  2297   \<forall> lvars_pre lvars0 ST LT.
  2298   jmb = (pns,lvars0,blk,res) \<and>
  2299   lvars0 = (lvars_pre @ lvars) \<and>
  2300   length LT = (length pns) + (length lvars0) + 1 \<and>
  2301   wf_java_mdecl G C ((mn, pTs), rT, jmb)
  2302  \<longrightarrow> bc_mt_corresp (compInitLvars jmb lvars) (compTpInitLvars jmb lvars) (ST, LT) (comp G) rT 
  2303        (length LT) (length (compInitLvars jmb lvars))"
  2304 apply (induct lvars)
  2305 apply (simp add: compInitLvars_def)
  2306 
  2307 apply (intro strip, (erule conjE)+)
  2308 apply (subgoal_tac "\<exists> vn ty. a = (vn, ty)")
  2309   prefer 2 apply (simp (no_asm_simp)) 
  2310   apply ((erule exE)+, simp (no_asm_simp))
  2311 apply (drule_tac x="lvars_pre @ [a]" in spec)
  2312 apply (drule_tac x="lvars0" in spec)
  2313 apply (simp (no_asm_simp) add: compInitLvars_def)
  2314 apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb list"
  2315   in bc_mt_corresp_comb)
  2316 apply (simp (no_asm_simp) add: compInitLvars_def)+
  2317 
  2318 apply (rule_tac vn=vn and ty=ty in wt_method_compTpInit_corresp)
  2319 apply assumption+
  2320 apply (simp (no_asm_simp))+ 
  2321 apply (simp add: wf_java_mdecl_def)	(* is_type G ty *)
  2322 apply (simp add: compTpInit_def storeST_def pushST_def)
  2323 apply simp
  2324 done
  2325 
  2326 
  2327 lemma wt_method_compTpInitLvars_corresp: "\<lbrakk> jmb = (pns,lvars,blk,res); 
  2328   wf_java_mdecl G C ((mn, pTs), rT, jmb);
  2329   length LT = (length pns) + (length lvars) + 1; mxr = (length LT);
  2330   bc = (compInitLvars jmb lvars); f= (compTpInitLvars jmb lvars) \<rbrakk>
  2331   \<Longrightarrow> bc_mt_corresp bc f (ST, LT) (comp G) rT mxr (length bc)"
  2332 apply (simp only:)
  2333 apply (subgoal_tac "bc_mt_corresp (compInitLvars (pns, lvars, blk, res) lvars)
  2334         (compTpInitLvars (pns, lvars, blk, res) lvars) (ST, LT) (TranslComp.comp G) rT
  2335         (length LT) (length (compInitLvars (pns, lvars, blk, res) lvars))")
  2336 apply simp
  2337 apply (rule_tac lvars_pre="[]" in wt_method_compTpInitLvars_corresp_aux)
  2338 apply auto
  2339 done
  2340 
  2341 
  2342   (**********************************************************************************)
  2343 
  2344 
  2345 
  2346 lemma wt_method_comp_wo_return: "\<lbrakk> wf_prog wf_java_mdecl G;
  2347   wf_java_mdecl G C ((mn, pTs), rT, jmb); 
  2348   bc = compInitLvars jmb lvars @ compStmt jmb blk @ compExpr jmb res;
  2349   jmb = (pns,lvars,blk,res); 
  2350   f = (compTpInitLvars jmb lvars \<box> compTpStmt jmb G blk \<box> compTpExpr jmb G res);
  2351   sttp = (start_ST, start_LT C pTs (length lvars));
  2352   li = (length (inited_LT C pTs lvars))
  2353   \<rbrakk>
  2354 \<Longrightarrow> bc_mt_corresp bc f sttp (comp G) rT  li (length bc)"
  2355 apply (subgoal_tac "\<exists> E. (E = (local_env G C (mn, pTs) pns lvars) \<and> E \<turnstile> blk \<surd> \<and> 
  2356                          (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))")
  2357    apply (erule exE, (erule conjE)+)+
  2358 apply (simp only:)
  2359 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl)+
  2360 
  2361   (* InitLvars *)
  2362 apply (rule wt_method_compTpInitLvars_corresp) 
  2363    apply assumption+
  2364    apply (simp only:)
  2365    apply (simp (no_asm_simp) add: start_LT_def) 
  2366        apply (rule wf_java_mdecl_length_pTs_pns, assumption)
  2367    apply (simp (no_asm_simp) only: start_LT_def)
  2368    apply (simp (no_asm_simp) add: inited_LT_def)+
  2369 
  2370 apply (rule bc_mt_corresp_comb) apply (rule HOL.refl)+
  2371    apply (simp (no_asm_simp) add: compTpInitLvars_LT_ST)
  2372 
  2373      (* stmt *)
  2374 apply (simp only: compTpInitLvars_LT_ST)
  2375 apply (subgoal_tac "(Suc (length pTs + length lvars)) = (length (inited_LT C pTs lvars))")
  2376    prefer 2 apply (simp (no_asm_simp) add: inited_LT_def)
  2377 apply (simp only:)
  2378 apply (rule_tac s=blk in wt_method_compTpStmt_corresp)
  2379    apply assumption+
  2380    apply (simp only:)+
  2381    apply (simp (no_asm_simp) add: is_inited_LT_def)
  2382    apply (simp only:)+
  2383 
  2384      (* expr *)
  2385 apply (simp only: compTpInitLvars_LT_ST compTpStmt_LT_ST is_inited_LT_def)
  2386 apply (subgoal_tac "(Suc (length pTs + length lvars)) = (length (inited_LT C pTs lvars))")
  2387    prefer 2 apply (simp (no_asm_simp) add: inited_LT_def)
  2388 apply (simp only:)
  2389 apply (rule_tac ex=res in wt_method_compTpExpr_corresp)
  2390    apply assumption+
  2391    apply (simp only:)+
  2392    apply (simp (no_asm_simp) add: is_inited_LT_def)
  2393    apply (simp only:)+
  2394 
  2395      (* start_sttp_resp *)
  2396 apply (simp add: start_sttp_resp_comb)+
  2397 
  2398   (* subgoal *)
  2399 apply (simp add: wf_java_mdecl_def local_env_def) 
  2400 done
  2401 
  2402 
  2403   (**********************************************************************************)
  2404 
  2405 
  2406 
  2407 lemma check_type_start: "\<lbrakk> wf_mhead cG (mn, pTs) rT; is_class cG C\<rbrakk>
  2408   \<Longrightarrow> check_type cG (length start_ST) (Suc (length pTs + mxl))
  2409               (OK (Some (start_ST, start_LT C pTs mxl)))"
  2410 apply (simp add: check_type_def wf_mhead_def start_ST_def start_LT_def)
  2411 apply (simp add: check_type_simps)
  2412 apply (simp only: list_def)
  2413 apply (auto simp: err_def)
  2414 apply (subgoal_tac "set (replicate mxl Err) \<subseteq>  {Err}")
  2415 apply blast
  2416 apply (rule subset_replicate)
  2417 done
  2418 
  2419 
  2420 lemma wt_method_comp_aux: "\<lbrakk>   bc' = bc @ [Return]; f' = (f \<box> nochangeST);
  2421   bc_mt_corresp bc f sttp0 cG rT (1+length pTs+mxl) (length bc);
  2422   start_sttp_resp_cons f';
  2423   sttp0 = (start_ST, start_LT C pTs mxl);
  2424   mxs = max_ssize (mt_of (f' sttp0));
  2425   wf_mhead cG (mn, pTs) rT; is_class cG C;
  2426   sttp_of (f sttp0) = (T # ST, LT);
  2427 
  2428   check_type cG mxs (1+length pTs+mxl) (OK (Some (T # ST, LT))) \<longrightarrow>
  2429   wt_instr_altern Return cG rT (mt_of (f' sttp0)) mxs (1+length pTs+mxl) 
  2430          (Suc (length bc)) empty_et (length bc)
  2431 \<rbrakk>
  2432 \<Longrightarrow> wt_method_altern cG C pTs rT mxs mxl bc' empty_et (mt_of (f' sttp0))"
  2433 apply (subgoal_tac "check_type cG (length start_ST) (Suc (length pTs + mxl))
  2434               (OK (Some (start_ST, start_LT C pTs mxl)))")
  2435 apply (subgoal_tac "check_type cG mxs (1+length pTs+mxl) (OK (Some (T # ST, LT)))")
  2436 
  2437 apply (simp add: wt_method_altern_def)
  2438 
  2439   (* length (.. f ..) = length bc *)
  2440 apply (rule conjI)
  2441 apply (simp add: bc_mt_corresp_def split_beta)
  2442 
  2443   (* check_bounded *)
  2444 apply (rule conjI)
  2445 apply (simp add: bc_mt_corresp_def split_beta check_bounded_def) 
  2446 apply (erule conjE)+
  2447 apply (intro strip)
  2448 apply (subgoal_tac "pc < (length bc) \<or> pc = length bc")
  2449   apply (erule disjE)
  2450     (* case  pc < length bc *)
  2451     apply (subgoal_tac "(bc' ! pc) = (bc ! pc)")
  2452     apply (simp add: wt_instr_altern_def eff_def)
  2453       (* subgoal *)
  2454     apply (simp add: nth_append)
  2455     (* case  pc = length bc *)
  2456     apply (subgoal_tac "(bc' ! pc) = Return")
  2457     apply (simp add: wt_instr_altern_def)
  2458       (* subgoal *)
  2459     apply (simp add: nth_append)
  2460 
  2461     (* subgoal pc < length bc \<or> pc = length bc *)
  2462 apply arith
  2463 
  2464   (* wt_start *)
  2465 apply (rule conjI)
  2466 apply (simp add: wt_start_def start_sttp_resp_cons_def split_beta)
  2467   apply (drule_tac x=sttp0 in spec) apply (erule exE)
  2468   apply (simp add: mt_sttp_flatten_def start_ST_def start_LT_def)
  2469 
  2470   (* wt_instr *)
  2471 apply (intro strip)
  2472 apply (subgoal_tac "pc < (length bc) \<or> pc = length bc")
  2473 apply (erule disjE)
  2474 
  2475   (* pc < (length bc) *)
  2476 apply (simp (no_asm_use) add: bc_mt_corresp_def mt_sttp_flatten_def split_beta)
  2477 apply (erule conjE)+
  2478 apply (drule mp, assumption)+
  2479 apply (erule conjE)+
  2480 apply (drule spec, drule mp, assumption)
  2481 apply (simp add: nth_append)
  2482 apply (simp (no_asm_simp) add: comb_def split_beta nochangeST_def)
  2483 
  2484   (* pc = length bc *)
  2485 apply (simp add: nth_append)
  2486 
  2487   (* subgoal pc < (length bc) \<or> pc = length bc *)
  2488 apply arith
  2489 
  2490   (* subgoals *)
  2491 apply (simp (no_asm_use) add: bc_mt_corresp_def split_beta)
  2492 apply (subgoal_tac "check_type cG (length (fst sttp0)) (Suc (length pTs + mxl))
  2493          (OK (Some sttp0))")
  2494 apply ((erule conjE)+, drule mp, assumption)
  2495 apply (simp add: nth_append)
  2496 apply (simp (no_asm_simp) add: comb_def nochangeST_def split_beta)
  2497 apply (simp (no_asm_simp))
  2498 
  2499 apply (rule check_type_start, assumption+)
  2500 done
  2501 
  2502 
  2503 lemma wt_instr_Return: "\<lbrakk>fst f ! pc = Some (T # ST, LT); (G \<turnstile> T \<preceq> rT); pc < max_pc;
  2504   check_type (TranslComp.comp G) mxs mxr (OK (Some (T # ST, LT)))
  2505   \<rbrakk>
  2506   \<Longrightarrow> wt_instr_altern Return (comp G) rT  (mt_of f) mxs mxr max_pc empty_et pc"
  2507   apply (case_tac "(mt_of f ! pc)")
  2508   apply (simp  add: wt_instr_altern_def eff_def norm_eff_def app_def)+
  2509   apply (drule sym)
  2510   apply (simp add: comp_widen xcpt_app_def)
  2511   done
  2512 
  2513 
  2514 theorem wt_method_comp: "
  2515   \<lbrakk> wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths;
  2516   jmdcl = ((mn,pTs), rT, jmb);
  2517   mt = (compTpMethod G C jmdcl);
  2518   (mxs, mxl, bc, et) = mtd_mb (compMethod G C jmdcl) \<rbrakk>
  2519   \<Longrightarrow> wt_method (comp G) C pTs rT mxs mxl bc et mt"
  2520 
  2521   (* show statement for wt_method_altern *)
  2522 apply (rule wt_method_altern_wt_method)
  2523 
  2524 apply (subgoal_tac "wf_java_mdecl G C jmdcl")
  2525 apply (subgoal_tac "wf_mhead G (mn, pTs) rT")
  2526 apply (subgoal_tac "is_class G C")
  2527 apply (subgoal_tac "\<forall> jmb. \<exists> pns lvars blk res. jmb = (pns, lvars, blk, res)")
  2528    apply (drule_tac x=jmb in spec, (erule exE)+)
  2529 apply (subgoal_tac "\<exists> E. (E = (local_env G C (mn, pTs) pns lvars) \<and> E \<turnstile> blk \<surd> \<and> 
  2530                          (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))")
  2531    apply (erule exE, (erule conjE)+)+
  2532 apply (simp add: compMethod_def compTpMethod_def split_beta)
  2533 apply (rule_tac T=T and LT="inited_LT C pTs lvars" and ST=start_ST in wt_method_comp_aux)
  2534 
  2535   (* bc *)
  2536 apply (simp only: append_assoc [THEN sym])
  2537 
  2538   (* comb *)
  2539 apply (simp only: comb_assoc [THEN sym])
  2540 
  2541   (* bc_corresp *)
  2542 apply (rule wt_method_comp_wo_return)
  2543   apply assumption+
  2544   apply (simp (no_asm_use) only: append_assoc)
  2545   apply (rule HOL.refl)
  2546   apply (simp (no_asm_simp))+
  2547   apply (simp (no_asm_simp) add: inited_LT_def)
  2548 
  2549   (* start_sttp_resp *)
  2550 apply (simp add: start_sttp_resp_cons_comb_cons_r)+
  2551 
  2552   (* wf_mhead / is_class *)
  2553 apply (simp add: wf_mhead_def comp_is_type)
  2554 apply (simp add: comp_is_class)
  2555 
  2556   (* sttp_of .. = (T # ST, LT) *)
  2557 apply (simp (no_asm_simp) add: compTpInitLvars_LT_ST compTpExpr_LT_ST compTpStmt_LT_ST is_inited_LT_def)
  2558 apply (subgoal_tac "(snd (compTpInitLvars (pns, lvars, blk, res) lvars
  2559                               (start_ST, start_LT C pTs (length lvars))))
  2560                 = (start_ST, inited_LT C pTs lvars)") 
  2561    prefer 2 apply (rule compTpInitLvars_LT_ST) apply (rule HOL.refl) apply assumption
  2562 apply (simp only:)
  2563 apply (subgoal_tac "(snd (compTpStmt (pns, lvars, blk, res) G blk
  2564                        (start_ST, inited_LT C pTs lvars))) 
  2565                 = (start_ST, inited_LT C pTs lvars)") 
  2566    prefer 2 apply (erule conjE)+
  2567    apply (rule compTpStmt_LT_ST) apply (rule HOL.refl) apply assumption+
  2568    apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
  2569 apply (simp only:)
  2570 apply (rule compTpExpr_LT_ST) apply (rule HOL.refl) apply assumption+
  2571    apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
  2572 
  2573 
  2574    (* Return *)
  2575 apply (intro strip)
  2576 apply (rule_tac T=T and ST=start_ST and LT="inited_LT C pTs lvars" in wt_instr_Return)
  2577 apply (simp (no_asm_simp) add: nth_append 
  2578   length_compTpInitLvars length_compTpStmt length_compTpExpr)
  2579 apply (simp only: compTpInitLvars_LT_ST compTpStmt_LT_ST compTpExpr_LT_ST 
  2580   nochangeST_def)
  2581 apply (simp only: is_inited_LT_def compTpStmt_LT_ST compTpExpr_LT_ST)
  2582 apply (simp (no_asm_simp))+
  2583 apply simp
  2584 
  2585   (* subgoal \<exists> E. \<dots> *)
  2586 apply (simp add: wf_java_mdecl_def local_env_def)
  2587 
  2588   (* subgoal jmb = (\<dots>) *)
  2589 apply (simp only: split_paired_All, simp)
  2590 
  2591   (* subgoal is_class / wf_mhead / wf_java_mdecl *)
  2592 apply (blast intro: methd [THEN conjunct2])
  2593 apply (frule wf_prog_wf_mdecl, assumption+) apply (simp only:) apply (simp add: wf_mdecl_def)
  2594 apply (rule wf_java_prog_wf_java_mdecl, assumption+)
  2595 done
  2596 
  2597 
  2598 lemma comp_set_ms: "(C, D, fs, cms)\<in>set (comp G) 
  2599   \<Longrightarrow> \<exists> ms. (C, D, fs, ms) \<in>set G   \<and> cms = map (compMethod G C) ms"
  2600 by (auto simp: comp_def compClass_def)
  2601 
  2602 
  2603   (* ---------------------------------------------------------------------- *)
  2604 
  2605 section "Main Theorem"
  2606   (* MAIN THEOREM: 
  2607   Methodtype computed by comp is correct for bytecode generated by compTp *)
  2608 theorem wt_prog_comp: "wf_java_prog G  \<Longrightarrow> wt_jvm_prog (comp G) (compTp G)"
  2609 apply (simp add: wf_prog_def)
  2610 
  2611 apply (subgoal_tac "wf_java_prog G") prefer 2 apply (simp add: wf_prog_def)
  2612 apply (simp (no_asm_simp) add: wf_prog_def wt_jvm_prog_def)
  2613 apply (simp add: comp_ws_prog)
  2614 
  2615 apply (intro strip)
  2616 apply (subgoal_tac "\<exists> C D fs cms. c = (C, D, fs, cms)")
  2617 apply clarify
  2618 apply (frule comp_set_ms)
  2619 apply clarify
  2620 apply (drule bspec, assumption)
  2621 apply (rule conjI)
  2622 
  2623   (* wf_mrT *)
  2624 apply (case_tac "C = Object")
  2625 apply (simp add: wf_mrT_def)
  2626 apply (subgoal_tac "is_class G D")
  2627 apply (simp add: comp_wf_mrT)
  2628 apply (simp add: wf_prog_def ws_prog_def ws_cdecl_def)
  2629 apply blast
  2630 
  2631   (* wf_cdecl_mdecl *)
  2632 apply (simp add: wf_cdecl_mdecl_def)
  2633 apply (simp add: split_beta)
  2634 apply (intro strip)
  2635 
  2636   (* show wt_method \<dots> *)
  2637 apply (subgoal_tac "\<exists> sig rT mb. x = (sig, rT, mb)") 
  2638 apply (erule exE)+
  2639 apply (simp (no_asm_simp) add: compMethod_def split_beta)
  2640 apply (erule conjE)+
  2641 apply (drule_tac x="(sig, rT, mb)" in bspec) apply simp
  2642 apply (rule_tac mn="fst sig" and pTs="snd sig" in wt_method_comp)
  2643   apply assumption+
  2644   apply simp
  2645 apply (simp (no_asm_simp) add: compTp_def)
  2646 apply (simp (no_asm_simp) add: compMethod_def split_beta)
  2647 apply (frule WellForm.methd) apply assumption+
  2648 apply simp
  2649 apply simp
  2650 apply (simp add: compMethod_def split_beta)
  2651 apply auto
  2652 done
  2653 
  2654 
  2655 
  2656   (**********************************************************************************)
  2657 
  2658 declare split_paired_All [simp add]
  2659 declare split_paired_Ex [simp add]
  2660 
  2661 
  2662 end