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