src/HOL/Bali/Conform.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 63648 f9f3006a5579
child 68451 c34aa23a1fb6
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@12857
     1
(*  Title:      HOL/Bali/Conform.thy
schirmer@12854
     2
    Author:     David von Oheimb
schirmer@12854
     3
*)
schirmer@12854
     4
wenzelm@62042
     5
subsection \<open>Conformance notions for the type soundness proof for Java\<close>
schirmer@12854
     6
haftmann@16417
     7
theory Conform imports State begin
schirmer@12854
     8
wenzelm@62042
     9
text \<open>
schirmer@12854
    10
design issues:
schirmer@12854
    11
\begin{itemize}
schirmer@12854
    12
\item lconf allows for (arbitrary) inaccessible values
schirmer@12854
    13
\item ''conforms'' does not directly imply that the dynamic types of all 
schirmer@12854
    14
      objects on the heap are indeed existing classes. Yet this can be 
schirmer@12854
    15
      inferred for all referenced objs.
schirmer@12854
    16
\end{itemize}
wenzelm@62042
    17
\<close>
schirmer@12854
    18
wenzelm@41778
    19
type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
schirmer@12854
    20
schirmer@12854
    21
wenzelm@58887
    22
subsubsection "extension of global store"
schirmer@12854
    23
schirmer@12925
    24
haftmann@35416
    25
definition gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_"       [71,71]   70) where
schirmer@12854
    26
   "s\<le>|s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj"
schirmer@12854
    27
wenzelm@62042
    28
text \<open>For the the proof of type soundness we will need the 
schirmer@12925
    29
property that during execution, objects are not lost and moreover retain the 
schirmer@12925
    30
values of their tags. So the object store grows conservatively. Note that if 
schirmer@12925
    31
we considered garbage collection, we would have to restrict this property to 
schirmer@12925
    32
accessible objects.
wenzelm@62042
    33
\<close>
schirmer@12925
    34
schirmer@12854
    35
lemma gext_objD: 
schirmer@12854
    36
"\<lbrakk>s\<le>|s'; globs s r = Some obj\<rbrakk> 
schirmer@12854
    37
\<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj"
schirmer@12854
    38
apply (simp only: gext_def)
schirmer@12854
    39
by force
schirmer@12854
    40
schirmer@12854
    41
lemma rev_gext_objD: 
schirmer@12854
    42
"\<lbrakk>globs s r = Some obj; s\<le>|s'\<rbrakk> 
schirmer@12854
    43
 \<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj"
schirmer@12854
    44
by (auto elim: gext_objD)
schirmer@12854
    45
schirmer@12854
    46
lemma init_class_obj_inited: 
schirmer@12854
    47
   "init_class_obj G C s1\<le>|s2 \<Longrightarrow> inited C (globs s2)"
schirmer@12854
    48
apply (unfold inited_def init_obj_def)
schirmer@12854
    49
apply (auto dest!: gext_objD)
schirmer@12854
    50
done
schirmer@12854
    51
schirmer@12854
    52
lemma gext_refl [intro!, simp]: "s\<le>|s"
schirmer@12854
    53
apply (unfold gext_def)
schirmer@12854
    54
apply (fast del: fst_splitE)
schirmer@12854
    55
done
schirmer@12854
    56
schirmer@12854
    57
