src/HOL/Bali/WellType.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46714 a7ca72710dfe
child 48001 c79adcae9869
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/WellType.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
header {* Well-typedness of Java programs *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
33965
f57c11db4ad4 Inl and Inr now with authentic syntax
haftmann
parents: 32960
diff changeset
     6
theory WellType
f57c11db4ad4 Inl and Inr now with authentic syntax
haftmann
parents: 32960
diff changeset
     7
imports DeclConcepts
f57c11db4ad4 Inl and Inr now with authentic syntax
haftmann
parents: 32960
diff changeset
     8
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
improvements over Java Specification 1.0:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\item methods of Object can be called upon references of interface or array type
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
simplifications:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
\item the type rules include all static checks on statements and expressions, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
      e.g. definedness of names (of parameters, locals, fields, methods)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
\item unified type judgment for statements, variables, expressions, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
      expression lists
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
\item statements are typed like expressions with dummy type Void
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
\item the typing rules take an extra argument that is capable of determining 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
  the dynamic type of objects. Therefore, they can be used for both 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
  checking static types and determining runtime types in transition semantics.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
41778
5f79a9e42507 modernized specifications;
wenzelm
parents: 37956
diff changeset
    31
type_synonym lenv
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
    32
        = "(lname, ty) table"  --{* local variables, including This and Result*}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
record env = 
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: 13524
diff changeset
    35
         prg:: "prog"    --{* program *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
    36
         cls:: "qtname"  --{* current package and class name *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
    37
         lcl:: "lenv"    --{* local environment *}     
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
    40
  (type) "lenv" <= (type) "(lname, ty) table"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
    41
  (type) "lenv" <= (type) "lname \<Rightarrow> ty option"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
    42
  (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
    43
  (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
    46
abbreviation
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: 13524
diff changeset
    47
  pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
    48
  where "pkg e == pid (cls e)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
section "Static overloading: maximally specific methods "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
41778
5f79a9e42507 modernized specifications;
wenzelm
parents: 37956
diff changeset
    52
type_synonym
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
  emhead = "ref_ty \<times> mhead"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
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: 13524
diff changeset
    55
--{* Some mnemotic selectors for emhead *}
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    56
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    57
  "declrefT" :: "emhead \<Rightarrow> ref_ty"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    58
  where "declrefT = fst"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    60
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    61
  "mhd" :: "emhead \<Rightarrow> mhead"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    62
  where "mhd \<equiv> snd"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
lemma declrefT_simp[simp]:"declrefT (r,m) = r"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
by (simp add: declrefT_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
lemma mhd_simp[simp]:"mhd (r,m) = m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
by (simp add: mhd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
lemma static_mhd_simp[simp]: "static (mhd m) = is_static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
by (cases m) (simp add: member_is_static_simp mhd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
by (cases m) simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
by (cases m) simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
by (cases m) simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    82
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    83
  cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    84
  where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    85
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    86
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    87
  Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    88
  "Objectmheads G S =
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    89
    (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    90
      ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    91
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    92
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    93
  accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    94
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    95
  "accObjectmheads G S T =
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    96
    (if G\<turnstile>RefT T accessible_in (pid S)
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    97
     then Objectmheads G S
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    98
     else (\<lambda>sig. {}))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
    99
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   100
primrec mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   101
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   102
  "mheads G S  NullT     = (\<lambda>sig. {})"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   103
| "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   104
                           ` accimethds G (pid S) I sig \<union> 
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   105
                             accObjectmheads G S (IfaceT I) sig)"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   106
| "mheads G S (ClassT C) = cmheads G S C"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   107
| "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
37406
982f3e02f3c4 modernized specifications
haftmann
parents: 36367
diff changeset
   109
definition
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: 13524
diff changeset
   110
  --{* applicable methods, cf. 15.11.2.1 *}
46212
d86ef6b96097 tuned white space;
wenzelm
parents: 41778
diff changeset
   111
  appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   112
  "appl_methds G S rt = (\<lambda> sig. 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
      {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
37406
982f3e02f3c4 modernized specifications
haftmann
parents: 36367
diff changeset
   114
                           G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
37406
982f3e02f3c4 modernized specifications
haftmann
parents: 36367
diff changeset
   116
definition
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: 13524
diff changeset
   117
  --{* more specific methods, cf. 15.11.2.2 *}
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   118
  more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   119
  "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
37406
982f3e02f3c4 modernized specifications
haftmann
parents: 36367
diff changeset
   122
definition
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: 13524
diff changeset
   123
  --{* maximally specific methods, cf. 15.11.2.2 *}
46212
d86ef6b96097 tuned white space;
wenzelm
parents: 41778
diff changeset
   124
  max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   125
  "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   126
                          (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
lemma max_spec2appl_meths: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
  "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
by (auto simp: max_spec_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
   mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
by (auto simp: appl_methds_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
lemma max_spec2mheads: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
"max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
 \<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   144
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   145
  empty_dt :: "dyn_ty"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   146
  where "empty_dt = (\<lambda>a. None)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   148
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   149
  invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   150
  "invmode m e = (if is_static m 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   151
                  then Static 
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   152
                  else if e=Super then SuperM else IntVir)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
lemma invmode_nonstatic [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
  "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
apply (unfold invmode_def)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   157
apply (simp (no_asm) add: member_is_static_simp)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   158
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   159
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   160
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   161
lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   162
apply (unfold invmode_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   167
lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
apply (unfold invmode_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
lemma Null_staticD: 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   173
  "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
apply (clarsimp simp add: invmode_IntVir_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
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: 13524
diff changeset
   177
section "Typing for unary operations"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   178
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   179
primrec unop_type :: "unop \<Rightarrow> prim_ty"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   180
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   181
  "unop_type UPlus   = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   182
| "unop_type UMinus  = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   183
| "unop_type UBitNot = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   184
| "unop_type UNot    = Boolean"    
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   186
primrec wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   187
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   188
  "wt_unop UPlus   t = (t = PrimT Integer)"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   189
| "wt_unop UMinus  t = (t = PrimT Integer)"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   190
| "wt_unop UBitNot t = (t = PrimT Integer)"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   191
| "wt_unop UNot    t = (t = PrimT Boolean)"
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   192
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: 13524
diff changeset
   193
section "Typing for binary operations"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   194
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   195
primrec binop_type :: "binop \<Rightarrow> prim_ty"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   196
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   197
  "binop_type Mul      = Integer"     
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   198
| "binop_type Div      = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   199
| "binop_type Mod      = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   200
| "binop_type Plus     = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   201
| "binop_type Minus    = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   202
| "binop_type LShift   = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   203
| "binop_type RShift   = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   204
| "binop_type RShiftU  = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   205
| "binop_type Less     = Boolean"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   206
| "binop_type Le       = Boolean"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   207
| "binop_type Greater  = Boolean"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   208
| "binop_type Ge       = Boolean"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   209
| "binop_type Eq       = Boolean"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   210
| "binop_type Neq      = Boolean"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   211
| "binop_type BitAnd   = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   212
| "binop_type And      = Boolean"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   213
| "binop_type BitXor   = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   214
| "binop_type Xor      = Boolean"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   215
| "binop_type BitOr    = Integer"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   216
| "binop_type Or       = Boolean"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   217
| "binop_type CondAnd  = Boolean"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   218
| "binop_type CondOr   = Boolean"
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   219
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   220
primrec wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   221
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   222
  "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   223
| "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   224
| "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   225
| "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   226
| "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   227
| "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   228
| "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   229
| "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   230
| "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   231
| "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   232
| "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   233
| "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   234
| "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   235
| "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   236
| "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   237
| "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   238
| "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   239
| "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   240
| "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   241
| "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   242
| "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   243
| "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   244
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: 13524
diff changeset
   245
section "Typing for terms"
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   246
41778
5f79a9e42507 modernized specifications;
wenzelm
parents: 37956
diff changeset
   247
type_synonym tys  = "ty + ty list"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   249
  (type) "tys" <= (type) "ty + ty list"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   251
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   252
inductive wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37406
diff changeset
   253
  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51] 50)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   254
  and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   255
  and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   256
  and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   257
    ("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   258
where
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   259
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   260
  "E,dt\<Turnstile>s\<Colon>\<surd> \<equiv> E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   261
| "E,dt\<Turnstile>e\<Colon>-T \<equiv> E,dt\<Turnstile>In1l e\<Colon>Inl T"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   262
| "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2  e\<Colon>Inl T"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   263
| "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3  e\<Colon>Inr T"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   264
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   265
--{* well-typed statements *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   266
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   267
| Skip:                                 "E,dt\<Turnstile>Skip\<Colon>\<surd>"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   268
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   269
| Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   270
                                         E,dt\<Turnstile>Expr e\<Colon>\<surd>"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   271
  --{* cf. 14.6 *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   272
| Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   273
                                         E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   274
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   275
| Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   276
          E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   277
                                         E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   278
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   279
  --{* cf. 14.8 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   280
| If:   "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   281
          E,dt\<Turnstile>c1\<Colon>\<surd>;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   282
          E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   283
                                         E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   284
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   285
  --{* cf. 14.10 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   286
| Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   287
          E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   288
                                         E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   289
  --{* cf. 14.13, 14.15, 14.16 *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   290
| Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   292
  --{* cf. 14.16 *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   293
| Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   294
          prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   295
                                         E,dt\<Turnstile>Throw e\<Colon>\<surd>"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   296
  --{* cf. 14.18 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   297
| Try:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   298
          lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   299
          \<Longrightarrow>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   300
                                         E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   301
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   302
  --{* cf. 14.18 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   303
| Fin:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   304
                                         E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   305
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   306
| Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   307
                                         E,dt\<Turnstile>Init C\<Colon>\<surd>"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   308
  --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   309
     The class isn't necessarily accessible from the points @{term Init} 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   310
     is called. Therefor we only demand @{term is_class} and not 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   311
     @{term is_acc_class} here. 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   312
   *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   313
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   314
--{* well-typed expressions *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   315
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   316
  --{* cf. 15.8 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   317
| NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   318
                                         E,dt\<Turnstile>NewC C\<Colon>-Class C"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   319
  --{* cf. 15.9 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   320
| NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   321
          E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   322
                                         E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   323
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   324
  --{* cf. 15.15 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   325
| Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   326
          prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   327
                                         E,dt\<Turnstile>Cast T' e\<Colon>-T'"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   328
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   329
  --{* cf. 15.19.2 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   330
| Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   331
          prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   332
                                         E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   333
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   334
  --{* cf. 15.7.1 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   335
| Lit:  "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   336
                                         E,dt\<Turnstile>Lit x\<Colon>-T"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   338
| UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   339
          \<Longrightarrow>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   340
          E,dt\<Turnstile>UnOp unop e\<Colon>-T"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   341
  
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   342
| BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   343
           T=PrimT (binop_type binop)\<rbrakk> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   344
           \<Longrightarrow>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   345
           E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   346
  
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   347
  --{* cf. 15.10.2, 15.11.1 *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   348
| Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   349
          class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   350
                                         E,dt\<Turnstile>Super\<Colon>-Class (super c)"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   351
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   352
  --{* cf. 15.13.1, 15.10.1, 15.12 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   353
| Acc:  "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   354
                                         E,dt\<Turnstile>Acc va\<Colon>-T"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   355
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   356
  --{* cf. 15.25, 15.25.1 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   357
| Ass:  "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   358
          E,dt\<Turnstile>v \<Colon>-T';
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   359
          prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   360
                                         E,dt\<Turnstile>va:=v\<Colon>-T'"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   361
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   362
  --{* cf. 15.24 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   363
| Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   364
          E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   365
          prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   366
                                         E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   367
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   368
  --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   369
| Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   370
          E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   371
          max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   372
            = {((statDeclT,m),pTs')}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   373
         \<rbrakk> \<Longrightarrow>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   374
                   E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   376
| Methd: "\<lbrakk>is_class (prg E) C;
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   377
          methd (prg E) C sig = Some m;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   378
          E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   379
                                         E,dt\<Turnstile>Methd C sig\<Colon>-T"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   380
 --{* The class @{term C} is the dynamic class of the method call 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   381
    (cf. Eval.thy). 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   382
    It hasn't got to be directly accessible from the current package 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   383
    @{term "(pkg E)"}. 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   384
    Only the static class must be accessible (enshured indirectly by 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   385
    @{term Call}). 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   386
    Note that l is just a dummy value. It is only used in the smallstep 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   387
    semantics. To proof typesafety directly for the smallstep semantics 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   388
    we would have to assume conformance of l here!
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   389
  *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   390
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   391
| Body: "\<lbrakk>is_class (prg E) D;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   392
          E,dt\<Turnstile>blk\<Colon>\<surd>;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   393
          (lcl E) Result = Some T;
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   394
          is_type (prg E) T\<rbrakk> \<Longrightarrow>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   395
                                         E,dt\<Turnstile>Body D blk\<Colon>-T"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   396
--{* The class @{term D} implementing the method must not directly be 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   397
     accessible  from the current package @{term "(pkg E)"}, but can also 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   398
     be indirectly accessible due to inheritance (enshured in @{term Call})
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   399
    The result type hasn't got to be accessible in Java! (If it is not 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   400
    accessible you can only assign it to Object).
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   401
    For dummy value l see rule @{term Methd}. 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   402
   *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   403
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   404
--{* well-typed variables *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   405
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   406
  --{* cf. 15.13.1 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   407
| LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   408
                                         E,dt\<Turnstile>LVar vn\<Colon>=T"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   409
  --{* cf. 15.10.1 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   410
| FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   411
          accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   412
                         E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   413
  --{* cf. 15.12 *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   414
| AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   415
          E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   416
                                         E,dt\<Turnstile>e.[i]\<Colon>=T"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   417
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   418
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   419
--{* well-typed expression lists *}
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   420
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   421
  --{* cf. 15.11.??? *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   422
| Nil:                                  "E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   423
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   424
  --{* cf. 15.11.??? *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   425
| Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   426
          E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   427
                                         E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   428
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   430
(* for purely static typing *)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   431
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   432
  wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   433
  where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   434
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   435
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   436
  wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   437
  where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   438
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   439
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   440
  ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   441
  where "E|-e:-T == E|-In1l e :: Inl T"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   443
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   444
  ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   445
  where "E|-e:=T == E|-In2 e :: Inl T"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   447
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   448
  ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   449
  where "E|-e:#T == E|-In3 e :: Inr T"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   451
notation (xsymbols)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   452
  wt_syntax  ("_\<turnstile>_\<Colon>_"  [51,51,51] 50) and
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   453
  wt_stmt_syntax  ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50) and
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   454
  ty_expr_syntax  ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   455
  ty_var_syntax  ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 33965
diff changeset
   456
  ty_exprs_syntax  ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   457
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
declare not_None_eq [simp del] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
declare split_if [split del] split_if_asm [split del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
declare split_paired_All [simp del] split_paired_Ex [simp del]
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   461
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
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: 13524
diff changeset
   462
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   463
inductive_cases wt_elim_cases [cases set]:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   464
        "E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   465
        "E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   466
        "E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   467
        "E,dt\<Turnstile>In1l (NewC C)                \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   468
        "E,dt\<Turnstile>In1l (New T'[i])             \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   469
        "E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   470
        "E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   471
        "E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   472
        "E,dt\<Turnstile>In1l (UnOp unop e)           \<Colon>T"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   473
        "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     \<Colon>T"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   474
        "E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   475
        "E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   476
        "E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   477
        "E,dt\<Turnstile>In1l (e0 ? e1 : e2)          \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   478
        "E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   479
        "E,dt\<Turnstile>In1l (Methd C sig)           \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   480
        "E,dt\<Turnstile>In1l (Body D blk)            \<Colon>T"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   481
        "E,dt\<Turnstile>In3  ([])                    \<Colon>Ts"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   482
        "E,dt\<Turnstile>In3  (e#es)                  \<Colon>Ts"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   483
        "E,dt\<Turnstile>In1r  Skip                   \<Colon>x"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   484
        "E,dt\<Turnstile>In1r (Expr e)                \<Colon>x"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   485
        "E,dt\<Turnstile>In1r (c1;; c2)               \<Colon>x"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
        "E,dt\<Turnstile>In1r (l\<bullet> c)                  \<Colon>x" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   487
        "E,dt\<Turnstile>In1r (If(e) c1 Else c2)      \<Colon>x"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   488
        "E,dt\<Turnstile>In1r (l\<bullet> While(e) c)         \<Colon>x"
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: 13524
diff changeset
   489
        "E,dt\<Turnstile>In1r (Jmp jump)              \<Colon>x"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   490
        "E,dt\<Turnstile>In1r (Throw e)               \<Colon>x"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   491
        "E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   492
        "E,dt\<Turnstile>In1r (c1 Finally c2)         \<Colon>x"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   493
        "E,dt\<Turnstile>In1r (Init C)                \<Colon>x"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
declare not_None_eq [simp] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
declare split_if [split] split_if_asm [split]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
declare split_paired_All [simp] split_paired_Ex [simp]
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   497
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
lemma is_acc_class_is_accessible: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
  "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
by (auto simp add: is_acc_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
by (auto simp add: is_acc_iface_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13462
diff changeset
   506
lemma is_acc_iface_Iface_is_accessible: 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
  "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
by (auto simp add: is_acc_iface_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
by (auto simp add: is_acc_type_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13462
diff changeset
   513
lemma is_acc_iface_is_accessible:
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13462
diff changeset
   514
  "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
by (auto simp add: is_acc_type_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
lemma wt_Methd_is_methd: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
  "E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
apply (erule_tac wt_elim_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
apply (erule is_methdI, assumption)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
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: 13524
diff changeset
   524
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   525
text {* Special versions of some typing rules, better suited to pattern 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   526
        match the conclusion (no selectors in the conclusion)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   527
*}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
lemma wt_Call: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   532
    = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   533
 mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
by (auto elim: wt.Call)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
lemma invocationTypeExpr_noClassD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
"\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
 \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
  assume wt: "E\<turnstile>e\<Colon>-RefT statT"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
  proof (cases "e=Super")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
    case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
    with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
    then show ?thesis by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   547
  next 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
    case False then show ?thesis 
46714
a7ca72710dfe tuned proofs;
wenzelm
parents: 46212
diff changeset
   549
      by (auto simp add: invmode_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   551
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
lemma wt_Super: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
by (auto elim: wt.Super)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   558
lemma wt_FVar:  
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   559
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   560
  sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   561
\<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   562
by (auto dest: wt.FVar)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
by (auto elim: wt_elim_cases intro: "wt.Init")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
declare wt.Skip [iff]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
lemma wt_StatRef: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
  "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
apply (rule wt.Cast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
apply  (rule wt.Lit)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
apply   (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
apply  (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
apply (rule cast.widen)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
lemma wt_Inj_elim: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
  "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
                       In1 ec \<Rightarrow> (case ec of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
                                    Inl e \<Rightarrow> \<exists>T. U=Inl T  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
                                  | Inr s \<Rightarrow> U=Inl (PrimT Void))  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
                     | In2 e \<Rightarrow> (\<exists>T. U=Inl T) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
                     | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
apply (erule wt.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
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: 13524
diff changeset
   591
--{* In the special syntax to distinguish the typing judgements for expressions, 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   592
     statements, variables and expression lists the kind of term corresponds
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   593
     to the kind of type in the end e.g. An statement (injection @{term In3} 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   594
    into terms, always has type void (injection @{term Inl} into the generalised
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   595
    types. The following simplification procedures establish these kinds of
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   596
    correlation. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   597
 *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   598
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   599
lemma wt_expr_eq: "E,dt\<Turnstile>In1l t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T)"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   600
  by (auto, frule wt_Inj_elim, auto)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   601
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   602
lemma wt_var_eq: "E,dt\<Turnstile>In2 t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T)"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   603
  by (auto, frule wt_Inj_elim, auto)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   604
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   605
lemma wt_exprs_eq: "E,dt\<Turnstile>In3 t\<Colon>U = (\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts)"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   606
  by (auto, frule wt_Inj_elim, auto)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   607
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   608
lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   609
  by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   610
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   611
simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = {*
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   612
  fn _ => fn _ => fn ct =>
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   613
    (case Thm.term_of ct of
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   614
      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   615
    | _ => SOME (mk_meta_eq @{thm wt_expr_eq})) *}
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   616
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   617
simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = {*
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   618
  fn _ => fn _ => fn ct =>
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   619
    (case Thm.term_of ct of
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   620
      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   621
    | _ => SOME (mk_meta_eq @{thm wt_var_eq})) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   623
simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = {*
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   624
  fn _ => fn _ => fn ct =>
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   625
    (case Thm.term_of ct of
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   626
      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   627
    | _ => SOME (mk_meta_eq @{thm wt_exprs_eq})) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   629
simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = {*
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   630
  fn _ => fn _ => fn ct =>
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   631
    (case Thm.term_of ct of
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   632
      (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23747
diff changeset
   633
    | _ => SOME (mk_meta_eq @{thm wt_stmt_eq})) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
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: 13524
diff changeset
   635
lemma wt_elim_BinOp:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   636
  "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>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: 13524
diff changeset
   637
    \<And>T1 T2 T3.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   638
       \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   639
          E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   640
          T = Inl (PrimT (binop_type binop))\<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: 13524
diff changeset
   641
       \<Longrightarrow> P\<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: 13524
diff changeset
   642
\<Longrightarrow> P"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   643
apply (erule wt_elim_cases)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13524
diff changeset
   644
apply (cases 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: 13524
diff changeset
   645
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: 13524
diff changeset
   646
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: 13524
diff changeset
   647
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   648
lemma Inj_eq_lemma [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   649
  "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   651
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
lemma single_valued_tys_lemma [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
  "\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
     G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
apply (cases "E", erule wt.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
apply (safe del: disjE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
apply (simp_all (no_asm_use) split del: split_if_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
apply (safe del: disjE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
(* 17 subgoals *)
27208
5fe899199f85 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 24783
diff changeset
   661
apply (tactic {* ALLGOALS (fn i =>
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27208
diff changeset
   662
  if i = 11 then EVERY'
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27208
diff changeset
   663
   [thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27208
diff changeset
   664
    thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27208
diff changeset
   665
    thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27208
diff changeset
   666
  else thin_tac @{context} "All ?P" i) *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
(*apply (safe del: disjE elim!: wt_elim_cases)*)
27208
5fe899199f85 proper context for tactics derived from res_inst_tac;
wenzelm
parents: 24783
diff changeset
   668
apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
apply (simp_all (no_asm_use) split del: split_if_asm)
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   670
apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
apply ((blast del: equalityCE dest: sym [THEN trans])+)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   672
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   673
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   674
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   675
lemma single_valued_tys: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
"ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   677
apply (unfold single_valued_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   679
apply (rule single_valued_tys_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   680
apply (auto intro!: widen_antisym)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   681
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   682
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   683
lemma typeof_empty_is_type [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   684
  "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   685
apply (rule val.induct)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   686
apply           auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   687
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   688
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   689
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   690
lemma typeof_is_type [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   691
 "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
apply (rule val.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   693
prefer 5 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   694
apply     fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   695
apply  (simp_all (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   696
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   697
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   698
end