src/HOL/Bali/Example.thy
author wenzelm
Tue, 27 Aug 2002 11:03:05 +0200
changeset 13524 604d0f3622d6
parent 12925 99131847fb93
child 13688 a0b16d42d489
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Example.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
12858
wenzelm
parents: 12857
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Example Bali program *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
theory Example = Eval + WellForm:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
The following example Bali program includes:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\item class and interface declarations with inheritance, hiding of fields,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
    overriding of methods (with refined result type), array type,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
\item method call (with dynamic binding), parameter access, return expressions,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
\item expression statements, sequential composition, literal values, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
    local assignment, local access, field assignment, type cast,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
\item exception generation and propagation, try and catch statement, throw 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
      statement
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
\item instance creation and (default) static initialization
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
\begin{verbatim}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
package java_lang
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
public interface HasFoo {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
  public Base foo(Base z);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
public class Base implements HasFoo {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
  static boolean arr[] = new boolean[2];
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
  public HasFoo vee;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
  public Base foo(Base z) {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
    return z;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
  }
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
public class Ext extends Base {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
  public int vee;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
  public Ext foo(Base z) {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
    ((Ext)z).vee = 1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
    return null;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
  }
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    45
public class Main {
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
  public static void main(String args[]) throws Throwable {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
    Base e = new Ext();
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
    try {e.foo(null); }
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
    catch(NullPointerException z) { 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
      while(Ext.arr[2]) ;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
    }
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
  }
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
\end{verbatim}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
declare widen.null [intro]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
apply (unfold wf_fdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
declare wf_fdecl_def2 [iff]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
section "type and expression names"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
(** unfortunately cannot simply instantiate tnam **)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    69
datatype tnam_  = HasFoo_ | Base_ | Ext_ | Main_
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
datatype vnam_  = arr_ | vee_ | z_ | e_
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
datatype label_ = lab1_
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
  tnam_ :: "tnam_  \<Rightarrow> tnam"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
  vnam_ :: "vnam_  \<Rightarrow> vname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
  label_:: "label_ \<Rightarrow> label"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
axioms  (** tnam_, vnam_ and label are intended to be isomorphic 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
            to tnam, vname and label **)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
  inj_tnam_  [simp]: "(tnam_  x = tnam_  y) = (x = y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
  inj_vnam_  [simp]: "(vnam_  x = vnam_  y) = (x = y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
  inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
  surj_tnam_:  "\<exists>m. n = tnam_  m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
  surj_vnam_:  "\<exists>m. n = vnam_  m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
  surj_label_:" \<exists>m. n = label_ m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
  HasFoo :: qtname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
  Base   :: qtname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
  Ext    :: qtname
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    95
  Main   :: qtname
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
  arr :: ename
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
  vee :: ename
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
  z   :: ename
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
  e   :: ename
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
  lab1:: label
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
  "HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
  "Base"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
  "Ext"    == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   106
  "Main"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Main_)\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
  "arr"    ==        "(vnam_ arr_)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
  "vee"    ==        "(vnam_ vee_)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
  "z"      ==        "(vnam_ z_)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
  "e"      ==        "(vnam_ e_)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
  "lab1"   ==        "label_ lab1_"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
lemma neq_Base_Object [simp]: "Base\<noteq>Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
by (simp add: Object_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
lemma neq_Ext_Object [simp]: "Ext\<noteq>Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
by (simp add: Object_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   120
lemma neq_Main_Object [simp]: "Main\<noteq>Object"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   121
by (simp add: Object_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   122
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
lemma neq_Base_SXcpt [simp]: "Base\<noteq>SXcpt xn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
by (simp add: SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
by (simp add: SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 12925
diff changeset
   129
lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   130
by (simp add: SXcpt_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   131
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
section "classes and interfaces"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
defs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
  Object_mdecls_def: "Object_mdecls \<equiv> []"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
  SXcpt_mdecls_def:  "SXcpt_mdecls  \<equiv> []"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
  foo    :: mname
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
  foo_sig   :: sig
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
 "foo_sig   \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
  foo_mhead :: mhead
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
 "foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
  Base_foo :: mdecl
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
 "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
                        mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
12925
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
constdefs
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
  Ext_foo  :: mdecl
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
 "Ext_foo  \<equiv> (foo_sig, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
              \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
	       mbody=\<lparr>lcls=[]
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   162
                     ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
       	                                                     Lit (Intg 1))\<rparr>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
	      \<rparr>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
  
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   168
arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   169
"arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
BaseCl :: class
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
"BaseCl \<equiv> \<lparr>access=Public,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
           cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
	            (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
           methods=[Base_foo],
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   176
           init=Expr(arr_viewed_from Base Base 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   177
                     :=New (PrimT Boolean)[Lit (Intg 2)]),
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
           super=Object,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
           superIfs=[HasFoo]\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
ExtCl  :: class
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
"ExtCl  \<equiv> \<lparr>access=Public,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
           cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
           methods=[Ext_foo],
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
           init=Skip,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
           super=Base,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
           superIfs=[]\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   189
MainCl :: class
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   190
"MainCl \<equiv> \<lparr>access=Public,
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   191
           cfields=[], 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   192
           methods=[], 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   193
           init=Skip,
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   194
           super=Object,
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   195
           superIfs=[]\<rparr>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   196
(* The "main" method is modeled seperately (see tprg) *)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   197
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
  HasFooInt :: iface
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
 "HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
  Ifaces ::"idecl list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
 "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
 "Classes" ::"cdecl list"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   207
 "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
lemmas table_classes_defs = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
     Classes_def standard_classes_def ObjectC_def SXcptC_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
lemma table_ifaces [simp]: "table_of Ifaces = empty(HasFoo\<mapsto>HasFooInt)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
apply (unfold Ifaces_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
lemma table_classes_Object [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
 "table_of Classes Object = Some \<lparr>access=Public,cfields=[]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
                                 ,methods=Object_mdecls
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
                                 ,init=Skip,super=arbitrary,superIfs=[]\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
apply (unfold table_classes_defs)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
apply (simp (no_asm) add:Object_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
lemma table_classes_SXcpt [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
  "table_of Classes (SXcpt xn) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
    = Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
            init=Skip,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
            super=if xn = Throwable then Object else SXcpt Throwable,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
            superIfs=[]\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
apply (unfold table_classes_defs)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
apply (induct_tac xn)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
apply (simp add: Object_def SXcpt_def)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
lemma table_classes_HasFoo [simp]: "table_of Classes HasFoo = None"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
apply (unfold table_classes_defs)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
apply (simp (no_asm) add: Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
lemma table_classes_Base [simp]: "table_of Classes Base = Some BaseCl"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
apply (unfold table_classes_defs )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
apply (simp (no_asm) add: Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
lemma table_classes_Ext [simp]: "table_of Classes Ext = Some ExtCl"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
apply (unfold table_classes_defs )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
apply (simp (no_asm) add: Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   251
lemma table_classes_Main [simp]: "table_of Classes Main = Some MainCl"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   252
apply (unfold table_classes_defs )
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   253
apply (simp (no_asm) add: Object_def SXcpt_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   254
done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
section "program"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
  tprg :: prog
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
  "tprg" == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
  test    :: "(ty)list \<Rightarrow> stmt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
 "test pTs \<equiv> e:==NewC Ext;; 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   267
           \<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
           \<spacespace> Catch((SXcpt NullPointer) z)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   269
           (lab1\<bullet> While(Acc 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   270
                        (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
section "well-structuredness"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
apply (auto dest!: tranclD subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
lemma not_Throwable_subcls_SXcpt [elim!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
  "(SXcpt Throwable, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
apply (auto dest!: tranclD subcls1D) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
apply (simp add: Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
lemma not_SXcpt_n_subcls_SXcpt_n [elim!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
  "(SXcpt xn, SXcpt xn)  \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
apply (auto dest!: tranclD subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
apply (drule rtranclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+  \<Longrightarrow> R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
  "(\<lparr>pid=java_lang,tid=TName tn\<rparr>, \<lparr>pid=java_lang,tid=TName tn\<rparr>) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
   \<in> (subcls1 tprg)^+ \<longrightarrow> R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
apply (rule_tac n1 = "tn" in surj_tnam_ [THEN exE])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
apply (erule ssubst)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
apply (rule tnam_.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
apply  safe
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   303
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def MainCl_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
apply (drule rtranclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
apply (unfold ws_idecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
lemma ws_cdecl_Object: "ws_cdecl tprg Object any"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
apply (unfold ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
lemma ws_cdecl_Throwable: "ws_cdecl tprg (SXcpt Throwable) Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
apply (unfold ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
lemma ws_cdecl_SXcpt: "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
apply (unfold ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
lemma ws_cdecl_Base: "ws_cdecl tprg Base Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
apply (unfold ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
apply (unfold ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   339
lemma ws_cdecl_Main: "ws_cdecl tprg Main Object"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   340
apply (unfold ws_cdecl_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   341
apply auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   342
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   343
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   345
                   ws_cdecl_Base ws_cdecl_Ext ws_cdecl_Main
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
declare not_Object_subcls_any [rule del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
          not_Throwable_subcls_SXcpt [rule del] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
          not_SXcpt_n_subcls_SXcpt_n [rule del] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
          not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
lemma ws_idecl_all: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
 "G=tprg \<Longrightarrow> (\<forall>(I,i)\<in>set Ifaces. ws_idecl G I (isuperIfs i))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
apply (simp (no_asm) add: Ifaces_def HasFooInt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
apply (auto intro!: ws_idecl_HasFoo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
lemma ws_cdecl_all: "G=tprg \<Longrightarrow> (\<forall>(C,c)\<in>set Classes. ws_cdecl G C (super c))"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   359
apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def MainCl_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
        SXcptC_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
lemma ws_tprg: "ws_prog tprg"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
apply (unfold ws_prog_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
apply (auto intro!: ws_idecl_all ws_cdecl_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
section "misc program properties (independent of well-structuredness)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
apply (unfold Ifaces_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
lemma empty_subint1 [simp]: "subint1 tprg = {}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
apply (unfold subint1_def Ifaces_def HasFooInt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
lemma unique_ifaces: "unique Ifaces"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
apply (unfold Ifaces_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
lemma unique_classes: "unique Classes"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
apply (unfold table_classes_defs )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
apply (simp )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
lemma SXcpt_subcls_Throwable [simp]: "tprg\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
apply (rule SXcpt_subcls_Throwable_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
lemma Ext_subclseq_Base [simp]: "tprg\<turnstile>Ext \<preceq>\<^sub>C Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
apply (rule subcls_direct1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
apply  (simp (no_asm) add: ExtCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
apply  (simp add: Object_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext \<prec>\<^sub>C Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
apply (rule subcls_direct2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
apply  (simp (no_asm) add: ExtCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
apply  (simp add: Object_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   412
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   413
section "fields and method lookup"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   414
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   415
lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
by (rule ws_tprg [THEN fields_emptyI], force+)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   418
lemma fields_tprg_Throwable [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
  "DeclConcepts.fields tprg (SXcpt Throwable) = []"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
by (rule ws_tprg [THEN fields_emptyI], force+)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
lemma fields_tprg_SXcpt [simp]: "DeclConcepts.fields tprg (SXcpt xn) = []"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
apply (case_tac "xn = Throwable")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   424
apply  (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
by (rule ws_tprg [THEN fields_emptyI], force+)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
lemmas fields_rec_ = fields_rec [OF _ ws_tprg]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
lemma fields_Base [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
"DeclConcepts.fields tprg Base 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
  = [((arr,Base), \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
     ((vee,Base), \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
apply (subst fields_rec_)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
apply   (auto simp add: BaseCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
lemma fields_Ext [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
 "DeclConcepts.fields tprg Ext  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
  = [((vee,Ext), \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
    @ DeclConcepts.fields tprg Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
apply (rule trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
apply (rule fields_rec_)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
apply   (auto simp add: ExtCl_def Object_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
lemmas imethds_rec_ = imethds_rec [OF _ ws_tprg]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
lemmas methd_rec_  = methd_rec  [OF _ ws_tprg]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
lemma imethds_HasFoo [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
  "imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
apply (rule trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
apply (rule imethds_rec_)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
apply  (auto simp add: HasFooInt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
lemma methd_tprg_Object [simp]: "methd tprg Object = empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
apply (subst methd_rec_)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
apply (auto simp add: Object_mdecls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
lemma methd_Base [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
  "methd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
apply (rule trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
apply (rule methd_rec_)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
apply   (auto simp add: BaseCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
lemma memberid_Base_foo_simp [simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
 "memberid (mdecl Base_foo) = mid foo_sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
by (simp add: Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
lemma memberid_Ext_foo_simp [simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
 "memberid (mdecl Ext_foo) = mid foo_sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
by (simp add: Ext_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
lemma Base_declares_foo:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
  "tprg\<turnstile>mdecl Base_foo declared_in Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
by (auto simp add: declared_in_def cdeclaredmethd_def BaseCl_def Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
lemma foo_sig_not_undeclared_in_Base:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
  "\<not> tprg\<turnstile>mid foo_sig undeclared_in Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
  from Base_declares_foo
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
    by (auto dest!: declared_not_undeclared )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
lemma Ext_declares_foo:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
  "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
by (auto simp add: declared_in_def cdeclaredmethd_def ExtCl_def Ext_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
lemma foo_sig_not_undeclared_in_Ext:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
  "\<not> tprg\<turnstile>mid foo_sig undeclared_in Ext"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
  from Ext_declares_foo
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
    by (auto dest!: declared_not_undeclared )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
lemma Base_foo_not_inherited_in_Ext:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
 "\<not> tprg \<turnstile> Ext inherits (Base,mdecl Base_foo)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
by (auto simp add: inherits_def foo_sig_not_undeclared_in_Ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
lemma Ext_method_inheritance:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
 "filter_tab (\<lambda>sig m. tprg \<turnstile> Ext inherits method sig m)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
     (empty(fst ((\<lambda>(s, m). (s, Base, m)) Base_foo)\<mapsto>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
      snd ((\<lambda>(s, m). (s, Base, m)) Base_foo)))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
  = empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
  from Base_foo_not_inherited_in_Ext
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
    by (auto intro: filter_tab_all_False simp add: Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
lemma methd_Ext [simp]: "methd tprg Ext =   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
  table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
apply (rule trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
apply (rule methd_rec_)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
apply   (auto simp add: ExtCl_def Object_def Ext_method_inheritance)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
section "accessibility"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
lemma classesDefined: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
 "\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   527
apply (auto simp add: Classes_def standard_classes_def 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   528
                      BaseCl_def ExtCl_def MainCl_def
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
                      SXcptC_def ObjectC_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
lemma superclassesBase [simp]: "superclasses tprg Base={Object}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
  have ws: "ws_prog tprg" by (rule ws_tprg)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
  then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
    by (auto simp add: superclasses_rec  BaseCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
lemma superclassesExt [simp]: "superclasses tprg Ext={Base,Object}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
  have ws: "ws_prog tprg" by (rule ws_tprg)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
  then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
    by (auto simp add: superclasses_rec  ExtCl_def BaseCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   546
lemma superclassesMain [simp]: "superclasses tprg Main={Object}"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   547
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   548
  have ws: "ws_prog tprg" by (rule ws_tprg)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   549
  then show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   550
    by (auto simp add: superclasses_rec  MainCl_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   551
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   552
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
lemma HasFoo_accessible[simp]:"tprg\<turnstile>(Iface HasFoo) accessible_in P" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
by (simp add: accessible_in_RefT_simp is_public_def HasFooInt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
lemma HasFoo_is_acc_iface[simp]: "is_acc_iface tprg P HasFoo"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
by (simp add: is_acc_iface_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
lemma HasFoo_is_acc_type[simp]: "is_acc_type tprg P (Iface HasFoo)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
by (simp add: is_acc_type_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
lemma Base_accessible[simp]:"tprg\<turnstile>(Class Base) accessible_in P" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
by (simp add: accessible_in_RefT_simp is_public_def BaseCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
lemma Base_is_acc_class[simp]: "is_acc_class tprg P Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
by (simp add: is_acc_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
lemma Base_is_acc_type[simp]: "is_acc_type tprg P (Class Base)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
by (simp add: is_acc_type_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
lemma Ext_accessible[simp]:"tprg\<turnstile>(Class Ext) accessible_in P" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
by (simp add: accessible_in_RefT_simp is_public_def ExtCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
lemma Ext_is_acc_class[simp]: "is_acc_class tprg P Ext"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
by (simp add: is_acc_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
lemma Ext_is_acc_type[simp]: "is_acc_type tprg P (Class Ext)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
by (simp add: is_acc_type_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
apply (unfold accmethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
apply (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
lemma  snd_special_simp: "snd ((\<lambda>(s, m). (s, a, m)) x) = (a,snd x)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
by (cases x) (auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
lemma  fst_special_simp: "fst ((\<lambda>(s, m). (s, a, m)) x) = fst x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
by (cases x) (auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
lemma foo_sig_undeclared_in_Object:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
  "tprg\<turnstile>mid foo_sig undeclared_in Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   594
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
lemma unique_sig_Base_foo:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   596
 "tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base \<Longrightarrow> sig=foo_sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
by (auto simp add: declared_in_def cdeclaredmethd_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
                   Base_foo_def BaseCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   599
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
lemma Base_foo_no_override:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
 "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides old \<Longrightarrow> P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   602
apply (drule overrides_commonD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   603
apply (clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
apply (frule subclsEval)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
apply    (rule ws_tprg)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
apply    (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
apply    (rule classesDefined) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   608
apply    assumption+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
apply (frule unique_sig_Base_foo) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
            dest: unique_sig_Base_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
lemma Base_foo_no_stat_override:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
 "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides\<^sub>S old \<Longrightarrow> P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
apply (drule stat_overrides_commonD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
apply (clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
apply (frule subclsEval)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
apply    (rule ws_tprg)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   620
apply    (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   621
apply    (rule classesDefined) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
apply    assumption+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
apply (frule unique_sig_Base_foo) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   624
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
            dest: unique_sig_Base_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
lemma Base_foo_no_hide:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
 "tprg,sig\<turnstile>(Base,(snd Base_foo)) hides old \<Longrightarrow> P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
by (auto dest: hidesD simp add: Base_foo_def member_is_static_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
lemma Ext_foo_no_hide:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
 "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) hides old \<Longrightarrow> P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
by (auto dest: hidesD simp add: Ext_foo_def member_is_static_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   637
lemma unique_sig_Ext_foo:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
 "tprg\<turnstile> mdecl (sig, snd Ext_foo) declared_in Ext \<Longrightarrow> sig=foo_sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   639
by (auto simp add: declared_in_def cdeclaredmethd_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
                   Ext_foo_def ExtCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   642
lemma Ext_foo_override:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   643
 "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   644
  \<Longrightarrow> old = (Base,(snd Base_foo))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   645
apply (drule overrides_commonD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   646
apply (clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   647
apply (frule subclsEval)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   648
apply    (rule ws_tprg)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   649
apply    (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
apply    (rule classesDefined) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   651
apply    assumption+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
apply (frule unique_sig_Ext_foo) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
apply (case_tac "old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
apply (auto simp add: ExtCl_def Ext_foo_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
                      BaseCl_def Base_foo_def Object_mdecls_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
                      split_paired_all
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
                      member_is_static_simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
           dest: declared_not_undeclared unique_declaration)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   661
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
lemma Ext_foo_stat_override:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
 "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides\<^sub>S old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
  \<Longrightarrow> old = (Base,(snd Base_foo))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
apply (drule stat_overrides_commonD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
apply (clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
apply (frule subclsEval)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   668
apply    (rule ws_tprg)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
apply    (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   670
apply    (rule classesDefined) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
apply    assumption+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   672
apply (frule unique_sig_Ext_foo) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   673
apply (case_tac "old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   674
apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   675
apply (auto simp add: ExtCl_def Ext_foo_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
                      BaseCl_def Base_foo_def Object_mdecls_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   677
                      split_paired_all
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
                      member_is_static_simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   679
           dest: declared_not_undeclared unique_declaration)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   680
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   681
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   682
lemma Base_foo_member_of_Base: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   683
  "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   684
by (auto intro!: members.Immediate Base_declares_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   685
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   686
lemma Base_foo_member_in_Base: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   687
  "tprg\<turnstile>(Base,mdecl Base_foo) member_in Base"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   688
by (rule member_of_to_member_in [OF Base_foo_member_of_Base])
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   689
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   690
lemma Ext_foo_member_of_Ext: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   691
  "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
by (auto intro!: members.Immediate Ext_declares_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   693
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   694
lemma Ext_foo_member_in_Ext: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   695
  "tprg\<turnstile>(Ext,mdecl Ext_foo) member_in Ext"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   696
by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext])
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   697
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   698
lemma Base_foo_permits_acc:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   699
 "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   700
by ( simp add: permits_acc_def Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   701
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   702
lemma Base_foo_accessible [simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   703
 "tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   704
by (auto intro: accessible_fromR.Immediate 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
                Base_foo_member_of_Base Base_foo_permits_acc)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   706
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   707
lemma Base_foo_dyn_accessible [simp]:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   708
 "tprg\<turnstile>(Base,mdecl Base_foo) in Base dyn_accessible_from S"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   709
apply (rule dyn_accessible_fromR.Immediate)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   710
apply   (rule Base_foo_member_in_Base)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   711
apply   (rule Base_foo_permits_acc)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   712
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   713
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   714
lemma accmethd_Base [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   715
  "accmethd tprg S Base = methd tprg Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   716
apply (simp add: accmethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   717
apply (rule filter_tab_all_True)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   718
apply (simp add: snd_special_simp fst_special_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   719
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   720
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   721
lemma Ext_foo_permits_acc:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   722
 "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   723
by ( simp add: permits_acc_def Ext_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   724
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   725
lemma Ext_foo_accessible [simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   726
 "tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   727
by (auto intro: accessible_fromR.Immediate 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   728
                Ext_foo_member_of_Ext Ext_foo_permits_acc)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   729
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   730
lemma Ext_foo_dyn_accessible [simp]:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   731
 "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from S"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   732
apply (rule dyn_accessible_fromR.Immediate) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   733
apply   (rule Ext_foo_member_in_Ext)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   734
apply   (rule Ext_foo_permits_acc)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   735
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   736
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   737
lemma Ext_foo_overrides_Base_foo:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   738
 "tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   739
proof (rule overridesR.Direct, simp_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   740
  show "\<not> is_static Ext_foo" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   741
    by (simp add: member_is_static_simp Ext_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   742
  show "\<not> is_static Base_foo"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   743
    by (simp add: member_is_static_simp Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   744
  show "accmodi Ext_foo \<noteq> Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   745
    by (simp add: Ext_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   746
  show "msig (Ext, Ext_foo) = msig (Base, Base_foo)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   747
    by (simp add: Ext_foo_def Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   748
  show "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   749
    by (auto intro: Ext_declares_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   750
  show "tprg\<turnstile>mdecl Base_foo declared_in Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   751
    by (auto intro: Base_declares_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   752
  show "tprg \<turnstile>(Base, mdecl Base_foo) inheritable_in java_lang"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   753
    by (simp add: inheritable_in_def Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   754
  show "tprg\<turnstile>resTy Ext_foo\<preceq>resTy Base_foo"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   755
    by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   756
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   757
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   758
lemma accmethd_Ext [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   759
  "accmethd tprg S Ext = methd tprg Ext"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   760
apply (simp add: accmethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   761
apply (rule filter_tab_all_True)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   762
apply (auto simp add: snd_special_simp fst_special_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   763
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   764
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
lemma cls_Ext: "class tprg Ext = Some ExtCl"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   767
lemma dynmethd_Ext_foo:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
 "dynmethd tprg Base Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   769
  = Some (Ext,snd Ext_foo)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   770
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   771
  have "methd tprg Base \<lparr>name = foo, parTs = [Class Base]\<rparr> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   772
          = Some (Base,snd Base_foo)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   773
       "methd tprg Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   774
          = Some (Ext,snd Ext_foo)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   775
    by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   776
  with cls_Ext ws_tprg Ext_foo_overrides_Base_foo
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   777
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   778
    by (auto simp add: dynmethd_rec simp add: Ext_foo_def Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   779
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   780
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   781
lemma Base_fields_accessible[simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   782
 "accfield tprg S Base 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   783
  = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   784
apply (auto simp add: accfield_def expand_fun_eq Let_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   785
                      accessible_in_RefT_simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   786
                      is_public_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   787
                      BaseCl_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   788
                      permits_acc_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   789
                      declared_in_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   790
                      cdeclaredfield_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   791
               intro!: filter_tab_all_True_Some filter_tab_None
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   792
                       accessible_fromR.Immediate
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   793
               intro: members.Immediate)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   794
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   795
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   796
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   797
lemma arr_member_of_Base:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   798
  "tprg\<turnstile>(Base, fdecl (arr, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   799
                 \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   800
          member_of Base"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   801
by (auto intro: members.Immediate 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   802
       simp add: declared_in_def cdeclaredfield_def BaseCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   804
lemma arr_member_in_Base:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   805
  "tprg\<turnstile>(Base, fdecl (arr, 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   806
                 \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   807
          member_in Base"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   808
by (rule member_of_to_member_in [OF arr_member_of_Base])
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   809
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   810
lemma arr_member_of_Ext:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   811
  "tprg\<turnstile>(Base, fdecl (arr, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   812
                    \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   813
             member_of Ext"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   814
apply (rule members.Inherited)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   815
apply   (simp add: inheritable_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   816
apply   (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   817
apply   (auto intro: arr_member_of_Base simp add: subcls1_def ExtCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   818
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   819
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   820
lemma arr_member_in_Ext:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   821
  "tprg\<turnstile>(Base, fdecl (arr, 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   822
                 \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   823
          member_in Ext"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   824
by (rule member_of_to_member_in [OF arr_member_of_Ext])
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   825
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   826
lemma Ext_fields_accessible[simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   827
"accfield tprg S Ext 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   828
  = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   829
apply (auto simp add: accfield_def expand_fun_eq Let_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   830
                      accessible_in_RefT_simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   831
                      is_public_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   832
                      BaseCl_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   833
                      ExtCl_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   834
                      permits_acc_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   835
               intro!: filter_tab_all_True_Some filter_tab_None
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   836
                       accessible_fromR.Immediate)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   837
apply (auto intro: members.Immediate arr_member_of_Ext
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   838
            simp add: declared_in_def cdeclaredfield_def ExtCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   839
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   840
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   841
lemma arr_Base_dyn_accessible [simp]:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   842
"tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   843
       in Base dyn_accessible_from S"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   844
apply (rule dyn_accessible_fromR.Immediate)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   845
apply   (rule arr_member_in_Base)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   846
apply   (simp add: permits_acc_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   847
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   848
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   849
lemma arr_Ext_dyn_accessible[simp]:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   850
"tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   851
       in Ext dyn_accessible_from S"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   852
apply (rule dyn_accessible_fromR.Immediate)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   853
apply   (rule arr_member_in_Ext)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   854
apply   (simp add: permits_acc_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   855
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   856
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   857
lemma array_of_PrimT_acc [simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   858
 "is_acc_type tprg java_lang (PrimT t.[])"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   859
apply (simp add: is_acc_type_def accessible_in_RefT_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   860
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   861
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   862
lemma PrimT_acc [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   863
 "is_acc_type tprg java_lang (PrimT t)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   864
apply (simp add: is_acc_type_def accessible_in_RefT_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   865
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   866
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   867
lemma Object_acc [simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   868
 "is_acc_class tprg java_lang Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   869
apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   870
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   871
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   872
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   873
section "well-formedness"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   874
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   875
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   876
lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   877
apply (unfold wf_idecl_def HasFooInt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   878
apply (auto intro!: wf_mheadI ws_idecl_HasFoo 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   879
            simp add: foo_sig_def foo_mhead_def mhead_resTy_simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   880
                      member_is_static_simp )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   881
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   882
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   883
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   884
declare member_is_static_simp [simp]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   885
declare wt.Skip [rule del] wt.Init [rule del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   886
lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   887
lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   888
ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   889
lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   890
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   891
lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   892
apply (unfold Base_foo_defs )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   893
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   894
            simp add: mhead_resTy_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   895
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   896
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   897
lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   898
apply (unfold Ext_foo_defs )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   899
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   900
            simp add: mhead_resTy_simp )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   901
apply  (rule wt.Cast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   902
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   903
apply    simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   904
apply   (rule_tac [2] narrow.subcls [THEN cast.narrow])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   905
apply   (auto intro!: wtIs)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   906
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   907
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   908
declare mhead_resTy_simp [simp add]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   909
declare member_is_static_simp [simp add]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   910
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   911
lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   912
apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   913
apply (auto intro!: wf_Base_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   914
apply       (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   915
apply (auto intro!: wtIs)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   916
apply (auto simp add: Base_foo_defs entails_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   917
apply   (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   918
apply   (insert Base_foo_no_hide         , simp add: Base_foo_def,blast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   919
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   920
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   921
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   922
lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   923
apply (unfold wf_cdecl_def ExtCl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   924
apply (auto intro!: wf_Ext_foo ws_cdecl_Ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   925
apply (auto simp add: entails_def snd_special_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   926
apply (insert Ext_foo_stat_override)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   927
apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   928
apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   929
apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   930
apply (insert Ext_foo_no_hide)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   931
apply  (simp_all add: qmdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   932
apply  blast+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   933
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   934
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   935
lemma wf_MainC: "wf_cdecl tprg (Main,MainCl)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   936
apply (unfold wf_cdecl_def MainCl_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   937
apply (auto intro: ws_cdecl_Main)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   938
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   939
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   940
lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   941
apply (simp (no_asm) add: Ifaces_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   942
apply (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   943
apply (rule wf_HasFoo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   944
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   945
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   946
lemma wf_cdecl_all_standard_classes: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   947
  "Ball (set standard_classes) (wf_cdecl tprg)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   948
apply (unfold standard_classes_def Let_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   949
       ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   950
apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   951
apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   952
apply (auto simp add: Object_def Classes_def standard_classes_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   953
                      SXcptC_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   954
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   955
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   956
lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set Classes) (wf_cdecl p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   957
apply (simp (no_asm) add: Classes_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   958
apply (simp (no_asm_simp))
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   959
apply    (rule wf_BaseC [THEN conjI])
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   960
apply   (rule wf_ExtC [THEN conjI])
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   961
apply  (rule wf_MainC [THEN conjI])
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   962
apply (rule wf_cdecl_all_standard_classes)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   963
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   964
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   965
theorem wf_tprg: "wf_prog tprg"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   966
apply (unfold wf_prog_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   967
apply (simp (no_asm) add: unique_ifaces unique_classes)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   968
apply (rule conjI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   969
apply  ((simp (no_asm) add: Classes_def standard_classes_def))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   970
apply (rule conjI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   971
apply (simp add: Object_mdecls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   972
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   973
apply  (cut_tac xn_cases_old)   (* FIXME (insert xn_cases) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   974
apply  (simp (no_asm_simp) add: Classes_def standard_classes_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   975
apply  (insert wf_idecl_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   976
apply  (insert wf_cdecl_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   977
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   978
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   979
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   980
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   981
section "max spec"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   982
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   983
lemma appl_methds_Base_foo: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   984
"appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   985
  {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   986
    ,[Class Base])}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   987
apply (unfold appl_methds_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   988
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   989
apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   990
apply  (auto simp add: cmheads_def Base_foo_defs)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   991
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   992
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   993
lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   994
  {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   995
   , [Class Base])}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   996
apply (unfold max_spec_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   997
apply (simp (no_asm) add: appl_methds_Base_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   998
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   999
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1000
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1001
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1002
section "well-typedness"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1003
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1004
lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1005
apply (unfold test_def arr_viewed_from_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1006
(* ?pTs = [Class Base] *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1007
apply (rule wtIs (* ;; *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1008
apply  (rule wtIs (* Ass *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1009
apply  (rule wtIs (* NewC *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1010
apply     (rule wtIs (* LVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1011
apply      (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1012
apply     (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1013
apply    (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1014
apply   (rule wtIs (* NewC *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1015
apply   (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1016
apply  (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1017
apply (rule wtIs (* Try *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1018
prefer 4
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1019
apply    (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1020
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1021
apply    (rule wtIs (* Expr *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1022
apply    (rule wtIs (* Call *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1023
apply       (rule wtIs (* Acc *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1024
apply       (rule wtIs (* LVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1025
apply        (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1026
apply       (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1027
apply      (rule wtIs (* Cons *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1028
apply       (rule wtIs (* Lit *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1029
apply       (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1030
apply      (rule wtIs (* Nil *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1031
apply     (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1032
apply     (rule max_spec_Base_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1033
apply    (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1034
apply   (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1035
apply  (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1036
apply  (simp)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1037
apply  (simp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1038
apply (rule wtIs (* While *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1039
apply  (rule wtIs (* Acc *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1040
apply   (rule wtIs (* AVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1041
apply   (rule wtIs (* Acc *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1042
apply   (rule wtIs (* FVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1043
apply    (rule wtIs (* StatRef *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1044
apply    (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1045
apply   (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1046
apply   (simp )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1047
apply   (simp)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1048
apply   (simp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1049
apply  (rule wtIs (* LVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1050
apply  (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1051
apply (rule wtIs (* Skip *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1052
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1053
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1054
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1055
section "execution"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1056
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1057
lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1058
  new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1059
apply (frule atleast_free_SucD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1060
apply (drule atleast_free_Suc [THEN iffD1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1061
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1062
apply (frule new_Addr_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1063
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1064
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1065
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1066
declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1067
declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1068
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1069
        Base_foo_defs  [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1070
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1071
ML {* bind_thms ("eval_intros", map 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1072
        (simplify (simpset() delsimps [thm "Skip_eq"]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1073
                             addsimps [thm "lvar_def"]) o 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1074
         rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1075
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1076
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1077
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1078
  a :: loc
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1079
  b :: loc
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1080
  c :: loc
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1081
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1082
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1083
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1084
  tprg :: prog
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1085
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1086
  obj_a :: obj
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1087
  obj_b :: obj
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1088
  obj_c :: obj
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1089
  arr_N :: "(vn, val) table"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1090
  arr_a :: "(vn, val) table"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1091
  globs1 :: globs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1092
  globs2 :: globs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1093
  globs3 :: globs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1094
  globs8 :: globs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1095
  locs3 :: locals
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1096
  locs4 :: locals
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1097
  locs8 :: locals
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1098
  s0  :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1099
  s0' :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1100
  s9' :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1101
  s1  :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1102
  s1' :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1103
  s2  :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1104
  s2' :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1105
  s3  :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1106
  s3' :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1107
  s4  :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1108
  s4' :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1109
  s6' :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1110
  s7' :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1111
  s8  :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1112
  s8' :: state
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1113
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1114
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1115
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1116
  "tprg"    == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1117
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1118
  "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) two
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1119
                ,values=empty(Inr 0\<mapsto>Bool False)(Inr one\<mapsto>Bool False)\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1120
  "obj_b"   <= "\<lparr>tag=CInst Ext
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1121
                ,values=(empty(Inl (vee, Base)\<mapsto>Null   ) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1122
			      (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1123
  "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=empty\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1124
  "arr_N"   == "empty(Inl (arr, Base)\<mapsto>Null)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1125
  "arr_a"   == "empty(Inl (arr, Base)\<mapsto>Addr a)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1126
  "globs1"  == "empty(Inr Ext   \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1127
		     (Inr Base  \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1128
		     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1129
  "globs2"  == "empty(Inr Ext   \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1130
		     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1131
		     (Inl a\<mapsto>obj_a)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1132
		     (Inr Base  \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1133
  "globs3"  == "globs2(Inl b\<mapsto>obj_b)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1134
  "globs8"  == "globs3(Inl c\<mapsto>obj_c)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1135
  "locs3"   == "empty(VName e\<mapsto>Addr b)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1136
  "locs4"   == "empty(VName z\<mapsto>Null)(Inr()\<mapsto>Addr b)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1137
  "locs8"   == "locs3(VName z\<mapsto>Addr c)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1138
  "s0"  == "       st empty  empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1139
  "s0'" == " Norm  s0"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1140
  "s1"  == "       st globs1 empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1141
  "s1'" == " Norm  s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1142
  "s2"  == "       st globs2 empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1143
  "s2'" == " Norm  s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1144
  "s3"  == "       st globs3 locs3 "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1145
  "s3'" == " Norm  s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1146
  "s4"  == "       st globs3 locs4"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1147
  "s4'" == " Norm  s4"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1148
  "s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1149
  "s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1150
  "s8"  == "       st globs8 locs8"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1151
  "s8'" == " Norm  s8"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1152
  "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1153
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1154
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1155
syntax "four"::nat
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1156
       "tree"::nat
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1157
       "two" ::nat
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1158
       "one" ::nat
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1159
translations 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1160
  "one"  == "Suc 0"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1161
  "two"  == "Suc one"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1162
  "tree" == "Suc two"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1163
  "four" == "Suc tree"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1164
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1165
declare Pair_eq [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1166
lemma exec_test: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1167
"\<lbrakk>the (new_Addr (heap  s1)) = a;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1168
  the (new_Addr (heap ?s2)) = b;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1169
  the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1170
  atleast_free  (heap s0) four \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1171
  tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1172
apply (unfold test_def arr_viewed_from_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1173
(* ?s9' = s9' *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1174
apply (simp (no_asm_use))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1175
apply (drule (1) alloc_one,clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1176
apply (rule eval_Is (* ;; *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1177
apply  (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1178
apply  (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1179
apply  (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1180
apply  (rule eval_Is (* Expr *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1181
apply  (rule eval_Is (* Ass *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1182
apply   (rule eval_Is (* LVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1183
apply  (rule eval_Is (* NewC *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1184
      (* begin init Ext *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1185
apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1186
apply   (erule_tac V = "atleast_free ?h tree" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1187
apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1188
apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1189
apply   (rule eval_Is (* Init Ext *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1190
apply   (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1191
apply   (rule conjI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1192
prefer 2 apply (rule conjI HOL.refl)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1193
apply   (rule eval_Is (* Init Base *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1194
apply   (simp add: arr_viewed_from_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1195
apply   (rule conjI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1196
apply    (rule eval_Is (* Init Object *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1197
apply    (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1198
apply    (rule conjI, rule HOL.refl)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1199
apply    (rule HOL.refl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1200
apply   (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1201
apply   (rule conjI, rule_tac [2] HOL.refl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1202
apply   (rule eval_Is (* Expr *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1203
apply   (rule eval_Is (* Ass *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1204
apply    (rule eval_Is (* FVar *))
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1205
apply         (rule init_done, simp)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1206
apply        (rule eval_Is (* StatRef *))
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1207
apply       (simp)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1208
apply     (simp add: check_field_access_def Let_def) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1209
apply   (rule eval_Is (* NewA *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1210
apply     (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1211
apply    (rule eval_Is (* Lit *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1212
apply   (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1213
apply   (rule halloc.New)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1214
apply    (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1215
apply   (drule atleast_free_weaken,rotate_tac -1,drule atleast_free_weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1216
apply   (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1217
apply  (simp add: upd_gobj_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1218
      (* end init Ext *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1219
apply  (rule halloc.New)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1220
apply   (drule alloc_one)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1221
prefer 2 apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1222
apply   (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1223
apply  (drule atleast_free_weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1224
apply  force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1225
apply (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1226
apply (drule alloc_one)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1227
apply  (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1228
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1229
apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1230
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1231
apply (simp (no_asm_use))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1232
apply (rule eval_Is (* Try *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1233
apply   (rule eval_Is (* Expr *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1234
      (* begin method call *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1235
apply   (rule eval_Is (* Call *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1236
apply      (rule eval_Is (* Acc *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1237
apply      (rule eval_Is (* LVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1238
apply     (rule eval_Is (* Cons *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1239
apply      (rule eval_Is (* Lit *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1240
apply     (rule eval_Is (* Nil *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1241
apply    (simp)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1242
apply    (simp)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1243
apply    (subgoal_tac
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1244
             "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from Main")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1245
apply      (simp add: check_method_access_def Let_def
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1246
                      invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1247
apply      (rule Ext_foo_dyn_accessible)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1248
apply   (rule eval_Is (* Methd *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1249
apply   (simp add: body_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1250
apply   (rule eval_Is (* Body *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1251
apply     (rule init_done, simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1252
apply       (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1253
apply    (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1254
apply    (rule eval_Is (* Expr *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1255
apply    (rule eval_Is (* Ass *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1256
apply     (rule eval_Is (* FVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1257
apply       (rule init_done, simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1258
apply      (rule eval_Is (* Cast *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1259
apply       (rule eval_Is (* Acc *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1260
apply       (rule eval_Is (* LVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1261
apply      (simp)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1262
apply      (simp split del: split_if)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1263
apply      (simp add: check_field_access_def Let_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1264
apply    (rule eval_Is (* XcptE *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1265
apply   (simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1266
      (* end method call *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1267
apply  (rule sxalloc.intros)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1268
apply  (rule halloc.New)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1269
apply   (erule alloc_one [THEN conjunct1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1270
apply   (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1271
apply  (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1272
apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1273
apply (drule alloc_one [THEN conjunct1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1274
apply  (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1275
apply (erule_tac V = "atleast_free ?h two" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1276
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1277
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1278
apply (rule eval_Is (* While *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1279
apply  (rule eval_Is (* Acc *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1280
apply  (rule eval_Is (* AVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1281
apply    (rule eval_Is (* Acc *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1282
apply    (rule eval_Is (* FVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1283
apply      (rule init_done, simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1284
apply     (rule eval_Is (* StatRef *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1285
apply    (simp)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1286
apply    (simp add: check_field_access_def Let_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1287
apply   (rule eval_Is (* Lit *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1288
apply  (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1289
apply (auto simp add: in_bounds_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1290
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1291
declare Pair_eq [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1292
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1293
end