lemma gext_gupd [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|gupd(r\<mapsto>x)s"
schirmer@12854
    58
by (auto simp: gext_def)
schirmer@12854
    59
schirmer@12854
    60
lemma gext_new [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|init_obj G oi r s"
schirmer@12854
    61
apply (simp only: init_obj_def)
schirmer@12854
    62
apply (erule_tac gext_gupd)
schirmer@12854
    63
done
schirmer@12854
    64
schirmer@12854
    65
lemma gext_trans [elim]: "\<And>X. \<lbrakk>s\<le>|s'; s'\<le>|s''\<rbrakk> \<Longrightarrow> s\<le>|s''" 
schirmer@12854
    66
by (force simp: gext_def)
schirmer@12854
    67
schirmer@12854
    68
lemma gext_upd_gobj [intro!]: "s\<le>|upd_gobj r n v s"
schirmer@12854
    69
apply (simp only: gext_def)
schirmer@12854
    70
apply auto
schirmer@12854
    71
apply (case_tac "ra = r")
schirmer@12854
    72
apply auto
schirmer@12854
    73
apply (case_tac "globs s r = None")
schirmer@12854
    74
apply auto
schirmer@12854
    75
done
schirmer@12854
    76
schirmer@12854
    77
lemma gext_cong1 [simp]: "set_locals l s1\<le>|s2 = s1\<le>|s2"
schirmer@12854
    78
by (auto simp: gext_def)
schirmer@12854
    79
schirmer@12854
    80
lemma gext_cong2 [simp]: "s1\<le>|set_locals l s2 = s1\<le>|s2"
schirmer@12854
    81
by (auto simp: gext_def)
schirmer@12854
    82
schirmer@12854
    83
schirmer@12854
    84
lemma gext_lupd1 [simp]: "lupd(vn\<mapsto>v)s1\<le>|s2 = s1\<le>|s2"
schirmer@12854
    85
by (auto simp: gext_def)
schirmer@12854
    86
schirmer@12854
    87
lemma gext_lupd2 [simp]: "s1\<le>|lupd(vn\<mapsto>v)s2 = s1\<le>|s2"
schirmer@12854
    88
by (auto simp: gext_def)
schirmer@12854
    89
schirmer@12854
    90
schirmer@12854
    91
lemma inited_gext: "\<lbrakk>inited C (globs s); s\<le>|s'\<rbrakk> \<Longrightarrow> inited C (globs s')"
schirmer@12854
    92
apply (unfold inited_def)
schirmer@12854
    93
apply (auto dest: gext_objD)
schirmer@12854
    94
done
schirmer@12854
    95
schirmer@12854
    96
wenzelm@58887
    97
subsubsection "value conformance"
schirmer@12854
    98
wenzelm@37956
    99
definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
blanchet@55466
   100
  where "G,s\<turnstile>v\<Colon>\<preceq>T = (\<exists>T'\<in>typeof (\<lambda>a. map_option obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T)"
schirmer@12854
   101
schirmer@12854
   102
lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
schirmer@12854
   103
by (auto simp: conf_def)
schirmer@12854
   104
schirmer@12854
   105
lemma conf_lupd [simp]: "G,lupd(vn\<mapsto>va)s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
schirmer@12854
   106
by (auto simp: conf_def)
schirmer@12854
   107
schirmer@12854
   108
lemma conf_PrimT [simp]: "\<forall>dt. typeof dt v = Some (PrimT t) \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>PrimT t"
schirmer@12854
   109
apply (simp add: conf_def)
schirmer@12854
   110
done
schirmer@12854
   111
schirmer@13688
   112
lemma conf_Boolean: "G,s\<turnstile>v\<Colon>\<preceq>PrimT Boolean \<Longrightarrow> \<exists> b. v=Bool b"
schirmer@13688
   113
by (cases v)
schirmer@13688
   114
   (auto simp: conf_def obj_ty_def 
schirmer@13688
   115
         dest: widen_Boolean2 
schirmer@13688
   116
        split: obj_tag.splits)
schirmer@13688
   117
schirmer@13688
   118
schirmer@12854
   119
lemma conf_litval [rule_format (no_asm)]: 
schirmer@12854
   120
  "typeof (\<lambda>a. None) v = Some T \<longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
schirmer@12854
   121
apply (unfold conf_def)
schirmer@12854
   122
apply (rule val.induct)
schirmer@12854
   123
apply auto
schirmer@12854
   124
done
schirmer@12854
   125
schirmer@12854
   126
lemma conf_Null [simp]: "G,s\<turnstile>Null\<Colon>\<preceq>T = G\<turnstile>NT\<preceq>T"
schirmer@12854
   127
by (simp add: conf_def)
schirmer@12854
   128
schirmer@12854
   129
lemma conf_Addr: 
schirmer@12854
   130
  "G,s\<turnstile>Addr a\<Colon>\<preceq>T = (\<exists>obj. heap s a = Some obj \<and> G\<turnstile>obj_ty obj\<preceq>T)"
schirmer@12854
   131
by (auto simp: conf_def)
schirmer@12854
   132
schirmer@12854
   133
lemma conf_AddrI:"\<lbrakk>heap s a = Some obj; G\<turnstile>obj_ty obj\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T"
schirmer@12854
   134
apply (rule conf_Addr [THEN iffD2])
schirmer@12854
   135
by fast
schirmer@12854
   136
schirmer@12854
   137
lemma defval_conf [rule_format (no_asm), elim]: 
schirmer@12854
   138
  "is_type G T \<longrightarrow> G,s\<turnstile>default_val T\<Colon>\<preceq>T"
schirmer@12854
   139
apply (unfold conf_def)
schirmer@12854
   140
apply (induct "T")
schirmer@12854
   141
apply (auto intro: prim_ty.induct)
schirmer@12854
   142
done
schirmer@12854
   143
schirmer@12854
   144
lemma conf_widen [rule_format (no_asm), elim]: 
schirmer@12854
   145
  "G\<turnstile>T\<preceq>T' \<Longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T \<longrightarrow> ws_prog G \<longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T'"
schirmer@12854
   146
apply (unfold conf_def)
schirmer@12854
   147
apply (rule val.induct)
schirmer@12854
   148
apply (auto elim: ws_widen_trans)
schirmer@12854
   149
done
schirmer@12854
   150
schirmer@12854
   151
lemma conf_gext [rule_format (no_asm), elim]: 
schirmer@12854
   152
  "G,s\<turnstile>v\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T"
schirmer@12854
   153
apply (unfold gext_def conf_def)
schirmer@12854
   154
apply (rule val.induct)
schirmer@12854
   155
apply force+
schirmer@12854
   156
done
schirmer@12854
   157
schirmer@12854
   158
schirmer@12854
   159
lemma conf_list_widen [rule_format (no_asm)]: 
schirmer@12854
   160
"ws_prog G \<Longrightarrow>  
schirmer@12854
   161
  \<forall>Ts Ts'. list_all2 (conf G s) vs Ts 
schirmer@12854
   162
           \<longrightarrow>   G\<turnstile>Ts[\<preceq>] Ts' \<longrightarrow> list_all2 (conf G s) vs Ts'"
schirmer@12854
   163
apply (unfold widens_def)
schirmer@12854
   164
apply (rule list_all2_trans)
schirmer@12854
   165
apply auto
schirmer@12854
   166
done
schirmer@12854
   167
schirmer@12854
   168
lemma conf_RefTD [rule_format (no_asm)]: 
schirmer@12854
   169
 "G,s\<turnstile>a'\<Colon>\<preceq>RefT T 
schirmer@12854
   170
  \<longrightarrow> a' = Null \<or> (\<exists>a obj T'. a' = Addr a \<and> heap s a = Some obj \<and>  
schirmer@12854
   171
                    obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)"
schirmer@12854
   172
apply (unfold conf_def)
schirmer@12854
   173
apply (induct_tac "a'")
schirmer@12854
   174
apply (auto dest: widen_PrimT)
schirmer@12854
   175
done
schirmer@12854
   176
schirmer@12854
   177
wenzelm@58887
   178
subsubsection "value list conformance"
schirmer@12854
   179
wenzelm@37956
   180
definition
wenzelm@37956
   181
  lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
wenzelm@37956
   182
  where "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
schirmer@12854
   183
schirmer@12854
   184
lemma lconfD: "\<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T"
schirmer@12854
   185
by (force simp: lconf_def)
schirmer@12854
   186
schirmer@12854
   187
schirmer@12854
   188
lemma lconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
schirmer@12854
   189
by (auto simp: lconf_def)
schirmer@12854
   190
schirmer@12854
   191
lemma lconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
schirmer@12854
   192
by (auto simp: lconf_def)
schirmer@12854
   193
schirmer@12854
   194
(* unused *)
schirmer@12854
   195
lemma lconf_new: "\<lbrakk>L vn = None; G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
schirmer@12854
   196
by (auto simp: lconf_def)
schirmer@12854
   197
schirmer@12854
   198
lemma lconf_upd: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow>  
schirmer@12854
   199
  G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
schirmer@12854
   200
by (auto simp: lconf_def)
schirmer@12854
   201
schirmer@12854
   202
lemma lconf_ext: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L(vn\<mapsto>T)"
schirmer@12854
   203
by (auto simp: lconf_def)
schirmer@12854
   204
schirmer@12854
   205
lemma lconf_map_sum [simp]: 
schirmer@12854
   206
 "G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<Colon>\<preceq>]L2)"
schirmer@12854
   207
apply (unfold lconf_def)
schirmer@12854
   208
apply safe
schirmer@12854
   209
apply (case_tac [3] "n")
nipkow@63648
   210
apply (force split: sum.split)+
schirmer@12854
   211
done
schirmer@12854
   212
schirmer@12854
   213
lemma lconf_ext_list [rule_format (no_asm)]: "
schirmer@12854
   214
 \<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
wenzelm@12893
   215
      \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
schirmer@12854
   216
      \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
schirmer@12854
   217
apply (unfold lconf_def)
schirmer@12854
   218
apply (induct_tac "vns")
schirmer@12854
   219
apply  clarsimp
nipkow@14025
   220
apply clarify
schirmer@12854
   221
apply (frule list_all2_lengthD)
nipkow@14025
   222
apply (clarsimp)
schirmer@12854
   223
done
schirmer@12854
   224
schirmer@12854
   225
schirmer@12854
   226
lemma lconf_deallocL: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<Colon>\<preceq>]L"
schirmer@12854
   227
