src/HOL/Bali/Decl.thy
author wenzelm
Mon, 26 Jul 2010 17:41:26 +0200
changeset 37956 ee939247b2fb
parent 37678 0040bafffdef
child 41525 a42cbf5b44c8
permissions -rw-r--r--
modernized/unified some specifications;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Decl.thy
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
     2
    Author:     David von Oheimb and Norbert Schirmer
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
header {* Field, method, interface, and class declarations, whole Java programs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
26566
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
     7
theory Decl
27682
25aceefd4786 added class preorder
haftmann
parents: 26566
diff changeset
     8
imports Term Table (** order is significant, because of clash for "var" **)
26566
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
     9
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
improvements:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\item clarification and correction of some aspects of the package/access concept
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
  (Also submitted as bug report to the Java Bug Database:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
   Bug Id: 4485402 and Bug Id: 4493343 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
   http://developer.java.sun.com/developer/bugParade/index.jshtml
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
  )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
simplifications:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
\item the only field and method modifiers are static and the access modifiers
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
\item no constructors, which may be simulated by new + suitable methods
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
\item there is just one global initializer per class, which can simulate all 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
      others
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
\item no throws clause
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
\item a void method is replaced by one that returns Unit (of dummy type Void)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
\item no interface fields
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
\item every class has an explicit superclass (unused for Object)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
\item the (standard) methods of Object and of standard exceptions are not 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
      specified
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
\item no main method
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
subsection {* Modifier*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
subsubsection {* Access modifier *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
datatype acc_modi (* access modifier *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
         = Private | Package | Protected | Public 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
text {* 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
We can define a linear order for the access modifiers. With Private yielding the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
most restrictive access and public the most liberal access policy:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
  Private < Package < Protected < Public
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
 
26566
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
    53
instantiation acc_modi :: linorder
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
    54
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
26566
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
    56
definition
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
    57
  less_acc_def: "a < b
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
    58
      \<longleftrightarrow> (case a of
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
             Private    \<Rightarrow> (b=Package \<or> b=Protected \<or> b=Public)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
           | Package    \<Rightarrow> (b=Protected \<or> b=Public)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
           | Protected  \<Rightarrow> (b=Public)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
           | Public     \<Rightarrow> False)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
26566
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
    64
definition
27682
25aceefd4786 added class preorder
haftmann
parents: 26566
diff changeset
    65
  le_acc_def: "(a :: acc_modi) \<le> b \<longleftrightarrow> a < b \<or> a = b"
26566
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
    66
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
    67
instance proof
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
  fix x y z::acc_modi
27682
25aceefd4786 added class preorder
haftmann
parents: 26566
diff changeset
    69
  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
25aceefd4786 added class preorder
haftmann
parents: 26566
diff changeset
    70
    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
  {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
  show "x \<le> x"               \<spacespace>\<spacespace>    -- reflexivity
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
    by (auto simp add: le_acc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
  assume "x \<le> y" "y \<le> z"           -- transitivity 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
  thus "x \<le> z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
  assume "x \<le> y" "y \<le> x"           -- antisymmetry
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
  thus "x = y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
  proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
    have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
      by (auto simp add: less_acc_def split add: acc_modi.split)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
    with prems show ?thesis
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
    85
      by (unfold le_acc_def) iprover
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
  fix x y:: acc_modi
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
  show  "x \<le> y \<or> y \<le> x"   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
  by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
27682
25aceefd4786 added class preorder
haftmann
parents: 26566
diff changeset
    91
  }
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
qed
26566
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
    93
  
36a93808642c instantiation replacing primitive instance plus overloaded defs
haftmann
parents: 24783
diff changeset
    94
end
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
lemma acc_modi_top [simp]: "Public \<le> a \<Longrightarrow> a = Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
lemma acc_modi_top1 [simp, intro!]: "a \<le> Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
lemma acc_modi_le_Public: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
"a \<le> Public \<Longrightarrow> a=Private \<or> a = Package \<or> a=Protected \<or> a=Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
lemma acc_modi_bottom: "a \<le> Private \<Longrightarrow> a = Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
lemma acc_modi_Private_le: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
"Private \<le> a \<Longrightarrow> a=Private \<or> a = Package \<or> a=Protected \<or> a=Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
lemma acc_modi_Package_le: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
  "Package \<le> a \<Longrightarrow> a = Package \<or> a=Protected \<or> a=Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
lemma acc_modi_le_Package: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
  "a \<le> Package \<Longrightarrow> a=Private \<or> a = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
lemma acc_modi_Protected_le: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
  "Protected \<le> a \<Longrightarrow> a=Protected \<or> a=Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
lemma acc_modi_le_Protected: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
  "a \<le> Protected  \<Longrightarrow> a=Private \<or> a = Package \<or> a = Protected"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
lemmas acc_modi_le_Dests = acc_modi_top           acc_modi_le_Public
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
                           acc_modi_Private_le    acc_modi_bottom
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
                           acc_modi_Package_le    acc_modi_le_Package
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
                           acc_modi_Protected_le  acc_modi_le_Protected
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
lemma acc_modi_Package_le_cases 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
 [consumes 1,case_names Package Protected Public]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
 "Package \<le> m \<Longrightarrow> ( m = Package \<Longrightarrow> P m) \<Longrightarrow> (m=Protected \<Longrightarrow> P m) \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
   (m=Public \<Longrightarrow> P m) \<Longrightarrow> P m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
by (auto dest: acc_modi_Package_le)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
subsubsection {* Static Modifier *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
types stat_modi = bool (* modifier: static *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
subsection {* Declaration (base "class" for member,interface and class
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
 declarations *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
record decl =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
        access :: acc_modi
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   152
  (type) "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   153
  (type) "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
subsection {* Member (field or method)*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
record  member = decl +
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
         static :: stat_modi
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   160
  (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   161
  (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
subsection {* Field *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
record field = member +
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
        type :: ty
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   168
  (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   169
  (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
types     
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
        fdecl           (* field declaration, cf. 8.3 *)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   173
        = "vname \<times> field"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   177
  (type) "fdecl" <= (type) "vname \<times> field"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
subsection  {* Method *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
record mhead = member +     (* method head (excluding signature) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
        pars ::"vname list" (* parameter names *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
        resT ::ty           (* result type *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
record mbody =                      (* method body *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
        lcls::  "(vname \<times> ty) list" (* local variables *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
        stmt:: stmt                 (* the body statement *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
record methd = mhead + (* method in a class *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
        mbody::mbody
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
types mdecl = "sig \<times> methd"  (* method declaration in a class *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   196
  (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
                      pars::vname list, resT::ty\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   198
  (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
                      pars::vname list, resT::ty,\<dots>::'a\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   200
  (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   201
  (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"      
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   202
  (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
                      pars::vname list, resT::ty,mbody::mbody\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   204
  (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
                      pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   206
  (type) "mdecl" <= (type) "sig \<times> methd"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   209
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   210
  mhead :: "methd \<Rightarrow> mhead"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   211
  where "mhead m = \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
lemma access_mhead [simp]:"access (mhead m) = access m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
lemma static_mhead [simp]:"static (mhead m) = static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
lemma pars_mhead [simp]:"pars (mhead m) = pars m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
lemma resT_mhead [simp]:"resT (mhead m) = resT m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
text {* To be able to talk uniformaly about field and method declarations we
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
introduce the notion of a member declaration (e.g. useful to define 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
accessiblity ) *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
datatype memberdecl = fdecl fdecl | mdecl mdecl
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
datatype memberid = fid vname | mid sig
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   233
class has_memberid =
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   234
  fixes memberid :: "'a \<Rightarrow> memberid"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   236
instantiation memberdecl :: has_memberid
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   237
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   239
definition
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
memberdecl_memberid_def:
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   241
  "memberid m = (case m of
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
                    fdecl (vn,f)  \<Rightarrow> fid vn
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
                  | mdecl (sig,m) \<Rightarrow> mid sig)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   245
instance ..
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   246
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   247
end
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   248
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
by (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
lemma memberid_fdecl_simp1: "memberid (fdecl f) = fid (fst f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
by (cases f) (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
lemma memberid_mdecl_simp[simp]: "memberid (mdecl (sig,m)) = mid sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
by (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
by (cases m) (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 35547
diff changeset
   261
instantiation prod :: (type, has_memberid) has_memberid
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   262
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   264
definition
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
pair_memberid_def:
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   266
  "memberid p = memberid (snd p)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   268
instance ..
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   269
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   270
end
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   271
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
by (simp add: pair_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
lemma memberid_pair_simp1: "memberid p  = memberid (snd p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
by (simp add: pair_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   278
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   279
  is_field :: "qtname \<times> memberdecl \<Rightarrow> bool"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   280
  where "is_field m = (\<exists> declC f. m=(declC,fdecl f))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
by (simp add: is_field_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
lemma is_fieldI: "is_field (C,fdecl f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
by (simp add: is_field_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   288
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   289
  is_method :: "qtname \<times> memberdecl \<Rightarrow> bool"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   290
  where "is_method membr = (\<exists>declC m. membr=(declC,mdecl m))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
by (simp add: is_method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
lemma is_methodI: "is_method (C,mdecl m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
by (simp add: is_method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
subsection {* Interface *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
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: 13601
diff changeset
   302
record  ibody = decl +  --{* interface body *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   303
          imethods :: "(sig \<times> mhead) list" --{* method heads *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
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: 13601
diff changeset
   305
record  iface = ibody + --{* interface *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   306
         isuperIfs:: "qtname list" --{* superinterface list *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   307
types
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   308
        idecl           --{* interface declaration, cf. 9.1 *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   309
        = "qtname \<times> iface"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   312
  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   313
  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   314
  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
                      isuperIfs::qtname list\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   316
  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
                      isuperIfs::qtname list,\<dots>::'a\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   318
  (type) "idecl" <= (type) "qtname \<times> iface"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   320
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   321
  ibody :: "iface \<Rightarrow> ibody"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   322
  where "ibody i = \<lparr>access=access i,imethods=imethods i\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
lemma access_ibody [simp]: "(access (ibody i)) = access i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
by (simp add: ibody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
lemma imethods_ibody [simp]: "(imethods (ibody i)) = imethods i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
by (simp add: ibody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
subsection  {* Class *}
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: 13601
diff changeset
   331
record cbody = decl +          --{* class body *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
         cfields:: "fdecl list" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
         methods:: "mdecl list"
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: 13601
diff changeset
   334
         init   :: "stmt"       --{* initializer *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
18551
be0705186ff5 class now an keyword, quoted where necessary
haftmann
parents: 18447
diff changeset
   336
record "class" = cbody +           --{* class *}
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: 13601
diff changeset
   337
        super   :: "qtname"      --{* superclass *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   338
        superIfs:: "qtname list" --{* implemented interfaces *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   339
types
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   340
        cdecl           --{* class declaration, cf. 8.1 *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   341
        = "qtname \<times> class"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   344
  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
                      methods::mdecl list,init::stmt\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   346
  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
                      methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   348
  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
                      methods::mdecl list,init::stmt,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
                      super::qtname,superIfs::qtname list\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   351
  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
                      methods::mdecl list,init::stmt,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
                      super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   354
  (type) "cdecl" <= (type) "qtname \<times> class"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   356
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   357
  cbody :: "class \<Rightarrow> cbody"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   358
  where "cbody c = \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
lemma access_cbody [simp]:"access (cbody c) = access c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
lemma cfields_cbody [simp]:"cfields (cbody c) = cfields c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
lemma methods_cbody [simp]:"methods (cbody c) = methods c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
lemma init_cbody [simp]:"init (cbody c) = init c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
section "standard classes"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
consts
14674
3506a9af46fc *** empty log message ***
wenzelm
parents: 14171
diff changeset
   376
  Object_mdecls  ::  "mdecl list" --{* methods of Object *}
3506a9af46fc *** empty log message ***
wenzelm
parents: 14171
diff changeset
   377
  SXcpt_mdecls   ::  "mdecl list" --{* methods of SXcpts *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   379
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   380
  ObjectC ::         "cdecl"      --{* declaration  of root      class   *} where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   381
  "ObjectC = (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   382
                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   384
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   385
  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *} where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   386
  "SXcptC xn = (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
                                   init=Skip,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
                                   super=if xn = Throwable then Object 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
                                                           else SXcpt Throwable,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
                                   superIfs=[]\<rparr>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
lemma ObjectC_neq_SXcptC [simp]: "ObjectC \<noteq> SXcptC xn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
17778
93d7e524417a changes due to new neq_simproc in simpdata.ML
nipkow
parents: 17589
diff changeset
   396
by (simp add: SXcptC_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   398
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   399
  standard_classes :: "cdecl list" where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   400
  "standard_classes = [ObjectC, SXcptC Throwable,
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   401
                SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   402
                SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
section "programs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
record prog =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
        ifaces ::"idecl list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
        "classes"::"cdecl list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   412
     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   413
     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   414
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   415
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   416
  iface :: "prog  \<Rightarrow> (qtname, iface) table"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   417
  where "iface G I == table_of (ifaces G) I"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   418
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   419
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   420
  "class" :: "prog  \<Rightarrow> (qtname, class) table"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   421
  where "class G C == table_of (classes G) C"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   423
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   424
  is_iface :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   425
  where "is_iface G I == iface G I \<noteq> None"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   426
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   427
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   428
  is_class :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   429
  where "is_class G C == class G C \<noteq> None"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
section "is type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   434
primrec is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   435
  and isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   436
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   437
  "is_type G (PrimT pt)  = True"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   438
| "is_type G (RefT  rt)  = isrtype G rt"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   439
| "isrtype G (NullT) = True"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   440
| "isrtype G (IfaceT tn) = is_iface G tn"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   441
| "isrtype G (ClassT tn) = is_class G tn"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   442
| "isrtype G (ArrayT T ) = is_type  G T"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
lemma type_is_class: "is_type G (Class C) \<Longrightarrow>  is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
section "subinterface and subclass relation, in anticipation of TypeRel.thy"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   453
definition
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: 13601
diff changeset
   454
  subint1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subinterface *}
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   455
  where "subint1 G = {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   457
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   458
  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass *}
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   459
  where "subcls1 G = {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   461
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   462
  subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   463
  where "G|-C <:C1 D == (C,D) \<in> subcls1 G"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   464
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   465
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   466
  subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   467
  where "G|-C <=:C D == (C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   469
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   470
  subcls_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   471
  where "G|-C <:C D == (C,D) \<in>(subcls1 G)^+"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   473
notation (xsymbols)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   474
  subcls1_syntax  ("_\<turnstile>_\<prec>\<^sub>C1_"  [71,71,71] 70) and
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   475
  subclseq_syntax  ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70) and
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   476
  subcls_syntax  ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
lemma subint1I: "\<lbrakk>iface G I = Some i; J \<in> set (isuperIfs i)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
                 \<Longrightarrow> (I,J) \<in> subint1 G" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
apply (simp add: subint1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
lemma subcls1I:"\<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk> \<Longrightarrow> (C,(super c)) \<in> subcls1 G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
apply (simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
lemma subint1D: "(I,J)\<in>subint1 G\<Longrightarrow> \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
by (simp add: subint1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
lemma subcls1D: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
  "(C,D)\<in>subcls1 G \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c. class G C = Some c \<and> (super c = D))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
apply (simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
lemma subint1_def2:  
14952
47455995693d removal of x-symbol syntax <Sigma> for dependent products
paulson
parents: 14674
diff changeset
   498
  "subint1 G = (SIGMA I: {I. is_iface G I}. set (isuperIfs (the (iface G I))))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
apply (unfold subint1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
lemma subcls1_def2: 
14952
47455995693d removal of x-symbol syntax <Sigma> for dependent products
paulson
parents: 14674
diff changeset
   504
  "subcls1 G = 
47455995693d removal of x-symbol syntax <Sigma> for dependent products
paulson
parents: 14674
diff changeset
   505
     (SIGMA C: {C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
apply (unfold subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
lemma subcls_is_class:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D\<rbrakk> \<Longrightarrow> \<exists> c. class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
by (auto simp add: subcls1_def dest: tranclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   514
lemma no_subcls1_Object:"G\<turnstile>Object\<prec>\<^sub>C1 D \<Longrightarrow> P"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
by (auto simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
lemma no_subcls_Object: "G\<turnstile>Object\<prec>\<^sub>C D \<Longrightarrow> P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
apply (erule trancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
apply (auto intro: no_subcls1_Object)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
section "well-structured programs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   524
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   525
  ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   526
  where "ws_idecl G I si = (\<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   527
  
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   528
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   529
  ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   530
  where "ws_cdecl G C sc = (C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
  
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   532
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   533
  ws_prog  :: "prog \<Rightarrow> bool" where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   534
  "ws_prog G = ((\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   535
                 (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c)))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
lemma ws_progI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
"\<lbrakk>\<forall>(I,i)\<in>set (ifaces G). \<forall>J\<in>set (isuperIfs i). is_iface G J \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
                                                (J,I) \<notin> (subint1 G)^+; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
  \<forall>(C,c)\<in>set (classes G). C\<noteq>Object \<longrightarrow> is_class G (super c) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
                                        ((super c),C) \<notin> (subcls1 G)^+  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
 \<rbrakk> \<Longrightarrow> ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
apply (unfold ws_prog_def ws_idecl_def ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
apply (erule_tac conjI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   547
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   549
lemma ws_prog_ideclD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
"\<lbrakk>iface G I = Some i; J\<in>set (isuperIfs i); ws_prog G\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   551
  is_iface G J \<and> (J,I)\<notin>(subint1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
apply (unfold ws_prog_def ws_idecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
apply (drule_tac map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
lemma ws_prog_cdeclD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
"\<lbrakk>class G C = Some c; C\<noteq>Object; ws_prog G\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
  is_class G (super c) \<and> (super c,C)\<notin>(subcls1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
apply (unfold ws_prog_def ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
apply (drule_tac map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
section "well-foundedness"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
lemma finite_is_iface: "finite {I. is_iface G I}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
apply (fold dom_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
apply (rule_tac finite_dom_map_of)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
lemma finite_is_class: "finite {C. is_class G C}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
apply (fold dom_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
apply (rule_tac finite_dom_map_of)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
lemma finite_subint1: "finite (subint1 G)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
apply (subst subint1_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
apply (rule finite_SigmaI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
apply (rule finite_is_iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
lemma finite_subcls1: "finite (subcls1 G)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
apply (subst subcls1_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
apply (rule finite_SigmaI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
apply (rule finite_is_class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
apply (rule_tac B = "{super (the (class G C))}" in finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   594
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
lemma subint1_irrefl_lemma1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   596
  "ws_prog G \<Longrightarrow> (subint1 G)^-1 \<inter> (subint1 G)^+ = {}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
apply (force dest: subint1D ws_prog_ideclD conjunct2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   599
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
lemma subcls1_irrefl_lemma1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
  "ws_prog G \<Longrightarrow> (subcls1 G)^-1 \<inter> (subcls1 G)^+ = {}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   602
apply (force dest: subcls1D ws_prog_cdeclD conjunct2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   603
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
lemmas subint1_irrefl_lemma2 = subint1_irrefl_lemma1 [THEN irrefl_tranclI']
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   608
lemma subint1_irrefl: "\<lbrakk>(x, y) \<in> subint1 G; ws_prog G\<rbrakk> \<Longrightarrow> x \<noteq> y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
apply (rule irrefl_trancl_rD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
apply (rule subint1_irrefl_lemma2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1 G; ws_prog G\<rbrakk> \<Longrightarrow> x \<noteq> y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
apply (rule irrefl_trancl_rD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
apply (rule subcls1_irrefl_lemma2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   620
lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   621
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   624
lemma wf_subint1: "ws_prog G \<Longrightarrow> wf ((subint1 G)\<inverse>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
by (auto intro: finite_acyclic_wf_converse finite_subint1 subint1_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
lemma wf_subcls1: "ws_prog G \<Longrightarrow> wf ((subcls1 G)\<inverse>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
lemma subint1_induct: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
  "\<lbrakk>ws_prog G; \<And>x. \<forall>y. (x, y) \<in> subint1 G \<longrightarrow> P y \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
apply (frule wf_subint1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
apply (erule wf_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
apply (simp (no_asm_use) only: converse_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
apply blast
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
lemma subcls1_induct [consumes 1]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
  "\<lbrakk>ws_prog G; \<And>x. \<forall>y. (x, y) \<in> subcls1 G \<longrightarrow> P y \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
apply (frule wf_subcls1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   642
apply (erule wf_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   643
apply (simp (no_asm_use) only: converse_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   644
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   645
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   646
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   647
lemma ws_subint1_induct: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   648
 "\<lbrakk>is_iface G I; ws_prog G; \<And>I i. \<lbrakk>iface G I = Some i \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   649
   (\<forall>J \<in> set (isuperIfs i). (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J)\<rbrakk> \<Longrightarrow> P I
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
  \<rbrakk> \<Longrightarrow> P I"
24038
18182c4aec9e replaced make_imp by rev_mp;
wenzelm
parents: 18576
diff changeset
   651
apply (erule rev_mp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
apply (rule subint1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
apply  assumption
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 17778
diff changeset
   654
apply (simp (no_asm)) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
apply safe
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 17778
diff changeset
   656
apply (blast dest: subint1I ws_prog_ideclD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
lemma ws_subcls1_induct: "\<lbrakk>is_class G C; ws_prog G;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   661
  \<And>C c. \<lbrakk>class G C = Some c;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
 (C \<noteq> Object \<longrightarrow> (C,(super c))\<in>subcls1 G \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
                  P (super c) \<and> is_class G (super c))\<rbrakk> \<Longrightarrow> P C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
 \<rbrakk> \<Longrightarrow> P C"
24038
18182c4aec9e replaced make_imp by rev_mp;
wenzelm
parents: 18576
diff changeset
   665
apply (erule rev_mp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
apply (rule subcls1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
apply  assumption
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 17778
diff changeset
   668
apply (simp (no_asm)) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   670
apply (fast dest: subcls1I ws_prog_cdeclD)
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 ws_class_induct [consumes 2, case_names Object Subcls]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   674
"\<lbrakk>class G C = Some c; ws_prog G; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   675
  \<And> co. class G Object = Some co \<Longrightarrow> P Object; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
  \<And>  C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   677
 \<rbrakk> \<Longrightarrow> P C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   679
  assume clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   680
  and    init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   681
  and    step: "\<And>   C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   682
  assume ws: "ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   683
  then have "is_class G C \<Longrightarrow> P C"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   684
  proof (induct rule: subcls1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   685
    fix C
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   686
    assume   hyp:"\<forall> S. G\<turnstile>C \<prec>\<^sub>C1 S \<longrightarrow> is_class G S \<longrightarrow> P S"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   687
       and iscls:"is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   688
    show "P C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   689
    proof (cases "C=Object")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   690
      case True with iscls init show "P C" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   691
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
      case False with ws step hyp iscls 
18576
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18551
diff changeset
   693
      show "P C" by (auto dest: subcls1I ws_prog_cdeclD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   694
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   695
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   696
  with clsC show ?thesis by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   697
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   698
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   699
lemma ws_class_induct' [consumes 2, case_names Object Subcls]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   700
"\<lbrakk>is_class G C; ws_prog G; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   701
  \<And> co. class G Object = Some co \<Longrightarrow> P Object; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   702
  \<And> C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   703
 \<rbrakk> \<Longrightarrow> P C"
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 17778
diff changeset
   704
by (auto intro: ws_class_induct)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   706
lemma ws_class_induct'' [consumes 2, case_names Object Subcls]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   707
"\<lbrakk>class G C = Some c; ws_prog G; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   708
  \<And> co. class G Object = Some co \<Longrightarrow> P Object co; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   709
  \<And>  C c sc. \<lbrakk>class G C = Some c; class G (super c) = Some sc;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   710
            C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   711
 \<rbrakk> \<Longrightarrow> P C c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   712
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   713
  assume clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   714
  and    init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object co"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   715
  and    step: "\<And> C c sc . \<lbrakk>class G C = Some c; class G (super c) = Some sc;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   716
                             C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   717
  assume ws: "ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   718
  then have "\<And> c. class G C = Some c\<Longrightarrow> P C c"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   719
  proof (induct rule: subcls1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   720
    fix C c
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   721
    assume   hyp:"\<forall> S. G\<turnstile>C \<prec>\<^sub>C1 S \<longrightarrow> (\<forall> s. class G S = Some s \<longrightarrow> P S s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   722
       and iscls:"class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   723
    show "P C c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   724
    proof (cases "C=Object")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   725
      case True with iscls init show "P C c" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   726
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   727
      case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   728
      with ws iscls obtain sc where
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   729
        sc: "class G (super c) = Some sc"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   730
        by (auto dest: ws_prog_cdeclD)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   731
      from iscls False have "G\<turnstile>C \<prec>\<^sub>C1 (super c)" by (rule subcls1I)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   732
      with False ws step hyp iscls sc
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   733
      show "P C c" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   734
        by (auto)  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   735
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   736
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   737
  with clsC show "P C c" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   738
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   739
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   740
lemma ws_interface_induct [consumes 2, case_names Step]:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   741
  assumes is_if_I: "is_iface G I" and 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   742
               ws: "ws_prog G" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   743
          hyp_sub: "\<And>I i. \<lbrakk>iface G I = Some i; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   744
                            \<forall> J \<in> set (isuperIfs i).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   745
                                 (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J\<rbrakk> \<Longrightarrow> P I"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   746
  shows "P I"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   747
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   748
  from is_if_I ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   749
  show "P I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   750
  proof (rule ws_subint1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   751
    fix I i
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   752
    assume hyp: "iface G I = Some i \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   753
                (\<forall>J\<in>set (isuperIfs i). (I,J) \<in>subint1 G \<and> P J \<and> is_iface G J)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   754
    then have if_I: "iface G I = Some i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   755
      by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   756
    show "P I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   757
    proof (cases "isuperIfs i")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   758
      case Nil
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   759
      with if_I hyp_sub 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   760
      show "P I" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   761
        by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   762
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   763
      case (Cons hd tl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   764
      with hyp if_I hyp_sub 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
      show "P I" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   766
        by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   767
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   769
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   770
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   771
section "general recursion operators for the interface and class hiearchies"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   772
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   773
function
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   774
  iface_rec  :: "prog \<Rightarrow> qtname \<Rightarrow>   \<spacespace>(qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   775
where
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   776
[simp del]: "iface_rec G I f = 
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   777
  (case iface G I of 
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27682
diff changeset
   778
         None \<Rightarrow> undefined 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   779
       | Some i \<Rightarrow> if ws_prog G 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   780
                      then f I i 
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   781
                               ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27682
diff changeset
   782
                      else undefined)"
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   783
by auto
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   784
termination
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   785
by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subint1 G)^-1)) (%(x,y,z). (x,y))")
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   786
 (auto simp: wf_subint1 subint1I wf_same_fst)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   787
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   788
lemma iface_rec: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   789
"\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow> 
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   790
 iface_rec G I f = f I i ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   791
apply (subst iface_rec.simps)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   792
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   793
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   794
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   795
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   796
function
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   797
  class_rec  :: "prog \<Rightarrow> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a     \<Rightarrow> 'a) \<Rightarrow> 'a"
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   798
where
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   799
[simp del]: "class_rec G C t f = 
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   800
  (case class G C of 
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27682
diff changeset
   801
           None \<Rightarrow> undefined 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   802
         | Some c \<Rightarrow> if ws_prog G 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
                        then f C c 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   804
                                 (if C = Object then t 
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   805
                                                else class_rec G (super c) t f)
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27682
diff changeset
   806
                        else undefined)"
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   807
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   808
by auto
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   809
termination
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   810
by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)) (%(x,y,z,w). (x,y))")
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   811
 (auto simp: wf_subcls1 subcls1I wf_same_fst)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   812
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   813
lemma class_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   814
 class_rec G C t f = 
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   815
   f C c (if C = Object then t else class_rec G (super c) t f)"
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   816
apply (subst class_rec.simps)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   817
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   818
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   819
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   820
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   821
  imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
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: 13601
diff changeset
   822
  --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 37678
diff changeset
   823
  "imethds G I = iface_rec G I
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   824
              (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
30235
58d147683393 Made Option a separate theory and renamed option_map to Option.map
nipkow
parents: 28524
diff changeset
   825
                        (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   826
        
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   827
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   828
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   829
end