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