src/HOL/MicroJava/BV/LBVComplete.thy
author kleing
Mon Aug 07 14:32:56 2000 +0200 (2000-08-07)
changeset 9549 40d64cb4f4e6
parent 9376 c32c5696ec2a
child 9559 1f99296758c2
permissions -rw-r--r--
BV and LBV specified in terms of app and step functions
kleing@8388
     1
(*  Title:      HOL/MicroJava/BV/LBVComplete.thy
kleing@8388
     2
    ID:         $Id$
kleing@8388
     3
    Author:     Gerwin Klein
kleing@8388
     4
    Copyright   2000 Technische Universitaet Muenchen
kleing@9054
     5
*)
kleing@8388
     6
kleing@9054
     7
header {* Completeness of the LBV *}
kleing@8388
     8
kleing@9549
     9
theory LBVComplete = BVSpec + LBVSpec:
kleing@9549
    10
kleing@9012
    11
kleing@9549
    12
ML_setup {* bind_thm ("widen_RefT", widen_RefT) *}
kleing@9549
    13
ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *}
kleing@9549
    14
kleing@8388
    15
kleing@8388
    16
constdefs
kleing@8388
    17
  is_approx :: "['a option list, 'a list] \\<Rightarrow> bool"
kleing@8388
    18
  "is_approx a b \\<equiv> length a = length b \\<and> (\\<forall> n. n < length a \\<longrightarrow>
kleing@8388
    19
                   (a!n = None \\<or> a!n = Some (b!n)))"
kleing@8388
    20
  
kleing@8388
    21
  contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
kleing@8388
    22
  "contains_dead ins cert phi pc \\<equiv>
kleing@9549
    23
     Suc pc \\<notin> succs (ins!pc) pc \\<and> Suc pc < length phi \\<longrightarrow>
kleing@9549
    24
     cert ! (Suc pc) = Some (phi ! Suc pc)"
kleing@8388
    25
kleing@8388
    26
  contains_targets :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
kleing@9549
    27
  "contains_targets ins cert phi pc \\<equiv> (
kleing@9549
    28
     \\<forall> pc' \\<in> succs (ins!pc) pc. pc' \\<noteq> Suc pc \\<and> pc' < length phi \\<longrightarrow> 
kleing@9549
    29
     cert!pc' = Some (phi!pc'))" 
kleing@9549
    30
kleing@8388
    31
kleing@9012
    32
  fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool"
kleing@9012
    33
  "fits ins cert phi \\<equiv> is_approx cert phi \\<and> length ins < length phi \\<and>
kleing@9012
    34
                            (\\<forall> pc. pc < length ins \\<longrightarrow>
kleing@9012
    35
                                   contains_dead ins cert phi pc \\<and> 
kleing@9012
    36
                                   contains_targets ins cert phi pc)"
kleing@9012
    37
kleing@8388
    38
  is_target :: "[instr list, p_count] \\<Rightarrow> bool" 
kleing@9549
    39
  "is_target ins pc \\<equiv> \\<exists> pc'. pc' < length ins \\<and> pc \\<in> succs (ins!pc') pc'"
kleing@9549
    40
kleing@8388
    41
  maybe_dead :: "[instr list, p_count] \\<Rightarrow> bool"
kleing@9549
    42
  "maybe_dead ins pc \\<equiv> \\<exists> pc'. pc = pc'+1 \\<and> pc \\<notin> succs (ins!pc') pc'"
kleing@8388
    43
kleing@8388
    44
  mdot :: "[instr list, p_count] \\<Rightarrow> bool"
kleing@9549
    45
  "mdot ins pc \\<equiv> maybe_dead ins pc \\<or> is_target ins pc"
kleing@8388
    46
kleing@8388
    47
kleing@8388
    48
consts
kleing@9549
    49
  option_filter_n :: "['a list, nat \\<Rightarrow> bool, nat] \\<Rightarrow> 'a option list"
kleing@8388
    50
primrec 
kleing@8388
    51
  "option_filter_n []    P n = []"  
kleing@8388
    52
  "option_filter_n (h#t) P n = (if (P n) then Some h # option_filter_n t P (n+1) 
kleing@9549
    53
                                         else None   # option_filter_n t P (n+1))"  
kleing@8388
    54
  
kleing@8388
    55
constdefs 
kleing@8388
    56
  option_filter :: "['a list, nat \\<Rightarrow> bool] \\<Rightarrow> 'a option list" 
