src/HOL/Bali/Decl.thy
author schirmer
Thu, 31 Oct 2002 18:27:10 +0100
changeset 13688 a0b16d42d489
parent 13601 fd3e3d6b37b2
child 14171 0cab06e3bbd0
permissions -rw-r--r--
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
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
12858
wenzelm
parents: 12857
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Field, method, interface, and class declarations, whole Java programs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
(** order is significant, because of clash for "var" **)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
theory Decl = Term + Table:
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
 
12859
wenzelm
parents: 12858
diff changeset
    54
instance acc_modi:: ord ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
less_acc_def: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
 "a < (b::acc_modi) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
      \<equiv> (case a of
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
le_acc_def:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
 "a \<le> (b::acc_modi) \<equiv> (a = b) \<or> (a < b)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
instance acc_modi:: order
12859
wenzelm
parents: 12858
diff changeset
    68
proof
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
  fix x y z::acc_modi
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
  {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
  show "x \<le> x"               \<spacespace>\<spacespace>    -- reflexivity
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
    by (auto simp add: le_acc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
  assume "x \<le> y" "y \<le> z"           -- transitivity 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
  thus "x \<le> z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
  assume "x \<le> y" "y \<le> x"           -- antisymmetry
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
  thus "x = y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
  proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
    have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
      by (auto simp add: less_acc_def split add: acc_modi.split)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
    with prems show ?thesis
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 12937
diff changeset
    84
      by (unfold le_acc_def) rules
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
  show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
    by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
  }
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
instance acc_modi:: linorder
12859
wenzelm
parents: 12858
diff changeset
    93
proof
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
  fix x y:: acc_modi
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
  show  "x \<le> y \<or> y \<le> x"   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
  by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
lemma acc_modi_top [simp]: "Public \<le> a \<Longrightarrow> a = Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
lemma acc_modi_top1 [simp, intro!]: "a \<le> Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
lemma acc_modi_le_Public: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
"a \<le> Public \<Longrightarrow> a=Private \<or> a = Package \<or> a=Protected \<or> a=Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
lemma acc_modi_bottom: "a \<le> Private \<Longrightarrow> a = Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
lemma acc_modi_Private_le: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
"Private \<le> a \<Longrightarrow> a=Private \<or> a = Package \<or> a=Protected \<or> a=Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
lemma acc_modi_Package_le: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
  "Package \<le> a \<Longrightarrow> a = Package \<or> a=Protected \<or> a=Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
lemma acc_modi_le_Package: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
  "a \<le> Package \<Longrightarrow> a=Private \<or> a = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
lemma acc_modi_Protected_le: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
  "Protected \<le> a \<Longrightarrow> a=Protected \<or> a=Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
lemma acc_modi_le_Protected: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
  "a \<le> Protected  \<Longrightarrow> a=Private \<or> a = Package \<or> a = Protected"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
lemmas acc_modi_le_Dests = acc_modi_top           acc_modi_le_Public
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
                           acc_modi_Private_le    acc_modi_bottom
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
                           acc_modi_Package_le    acc_modi_le_Package
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
                           acc_modi_Protected_le  acc_modi_le_Protected
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
lemma acc_modi_Package_le_cases 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
 [consumes 1,case_names Package Protected Public]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
 "Package \<le> m \<Longrightarrow> ( m = Package \<Longrightarrow> P m) \<Longrightarrow> (m=Protected \<Longrightarrow> P m) \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
   (m=Public \<Longrightarrow> P m) \<Longrightarrow> P m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
by (auto dest: acc_modi_Package_le)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
subsubsection {* Static Modifier *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
types stat_modi = bool (* modifier: static *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
subsection {* Declaration (base "class" for member,interface and class
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
 declarations *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
record decl =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
        access :: acc_modi
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
  "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
  "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
subsection {* Member (field or method)*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
record  member = decl +
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
         static :: stat_modi
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
  "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
  "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
subsection {* Field *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
record field = member +
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
        type :: ty
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
  "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
  "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
types     
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
        fdecl           (* field declaration, cf. 8.3 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
	= "vname \<times> field"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
  "fdecl" <= (type) "vname \<times> field"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
subsection  {* Method *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
record mhead = member +     (* method head (excluding signature) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
        pars ::"vname list" (* parameter names *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
        resT ::ty           (* result type *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
record mbody =                      (* method body *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
        lcls::  "(vname \<times> ty) list" (* local variables *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
        stmt:: stmt                 (* the body statement *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
record methd = mhead + (* method in a class *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
        mbody::mbody
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
types mdecl = "sig \<times> methd"  (* method declaration in a class *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
translations
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\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
  "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
                      pars::vname list, resT::ty,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
  "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
  "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<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\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
  "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
                      pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
  "mdecl" <= (type) "sig \<times> methd"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
constdefs 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
  mhead::"methd \<Rightarrow> mhead"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
  "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
   215
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
lemma access_mhead [simp]:"access (mhead m) = access m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
lemma static_mhead [simp]:"static (mhead m) = static m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
lemma pars_mhead [simp]:"pars (mhead m) = pars m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
lemma resT_mhead [simp]:"resT (mhead m) = resT m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
by (simp add: mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
text {* To be able to talk uniformaly about field and method declarations we
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
introduce the notion of a member declaration (e.g. useful to define 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
accessiblity ) *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
datatype memberdecl = fdecl fdecl | mdecl mdecl
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
datatype memberid = fid vname | mid sig
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
axclass has_memberid < "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
 memberid :: "'a::has_memberid \<Rightarrow> memberid"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
12859
wenzelm
parents: 12858
diff changeset
   240
instance memberdecl::has_memberid ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
memberdecl_memberid_def:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
  "memberid m \<equiv> (case m of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
                    fdecl (vn,f)  \<Rightarrow> fid vn
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
                  | mdecl (sig,m) \<Rightarrow> mid sig)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
by (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
lemma memberid_fdecl_simp1: "memberid (fdecl f) = fid (fst f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
by (cases f) (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
lemma memberid_mdecl_simp[simp]: "memberid (mdecl (sig,m)) = mid sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
by (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
by (cases m) (simp add: memberdecl_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
12859
wenzelm
parents: 12858
diff changeset
   260
instance * :: (type, has_memberid) has_memberid ..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
defs (overloaded)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
pair_memberid_def:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
  "memberid p \<equiv> memberid (snd p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
by (simp add: pair_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
lemma memberid_pair_simp1: "memberid p  = memberid (snd p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
by (simp add: pair_memberid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
constdefs is_field :: "qtname \<times> memberdecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
"is_field m \<equiv> \<exists> declC f. m=(declC,fdecl f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
by (simp add: is_field_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
lemma is_fieldI: "is_field (C,fdecl f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
by (simp add: is_field_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
constdefs is_method :: "qtname \<times> memberdecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
"is_method membr \<equiv> \<exists> declC m. membr=(declC,mdecl m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
by (simp add: is_method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
lemma is_methodI: "is_method (C,mdecl m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
by (simp add: is_method_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
subsection {* Interface *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
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
   294
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
   295
          imethods :: "(sig \<times> mhead) list" --{* method heads *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
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
   297
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
   298
         isuperIfs:: "qtname list" --{* superinterface list *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
types	
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
   300
	idecl           --{* interface declaration, cf. 9.1 *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
	= "qtname \<times> iface"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
  "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
  "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<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\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
  "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
                      isuperIfs::qtname list,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
  "idecl" <= (type) "qtname \<times> iface"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
  ibody :: "iface \<Rightarrow> ibody"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
  "ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
lemma access_ibody [simp]: "(access (ibody i)) = access i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
by (simp add: ibody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
lemma imethods_ibody [simp]: "(imethods (ibody i)) = imethods i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
by (simp add: ibody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
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
   323
record cbody = decl +          --{* class body *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
         cfields:: "fdecl list" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
         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
   326
         init   :: "stmt"       --{* initializer *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
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
   328
record class = cbody +           --{* class *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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
   329
        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
   330
        superIfs:: "qtname list" --{* implemented interfaces *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
types	
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
   332
	cdecl           --{* class declaration, cf. 8.1 *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
	= "qtname \<times> class"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
translations
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\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
  "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
                      methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
  "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
                      methods::mdecl list,init::stmt,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
                      super::qtname,superIfs::qtname list\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
  "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
                      methods::mdecl list,init::stmt,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
                      super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
  "cdecl" <= (type) "qtname \<times> class"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
  cbody :: "class \<Rightarrow> cbody"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
  "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
   351
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
lemma access_cbody [simp]:"access (cbody c) = access c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
lemma cfields_cbody [simp]:"cfields (cbody c) = cfields c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
lemma methods_cbody [simp]:"methods (cbody c) = methods c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
lemma init_cbody [simp]:"init (cbody c) = init c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
by (simp add: cbody_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
section "standard classes"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
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
   369
  Object_mdecls  ::  "mdecl list" --{* methods of Object *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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
  SXcpt_mdecls   ::  "mdecl list" --{* methods of SXcpts *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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
   371
  ObjectC ::         "cdecl"      --{* declaration  of root      class   *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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
   372
  SXcptC  ::"xname \<Rightarrow> cdecl"      --{* declarations of throwable classes *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
defs 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
ObjectC_def:"ObjectC  \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
                                  init=Skip,super=arbitrary,superIfs=[]\<rparr>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
                                   init=Skip,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
                                   super=if xn = Throwable then Object 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
                                                           else SXcpt Throwable,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
                                   superIfs=[]\<rparr>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
lemma ObjectC_neq_SXcptC [simp]: "ObjectC \<noteq> SXcptC xn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
apply (simp add: SXcptC_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
constdefs standard_classes :: "cdecl list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
         "standard_classes \<equiv> [ObjectC, SXcptC Throwable,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
		SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
		SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
section "programs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
record prog =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
        ifaces ::"idecl list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
        "classes"::"cdecl list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
     "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
     "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
  iface     :: "prog  \<Rightarrow> (qtname, iface) table"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
  class     :: "prog  \<Rightarrow> (qtname, class) table"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   412
  is_iface  :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   413
  is_class  :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   414
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   415
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
	   "iface G I" == "table_of (ifaces G) I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
	   "class G C" == "table_of (classes G) C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   418
	"is_iface G I" == "iface G I \<noteq> None"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
	"is_class G C" == "class G C \<noteq> None"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
section "is type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   424
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
  is_type :: "prog \<Rightarrow>     ty \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
  isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
primrec	"is_type G (PrimT pt)  = True"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
	"is_type G (RefT  rt)  = isrtype G rt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
	"isrtype G (NullT    ) = True"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
	"isrtype G (IfaceT tn) = is_iface G tn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
	"isrtype G (ClassT tn) = is_class G tn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
	"isrtype G (ArrayT T ) = is_type  G T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
lemma type_is_class: "is_type G (Class C) \<Longrightarrow>  is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
section "subinterface and subclass relation, in anticipation of TypeRel.thy"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
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
   445
  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
   446
  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass     *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
defs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
  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
   450
  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
   451
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
 "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
 "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
 "@subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
syntax (xsymbols)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
  "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
  "@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
  "@subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
        "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
	"G\<turnstile>C \<preceq>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
        "G\<turnstile>C \<prec>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
lemma subint1I: "\<lbrakk>iface G I = Some i; J \<in> set (isuperIfs i)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
                 \<Longrightarrow> (I,J) \<in> subint1 G" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
apply (simp add: subint1_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
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
   474
apply (simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
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
   479
by (simp add: subint1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
lemma subcls1D: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
  "(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
   483
apply (simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
lemma subint1_def2:  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
   "subint1 G = (\<Sigma> I\<in>{I. is_iface G I}. set (isuperIfs (the (iface G I))))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
apply (unfold subint1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
lemma subcls1_def2: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
 "subcls1 G = (\<Sigma>C\<in>{C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
apply (unfold subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
lemma subcls_is_class:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
"\<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
   501
by (auto simp add: subcls1_def dest: tranclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
lemma no_subcls1_Object:"G\<turnstile>Object\<prec>\<^sub>C\<^sub>1 D \<Longrightarrow> P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
by (auto simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
lemma no_subcls_Object: "G\<turnstile>Object\<prec>\<^sub>C D \<Longrightarrow> P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
apply (erule trancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
apply (auto intro: no_subcls1_Object)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
section "well-structured programs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
  ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
 "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
   516
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
  ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
 "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
   519
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
  ws_prog  :: "prog \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
 "ws_prog G \<equiv> (\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
	      (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
lemma ws_progI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
"\<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
   527
                                                (J,I) \<notin> (subint1 G)^+; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
  \<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
   529
                                        ((super c),C) \<notin> (subcls1 G)^+  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
 \<rbrakk> \<Longrightarrow> ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
apply (unfold ws_prog_def ws_idecl_def ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
apply (erule_tac conjI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
lemma ws_prog_ideclD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
"\<lbrakk>iface G I = Some i; J\<in>set (isuperIfs i); ws_prog G\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
  is_iface G J \<and> (J,I)\<notin>(subint1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
apply (unfold ws_prog_def ws_idecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
apply (drule_tac map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
lemma ws_prog_cdeclD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
"\<lbrakk>class G C = Some c; C\<noteq>Object; ws_prog G\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   547
  is_class G (super c) \<and> (super c,C)\<notin>(subcls1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
apply (unfold ws_prog_def ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   549
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
apply (drule_tac map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   551
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
section "well-foundedness"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
lemma finite_is_iface: "finite {I. is_iface G I}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
apply (fold dom_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
apply (rule_tac finite_dom_map_of)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
lemma finite_is_class: "finite {C. is_class G C}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
apply (fold dom_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
apply (rule_tac finite_dom_map_of)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
lemma finite_subint1: "finite (subint1 G)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
apply (subst subint1_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
apply (rule finite_SigmaI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
apply (rule finite_is_iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
lemma finite_subcls1: "finite (subcls1 G)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
apply (subst subcls1_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
apply (rule finite_SigmaI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
apply (rule finite_is_class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
apply (rule_tac B = "{super (the (class G C))}" in finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
lemma subint1_irrefl_lemma1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
  "ws_prog G \<Longrightarrow> (subint1 G)^-1 \<inter> (subint1 G)^+ = {}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
apply (force dest: subint1D ws_prog_ideclD conjunct2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
lemma subcls1_irrefl_lemma1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
  "ws_prog G \<Longrightarrow> (subcls1 G)^-1 \<inter> (subcls1 G)^+ = {}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
apply (force dest: subcls1D ws_prog_cdeclD conjunct2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
lemmas subint1_irrefl_lemma2 = subint1_irrefl_lemma1 [THEN irrefl_tranclI']
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   594
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
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
   596
apply (rule irrefl_trancl_rD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
apply (rule subint1_irrefl_lemma2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   599
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
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
   602
apply (rule irrefl_trancl_rD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   603
apply (rule subcls1_irrefl_lemma2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   608
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
lemma wf_subint1: "ws_prog G \<Longrightarrow> wf ((subint1 G)\<inverse>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
by (auto intro: finite_acyclic_wf_converse finite_subint1 subint1_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
lemma wf_subcls1: "ws_prog G \<Longrightarrow> wf ((subcls1 G)\<inverse>)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
lemma subint1_induct: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
  "\<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
   620
apply (frule wf_subint1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   621
apply (erule wf_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
apply (simp (no_asm_use) only: converse_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   624
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
lemma subcls1_induct [consumes 1]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
  "\<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
   628
apply (frule wf_subcls1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
apply (erule wf_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
apply (simp (no_asm_use) only: converse_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
lemma ws_subint1_induct: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
 "\<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
   636
   (\<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
   637
  \<rbrakk> \<Longrightarrow> P I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
apply (erule make_imp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   639
apply (rule subint1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
apply  assumption
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   642
apply (fast dest: subint1I ws_prog_ideclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   643
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   644
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   645
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   646
lemma ws_subcls1_induct: "\<lbrakk>is_class G C; ws_prog G;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   647
  \<And>C c. \<lbrakk>class G C = Some c;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   648
 (C \<noteq> Object \<longrightarrow> (C,(super c))\<in>subcls1 G \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   649
                  P (super c) \<and> is_class G (super c))\<rbrakk> \<Longrightarrow> P C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
 \<rbrakk> \<Longrightarrow> P C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   651
apply (erule make_imp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
apply (rule subcls1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
apply  assumption
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
apply (fast dest: subcls1I ws_prog_cdeclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
lemma ws_class_induct [consumes 2, case_names Object Subcls]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
"\<lbrakk>class G C = Some c; ws_prog G; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
  \<And> co. class G Object = Some co \<Longrightarrow> P Object; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   661
  \<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
   662
 \<rbrakk> \<Longrightarrow> P C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
  assume clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
  and    init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
  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
   667
  assume ws: "ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   668
  then have "is_class G C \<Longrightarrow> P C"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
  proof (induct rule: subcls1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   670
    fix C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
    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
   672
       and iscls:"is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   673
    show "P C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   674
    proof (cases "C=Object")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   675
      case True with iscls init show "P C" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   677
      case False with ws step hyp iscls 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
      show "P C" by (auto dest: subcls1I ws_prog_cdeclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   679
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   680
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   681
  with clsC show ?thesis by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   682
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   683
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   684
lemma ws_class_induct' [consumes 2, case_names Object Subcls]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   685
"\<lbrakk>is_class G C; ws_prog G; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   686
  \<And> co. class G Object = Some co \<Longrightarrow> P Object; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   687
  \<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
   688
 \<rbrakk> \<Longrightarrow> P C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   689
by (blast intro: ws_class_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   690
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   691
lemma ws_class_induct'' [consumes 2, case_names Object Subcls]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
"\<lbrakk>class G C = Some c; ws_prog G; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   693
  \<And> co. class G Object = Some co \<Longrightarrow> P Object co; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   694
  \<And>  C c sc. \<lbrakk>class G C = Some c; class G (super c) = Some sc;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   695
            C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   696
 \<rbrakk> \<Longrightarrow> P C c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   697
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   698
  assume clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   699
  and    init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object co"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   700
  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
   701
                             C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   702
  assume ws: "ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   703
  then have "\<And> c. class G C = Some c\<Longrightarrow> P C c"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   704
  proof (induct rule: subcls1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
    fix C c
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   706
    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
   707
       and iscls:"class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   708
    show "P C c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   709
    proof (cases "C=Object")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   710
      case True with iscls init show "P C c" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   711
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   712
      case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   713
      with ws iscls obtain sc where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   714
	sc: "class G (super c) = Some sc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   715
	by (auto dest: ws_prog_cdeclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   716
      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
   717
      with False ws step hyp iscls sc
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   718
      show "P C c" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   719
	by (auto)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   720
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   721
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   722
  with clsC show "P C c" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   723
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   724
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   725
lemma ws_interface_induct [consumes 2, case_names Step]:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   726
  assumes is_if_I: "is_iface G I" and 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   727
               ws: "ws_prog G" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   728
          hyp_sub: "\<And>I i. \<lbrakk>iface G I = Some i; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   729
                            \<forall> J \<in> set (isuperIfs i).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   730
                                 (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
   731
  shows "P I"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   732
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   733
  from is_if_I ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   734
  show "P I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   735
  proof (rule ws_subint1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   736
    fix I i
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   737
    assume hyp: "iface G I = Some i \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   738
                (\<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
   739
    then have if_I: "iface G I = Some i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   740
      by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   741
    show "P I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   742
    proof (cases "isuperIfs i")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   743
      case Nil
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   744
      with if_I hyp_sub 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   745
      show "P I" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   746
	by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   747
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   748
      case (Cons hd tl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   749
      with hyp if_I hyp_sub 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   750
      show "P I" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   751
	by auto
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
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   755
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   756
section "general recursion operators for the interface and class hiearchies"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   757
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   758
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   759
  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
   760
  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
   761
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   762
recdef iface_rec "same_fst ws_prog (\<lambda>G. (subint1 G)^-1)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   763
"iface_rec (G,I) = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   764
  (\<lambda>f. case iface G I of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
         None \<Rightarrow> arbitrary 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
       | Some i \<Rightarrow> if ws_prog G 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   767
                      then f I i 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
                               ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   769
                      else arbitrary)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   770
(hints recdef_wf: wf_subint1 intro: subint1I)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   771
declare iface_rec.simps [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   772
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   773
lemma iface_rec: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   774
"\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   775
 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
   776
apply (subst iface_rec.simps)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   777
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   778
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   779
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   780
recdef class_rec "same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   781
"class_rec(G,C) = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   782
  (\<lambda>t f. case class G C of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   783
           None \<Rightarrow> arbitrary 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   784
         | Some c \<Rightarrow> if ws_prog G 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   785
                        then f C c 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   786
                                 (if C = Object then t 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   787
                                                else class_rec (G,super c) t f)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   788
                        else arbitrary)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   789
(hints recdef_wf: wf_subcls1 intro: subcls1I)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   790
declare class_rec.simps [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   791
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   792
lemma class_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   793
 class_rec (G,C) t f = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   794
   f C c (if C = Object then t else class_rec (G,super c) t f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   795
apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   796
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   797
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   798
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   799
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   800
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
   801
  --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   802
"imethds G I 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
  \<equiv> iface_rec (G,I)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   804
              (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   805
                        (o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   809
end