src/HOL/Bali/Conform.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46222 cb3f370e66e1
child 55417 01fbfb60c33e
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
header {* Conformance notions for the type soundness proof for Java *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     7
theory Conform imports State begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
\item lconf allows for (arbitrary) inaccessible values
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\item ''conforms'' does not directly imply that the dynamic types of all 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
      objects on the heap are indeed existing classes. Yet this can be 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
      inferred for all referenced objs.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
41778
5f79a9e42507 modernized specifications;
wenzelm
parents: 37956
diff changeset
    19
type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
section "extension of global store"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    24
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35069
diff changeset
    25
definition gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_"       [71,71]   70) where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
   "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
    27
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    28
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
    29
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
    30
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
    31
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
    32
accessible objects.
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    33
*}
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    34
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
lemma gext_objD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
"\<lbrakk>s\<le>|s'; globs s r = Some obj\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
\<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
apply (simp only: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
by force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
lemma rev_gext_objD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
"\<lbrakk>globs s r = Some obj; s\<le>|s'\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
 \<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
by (auto elim: gext_objD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
lemma init_class_obj_inited: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
   "init_class_obj G C s1\<le>|s2 \<Longrightarrow> inited C (globs s2)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
apply (unfold inited_def init_obj_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
apply (auto dest!: gext_objD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
lemma gext_refl [intro!, simp]: "s\<le>|s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
apply (unfold gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
apply (fast del: fst_splitE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
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
    58
by (auto simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
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
    61
apply (simp only: init_obj_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
apply (erule_tac gext_gupd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
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
    66
by (force simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
lemma gext_upd_gobj [intro!]: "s\<le>|upd_gobj r n v s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
apply (simp only: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
apply (case_tac "ra = r")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
apply (case_tac "globs s r = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
lemma gext_cong1 [simp]: "set_locals l s1\<le>|s2 = s1\<le>|s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
by (auto simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
lemma gext_cong2 [simp]: "s1\<le>|set_locals l s2 = s1\<le>|s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
by (auto simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
lemma gext_lupd1 [simp]: "lupd(vn\<mapsto>v)s1\<le>|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
lemma gext_lupd2 [simp]: "s1\<le>|lupd(vn\<mapsto>v)s2 = s1\<le>|s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
by (auto simp: gext_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
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
    92
apply (unfold inited_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
apply (auto dest: gext_objD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
section "value conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
    99
definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   100
  where "G,s\<turnstile>v\<Colon>\<preceq>T = (\<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
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
   103
by (auto simp: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
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
   106
by (auto simp: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
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
   109
apply (simp add: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
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
   112
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
   113
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
   114
   (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
   115
         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
   116
        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
   117
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
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
lemma conf_litval [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
  "typeof (\<lambda>a. None) v = Some T \<longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
apply (rule val.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
lemma conf_Null [simp]: "G,s\<turnstile>Null\<Colon>\<preceq>T = G\<turnstile>NT\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
by (simp add: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
lemma conf_Addr: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
  "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
   131
by (auto simp: conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
lemma conf_AddrI:"\<lbrakk>heap s a = Some obj; G\<turnstile>obj_ty obj\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
apply (rule conf_Addr [THEN iffD2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
by fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
lemma defval_conf [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
  "is_type G T \<longrightarrow> G,s\<turnstile>default_val T\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
apply (induct "T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
apply (auto intro: prim_ty.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
lemma conf_widen [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
  "G\<turnstile>T\<preceq>T' \<Longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T \<longrightarrow> ws_prog G \<longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
apply (rule val.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
apply (auto elim: ws_widen_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
lemma conf_gext [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
  "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
   153
apply (unfold gext_def conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
apply (rule val.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
apply force+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
lemma conf_list_widen [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
"ws_prog G \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
  \<forall>Ts Ts'. list_all2 (conf G s) vs Ts 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
           \<longrightarrow>   G\<turnstile>Ts[\<preceq>] Ts' \<longrightarrow> list_all2 (conf G s) vs Ts'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
apply (unfold widens_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
apply (rule list_all2_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
lemma conf_RefTD [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
 "G,s\<turnstile>a'\<Colon>\<preceq>RefT T 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
  \<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
   171
                    obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
apply (induct_tac "a'")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
apply (auto dest: widen_PrimT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
section "value list conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   180
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   181
  lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   182
  where "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
lemma lconfD: "\<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
by (force simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
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
   189
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
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
   192
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
lemma lconf_new: "\<lbrakk>L vn = None; G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
lemma lconf_upd: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
  G,s\<turnstile>l(vn\<mapsto>v)[\<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
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
   203
by (auto simp: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
lemma lconf_map_sum [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
 "G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<Colon>\<preceq>]L2)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
apply (case_tac [3] "n")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
apply (force split add: sum.split)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
lemma lconf_ext_list [rule_format (no_asm)]: "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
 \<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
12893
cbb4dc5e6478 replaced nodups by distinct;
wenzelm
parents: 12858
diff changeset
   215
      \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
      \<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
   217
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
apply (induct_tac "vns")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
apply  clarsimp
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13688
diff changeset
   220
apply clarify
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
apply (frule list_all2_lengthD)
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13688
diff changeset
   222
apply (clarsimp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
lemma lconf_deallocL: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<Colon>\<preceq>]L"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
apply (simp only: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
apply (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
apply (drule ospec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
done 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
lemma lconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<Colon>\<preceq>]L"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
apply (simp only: lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
lemma lconf_init_vals [intro!]: 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   246
        " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
apply (unfold lconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
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
   251
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
   252
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
   253
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
   254
        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
   255
        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
   256
        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
   257
        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
   258
        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
   259
        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
   260
        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
   261
*}
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
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
  
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   264
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   265
  wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   266
  where "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
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
   267
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
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
   269
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
   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
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
   273
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
   274
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
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
   276
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
   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
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
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
   280
  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
   281
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
   282
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
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
   284
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
   285
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
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
   287
 "G,s\<turnstile>l1 (+) l2[\<sim>\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<sim>\<Colon>\<preceq>]L2)"
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
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
   289
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
   290
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
   291
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
   292
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
   293
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
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
   295
 \<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
   296
      \<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
   297
      \<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
   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 (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
   300
apply  clarsimp
14025
d9b155757dc8 *** empty log message ***
nipkow
parents: 13688
diff changeset
   301
apply clarify
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
   302
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
   303
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
   304
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
   305
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
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
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
   308
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
   309
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
   310
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
   311
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
   312
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
   313
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
   314
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
   315
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
   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
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
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
   319
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
   320
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
   321
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
   322
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
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
   324
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
   325
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
   326
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
   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_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
   329
  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
   330
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
lemma wlconf_init_vals [intro!]: 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   332
        " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<sim>\<Colon>\<preceq>]fs"
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
   333
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
   334
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
   335
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
   336
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
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
   338
 "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
   339
by (force simp add: lconf_def wlconf_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
section "object conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   343
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   344
  oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   345
  "(G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r) = (G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
                           (case r of 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   347
                              Heap a \<Rightarrow> is_type G (obj_ty obj) 
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   348
                            | 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
   349
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
   350
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
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
   352
by (auto simp: oconf_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
lemma oconf_lconf: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<Longrightarrow> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
by (simp add: oconf_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
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
   358
by (auto simp: oconf_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
lemma oconf_init_obj_lemma: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
"\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (DeclConcepts.fields G C);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
  \<And>C c f fld. \<lbrakk>class G C = Some c; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
                table_of (DeclConcepts.fields G C) f = Some fld \<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
            \<Longrightarrow> is_type G (type fld);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
  (case r of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
     Heap a \<Rightarrow> is_type G (obj_ty obj) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
  | Stat C \<Rightarrow> is_class G C)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
\<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
   369
apply (auto simp add: oconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
apply (subst obj_ty_cong)
46222
cb3f370e66e1 tuned proofs;
wenzelm
parents: 46212
diff changeset
   373
apply (auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
section "state conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   378
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   379
  conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"  ("_\<Colon>\<preceq>_" [71,71] 70)  where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   380
   "xs\<Colon>\<preceq>E =
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   381
      (let (G, L) = E; s = snd xs; l = locals s in
46212
d86ef6b96097 tuned white space;
wenzelm
parents: 41778
diff changeset
   382
        (\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and> G,s\<turnstile>l [\<sim>\<Colon>\<preceq>]L \<and>
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   383
        (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   384
             (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
section "conforms"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
lemma conforms_globsD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
"\<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
   390
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
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
   392
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
   393
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow>  
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   396
          G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
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
   399
lemma conforms_RetD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Jump Ret)\<rbrakk> \<Longrightarrow>  
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   400
          (locals s) Result \<noteq> None"
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
   401
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
   402
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
lemma conforms_RefTD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
 "\<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
   405
   \<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
   G\<turnstile>obj_ty obj\<preceq>RefT t \<and> is_type G (obj_ty obj)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
apply (drule_tac conf_RefTD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
apply (rule conforms_globsD [THEN oconf_is_type])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   412
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   413
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
   414
  "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
   415
   \<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
   416
by (auto simp: conforms_def Let_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   418
lemma conforms_StdXcpt [iff]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
  "((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
by (auto simp: conforms_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   422
lemma conforms_Err [iff]:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   423
   "((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
   424
  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
   425
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
lemma conforms_raise_if [iff]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
  "((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
by (auto simp: abrupt_if_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   430
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
   431
  "((error_if c err x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
46222
cb3f370e66e1 tuned proofs;
wenzelm
parents: 46212
diff changeset
   432
by (auto simp: abrupt_if_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
lemma conforms_absorb [rule_format]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
  "(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
apply (rule impI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
apply ( case_tac a)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
apply (case_tac "absorb j a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
apply (case_tac "absorb j (Some a)",auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
apply (erule conforms_NormI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
lemma 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
   448
     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
   449
     \<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
   450
     x = Some (Jump Ret)\<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
  (x, s)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
by (auto simp: conforms_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
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
   455
 \<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
   456
     x' = Some (Jump Ret) \<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
 (x',s)\<Colon>\<preceq>(G,L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
by (fast intro: conformsI elim: conforms_globsD conforms_localD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
lemma conforms_lupd: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
 "\<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
   462
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
   463
                                           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
   464
          simp: oconf_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
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
   467
lemmas conforms_allocL_aux = conforms_localD [THEN wlconf_ext]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
lemma conforms_allocL: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
  "\<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
   471
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
   472
          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
   473
          simp: oconf_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
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
lemmas conforms_deallocL_aux = conforms_localD [THEN wlconf_deallocL]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
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
   478
by (fast intro: conformsI dest: conforms_globsD conforms_RetD
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
         elim: conforms_XcptLocD conforms_deallocL_aux)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s';  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
  \<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
   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
   484
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
   485
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
   486
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
   487
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
   488
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
   489
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
   490
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
   491
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
   492
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
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
   496
  "\<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
   497
   \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
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
   499
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
   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_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
   502
apply (auto dest: domI)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
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
   506
\<Longrightarrow>  (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
apply (rule conforms_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
apply    auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
apply (force dest: conforms_globsD simp add: oconf_def)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some obj; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
  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
   514
apply (rule conforms_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
apply (drule (1) conforms_globsD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
apply (simp add: oconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
apply (rule lconf_upd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
apply (simp only: obj_ty_cong) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
apply (force dest: conforms_globsD intro!: lconf_upd 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
       simp add: oconf_def cong del: sum.weak_case_cong)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
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
   527
  "\<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
   528
   \<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
   529
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
   530
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
   531
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
   532
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
   533
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
   534
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
   535
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
   536
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
   537
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
   538
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
   539
apply simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
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
   542
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
   543
  "\<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
   544
   \<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
   545
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
   546
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   547
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
   548
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
   549
"\<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
   550
  (x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   551
apply (rule conforms_xconf)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
prefer 2 apply (force dest: conforms_XcptLocD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
apply (erule conforms_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
apply (force dest: conforms_globsD)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
   557
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
end