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