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