src/HOL/MicroJava/Comp/CorrComp.thy
author ballarin
Fri Aug 29 15:19:02 2003 +0200 (2003-08-29)
changeset 14174 f3cafd2929d5
parent 14143 7544966fa07d
child 14981 e73f8140af78
permissions -rw-r--r--
Methods rule_tac etc support static (Isar) contexts.
streckem@13673
     1
(*  Title:      HOL/MicroJava/Comp/CorrComp.thy
streckem@13673
     2
    ID:         $Id$
streckem@13673
     3
    Author:     Martin Strecker
streckem@13673
     4
    Copyright   GPL 2002
streckem@13673
     5
*)
streckem@13673
     6
streckem@13673
     7
(* Compiler correctness statement and proof *)
streckem@13673
     8
streckem@13673
     9
theory CorrComp =  JTypeSafe + LemmasComp:
streckem@13673
    10
streckem@14045
    11
declare wf_prog_ws_prog [simp add]
streckem@13673
    12
streckem@13673
    13
(* If no exception is present after evaluation/execution, 
streckem@13673
    14
  none can have been present before *)
streckem@13673
    15
lemma eval_evals_exec_xcpt:
streckem@13673
    16
 "((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
streckem@13673
    17
  ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
streckem@13673
    18
  ((xs,st,xs') \<in> Eval.exec G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)"
streckem@13673
    19
by (induct rule: eval_evals_exec.induct, auto)
streckem@13673
    20
streckem@13673
    21
streckem@13673
    22
(* instance of eval_evals_exec_xcpt for eval *)
streckem@13673
    23
lemma eval_xcpt: "(xs,ex,val,xs') \<in> Eval.eval G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
streckem@13673
    24
 (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
streckem@13673
    25
proof-
streckem@13673
    26
  assume h1: ?H1
streckem@13673
    27
  assume h2: ?H2
streckem@13673
    28
  from h1 h2 eval_evals_exec_xcpt show "?T" by simp
streckem@13673
    29
qed
streckem@13673
    30
streckem@13673
    31
(* instance of eval_evals_exec_xcpt for evals *)
streckem@13673
    32
lemma evals_xcpt: "(xs,exs,vals,xs') \<in> Eval.evals G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
streckem@13673
    33
 (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
streckem@13673
    34
proof-
streckem@13673
    35
  assume h1: ?H1
streckem@13673
    36
  assume h2: ?H2
streckem@13673
    37
  from h1 h2 eval_evals_exec_xcpt show "?T" by simp
streckem@13673
    38
qed
streckem@13673
    39
streckem@13673
    40
(* instance of eval_evals_exec_xcpt for exec *)
streckem@13673
    41
lemma exec_xcpt: "(xs,st,xs') \<in> Eval.exec G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
streckem@13673
    42
 (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
streckem@13673
    43
proof-
streckem@13673
    44
  assume h1: ?H1
streckem@13673
    45
  assume h2: ?H2
streckem@13673
    46
  from h1 h2 eval_evals_exec_xcpt show "?T" by simp
streckem@13673
    47
qed
streckem@13673
    48
streckem@13673
    49
(**********************************************************************)
streckem@13673
    50
streckem@13673
    51
theorem exec_all_trans: "\<lbrakk>(exec_all G s0 s1); (exec_all G s1 s2)\<rbrakk> \<Longrightarrow> (exec_all G s0 s2)"
streckem@13673
    52
apply (auto simp: exec_all_def elim: Transitive_Closure.rtrancl_trans)
streckem@13673
    53
done
streckem@13673
    54
streckem@13673
    55
theorem exec_all_refl: "exec_all G s s"
streckem@13673
    56
by (simp only: exec_all_def, rule rtrancl_refl)
streckem@13673
    57
streckem@13673
    58
streckem@13673
    59
theorem exec_instr_in_exec_all:
streckem@13673
    60
  "\<lbrakk> exec_instr i G hp stk lvars C S pc frs =  (None, hp', frs');
streckem@13673
    61
             gis (gmb G C S) ! pc = i\<rbrakk>  \<Longrightarrow>
streckem@13673
    62
       G \<turnstile> (None, hp, (stk, lvars, C, S, pc) # frs) -jvm\<rightarrow> (None, hp', frs')"
streckem@13673
    63
apply (simp only: exec_all_def)
streckem@13673
    64
apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
streckem@13673
    65
apply (simp add: gis_def gmb_def)
streckem@13673
    66
apply (case_tac frs', simp+)
streckem@13673
    67
done
streckem@13673
    68
streckem@13673
    69
theorem exec_all_one_step: "
streckem@13673
    70
  \<lbrakk> gis (gmb G C S) = pre @ (i # post); pc0 = length pre;
streckem@13673
    71
  (exec_instr i G hp0 stk0 lvars0 C S pc0 frs) = 
streckem@13673
    72
  (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs) \<rbrakk>
streckem@13673
    73
  \<Longrightarrow> 
streckem@13673
    74
  G \<turnstile> (None, hp0, (stk0,lvars0,C,S, pc0)#frs) -jvm\<rightarrow> 
streckem@13673
    75
  (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs)"
streckem@13673
    76
apply (unfold exec_all_def)
streckem@13673
    77
apply (rule r_into_rtrancl)
streckem@13673
    78
apply (simp add: gis_def gmb_def split_beta)
streckem@13673
    79
done
streckem@13673
    80
streckem@13673
    81
streckem@13673
    82
(***********************************************************************)
streckem@13673
    83
streckem@13673
    84
constdefs
streckem@13673
    85
  progression :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
streckem@13673
    86
                 aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow>
streckem@13673
    87
                 bytecode \<Rightarrow>
streckem@13673
    88
                 aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow> 
streckem@13673
    89
                 bool"
streckem@13673
    90
  ("{_,_,_} \<turnstile> {_, _, _} >- _ \<rightarrow> {_, _, _}" [61,61,61,61,61,61,90,61,61,61]60)
streckem@13673
    91
  "{G,C,S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1} ==
streckem@13673
    92
  \<forall> pre post frs.
streckem@13673
    93
  (gis (gmb G C S) = pre @ instrs @ post) \<longrightarrow>
streckem@13673
    94
   G \<turnstile> (None,hp0,(os0,lvars0,C,S,length pre)#frs) -jvm\<rightarrow>
streckem@13673
    95
       (None,hp1,(os1,lvars1,C,S,(length pre) + (length instrs))#frs)"
streckem@13673
    96
streckem@13673
    97
streckem@13673
    98
streckem@13673
    99
lemma progression_call: 
streckem@13673
   100
  "\<lbrakk> \<forall> pc frs.
streckem@13673
   101
  exec_instr instr G hp0 os0 lvars0 C S pc frs =
streckem@13673
   102
      (None, hp', (os', lvars', C', S', 0) # (fr pc) # frs) \<and> 
streckem@13673
   103
  gis (gmb G C' S') = instrs' @ [Return] \<and> 
streckem@13673
   104
  {G, C', S'} \<turnstile> {hp', os', lvars'} >- instrs' \<rightarrow> {hp'', os'', lvars''}  \<and>
streckem@13673
   105
  exec_instr Return G hp'' os'' lvars'' C' S' (length instrs') 
streckem@13673
   106
                                               ((fr pc) # frs) =
streckem@13673
   107
      (None, hp2, (os2, lvars2, C, S, Suc pc) # frs) \<rbrakk> \<Longrightarrow>
streckem@13673
   108
  {G, C, S} \<turnstile> {hp0, os0, lvars0} >-[instr]\<rightarrow> {hp2,os2,lvars2}"
streckem@13673
   109
apply (simp only: progression_def)
streckem@13673
   110
apply (intro strip)
streckem@13673
   111
apply (drule_tac x="length pre" in spec)
streckem@13673
   112
apply (drule_tac x="frs" in spec)
streckem@13673
   113
apply clarify
streckem@13673
   114
apply (rule exec_all_trans)
streckem@13673
   115
apply (rule exec_instr_in_exec_all) apply simp
streckem@13673
   116
apply simp
streckem@13673
   117
apply (rule exec_all_trans)
streckem@13673
   118
apply (simp only: append_Nil)
streckem@13673
   119
apply (drule_tac x="[]" in spec)
streckem@13673
   120
apply (simp only: list.simps)
streckem@13673
   121
apply blast
streckem@13673
   122
apply (rule exec_instr_in_exec_all)
streckem@13673
   123
apply auto
streckem@13673
   124
done
streckem@13673
   125
streckem@13673
   126
streckem@13673
   127
lemma progression_transitive: 
streckem@13673
   128
  "\<lbrakk> instrs_comb = instrs0 @ instrs1; 
streckem@13673
   129
  {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs0 \<rightarrow> {hp1, os1, lvars1};
streckem@13673
   130
  {G, C, S} \<turnstile> {hp1, os1, lvars1} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk>
streckem@13673
   131
  \<Longrightarrow>
streckem@13673
   132
  {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
streckem@13673
   133
apply (simp only: progression_def)
streckem@13673
   134
apply (intro strip)
ballarin@14174
   135
apply (rule_tac ?s1.0 = "Norm (hp1, (os1, lvars1, C, S, 
streckem@13673
   136
                          length pre + length instrs0) # frs)"  
streckem@13673
   137
       in exec_all_trans)
streckem@13673
   138
apply (simp only: append_assoc)
streckem@13673
   139
apply (erule thin_rl, erule thin_rl)
streckem@13673
   140
apply (drule_tac x="pre @ instrs0" in spec)
streckem@13673
   141
apply (simp add: add_assoc)
streckem@13673
   142
done
streckem@13673
   143
streckem@13673
   144
lemma progression_refl: 
streckem@13673
   145
  "{G, C, S} \<turnstile> {hp0, os0, lvars0} >- [] \<rightarrow> {hp0, os0, lvars0}"
streckem@13673
   146
apply (simp add: progression_def)
streckem@13673
   147
apply (intro strip)
streckem@13673
   148
apply (rule exec_all_refl)
streckem@13673
   149
done
streckem@13673
   150
streckem@13673
   151
lemma progression_one_step: "
streckem@13673
   152
  \<forall> pc frs. 
streckem@13673
   153
  (exec_instr i G hp0 os0 lvars0 C S pc frs) = 
streckem@13673
   154
  (None, hp1, (os1,lvars1,C,S, Suc pc)#frs)
streckem@13673
   155
  \<Longrightarrow> {G, C, S} \<turnstile> {hp0, os0, lvars0} >- [i] \<rightarrow> {hp1, os1, lvars1}"
streckem@13673
   156
apply (unfold progression_def)
streckem@13673
   157
apply (intro strip)
streckem@13673
   158
apply simp
streckem@13673
   159
apply (rule exec_all_one_step)
streckem@13673
   160
apply auto
streckem@13673
   161
done
streckem@13673
   162
streckem@13673
   163
(*****)
streckem@13673
   164
constdefs
streckem@13673
   165
  jump_fwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
streckem@13673
   166
                 aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow> 
streckem@13673
   167
                 instr \<Rightarrow> bytecode \<Rightarrow> bool"
streckem@13673
   168
  "jump_fwd G C S hp lvars os0 os1 instr instrs ==
streckem@13673
   169
  \<forall> pre post frs.
streckem@13673
   170
  (gis (gmb G C S) = pre @ instr # instrs @ post) \<longrightarrow>
streckem@13673
   171
   exec_all G (None,hp,(os0,lvars,C,S, length pre)#frs)
streckem@13673
   172
    (None,hp,(os1,lvars,C,S,(length pre) + (length instrs) + 1)#frs)"
streckem@13673
   173
streckem@13673
   174
streckem@13673
   175
lemma jump_fwd_one_step:
streckem@13673
   176
  "\<forall> pc frs.
streckem@13673
   177
  exec_instr instr G hp os0 lvars C S pc frs = 
streckem@13673
   178
    (None, hp, (os1, lvars, C, S, pc + (length instrs) + 1)#frs)
streckem@13673
   179
  \<Longrightarrow> jump_fwd G C S hp lvars os0 os1 instr instrs"
streckem@13673
   180
apply (unfold jump_fwd_def)
streckem@13673
   181
apply (intro strip)
streckem@13673
   182
apply (rule exec_instr_in_exec_all)
streckem@13673
   183
apply auto
streckem@13673
   184
done
streckem@13673
   185
streckem@13673
   186
streckem@13673
   187
lemma jump_fwd_progression_aux: 
streckem@13673
   188
  "\<lbrakk> instrs_comb = instr # instrs0 @ instrs1; 
streckem@13673
   189
     jump_fwd G C S hp lvars os0 os1 instr instrs0;
streckem@13673
   190
     {G, C, S} \<turnstile> {hp, os1, lvars} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk> 
streckem@13673
   191
  \<Longrightarrow> {G, C, S} \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
streckem@13673
   192
apply (simp only: progression_def jump_fwd_def)
streckem@13673
   193
apply (intro strip)
ballarin@14174
   194
apply (rule_tac ?s1.0 = "Norm(hp, (os1, lvars, C, S, length pre + length instrs0 + 1) # frs)" in exec_all_trans)
streckem@13673
   195
apply (simp only: append_assoc)
streckem@13673
   196
apply (subgoal_tac "pre @ (instr # instrs0 @ instrs1) @ post = pre @ instr # instrs0 @ (instrs1 @ post)")
streckem@13673
   197
apply blast
streckem@13673
   198
apply simp
streckem@13673
   199
apply (erule thin_rl, erule thin_rl)
streckem@13673
   200
apply (drule_tac x="pre @ instr # instrs0" in spec)
streckem@13673
   201
apply (simp add: add_assoc)
streckem@13673
   202
done
streckem@13673
   203
streckem@13673
   204
streckem@13673
   205
lemma jump_fwd_progression:
streckem@13673
   206
  "\<lbrakk> instrs_comb = instr # instrs0 @ instrs1; 
streckem@13673
   207
  \<forall> pc frs.
streckem@13673
   208
  exec_instr instr G hp os0 lvars C S pc frs = 
streckem@13673
   209
    (None, hp, (os1, lvars, C, S, pc + (length instrs0) + 1)#frs);
streckem@13673
   210
  {G, C, S} \<turnstile> {hp, os1, lvars} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk> 
streckem@13673
   211
  \<Longrightarrow> {G, C, S}  \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
streckem@13673
   212
apply (rule jump_fwd_progression_aux)
streckem@13673
   213
apply assumption
streckem@13673
   214
apply (rule jump_fwd_one_step) apply assumption+
streckem@13673
   215
done
streckem@13673
   216
streckem@13673
   217
streckem@13673
   218
(* note: instrs and instr reversed wrt. jump_fwd *)
streckem@13673
   219
constdefs
streckem@13673
   220
  jump_bwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
streckem@13673
   221
                 aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow> 
streckem@13673
   222
                 bytecode \<Rightarrow> instr \<Rightarrow> bool"
streckem@13673
   223
  "jump_bwd G C S hp lvars os0 os1 instrs instr ==
streckem@13673
   224
  \<forall> pre post frs.
streckem@13673
   225
  (gis (gmb G C S) = pre @ instrs @ instr # post) \<longrightarrow>
streckem@13673
   226
   exec_all G (None,hp,(os0,lvars,C,S, (length pre) + (length instrs))#frs)
streckem@13673
   227
    (None,hp,(os1,lvars,C,S, (length pre))#frs)"
streckem@13673
   228
streckem@13673
   229
streckem@13673
   230
lemma jump_bwd_one_step:
streckem@13673
   231
  "\<forall> pc frs.
streckem@13673
   232
  exec_instr instr G hp os0 lvars C S (pc + (length instrs)) frs = 
streckem@13673
   233
    (None, hp, (os1, lvars, C, S, pc)#frs)
streckem@13673
   234
  \<Longrightarrow> 
streckem@13673
   235
  jump_bwd G C S hp lvars os0 os1 instrs instr"
streckem@13673
   236
apply (unfold jump_bwd_def)
streckem@13673
   237
apply (intro strip)
streckem@13673
   238
apply (rule exec_instr_in_exec_all)
streckem@13673
   239
apply auto
streckem@13673
   240
done
streckem@13673
   241
streckem@13673
   242
lemma jump_bwd_progression: 
streckem@13673
   243
  "\<lbrakk> instrs_comb = instrs @ [instr]; 
streckem@13673
   244
  {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1};
streckem@13673
   245
  jump_bwd G C S hp1 lvars1 os1 os2 instrs instr;
streckem@13673
   246
  {G, C, S} \<turnstile> {hp1, os2, lvars1} >- instrs_comb \<rightarrow> {hp3, os3, lvars3} \<rbrakk> 
streckem@13673
   247
  \<Longrightarrow> {G, C, S}  \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp3, os3, lvars3}"
streckem@13673
   248
apply (simp only: progression_def jump_bwd_def)
streckem@13673
   249
apply (intro strip)
streckem@13673
   250
apply (rule exec_all_trans, force)
streckem@13673
   251
apply (rule exec_all_trans, force)
streckem@13673
   252
apply (rule exec_all_trans, force)
streckem@13673
   253
apply simp
streckem@13673
   254
apply (rule exec_all_refl)
streckem@13673
   255
done
streckem@13673
   256
streckem@13673
   257
streckem@13673
   258
(**********************************************************************)
streckem@13673
   259
streckem@13673
   260
(* class C with signature S is defined in program G *)
streckem@13673
   261
constdefs class_sig_defined :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> bool"
streckem@13673
   262
  "class_sig_defined G C S == 
streckem@13673
   263
  is_class G C \<and> (\<exists> D rT mb. (method (G, C) S = Some (D, rT, mb)))"
streckem@13673
   264
streckem@13673
   265
streckem@13673
   266
(* The environment of a java method body 
streckem@13673
   267
  (characterized by class and signature) *)
streckem@13673
   268
constdefs env_of_jmb :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> java_mb env"
streckem@13673
   269
  "env_of_jmb G C S == 
streckem@13673
   270
  (let (mn,pTs) = S;
streckem@13673
   271
       (D,rT,(pns,lvars,blk,res)) = the(method (G, C) S) in
streckem@13673
   272
  (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)))"
streckem@13673
   273
streckem@13673
   274
lemma env_of_jmb_fst [simp]: "fst (env_of_jmb G C S) = G"
streckem@13673
   275
by (simp add: env_of_jmb_def split_beta)
streckem@13673
   276
streckem@13673
   277
streckem@13673
   278
(**********************************************************************)
streckem@13673
   279
streckem@13673
   280
streckem@13673
   281
lemma method_preserves [rule_format (no_asm)]:
streckem@13673
   282
  "\<lbrakk> wf_prog wf_mb G; is_class G C; 
streckem@13673
   283
  \<forall> S rT mb. \<forall> cn \<in> fst ` set G. wf_mdecl wf_mb G cn (S,rT,mb)  \<longrightarrow> (P cn S (rT,mb))\<rbrakk>
streckem@13673
   284
 \<Longrightarrow> \<forall> D. 
streckem@13673
   285
  method (G, C) S = Some (D, rT, mb) \<longrightarrow> (P D S (rT,mb))"
streckem@13673
   286
streckem@14045
   287
apply (frule wf_prog_ws_prog [THEN wf_subcls1])
streckem@13673
   288
apply (rule subcls1_induct, assumption, assumption)
streckem@13673
   289
streckem@13673
   290
apply (intro strip)
streckem@13673
   291
apply ((drule spec)+, drule_tac x="Object" in bspec)
streckem@14045
   292
apply (simp add: wf_prog_def ws_prog_def wf_syscls_def)
streckem@13673
   293
apply (subgoal_tac "D=Object") apply simp
streckem@13673
   294
apply (drule mp)
streckem@13673
   295
apply (frule_tac C=Object in method_wf_mdecl)
streckem@14045
   296
 apply simp
streckem@14045
   297
 apply assumption apply simp apply assumption apply simp
streckem@13673
   298
streckem@13673
   299
apply (subst method_rec) apply simp
streckem@13673
   300
apply force
streckem@14045
   301
apply simp
nipkow@14025
   302
apply (simp only: map_add_def)
streckem@13673
   303
apply (split option.split)
streckem@13673
   304
apply (rule conjI)
streckem@13673
   305
apply force
streckem@13673
   306
apply (intro strip)
streckem@13673
   307
apply (frule_tac
ballarin@14174
   308
  ?P1.0 = "wf_mdecl wf_mb G Ca" and
ballarin@14174
   309
  ?P2.0 = "%(S, (Da, rT, mb)). P Da S (rT, mb)" in map_of_map_prop)
streckem@13673
   310
apply (force simp: wf_cdecl_def)
streckem@13673
   311
streckem@13673
   312
apply clarify
streckem@13673
   313
streckem@13673
   314
apply (simp only: class_def)
streckem@13673
   315
apply (drule map_of_SomeD)+
streckem@13673
   316
apply (frule_tac A="set G" and f=fst in imageI, simp)
streckem@13673
   317
apply blast
streckem@13673
   318
apply simp
streckem@13673
   319
done
streckem@13673
   320
streckem@13673
   321
streckem@13673
   322
lemma method_preserves_length:
streckem@13673
   323
  "\<lbrakk> wf_java_prog G; is_class G C; 
streckem@13673
   324
  method (G, C) (mn,pTs) = Some (D, rT, pns, lvars, blk, res)\<rbrakk>
streckem@13673
   325
 \<Longrightarrow> length pns = length pTs"
streckem@13673
   326
apply (frule_tac 
streckem@13673
   327
  P="%D (mn,pTs) (rT, pns, lvars, blk, res). length pns = length pTs"
streckem@13673
   328
  in method_preserves)
streckem@13673
   329
apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
streckem@13673
   330
done
streckem@13673
   331
streckem@13673
   332
(**********************************************************************)
streckem@13673
   333
streckem@13673
   334
constdefs wtpd_expr :: "java_mb env \<Rightarrow> expr \<Rightarrow> bool"
streckem@13673
   335
  "wtpd_expr E e == (\<exists> T. E\<turnstile>e :: T)"
streckem@13673
   336
  wtpd_exprs :: "java_mb env \<Rightarrow> (expr list) \<Rightarrow> bool"
streckem@13673
   337
  "wtpd_exprs E e == (\<exists> T. E\<turnstile>e [::] T)"
streckem@13673
   338
  wtpd_stmt :: "java_mb env \<Rightarrow> stmt \<Rightarrow> bool" 
streckem@13673
   339
  "wtpd_stmt E c == (E\<turnstile>c \<surd>)"
streckem@13673
   340
streckem@13673
   341
lemma wtpd_expr_newc: "wtpd_expr E (NewC C) \<Longrightarrow> is_class (prg E) C"
streckem@13673
   342
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
streckem@13673
   343
streckem@13673
   344
lemma wtpd_expr_cast: "wtpd_expr E (Cast cn e) \<Longrightarrow> (wtpd_expr E e)"
streckem@13673
   345
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
streckem@13673
   346
streckem@13673
   347
lemma wtpd_expr_lacc: "\<lbrakk> wtpd_expr (env_of_jmb G C S) (LAcc vn);
streckem@13673
   348
  class_sig_defined G C S \<rbrakk>
streckem@13673
   349
  \<Longrightarrow> vn \<in> set (gjmb_plns (gmb G C S)) \<or> vn = This"
streckem@13673
   350
apply (simp only: wtpd_expr_def env_of_jmb_def class_sig_defined_def galldefs)
streckem@13673
   351
apply clarify
streckem@13673
   352
apply (case_tac S)
streckem@13673
   353
apply simp
streckem@13673
   354
apply (erule ty_expr.cases)
streckem@13673
   355
apply (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma)
streckem@13673
   356
apply (drule map_upds_SomeD)
streckem@13673
   357
apply (erule disjE)
streckem@13673
   358
  apply assumption
streckem@13673
   359
  apply (drule map_of_SomeD) apply (auto dest: fst_in_set_lemma)
streckem@13673
   360
done
streckem@13673
   361
streckem@13673
   362
lemma wtpd_expr_lass: "wtpd_expr E (vn::=e)
streckem@13673
   363
  \<Longrightarrow> (vn \<noteq> This) & (wtpd_expr E (LAcc vn)) & (wtpd_expr E e)"
streckem@13673
   364
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
streckem@13673
   365
streckem@13673
   366
lemma wtpd_expr_facc: "wtpd_expr E ({fd}a..fn) 
streckem@13673
   367
  \<Longrightarrow> (wtpd_expr E a)"
streckem@13673
   368
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
streckem@13673
   369
streckem@13673
   370
lemma wtpd_expr_fass: "wtpd_expr E ({fd}a..fn:=v) 
streckem@13673
   371
  \<Longrightarrow> (wtpd_expr E ({fd}a..fn)) & (wtpd_expr E v)"
streckem@13673
   372
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
streckem@13673
   373
streckem@13673
   374
streckem@13673
   375
lemma wtpd_expr_binop: "wtpd_expr E (BinOp bop e1 e2)
streckem@13673
   376
  \<Longrightarrow> (wtpd_expr E e1) & (wtpd_expr E e2)"
streckem@13673
   377
by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
streckem@13673
   378
streckem@13673
   379
lemma wtpd_exprs_cons: "wtpd_exprs E (e # es)
streckem@13673
   380
  \<Longrightarrow> (wtpd_expr E e) & (wtpd_exprs E es)"
streckem@13673
   381
by (simp only: wtpd_exprs_def wtpd_expr_def, erule exE, erule ty_exprs.cases, auto)
streckem@13673
   382
streckem@13673
   383
lemma wtpd_stmt_expr: "wtpd_stmt E (Expr e) \<Longrightarrow> (wtpd_expr E e)"
streckem@13673
   384
by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
streckem@13673
   385
streckem@13673
   386
lemma wtpd_stmt_comp: "wtpd_stmt E (s1;; s2) \<Longrightarrow> 
streckem@13673
   387
   (wtpd_stmt E s1) &  (wtpd_stmt E s2)"
streckem@13673
   388
by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
streckem@13673
   389
streckem@13673
   390
lemma wtpd_stmt_cond: "wtpd_stmt E (If(e) s1 Else s2) \<Longrightarrow>
streckem@13673
   391
   (wtpd_expr E e) & (wtpd_stmt E s1) &  (wtpd_stmt E s2)
streckem@13673
   392
  & (E\<turnstile>e::PrimT Boolean)"
streckem@13673
   393
by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
streckem@13673
   394
streckem@13673
   395
lemma wtpd_stmt_loop: "wtpd_stmt E (While(e) s) \<Longrightarrow>
streckem@13673
   396
   (wtpd_expr E e) & (wtpd_stmt E s) & (E\<turnstile>e::PrimT Boolean)"
streckem@13673
   397
by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
streckem@13673
   398
streckem@13673
   399
lemma wtpd_expr_call: "wtpd_expr E ({C}a..mn({pTs'}ps))
streckem@13673
   400
  \<Longrightarrow> (wtpd_expr E a) & (wtpd_exprs E ps) 
streckem@13673
   401
  & (length ps = length pTs') & (E\<turnstile>a::Class C)
streckem@13673
   402
  & (\<exists> pTs md rT. 
streckem@13673
   403
       E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})"
streckem@13673
   404
apply (simp only: wtpd_expr_def wtpd_exprs_def)
streckem@13673
   405
apply (erule exE)
streckem@13673
   406
apply (ind_cases "E \<turnstile> {C}a..mn( {pTs'}ps) :: T")
streckem@13673
   407
apply (auto simp: max_spec_preserves_length)
streckem@13673
   408
done
streckem@13673
   409
streckem@13673
   410
lemma wtpd_blk: 
streckem@13673
   411
  "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); 
streckem@13673
   412
  wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
streckem@13673
   413
 \<Longrightarrow> wtpd_stmt (env_of_jmb G D (md, pTs)) blk"
streckem@13673
   414
apply (simp add: wtpd_stmt_def env_of_jmb_def)
streckem@13673
   415
apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> blk \<surd> " in method_preserves)
streckem@13673
   416
apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
streckem@13673
   417
done
streckem@13673
   418
streckem@13673
   419
lemma wtpd_res: 
streckem@13673
   420
  "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); 
streckem@13673
   421
  wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
streckem@13673
   422
 \<Longrightarrow> wtpd_expr (env_of_jmb G D (md, pTs)) res"
streckem@13673
   423
apply (simp add: wtpd_expr_def env_of_jmb_def)
streckem@13673
   424
apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \<exists>T. (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> res :: T " in method_preserves)
streckem@13673
   425
apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
streckem@13673
   426
done
streckem@13673
   427
streckem@13673
   428
streckem@13673
   429
(**********************************************************************)
streckem@13673
   430
streckem@13673
   431
streckem@13673
   432
(* Is there a more elegant proof? *)
streckem@13673
   433
lemma evals_preserves_length:
streckem@13673
   434
  "G\<turnstile> xs -es[\<succ>]vs-> (None, s) \<Longrightarrow> length es = length vs"
streckem@13673
   435
apply (subgoal_tac 
streckem@13673
   436
  "\<forall> xs'. (G \<turnstile> xk -xj\<succ>xi-> xh \<longrightarrow> True) & 
streckem@13673
   437
  (G\<turnstile> xs -es[\<succ>]vs-> xs' \<longrightarrow>  (\<exists> s. (xs' = (None, s))) \<longrightarrow> 
streckem@13673
   438
  length es = length vs) &
streckem@13673
   439
  ((xc, xb, xa) \<in> Eval.exec G \<longrightarrow> True)")
streckem@13673
   440
apply blast
streckem@13673
   441
apply (rule allI)
streckem@13673
   442
apply (rule Eval.eval_evals_exec.induct)
streckem@13673
   443
apply auto
streckem@13673
   444
done
streckem@13673
   445
streckem@13673
   446
(***********************************************************************)
streckem@13673
   447
streckem@13673
   448
(* required for translation of BinOp *)
streckem@13673
   449
streckem@13673
   450
streckem@13673
   451
lemma progression_Eq : "{G, C, S} \<turnstile>
streckem@13673
   452
  {hp, (v2 # v1 # os), lvars} 
streckem@13673
   453
  >- [Ifcmpeq 3, LitPush (Bool False), Goto 2, LitPush (Bool True)] \<rightarrow>
streckem@13673
   454
  {hp, (Bool (v1 = v2) # os), lvars}"
streckem@13673
   455
apply (case_tac "v1 = v2")
streckem@13673
   456
streckem@13673
   457
(* case v1 = v2 *)
ballarin@14174
   458
apply (rule_tac ?instrs1.0 = "[LitPush (Bool True)]" in jump_fwd_progression)
paulson@13837
   459
apply (auto simp: nat_add_distrib)
streckem@13673
   460
apply (rule progression_one_step) apply simp
streckem@13673
   461
streckem@13673
   462
(* case v1 \<noteq> v2 *)
streckem@13673
   463
apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified])
streckem@13673
   464
apply auto
streckem@13673
   465
apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) 
streckem@13673
   466
apply auto
ballarin@14174
   467
apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
paulson@13837
   468
apply (auto simp: nat_add_distrib intro: progression_refl)
streckem@13673
   469
done
streckem@13673
   470
streckem@13673
   471
streckem@13673
   472
(**********************************************************************)
streckem@13673
   473
streckem@13673
   474
streckem@13673
   475
(* to avoid automatic pair splits *)
streckem@13673
   476
streckem@13673
   477
declare split_paired_All [simp del] split_paired_Ex [simp del]
streckem@13673
   478
ML_setup {*
streckem@13673
   479
simpset_ref() := simpset() delloop "split_all_tac"
streckem@13673
   480
*}
streckem@13673
   481
streckem@13673
   482
lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C; 
streckem@13673
   483
  method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> 
streckem@13673
   484
  distinct (gjmb_plns (gmb G C S))"
streckem@13673
   485
apply (frule method_wf_mdecl [THEN conjunct2],  assumption, assumption)
streckem@13673
   486
apply (case_tac S)
streckem@13673
   487
apply (simp add: wf_mdecl_def wf_java_mdecl_def galldefs distinct_append)
streckem@13673
   488
apply (simp add: unique_def map_of_in_set)
streckem@13673
   489
apply blast
streckem@13673
   490
done
streckem@13673
   491
streckem@13673
   492
lemma distinct_method_if_class_sig_defined : 
streckem@13673
   493
  "\<lbrakk> wf_java_prog G; class_sig_defined G C S \<rbrakk> \<Longrightarrow> 
streckem@13673
   494
  distinct (gjmb_plns (gmb G C S))"
streckem@13673
   495
by (auto intro: distinct_method simp: class_sig_defined_def)
streckem@13673
   496
streckem@13673
   497
streckem@13673
   498
lemma method_yields_wf_java_mdecl: "\<lbrakk> wf_java_prog G; is_class G C;
streckem@13673
   499
  method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk>  \<Longrightarrow> 
streckem@13673
   500
  wf_java_mdecl G D (S,rT,(pns,lvars,blk,res))"
streckem@13673
   501
apply (frule method_wf_mdecl)
streckem@13673
   502
apply (auto simp: wf_mdecl_def)
streckem@13673
   503
done
streckem@13673
   504
streckem@13673
   505
(**********************************************************************)
streckem@13673
   506
streckem@13673
   507
streckem@13673
   508
lemma progression_lvar_init_aux [rule_format (no_asm)]: "
streckem@13673
   509
  \<forall> zs prfx lvals lvars0. 
streckem@13673
   510
  lvars0 =  (zs @ lvars) \<longrightarrow>
streckem@13673
   511
  (disjoint_varnames pns lvars0 \<longrightarrow>
streckem@13673
   512
  (length lvars = length lvals) \<longrightarrow> 
streckem@13673
   513
  (Suc(length pns + length zs) = length prfx) \<longrightarrow> 
streckem@13673
   514
   ({cG, D, S} \<turnstile> 
streckem@13673
   515
    {h, os, (prfx @ lvals)}
streckem@13673
   516
    >- (concat (map (compInit (pns, lvars0, blk, res)) lvars)) \<rightarrow>
streckem@13673
   517
    {h, os, (prfx @ (map (\<lambda>p. (default_val (snd p))) lvars))}))"
streckem@13673
   518
apply simp
streckem@13673
   519
apply (induct lvars)
streckem@13673
   520
apply (clarsimp, rule progression_refl)
streckem@13673
   521
apply (intro strip)
streckem@13673
   522
apply (case_tac lvals) apply simp
streckem@13673
   523
apply (simp (no_asm_simp) )
streckem@13673
   524
ballarin@14174
   525
apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
streckem@13673
   526
apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def)
ballarin@14174
   527
apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
streckem@13673
   528
apply (rule progression_one_step)
streckem@13673
   529
apply (simp (no_asm_simp) add: load_default_val_def)
streckem@13673
   530
apply (rule conjI, simp)+ apply (rule HOL.refl)
streckem@13673
   531
streckem@13673
   532
apply (rule progression_one_step)
streckem@13673
   533
apply (simp (no_asm_simp))
streckem@13673
   534
apply (rule conjI, simp)+
streckem@13673
   535
apply (simp add: index_of_var2)
streckem@13673
   536
apply (drule_tac x="zs @ [a]" in spec) (* instantiate zs *)
streckem@13673
   537
apply (drule mp, simp)
streckem@13673
   538
apply (drule_tac x="(prfx @ [default_val (snd a)])" in spec) (* instantiate prfx *)
streckem@13673
   539
apply auto
streckem@13673
   540
done
streckem@13673
   541
streckem@13673
   542
lemma progression_lvar_init [rule_format (no_asm)]: 
streckem@13673
   543
  "\<lbrakk> wf_java_prog G; is_class G C;
streckem@13673
   544
  method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> 
streckem@13673
   545
  length pns = length pvs \<longrightarrow> 
streckem@13673
   546
  (\<forall> lvals. 
streckem@13673
   547
  length lvars = length lvals \<longrightarrow>
streckem@13673
   548
   {cG, D, S} \<turnstile>
streckem@13673
   549
   {h, os, (a' # pvs @ lvals)}
streckem@13673
   550
   >- (compInitLvars (pns, lvars, blk, res) lvars) \<rightarrow>
streckem@13673
   551
   {h, os, (locvars_xstate G C S (Norm (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))))})"
streckem@13673
   552
apply (simp only: compInitLvars_def)
streckem@13673
   553
apply (frule method_yields_wf_java_mdecl, assumption, assumption)
streckem@13673
   554
streckem@13673
   555
apply (simp only: wf_java_mdecl_def)
streckem@13673
   556
apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))")
streckem@13673
   557
apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd)
streckem@13673
   558
apply (intro strip)
streckem@13673
   559
apply (simp (no_asm_simp) only: append_Cons [THEN sym])
streckem@13673
   560
apply (rule progression_lvar_init_aux)
streckem@13673
   561
apply (auto simp: unique_def map_of_in_set disjoint_varnames_def)
streckem@13673
   562
done
streckem@13673
   563
streckem@13673
   564
streckem@13673
   565
streckem@13673
   566
streckem@13673
   567
(**********************************************************************)
streckem@13673
   568
streckem@14045
   569
lemma state_ok_eval: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_expr E e;
streckem@14045
   570
  (prg E)\<turnstile>xs -e\<succ>v -> xs'\<rbrakk> \<Longrightarrow>  xs'::\<preceq>E"
streckem@14045
   571
apply (simp only: wtpd_expr_def)
streckem@13673
   572
apply (erule exE)
streckem@14045
   573
apply (case_tac xs', case_tac xs)
streckem@14045
   574
apply (auto intro: eval_type_sound [THEN conjunct1])
streckem@13673
   575
done
streckem@13673
   576
streckem@14045
   577
lemma state_ok_evals: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_exprs E es;
streckem@14045
   578
  (xs,es,vs,xs') \<in> Eval.evals (prg E)\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
streckem@14045
   579
apply (simp only: wtpd_exprs_def)
streckem@14045
   580
apply (erule exE)
streckem@14045
   581
apply (case_tac xs) apply (case_tac xs')
streckem@14045
   582
apply (auto intro: evals_type_sound [THEN conjunct1])
streckem@13673
   583
done
streckem@13673
   584
streckem@14045
   585
lemma state_ok_exec: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_stmt E st;
streckem@14045
   586
  (xs,st,xs') \<in> Eval.exec (prg E)\<rbrakk> \<Longrightarrow>  xs'::\<preceq>E"
streckem@14045
   587
apply (simp only: wtpd_stmt_def)
streckem@14045
   588
apply (case_tac xs', case_tac xs)
streckem@14143
   589
apply (auto dest: exec_type_sound)
streckem@13673
   590
done
streckem@13673
   591
streckem@13673
   592
streckem@13673
   593
lemma state_ok_init: 
streckem@14045
   594
  "\<lbrakk> wf_java_prog G; (x, h, l)::\<preceq>(env_of_jmb G C S); 
streckem@13673
   595
  is_class G dynT;
streckem@13673
   596
  method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res);
streckem@13673
   597
  list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk>
streckem@13673
   598
\<Longrightarrow>
streckem@14045
   599
(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))"
streckem@14045
   600
apply (frule wf_prog_ws_prog)
streckem@13673
   601
apply (frule method_in_md [THEN conjunct2], assumption+)
streckem@13673
   602
apply (frule method_yields_wf_java_mdecl, assumption, assumption)
streckem@14045
   603
apply (simp add: env_of_jmb_def gs_def conforms_def split_beta)
streckem@13673
   604
apply (simp add: wf_java_mdecl_def)
streckem@13673
   605
apply (rule conjI)
streckem@13673
   606
apply (rule lconf_ext)
streckem@13673
   607
apply (rule lconf_ext_list)
streckem@13673
   608
apply (rule lconf_init_vars)
streckem@13673
   609
apply (auto dest: Ball_set_table)
streckem@13673
   610
apply (simp add: np_def xconf_raise_if)
streckem@13673
   611
done
streckem@13673
   612
streckem@13673
   613
streckem@13673
   614
lemma ty_exprs_list_all2 [rule_format (no_asm)]: 
streckem@13673
   615
  "(\<forall> Ts. (E \<turnstile> es [::] Ts) = list_all2 (\<lambda>e T. E \<turnstile> e :: T) es Ts)"
streckem@13673
   616
apply (rule list.induct)
streckem@13673
   617
apply simp
streckem@13673
   618
apply (rule allI)
streckem@13673
   619
apply (rule iffI)
streckem@13673
   620
  apply (ind_cases "E \<turnstile> [] [::] Ts", assumption)
streckem@13673
   621
  apply simp apply (rule WellType.Nil)
streckem@13673
   622
apply (simp add: list_all2_Cons1)
streckem@13673
   623
apply (rule allI)
streckem@13673
   624
apply (rule iffI)
streckem@13673
   625
  apply (rename_tac a exs Ts)
streckem@13673
   626
  apply (ind_cases "E \<turnstile> a # exs  [::] Ts") apply blast
streckem@13673
   627
  apply (auto intro: WellType.Cons)
streckem@13673
   628
done
streckem@13673
   629
streckem@13673
   630
streckem@13673
   631
lemma conf_bool: "G,h \<turnstile> v::\<preceq>PrimT Boolean \<Longrightarrow> \<exists> b. v = Bool b"
streckem@13673
   632
apply (simp add: conf_def)
streckem@13673
   633
apply (erule exE)
streckem@13673
   634
apply (case_tac v)
streckem@13673
   635
apply (auto elim: widen.cases)
streckem@13673
   636
done
streckem@13673
   637
streckem@13673
   638
streckem@14045
   639
lemma class_expr_is_class: "\<lbrakk>E \<turnstile> e :: Class C; ws_prog (prg E)\<rbrakk> 
streckem@13673
   640
  \<Longrightarrow> is_class (prg E) C"
streckem@13673
   641
by (case_tac E, auto dest: ty_expr_is_type)
streckem@13673
   642
streckem@13673
   643
streckem@13673
   644
lemma max_spec_widen: "max_spec G C (mn, pTs) = {((md,rT),pTs')} \<Longrightarrow> 
streckem@13673
   645
  list_all2 (\<lambda> T T'. G \<turnstile> T \<preceq> T') pTs pTs'"
streckem@13673
   646
by (blast dest: singleton_in_set max_spec2appl_meths appl_methsD)
streckem@13673
   647
streckem@13673
   648
streckem@14045
   649
lemma eval_conf: "\<lbrakk>G \<turnstile> s -e\<succ>v-> s'; wf_java_prog G; s::\<preceq>E;
streckem@13673
   650
  E\<turnstile>e::T; gx s' = None; prg E = G \<rbrakk> 
streckem@13673
   651
  \<Longrightarrow> G,gh s'\<turnstile>v::\<preceq>T"
streckem@13673
   652
apply (simp add: gh_def)
ballarin@14174
   653
apply (rule_tac x3="fst s" and s3="snd s"and x'3="fst s'"  
streckem@14143
   654
  in eval_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]], simplified])
streckem@14143
   655
apply assumption+
streckem@13673
   656
apply (simp (no_asm_use) add: surjective_pairing [THEN sym])
streckem@14045
   657
apply (simp only: surjective_pairing [THEN sym])
streckem@14045
   658
apply (auto simp add: gs_def gx_def)
streckem@13673
   659
done
streckem@13673
   660
streckem@13673
   661
lemma evals_preserves_conf:
streckem@13673
   662
  "\<lbrakk> G\<turnstile> s -es[\<succ>]vs-> s'; G,gh s \<turnstile> t ::\<preceq> T; E \<turnstile>es[::]Ts;
streckem@14045
   663
  wf_java_prog G; s::\<preceq>E; 
streckem@13673
   664
  prg E = G \<rbrakk> \<Longrightarrow> G,gh s' \<turnstile> t ::\<preceq> T"
streckem@13673
   665
apply (subgoal_tac "gh s\<le>| gh s'")
streckem@13673
   666
apply (frule conf_hext, assumption, assumption)
streckem@13673
   667
apply (frule eval_evals_exec_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]]]) 
streckem@13673
   668
apply (subgoal_tac "G \<turnstile> (gx s, (gh s, gl s)) -es[\<succ>]vs-> (gx s', (gh s', gl s'))")
streckem@13673
   669
apply assumption
streckem@13673
   670
apply (simp add: gx_def gh_def gl_def surjective_pairing [THEN sym])
streckem@13673
   671
apply (case_tac E)
streckem@14045
   672
apply (simp add: gx_def gs_def gh_def gl_def surjective_pairing [THEN sym])
streckem@13673
   673
done
streckem@13673
   674
streckem@13673
   675
lemma eval_of_class: "\<lbrakk> G \<turnstile> s -e\<succ>a'-> s'; E \<turnstile> e :: Class C; 
streckem@14045
   676
  wf_java_prog G; s::\<preceq>E; gx s'=None; a' \<noteq> Null; G=prg E\<rbrakk>
streckem@13673
   677
  \<Longrightarrow> (\<exists> lc. a' = Addr lc)"
streckem@13673
   678
apply (case_tac s, case_tac s', simp)
streckem@14045
   679
apply (frule eval_type_sound, (simp add: gs_def)+)
streckem@13673
   680
apply (case_tac a')
streckem@13673
   681
apply (auto simp: conf_def)
streckem@13673
   682
done
streckem@13673
   683
streckem@13673
   684
streckem@13673
   685
lemma dynT_subcls: 
streckem@13673
   686
  "\<lbrakk> a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; dynT = fst (the (h (the_Addr a')));
streckem@14045
   687
  is_class G dynT; ws_prog G \<rbrakk> \<Longrightarrow> G\<turnstile>dynT \<preceq>C C"
streckem@13673
   688
apply (case_tac "C = Object")
streckem@13673
   689
apply (simp, rule subcls_C_Object, assumption+)
streckem@14045
   690
apply simp
streckem@13673
   691
apply (frule non_np_objD, auto)
streckem@13673
   692
done
streckem@13673
   693
streckem@13673
   694
streckem@13673
   695
lemma method_defined: "\<lbrakk> 
streckem@13673
   696
  m = the (method (G, dynT) (mn, pTs)); 
streckem@13673
   697
  dynT = fst (the (h a)); is_class G dynT; wf_java_prog G; 
streckem@13673
   698
  a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; a = the_Addr a';
streckem@13673
   699
  \<exists>pTsa md rT. max_spec G C (mn, pTsa) = {((md, rT), pTs)} \<rbrakk>
streckem@13673
   700
\<Longrightarrow> (method (G, dynT) (mn, pTs)) = Some m"
streckem@13673
   701
apply (erule exE)+
streckem@13673
   702
apply (drule singleton_in_set, drule max_spec2appl_meths)
streckem@13673
   703
apply (simp add: appl_methds_def)
streckem@13673
   704
apply ((erule exE)+, (erule conjE)+, (erule exE)+)
streckem@13673
   705
apply (drule widen_methd)
streckem@13673
   706
apply assumption
streckem@14045
   707
apply (rule dynT_subcls) apply assumption+ apply simp apply simp
streckem@13673
   708
apply (erule exE)+ apply simp
streckem@13673
   709
done
streckem@13673
   710
streckem@13673
   711
streckem@13673
   712
streckem@13673
   713
(**********************************************************************)
streckem@13673
   714
streckem@13673
   715
streckem@13673
   716
(* 1. any difference between locvars_xstate \<dots> and L ??? *)
streckem@13673
   717
(* 2. possibly skip env_of_jmb ??? *)
streckem@13673
   718
theorem compiler_correctness: 
streckem@13673
   719
  "wf_java_prog G \<Longrightarrow>
streckem@13673
   720
  ((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow>
streckem@13673
   721
  gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
streckem@13673
   722
  (\<forall> os CL S.
streckem@13673
   723
  (class_sig_defined G CL S) \<longrightarrow> 
streckem@13673
   724
  (wtpd_expr (env_of_jmb G CL S) ex) \<longrightarrow>
streckem@14045
   725
  (xs ::\<preceq> (env_of_jmb G CL S)) \<longrightarrow>
streckem@13673
   726
  ( {TranslComp.comp G, CL, S} \<turnstile>
streckem@13673
   727
    {gh xs, os, (locvars_xstate G CL S xs)}
streckem@13673
   728
    >- (compExpr (gmb G CL S) ex) \<rightarrow>
streckem@13673
   729
    {gh xs', val#os, locvars_xstate G CL S xs'}))) \<and> 
streckem@13673
   730
streckem@13673
   731
 ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow>
streckem@13673
   732
  gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
streckem@13673
   733
  (\<forall> os CL S.
streckem@13673
   734
  (class_sig_defined G CL S) \<longrightarrow> 
streckem@13673
   735
  (wtpd_exprs (env_of_jmb G CL S) exs) \<longrightarrow>
streckem@14045
   736
  (xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow>
streckem@13673
   737
  ( {TranslComp.comp G, CL, S} \<turnstile>
streckem@13673
   738
    {gh xs, os, (locvars_xstate G CL S xs)}
streckem@13673
   739
    >- (compExprs (gmb G CL S) exs) \<rightarrow>
streckem@13673
   740
    {gh xs', (rev vals)@os, (locvars_xstate G CL S xs')}))) \<and> 
streckem@13673
   741
streckem@13673
   742
  ((xs,st,xs') \<in> Eval.exec G \<longrightarrow>
streckem@13673
   743
   gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
streckem@13673
   744
  (\<forall> os CL S.
streckem@13673
   745
  (class_sig_defined G CL S) \<longrightarrow> 
streckem@13673
   746
  (wtpd_stmt (env_of_jmb G CL S) st) \<longrightarrow>
streckem@14045
   747
  (xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow>
streckem@13673
   748
  ( {TranslComp.comp G, CL, S} \<turnstile>
streckem@13673
   749
    {gh xs, os, (locvars_xstate G CL S xs)}
streckem@13673
   750
    >- (compStmt (gmb G CL S) st) \<rightarrow>
streckem@13673
   751
    {gh xs', os, (locvars_xstate G CL S xs')})))"
streckem@13673
   752
apply (rule Eval.eval_evals_exec.induct)
streckem@13673
   753
streckem@13673
   754
(* case XcptE *)
streckem@13673
   755
apply simp
streckem@13673
   756
streckem@13673
   757
(* case NewC *) 
streckem@14045
   758
apply clarify 
streckem@14045
   759
apply (frule wf_prog_ws_prog [THEN wf_subcls1]) (* establish  wf ((subcls1 G)^-1) *)
streckem@13673
   760
apply (simp add: c_hupd_hp_invariant)
streckem@13673
   761
apply (rule progression_one_step)
streckem@13673
   762
apply (rotate_tac 1, drule sym) (* reverse equation (a, None) = new_Addr (fst s) *)
streckem@13673
   763
apply (simp add: locvars_xstate_def locvars_locals_def comp_fields)
streckem@13673
   764
streckem@13673
   765
streckem@13673
   766
(* case Cast *)
streckem@13673
   767
apply (intro allI impI)
streckem@13673
   768
apply simp
streckem@13673
   769
apply (frule raise_if_NoneD)
streckem@13673
   770
apply (frule wtpd_expr_cast)
streckem@13673
   771
apply simp
ballarin@14174
   772
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, simp)
streckem@13673
   773
apply blast
streckem@13673
   774
apply (rule progression_one_step)
streckem@13673
   775
apply (simp add: raise_system_xcpt_def  gh_def comp_cast_ok)
streckem@13673
   776
streckem@13673
   777
streckem@13673
   778
(* case Lit *)
streckem@13673
   779
apply simp
streckem@13673
   780
apply (intro strip)
streckem@13673
   781
apply (rule progression_one_step)
streckem@13673
   782
apply simp
streckem@13673
   783
streckem@13673
   784
streckem@13673
   785
(* case BinOp *)
streckem@13673
   786
apply (intro allI impI)
streckem@13673
   787
apply (frule_tac xs=s1 in eval_xcpt, assumption) (* establish (gx s1 = None) *)
streckem@13673
   788
apply (frule wtpd_expr_binop)
streckem@14045
   789
(* establish (s1::\<preceq> \<dots>) *)
streckem@13673
   790
apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp)) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) 
streckem@13673
   791
streckem@13673
   792
streckem@13673
   793
apply (simp (no_asm_use) only: compExpr_compExprs.simps)
ballarin@14174
   794
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast
ballarin@14174
   795
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast
streckem@13673
   796
apply (case_tac bop)
streckem@13673
   797
  (*subcase bop = Eq *)  apply simp apply (rule progression_Eq)
streckem@13673
   798
  (*subcase bop = Add *) apply simp apply (rule progression_one_step) apply simp
streckem@13673
   799
streckem@13673
   800
streckem@13673
   801
(* case LAcc *)
streckem@13673
   802
apply simp
streckem@13673
   803
apply (intro strip)
streckem@13673
   804
apply (rule progression_one_step)
streckem@13673
   805
apply (simp add: locvars_xstate_def locvars_locals_def)
streckem@13673
   806
apply (frule wtpd_expr_lacc)
streckem@13673
   807
apply assumption
streckem@13673
   808
apply (simp add: gl_def)
streckem@13673
   809
apply (erule select_at_index)
streckem@13673
   810
streckem@13673
   811
streckem@13673
   812
(* case LAss *)
streckem@13673
   813
apply (intro allI impI)
streckem@13673
   814
apply (frule wtpd_expr_lass, erule conjE, erule conjE)
streckem@13673
   815
apply (simp add: compExpr_compExprs.simps)
streckem@13673
   816
ballarin@14174
   817
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
streckem@13673
   818
apply blast
streckem@13673
   819
ballarin@14174
   820
apply (rule_tac ?instrs0.0 = "[Dup]" in progression_transitive, simp)
streckem@13673
   821
apply (rule progression_one_step)
streckem@13673
   822
apply (simp add: gh_def)
streckem@13673
   823
apply (rule conjI, simp)+ apply simp
streckem@13673
   824
apply (rule progression_one_step)
streckem@13673
   825
apply (simp add: gh_def)
streckem@13673
   826
(* the following falls out of the general scheme *)
streckem@13673
   827
apply (frule wtpd_expr_lacc) apply assumption
streckem@13673
   828
apply (rule update_at_index)
streckem@13673
   829
apply (rule distinct_method_if_class_sig_defined) apply assumption
streckem@13673
   830
apply assumption apply simp apply assumption
streckem@13673
   831
streckem@13673
   832
streckem@13673
   833
(* case FAcc *)
streckem@13673
   834
apply (intro allI impI)
streckem@13673
   835
   (* establish x1 = None \<and> a' \<noteq> Null *)
streckem@13673
   836
apply (simp (no_asm_use) only: gx_conv, frule np_NoneD)
streckem@13673
   837
apply (frule wtpd_expr_facc)
streckem@13673
   838
streckem@13673
   839
apply (simp (no_asm_use) only: compExpr_compExprs.simps)
ballarin@14174
   840
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
streckem@13673
   841
apply blast
streckem@13673
   842
apply (rule progression_one_step)
streckem@13673
   843
apply (simp add: gh_def)
streckem@13673
   844
apply (case_tac "(the (fst s1 (the_Addr a')))")
streckem@13673
   845
apply (simp add: raise_system_xcpt_def)
streckem@13673
   846
streckem@13673
   847
streckem@13673
   848
(* case FAss *)
streckem@13673
   849
apply (intro allI impI)
streckem@13673
   850
apply (frule wtpd_expr_fass) apply (erule conjE) apply (frule wtpd_expr_facc)
streckem@13673
   851
apply (simp only: c_hupd_xcpt_invariant) (* establish x2 = None *)
streckem@13673
   852
   (* establish x1 = None  and  a' \<noteq> Null  *)
streckem@13673
   853
apply (frule_tac xs="(np a' x1, s1)" in eval_xcpt)
streckem@13673
   854
apply (simp only: gx_conv, simp only: gx_conv, frule np_NoneD, erule conjE)
streckem@13673
   855
streckem@13673
   856
streckem@14045
   857
  (* establish ((Norm s1)::\<preceq> \<dots>) *)
streckem@14045
   858
apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) 
streckem@14045
   859
   apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) 
streckem@13673
   860
streckem@13673
   861
apply (simp only: compExpr_compExprs.simps)
streckem@13673
   862
ballarin@14174
   863
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl)
streckem@13673
   864
apply fast (* blast does not seem to work - why? *)
ballarin@14174
   865
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl)
streckem@13673
   866
apply fast
ballarin@14174
   867
apply (rule_tac ?instrs0.0 = "[Dup_x1]" and ?instrs1.0 = "[Putfield fn T]" in progression_transitive, simp)
streckem@13673
   868
streckem@13673
   869
   (* Dup_x1 *)
streckem@13673
   870
   apply (rule progression_one_step)
streckem@13673
   871
   apply (simp add: gh_def)
streckem@13673
   872
   apply (rule conjI, simp)+ apply simp
streckem@13673
   873
streckem@13673
   874
streckem@13673
   875
   (* Putfield \<longrightarrow> still looks nasty*)
streckem@13673
   876
   apply (rule progression_one_step)
streckem@13673
   877
   apply simp
streckem@13673
   878
   apply (case_tac "(the (fst s2 (the_Addr a')))")
streckem@13673
   879
   apply (simp add: c_hupd_hp_invariant)
streckem@13673
   880
   apply (case_tac s2)
streckem@13673
   881
   apply (simp add: c_hupd_conv raise_system_xcpt_def)
streckem@13673
   882
   apply (rule locvars_xstate_par_dep, rule HOL.refl)
streckem@13673
   883
streckem@13673
   884
defer (* method call *)
streckem@13673
   885
streckem@13673
   886
(* case XcptEs *)
streckem@13673
   887
apply simp
streckem@13673
   888
streckem@13673
   889
(* case Nil *)
streckem@13673
   890
apply (simp add: compExpr_compExprs.simps)
streckem@13673
   891
apply (intro strip)
streckem@13673
   892
apply (rule progression_refl)
streckem@13673
   893
streckem@13673
   894
(* case Cons *)
streckem@13673
   895
apply (intro allI impI)
streckem@13673
   896
apply (frule_tac xs=s1 in evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *)
streckem@13673
   897
apply (frule wtpd_exprs_cons)
streckem@14045
   898
   (* establish ((Norm s0)::\<preceq> \<dots>) *)
streckem@13673
   899
apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
streckem@13673
   900
streckem@13673
   901
apply simp
ballarin@14174
   902
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
streckem@13673
   903
apply fast
streckem@13673
   904
apply fast
streckem@13673
   905
streckem@13673
   906
streckem@13673
   907
(* case Statement: exception *)
streckem@13673
   908
apply simp
streckem@13673
   909
streckem@13673
   910
(* case Skip *)
streckem@13673
   911
apply (intro allI impI)
streckem@13673
   912
apply simp
streckem@13673
   913
apply (rule progression_refl)
streckem@13673
   914
streckem@13673
   915
(* case Expr *)
streckem@13673
   916
apply (intro allI impI)
streckem@13673
   917
apply (frule wtpd_stmt_expr)
streckem@13673
   918
apply simp
ballarin@14174
   919
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
streckem@13673
   920
apply fast
streckem@13673
   921
apply (rule progression_one_step)
streckem@13673
   922
apply simp
streckem@13673
   923
streckem@13673
   924
(* case Comp *)
streckem@13673
   925
apply (intro allI impI)
streckem@13673
   926
apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
streckem@13673
   927
apply (frule wtpd_stmt_comp)
streckem@13673
   928
streckem@14045
   929
  (* establish (s1::\<preceq> \<dots>) *)
streckem@13673
   930
apply (frule_tac st=c1 in state_ok_exec) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
streckem@13673
   931
streckem@13673
   932
apply simp
ballarin@14174
   933
apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, rule HOL.refl)
streckem@13673
   934
apply fast
streckem@13673
   935
apply fast
streckem@13673
   936
streckem@13673
   937
streckem@13673
   938
(* case Cond *)
streckem@13673
   939
apply (intro allI impI)
streckem@13673
   940
apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
streckem@13673
   941
apply (frule wtpd_stmt_cond, (erule conjE)+)
streckem@14045
   942
(* establish (s1::\<preceq> \<dots>) *)
streckem@13673
   943
apply (frule_tac e=e in state_ok_eval) 
streckem@13673
   944
apply (simp (no_asm_simp) only: env_of_jmb_fst)
streckem@13673
   945
apply assumption 
streckem@13673
   946
apply (simp (no_asm_use) only: env_of_jmb_fst) 
streckem@13673
   947
(* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
streckem@13673
   948
apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
streckem@13673
   949
apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
streckem@13673
   950
apply (erule exE)
streckem@13673
   951
streckem@13673
   952
apply simp
ballarin@14174
   953
apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
streckem@13673
   954
apply (rule progression_one_step,  simp)
streckem@13673
   955
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
streckem@13673
   956
ballarin@14174
   957
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
streckem@13673
   958
apply fast
streckem@13673
   959
streckem@13673
   960
apply (case_tac b)
streckem@13673
   961
 (* case b= True *)
streckem@13673
   962
apply simp
ballarin@14174
   963
apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
streckem@13673
   964
apply (rule progression_one_step) apply simp
streckem@13673
   965
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
ballarin@14174
   966
apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
streckem@13673
   967
apply fast
ballarin@14174
   968
apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
streckem@13673
   969
apply (simp, rule conjI, (rule HOL.refl)+)
paulson@13837
   970
apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
streckem@13673
   971
apply (rule progression_refl)
streckem@13673
   972
streckem@13673
   973
 (* case b= False *)
streckem@13673
   974
apply simp
ballarin@14174
   975
apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
streckem@13673
   976
apply (simp, rule conjI, (rule HOL.refl)+)
paulson@13837
   977
apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
streckem@13673
   978
apply fast
streckem@13673
   979
streckem@13673
   980
(* case exit Loop *)
streckem@13673
   981
apply (intro allI impI)
streckem@13673
   982
apply (frule wtpd_stmt_loop, (erule conjE)+)
streckem@13673
   983
streckem@13673
   984
(* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
streckem@13673
   985
apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
streckem@13673
   986
apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
streckem@13673
   987
apply (erule exE)
streckem@13673
   988
apply (case_tac b)
streckem@13673
   989
streckem@13673
   990
 (* case b= True \<longrightarrow> contradiction *)
streckem@13673
   991
apply simp
streckem@13673
   992
streckem@13673
   993
 (* case b= False *)
streckem@13673
   994
apply simp
streckem@13673
   995
ballarin@14174
   996
apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
streckem@13673
   997
apply (rule progression_one_step)
streckem@13673
   998
   apply simp 
streckem@13673
   999
   apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
streckem@13673
  1000
ballarin@14174
  1001
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
streckem@13673
  1002
apply fast
ballarin@14174
  1003
apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
streckem@13673
  1004
apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
paulson@13837
  1005
apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
streckem@13673
  1006
apply (rule progression_refl)
streckem@13673
  1007
streckem@13673
  1008
streckem@13673
  1009
(* case continue Loop *)
streckem@13673
  1010
apply (intro allI impI)
streckem@13673
  1011
apply (frule_tac xs=s2 in exec_xcpt, assumption) (* establish (gx s2 = None) *)
streckem@13673
  1012
apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
streckem@13673
  1013
apply (frule wtpd_stmt_loop, (erule conjE)+)
streckem@13673
  1014
streckem@14045
  1015
(* establish (s1::\<preceq> \<dots>) *)
streckem@13673
  1016
apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
streckem@14045
  1017
(* establish (s2::\<preceq> \<dots>) *)
streckem@13673
  1018
apply (frule_tac xs=s1 and st=c in state_ok_exec)
streckem@13673
  1019
apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
streckem@13673
  1020
streckem@13673
  1021
(* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
streckem@13673
  1022
apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
streckem@13673
  1023
apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
streckem@13673
  1024
apply (erule exE)
streckem@13673
  1025
streckem@13673
  1026
apply simp
streckem@13673
  1027
apply (rule jump_bwd_progression) 
streckem@13673
  1028
apply simp
streckem@13673
  1029
apply (rule conjI, (rule HOL.refl)+)
streckem@13673
  1030
ballarin@14174
  1031
apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
streckem@13673
  1032
apply (rule progression_one_step)
streckem@13673
  1033
   apply simp 
streckem@13673
  1034
   apply (rule conjI, simp)+ apply simp
streckem@13673
  1035
ballarin@14174
  1036
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
streckem@13673
  1037
apply fast
streckem@13673
  1038
streckem@13673
  1039
apply (case_tac b)
streckem@13673
  1040
 (* case b= True *)
streckem@13673
  1041
apply simp
streckem@13673
  1042
ballarin@14174
  1043
apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
streckem@13673
  1044
apply (rule progression_one_step) apply simp
streckem@13673
  1045
apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
streckem@13673
  1046
apply fast
streckem@13673
  1047
streckem@13673
  1048
 (* case b= False \<longrightarrow> contradiction*)
streckem@13673
  1049
apply simp
streckem@13673
  1050
streckem@13673
  1051
apply (rule jump_bwd_one_step)
streckem@13673
  1052
apply simp
streckem@13673
  1053
apply blast
streckem@13673
  1054
streckem@13673
  1055
(*****)
streckem@14045
  1056
(* case method call *)
streckem@13673
  1057
streckem@13673
  1058
apply (intro allI impI)
streckem@13673
  1059
streckem@13673
  1060
apply (frule_tac xs=s3 in eval_xcpt, simp only: gx_conv) (* establish gx s3 = None *)
streckem@13673
  1061
apply (frule exec_xcpt, assumption, simp (no_asm_use) only: gx_conv, frule np_NoneD) (* establish x = None \<and> a' \<noteq> Null *)
streckem@13673
  1062
apply (frule evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *)
streckem@13673
  1063
streckem@13673
  1064
apply (frule wtpd_expr_call, (erule conjE)+)
streckem@13673
  1065
streckem@13673
  1066
streckem@13673
  1067
(* assumptions about state_ok and is_class *)
streckem@13673
  1068
streckem@14045
  1069
(* establish s1::\<preceq> (env_of_jmb G CL S) *)
streckem@13673
  1070
apply (frule_tac xs="Norm s0" and e=e in state_ok_eval)
streckem@13673
  1071
apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp (no_asm_use) only: env_of_jmb_fst)
streckem@13673
  1072
streckem@14045
  1073
(* establish (x, h, l)::\<preceq>(env_of_jmb G CL S) *)
streckem@13673
  1074
apply (frule_tac xs=s1 and xs'="(x, h, l)" in state_ok_evals)
streckem@13673
  1075
apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst)
streckem@13673
  1076
streckem@13673
  1077
(* establish \<exists> lc. a' = Addr lc *)
streckem@13673
  1078
apply (frule (5) eval_of_class, rule env_of_jmb_fst [THEN sym])
streckem@13673
  1079
apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class C")
streckem@13673
  1080
apply (subgoal_tac "is_class G dynT")
streckem@13673
  1081
streckem@13673
  1082
(* establish method (G, dynT) (mn, pTs) = Some(md, rT, pns, lvars, blk, res) *)
streckem@13673
  1083
apply (drule method_defined, assumption+)
streckem@13673
  1084
apply (simp only: env_of_jmb_fst)
streckem@13673
  1085
apply ((erule exE)+, erule conjE, (rule exI)+, assumption) 
streckem@13673
  1086
streckem@13673
  1087
apply (subgoal_tac "is_class G md")
streckem@13673
  1088
apply (subgoal_tac "G\<turnstile>Class dynT \<preceq> Class md")
streckem@13673
  1089
apply (subgoal_tac " method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res)")
streckem@13673
  1090
apply (subgoal_tac "list_all2 (conf G h) pvs pTs")
streckem@13673
  1091
streckem@14045
  1092
(* establish (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs)) *)
streckem@13673
  1093
apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class dynT")
streckem@13673
  1094
apply (frule (2) conf_widen)
streckem@13673
  1095
apply (frule state_ok_init, assumption+)
streckem@13673
  1096
streckem@13673
  1097
apply (subgoal_tac "class_sig_defined G md (mn, pTs)")
streckem@13673
  1098
apply (frule wtpd_blk, assumption, assumption)
streckem@13673
  1099
apply (frule wtpd_res, assumption, assumption)
streckem@14045
  1100
apply (subgoal_tac "s3::\<preceq>(env_of_jmb G md (mn, pTs))")
streckem@13673
  1101
streckem@14045
  1102
apply (subgoal_tac "method (TranslComp.comp G, md) (mn, pTs) =
streckem@14045
  1103
          Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))")
streckem@14045
  1104
prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method])
streckem@14045
  1105
apply (subgoal_tac "method (TranslComp.comp G, dynT) (mn, pTs) =
streckem@14045
  1106
          Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))")
streckem@14045
  1107
prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method])
streckem@13673
  1108
 apply (simp only: fst_conv snd_conv)
streckem@13673
  1109
streckem@13673
  1110
(* establish length pns = length pTs *)
streckem@13673
  1111
apply (frule method_preserves_length, assumption, assumption) 
streckem@13673
  1112
(* establish length pvs = length ps *)
streckem@13673
  1113
apply (frule evals_preserves_length [THEN sym])
streckem@13673
  1114
streckem@13673
  1115
(** start evaluating subexpressions **)
streckem@13673
  1116
apply (simp (no_asm_use) only: compExpr_compExprs.simps)
streckem@13673
  1117
streckem@13673
  1118
  (* evaluate e *)
ballarin@14174
  1119
apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
streckem@13673
  1120
apply fast
streckem@13673
  1121
streckem@13673
  1122
  (* evaluate parameters *)
ballarin@14174
  1123
apply (rule_tac ?instrs0.0 = "compExprs (gmb G CL S) ps" in progression_transitive, rule HOL.refl)
streckem@13673
  1124
apply fast
streckem@13673
  1125
streckem@13673
  1126
  (* invokation *)
streckem@13673
  1127
apply (rule progression_call)
streckem@13673
  1128
apply (intro allI impI conjI)
streckem@13673
  1129
     (* execute Invoke statement *)
streckem@13673
  1130
apply (simp (no_asm_use) only: exec_instr.simps)
streckem@13673
  1131
apply (erule thin_rl, erule thin_rl, erule thin_rl)
streckem@13673
  1132
apply (simp add: compMethod_def raise_system_xcpt_def)
streckem@13673
  1133
apply (rule conjI, simp)+ apply (rule HOL.refl)
streckem@13673
  1134
streckem@13673
  1135
     (* get instructions of invoked method *)
streckem@13673
  1136
apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def)
streckem@13673
  1137
streckem@13673
  1138
       (* var. initialization *)
ballarin@14174
  1139
apply (rule_tac ?instrs0.0 = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
streckem@13673
  1140
apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption)
streckem@13673
  1141
apply (simp (no_asm_simp)) (* length pns = length pvs *)
streckem@13673
  1142
apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) arbitrary) *)
streckem@13673
  1143
streckem@13673
  1144
streckem@13673
  1145
       (* body statement *)
ballarin@14174
  1146
apply (rule_tac ?instrs0.0 = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl)
streckem@13673
  1147
apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
streckem@13673
  1148
apply (simp (no_asm_simp))
streckem@13673
  1149
apply (simp only: gh_conv)
streckem@13673
  1150
apply ((drule mp, rule TrueI)+, (drule spec)+, (drule mp, assumption)+, assumption)
streckem@13673
  1151
apply (simp (no_asm_use))
streckem@13673
  1152
apply (simp (no_asm_simp) add: gmb_def)
streckem@13673
  1153
streckem@13673
  1154
       (* return expression *) 
streckem@13673
  1155
apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
streckem@13673
  1156
apply (simp (no_asm_simp))
streckem@13673
  1157
apply (simp only: gh_conv)
streckem@13673
  1158
apply ((drule mp, rule TrueI)+, (drule spec)+, (drule mp, assumption)+, assumption)
streckem@13673
  1159
apply (simp (no_asm_use))
streckem@13673
  1160
apply (simp (no_asm_simp) add: gmb_def)
streckem@13673
  1161
streckem@13673
  1162
      (* execute return statement *)
streckem@13673
  1163
apply (simp (no_asm_use) add: gh_def locvars_xstate_def gl_def del: drop_append)
streckem@13673
  1164
apply (subgoal_tac "rev pvs @ a' # os = (rev (a' # pvs)) @ os")
streckem@13673
  1165
apply (simp only: drop_append)
streckem@13673
  1166
apply (simp (no_asm_simp))
streckem@13673
  1167
apply (simp (no_asm_simp))
streckem@13673
  1168
streckem@14045
  1169
(* show s3::\<preceq>\<dots> *)
streckem@13673
  1170
apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" and st=blk in state_ok_exec)
streckem@13673
  1171
apply assumption apply (simp (no_asm_simp) only: env_of_jmb_fst) 
streckem@13673
  1172
apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
streckem@13673
  1173
streckem@13673
  1174
(* show class_sig_defined G md (mn, pTs) *)
streckem@13673
  1175
apply (simp (no_asm_simp) add: class_sig_defined_def)
streckem@13673
  1176
streckem@13673
  1177
(* show G,h \<turnstile> a' ::\<preceq> Class dynT *)
streckem@13673
  1178
apply (frule non_npD) apply assumption
streckem@13673
  1179
apply (erule exE)+ apply simp
streckem@13673
  1180
apply (rule conf_obj_AddrI) apply simp 
streckem@13673
  1181
apply (rule conjI, (rule HOL.refl)+)
streckem@13673
  1182
apply (rule widen_Class_Class [THEN iffD1], rule widen.refl)
streckem@13673
  1183
streckem@13673
  1184
streckem@13673
  1185
  (* show list_all2 (conf G h) pvs pTs *)
streckem@13673
  1186
apply (erule exE)+ apply (erule conjE)+
streckem@13673
  1187
apply (rule_tac Ts="pTsa" in conf_list_gext_widen) apply assumption
streckem@13673
  1188
apply (subgoal_tac "((gx s1, gs s1), ps, pvs, x, h, l) \<in> evals G")
streckem@13673
  1189
apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound)
streckem@14143
  1190
apply assumption+
streckem@13673
  1191
apply (simp only: env_of_jmb_fst) 
streckem@13673
  1192
apply (simp add: conforms_def xconf_def gs_def)
streckem@13673
  1193
apply simp
streckem@13673
  1194
apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
streckem@13673
  1195
apply (simp (no_asm_use) only: ty_exprs_list_all2) apply simp
streckem@14143
  1196
apply simp
streckem@13673
  1197
apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
streckem@13673
  1198
    (* list_all2 (\<lambda>T T'. G \<turnstile> T \<preceq> T') pTsa pTs *)
streckem@13673
  1199
    apply (rule max_spec_widen, simp only: env_of_jmb_fst)
streckem@13673
  1200
streckem@13673
  1201
streckem@13673
  1202
(* show method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res) *)
streckem@14045
  1203
apply (frule wf_prog_ws_prog [THEN method_in_md [THEN conjunct2]], assumption+)
streckem@13673
  1204
streckem@13673
  1205
  (* show G\<turnstile>Class dynT \<preceq> Class md *)
streckem@13673
  1206
apply (simp (no_asm_use) only: widen_Class_Class)
streckem@13673
  1207
apply (rule method_wf_mdecl [THEN conjunct1], assumption+)
streckem@13673
  1208
streckem@13673
  1209
  (* is_class G md *)
streckem@14045
  1210
apply (rule wf_prog_ws_prog [THEN method_in_md [THEN conjunct1]], assumption+)
streckem@13673
  1211
streckem@13673
  1212
  (* show is_class G dynT *)
streckem@13673
  1213
apply (frule non_npD) apply assumption
streckem@13673
  1214
apply (erule exE)+ apply (erule conjE)+
streckem@13673
  1215
apply simp
streckem@13673
  1216
apply (rule subcls_is_class2) apply assumption
streckem@13673
  1217
apply (frule class_expr_is_class) apply (simp only: env_of_jmb_fst)
streckem@14045
  1218
apply (rule wf_prog_ws_prog, assumption)
streckem@13673
  1219
apply (simp only: env_of_jmb_fst)
streckem@13673
  1220
streckem@13673
  1221
 (* show G,h \<turnstile> a' ::\<preceq> Class C *)
streckem@13673
  1222
apply (simp only: wtpd_exprs_def, erule exE)
streckem@13673
  1223
apply (frule evals_preserves_conf)
streckem@13673
  1224
apply (rule eval_conf, assumption+)
streckem@13673
  1225
apply (rule env_of_jmb_fst, assumption+)
streckem@13673
  1226
apply (rule env_of_jmb_fst)
streckem@13673
  1227
apply (simp only: gh_conv)
streckem@13673
  1228
done
streckem@13673
  1229
streckem@13673
  1230
streckem@13673
  1231
theorem compiler_correctness_eval: "
streckem@13673
  1232
  \<lbrakk> G \<turnstile> (None,hp,loc) -ex \<succ> val-> (None,hp',loc');
streckem@13673
  1233
  wf_java_prog G;
streckem@13673
  1234
  class_sig_defined G C S;
streckem@13673
  1235
  wtpd_expr (env_of_jmb G C S) ex;
streckem@13673
  1236
  (None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow>
streckem@13673
  1237
  {(TranslComp.comp G), C, S} \<turnstile> 
streckem@13673
  1238
    {hp, os, (locvars_locals G C S loc)}
streckem@13673
  1239
      >- (compExpr (gmb G C S) ex) \<rightarrow> 
streckem@13673
  1240
    {hp', val#os, (locvars_locals G C S loc')}"
streckem@13673
  1241
apply (frule compiler_correctness [THEN conjunct1])
streckem@14045
  1242
apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def)
streckem@13673
  1243
done
streckem@13673
  1244
streckem@13673
  1245
theorem compiler_correctness_exec: "
streckem@13673
  1246
  \<lbrakk> ((None,hp,loc), st, (None,hp',loc')) \<in> Eval.exec G;
streckem@13673
  1247
  wf_java_prog G;
streckem@13673
  1248
  class_sig_defined G C S;
streckem@13673
  1249
  wtpd_stmt (env_of_jmb G C S) st;
streckem@13673
  1250
  (None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow>
streckem@13673
  1251
  {(TranslComp.comp G), C, S} \<turnstile> 
streckem@13673
  1252
    {hp, os, (locvars_locals G C S loc)}
streckem@13673
  1253
      >- (compStmt (gmb G C S) st) \<rightarrow>
streckem@13673
  1254
    {hp', os, (locvars_locals G C S loc')}"
streckem@13673
  1255
apply (frule compiler_correctness [THEN conjunct2 [THEN conjunct2]])
streckem@14045
  1256
apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def)
streckem@13673
  1257
done
streckem@13673
  1258
streckem@13673
  1259
(**********************************************************************)
streckem@13673
  1260
streckem@13673
  1261
streckem@13673
  1262
(* reinstall pair splits *)
streckem@13673
  1263
declare split_paired_All [simp] split_paired_Ex [simp]
streckem@13673
  1264
ML_setup {*
streckem@13673
  1265
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
streckem@13673
  1266
*}
streckem@13673
  1267
streckem@14045
  1268
declare wf_prog_ws_prog [simp del]
streckem@14045
  1269
streckem@13673
  1270
end