kleing@8388
    57
  "option_filter l P \\<equiv> option_filter_n l P 0" 
kleing@8388
    58
  
kleing@8388
    59
  make_cert :: "[instr list, method_type] \\<Rightarrow> certificate"
kleing@8388
    60
  "make_cert ins phi \\<equiv> option_filter phi (mdot ins)"
kleing@8388
    61
  
kleing@8388
    62
  make_Cert :: "[jvm_prog, prog_type] \\<Rightarrow> prog_certificate"
kleing@8388
    63
  "make_Cert G Phi \\<equiv>  \\<lambda> C sig.
kleing@8388
    64
    let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in
kleing@8388
    65
      let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in
kleing@9549
    66
        make_cert b (Phi C sig)"
kleing@8388
    67
  
kleing@9012
    68
kleing@9549
    69
lemma length_ofn: "\\<forall>n. length (option_filter_n l P n) = length l"
kleing@9549
    70
  by (induct l) auto
kleing@9012
    71
kleing@9012
    72
lemma is_approx_option_filter_n:
kleing@9549
    73
"\\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a")
kleing@9549
    74
proof (induct a)
kleing@9549
    75
  show "?P []" by (auto simp add: is_approx_def)
kleing@9012
    76
kleing@9549
    77
  fix l ls
kleing@9549
    78
  assume Cons: "?P ls"
kleing@9012
    79
kleing@9549
    80
  show "?P (l#ls)"
kleing@9549
    81
  proof (unfold is_approx_def, intro allI conjI impI)
kleing@9549
    82
    fix n
kleing@9549
    83
    show "length (option_filter_n (l # ls) P n) = length (l # ls)" 
kleing@9549
    84
      by (simp only: length_ofn)
kleing@9012
    85
    
kleing@9549
    86
    fix m
kleing@9549
    87
    assume "m < length (option_filter_n (l # ls) P n)"
kleing@9549
    88
    hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp
kleing@9012
    89
 
kleing@9012
    90
    show "option_filter_n (l # ls) P n ! m = None \\<or>
kleing@9549
    91
          option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)" 
kleing@9549
    92
    proof (cases "m")
kleing@9549
    93
      assume "m = 0"
kleing@9549
    94
      with m show ?thesis by simp
kleing@9549
    95
    next
kleing@9549
    96
      fix m' assume Suc: "m = Suc m'"
kleing@9549
    97
      from Cons
kleing@9549
    98
      show ?thesis
kleing@9549
    99
      proof (unfold is_approx_def, elim allE impE conjE)
kleing@9549
   100
        from m Suc
kleing@9549
   101
        show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn)
kleing@9012
   102
kleing@9012
   103
        assume "option_filter_n ls P (Suc n) ! m' = None \\<or> 
kleing@9549
   104
                option_filter_n ls P (Suc n) ! m' = Some (ls ! m')"
kleing@9549
   105
        with m Suc
kleing@9549
   106
        show ?thesis by auto
kleing@9376
   107
      qed
kleing@9376
   108
    qed
kleing@9376
   109
  qed
kleing@9376
   110
qed
kleing@9012
   111
kleing@9549
   112
lemma is_approx_option_filter: "is_approx (option_filter l P) l" 
kleing@9549
   113
  by (simp add: option_filter_def is_approx_option_filter_n)
kleing@9549
   114
kleing@9549
   115
lemma option_filter_Some:
kleing@9549
   116
"\\<lbrakk>n < length l; P n\\<rbrakk> \\<Longrightarrow> option_filter l P ! n = Some (l!n)"
kleing@9549
   117
proof -
kleing@9549
   118
  
kleing@9549
   119
  assume 1: "n < length l" "P n"
kleing@9549
   120
kleing@9549
   121
  have "\\<forall>n n'. n < length l \\<longrightarrow> P (n+n') \\<longrightarrow>  option_filter_n l P n' ! n = Some (l!n)"
kleing@9549
   122
    (is "?P l")
kleing@9549
   123
  proof (induct l)
kleing@9549
   124
    show "?P []" by simp
kleing@9012
   125
kleing@9549
   126
    fix l ls assume Cons: "?P ls"
kleing@9549
   127
    show "?P (l#ls)"
kleing@9549
   128
    proof (intro)
kleing@9549
   129
      fix n n'
kleing@9549
   130
      assume l: "n < length (l # ls)"
