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