src/HOL/Bali/TypeRel.thy
author wenzelm
Mon, 25 Feb 2002 20:48:14 +0100
changeset 12937 0c4fd7529467
parent 12858 6214f03d6d27
child 13688 a0b16d42d489
permissions -rw-r--r--
clarified syntax of ``long'' statements: fixes/assumes/shows;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/TypeRel.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
12858
wenzelm
parents: 12857
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* The relations between Java types *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
theory TypeRel = Decl:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
simplifications:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\item subinterface, subclass and widening relation includes identity
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
improvements over Java Specification 1.0:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
\item narrowing reference conversion also in cases where the return types of a 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
      pair of methods common to both types are in widening (rather identity) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
      relation
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
\item one could add similar constraints also for other cases
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
\item the type relations do not require @{text is_type} for their arguments
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
\item the subint1 and subcls1 relations imply @{text is_iface}/@{text is_class}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
      for their first arguments, which is required for their finiteness
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
(*subint1, in Decl.thy*)                     (* direct subinterface       *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
(*subint , by translation*)                  (* subinterface (+ identity) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
(*subcls1, in Decl.thy*)                     (* direct subclass           *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
(*subcls , by translation*)                  (*        subclass           *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
(*subclseq, by translation*)                 (* subclass + identity       *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
  implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" (* direct implementation *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
  implmt    :: "prog \<Rightarrow> (qtname \<times> qtname) set" (*        implementation *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
  widen     :: "prog \<Rightarrow> (ty    \<times> ty   ) set" (*        widening       *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
  narrow    :: "prog \<Rightarrow> (ty    \<times> ty   ) set" (*        narrowing      *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
  cast     :: "prog \<Rightarrow> (ty    \<times> ty   ) set"  (*        casting        *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
 "@subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
 "@subint"  :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
 (* Defined in Decl.thy:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
 "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
 "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
 "@subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
 "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
 "@implmt"  :: "prog => [qtname, qtname] => bool" ("_|-_~>_"   [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
 "@widen"   :: "prog => [ty   , ty   ] => bool" ("_|-_<=:_"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
 "@narrow"  :: "prog => [ty   , ty   ] => bool" ("_|-_:>_"   [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
 "@cast"    :: "prog => [ty   , ty   ] => bool" ("_|-_<=:? _"[71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
syntax (symbols)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
  "@subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
  "@subint"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
  (* Defined in Decl.thy:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
\  "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
  "@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
  "@subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
  *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
  "@implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
  "@implmt"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_"   [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
  "@widen"   :: "prog \<Rightarrow> [ty   , ty   ] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_"    [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
  "@narrow"  :: "prog \<Rightarrow> [ty   , ty   ] \<Rightarrow> bool" ("_\<turnstile>_\<succ>_"    [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
  "@cast"    :: "prog \<Rightarrow> [ty   , ty   ] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _"  [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
	"G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
	"G\<turnstile>I \<preceq>I  J" == "(I,J) \<in>(subint1 G)^*" (* cf. 9.1.3 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
  	(* Defined in Decl.thy:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
        "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
	"G\<turnstile>C \<preceq>\<^sub>C  D" == "(C,D) \<in>(subcls1 G)^*" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
	*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
        "G\<turnstile>C \<leadsto>1 I" == "(C,I) \<in> implmt1 G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
	"G\<turnstile>C \<leadsto>  I" == "(C,I) \<in> implmt  G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
	"G\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
	"G\<turnstile>S \<succ>   T" == "(S,T) \<in> narrow  G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
	"G\<turnstile>S \<preceq>?  T" == "(S,T) \<in> cast    G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
section "subclass and subinterface relations"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
  (* direct subinterface in Decl.thy, cf. 9.1.3 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
  (* direct subclass     in Decl.thy, cf. 8.1.3 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
lemma subcls_direct1:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
 "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
apply (auto dest: subcls_direct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
lemma subcls1I1:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
 "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C\<^sub>1 D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
apply (auto dest: subcls1I)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
lemma subcls_direct2:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
 "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
apply (auto dest: subcls1I1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
lemma subclseq_trans: "\<lbrakk>G\<turnstile>A \<preceq>\<^sub>C B; G\<turnstile>B \<preceq>\<^sub>C C\<rbrakk> \<Longrightarrow> G\<turnstile>A \<preceq>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
by (blast intro: rtrancl_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
lemma subcls_trans: "\<lbrakk>G\<turnstile>A \<prec>\<^sub>C B; G\<turnstile>B \<prec>\<^sub>C C\<rbrakk> \<Longrightarrow> G\<turnstile>A \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
by (blast intro: trancl_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
lemma SXcpt_subcls_Throwable_lemma: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
"\<lbrakk>class G (SXcpt xn) = Some xc;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
  super xc = (if xn = Throwable then Object else  SXcpt Throwable)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
\<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
apply (case_tac "xn = Throwable")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
apply  simp_all
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
apply (drule subcls_direct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
apply (auto dest: sym)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
lemma subcls_ObjectI: "\<lbrakk>is_class G C; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
apply (erule ws_subcls1_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
apply (case_tac "C = Object")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
apply  (fast intro: r_into_rtrancl [THEN rtrancl_trans])+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
lemma subclseq_ObjectD [dest!]: "G\<turnstile>Object\<preceq>\<^sub>C C \<Longrightarrow> C = Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
apply (erule rtrancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
apply  (auto dest: subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
lemma subcls_ObjectD [dest!]: "G\<turnstile>Object\<prec>\<^sub>C C \<Longrightarrow> False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
apply (erule trancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
apply  (auto dest: subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
lemma subcls_ObjectI1 [intro!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
 "\<lbrakk>C \<noteq> Object;is_class G C;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C \<prec>\<^sub>C Object" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
apply (drule (1) subcls_ObjectI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
apply (auto intro: rtrancl_into_trancl3)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ \<Longrightarrow> is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
apply (erule trancl_trans_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
apply (auto dest!: subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
lemma subcls_is_class2 [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
 "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
apply (erule rtrancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
apply (drule_tac [2] subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
apply  auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
lemma single_inheritance: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
"\<lbrakk>G\<turnstile>A \<prec>\<^sub>C\<^sub>1 B; G\<turnstile>A \<prec>\<^sub>C\<^sub>1 C\<rbrakk> \<Longrightarrow> B = C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
by (auto simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
lemma subcls_compareable:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
"\<lbrakk>G\<turnstile>A \<preceq>\<^sub>C X; G\<turnstile>A \<preceq>\<^sub>C Y 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
 \<rbrakk> \<Longrightarrow> G\<turnstile>X \<preceq>\<^sub>C Y \<or> G\<turnstile>Y \<preceq>\<^sub>C X"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
by (rule triangle_lemma)  (auto intro: single_inheritance) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
lemma subcls1_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D; ws_prog G \<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
 \<Longrightarrow> C \<noteq> D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
proof 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
  assume ws: "ws_prog G" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
    subcls1: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
     eq_C_D: "C=D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
  from subcls1 obtain c 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
    where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
      neq_C_Object: "C\<noteq>Object" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
              clsC: "class G C = Some c" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
           super_c: "super c = D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
    by (auto simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
  with super_c subcls1 eq_C_D 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
  have subcls_super_c_C: "G\<turnstile>super c \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
    by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
  from ws clsC neq_C_Object 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
  have "\<not> G\<turnstile>super c \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
    by (auto dest: ws_prog_cdeclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
  from this subcls_super_c_C 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
  show "False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
    by (rule notE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
lemma no_subcls_Object: "G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> C \<noteq> Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
by (erule converse_trancl_induct) (auto dest: subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
lemma subcls_acyclic: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk> \<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
  assume         ws: "ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
  assume subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
  then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
  proof (induct rule: converse_trancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
    fix C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
    assume subcls1_C_D: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
    then obtain c  where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
        "C\<noteq>Object" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
        "class G C = Some c" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
        "super c = D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
      by (auto simp add: subcls1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
    with ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
    show "\<not> G\<turnstile>D \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
      by (auto dest: ws_prog_cdeclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
    fix C Z
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
    assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 Z" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
            subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
           nsubcls_D_Z: "\<not> G\<turnstile>D \<prec>\<^sub>C Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
    show "\<not> G\<turnstile>D \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
    proof
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
      assume subcls_D_C: "G\<turnstile>D \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
      show "False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
      proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
	from subcls_D_C subcls1_C_Z
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
	have "G\<turnstile>D \<prec>\<^sub>C Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
	  by (auto dest: r_into_trancl trancl_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
	with nsubcls_D_Z
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
	show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
	  by (rule notE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
  qed  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
lemma subclseq_cases [consumes 1, case_names Eq Subcls]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
 "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C = D \<Longrightarrow> P; G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
by (blast intro: rtrancl_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
lemma subclseq_acyclic: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
 "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> \<Longrightarrow> C=D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
by (auto elim: subclseq_cases dest: subcls_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
lemma subcls_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
 \<Longrightarrow> C \<noteq> D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
  assume     ws: "ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
  assume subcls: "G\<turnstile>C \<prec>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
  then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
  proof (induct rule: converse_trancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
    fix C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
    assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
    with ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
    show "C\<noteq>D" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
      by (blast dest: subcls1_irrefl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
    fix C Z
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
    assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 Z" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
            subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
               neq_Z_D: "Z \<noteq> D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
    show "C\<noteq>D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
    proof
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
      assume eq_C_D: "C=D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
      show "False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
      proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
	from subcls1_C_Z eq_C_D 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
	have "G\<turnstile>D \<prec>\<^sub>C Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
	  by (auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
	also
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
	from subcls_Z_D ws   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
	have "\<not> G\<turnstile>D \<prec>\<^sub>C Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
	  by (rule subcls_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
	ultimately 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
	show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
	  by - (rule notE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
lemma invert_subclseq:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; ws_prog G\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
 \<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
  assume       ws: "ws_prog G" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
     subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
  proof (cases "D=C")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
    case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
    with ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
    show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
      by (auto dest: subcls_irrefl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
    case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
    with subclseq_C_D 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
    have "G\<turnstile>C \<prec>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
      by (blast intro: rtrancl_into_trancl3) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
    with ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
    show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
      by (blast dest: subcls_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
lemma invert_subcls:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
 \<Longrightarrow> \<not> G\<turnstile>D \<preceq>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
  assume        ws: "ws_prog G" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
        subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
  then 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
  have nsubcls_D_C: "\<not> G\<turnstile>D \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
    by (blast dest: subcls_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
  proof
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
    assume "G\<turnstile>D \<preceq>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
    then show "False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
    proof (cases rule: subclseq_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
      case Eq
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
      with ws subcls_C_D
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
      show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
	by (auto dest: subcls_irrefl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
      case Subcls
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
      with nsubcls_D_C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
	by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
lemma subcls_superD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
 "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; class G C = Some c\<rbrakk> \<Longrightarrow> G\<turnstile>(super c) \<preceq>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
  assume       clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
  assume subcls_C_C: "G\<turnstile>C \<prec>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
  then obtain S where 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
                  "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
    subclseq_S_D: "G\<turnstile>S \<preceq>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
    by (blast dest: tranclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
  with clsC 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
  have "S=super c" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
    by (auto dest: subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
  with subclseq_S_D show ?thesis by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
lemma subclseq_superD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
 "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C\<noteq>D;class G C = Some c\<rbrakk> \<Longrightarrow> G\<turnstile>(super c) \<preceq>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
  assume neq_C_D: "C\<noteq>D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
  assume    clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
  assume subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
  then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
  proof (cases rule: subclseq_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
    case Eq with neq_C_D show ?thesis by contradiction
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
    case Subcls
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
    with clsC show ?thesis by (blast dest: subcls_superD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
section "implementation relation"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
defs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
  (* direct implementation, cf. 8.1.3 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
implmt1_def:"implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
apply (unfold implmt1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
inductive "implmt G" intros                    (* cf. 8.1.4 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
  direct:         "G\<turnstile>C\<leadsto>1J     \<spacespace>\<spacespace>     \<Longrightarrow> G\<turnstile>C\<leadsto>J"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
  subint:        "\<lbrakk>G\<turnstile>C\<leadsto>1I; G\<turnstile>I\<preceq>I J\<rbrakk>  \<Longrightarrow> G\<turnstile>C\<leadsto>J"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
  subcls1:       "\<lbrakk>G\<turnstile>C\<prec>\<^sub>C\<^sub>1D; G\<turnstile>D\<leadsto>J \<rbrakk>  \<Longrightarrow> G\<turnstile>C\<leadsto>J"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
lemma implmtD: "G\<turnstile>C\<leadsto>J \<Longrightarrow> (\<exists>I. G\<turnstile>C\<leadsto>1I \<and> G\<turnstile>I\<preceq>I J) \<or> (\<exists>D. G\<turnstile>C\<prec>\<^sub>C\<^sub>1D \<and> G\<turnstile>D\<leadsto>J)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
apply (erule implmt.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
apply fast+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
lemma implmt_ObjectE [elim!]: "G\<turnstile>Object\<leadsto>I \<Longrightarrow> R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
by (auto dest!: implmtD implmt1D subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
lemma subcls_implmt [rule_format (no_asm)]: "G\<turnstile>A\<preceq>\<^sub>C B \<Longrightarrow> G\<turnstile>B\<leadsto>K \<longrightarrow> G\<turnstile>A\<leadsto>K"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
apply (erule rtrancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
apply  (auto intro: implmt.subcls1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
lemma implmt_subint2: "\<lbrakk> G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K\<rbrakk> \<Longrightarrow> G\<turnstile>A\<leadsto>K"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
apply (erule make_imp, erule implmt.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
apply (erule implmt.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
apply (blast dest: implmt1D subcls1D)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
section "widening relation"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
inductive "widen G" intros(*widening, viz. method invocation conversion, cf. 5.3
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
			    i.e. kind of syntactic subtyping *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
  refl:    "G\<turnstile>T\<preceq>T"(*identity conversion, cf. 5.1.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
  subint:  "G\<turnstile>I\<preceq>I J  \<Longrightarrow> G\<turnstile>Iface I\<preceq> Iface J"(*wid.ref.conv.,cf. 5.1.4 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
  int_obj: "G\<turnstile>Iface I\<preceq> Class Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
  subcls:  "G\<turnstile>C\<preceq>\<^sub>C D  \<Longrightarrow> G\<turnstile>Class C\<preceq> Class D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
  implmt:  "G\<turnstile>C\<leadsto>I   \<Longrightarrow> G\<turnstile>Class C\<preceq> Iface I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
  null:    "G\<turnstile>NT\<preceq> RefT R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
  arr_obj: "G\<turnstile>T.[]\<preceq> Class Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   412
  array:   "G\<turnstile>RefT S\<preceq>RefT T \<Longrightarrow> G\<turnstile>RefT S.[]\<preceq> RefT T.[]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   413
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   414
declare widen.refl [intro!]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   415
declare widen.intros [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
(* too strong in general:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   418
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> (\<exists>y. T = PrimT y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   424
(* too strong in general:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> \<exists>y. S = PrimT y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>D. S = Class D)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
apply (ind_cases "G\<turnstile>S\<preceq>T")
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
lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J \<Longrightarrow> G\<turnstile>I\<preceq>I J"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
apply (rule iffI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
apply  (erule widen_Iface_Iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
apply (erule widen.subint)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
lemma widen_Class: "G\<turnstile>Class C\<preceq>T \<Longrightarrow>  (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
lemma widen_Class2: "G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>D. S = Class D)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C cm"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>\<^sub>C cm"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
apply (rule iffI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
apply  (erule widen_Class_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
apply (erule widen.subcls)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I \<Longrightarrow> G\<turnstile>C\<leadsto>I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
apply (rule iffI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
apply  (erule widen_Class_Iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
apply (erule widen.implmt)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
lemma widen_Array: "G\<turnstile>S.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
lemma widen_ArrayRefT: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
  "G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
lemma widen_ArrayRefT_ArrayRefT_eq [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
  "G\<turnstile>RefT T.[]\<preceq>RefT T'.[] = G\<turnstile>RefT T\<preceq>RefT T'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
apply (rule iffI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
apply (drule widen_ArrayRefT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
apply (erule widen.array)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
lemma widen_Array_Array: "G\<turnstile>T.[]\<preceq>T'.[] \<Longrightarrow> G\<turnstile>T\<preceq>T'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
apply (drule widen_Array)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
lemma widen_Array_Class: "G\<turnstile>S.[] \<preceq> Class C \<Longrightarrow> C=Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
by (auto dest: widen_Array)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
qed_typerel "widen_NT2" "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
 [prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> T = NT \<longrightarrow> S = NT"]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
apply (ind_cases "G\<turnstile>S\<preceq>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   527
lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
apply (case_tac T)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
apply (auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
apply (subgoal_tac "G\<turnstile>pid_field_type\<preceq>\<^sub>C Object")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
apply (auto intro: subcls_ObjectI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
lemma widen_trans_lemma [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
  "\<lbrakk>G\<turnstile>S\<preceq>U; \<forall>C. is_class G C \<longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object\<rbrakk> \<Longrightarrow> \<forall>T. G\<turnstile>U\<preceq>T \<longrightarrow> G\<turnstile>S\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
apply (erule widen.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
apply        safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
prefer      5 apply (drule widen_RefT) apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
apply      (frule_tac [1] widen_Iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
apply      (frule_tac [2] widen_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
apply      (frule_tac [3] widen_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
apply      (frule_tac [4] widen_Iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
apply      (frule_tac [5] widen_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
apply      (frule_tac [6] widen_Array)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
apply      safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
apply            (rule widen.int_obj)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   547
prefer          6 apply (drule implmt_is_class) apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
apply (tactic "ALLGOALS (etac thin_rl)")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   549
prefer         6 apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
apply          (rule_tac [9] widen.arr_obj)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   551
apply         (rotate_tac [9] -1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
apply         (frule_tac [9] widen_RefT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
apply         (auto elim!: rtrancl_trans subcls_implmt implmt_subint2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
lemma ws_widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
by (auto intro: widen_trans_lemma subcls_ObjectI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
lemma widen_antisym_lemma [rule_format (no_asm)]: "\<lbrakk>G\<turnstile>S\<preceq>T;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
 \<forall>I J. G\<turnstile>I\<preceq>I J \<and> G\<turnstile>J\<preceq>I I \<longrightarrow> I = J;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
 \<forall>C D. G\<turnstile>C\<preceq>\<^sub>C D \<and> G\<turnstile>D\<preceq>\<^sub>C C \<longrightarrow> C = D;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
 \<forall>I  . G\<turnstile>Object\<leadsto>I        \<longrightarrow> False\<rbrakk> \<Longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
apply (erule widen.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
apply (auto dest: widen_Iface widen_NT2 widen_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
lemmas subint_antisym = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
       subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
lemmas subcls_antisym = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
       subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
                                   subcls_antisym [THEN antisymD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
lemma widen_ObjectD [dest!]: "G\<turnstile>Class Object\<preceq>T \<Longrightarrow> T=Class Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
apply (frule widen_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
apply (fast dest: widen_Class_Class widen_Class_Iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
  widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
 "G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
apply (unfold widens_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
lemma widens_Cons [simp]: "G\<turnstile>(S#Ss)[\<preceq>](T#Ts) = (G\<turnstile>S\<preceq>T \<and> G\<turnstile>Ss[\<preceq>]Ts)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
apply (unfold widens_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   594
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   596
section "narrowing relation"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
(* all properties of narrowing and casting conversions we actually need *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   599
(* these can easily be proven from the definitions below *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
rules
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   602
  cast_RefT2   "G\<turnstile>S\<preceq>? RefT R   \<Longrightarrow> \<exists>t. S=RefT t" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   603
  cast_PrimT2  "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
(* more detailed than necessary for type-safety, see above rules. *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
inductive "narrow G" intros (* narrowing reference conversion, cf. 5.1.5 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   608
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
  subcls:  "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile>     Class D\<succ>Class C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
  implmt:  "\<not>G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile>     Class C\<succ>Iface I"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
  obj_arr: "G\<turnstile>Class Object\<succ>T.[]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
  int_cls: "G\<turnstile>     Iface I\<succ>Class C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
  subint:  "imethds G I hidings imethds G J entails 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
	   (\<lambda>(md, mh   ) (md',mh').\<spacespace>G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
	   \<not>G\<turnstile>I\<preceq>I J         \<spacespace>\<spacespace>\<spacespace>\<Longrightarrow> G\<turnstile>     Iface I\<succ>Iface J"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
  array:   "G\<turnstile>RefT S\<succ>RefT T   \<spacespace>\<Longrightarrow> G\<turnstile>   RefT S.[]\<succ>RefT T.[]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
(*unused*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   620
apply (ind_cases "G\<turnstile>S\<succ>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   621
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   624
apply (ind_cases "G\<turnstile>S\<succ>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
(*unused*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
apply (ind_cases "G\<turnstile>S\<succ>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
				  \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
apply (ind_cases "G\<turnstile>S\<succ>T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   637
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
section "casting relation"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   639
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
inductive "cast G" intros (* casting conversion, cf. 5.5 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   642
  widen:   "G\<turnstile>S\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   643
  narrow:  "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   644
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   645
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   646
lemma ??unknown??: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>S\<succ>T\<rbrakk> \<Longrightarrow> R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   647
 deferred *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   648
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   649
(*unused*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   651
apply (ind_cases "G\<turnstile>S\<preceq>? T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
by (auto dest: widen_RefT narrow_RefT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
apply (ind_cases "G\<turnstile>S\<preceq>? T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
by (auto dest: widen_RefT2 narrow_RefT2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
(*unused*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
apply (ind_cases "G\<turnstile>S\<preceq>? T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   661
by (auto dest: widen_PrimT narrow_PrimT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
apply (ind_cases "G\<turnstile>S\<preceq>? T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
by (auto dest: widen_PrimT2 narrow_PrimT2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
end