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