kleing@9549
   131
      assume P: "P (n + n')"
kleing@9549
   132
      show "option_filter_n (l # ls) P n' ! n = Some ((l # ls) ! n)"
kleing@9549
   133
      proof (cases "n")
kleing@9549
   134
        assume "n=0"
kleing@9549
   135
        with P show ?thesis by simp
kleing@9549
   136
      next
kleing@9549
   137
        fix m assume "n = Suc m"
kleing@9549
   138
        with l P Cons
kleing@9549
   139
        show ?thesis by simp
kleing@9549
   140
      qed
kleing@9549
   141
    qed
kleing@9549
   142
  qed
kleing@9549
   143
kleing@9549
   144
  with 1
kleing@9549
   145
  show ?thesis by (auto simp add: option_filter_def)
kleing@9549
   146
qed
kleing@9549
   147
kleing@9549
   148
lemma option_filter_contains_dead:
kleing@9549
   149
"contains_dead ins (option_filter phi (mdot ins)) phi pc" 
kleing@9549
   150
  by (auto intro: option_filter_Some simp add: contains_dead_def mdot_def maybe_dead_def)
kleing@9012
   151
kleing@9549
   152
lemma option_filter_contains_targets:
kleing@9549
   153
"pc < length ins \\<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc"
kleing@9549
   154
proof (unfold contains_targets_def, clarsimp)
kleing@9549
   155
 
kleing@9549
   156
  fix pc'
kleing@9549
   157
  assume "pc < length ins" 
kleing@9549
   158
         "pc' \\<in> succs (ins ! pc) pc" 
kleing@9549
   159
         "pc' \\<noteq> Suc pc" and
kleing@9549
   160
    pc': "pc' < length phi"
kleing@9549
   161
kleing@9549
   162
  hence "is_target ins pc'" by (auto simp add: is_target_def)
kleing@9549
   163
kleing@9549
   164
  with pc'
kleing@9549
   165
  show "option_filter phi (mdot ins) ! pc' = Some (phi ! pc')"
kleing@9549
   166
    by (auto intro: option_filter_Some simp add: mdot_def)
kleing@9549
   167
qed
kleing@9549
   168
  
kleing@9549
   169
kleing@9549
   170
lemma fits_make_cert:
kleing@9549
   171
  "length ins < length phi \\<Longrightarrow> fits ins (make_cert ins phi) phi"
kleing@9549
   172
proof -
kleing@9549
   173
  assume l: "length ins < length phi"
kleing@9012
   174
kleing@9549
   175
  thus "fits ins (make_cert ins phi) phi"
kleing@9549
   176
  proof (unfold fits_def make_cert_def, intro conjI allI impI)
kleing@9549
   177
    show "is_approx (option_filter phi (mdot ins)) phi" 
kleing@9549
   178
      by (rule is_approx_option_filter)
kleing@9549
   179
kleing@9549
   180
    show "length ins < length phi" .
kleing@9549
   181
kleing@9549
   182
    fix pc
kleing@9549
   183
    show "contains_dead ins (option_filter phi (mdot ins)) phi pc" 
kleing@9549
   184
      by (rule option_filter_contains_dead)
kleing@9549
   185
    
kleing@9549
   186
    assume "pc < length ins" 
kleing@9549
   187
    thus "contains_targets ins (option_filter phi (mdot ins)) phi pc" 
kleing@9549
   188
      by (rule option_filter_contains_targets)
kleing@9549
   189
  qed
kleing@9549
   190
qed
kleing@9549
   191
kleing@9549
   192
lemma fitsD: 
kleing@9549
   193
"\\<lbrakk>fits ins cert phi; pc' \\<in> succs (ins!pc) pc; pc' \\<noteq> Suc pc; pc < length ins; pc' < length ins\\<rbrakk> 
kleing@9549
   194
  \\<Longrightarrow> cert!pc' = Some (phi!pc')"
kleing@9549
   195
by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
kleing@9549
   196
kleing@9549
   197
lemma fitsD2:
kleing@9549
   198
"\\<lbrakk>fits ins cert phi; Suc pc \\<notin> succs (ins!pc) pc;  pc < length ins\\<rbrakk> 
kleing@9549
   199
  \\<Longrightarrow> cert ! Suc pc = Some (phi ! Suc pc)"
kleing@9549
   200
by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
kleing@9012
   201
kleing@9012
   202
kleing@9012
   203
