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