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