kleing@9549
   204
lemmas [trans] = sup_state_trans
kleing@9012
   205
kleing@9549
   206
lemma wtl_inst_mono:
kleing@9012
   207
"\\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; wf_prog wf_mb G; 
kleing@9012
   208
  G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> 
kleing@9549
   209
 \\<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
kleing@9549
   210
proof -
kleing@9549
   211
  assume pc:   "pc < length ins" "i = ins!pc"
kleing@9549
   212
  assume wtl:  "wtl_inst i G rT s1 s1' cert mpc pc"
kleing@9549
   213
  assume fits: "fits ins cert phi"
kleing@9549
   214
  assume G:    "G \\<turnstile> s2 <=s s1"
kleing@9549
   215
  
kleing@9549
   216
  let "?step s" = "step (i, G, s)"
kleing@9012
   217
kleing@9549
   218
  from wtl G
kleing@9549
   219
  have app: "app (i, G, rT, s2)" by (auto simp add: wtl_inst_def app_mono)
kleing@9549
   220
  
kleing@9549
   221
  from wtl G
kleing@9549
   222
  have step: "succs i pc \\<noteq> {} \\<Longrightarrow> G \\<turnstile> the (?step s2) <=s the (?step s1)" 
kleing@9549
   223
    by - (drule step_mono, auto simp add: wtl_inst_def)
kleing@9549
   224
  
kleing@9549
   225
  with app
kleing@9549
   226
  have some: "succs i pc \\<noteq> {} \\<Longrightarrow> ?step s2 \\<noteq> None" by (simp add: app_step_some)
kleing@9012
   227
kleing@9549
   228
  {
kleing@9549
   229
    fix pc'
kleing@9549
   230
    assume 0: "pc' \\<in> succs i pc" "pc' \\<noteq> pc+1"
kleing@9549
   231
    hence "succs i pc \\<noteq> {}" by auto
kleing@9549
   232
    hence "G \\<turnstile> the (?step s2) <=s the (?step s1)" by (rule step)
kleing@9549
   233
    also 
kleing@9549
   234
    from wtl 0
kleing@9549
   235
    have "G \\<turnstile> the (?step s1) <=s the (cert!pc')"
kleing@9549
   236
      by (auto simp add: wtl_inst_def) 
kleing@9549
   237
    finally
kleing@9549
   238
    have "G\\<turnstile> the (?step s2) <=s the (cert!pc')" .
kleing@9549
   239
  } note cert = this
kleing@9549
   240
    
kleing@9549
   241
  have "\\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \\<and> G \\<turnstile> s2' <=s s1'"
kleing@9549
   242
  proof (cases "pc+1 \\<in> succs i pc")
kleing@9549
   243
    case True
kleing@9549
   244
    with wtl
kleing@9549
   245
    have s1': "s1' = the (?step s1)" by (simp add: wtl_inst_def)
kleing@9012
   246
kleing@9549
   247
    have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \\<and> G \\<turnstile> (the (?step s2)) <=s s1'" 
kleing@9549
   248
      (is "?wtl \\<and> ?G")
kleing@9549
   249
    proof
kleing@9549
   250
      from True s1'
kleing@9549
   251
      show ?G by (auto intro: step)
kleing@9549
   252
kleing@9549
   253
      from True app wtl
kleing@9549
   254
      show ?wtl
kleing@9549
   255
        by (clarsimp intro: cert simp add: wtl_inst_def)
kleing@9376
   256
    qed
kleing@9549
   257
    thus ?thesis by blast
kleing@9376
   258
  next
kleing@9549
   259
    case False
kleing@9549
   260
    with wtl
kleing@9549
   261
    have "s1' = the (cert ! Suc pc)" by (simp add: wtl_inst_def)
kleing@9012
   262
kleing@9549
   263
    with False app wtl
kleing@9549
   264
    have "wtl_inst i G rT s2 s1' cert mpc pc \\<and> G \\<turnstile> s1' <=s s1'"
kleing@9549
   265
      by (clarsimp intro: cert simp add: wtl_inst_def)
kleing@9549
   266
kleing@9549
   267
    thus ?thesis by blast
kleing@9549
   268
  qed
kleing@9012
   269
  
kleing@9549
   270
  with pc show ?thesis by simp
kleing@9376
   271
qed
kleing@9549
   272
    
kleing@9549
   273
    
kleing@9012
   274
