src/HOL/Bali/TypeRel.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47176 568fdc70e565
child 58887 38db8ddc0f57
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/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
47176
568fdc70e565 simplified statements and proofs;
wenzelm
parents: 46212
diff changeset
   203
lemma subclseq_cases:
568fdc70e565 simplified statements and proofs;
wenzelm
parents: 46212
diff changeset
   204
  assumes "G\<turnstile>C \<preceq>\<^sub>C D"
568fdc70e565 simplified statements and proofs;
wenzelm
parents: 46212
diff changeset
   205
  obtains (Eq) "C = D" | (Subcls) "G\<turnstile>C \<prec>\<^sub>C D"
568fdc70e565 simplified statements and proofs;
wenzelm
parents: 46212
diff changeset
   206
using assms by (blast intro: rtrancl_cases)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
lemma subclseq_acyclic: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
 "\<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
   210
by (auto elim: subclseq_cases dest: subcls_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
lemma subcls_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
 \<Longrightarrow> C \<noteq> D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
  assume     ws: "ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
  assume subcls: "G\<turnstile>C \<prec>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
  then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
  proof (induct rule: converse_trancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
    fix C
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35069
diff changeset
   220
    assume "G\<turnstile>C \<prec>\<^sub>C1 D"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
    with ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
    show "C\<noteq>D" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
      by (blast dest: subcls1_irrefl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
    fix C Z
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35069
diff changeset
   226
    assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C1 Z" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
            subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
               neq_Z_D: "Z \<noteq> D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
    show "C\<noteq>D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
    proof
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
      assume eq_C_D: "C=D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
      show "False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
   234
        from subcls1_C_Z eq_C_D 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
   235
        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
   236
          by (auto)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
   237
        also
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
   238
        from subcls_Z_D ws   
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
   239
        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
   240
          by (rule subcls_acyclic)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
   241
        ultimately 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
   242
        show ?thesis 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
   243
          by - (rule notE)
12854
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
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
lemma invert_subclseq:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; ws_prog G\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
 \<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
  assume       ws: "ws_prog G" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
     subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
  proof (cases "D=C")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
    case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
    with ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
    show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
      by (auto dest: subcls_irrefl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
    case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
    with subclseq_C_D 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
    have "G\<turnstile>C \<prec>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
      by (blast intro: rtrancl_into_trancl3) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
    with ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
    show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
      by (blast dest: subcls_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
lemma invert_subcls:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
 \<Longrightarrow> \<not> G\<turnstile>D \<preceq>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
  assume        ws: "ws_prog G" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
        subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
  then 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
  have nsubcls_D_C: "\<not> G\<turnstile>D \<prec>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
    by (blast dest: subcls_acyclic)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
  proof
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
    assume "G\<turnstile>D \<preceq>\<^sub>C C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
    then show "False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
    proof (cases rule: subclseq_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
      case Eq
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
      with ws subcls_C_D
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
      show ?thesis 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
   289
        by (auto dest: subcls_irrefl)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
      case Subcls
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
      with nsubcls_D_C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24783
diff changeset
   294
        by blast
12854
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
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
lemma subcls_superD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
 "\<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
   301
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
  assume       clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
  assume subcls_C_C: "G\<turnstile>C \<prec>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
  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
   305
                  "G\<turnstile>C \<prec>\<^sub>C1 S" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
    subclseq_S_D: "G\<turnstile>S \<preceq>\<^sub>C D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
    by (blast dest: tranclD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
  with clsC 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
  have "S=super c" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
    by (auto dest: subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
  with subclseq_S_D show ?thesis by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
lemma subclseq_superD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
 "\<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
   317
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
  assume neq_C_D: "C\<noteq>D"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
  assume    clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
  assume subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
  then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
  proof (cases rule: subclseq_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
    case Eq with neq_C_D show ?thesis by contradiction
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
    case Subcls
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
    with clsC show ?thesis by (blast dest: subcls_superD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
section "implementation relation"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
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
   333
apply (unfold implmt1_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   337
inductive --{* implementation, cf. 8.1.4 *}
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   338
  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
   339
  for G :: prog
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   340
where
46212
d86ef6b96097 tuned white space;
wenzelm
parents: 45605
diff changeset
   341
  direct: "G\<turnstile>C\<leadsto>1J \<Longrightarrow> G\<turnstile>C\<leadsto>J"
d86ef6b96097 tuned white space;
wenzelm
parents: 45605
diff changeset
   342
| 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
   343
| 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
   344
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35069
diff changeset
   345
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
   346
apply (erule implmt.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
apply fast+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
lemma implmt_ObjectE [elim!]: "G\<turnstile>Object\<leadsto>I \<Longrightarrow> R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
by (auto dest!: implmtD implmt1D subcls1D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
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
   354
apply (erule rtrancl_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
apply  (auto intro: implmt.subcls1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
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
   359
apply (erule rev_mp, erule implmt.induct)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
apply (erule implmt.induct)
18447
da548623916a removed or modified some instances of [iff]
paulson
parents: 16417
diff changeset
   365
apply (auto dest: implmt1D subcls1D)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
section "widening relation"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   371
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
   372
 --{*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
   373
                            i.e. kind of syntactic subtyping *}
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   374
  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
   375
  for G :: prog
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   376
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
   377
  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
   378
| 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
   379
| int_obj: "G\<turnstile>Iface I\<preceq> Class Object"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   380
| 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
   381
| 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
   382
| null:    "G\<turnstile>NT\<preceq> RefT R"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   383
| arr_obj: "G\<turnstile>T.[]\<preceq> Class Object"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   384
| 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
   385
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
declare widen.refl [intro!]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
declare widen.intros [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
(* too strong in general:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
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
   393
apply (ind_cases "G\<turnstile>PrimT x\<preceq>T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
(* too strong in general:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
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
   400
apply (ind_cases "G\<turnstile>S\<preceq>PrimT x")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
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
   403
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
   404
   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
   405
   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
   406
   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
   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
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12858
diff changeset
   409
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
   410
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
   411
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
   412
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
   413
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
   414
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
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
   416
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12858
diff changeset
   417
lemma widen_Boolean: "G\<turnstile>PrimT Boolean\<preceq>T \<Longrightarrow> T = PrimT Boolean"
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   418
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
   419
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
   420
lemma widen_Boolean2: "G\<turnstile>S\<preceq>PrimT Boolean \<Longrightarrow> S = PrimT Boolean"
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   421
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
   422
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
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
   424
apply (ind_cases "G\<turnstile>RefT R\<preceq>T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
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
   428
apply (ind_cases "G\<turnstile>S\<preceq>RefT R")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
lemma widen_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
   432
apply (ind_cases "G\<turnstile>Iface I\<preceq>T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
lemma widen_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
   436
apply (ind_cases "G\<turnstile>S\<preceq> Iface J")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
lemma widen_Iface_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
   440
apply (ind_cases "G\<turnstile>Iface I\<preceq> Iface J")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
lemma widen_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
   444
apply (rule iffI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
apply  (erule widen_Iface_Iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
apply (erule widen.subint)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
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
   450
apply (ind_cases "G\<turnstile>Class C\<preceq>T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
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
   454
apply (ind_cases "G\<turnstile>S\<preceq> Class C")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
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
   458
apply (ind_cases "G\<turnstile>Class C\<preceq> Class cm")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
lemma widen_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
   462
apply (rule iffI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
apply  (erule widen_Class_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
apply (erule widen.subcls)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
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
   468
apply (ind_cases "G\<turnstile>Class C\<preceq> Iface I")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
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
   472
apply (rule iffI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
apply  (erule widen_Class_Iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
apply (erule widen.implmt)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
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
   478
apply (ind_cases "G\<turnstile>S.[]\<preceq>T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
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
   482
apply (ind_cases "G\<turnstile>S\<preceq>T.[]")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
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
   487
apply (ind_cases "G\<turnstile>PrimT t.[]\<preceq>T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
lemma widen_ArrayRefT: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
  "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
   492
apply (ind_cases "G\<turnstile>RefT t.[]\<preceq>T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
lemma widen_ArrayRefT_ArrayRefT_eq [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
  "G\<turnstile>RefT T.[]\<preceq>RefT T'.[] = G\<turnstile>RefT T\<preceq>RefT T'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
apply (rule iffI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
apply (drule widen_ArrayRefT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
apply (erule widen.array)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
lemma widen_Array_Array: "G\<turnstile>T.[]\<preceq>T'.[] \<Longrightarrow> G\<turnstile>T\<preceq>T'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
apply (drule widen_Array)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
lemma widen_Array_Class: "G\<turnstile>S.[] \<preceq> Class C \<Longrightarrow> C=Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
by (auto dest: widen_Array)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
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
   511
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   513
apply (ind_cases "G\<turnstile>S\<preceq>NT")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
38541
9cfafdb56749 robustified proof
haftmann
parents: 37956
diff changeset
   516
lemma widen_Object:
9cfafdb56749 robustified proof
haftmann
parents: 37956
diff changeset
   517
  assumes "isrtype G T" and "ws_prog G"
9cfafdb56749 robustified proof
haftmann
parents: 37956
diff changeset
   518
  shows "G\<turnstile>RefT T \<preceq> Class Object"
9cfafdb56749 robustified proof
haftmann
parents: 37956
diff changeset
   519
proof (cases T)
9cfafdb56749 robustified proof
haftmann
parents: 37956
diff changeset
   520
  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
   521
  with ClassT show ?thesis by auto
9cfafdb56749 robustified proof
haftmann
parents: 37956
diff changeset
   522
qed simp_all
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
lemma widen_trans_lemma [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
  "\<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
   526
apply (erule widen.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   527
apply        safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
prefer      5 apply (drule widen_RefT) apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
apply      (frule_tac [1] widen_Iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
apply      (frule_tac [2] widen_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
apply      (frule_tac [3] widen_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
apply      (frule_tac [4] widen_Iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
apply      (frule_tac [5] widen_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
apply      (frule_tac [6] widen_Array)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
apply      safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
apply            (rule widen.int_obj)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
prefer          6 apply (drule implmt_is_class) apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
apply (tactic "ALLGOALS (etac thin_rl)")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
prefer         6 apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
apply          (rule_tac [9] widen.arr_obj)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
apply         (rotate_tac [9] -1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
apply         (frule_tac [9] widen_RefT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
apply         (auto elim!: rtrancl_trans subcls_implmt implmt_subint2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
lemma ws_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
   547
by (auto intro: widen_trans_lemma subcls_ObjectI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   549
lemma widen_antisym_lemma [rule_format (no_asm)]: "\<lbrakk>G\<turnstile>S\<preceq>T;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
 \<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
   551
 \<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
   552
 \<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
   553
apply (erule widen.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
apply (auto dest: widen_Iface widen_NT2 widen_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
lemmas subint_antisym = 
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 38541
diff changeset
   558
       subint1_acyclic [THEN acyclic_impl_antisym_rtrancl]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
lemmas subcls_antisym = 
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 38541
diff changeset
   560
       subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
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
   563
by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
                                   subcls_antisym [THEN antisymD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
lemma widen_ObjectD [dest!]: "G\<turnstile>Class Object\<preceq>T \<Longrightarrow> T=Class Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
apply (frule widen_Class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
apply (fast dest: widen_Class_Class widen_Class_Iface)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   571
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 35416
diff changeset
   572
  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
   573
  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
   574
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
apply (unfold widens_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
lemma 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
   581
apply (unfold widens_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
section "narrowing relation"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
(* all properties of narrowing and casting conversions we actually need *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
(* these can easily be proven from the definitions below *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
rules
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
  cast_RefT2   "G\<turnstile>S\<preceq>? RefT R   \<Longrightarrow> \<exists>t. S=RefT t" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
  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
   594
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   596
(* more detailed than necessary for type-safety, see above rules. *)
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   597
inductive --{* narrowing reference conversion, cf. 5.1.5 *}
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   598
  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
   599
  for G :: prog
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   600
where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
  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
   602
| 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
   603
| obj_arr: "G\<turnstile>Class Object\<succ>T.[]"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   604
| int_cls: "G\<turnstile>     Iface I\<succ>Class C"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   605
| subint:  "imethds G I hidings imethds G J entails 
46212
d86ef6b96097 tuned white space;
wenzelm
parents: 45605
diff changeset
   606
           (\<lambda>(md, mh   ) (md',mh'). G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>
d86ef6b96097 tuned white space;
wenzelm
parents: 45605
diff changeset
   607
           \<not>G\<turnstile>I\<preceq>I J         \<Longrightarrow> G\<turnstile>     Iface I\<succ>Iface J"
d86ef6b96097 tuned white space;
wenzelm
parents: 45605
diff changeset
   608
| 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
   609
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
(*unused*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
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
   612
apply (ind_cases "G\<turnstile>RefT R\<succ>T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
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
   616
apply (ind_cases "G\<turnstile>S\<succ>RefT R")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
(*unused*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   620
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
   621
by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
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
   624
                                  \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   625
by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
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
   627
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
   628
   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
   629
   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
   630
   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
   631
 *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12858
diff changeset
   632
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
   633
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
   634
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12858
diff changeset
   635
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
   636
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
   637
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
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
   639
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12858
diff changeset
   640
lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T \<Longrightarrow> T=PrimT Boolean"
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   641
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
   642
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 12858
diff changeset
   643
lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   644
by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   645
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   646
section "casting relation"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   647
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
   648
inductive --{* casting conversion, cf. 5.5 *}
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   649
  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
   650
  for G :: prog
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 18447
diff changeset
   651
where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
  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
   653
| narrow:  "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
(*unused*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
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
   657
apply (ind_cases "G\<turnstile>RefT R\<preceq>? T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
by (auto dest: widen_RefT narrow_RefT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
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
   661
apply (ind_cases "G\<turnstile>S\<preceq>? RefT R")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
by (auto dest: widen_RefT2 narrow_RefT2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
(*unused*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
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
   666
apply (ind_cases "G\<turnstile>PrimT pt\<preceq>? T")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
by (auto dest: widen_PrimT narrow_PrimT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   668
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
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
   670
apply (ind_cases "G\<turnstile>S\<preceq>? PrimT pt")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
by (auto dest: widen_PrimT2 narrow_PrimT2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   672
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
   673
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
   674
  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
   675
  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
   676
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
   677
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
   678
  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
   679
  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
   680
    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
   681
  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
   682
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
   683
  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
   684
  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
   685
    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
   686
  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
   687
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
   688
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
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
   690
  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
   691
  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
   692
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
   693
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
   694
  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
   695
  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
   696
    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
   697
  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
   698
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
   699
  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
   700
  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
   701
    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
   702
  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
   703
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
   704
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
end