src/HOL/MicroJava/BV/LBVCorrect.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 15425 6356d2523f73
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
kleing@13078
     1
(*
kleing@8245
     2
    ID:         $Id$
kleing@8245
     3
    Author:     Gerwin Klein
kleing@8245
     4
    Copyright   1999 Technische Universitaet Muenchen
kleing@9054
     5
*)
kleing@8245
     6
kleing@12911
     7
header {* \isaheader{Correctness of the LBV} *}
kleing@8245
     8
kleing@13062
     9
theory LBVCorrect = LBVSpec + Typing_Framework:
kleing@9757
    10
wenzelm@13365
    11
locale (open) lbvs = lbv +
kleing@13649
    12
  fixes s0  :: 'a ("s\<^sub>0")
kleing@13078
    13
  fixes c   :: "'a list"
kleing@13078
    14
  fixes ins :: "'b list"
kleing@13078
    15
  fixes phi :: "'a list" ("\<phi>")
kleing@13078
    16
  defines phi_def:
kleing@13080
    17
  "\<phi> \<equiv> map (\<lambda>pc. if c!pc = \<bottom> then wtl (take pc ins) c 0 s0 else c!pc) 
nipkow@15425
    18
       [0..<length ins]"
kleing@13080
    19
kleing@13080
    20
  assumes bounded: "bounded step (length ins)"
kleing@13080
    21
  assumes cert: "cert_ok c (length ins) \<top> \<bottom> A"
kleing@13080
    22
  assumes pres: "pres_type step (length ins) A"
kleing@9012
    23
kleing@9012
    24
kleing@13080
    25
lemma (in lbvs) phi_None [intro?]:
kleing@13078
    26
  "\<lbrakk> pc < length ins; c!pc = \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = wtl (take pc ins) c 0 s0"
kleing@13078
    27
  by (simp add: phi_def)
kleing@9757
    28
kleing@13080
    29
lemma (in lbvs) phi_Some [intro?]:
kleing@13078
    30
  "\<lbrakk> pc < length ins; c!pc \<noteq> \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = c ! pc"
kleing@13078
    31
  by (simp add: phi_def)
kleing@13062
    32
kleing@13080
    33
lemma (in lbvs) phi_len [simp]:
kleing@13078
    34
  "length \<phi> = length ins"
kleing@13078
    35
  by (simp add: phi_def)
kleing@13078
    36
kleing@9012
    37
kleing@13080
    38
lemma (in lbvs) wtl_suc_pc:
kleing@13649
    39
  assumes all: "wtl ins c 0 s\<^sub>0 \<noteq> \<top>" 
kleing@13078
    40
  assumes pc:  "pc+1 < length ins"
kleing@13649
    41
  shows "wtl (take (pc+1) ins) c 0 s0 \<le>\<^sub>r \<phi>!(pc+1)"
kleing@13078
    42
proof -
kleing@13078
    43
  from all pc
kleing@13078
    44
  have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) \<noteq> T" by (rule wtl_all)
kleing@13078
    45
  with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm)
kleing@9580
    46
qed
kleing@9012
    47
kleing@9012
    48
kleing@13080
    49
lemma (in lbvs) wtl_stable:
kleing@13080
    50
  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>" 
kleing@13080
    51
  assumes s0:  "s0 \<in> A" 
kleing@13080
    52
  assumes pc:  "pc < length ins" 
kleing@13078
    53
  shows "stable r step \<phi> pc"
kleing@13062
    54
proof (unfold stable_def, clarify)
kleing@13078
    55
  fix pc' s' assume step: "(pc',s') \<in> set (step pc (\<phi> ! pc))" 
kleing@13062
    56
                      (is "(pc',s') \<in> set (?step pc)")
kleing@13062
    57
  
kleing@13080
    58
  from bounded pc step have pc': "pc' < length ins" by (rule boundedD)
kleing@13078
    59
kleing@13078
    60
  have tkpc: "wtl (take pc ins) c 0 s0 \<noteq> \<top>" (is "?s1 \<noteq> _") by (rule wtl_take)
kleing@13078
    61
  have s2: "wtl (take (pc+1) ins) c 0 s0 \<noteq> \<top>" (is "?s2 \<noteq> _") by (rule wtl_take)
kleing@13062
    62
  
kleing@13080
    63
  from wtl pc have wt_s1: "wtc c pc ?s1 \<noteq> \<top>" by (rule wtl_all)
kleing@9012
    64
kleing@13078
    65
  have c_Some: "\<forall>pc t. pc < length ins \<longrightarrow> c!pc \<noteq> \<bottom> \<longrightarrow> \<phi>!pc = c!pc" 
kleing@13078
    66
    by (simp add: phi_def)
kleing@13078
    67
  have c_None: "c!pc = \<bottom> \<Longrightarrow> \<phi>!pc = ?s1" ..
