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