apply (simp only: lconf_def)
schirmer@12854
   228
apply safe
schirmer@12854
   229
apply (drule spec)
schirmer@12854
   230
apply (drule ospec)
schirmer@12854
   231
apply auto
schirmer@12854
   232
done 
schirmer@12854
   233
schirmer@12854
   234
schirmer@12854
   235
lemma lconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<Colon>\<preceq>]L"
schirmer@12854
   236
apply (simp only: lconf_def)
schirmer@12854
   237
apply fast
schirmer@12854
   238
done
schirmer@12854
   239
schirmer@12854
   240
lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty"
schirmer@12854
   241
apply (unfold lconf_def)
schirmer@12854
   242
apply force
schirmer@12854
   243
done
schirmer@12854
   244
schirmer@12854
   245
lemma lconf_init_vals [intro!]: 
wenzelm@32960
   246
        " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs"
schirmer@12854
   247
apply (unfold lconf_def)
schirmer@12854
   248
apply force
schirmer@12854
   249
done
schirmer@12854
   250
wenzelm@58887
   251
subsubsection "weak value list conformance"
schirmer@13688
   252
wenzelm@62042
   253
text \<open>Only if the value is defined it has to conform to its type. 
schirmer@13688
   254
        This is the contribution of the definite assignment analysis to 
