src/HOL/Bali/Decl.thy
author wenzelm
Wed, 03 Mar 2010 00:33:02 +0100
changeset 35431 8758fe1fc9f8
parent 35416 d8d7d1b785af
child 35547 991a6af75978
permissions -rw-r--r--
cleanup type translations;
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
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   209
definition mhead :: "methd \<Rightarrow> mhead" where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
  "mhead m \<equiv> \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
lemma access_mhead [simp]:"access (mhead m) = access m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
lemma static_mhead [simp]:"static (mhead m) = static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
lemma pars_mhead [simp]:"pars (mhead m) = pars m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
lemma resT_mhead [simp]:"resT (mhead m) = resT m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
text {* To be able to talk uniformaly about field and method declarations we
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
introduce the notion of a member declaration (e.g. useful to define 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
accessiblity ) *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
datatype memberdecl = fdecl fdecl | mdecl mdecl
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
datatype memberid = fid vname | mid sig
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   232
class has_memberid =
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   233
  fixes memberid :: "'a \<Rightarrow> memberid"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   235
instantiation memberdecl :: has_memberid
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   236
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   238
definition
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
memberdecl_memberid_def:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
  "memberid m \<equiv> (case m of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
                    fdecl (vn,f)  \<Rightarrow> fid vn
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
                  | mdecl (sig,m) \<Rightarrow> mid sig)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   244
