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