schirmer@13688
   255
        the notion of conformance. The definite assignment analysis ensures
schirmer@13688
   256
        that the program only attempts to access local variables that 
schirmer@13688
   257
        actually have a defined value in the state. 
schirmer@13688
   258
        So conformance must only ensure that the
schirmer@13688
   259
        defined values are of the right type, and not also that the value
schirmer@13688
   260
        is defined. 
wenzelm@62042
   261
\<close>
schirmer@13688
   262
schirmer@13688
   263
  
wenzelm@37956
   264
definition
wenzelm@37956
   265
  wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
wenzelm@37956
   266
  where "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
schirmer@13688
   267
schirmer@13688
   268
lemma wlconfD: "\<lbrakk>G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts; Ts n = Some T; vs n = Some v\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
schirmer@13688
   269
by (auto simp: wlconf_def)
schirmer@13688
   270
schirmer@13688
   271
schirmer@13688
   272
lemma wlconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<sim>\<Colon>\<preceq>]L = G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
schirmer@13688
   273
by (auto simp: wlconf_def)
schirmer@13688
   274
schirmer@13688
   275
lemma wlconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<sim>\<Colon>\<preceq>]L = G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
schirmer@13688
   276
by (auto simp: wlconf_def)
schirmer@13688
   277
schirmer@13688
   278
schirmer@13688
   279
