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