lemma wt_instr_imp_wtl_inst:
kleing@9012
   275
"\\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
kleing@9012
   276
  pc < length ins; length ins = max_pc\\<rbrakk> \\<Longrightarrow> 
kleing@9012
   277
  \\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
kleing@9376
   278
proof -
kleing@9549
   279
  assume wt:   "wt_instr (ins!pc) G rT phi max_pc pc" 
kleing@9549
   280
  assume fits: "fits ins cert phi"
kleing@9549
   281
  assume pc:   "pc < length ins" "length ins = max_pc"
kleing@9549
   282
kleing@9549
   283
  from wt 
kleing@9549
   284
  have app: "app (ins!pc, G, rT, phi!pc)" by (simp add: wt_instr_def);
kleing@9549
   285
kleing@9549
   286
  from wt pc
kleing@9549
   287
  have pc': "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> pc' < length ins"
kleing@9549
   288
    by (simp add: wt_instr_def)
kleing@9376
   289
kleing@9549
   290
  let ?s' = "the (step (ins!pc,G, phi!pc))"
kleing@9549
   291
kleing@9549
   292
  from wt
kleing@9549
   293
  have G: "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> G \\<turnstile> ?s' <=s phi ! pc'"
kleing@9549
   294
    by (simp add: wt_instr_def)
kleing@9549
   295
kleing@9549
   296
  from wt fits pc
kleing@9549
   297
  have cert: "!!pc'. \\<lbrakk>pc' \\<in> succs (ins!pc) pc; pc' < max_pc; pc' \\<noteq> pc+1\\<rbrakk> 
kleing@9549
   298
    \\<Longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> ?s' <=s the (cert!pc')"
kleing@9549
   299
    by (auto dest: fitsD simp add: wt_instr_def simp del: split_paired_Ex)
kleing@9012
   300
kleing@9376
   301
  show ?thesis
kleing@9549
   302
  proof (cases "pc+1 \\<in> succs (ins!pc) pc")
kleing@9549
   303
    case True
kleing@9549
   304
kleing@9549
   305
    have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \\<and> G \\<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \\<and> ?G")
kleing@9549
   306
    proof 
kleing@9549
   307
      from True
kleing@9549
   308
      show "G \\<turnstile> ?s' <=s phi ! Suc pc"  by (simp add: G)
kleing@9549
   309
kleing@9549
   310
      from True fits app pc cert pc'
kleing@9549
   311
      show "?wtl"
kleing@9549
   312
        by (auto simp add: wtl_inst_def)
kleing@9549
   313
    qed
kleing@9012
   314
kleing@9549
   315
    thus ?thesis by blast
kleing@9549
   316
    
kleing@9549
   317
  next    
kleing@9549
   318
    let ?s'' = "the (cert ! Suc pc)"
kleing@9012
   319
kleing@9549
   320
    case False
kleing@9549
   321
    with fits app pc cert pc'
kleing@9549
   322
    have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \\<and> G \\<turnstile> ?s'' <=s phi ! Suc pc" 
kleing@9549
   323
      by (auto dest: fitsD2 simp add: wtl_inst_def)
kleing@9012
   324
kleing@9549
   325
    thus ?thesis by blast
kleing@9549
   326
  qed
kleing@9376
   327
qed
kleing@9012
   328
kleing@9012
   329
  
kleing@9012
   330
lemma wt_instr_imp_wtl_option:
kleing@9012
   331
"\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc;  max_pc = length ins\\<rbrakk> \\<Longrightarrow> 
kleing@9012
   332
 \\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
kleing@9376
   333
proof -
kleing@9012
   334
  assume fits : "fits ins cert phi" "pc < length ins" 
kleing@9012
   335
         and "wt_instr (ins!pc) G rT phi max_pc pc" 
kleing@9012
   336
             "max_pc = length ins";
kleing@9012
   337
kleing@9012
   338
  hence * : "\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
kleing@9012
   339
    by - (rule wt_instr_imp_wtl_inst, simp+);
kleing@9012
   340
  
kleing@9012
   341
  show ?thesis;
kleing@9012
   342
  proof (cases "cert ! pc");
kleing@9012
   343
    case None;
kleing@9012
   344
    with *;
kleing@9012
   345
    show ?thesis; by (simp add: wtl_inst_option_def);
kleing@9012
   346
kleing@9012
   347
  next;
kleing@9012
   348
    case Some;
kleing@9012
   349