lemma wlconf_upd: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow>  
schirmer@13688
   280
  G,s\<turnstile>l(vn\<mapsto>v)[\<sim>\<Colon>\<preceq>]L"
schirmer@13688
   281
by (auto simp: wlconf_def)
schirmer@13688
   282
schirmer@13688
   283
lemma wlconf_ext: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<sim>\<Colon>\<preceq>]L(vn\<mapsto>T)"
schirmer@13688
   284
by (auto simp: wlconf_def)
schirmer@13688
   285
schirmer@13688
   286
lemma wlconf_map_sum [simp]: 
schirmer@13688
   287
 "G,s\<turnstile>l1 (+) l2[\<sim>\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<sim>\<Colon>\<preceq>]L2)"
schirmer@13688
   288
apply (unfold wlconf_def)
schirmer@13688
   289
apply safe
schirmer@13688
   290
apply (case_tac [3] "n")
nipkow@63648
   291
apply (force split: sum.split)+
schirmer@13688
   292
done
schirmer@13688
   293
schirmer@13688
   294
lemma wlconf_ext_list [rule_format (no_asm)]: "
schirmer@13688
   295
 \<And>X. \<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
schirmer@13688
   296
      \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
schirmer@13688
   297
      \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<sim>\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
schirmer@13688
   298
apply (unfold wlconf_def)
schirmer@13688
   299
apply (induct_tac "vns")
schirmer@13688
   300
apply  clarsimp
nipkow@14025
   301
apply clarify
schirmer@13688
   302
apply (frule list_all2_lengthD)
schirmer@13688
   303
apply clarsimp
schirmer@13688
   304
done
schirmer@13688
   305
schirmer@13688
   306
schirmer@13688
   307
lemma wlconf_deallocL: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
schirmer@13688
   308
apply (simp only: wlconf_def)
schirmer@13688
   309
apply safe
schirmer@13688
   310
apply (drule spec)
schirmer@13688
   311
apply (drule ospec)
schirmer@13688
   312
defer
schirmer@13688
   313
apply (drule ospec )
schirmer@13688
   314
apply auto
schirmer@13688
   315
done 
schirmer@13688
   316
schirmer@13688
   317
schirmer@13688
   318
lemma wlconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
schirmer@13688
   319
apply (simp only: wlconf_def)
schirmer@13688
   320
apply fast
schirmer@13688
   321
done
schirmer@13688
   322
schirmer@13688
   323
lemma wlconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]empty"
schirmer@13688
   324
apply (unfold wlconf_def)
schirmer@13688
   325
apply force
schirmer@13688
   326
done
schirmer@13688
   327
schirmer@13688
   328
lemma wlconf_empty_vals: "G,s\<turnstile>empty[\<sim>\<Colon>\<preceq>]ts"
schirmer@13688
   329
  by (simp add: wlconf_def)
schirmer@13688
   330
schirmer@13688
   331
lemma wlconf_init_vals [intro!]: 
wenzelm@32960
   332
        " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<sim>\<Colon>\<preceq>]fs"
schirmer@13688
   333
apply (unfold wlconf_def)
schirmer@13688
   334
apply force
schirmer@13688
   335
done
schirmer@13688
   336
schirmer@13688
   337
lemma lconf_wlconf:
schirmer@13688
   338
 "G,s\<turnstile>l[\<Colon>\<preceq>]L \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
schirmer@13688
   339
by (force simp add: lconf_def wlconf_def)
schirmer@12854
   340
wenzelm@58887
   341
subsubsection "object conformance"
schirmer@12854
   342
wenzelm@37956
   343
definition
wenzelm@37956
   344
  oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
wenzelm@37956
   345
  "(G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r) = (G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
schirmer@12854
   346
                           (case r of 
wenzelm@32960
   347
                              Heap a \<Rightarrow> is_type G (obj_ty obj) 
wenzelm@37956
   348
                            | Stat C \<Rightarrow> True))"
schirmer@13688
   349
schirmer@13688
   350
schirmer@12854
   351
lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
schirmer@12854
   352
by (auto simp: oconf_def Let_def)
schirmer@12854
   353
schirmer@12854
   354
lemma oconf_lconf: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<Longrightarrow> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r"
schirmer@12854
   355