instance ..
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   245
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   246
end
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   247
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
by (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
lemma memberid_fdecl_simp1: "memberid (fdecl f) = fid (fst f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
by (cases f) (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
lemma memberid_mdecl_simp[simp]: "memberid (mdecl (sig,m)) = mid sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
by (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
by (cases m) (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   260
instantiation * :: (type, has_memberid) has_memberid
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   261
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   263
definition
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
pair_memberid_def:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
  "memberid p \<equiv> memberid (snd p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
35315
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   267
instance ..
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   268
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   269
end
fbdc860d87a3 dropped axclass
haftmann
parents: 35069
diff changeset
   270
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
by (simp add: pair_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
lemma memberid_pair_simp1: "memberid p  = memberid (snd p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
by (simp add: pair_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   277
definition is_field :: "qtname \<times> memberdecl \<Rightarrow> bool" where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
"is_field m \<equiv> \<exists> declC f. m=(declC,fdecl f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
by (simp add: is_field_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
lemma is_fieldI: "is_field (C,fdecl f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
by (simp add: is_field_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   286
definition is_method :: "qtname \<times> memberdecl \<Rightarrow> bool" where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
"is_method membr \<equiv> \<exists> declC m. membr=(declC,mdecl m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
by (simp add: is_method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
lemma is_methodI: "is_method (C,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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
subsection {* Interface *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
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
   299
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
   300
          imethods :: "(sig \<times> mhead) list" --{* method heads *}
12854
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  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
   303
         isuperIfs:: "qtname list" --{* superinterface list *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   304
types
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   305
        idecl           --{* interface declaration, cf. 9.1 *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   306
        = "qtname \<times> iface"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   309
  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   310
  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   311
  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
                      isuperIfs::qtname list\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   313
  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
                      isuperIfs::qtname list,\<dots>::'a\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   315
  (type) "idecl" <= (type) "qtname \<times> iface"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   317
definition ibody :: "iface \<Rightarrow> ibody" where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
  "ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
lemma access_ibody [simp]: "(access (ibody i)) = access i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
by (simp add: ibody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
lemma imethods_ibody [simp]: "(imethods (ibody i)) = imethods i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
by (simp add: ibody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
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
   327
record cbody = decl +          --{* class body *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
         cfields:: "fdecl list" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
         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
   330
         init   :: "stmt"       --{* initializer *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
18551
be0705186ff5 class now an keyword, quoted where necessary
haftmann
parents: 18447
diff changeset
   332
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
   333
        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
   334
        superIfs:: "qtname list" --{* implemented interfaces *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   335
types
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   336
        cdecl           --{* class declaration, cf. 8.1 *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   337
        = "qtname \<times> class"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   340
  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
                      methods::mdecl list,init::stmt\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   342
  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
                      methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   344
  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
                      methods::mdecl list,init::stmt,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
                      super::qtname,superIfs::qtname list\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   347
  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
                      methods::mdecl list,init::stmt,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
                      super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   350
  (type) "cdecl" <= (type) "qtname \<times> class"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   352
definition cbody :: "class \<Rightarrow> cbody" where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
  "cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
lemma access_cbody [simp]:"access (cbody c) = access c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
lemma cfields_cbody [simp]:"cfields (cbody c) = cfields c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
lemma methods_cbody [simp]:"methods (cbody c) = methods c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
lemma init_cbody [simp]:"init (cbody c) = init c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
section "standard classes"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
14674
3506a9af46fc *** empty log message ***
wenzelm
parents: 14171
diff changeset
   372
  Object_mdecls  ::  "mdecl list" --{* methods of Object *}
3506a9af46fc *** empty log message ***
wenzelm
parents: 14171
diff changeset
   373
  SXcpt_mdecls   ::  "mdecl list" --{* methods of SXcpts *}
3506a9af46fc *** empty log message ***
wenzelm
parents: 14171
diff changeset
   374
  ObjectC ::         "cdecl"      --{* declaration  of root      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
   375
  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
defs 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
ObjectC_def:"ObjectC  \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27682
diff changeset
   381
                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
                                   init=Skip,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
                                   super=if xn = Throwable then Object 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
                                                           else SXcpt Throwable,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
                                   superIfs=[]\<rparr>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
lemma ObjectC_neq_SXcptC [simp]: "ObjectC \<noteq> SXcptC xn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
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
   392
by (simp add: SXcptC_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   394
definition standard_classes :: "cdecl list" where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
         "standard_classes \<equiv> [ObjectC, SXcptC Throwable,
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   396
                SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   397
                SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
section "programs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
record prog =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
        ifaces ::"idecl list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
        "classes"::"cdecl list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
translations
35431
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   407
     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
8758fe1fc9f8 cleanup type translations;
wenzelm
parents: 35416
diff changeset
   408
     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   410
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   411
  iface :: "prog  \<Rightarrow> (qtname, iface) table"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   412
  where "iface G I == table_of (ifaces G) I"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   413
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   414
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   415
  "class" :: "prog  \<Rightarrow> (qtname, class) table"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   416
  where "class G C == table_of (classes G) C"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   418
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   419
  is_iface :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   420
  where "is_iface G I == iface G I \<noteq> None"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   421
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   422
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   423
  is_class :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   424
  where "is_class G C == class G C \<noteq> None"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
section "is type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
  is_type :: "prog \<Rightarrow>     ty \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
  isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   433
primrec "is_type G (PrimT pt)  = True"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   434
        "is_type G (RefT  rt)  = isrtype G rt"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   435
        "isrtype G (NullT    ) = True"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   436
        "isrtype G (IfaceT tn) = is_iface G tn"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   437
        "isrtype G (ClassT tn) = is_class G tn"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   438
        "isrtype G (ArrayT T ) = is_type  G T"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
lemma type_is_class: "is_type G (Class C) \<Longrightarrow>  is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
section "subinterface and subclass relation, in anticipation of TypeRel.thy"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
consts 
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
   450
  subint1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subinterface *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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
   451
  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass     *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
defs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
  subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
  subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   457
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   458
  subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   459
  where "G|-C <:C1 D == (C,D) \<in> subcls1 G"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   460
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
  subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   463
  where "G|-C <=:C D == (C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
35067
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
  subcls_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)^+"
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
notation (xsymbols)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   470
  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
   471
  subclseq_syntax  ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70) and
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   472
  subcls_syntax  ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
lemma subint1I: "\<lbrakk>iface G I = Some i; J \<in> set (isuperIfs i)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
                 \<Longrightarrow> (I,J) \<in> subint1 G" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
apply (simp add: subint1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
lemma 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
   480
apply (simp add: subcls1_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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
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
   485
by (simp add: subint1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
lemma subcls1D: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
  "(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
   489
apply (simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
lemma subint1_def2:  
14952
47455995693d removal of x-symbol syntax <Sigma> for dependent products
paulson
parents: 14674
diff changeset
   494
  "subint1 G = (SIGMA I: {I. is_iface G I}. set (isuperIfs (the (iface G I))))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
apply (unfold subint1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
lemma subcls1_def2: 
14952
47455995693d removal of x-symbol syntax <Sigma> for dependent products
paulson
parents: 14674
diff changeset
   500
  "subcls1 G = 
47455995693d removal of x-symbol syntax <Sigma> for dependent products
paulson
parents: 14674
diff changeset
   501
     (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
   502
apply (unfold subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
lemma subcls_is_class:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
"\<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
   508
by (auto simp add: subcls1_def dest: tranclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   510
lemma no_subcls1_Object:"G\<turnstile>Object\<prec>\<^sub>C1 D \<Longrightarrow> P"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
by (auto simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
lemma no_subcls_Object: "G\<turnstile>Object\<prec>\<^sub>C D \<Longrightarrow> P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
apply (erule trancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
apply (auto intro: no_subcls1_Object)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
section "well-structured programs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   520
definition ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool" where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
 "ws_idecl G I si \<equiv> \<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
  
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   523
definition ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
 "ws_cdecl G C sc \<equiv> C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
  
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   526
definition ws_prog  :: "prog \<Rightarrow> bool" where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   527
 "ws_prog G \<equiv> (\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   528
              (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
lemma ws_progI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
"\<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
   533
                                                (J,I) \<notin> (subint1 G)^+; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
  \<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
   535
                                        ((super c),C) \<notin> (subcls1 G)^+  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
 \<rbrakk> \<Longrightarrow> ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
apply (unfold ws_prog_def ws_idecl_def ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
apply (erule_tac conjI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
lemma ws_prog_ideclD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
"\<lbrakk>iface G I = Some i; J\<in>set (isuperIfs i); ws_prog G\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
  is_iface G J \<and> (J,I)\<notin>(subint1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
apply (unfold ws_prog_def ws_idecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   547
apply (drule_tac map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   549
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   551
lemma ws_prog_cdeclD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
"\<lbrakk>class G C = Some c; C\<noteq>Object; ws_prog G\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
  is_class G (super c) \<and> (super c,C)\<notin>(subcls1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
apply (unfold ws_prog_def ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
apply (drule_tac map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
section "well-foundedness"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
lemma finite_is_iface: "finite {I. is_iface G I}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
apply (fold dom_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
apply (rule_tac finite_dom_map_of)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
lemma finite_is_class: "finite {C. is_class G C}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
apply (fold dom_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
apply (rule_tac finite_dom_map_of)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
lemma finite_subint1: "finite (subint1 G)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
apply (subst subint1_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
apply (rule finite_SigmaI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
apply (rule finite_is_iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
apply (simp (no_asm))
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_subcls1: "finite (subcls1 G)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
apply (subst subcls1_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_class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
apply (rule_tac B = "{super (the (class G C))}" in finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
lemma subint1_irrefl_lemma1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
  "ws_prog G \<Longrightarrow> (subint1 G)^-1 \<inter> (subint1 G)^+ = {}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
apply (force dest: subint1D ws_prog_ideclD conjunct2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
lemma subcls1_irrefl_lemma1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   594
  "ws_prog G \<Longrightarrow> (subcls1 G)^-1 \<inter> (subcls1 G)^+ = {}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
apply (force dest: subcls1D ws_prog_cdeclD conjunct2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   596
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
lemmas subint1_irrefl_lemma2 = subint1_irrefl_lemma1 [THEN irrefl_tranclI']
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   599
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
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
   602
apply (rule irrefl_trancl_rD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   603
apply (rule subint1_irrefl_lemma2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
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
   608
apply (rule irrefl_trancl_rD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
apply (rule subcls1_irrefl_lemma2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
lemma wf_subint1: "ws_prog G \<Longrightarrow> wf ((subint1 G)\<inverse>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
by (auto intro: finite_acyclic_wf_converse finite_subint1 subint1_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   620
lemma wf_subcls1: "ws_prog G \<Longrightarrow> wf ((subcls1 G)\<inverse>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   621
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
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 subint1_induct: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
  "\<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
   626
apply (frule wf_subint1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
apply (erule wf_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
apply (simp (no_asm_use) only: converse_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
lemma subcls1_induct [consumes 1]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
  "\<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
   634
apply (frule wf_subcls1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
apply (erule wf_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
apply (simp (no_asm_use) only: converse_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   637
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   639
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
lemma ws_subint1_induct: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
 "\<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
   642
   (\<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
   643
  \<rbrakk> \<Longrightarrow> P I"
24038
18182c4aec9e replaced make_imp by rev_mp;
wenzelm
parents: 18576
diff changeset
   644
apply (erule rev_mp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   645
apply (rule subint1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   646
apply  assumption
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 17778
diff changeset
   647
apply (simp (no_asm)) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   648
apply safe
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 17778
diff changeset
   649
apply (blast dest: subint1I ws_prog_ideclD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   651
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
lemma ws_subcls1_induct: "\<lbrakk>is_class G C; ws_prog G;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
  \<And>C c. \<lbrakk>class G C = Some c;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
 (C \<noteq> Object \<longrightarrow> (C,(super c))\<in>subcls1 G \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
                  P (super c) \<and> is_class G (super c))\<rbrakk> \<Longrightarrow> P C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
 \<rbrakk> \<Longrightarrow> P C"
24038
18182c4aec9e replaced make_imp by rev_mp;
wenzelm
parents: 18576
diff changeset
   658
apply (erule rev_mp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
apply (rule subcls1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
apply  assumption
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 17778
diff changeset
   661
apply (simp (no_asm)) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
apply (fast dest: subcls1I ws_prog_cdeclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
lemma ws_class_induct [consumes 2, case_names Object Subcls]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
"\<lbrakk>class G C = Some c; ws_prog G; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   668
  \<And> co. class G Object = Some co \<Longrightarrow> P Object; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
  \<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
   670
 \<rbrakk> \<Longrightarrow> P C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   672
  assume clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   673
  and    init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   674
  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
   675
  assume ws: "ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
  then have "is_class G C \<Longrightarrow> P C"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   677
  proof (induct rule: subcls1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
    fix C
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   679
    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
   680
       and iscls:"is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   681
    show "P C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   682
    proof (cases "C=Object")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   683
      case True with iscls init show "P C" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   684
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   685
      case False with ws step hyp iscls 
18576
8d98b7711e47 Reversed Larry's option/iff change.
nipkow
parents: 18551
diff changeset
   686
      show "P C" by (auto dest: subcls1I ws_prog_cdeclD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   687
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   688
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   689
  with clsC show ?thesis by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   690
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   691
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
lemma ws_class_induct' [consumes 2, case_names Object Subcls]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   693
"\<lbrakk>is_class G C; ws_prog G; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   694
  \<And> co. class G Object = Some co \<Longrightarrow> P Object; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   695
  \<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
   696
 \<rbrakk> \<Longrightarrow> P C"
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 17778
diff changeset
   697
by (auto intro: ws_class_induct)
12854
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>class G C = Some c; ws_prog G; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   701
  \<And> co. class G Object = Some co \<Longrightarrow> P Object co; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   702
  \<And>  C c sc. \<lbrakk>class G C = Some c; class G (super c) = Some sc;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   703
            C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   704
 \<rbrakk> \<Longrightarrow> P C c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   706
  assume clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   707
  and    init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object co"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   708
  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
   709
                             C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   710
  assume ws: "ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   711
  then have "\<And> c. class G C = Some c\<Longrightarrow> P C c"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   712
  proof (induct rule: subcls1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   713
    fix C c
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   714
    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
   715
       and iscls:"class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   716
    show "P C c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   717
    proof (cases "C=Object")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   718
      case True with iscls init show "P C c" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   719
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   720
      case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   721
      with ws iscls obtain sc where
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   722
        sc: "class G (super c) = Some sc"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   723
        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
   724
      from iscls False have "G\<turnstile>C \<prec>\<^sub>C1 (super c)" by (rule subcls1I)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   725
      with False ws step hyp iscls sc
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   726
      show "P C c" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   727
        by (auto)  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   728
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   729
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   730
  with clsC show "P C c" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   731
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   732
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   733
lemma ws_interface_induct [consumes 2, case_names Step]:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   734
  assumes is_if_I: "is_iface G I" and 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   735
               ws: "ws_prog G" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   736
          hyp_sub: "\<And>I i. \<lbrakk>iface G I = Some i; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   737
                            \<forall> J \<in> set (isuperIfs i).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   738
                                 (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
   739
  shows "P I"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   740
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   741
  from is_if_I ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   742
  show "P I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   743
  proof (rule ws_subint1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   744
    fix I i
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   745
    assume hyp: "iface G I = Some i \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   746
                (\<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
   747
    then have if_I: "iface G I = Some i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   748
      by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   749
    show "P I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   750
    proof (cases "isuperIfs i")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   751
      case Nil
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   752
      with if_I hyp_sub 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   753
      show "P I" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   754
        by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   755
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   756
      case (Cons hd tl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   757
      with hyp if_I hyp_sub 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   758
      show "P I" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   759
        by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   760
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   761
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   762
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   763
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   764
section "general recursion operators for the interface and class hiearchies"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   767
  iface_rec  :: "prog \<times> qtname \<Rightarrow>   \<spacespace>  (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
  class_rec  :: "prog \<times> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a     \<Rightarrow> 'a) \<Rightarrow> 'a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   769
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   770
recdef iface_rec "same_fst ws_prog (\<lambda>G. (subint1 G)^-1)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   771
"iface_rec (G,I) = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   772
  (\<lambda>f. case iface G I of 
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27682
diff changeset
   773
         None \<Rightarrow> undefined 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   774
       | Some i \<Rightarrow> if ws_prog G 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   775
                      then f I i 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   776
                               ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27682
diff changeset
   777
                      else undefined)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   778
(hints recdef_wf: wf_subint1 intro: subint1I)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   779
declare iface_rec.simps [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   780
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   781
lemma iface_rec: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   782
"\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   783
 iface_rec (G,I) f = f I i ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   784
apply (subst iface_rec.simps)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   785
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   786
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   787
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   788
recdef class_rec "same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   789
"class_rec(G,C) = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   790
  (\<lambda>t f. case class G C of 
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27682
diff changeset
   791
           None \<Rightarrow> undefined 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   792
         | Some c \<Rightarrow> if ws_prog G 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   793
                        then f C c 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   794
                                 (if C = Object then t 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   795
                                                else class_rec (G,super c) t f)
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27682
diff changeset
   796
                        else undefined)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   797
(hints recdef_wf: wf_subcls1 intro: subcls1I)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   798
declare class_rec.simps [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   799
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   800
lemma class_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   801
 class_rec (G,C) t f = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   802
   f C c (if C = Object then t else class_rec (G,super c) t f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   804
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   805
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   806
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35315
diff changeset
   807
definition 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
   808
  --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   809
"imethds G I 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   810
  \<equiv> iface_rec (G,I)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   811
              (\<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
   812
                        (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
   813
        
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   814
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   815
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   816
end