src/HOL/Bali/Conform.thy
author schirmer
Thu, 31 Oct 2002 18:27:10 +0100
changeset 13688 a0b16d42d489
parent 12925 99131847fb93
child 14025 d9b155757dc8
permissions -rw-r--r--
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
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
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   118
lemma conf_Boolean: "G,s\<turnstile>v\<Colon>\<preceq>PrimT Boolean \<Longrightarrow> \<exists> b. v=Bool b"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   119
by (cases v)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   120
   (auto simp: conf_def obj_ty_def 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   121
         dest: widen_Boolean2 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   122
        split: obj_tag.splits)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   123
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   124
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
lemma conf_litval [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
  "typeof (\<lambda>a. None) v = Some T \<longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
apply (rule val.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
lemma conf_Null [simp]: "G,s\<turnstile>Null\<Colon>\<preceq>T = G\<turnstile>NT\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
by (simp add: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
lemma conf_Addr: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
  "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
   137
by (auto simp: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
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
   140
apply (rule conf_Addr [THEN iffD2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
by fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
lemma defval_conf [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
  "is_type G T \<longrightarrow> G,s\<turnstile>default_val T\<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 (induct "T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
apply (auto intro: prim_ty.induct)
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_widen [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
  "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
   152
apply (unfold 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 (auto elim: ws_widen_trans)
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
lemma conf_gext [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
  "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
   159
apply (unfold gext_def conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
apply (rule val.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
apply force+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
lemma conf_list_widen [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
"ws_prog G \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
  \<forall>Ts Ts'. list_all2 (conf G s) vs Ts 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
           \<longrightarrow>   G\<turnstile>Ts[\<preceq>] Ts' \<longrightarrow> list_all2 (conf G s) vs Ts'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
apply (unfold widens_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
apply (rule list_all2_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
lemma conf_RefTD [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
 "G,s\<turnstile>a'\<Colon>\<preceq>RefT T 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
  \<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
   177
                    obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
apply (induct_tac "a'")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
apply (auto dest: widen_PrimT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
section "value list conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
  lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
                                                ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
           "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
   191
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
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
   193
by (force simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
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
   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_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
   200
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
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
   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_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
   207
  G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
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
   211
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
lemma lconf_map_sum [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
 "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
   215
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
apply (case_tac [3] "n")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
apply (force split add: sum.split)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
lemma lconf_ext_list [rule_format (no_asm)]: "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
 \<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
12893
cbb4dc5e6478 replaced nodups by distinct;
wenzelm
parents: 12858
diff changeset
   223
      \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
      \<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
   225
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
apply (induct_tac "vns")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
apply (frule list_all2_lengthD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
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
   235
apply (simp only: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
apply (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
apply (drule ospec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
done 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
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
   244
apply (simp only: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
lemma lconf_init_vals [intro!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
	" \<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
   255
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   259
section "weak value list conformance"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   260
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   261
text {* Only if the value is defined it has to conform to its type. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   262
        This is the contribution of the definite assignment analysis to 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   263
        the notion of conformance. The definite assignment analysis ensures
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   264
        that the program only attempts to access local variables that 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   265
        actually have a defined value in the state. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   266
        So conformance must only ensure that the
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   267
        defined values are of the right type, and not also that the value
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   268
        is defined. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   269
*}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   270
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   271
  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   272
constdefs
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   273
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   274
  wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   275
                                          ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   276
           "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   277
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   278
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"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   279
by (auto simp: wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   280
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   281
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   282
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"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   283
by (auto simp: wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   284
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   285
lemma wlconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<sim>\<Colon>\<preceq>]L = G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   286
by (auto simp: wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   287
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   288
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   289
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>  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   290
  G,s\<turnstile>l(vn\<mapsto>v)[\<sim>\<Colon>\<preceq>]L"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   291
by (auto simp: wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   292
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   293
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)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   294
by (auto simp: wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   295
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   296
lemma wlconf_map_sum [simp]: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   297
 "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)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   298
apply (unfold wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   299
apply safe
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   300
apply (case_tac [3] "n")
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   301
apply (force split add: sum.split)+
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   302
done
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   303
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   304
lemma wlconf_ext_list [rule_format (no_asm)]: "
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   305
 \<And>X. \<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   306
      \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   307
      \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<sim>\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   308
apply (unfold wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   309
apply (induct_tac "vns")
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   310
apply  clarsimp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   311
apply clarsimp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   312
apply (frule list_all2_lengthD)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   313
apply clarsimp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   314
done
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   315
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   316
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   317
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"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   318
apply (simp only: wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   319
apply safe
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   320
apply (drule spec)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   321
apply (drule ospec)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   322
defer
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   323
apply (drule ospec )
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   324
apply auto
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   325
done 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   326
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   327
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   328
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"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   329
apply (simp only: wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   330
apply fast
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   331
done
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   332
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   333
lemma wlconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]empty"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   334
apply (unfold wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   335
apply force
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   336
done
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   337
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   338
lemma wlconf_empty_vals: "G,s\<turnstile>empty[\<sim>\<Colon>\<preceq>]ts"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   339
  by (simp add: wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   340
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   341
lemma wlconf_init_vals [intro!]: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   342
	" \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<sim>\<Colon>\<preceq>]fs"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   343
apply (unfold wlconf_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   344
apply force
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   345
done
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   346
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   347
lemma lconf_wlconf:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   348
 "G,s\<turnstile>l[\<Colon>\<preceq>]L \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   349
by (force simp add: lconf_def wlconf_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
section "object conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
  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
   356
	   "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
   357
                           (case r of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
		              Heap a \<Rightarrow> is_type G (obj_ty obj) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
                            | Stat C \<Rightarrow> True)"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   360
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   361
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
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
   363
by (auto simp: oconf_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
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
   366
by (simp add: oconf_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
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
   369
by (auto simp: oconf_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
lemma oconf_init_obj_lemma: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
"\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (DeclConcepts.fields G C);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
  \<And>C c f fld. \<lbrakk>class G C = Some c; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
                table_of (DeclConcepts.fields G C) f = Some fld \<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
            \<Longrightarrow> is_type G (type fld);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
  (case r of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
     Heap a \<Rightarrow> is_type G (obj_ty obj) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
  | Stat C \<Rightarrow> is_class G C)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
\<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
   380
apply (auto simp add: oconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
apply (subst obj_ty_cong)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
apply(auto dest!: fields_table_SomeD obj_ty_CInst1 obj_ty_Arr1
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
           split add: sum.split_asm obj_tag.split_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
section "state conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
  conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
   "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   394
    (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   395
                \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   396
    (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   397
         (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
section "conforms"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
lemma conforms_globsD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
"\<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
   403
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   405
lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
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
   409
	  G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   412
lemma conforms_RetD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Jump Ret)\<rbrakk> \<Longrightarrow>  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   413
	  (locals s) Result \<noteq> None"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   414
by (auto simp: conforms_def Let_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   415
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
lemma conforms_RefTD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
 "\<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
   418
   \<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
   G\<turnstile>obj_ty obj\<preceq>RefT t \<and> is_type G (obj_ty obj)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
apply (drule_tac conf_RefTD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
apply (rule conforms_globsD [THEN oconf_is_type])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
apply auto
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_Jump [iff]:
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   427
  "j=Ret \<longrightarrow> locals s Result \<noteq> None 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   428
   \<Longrightarrow> ((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   429
by (auto simp: conforms_def Let_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
lemma conforms_StdXcpt [iff]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
  "((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
by (auto simp: conforms_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   435
lemma conforms_Err [iff]:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   436
   "((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
   437
  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
   438
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
lemma conforms_raise_if [iff]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
  "((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
by (auto simp: abrupt_if_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   443
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
   444
  "((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
   445
by (auto simp: abrupt_if_def split: split_if)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
lemma conforms_absorb [rule_format]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
  "(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
apply (rule impI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
apply ( case_tac a)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
apply (case_tac "absorb j a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
apply (case_tac "absorb j (Some a)",auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
apply (erule conforms_NormI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   461
     G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L;  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   462
     \<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   463
     x = Some (Jump Ret)\<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
  (x, s)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
lemma conforms_xconf: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L);   
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   468
 \<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   469
     x' = Some (Jump Ret) \<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
 (x',s)\<Colon>\<preceq>(G,L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
by (fast intro: conformsI elim: conforms_globsD conforms_localD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
lemma conforms_lupd: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
 "\<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)"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   475
by (force intro: conformsI wlconf_upd dest: conforms_globsD conforms_localD 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   476
                                           conforms_XcptLocD conforms_RetD 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   477
          simp: oconf_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   480
lemmas conforms_allocL_aux = conforms_localD [THEN wlconf_ext]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
lemma conforms_allocL: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
  "\<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))"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   484
by (force intro: conformsI dest: conforms_globsD conforms_RetD 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   485
          elim: conforms_XcptLocD  conforms_allocL_aux 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   486
          simp: oconf_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   488
lemmas conforms_deallocL_aux = conforms_localD [THEN wlconf_deallocL]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
lemma conforms_deallocL: "\<And>s.\<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   491
by (fast intro: conformsI dest: conforms_globsD conforms_RetD
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
         elim: conforms_XcptLocD conforms_deallocL_aux)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s';  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
  \<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
   locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)"
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   497
apply (rule conformsI)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   498
apply     assumption
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   499
apply    (drule conforms_localD) apply force
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   500
apply   (intro strip)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   501
apply  (drule (1) conforms_XcptLocD) apply force 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   502
apply (intro strip)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   503
apply (drule (1) conforms_RetD) apply force
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   504
done
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   505
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
lemma conforms_xgext: 
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   509
  "\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s;dom (locals s') \<subseteq> dom (locals s)\<rbrakk> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   510
   \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
apply (erule_tac conforms_xconf)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   512
apply  (fast dest: conforms_XcptLocD)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   513
apply (intro strip)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   514
apply (drule (1) conforms_RetD) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   515
apply (auto dest: domI)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
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
   519
\<Longrightarrow>  (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
apply (rule conforms_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
apply    auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
apply (force dest: conforms_globsD simp add: oconf_def)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some obj; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
  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
   527
apply (rule conforms_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
apply (drule (1) conforms_globsD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
apply (simp add: oconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
apply (rule lconf_upd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
apply (simp only: obj_ty_cong) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
apply (force dest: conforms_globsD intro!: lconf_upd 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
       simp add: oconf_def cong del: sum.weak_case_cong)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
lemma conforms_set_locals: 
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   540
  "\<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> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   541
   \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   542
apply (rule conformsI)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   543
apply     (intro strip)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   544
apply     simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   545
apply     (drule (2) conforms_globsD)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   546
apply    simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   547
apply   (intro strip)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   548
apply   (drule (1) conforms_XcptLocD)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   549
apply   simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   550
apply (intro strip)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   551
apply (drule (1) conforms_RetD)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   552
apply simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   555
lemma conforms_locals: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   556
  "\<lbrakk>(a,b)\<Colon>\<preceq>(G, L); L x = Some T;locals b x \<noteq>None\<rbrakk>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   557
   \<Longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   558
apply (force simp: conforms_def Let_def wlconf_def)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   559
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   560
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   561
lemma conforms_return: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12925
diff changeset
   562
"\<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>  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
  (x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
apply (rule conforms_xconf)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
prefer 2 apply (force dest: conforms_XcptLocD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
apply (erule conforms_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
apply (force dest: conforms_globsD)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   570
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
end