by (simp add: oconf_def) 
schirmer@12854
   356
schirmer@12854
   357
lemma oconf_cong [simp]: "G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r = G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
schirmer@12854
   358
by (auto simp: oconf_def Let_def)
schirmer@12854
   359
schirmer@12854
   360
lemma oconf_init_obj_lemma: 
schirmer@12854
   361
"\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (DeclConcepts.fields G C);  
schirmer@12854
   362
  \<And>C c f fld. \<lbrakk>class G C = Some c; 
schirmer@12854
   363
                table_of (DeclConcepts.fields G C) f = Some fld \<rbrakk> 
schirmer@12854
   364
            \<Longrightarrow> is_type G (type fld);  
schirmer@12854
   365
  (case r of 
schirmer@12854
   366
     Heap a \<Rightarrow> is_type G (obj_ty obj) 
schirmer@12854
   367
  | Stat C \<Rightarrow> is_class G C)
schirmer@12854
   368
\<rbrakk> \<Longrightarrow>  G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
schirmer@12854
   369
apply (auto simp add: oconf_def)
schirmer@12854
   370
apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
schirmer@12854
   371
defer
schirmer@12854
   372
apply (subst obj_ty_cong)
nipkow@63648
   373
apply (auto dest!: fields_table_SomeD split: sum.split_asm obj_tag.split_asm)
schirmer@12854
   374
done
schirmer@12854
   375
wenzelm@58887
   376
subsubsection "state conformance"
schirmer@12854
   377
wenzelm@37956
   378
definition
wenzelm@37956
   379
  conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"  ("_\<Colon>\<preceq>_" [71,71] 70)  where
wenzelm@37956
   380
   "xs\<Colon>\<preceq>E =