kleing@13062
    68
kleing@13080
    69
  from wt_s1 pc c_None c_Some
kleing@13078
    70
  have inst: "wtc c pc ?s1  = wti c pc (\<phi>!pc)"
kleing@13078
    71
    by (simp add: wtc split: split_if_asm)
kleing@13062
    72
kleing@13078
    73
  have "?s1 \<in> A" by (rule wtl_pres) 
kleing@13080
    74
  with pc c_Some cert c_None
kleing@13078
    75
  have "\<phi>!pc \<in> A" by (cases "c!pc = \<bottom>") (auto dest: cert_okD1)
kleing@13062
    76
  with pc pres
kleing@13078
    77
  have step_in_A: "snd`set (?step pc) \<subseteq> A" by (auto dest: pres_typeD2)
kleing@9012
    78
kleing@13078
    79
  show "s' <=_r \<phi>!pc'" 
kleing@13062
    80
  proof (cases "pc' = pc+1")
kleing@13062
    81
    case True
kleing@13080
    82
    with pc' cert
kleing@13078
    83
    have cert_in_A: "c!(pc+1) \<in> A" by (auto dest: cert_okD1)
kleing@13078
    84
    from True pc' have pc1: "pc+1 < length ins" by simp
kleing@13078
    85
    with tkpc have "?s2 = wtc c pc ?s1" by - (rule wtl_Suc)
kleing@13078
    86
    with inst 
kleing@13078
    87
    have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti)
kleing@13062
    88
    also    
kleing@13078
    89
    from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
kleing@13078
    90
    with cert_in_A step_in_A
kleing@13078
    91
    have "?merge = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++_f (c!(pc+1)))"
kleing@13078
    92
      by (rule merge_not_top_s) 
kleing@13062
    93
    finally
kleing@13078
    94
    have "s' <=_r ?s2" using step_in_A cert_in_A True step 
kleing@13078
    95
      by (auto intro: pp_ub1')
kleing@13062
    96
    also 
kleing@13078
    97
    from wtl pc1 have "?s2 <=_r \<phi>!(pc+1)" by (rule wtl_suc_pc)
kleing@13062
    98
    also note True [symmetric]
kleing@13078
    99
    finally show ?thesis by simp    
kleing@13062
   100
  next
kleing@13062
   101
    case False
kleing@13080
   102
    from wt_s1 inst
kleing@13078
   103
    have "merge c pc (?step pc) (c!(pc+1)) \<noteq> \<top>" by (simp add: wti)
kleing@13078
   104
    with step_in_A
kleing@13078
   105
    have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" 
kleing@13078
   106
      by - (rule merge_not_top)
kleing@13062
   107
    with step False 
kleing@13078
   108
    have ok: "s' <=_r c!pc'" by blast
kleing@13062
   109
    moreover
kleing@13062
   110
    from ok
kleing@13078
   111
    have "c!pc' = \<bottom> \<Longrightarrow> s' = \<bottom>" by simp
kleing@13062
   112
    moreover
kleing@13062
   113
    from c_Some pc'
kleing@13078
   114
    have "c!pc' \<noteq> \<bottom> \<Longrightarrow> \<phi>!pc' = c!pc'" by auto
kleing@13062
   115
    ultimately
kleing@13078
   116
    show ?thesis by (cases "c!pc' = \<bottom>") auto 
kleing@13062
   117
  qed
kleing@9549
   118
qed
kleing@9012
   119
kleing@13078
   120
  
kleing@13080
   121
lemma (in lbvs) phi_not_top:
kleing@13078
   122
  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
kleing@13080
   123
  assumes pc:  "pc < length ins"
kleing@13078
   124
  shows "\<phi>!pc \<noteq> \<top>"
kleing@13078
   125
proof (cases "c!pc = \<bottom>")
kleing@13078
   126
  case False with pc
kleing@13078
   127
  have "\<phi>!pc = c!pc" ..
kleing@13080
   128
  also from cert pc have "\<dots> \<noteq> \<top>" by (rule cert_okD4)
kleing@13078
   129
  finally show ?thesis .
kleing@13078
   130
next
kleing@13078
   131
  case True with pc
kleing@13078
   132
  have "\<phi>!pc = wtl (take pc ins) c 0 s0" ..
kleing@13078
   133
  also from wtl have "\<dots> \<noteq> \<top>" by (rule wtl_take)
kleing@13078
   134
  finally show ?thesis .
kleing@13078
   135
qed
kleing@13207
   136
kleing@13215
   137
lemma (in lbvs) phi_in_A:
kleing@13215
   138
  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
kleing@13215
   139
  assumes s0:  "s0 \<in> A"
kleing@13215
   140
  shows "\<phi> \<in> list (length ins) A"
kleing@13215
   141
proof -
kleing@13215
   142
  { fix x assume "x \<in> set \<phi>"
kleing@13215
   143
    then obtain xs ys where "\<phi> = xs @ x # ys" 
kleing@13215
   144
      by (auto simp add: in_set_conv_decomp)
kleing@13215
   145
    then obtain pc where pc: "pc < length \<phi>" and x: "\<phi>!pc = x"
kleing@13215
   146
      by (simp add: that [of "length xs"] nth_append)
kleing@13215
   147
    
kleing@13215
   148
    from wtl s0 pc 
kleing@13215
   149
    have "wtl (take pc ins) c 0 s0 \<in> A" by (auto intro!: wtl_pres)
kleing@13215
   150
    moreover
kleing@13215
   151
    from pc have "pc < length ins" by simp
kleing@13215
   152
    with cert have "c!pc \<in> A" ..
kleing@13215
   153
    ultimately
kleing@13215
   154
    have "\<phi>!pc \<in> A" using pc by (simp add: phi_def)
kleing@13215
   155
    hence "x \<in> A" using x by simp
kleing@13215
   156
  } 
kleing@13215
   157
  hence "set \<phi> \<subseteq> A" ..
kleing@13215
   158
  thus ?thesis by (unfold list_def) simp
kleing@13215
   159
qed
kleing@13215
   160
kleing@13207
   161
kleing@13207
   162
lemma (in lbvs) phi0:
kleing@13207
   163
  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
kleing@13207
   164
  assumes 0:   "0 < length ins"
kleing@13207
   165
  shows "s0 <=_r \<phi>!0"
kleing@13207
   166
proof (cases "c!0 = \<bottom>")
kleing@13207
   167
  case True
kleing@13207
   168
  with 0 have "\<phi>!0 = wtl (take 0 ins) c 0 s0" ..
kleing@13207
   169
  moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp
kleing@13207
   170
  ultimately have "\<phi>!0 = s0" by simp
kleing@13207
   171
  thus ?thesis by simp
kleing@13207
   172
next
kleing@13207
   173
  case False
kleing@13207
   174
  with 0 have "phi!0 = c!0" ..
kleing@13207
   175
  moreover 
kleing@13207
   176
  have "wtl (take 1 ins) c 0 s0 \<noteq> \<top>"  by (rule wtl_take)
kleing@13207
   177
  with 0 False 
kleing@13207
   178
  have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm)