kleing@9012
   350
    from fits; 
kleing@9549
   351
    have "pc < length phi"; by (clarsimp simp add: fits_def);
kleing@9012
   352
    with fits Some;
kleing@9012
   353
    have "cert ! pc = Some (phi!pc)"; by (auto simp add: fits_def is_approx_def);
kleing@9012
   354
     
kleing@9012
   355
    with *; 
kleing@9012
   356
    show ?thesis; by (simp add: wtl_inst_option_def);
kleing@9549
   357
  qed
kleing@9549
   358
qed
kleing@9012
   359
kleing@9376
   360
kleing@9549
   361
lemma wtl_option_mono:
kleing@9012
   362
"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc;  fits ins cert phi; pc < length ins; 
kleing@9012
   363
  wf_prog wf_mb G; G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> 
kleing@9549
   364
 \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
kleing@9549
   365
proof -
kleing@9012
   366
  assume wtl:  "wtl_inst_option i G rT s1 s1' cert mpc pc" and
kleing@9012
   367
         fits: "fits ins cert phi" "pc < length ins"
kleing@9549
   368
               "wf_prog wf_mb G" "G \\<turnstile> s2 <=s s1" "i = ins!pc"
kleing@9012
   369
kleing@9549
   370
  show ?thesis
kleing@9549
   371
  proof (cases "cert!pc")
kleing@9549
   372
    case None
kleing@9012
   373
    with wtl fits;
kleing@9012
   374
    show ?thesis; 
kleing@9549
   375
      by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+);
kleing@9549
   376
  next
kleing@9549
   377
    case Some
kleing@9012
   378
    with wtl fits;
kleing@9012
   379
kleing@9549
   380
    have G: "G \\<turnstile> s2 <=s a"
kleing@9549
   381
     by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+)
kleing@9012
   382
kleing@9549
   383
    from Some wtl
kleing@9549
   384
    have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def)
kleing@9012
   385
kleing@9549
   386
    with G fits
kleing@9549
   387
    have "\\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
kleing@9549
   388
      by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+);
kleing@9012
   389
    
kleing@9012
   390
    with Some G;
kleing@9012
   391
    show ?thesis; by (simp add: wtl_inst_option_def);
kleing@9376
   392
  qed
kleing@9549
   393
qed
kleing@9012
   394
kleing@9012
   395
kleing@9012
   396
(* main induction over instruction list *)
kleing@9012
   397
theorem wt_imp_wtl_inst_list:
kleing@9012
   398
"\\<forall> pc. (\\<forall>pc'. pc' < length ins \\<longrightarrow> wt_instr (ins ! pc') G rT phi (pc+length ins) (pc+pc')) \\<longrightarrow>   
kleing@9012
   399
       wf_prog wf_mb G \\<longrightarrow> 
kleing@9012
   400
       fits all_ins cert phi \\<longrightarrow> (\\<exists> l. pc = length l \\<and> all_ins=l@ins) \\<longrightarrow> pc < length all_ins \\<longrightarrow>
kleing@9012
   401
       (\\<forall> s. (G \\<turnstile> s <=s (phi!pc)) \\<longrightarrow> 
kleing@9012
   402
       (\\<exists>s'. wtl_inst_list ins G rT s s' cert (pc+length ins) pc))" 
kleing@9012
   403
(is "\\<forall>pc. ?C pc ins" is "?P ins");
kleing@9012
   404
proof (induct "?P" "ins");
kleing@9012
   405
  case Nil;
kleing@9012
   406
  show "?P []"; by simp;
kleing@9012
   407
next;
kleing@9012
   408
  case Cons;
kleing@9012
   409
kleing@9012
   410
  show "?P (a#list)";
kleing@9012
   411
  proof (intro allI impI, elim exE conjE);
kleing@9012
   412
    fix pc s l;
kleing@9012
   413
    assume 1: "wf_prog wf_mb G" "fits all_ins cert phi";
kleing@9012
   414
    assume 2: "pc < length all_ins" "G \\<turnstile> s <=s phi ! pc"
kleing@9012
   415
              "all_ins = l @ a # list" "pc = length l";
kleing@9012
   416
kleing@9012
   417
    from Cons;
kleing@9012
   418
    have IH: "?C (Suc pc) list"; by blast;
kleing@9012
   419
kleing@9012
   420
    assume 3: "\\<forall>pc'. pc' < length (a # list) \\<longrightarrow>
