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