kleing@13207
   179
  ultimately
kleing@13207
   180
  show ?thesis by simp
kleing@13207
   181
qed
kleing@13207
   182
kleing@9376
   183
kleing@13080
   184
theorem (in lbvs) wtl_sound:
kleing@13078
   185
  assumes "wtl ins c 0 s0 \<noteq> \<top>" 
kleing@13080
   186
  assumes "s0 \<in> A" 
kleing@13078
   187
  shows "\<exists>ts. wt_step r \<top> step ts"
kleing@13207
   188
proof -
kleing@13207
   189
  have "wt_step r \<top> step \<phi>"
kleing@13207
   190
  proof (unfold wt_step_def, intro strip conjI)
kleing@13207
   191
    fix pc assume "pc < length \<phi>"
kleing@13207
   192
    then obtain "pc < length ins" by simp
kleing@13207
   193
    show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
kleing@13207
   194
    show "stable r step \<phi> pc" by (rule wtl_stable)
kleing@13207
   195
  qed
kleing@13207
   196
  thus ?thesis ..
kleing@13207
   197
qed
kleing@13207
   198
kleing@13207
   199
kleing@13207
   200
theorem (in lbvs) wtl_sound_strong:
kleing@13207
   201
  assumes "wtl ins c 0 s0 \<noteq> \<top>" 
kleing@13207
   202
  assumes "s0 \<in> A" 
kleing@13207
   203
  assumes "0 < length ins"
kleing@13215
   204
  shows "\<exists>ts \<in> list (length ins) A. wt_step r \<top> step ts \<and> s0 <=_r ts!0"
kleing@13215
   205
proof -
kleing@13215
   206
  have "\<phi> \<in> list (length ins) A" by (rule phi_in_A)
kleing@13215
   207
  moreover
kleing@13078
   208
  have "wt_step r \<top> step \<phi>"
kleing@13078
   209
  proof (unfold wt_step_def, intro strip conjI)
kleing@13078
   210
    fix pc assume "pc < length \<phi>"
kleing@13078
   211
    then obtain "pc < length ins" by simp
kleing@13078
   212
    show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
kleing@13078
   213
    show "stable r step \<phi> pc" by (rule wtl_stable)
kleing@13207
   214
  qed
kleing@13207
   215
  moreover
kleing@13207
   216
  have "s0 <=_r \<phi>!0" by (rule phi0)
kleing@13207
   217
  ultimately
kleing@13207
   218
  show ?thesis by fast
kleing@9549
   219
qed
kleing@9549
   220
kleing@13078
   221
end