kleing@9012
   421
               wt_instr ((a # list) ! pc') G rT phi (pc + length (a # list)) (pc + pc')";
kleing@9012
   422
    hence 4: "\\<forall>pc'. pc' < length list \\<longrightarrow>
kleing@9012
   423
              wt_instr (list ! pc') G rT phi (Suc pc + length list) (Suc pc + pc')"; by auto;    
kleing@9012
   424
kleing@9012
   425
    from 2; 
kleing@9182
   426
    have 5: "a = all_ins ! pc"; by (simp add: nth_append);
kleing@9012
   427
kleing@9012
   428
kleing@9012
   429
    show "\\<exists>s'. wtl_inst_list (a # list) G rT s s' cert (pc + length (a # list)) pc"; 
kleing@9012
   430
    proof (cases list);
kleing@9012
   431
      case Nil;
kleing@9012
   432
kleing@9012
   433
      with 1 2 3 5; 
kleing@9012
   434
      have "\\<exists>s'. wtl_inst_option a G rT (phi ! pc) s' cert (Suc (length l)) pc";
kleing@9012
   435
        by - (rule wt_instr_imp_wtl_option [elimify], force+);
kleing@9012
   436
kleing@9012
   437
      with Nil 1 2 5;
kleing@9012
   438
      have "\\<exists>s'. wtl_inst_option a G rT s s' cert (Suc (length l)) pc";
kleing@9549
   439
        by elim (rule wtl_option_mono [elimify], force+); 
kleing@9012
   440
kleing@9012
   441
      with Nil 2;
kleing@9012
   442
      show ?thesis; by auto;
kleing@9012
   443
    next;
kleing@9012
   444
      fix i' ins'; 
kleing@9012
   445
      assume Cons2: "list = i' # ins'";
kleing@9012
   446
kleing@9012
   447
      with IH 1 2 3;
kleing@9012
   448
      have * : "\\<forall> s. (G \\<turnstile> s <=s (phi!(Suc pc))) \\<longrightarrow> 
kleing@9012
   449
                     (\\<exists>s'. wtl_inst_list list G rT s s' cert ((Suc pc)+length list) (Suc pc))";
kleing@9012
   450
        by (elim impE) force+;
kleing@9012
   451
kleing@9012
   452
      from 3;
kleing@9012
   453
      have "wt_instr a G rT phi (pc + length (a # list)) pc"; by auto;
kleing@9012
   454
      
kleing@9012
   455
      with 1 2 5;
kleing@9012
   456
      have "\\<exists>s1'. wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc \\<and> G \\<turnstile> s1' <=s phi ! Suc pc";
kleing@9012
   457
        by - (rule wt_instr_imp_wtl_option [elimify], assumption+, simp+);
kleing@9012
   458
kleing@9012
   459
      hence "\\<exists>s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\<and>
kleing@9549
   460
                  (G \\<turnstile> s1 <=s (phi ! (Suc pc)))" (* \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s))"; *)
kleing@9012
   461
      proof elim; 
kleing@9012
   462
        fix s1';
kleing@9012
   463
        assume "wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc" and
kleing@9012
   464
            a :"G \\<turnstile> s1' <=s phi ! Suc pc";
kleing@9012
   465
        with 1 2 5;
kleing@9012
   466
        have "\\<exists>s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\<and>
kleing@9549
   467
                   ((G \\<turnstile> s1 <=s s1'))" (* \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s))"; *)
kleing@9549
   468
          by - (rule wtl_option_mono [elimify], simp+);
kleing@9012
   469
kleing@9012
   470
        with a;
kleing@9012
   471
        show ?thesis;
kleing@9012
   472
        proof (elim, intro);
kleing@9012
   473
          fix s1;
kleing@9012
   474
          assume "G \\<turnstile> s1 <=s s1'" "G \\<turnstile> s1' <=s phi ! Suc pc";
kleing@9012
   475
          show "G \\<turnstile> s1 <=s phi ! Suc pc"; by (rule sup_state_trans);
kleing@9012
   476
        qed auto;
kleing@9549
   477
      qed
kleing@9012
   478
kleing@9549
   479
      thus ?thesis
kleing@9012
   480
      proof (elim exE conjE); 
kleing@9012
   481
        fix s1;
kleing@9012
   482
        assume wto: "wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc"; 
kleing@9549
   483
        assume Gs1: "G \\<turnstile> s1 <=s phi ! Suc pc" (* \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s)"; *)
kleing@9012
   484
        
kleing@9549
   485
        with *
kleing@9549
   486
        have "\\<exists>s'. wtl_inst_list list G rT s1 s' cert ((Suc pc)+length list) (Suc pc)";  by blast
kleing@9012
   487
kleing@9012
   488
        with wto;
kleing@9012
   489
        show ?thesis; by (auto simp del: split_paired_Ex);
kleing@9549
   490
      qed
kleing@9549
   491
    qed
kleing@9549
   492
  qed
kleing@9549
   493
qed
kleing@9012
   494
kleing@9012
   495
kleing@9012
   496
lemma fits_imp_wtl_method_complete:
kleing@9012
   497
"\\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins cert";
kleing@9012
   498
by (simp add: wt_method_def wtl_method_def del: split_paired_Ex)
kleing@9012
   499
   (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex); 
kleing@9012
   500
kleing@9012
   501
kleing@9012
   502
lemma wtl_method_complete:
kleing@9012
   503
"\\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)";
kleing@9012
   504
proof -;
kleing@9012
   505
  assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G";
kleing@9012
   506
  
kleing@9012
   507
  hence "fits ins (make_cert ins phi) phi";
kleing@9012
   508
    by - (rule fits_make_cert, simp add: wt_method_def);
kleing@9012
   509
kleing@9012
   510
  with *;
kleing@9012
   511
  show ?thesis; by - (rule fits_imp_wtl_method_complete);
kleing@9012
   512
qed;
kleing@9012
   513
kleing@9012
   514
lemma unique_set:
kleing@9012
   515
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'";
kleing@9012
   516
  by (induct "l") auto;
kleing@9012
   517
kleing@9012
   518
lemma unique_epsilon:
kleing@9012
   519
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)";
kleing@9012
   520
  by (auto simp add: unique_set);
kleing@9012
   521
kleing@9012
   522
kleing@9012
   523
theorem wtl_complete: "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)";
kleing@9012
   524
proof (simp only: wt_jvm_prog_def);
kleing@9012
   525
kleing@9012
   526
  assume wfprog: "wf_prog (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G";
kleing@9012
   527
kleing@9012
   528
  thus ?thesis; 
kleing@9012
   529
  proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto);
kleing@9012
   530
    fix a aa ab b ac ba ad ae bb; 
kleing@9012
   531
    assume 1 : "\\<forall>(C,sc,fs,ms)\\<in>set G.
kleing@9012
   532
             Ball (set fs) (wf_fdecl G) \\<and>
kleing@9012
   533
             unique fs \\<and>
kleing@9012
   534
             (\\<forall>(sig,rT,mb)\\<in>set ms. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \\<and>
kleing@9012
   535
             unique ms \\<and>
kleing@9012
   536
             (case sc of None \\<Rightarrow> C = Object
kleing@9012
   537
              | Some D \\<Rightarrow>
kleing@9012
   538
                  is_class G D \\<and>
kleing@9012
   539
                  (D, C) \\<notin> (subcls1 G)^* \\<and>
kleing@9012
   540
                  (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
kleing@9012
   541
             "(a, aa, ab, b) \\<in> set G";
kleing@9012
   542
  
kleing@9012
   543
    assume uG : "unique G"; 
kleing@9012
   544
    assume b  : "((ac, ba), ad, ae, bb) \\<in> set b";
kleing@9012
   545
kleing@9012
   546
    from 1;
kleing@9012
   547
    show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))";
kleing@9549
   548
    proof (rule bspec [elimify], clarsimp);
kleing@9012
   549
      assume ub : "unique b";
kleing@9012
   550
      assume m: "\\<forall>(sig,rT,mb)\\<in>set b. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb"; 
kleing@9012
   551
      from m b;
kleing@9012
   552
      show ?thesis;
kleing@9549
   553
      proof (rule bspec [elimify], clarsimp);
kleing@9012
   554
        assume "wt_method G a ba ad ae bb (Phi a (ac, ba))";         
kleing@9012
   555
        with wfprog uG ub b 1;
kleing@9012
   556
        show ?thesis;
kleing@9012
   557
          by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon);
kleing@9012
   558
      qed; 
kleing@9012
   559
    qed;
kleing@9012
   560
  qed;
kleing@9549
   561
qed
kleing@9012
   562
kleing@9549
   563
kleing@9549
   564
end