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