src/HOL/Bali/Conform.thy
author wenzelm
Mon, 25 Feb 2002 20:48:14 +0100
changeset 12937 0c4fd7529467
parent 12925 99131847fb93
child 13688 a0b16d42d489
permissions -rw-r--r--
clarified syntax of ``long'' statements: fixes/assumes/shows;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Conform.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
12858
wenzelm
parents: 12857
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
header {* Conformance notions for the type soundness proof for Java *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
theory Conform = State:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\item lconf allows for (arbitrary) inaccessible values
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
\item ''conforms'' does not directly imply that the dynamic types of all 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
      objects on the heap are indeed existing classes. Yet this can be 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
      inferred for all referenced objs.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
types	env_ = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
section "extension of global store"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    26
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
  gext    :: "st \<Rightarrow> st \<Rightarrow> bool"                ("_\<le>|_"       [71,71]   70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
   "s\<le>|s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    32
text {* For the the proof of type soundness we will need the 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    33
property that during execution, objects are not lost and moreover retain the 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    34
values of their tags. So the object store grows conservatively. Note that if 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    35
we considered garbage collection, we would have to restrict this property to 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    36
accessible objects.
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    37
*}
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    38
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
lemma gext_objD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
"\<lbrakk>s\<le>|s'; globs s r = Some obj\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
\<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
apply (simp only: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
by force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
lemma rev_gext_objD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
"\<lbrakk>globs s r = Some obj; s\<le>|s'\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
 \<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
by (auto elim: gext_objD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
lemma init_class_obj_inited: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
   "init_class_obj G C s1\<le>|s2 \<Longrightarrow> inited C (globs s2)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
apply (unfold inited_def init_obj_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
apply (auto dest!: gext_objD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
lemma gext_refl [intro!, simp]: "s\<le>|s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
apply (unfold gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
apply (fast del: fst_splitE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
lemma gext_gupd [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|gupd(r\<mapsto>x)s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
by (auto simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
lemma gext_new [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|init_obj G oi r s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
apply (simp only: init_obj_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
apply (erule_tac gext_gupd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
lemma gext_trans [elim]: "\<And>X. \<lbrakk>s\<le>|s'; s'\<le>|s''\<rbrakk> \<Longrightarrow> s\<le>|s''" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
by (force simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
lemma gext_upd_gobj [intro!]: "s\<le>|upd_gobj r n v s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
apply (simp only: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
apply (case_tac "ra = r")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
apply (case_tac "globs s r = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
lemma gext_cong1 [simp]: "set_locals l s1\<le>|s2 = s1\<le>|s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
by (auto simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
lemma gext_cong2 [simp]: "s1\<le>|set_locals l s2 = s1\<le>|s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
by (auto simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
lemma gext_lupd1 [simp]: "lupd(vn\<mapsto>v)s1\<le>|s2 = s1\<le>|s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
by (auto simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
lemma gext_lupd2 [simp]: "s1\<le>|lupd(vn\<mapsto>v)s2 = s1\<le>|s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
by (auto simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
lemma inited_gext: "\<lbrakk>inited C (globs s); s\<le>|s'\<rbrakk> \<Longrightarrow> inited C (globs s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
apply (unfold inited_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
apply (auto dest: gext_objD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
section "value conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
  conf  :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool"    ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
	   "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. option_map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
by (auto simp: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
lemma conf_lupd [simp]: "G,lupd(vn\<mapsto>va)s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
by (auto simp: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
lemma conf_PrimT [simp]: "\<forall>dt. typeof dt v = Some (PrimT t) \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>PrimT t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
apply (simp add: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
lemma conf_litval [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
  "typeof (\<lambda>a. None) v = Some T \<longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
apply (rule val.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
lemma conf_Null [simp]: "G,s\<turnstile>Null\<Colon>\<preceq>T = G\<turnstile>NT\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
by (simp add: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
lemma conf_Addr: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
  "G,s\<turnstile>Addr a\<Colon>\<preceq>T = (\<exists>obj. heap s a = Some obj \<and> G\<turnstile>obj_ty obj\<preceq>T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
by (auto simp: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
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"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
apply (rule conf_Addr [THEN iffD2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
by fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
lemma defval_conf [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
  "is_type G T \<longrightarrow> G,s\<turnstile>default_val T\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
apply (induct "T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
apply (auto intro: prim_ty.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
lemma conf_widen [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
  "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'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
apply (rule val.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
apply (auto elim: ws_widen_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
lemma conf_gext [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
  "G,s\<turnstile>v\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
apply (unfold gext_def conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
apply (rule val.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
apply force+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
lemma conf_list_widen [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
"ws_prog G \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
  \<forall>Ts Ts'. list_all2 (conf G s) vs Ts 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
           \<longrightarrow>   G\<turnstile>Ts[\<preceq>] Ts' \<longrightarrow> list_all2 (conf G s) vs Ts'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
apply (unfold widens_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
apply (rule list_all2_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
lemma conf_RefTD [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
 "G,s\<turnstile>a'\<Colon>\<preceq>RefT T 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
  \<longrightarrow> a' = Null \<or> (\<exists>a obj T'. a' = Addr a \<and> heap s a = Some obj \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
                    obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
apply (induct_tac "a'")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
apply (auto dest: widen_PrimT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
section "value list conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
  lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
                                                ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
           "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
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"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
by (force simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
lemma lconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
lemma lconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
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"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
lemma lconf_upd: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
  G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
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)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
lemma lconf_map_sum [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
 "G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<Colon>\<preceq>]L2)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
apply (case_tac [3] "n")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
apply (force split add: sum.split)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
lemma lconf_ext_list [rule_format (no_asm)]: "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
 \<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
12893
cbb4dc5e6478 replaced nodups by distinct;
wenzelm
parents: 12858
diff changeset
   216
      \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
      \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
apply (induct_tac "vns")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
apply (frule list_all2_lengthD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
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"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
apply (simp only: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
apply (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
apply (drule ospec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
done 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
lemma lconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<Colon>\<preceq>]L"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
apply (simp only: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
lemma lconf_init_vals [intro!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
	" \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
section "object conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
  oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool"  ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
	   "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
                           (case r of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
		              Heap a \<Rightarrow> is_type G (obj_ty obj) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
                            | Stat C \<Rightarrow> True)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
lemma oconf_def2:  "G,s\<turnstile>\<lparr>tag=oi,values=fs\<rparr>\<Colon>\<preceq>\<surd>r =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
  (G,s\<turnstile>fs[\<Colon>\<preceq>]var_tys G oi r \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
  (case r of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>) | Stat C \<Rightarrow> True))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
by (simp add: oconf_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
lemma oconf_def2:  "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
  (G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
  (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> True))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
by (simp add: oconf_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
by (auto simp: oconf_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
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"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
by (simp add: oconf_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
lemma oconf_cong [simp]: "G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r = G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
by (auto simp: oconf_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
lemma oconf_init_obj_lemma: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
"\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (DeclConcepts.fields G C);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
  \<And>C c f fld. \<lbrakk>class G C = Some c; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
                table_of (DeclConcepts.fields G C) f = Some fld \<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
            \<Longrightarrow> is_type G (type fld);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
  (case r of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
     Heap a \<Rightarrow> is_type G (obj_ty obj) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
  | Stat C \<Rightarrow> is_class G C)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
\<rbrakk> \<Longrightarrow>  G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
apply (auto simp add: oconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
apply (subst obj_ty_cong)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
apply(auto dest!: fields_table_SomeD obj_ty_CInst1 obj_ty_Arr1
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
           split add: sum.split_asm obj_tag.split_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
lemma oconf_init_obj_lemma: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
"\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (fields G C);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
  \<And>C c f fld. \<lbrakk>class G C = Some c; table_of (fields G C) f = Some fld \<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
            \<Longrightarrow> is_type G (type fld);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
  (case r of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
     Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
  | Stat C \<Rightarrow> is_class G C)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
\<rbrakk> \<Longrightarrow>  G,s\<turnstile>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>\<Colon>\<preceq>\<surd>r"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
apply (auto simp add: oconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
apply (subst obj_ty_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
apply(auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
section "state conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
  conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
   "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
      (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
                  \<spacespace>                   G,s\<turnstile>l    [\<Colon>\<preceq>]L\<spacespace> \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
      (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
section "conforms"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
lemma conforms_globsD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<Colon>\<preceq>]L"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
	  G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
lemma conforms_RefTD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
 "\<lbrakk>G,s\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x,s) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
   \<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
   G\<turnstile>obj_ty obj\<preceq>RefT t \<and> is_type G (obj_ty obj)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
apply (drule_tac conf_RefTD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
apply (rule conforms_globsD [THEN oconf_is_type])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
lemma conforms_Jump [iff]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
  "((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
by (auto simp: conforms_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
lemma conforms_StdXcpt [iff]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
  "((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
by (auto simp: conforms_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   359
lemma conforms_Err [iff]:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   360
   "((Some (Error e), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   361
  by (auto simp: conforms_def)  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   362
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
lemma conforms_raise_if [iff]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
  "((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
by (auto simp: abrupt_if_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   367
lemma conforms_error_if [iff]: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   368
  "((error_if c err x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   369
by (auto simp: abrupt_if_def split: split_if)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
lemma conforms_absorb [rule_format]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
  "(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
apply (rule impI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
apply ( case_tac a)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
apply (case_tac "absorb j a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
apply (case_tac "absorb j (Some a)",auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
apply (erule conforms_NormI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
     G,s\<turnstile>locals s[\<Colon>\<preceq>]L;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
     \<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
  (x, s)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
lemma conforms_xconf: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L);   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
 \<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
 (x',s)\<Colon>\<preceq>(G,L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
by (fast intro: conformsI elim: conforms_globsD conforms_localD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
lemma conforms_lupd: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
 "\<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)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
by (force intro: conformsI lconf_upd dest: conforms_globsD conforms_localD 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
                                           conforms_XcptLocD simp: oconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
lemmas conforms_allocL_aux = conforms_localD [THEN lconf_ext]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
lemma conforms_allocL: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
  "\<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))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
by (force intro: conformsI dest: conforms_globsD 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
          elim: conforms_XcptLocD conforms_allocL_aux simp: oconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
lemmas conforms_deallocL_aux = conforms_localD [THEN lconf_deallocL]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
lemma conforms_deallocL: "\<And>s.\<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
by (fast intro: conformsI dest: conforms_globsD 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   412
         elim: conforms_XcptLocD conforms_deallocL_aux)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   413
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   414
lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s';  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   415
  \<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
   locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
by (force intro!: conformsI dest: conforms_localD conforms_XcptLocD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   418
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
lemma conforms_xgext: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
  "\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s\<rbrakk> \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
apply (erule_tac conforms_xconf)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
apply (fast dest: conforms_XcptLocD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   424
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
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> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
\<Longrightarrow>  (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
apply (rule conforms_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
apply    auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
apply (force dest: conforms_globsD simp add: oconf_def)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some obj; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
  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)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
apply (rule conforms_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
apply (drule (1) conforms_globsD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
apply (simp add: oconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
apply (rule lconf_upd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
apply (simp only: obj_ty_cong) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
apply (force dest: conforms_globsD intro!: lconf_upd 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
       simp add: oconf_def cong del: sum.weak_case_cong)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
lemma conforms_set_locals: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
apply (auto intro!: conformsI dest: conforms_globsD 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
            elim!: conforms_XcptLocD simp add: oconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   453
lemma conforms_locals [rule_format]: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   454
  "(a,b)\<Colon>\<preceq>(G, L) \<longrightarrow> L x = Some T \<longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   455
apply (force simp: conforms_def Let_def lconf_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   456
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   457
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
lemma conforms_return: "\<And>s'. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); (x',s')\<Colon>\<preceq>(G, L'); s\<le>|s'\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
  (x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
apply (rule conforms_xconf)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
prefer 2 apply (force dest: conforms_XcptLocD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
apply (erule conforms_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
apply (force dest: conforms_globsD)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   466
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
end