wenzelm@37956
   381
      (let (G, L) = E; s = snd xs; l = locals s in
wenzelm@46212
   382
        (\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and> G,s\<turnstile>l [\<sim>\<Colon>\<preceq>]L \<and>
wenzelm@37956
   383
        (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
wenzelm@37956
   384
             (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None))"
schirmer@12854
   385
wenzelm@58887
   386
subsubsection "conforms"
schirmer@12854
   387
schirmer@12854
   388
lemma conforms_globsD: 
schirmer@12854
   389
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
schirmer@12854
   390
by (auto simp: conforms_def Let_def)
schirmer@12854
   391
schirmer@13688
   392
lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L"
schirmer@12854
   393
by (auto simp: conforms_def Let_def)
schirmer@12854
   394
schirmer@12854
   395
lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow>  
wenzelm@32960
   396
          G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
schirmer@12854
   397
by (auto simp: conforms_def Let_def)
schirmer@12854
   398
schirmer@13688
   399
lemma conforms_RetD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Jump Ret)\<rbrakk> \<Longrightarrow>  
wenzelm@32960
   400
          (locals s) Result \<noteq> None"
schirmer@13688
   401
by (auto simp: conforms_def Let_def)
schirmer@13688
   402
schirmer@12854
   403
lemma conforms_RefTD: 
schirmer@12854
   404
 "\<lbrakk>G,s\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x,s) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow>  
schirmer@12854
   405
   \<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and>  
schirmer@12854
   406
   G\<turnstile>obj_ty obj\<preceq>RefT t \<and> is_type G (obj_ty obj)"
schirmer@12854
   407
apply (drule_tac conf_RefTD)
schirmer@12854
   408
apply clarsimp
schirmer@12854
   409
apply (rule conforms_globsD [THEN oconf_is_type])
schirmer@12854
   410
apply auto
schirmer@12854
   411
done
schirmer@12854
   412
schirmer@12854
   413
lemma conforms_Jump [iff]:
schirmer@13688
   414
  "j=Ret \<longrightarrow> locals s Result \<noteq> None 
schirmer@13688
   415
   \<Longrightarrow> ((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
schirmer@13688
   416
by (auto simp: conforms_def Let_def)
schirmer@12854
   417
schirmer@12854
   418
lemma conforms_StdXcpt [iff]: 
schirmer@12854
   419
  "((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
schirmer@12854
   420
by (auto simp: conforms_def)
schirmer@12854
   421
schirmer@12925
   422
lemma conforms_Err [iff]:
schirmer@12925
   423
   "((Some (Error e), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
schirmer@12925
   424
  by (auto simp: conforms_def)  
schirmer@12925
   425
schirmer@12854
   426
lemma conforms_raise_if [iff]: 
schirmer@12854
   427
  "((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
schirmer@12854
   428
by (auto simp: abrupt_if_def)
schirmer@12854
   429
schirmer@12925
   430
lemma conforms_error_if [iff]: 
schirmer@12925
   431
  "((error_if c err x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
wenzelm@46222
   432
by (auto simp: abrupt_if_def)
schirmer@12854
   433
schirmer@12854
   434
lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
schirmer@12854
   435
by (auto simp: conforms_def Let_def)
schirmer@12854
   436
schirmer@12854
   437
lemma conforms_absorb [rule_format]:
schirmer@12854
   438
  "(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)"
schirmer@12854
   439
apply (rule impI)
blanchet@55417
   440
apply (case_tac a)
schirmer@12854
   441
apply (case_tac "absorb j a")
schirmer@12854
   442
apply auto
thomas@57492
   443
apply (rename_tac a')
thomas@57492
   444
apply (case_tac "absorb j (Some a')",auto)
schirmer@12854
   445
apply (erule conforms_NormI)
schirmer@12854
   446
done
schirmer@12854
   447
schirmer@12854
   448
lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
schirmer@13688
   449
     G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L;  
schirmer@13688
   450
     \<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
schirmer@13688
   451
     x = Some (Jump Ret)\<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
schirmer@12854
   452
  (x, s)\<Colon>\<preceq>(G, L)"
schirmer@12854
   453
by (auto simp: conforms_def Let_def)
schirmer@12854
   454
schirmer@12854
   455
lemma conforms_xconf: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L);   
schirmer@13688
   456
 \<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
schirmer@13688
   457
     x' = Some (Jump Ret) \<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
schirmer@12854
   458
 (x',s)\<Colon>\<preceq>(G,L)"
schirmer@12854
   459
by (fast intro: conformsI elim: conforms_globsD conforms_localD)
schirmer@12854
   460
schirmer@12854
   461
lemma conforms_lupd: 
schirmer@12854
   462
 "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); L vn = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L)"
schirmer@13688
   463
by (force intro: conformsI wlconf_upd dest: conforms_globsD conforms_localD 
schirmer@13688
   464
                                           conforms_XcptLocD conforms_RetD 
schirmer@13688
   465
          simp: oconf_def)
schirmer@12854
   466
schirmer@12854
   467
schirmer@13688
   468
lemmas conforms_allocL_aux = conforms_localD [THEN wlconf_ext]
schirmer@12854
   469
schirmer@12854
   470
lemma conforms_allocL: 
schirmer@12854
   471
  "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L(vn\<mapsto>T))"
schirmer@13688
   472
by (force intro: conformsI dest: conforms_globsD conforms_RetD 
schirmer@13688
   473
          elim: conforms_XcptLocD  conforms_allocL_aux 
schirmer@13688
   474
          simp: oconf_def)
schirmer@12854
   475
schirmer@13688
   476
lemmas conforms_deallocL_aux = conforms_localD [THEN wlconf_deallocL]
schirmer@12854
   477
schirmer@12854
   478
lemma conforms_deallocL: "\<And>s.\<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)"
schirmer@13688
   479
by (fast intro: conformsI dest: conforms_globsD conforms_RetD
schirmer@12854
   480
         elim: conforms_XcptLocD conforms_deallocL_aux)
schirmer@12854
   481
schirmer@12854
   482
lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s';  
schirmer@12854
   483
  \<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
schirmer@12854
   484
   locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)"
schirmer@13688
   485
apply (rule conformsI)
schirmer@13688
   486
apply     assumption
schirmer@13688
   487
apply    (drule conforms_localD) apply force
schirmer@13688
   488
apply   (intro strip)
schirmer@13688
   489
apply  (drule (1) conforms_XcptLocD) apply force 
schirmer@13688
   490
apply (intro strip)
schirmer@13688
   491
apply (drule (1) conforms_RetD) apply force
schirmer@13688
   492
done
schirmer@13688
   493
schirmer@12854
   494
schirmer@12854
   495
schirmer@12854
   496
lemma conforms_xgext: 
schirmer@13688
   497
  "\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s;dom (locals s') \<subseteq> dom (locals s)\<rbrakk> 
schirmer@13688
   498
   \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
schirmer@12854
   499
apply (erule_tac conforms_xconf)
schirmer@13688
   500
apply  (fast dest: conforms_XcptLocD)
schirmer@13688
   501
apply (intro strip)
schirmer@13688
   502
apply (drule (1) conforms_RetD) 
schirmer@13688
   503
apply (auto dest: domI)
schirmer@12854
   504
done
schirmer@12854
   505
schirmer@12854
   506
lemma conforms_gupd: "\<And>obj. \<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r; s\<le>|gupd(r\<mapsto>obj)s\<rbrakk> 
schirmer@12854
   507
\<Longrightarrow>  (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)"
schirmer@12854
   508
apply (rule conforms_gext)
schirmer@12854
   509
apply    auto
schirmer@12854
   510
apply (force dest: conforms_globsD simp add: oconf_def)+
schirmer@12854
   511
done
schirmer@12854
   512
schirmer@12854
   513
lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some obj; 
schirmer@12854
   514
  var_tys G (tag obj) r n = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x,upd_gobj r n v s)\<Colon>\<preceq>(G,L)"
schirmer@12854
   515
apply (rule conforms_gext)
schirmer@12854
   516
apply auto
schirmer@12854
   517
apply (drule (1) conforms_globsD)
schirmer@12854
   518
apply (simp add: oconf_def)
schirmer@12854
   519
apply safe
schirmer@12854
   520
apply (rule lconf_upd)
schirmer@12854
   521
apply auto
wenzelm@63566
   522
apply (simp only: obj_ty_cong)
schirmer@12854
   523
apply (force dest: conforms_globsD intro!: lconf_upd 
wenzelm@63566
   524
       simp add: oconf_def cong del: old.sum.case_cong_weak)
schirmer@12854
   525
done
schirmer@12854
   526
schirmer@12854
   527
lemma conforms_set_locals: 
schirmer@13688
   528
  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; x=Some (Jump Ret) \<longrightarrow> l Result \<noteq> None\<rbrakk> 
schirmer@13688
   529
   \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)"
schirmer@13688
   530
apply (rule conformsI)
schirmer@13688
   531
apply     (intro strip)
schirmer@13688
   532
apply     simp
schirmer@13688
   533
apply     (drule (2) conforms_globsD)
schirmer@13688
   534
apply    simp
schirmer@13688
   535
apply   (intro strip)
schirmer@13688
   536
apply   (drule (1) conforms_XcptLocD)
schirmer@13688
   537
apply   simp
schirmer@13688
   538
apply (intro strip)
schirmer@13688
   539
apply (drule (1) conforms_RetD)
schirmer@13688
   540
apply simp
schirmer@12854
   541
done
schirmer@12854
   542
schirmer@13688
   543
lemma conforms_locals: 
schirmer@13688
   544
  "\<lbrakk>(a,b)\<Colon>\<preceq>(G, L); L x = Some T;locals b x \<noteq>None\<rbrakk>
schirmer@13688
   545
   \<Longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T"
schirmer@13688
   546
apply (force simp: conforms_def Let_def wlconf_def)
schirmer@12925
   547
done
schirmer@12925
   548
schirmer@13688
   549
lemma conforms_return: 
schirmer@13688
   550
"\<And>s'. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); (x',s')\<Colon>\<preceq>(G, L'); s\<le>|s';x'\<noteq>Some (Jump Ret)\<rbrakk> \<Longrightarrow>  
schirmer@12854
   551
  (x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)"
schirmer@12854
   552
apply (rule conforms_xconf)
schirmer@12854
   553
prefer 2 apply (force dest: conforms_XcptLocD)
schirmer@12854
   554
apply (erule conforms_gext)
schirmer@12854
   555
apply (force dest: conforms_globsD)+
schirmer@12854
   556
done
schirmer@12854
   557
schirmer@12854
   558
end