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