author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 15481 | fc075ae929e4 |
child 18447 | da548623916a |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/WellForm.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
11070 | 5 |
*) |
8011 | 6 |
|
12911 | 7 |
header {* \isaheader{Well-formedness of Java programs} *} |
8011 | 8 |
|
16417 | 9 |
theory WellForm imports TypeRel SystemClasses begin |
8011 | 10 |
|
11070 | 11 |
text {* |
12 |
for static checks on expressions and statements, see WellType. |
|
13 |
||
14 |
\begin{description} |
|
15 |
\item[improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):]\ \\ |
|
16 |
\begin{itemize} |
|
17 |
\item a method implementing or overwriting another method may have a result type |
|
18 |
that widens to the result type of the other method (instead of identical type) |
|
19 |
\end{itemize} |
|
20 |
||
21 |
\item[simplifications:]\ \\ |
|
22 |
\begin{itemize} |
|
23 |
\item for uniformity, Object is assumed to be declared like any other class |
|
24 |
\end{itemize} |
|
25 |
\end{description} |
|
26 |
*} |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
27 |
types 'c wf_mb = "'c prog => cname => 'c mdecl => bool" |
8011 | 28 |
|
29 |
constdefs |
|
14045 | 30 |
wf_syscls :: "'c prog => bool" |
31 |
"wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)" |
|
32 |
||
10069 | 33 |
wf_fdecl :: "'c prog => fdecl => bool" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
34 |
"wf_fdecl G == \<lambda>(fn,ft). is_type G ft" |
8011 | 35 |
|
10069 | 36 |
wf_mhead :: "'c prog => sig => ty => bool" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
37 |
"wf_mhead G == \<lambda>(mn,pTs) rT. (\<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT" |
8011 | 38 |
|
14045 | 39 |
ws_cdecl :: "'c prog => 'c cdecl => bool" |
40 |
"ws_cdecl G == |
|
41 |
\<lambda>(C,(D,fs,ms)). |
|
42 |
(\<forall>f\<in>set fs. wf_fdecl G f) \<and> unique fs \<and> |
|
43 |
(\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT) \<and> unique ms \<and> |
|
44 |
(C \<noteq> Object \<longrightarrow> is_class G D \<and> \<not>G\<turnstile>D\<preceq>C C)" |
|
45 |
||
46 |
ws_prog :: "'c prog => bool" |
|
47 |
"ws_prog G == |
|
48 |
wf_syscls G \<and> (\<forall>c\<in>set G. ws_cdecl G c) \<and> unique G" |
|
49 |
||
50 |
wf_mrT :: "'c prog => 'c cdecl => bool" |
|
51 |
"wf_mrT G == |
|
52 |
\<lambda>(C,(D,fs,ms)). |
|
53 |
(C \<noteq> Object \<longrightarrow> (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'. |
|
54 |
method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))" |
|
55 |
||
56 |
wf_cdecl_mdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool" |
|
57 |
"wf_cdecl_mdecl wf_mb G == |
|
58 |
\<lambda>(C,(D,fs,ms)). (\<forall>m\<in>set ms. wf_mb G C m)" |
|
59 |
||
60 |
wf_prog :: "'c wf_mb => 'c prog => bool" |
|
61 |
"wf_prog wf_mb G == |
|
62 |
ws_prog G \<and> (\<forall>c\<in> set G. wf_mrT G c \<and> wf_cdecl_mdecl wf_mb G c)" |
|
63 |
||
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
64 |
wf_mdecl :: "'c wf_mb => 'c wf_mb" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
65 |
"wf_mdecl wf_mb G C == \<lambda>(sig,rT,mb). wf_mhead G sig rT \<and> wf_mb G C (sig,rT,mb)" |
8011 | 66 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
67 |
wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool" |
10042 | 68 |
"wf_cdecl wf_mb G == |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
69 |
\<lambda>(C,(D,fs,ms)). |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
70 |
(\<forall>f\<in>set fs. wf_fdecl G f) \<and> unique fs \<and> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
71 |
(\<forall>m\<in>set ms. wf_mdecl wf_mb G C m) \<and> unique ms \<and> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
72 |
(C \<noteq> Object \<longrightarrow> is_class G D \<and> \<not>G\<turnstile>D\<preceq>C C \<and> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
73 |
(\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'. |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
74 |
method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))" |
8011 | 75 |
|
14045 | 76 |
lemma wf_cdecl_mrT_cdecl_mdecl: |
77 |
"(wf_cdecl wf_mb G c) = (ws_cdecl G c \<and> wf_mrT G c \<and> wf_cdecl_mdecl wf_mb G c)" |
|
78 |
apply (rule iffI) |
|
79 |
apply (simp add: wf_cdecl_def ws_cdecl_def wf_mrT_def wf_cdecl_mdecl_def |
|
80 |
wf_mdecl_def wf_mhead_def split_beta)+ |
|
81 |
done |
|
12951 | 82 |
|
14045 | 83 |
lemma wf_cdecl_ws_cdecl [intro]: "wf_cdecl wf_mb G cd \<Longrightarrow> ws_cdecl G cd" |
84 |
by (simp add: wf_cdecl_mrT_cdecl_mdecl) |
|
85 |
||
86 |
lemma wf_prog_ws_prog [intro]: "wf_prog wf_mb G \<Longrightarrow> ws_prog G" |
|
87 |
by (simp add: wf_prog_def ws_prog_def) |
|
88 |
||
89 |
lemma wf_prog_wf_mdecl: |
|
90 |
"\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls\<rbrakk> |
|
91 |
\<Longrightarrow> wf_mdecl wf_mb G C ((mn,pTs),rT,code)" |
|
92 |
by (auto simp add: wf_prog_def ws_prog_def wf_mdecl_def |
|
93 |
wf_cdecl_mdecl_def ws_cdecl_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
94 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
95 |
lemma class_wf: |
14045 | 96 |
"[|class G C = Some c; wf_prog wf_mb G|] |
97 |
==> wf_cdecl wf_mb G (C,c) \<and> wf_mrT G (C,c)" |
|
98 |
apply (unfold wf_prog_def ws_prog_def wf_cdecl_def class_def) |
|
99 |
apply clarify |
|
100 |
apply (drule_tac x="(C,c)" in bspec, fast dest: map_of_SomeD) |
|
101 |
apply (drule_tac x="(C,c)" in bspec, fast dest: map_of_SomeD) |
|
102 |
apply (simp add: wf_cdecl_def ws_cdecl_def wf_mdecl_def |
|
103 |
wf_cdecl_mdecl_def wf_mrT_def split_beta) |
|
104 |
done |
|
105 |
||
106 |
lemma class_wf_struct: |
|
107 |
"[|class G C = Some c; ws_prog G|] |
|
108 |
==> ws_cdecl G (C,c)" |
|
109 |
apply (unfold ws_prog_def class_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
110 |
apply (fast dest: map_of_SomeD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
111 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
112 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
113 |
lemma class_Object [simp]: |
14045 | 114 |
"ws_prog G ==> \<exists>X fs ms. class G Object = Some (X,fs,ms)" |
115 |
apply (unfold ws_prog_def wf_syscls_def class_def) |
|
12951 | 116 |
apply (auto simp: map_of_SomeI) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
117 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
118 |
|
14045 | 119 |
lemma class_Object_syscls [simp]: |
120 |
"wf_syscls G ==> unique G \<Longrightarrow> \<exists>X fs ms. class G Object = Some (X,fs,ms)" |
|
121 |
apply (unfold wf_syscls_def class_def) |
|
122 |
apply (auto simp: map_of_SomeI) |
|
123 |
done |
|
124 |
||
125 |
lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
126 |
apply (unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
127 |
apply (simp (no_asm_simp)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
128 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
129 |
|
14045 | 130 |
lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)" |
131 |
apply (simp add: ws_prog_def wf_syscls_def) |
|
13051 | 132 |
apply (simp add: is_class_def class_def) |
133 |
apply clarify |
|
134 |
apply (erule_tac x = x in allE) |
|
135 |
apply clarify |
|
136 |
apply (auto intro!: map_of_SomeI) |
|
137 |
done |
|
138 |
||
14045 | 139 |
lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
140 |
apply( frule r_into_trancl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
141 |
apply( drule subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
142 |
apply(clarify) |
14045 | 143 |
apply( drule (1) class_wf_struct) |
144 |
apply( unfold ws_cdecl_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
145 |
apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
146 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
147 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
148 |
lemma wf_cdecl_supD: |
14045 | 149 |
"!!r. \<lbrakk>ws_cdecl G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D" |
150 |
apply (unfold ws_cdecl_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
151 |
apply (auto split add: option.split_asm) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
152 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
153 |
|
14045 | 154 |
lemma subcls_asym: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
155 |
apply(erule tranclE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
156 |
apply(fast dest!: subcls1_wfD ) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
157 |
apply(fast dest!: subcls1_wfD intro: trancl_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
158 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
159 |
|
14045 | 160 |
lemma subcls_irrefl: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
161 |
apply (erule trancl_trans_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
162 |
apply (auto dest: subcls1_wfD subcls_asym) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
163 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
164 |
|
14045 | 165 |
lemma acyclic_subcls1: "ws_prog G ==> acyclic (subcls1 G)" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
166 |
apply (unfold acyclic_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
167 |
apply (fast dest: subcls_irrefl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
168 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
169 |
|
14045 | 170 |
lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)^-1)" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
171 |
apply (rule finite_acyclic_wf) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
172 |
apply ( subst finite_converse) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
173 |
apply ( rule finite_subcls1) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
174 |
apply (subst acyclic_converse) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
175 |
apply (erule acyclic_subcls1) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
176 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
177 |
|
14045 | 178 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
179 |
lemma subcls_induct: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
180 |
"[|wf_prog wf_mb G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
181 |
(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
182 |
proof - |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
183 |
assume p: "PROP ?P" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
184 |
assume ?A thus ?thesis apply - |
14045 | 185 |
apply (drule wf_prog_ws_prog) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
186 |
apply(drule wf_subcls1) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
187 |
apply(drule wf_trancl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
188 |
apply(simp only: trancl_converse) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
189 |
apply(erule_tac a = C in wf_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
190 |
apply(rule p) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
191 |
apply(auto) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
192 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
193 |
qed |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
194 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
195 |
lemma subcls1_induct: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
196 |
"[|is_class G C; wf_prog wf_mb G; P Object; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
197 |
!!C D fs ms. [|C \<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \<and> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
198 |
wf_cdecl wf_mb G (C,D,fs,ms) \<and> G\<turnstile>C\<prec>C1D \<and> is_class G D \<and> P D|] ==> P C |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
199 |
|] ==> P C" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
200 |
(is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
201 |
proof - |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
202 |
assume p: "PROP ?P" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
203 |
assume ?A ?B ?C thus ?thesis apply - |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
204 |
apply(unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
205 |
apply( rule impE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
206 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
207 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
208 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
209 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
210 |
apply( erule thin_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
211 |
apply( rule subcls_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
212 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
213 |
apply( rule impI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
214 |
apply( case_tac "C = Object") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
215 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
216 |
apply safe |
14045 | 217 |
apply( frule (1) class_wf) apply (erule conjE)+ |
218 |
apply (frule wf_cdecl_ws_cdecl) |
|
219 |
apply( frule (1) wf_cdecl_supD) |
|
220 |
||
221 |
apply( subgoal_tac "G\<turnstile>C\<prec>C1a") |
|
222 |
apply( erule_tac [2] subcls1I) |
|
223 |
apply( rule p) |
|
224 |
apply (unfold is_class_def) |
|
225 |
apply auto |
|
226 |
done |
|
227 |
qed |
|
228 |
||
229 |
lemma subcls_induct_struct: |
|
230 |
"[|ws_prog G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C" |
|
231 |
(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _") |
|
232 |
proof - |
|
233 |
assume p: "PROP ?P" |
|
234 |
assume ?A thus ?thesis apply - |
|
235 |
apply(drule wf_subcls1) |
|
236 |
apply(drule wf_trancl) |
|
237 |
apply(simp only: trancl_converse) |
|
238 |
apply(erule_tac a = C in wf_induct) |
|
239 |
apply(rule p) |
|
240 |
apply(auto) |
|
241 |
done |
|
242 |
qed |
|
243 |
||
244 |
||
245 |
lemma subcls1_induct_struct: |
|
246 |
"[|is_class G C; ws_prog G; P Object; |
|
247 |
!!C D fs ms. [|C \<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \<and> |
|
248 |
ws_cdecl G (C,D,fs,ms) \<and> G\<turnstile>C\<prec>C1D \<and> is_class G D \<and> P D|] ==> P C |
|
249 |
|] ==> P C" |
|
250 |
(is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _") |
|
251 |
proof - |
|
252 |
assume p: "PROP ?P" |
|
253 |
assume ?A ?B ?C thus ?thesis apply - |
|
254 |
apply(unfold is_class_def) |
|
255 |
apply( rule impE) |
|
256 |
prefer 2 |
|
257 |
apply( assumption) |
|
258 |
prefer 2 |
|
259 |
apply( assumption) |
|
260 |
apply( erule thin_rl) |
|
261 |
apply( rule subcls_induct_struct) |
|
262 |
apply( assumption) |
|
263 |
apply( rule impI) |
|
264 |
apply( case_tac "C = Object") |
|
265 |
apply( fast) |
|
266 |
apply safe |
|
267 |
apply( frule (1) class_wf_struct) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
268 |
apply( frule (1) wf_cdecl_supD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
269 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
270 |
apply( subgoal_tac "G\<turnstile>C\<prec>C1a") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
271 |
apply( erule_tac [2] subcls1I) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
272 |
apply( rule p) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
273 |
apply (unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
274 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
275 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
276 |
qed |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
277 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
278 |
lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma]; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
279 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
280 |
lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma]; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
281 |
|
14045 | 282 |
lemma field_rec: "\<lbrakk>class G C = Some (D, fs, ms); ws_prog G\<rbrakk> |
13672 | 283 |
\<Longrightarrow> field (G, C) = |
284 |
(if C = Object then empty else field (G, D)) ++ |
|
285 |
map_of (map (\<lambda>(s, f). (s, C, f)) fs)" |
|
286 |
apply (simp only: field_def) |
|
287 |
apply (frule fields_rec, assumption) |
|
288 |
apply (rule HOL.trans) |
|
289 |
apply (simp add: o_def) |
|
290 |
apply (simp (no_asm_use) |
|
291 |
add: split_beta split_def o_def map_compose [THEN sym] del: map_compose) |
|
292 |
done |
|
293 |
||
12951 | 294 |
lemma method_Object [simp]: |
14045 | 295 |
"method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> ws_prog G \<Longrightarrow> D = Object" |
12951 | 296 |
apply (frule class_Object, clarify) |
297 |
apply (drule method_rec, assumption) |
|
298 |
apply (auto dest: map_of_SomeD) |
|
299 |
done |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
300 |
|
13672 | 301 |
|
14045 | 302 |
lemma fields_Object [simp]: "\<lbrakk> ((vn, C), T) \<in> set (fields (G, Object)); ws_prog G \<rbrakk> |
13672 | 303 |
\<Longrightarrow> C = Object" |
304 |
apply (frule class_Object) |
|
305 |
apply clarify |
|
306 |
apply (subgoal_tac "fields (G, Object) = map (\<lambda>(fn,ft). ((fn,Object),ft)) fs") |
|
307 |
apply (simp add: image_iff split_beta) |
|
308 |
apply auto |
|
309 |
apply (rule trans) |
|
310 |
apply (rule fields_rec, assumption+) |
|
311 |
apply simp |
|
312 |
done |
|
313 |
||
14045 | 314 |
lemma subcls_C_Object: "[|is_class G C; ws_prog G|] ==> G\<turnstile>C\<preceq>C Object" |
315 |
apply(erule subcls1_induct_struct) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
316 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
317 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
318 |
apply(auto dest!: wf_cdecl_supD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
319 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
320 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
321 |
lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
322 |
apply (unfold wf_mhead_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
323 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
324 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
325 |
|
14045 | 326 |
lemma widen_fields_defpl': "[|is_class G C; ws_prog G|] ==> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
327 |
\<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd" |
14045 | 328 |
apply( erule subcls1_induct_struct) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
329 |
apply( assumption) |
12951 | 330 |
apply( frule class_Object) |
331 |
apply( clarify) |
|
332 |
apply( frule fields_rec, assumption) |
|
333 |
apply( fastsimp) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
334 |
apply( tactic "safe_tac HOL_cs") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
335 |
apply( subst fields_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
336 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
337 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
338 |
apply( simp (no_asm) split del: split_if) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
339 |
apply( rule ballI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
340 |
apply( simp (no_asm_simp) only: split_tupled_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
341 |
apply( simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
342 |
apply( erule UnE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
343 |
apply( force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
344 |
apply( erule r_into_rtrancl [THEN rtrancl_trans]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
345 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
346 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
347 |
|
12517 | 348 |
lemma widen_fields_defpl: |
14045 | 349 |
"[|((fn,fd),fT) \<in> set (fields (G,C)); ws_prog G; is_class G C|] ==> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
350 |
G\<turnstile>C\<preceq>C fd" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
351 |
apply( drule (1) widen_fields_defpl') |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
352 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
353 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
354 |
|
12517 | 355 |
lemma unique_fields: |
14045 | 356 |
"[|is_class G C; ws_prog G|] ==> unique (fields (G,C))" |
357 |
apply( erule subcls1_induct_struct) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
358 |
apply( assumption) |
12951 | 359 |
apply( frule class_Object) |
360 |
apply( clarify) |
|
361 |
apply( frule fields_rec, assumption) |
|
14045 | 362 |
apply( drule class_wf_struct, assumption) |
363 |
apply( simp add: ws_cdecl_def) |
|
12951 | 364 |
apply( rule unique_map_inj) |
365 |
apply( simp) |
|
13585 | 366 |
apply( rule inj_onI) |
12951 | 367 |
apply( simp) |
368 |
apply( safe dest!: wf_cdecl_supD) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
369 |
apply( drule subcls1_wfD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
370 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
371 |
apply( subst fields_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
372 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
373 |
apply( rotate_tac -1) |
14045 | 374 |
apply( frule class_wf_struct) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
375 |
apply auto |
14045 | 376 |
apply( simp add: ws_cdecl_def) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
377 |
apply( erule unique_append) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
378 |
apply( rule unique_map_inj) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
379 |
apply( clarsimp) |
13585 | 380 |
apply (rule inj_onI) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
381 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
382 |
apply(auto dest!: widen_fields_defpl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
383 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
384 |
|
12517 | 385 |
lemma fields_mono_lemma [rule_format (no_asm)]: |
14045 | 386 |
"[|ws_prog G; (C',C)\<in>(subcls1 G)^*|] ==> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
387 |
x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
388 |
apply(erule converse_rtrancl_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
389 |
apply( safe dest!: subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
390 |
apply(subst fields_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
391 |
apply( auto) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
392 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
393 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
394 |
lemma fields_mono: |
14045 | 395 |
"\<lbrakk>map_of (fields (G,C)) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; ws_prog G\<rbrakk> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
396 |
\<Longrightarrow> map_of (fields (G,D)) fn = Some f" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
397 |
apply (rule map_of_SomeI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
398 |
apply (erule (1) unique_fields) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
399 |
apply (erule (1) fields_mono_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
400 |
apply (erule map_of_SomeD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
401 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
402 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
403 |
lemma widen_cfs_fields: |
14045 | 404 |
"[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; ws_prog G|]==> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
405 |
map_of (fields (G,D)) (fn, fd) = Some fT" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
406 |
apply (drule field_fields) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
407 |
apply (drule rtranclD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
408 |
apply safe |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
409 |
apply (frule subcls_is_class) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
410 |
apply (drule trancl_into_rtrancl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
411 |
apply (fast dest: fields_mono) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
412 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
413 |
|
12517 | 414 |
lemma method_wf_mdecl [rule_format (no_asm)]: |
415 |
"wf_prog wf_mb G ==> is_class G C \<Longrightarrow> |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
416 |
method (G,C) sig = Some (md,mh,m) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
417 |
--> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))" |
14045 | 418 |
apply (frule wf_prog_ws_prog) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
419 |
apply( erule subcls1_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
420 |
apply( assumption) |
12951 | 421 |
apply( clarify) |
422 |
apply( frule class_Object) |
|
423 |
apply( clarify) |
|
424 |
apply( frule method_rec, assumption) |
|
425 |
apply( drule class_wf, assumption) |
|
426 |
apply( simp add: wf_cdecl_def) |
|
427 |
apply( drule map_of_SomeD) |
|
428 |
apply( subgoal_tac "md = Object") |
|
14045 | 429 |
apply( fastsimp) |
12951 | 430 |
apply( fastsimp) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
431 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
432 |
apply( frule_tac C = C in method_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
433 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
434 |
apply( rotate_tac -1) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
435 |
apply( simp) |
14025 | 436 |
apply( drule map_add_SomeD) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
437 |
apply( erule disjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
438 |
apply( erule_tac V = "?P --> ?Q" in thin_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
439 |
apply (frule map_of_SomeD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
440 |
apply (clarsimp simp add: wf_cdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
441 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
442 |
apply( rule rtrancl_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
443 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
444 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
445 |
apply( rule r_into_rtrancl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
446 |
apply( fast intro: subcls1I) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
447 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
448 |
|
13672 | 449 |
|
14045 | 450 |
lemma method_wf_mhead [rule_format (no_asm)]: |
451 |
"ws_prog G ==> is_class G C \<Longrightarrow> |
|
452 |
method (G,C) sig = Some (md,rT,mb) |
|
453 |
--> G\<turnstile>C\<preceq>C md \<and> wf_mhead G sig rT" |
|
454 |
apply( erule subcls1_induct_struct) |
|
455 |
apply( assumption) |
|
456 |
apply( clarify) |
|
457 |
apply( frule class_Object) |
|
458 |
apply( clarify) |
|
459 |
apply( frule method_rec, assumption) |
|
460 |
apply( drule class_wf_struct, assumption) |
|
461 |
apply( simp add: ws_cdecl_def) |
|
462 |
apply( drule map_of_SomeD) |
|
463 |
apply( subgoal_tac "md = Object") |
|
464 |
apply( fastsimp) |
|
465 |
apply( fastsimp) |
|
466 |
apply( clarify) |
|
467 |
apply( frule_tac C = C in method_rec) |
|
468 |
apply( assumption) |
|
469 |
apply( rotate_tac -1) |
|
470 |
apply( simp) |
|
471 |
apply( drule map_add_SomeD) |
|
472 |
apply( erule disjE) |
|
473 |
apply( erule_tac V = "?P --> ?Q" in thin_rl) |
|
474 |
apply (frule map_of_SomeD) |
|
475 |
apply (clarsimp simp add: ws_cdecl_def) |
|
476 |
apply blast |
|
477 |
apply clarify |
|
478 |
apply( rule rtrancl_trans) |
|
479 |
prefer 2 |
|
480 |
apply( assumption) |
|
481 |
apply( rule r_into_rtrancl) |
|
482 |
apply( fast intro: subcls1I) |
|
13672 | 483 |
done |
484 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
485 |
lemma subcls_widen_methd [rule_format (no_asm)]: |
14045 | 486 |
"[|G\<turnstile>T'\<preceq>C T; wf_prog wf_mb G|] ==> |
487 |
\<forall>D rT b. method (G,T) sig = Some (D,rT ,b) --> |
|
488 |
(\<exists>D' rT' b'. method (G,T') sig = Some (D',rT',b') \<and> G\<turnstile>D'\<preceq>C D \<and> G\<turnstile>rT'\<preceq>rT)" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
489 |
apply( drule rtranclD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
490 |
apply( erule disjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
491 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
492 |
apply( erule conjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
493 |
apply( erule trancl_trans_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
494 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
495 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
496 |
apply( drule spec, drule spec, drule spec, erule (1) impE) |
14045 | 497 |
apply( fast elim: widen_trans rtrancl_trans) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
498 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
499 |
apply( drule subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
500 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
501 |
apply( subst method_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
502 |
apply( assumption) |
14025 | 503 |
apply( unfold map_add_def) |
14045 | 504 |
apply( simp (no_asm_simp) add: wf_prog_ws_prog del: split_paired_Ex) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
505 |
apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
506 |
apply( erule exE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
507 |
apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
508 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
509 |
apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
510 |
apply( tactic "asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
511 |
apply( simp_all (no_asm_simp) del: split_paired_Ex) |
14045 | 512 |
apply( frule (1) class_wf) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
513 |
apply( simp (no_asm_simp) only: split_tupled_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
514 |
apply( unfold wf_cdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
515 |
apply( drule map_of_SomeD) |
14045 | 516 |
apply (auto simp add: wf_mrT_def) |
517 |
apply (rule rtrancl_trans) |
|
518 |
defer |
|
519 |
apply (rule method_wf_mhead [THEN conjunct1]) |
|
520 |
apply (simp only: wf_prog_def) |
|
521 |
apply (simp add: is_class_def) |
|
522 |
apply assumption |
|
523 |
apply (auto intro: subcls1I) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
524 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
525 |
|
14045 | 526 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
527 |
lemma subtype_widen_methd: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
528 |
"[| G\<turnstile> C\<preceq>C D; wf_prog wf_mb G; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
529 |
method (G,D) sig = Some (md, rT, b) |] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
530 |
==> \<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \<and> G\<turnstile>rT'\<preceq>rT" |
14045 | 531 |
apply(auto dest: subcls_widen_methd |
12517 | 532 |
simp add: wf_mdecl_def wf_mhead_def split_def) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
533 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
534 |
|
14045 | 535 |
|
12517 | 536 |
lemma method_in_md [rule_format (no_asm)]: |
14045 | 537 |
"ws_prog G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) |
12517 | 538 |
--> is_class G D \<and> method (G,D) sig = Some(D,mh,code)" |
14045 | 539 |
apply (erule (1) subcls1_induct_struct) |
12951 | 540 |
apply clarify |
541 |
apply (frule method_Object, assumption) |
|
542 |
apply hypsubst |
|
543 |
apply simp |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
544 |
apply (erule conjE) |
15481 | 545 |
apply (simplesubst method_rec, assumption+) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
546 |
apply (clarify) |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14045
diff
changeset
|
547 |
apply (erule_tac x = "Da" in allE) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
548 |
apply (clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
549 |
apply (simp add: map_of_map) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
550 |
apply (clarify) |
15481 | 551 |
apply (subst method_rec, assumption+) |
14025 | 552 |
apply (simp add: map_add_def map_of_map split add: option.split) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
553 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
554 |
|
13672 | 555 |
|
14045 | 556 |
lemma method_in_md_struct [rule_format (no_asm)]: |
557 |
"ws_prog G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) |
|
558 |
--> is_class G D \<and> method (G,D) sig = Some(D,mh,code)" |
|
559 |
apply (erule (1) subcls1_induct_struct) |
|
560 |
apply clarify |
|
561 |
apply (frule method_Object, assumption) |
|
562 |
apply hypsubst |
|
563 |
apply simp |
|
564 |
apply (erule conjE) |
|
15481 | 565 |
apply (simplesubst method_rec, assumption+) |
14045 | 566 |
apply (clarify) |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14045
diff
changeset
|
567 |
apply (erule_tac x = "Da" in allE) |
14045 | 568 |
apply (clarsimp) |
569 |
apply (simp add: map_of_map) |
|
570 |
apply (clarify) |
|
15481 | 571 |
apply (subst method_rec, assumption+) |
14045 | 572 |
apply (simp add: map_add_def map_of_map split add: option.split) |
573 |
done |
|
574 |
||
13672 | 575 |
lemma fields_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk> |
576 |
\<Longrightarrow> \<forall> vn D T. (((vn,D),T) \<in> set (fields (G,C)) |
|
577 |
\<longrightarrow> (is_class G D \<and> ((vn,D),T) \<in> set (fields (G,D))))" |
|
578 |
apply (erule (1) subcls1_induct) |
|
579 |
||
580 |
apply clarify |
|
14045 | 581 |
apply (frule wf_prog_ws_prog) |
13672 | 582 |
apply (frule fields_Object, assumption+) |
583 |
apply (simp only: is_class_Object) apply simp |
|
584 |
||
585 |
apply clarify |
|
586 |
apply (frule fields_rec) |
|
14045 | 587 |
apply (simp (no_asm_simp) add: wf_prog_ws_prog) |
13672 | 588 |
|
589 |
apply (case_tac "Da=C") |
|
590 |
apply blast (* case Da=C *) |
|
591 |
||
592 |
apply (subgoal_tac "((vn, Da), T) \<in> set (fields (G, D))") apply blast |
|
593 |
apply (erule thin_rl) |
|
594 |
apply (rotate_tac 1) |
|
595 |
apply (erule thin_rl, erule thin_rl, erule thin_rl, |
|
596 |
erule thin_rl, erule thin_rl, erule thin_rl) |
|
597 |
apply auto |
|
598 |
done |
|
599 |
||
600 |
lemma field_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk> |
|
601 |
\<Longrightarrow> \<forall> vn D T. (field (G,C) vn = Some(D,T) |
|
602 |
\<longrightarrow> is_class G D \<and> field (G,D) vn = Some(D,T))" |
|
603 |
apply (erule (1) subcls1_induct) |
|
604 |
||
605 |
apply clarify |
|
606 |
apply (frule field_fields) |
|
607 |
apply (drule map_of_SomeD) |
|
14045 | 608 |
apply (frule wf_prog_ws_prog) |
13672 | 609 |
apply (drule fields_Object, assumption+) |
610 |
apply simp |
|
611 |
||
612 |
apply clarify |
|
613 |
apply (subgoal_tac "((field (G, D)) ++ map_of (map (\<lambda>(s, f). (s, C, f)) fs)) vn = Some (Da, T)") |
|
14025 | 614 |
apply (simp (no_asm_use) only: map_add_Some_iff) |
13672 | 615 |
apply (erule disjE) |
616 |
apply (simp (no_asm_use) add: map_of_map) apply blast |
|
617 |
apply blast |
|
618 |
apply (rule trans [THEN sym], rule sym, assumption) |
|
619 |
apply (rule_tac x=vn in fun_cong) |
|
620 |
apply (rule trans, rule field_rec, assumption+) |
|
14045 | 621 |
apply (simp (no_asm_simp) add: wf_prog_ws_prog) |
13672 | 622 |
apply (simp (no_asm_use)) apply blast |
623 |
done |
|
624 |
||
625 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
626 |
lemma widen_methd: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
627 |
"[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\<turnstile>T''\<preceq>C C|] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
628 |
==> \<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \<and> G\<turnstile>rT'\<preceq>rT" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
629 |
apply( drule subcls_widen_methd) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
630 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
631 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
632 |
|
13672 | 633 |
lemma widen_field: "\<lbrakk> (field (G,C) fn) = Some (fd, fT); wf_prog wf_mb G; is_class G C \<rbrakk> |
634 |
\<Longrightarrow> G\<turnstile>C\<preceq>C fd" |
|
635 |
apply (rule widen_fields_defpl) |
|
636 |
apply (simp add: field_def) |
|
637 |
apply (rule map_of_SomeD) |
|
638 |
apply (rule table_of_remap_SomeD) |
|
639 |
apply assumption+ |
|
14045 | 640 |
apply (simp (no_asm_simp) add: wf_prog_ws_prog)+ |
13672 | 641 |
done |
642 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
643 |
lemma Call_lemma: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
644 |
"[|method (G,C) sig = Some (md,rT,b); G\<turnstile>T''\<preceq>C C; wf_prog wf_mb G; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
645 |
class G C = Some y|] ==> \<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \<and> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
646 |
G\<turnstile>rT'\<preceq>rT \<and> G\<turnstile>T''\<preceq>C T' \<and> wf_mhead G sig rT' \<and> wf_mb G T' (sig,rT',b)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
647 |
apply( drule (2) widen_methd) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
648 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
649 |
apply( frule subcls_is_class2) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
650 |
apply (unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
651 |
apply (simp (no_asm_simp)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
652 |
apply( drule method_wf_mdecl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
653 |
apply( unfold wf_mdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
654 |
apply( unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
655 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
656 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
657 |
|
12517 | 658 |
lemma fields_is_type_lemma [rule_format (no_asm)]: |
14045 | 659 |
"[|is_class G C; ws_prog G|] ==> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
660 |
\<forall>f\<in>set (fields (G,C)). is_type G (snd f)" |
14045 | 661 |
apply( erule (1) subcls1_induct_struct) |
12951 | 662 |
apply( frule class_Object) |
663 |
apply( clarify) |
|
664 |
apply( frule fields_rec, assumption) |
|
14045 | 665 |
apply( drule class_wf_struct, assumption) |
666 |
apply( simp add: ws_cdecl_def wf_fdecl_def) |
|
12951 | 667 |
apply( fastsimp) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
668 |
apply( subst fields_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
669 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
670 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
671 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
672 |
apply( safe) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
673 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
674 |
apply( force) |
14045 | 675 |
apply( drule (1) class_wf_struct) |
676 |
apply( unfold ws_cdecl_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
677 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
678 |
apply( drule (1) bspec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
679 |
apply( unfold wf_fdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
680 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
681 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
682 |
|
14045 | 683 |
|
12517 | 684 |
lemma fields_is_type: |
14045 | 685 |
"[|map_of (fields (G,C)) fn = Some f; ws_prog G; is_class G C|] ==> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
686 |
is_type G f" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
687 |
apply(drule map_of_SomeD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
688 |
apply(drule (2) fields_is_type_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
689 |
apply(auto) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
690 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
691 |
|
14045 | 692 |
|
693 |
lemma field_is_type: "\<lbrakk> ws_prog G; is_class G C; field (G, C) fn = Some (fd, fT) \<rbrakk> |
|
694 |
\<Longrightarrow> is_type G fT" |
|
695 |
apply (frule_tac f="((fn, fd), fT)" in fields_is_type_lemma) |
|
696 |
apply (auto simp add: field_def dest: map_of_SomeD) |
|
697 |
done |
|
698 |
||
699 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
700 |
lemma methd: |
14045 | 701 |
"[| ws_prog G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |] |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
702 |
==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
703 |
proof - |
14045 | 704 |
assume wf: "ws_prog G" and C: "(C,S,fs,mdecls) \<in> set G" and |
12951 | 705 |
m: "(sig,rT,code) \<in> set mdecls" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
706 |
moreover |
12951 | 707 |
from wf C have "class G C = Some (S,fs,mdecls)" |
14045 | 708 |
by (auto simp add: ws_prog_def class_def is_class_def intro: map_of_SomeI) |
12951 | 709 |
moreover |
710 |
from wf C |
|
14045 | 711 |
have "unique mdecls" by (unfold ws_prog_def ws_cdecl_def) auto |
12951 | 712 |
hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto) |
713 |
with m |
|
714 |
have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)" |
|
715 |
by (force intro: map_of_SomeI) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
716 |
ultimately |
12517 | 717 |
show ?thesis by (auto simp add: is_class_def dest: method_rec) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
718 |
qed |
8011 | 719 |
|
12951 | 720 |
|
721 |
lemma wf_mb'E: |
|
722 |
"\<lbrakk> wf_prog wf_mb G; \<And>C S fs ms m.\<lbrakk>(C,S,fs,ms) \<in> set G; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_mb' G C m \<rbrakk> |
|
723 |
\<Longrightarrow> wf_prog wf_mb' G" |
|
14045 | 724 |
apply (simp only: wf_prog_def) |
12951 | 725 |
apply auto |
14045 | 726 |
apply (simp add: wf_cdecl_mdecl_def) |
12951 | 727 |
apply safe |
728 |
apply (drule bspec, assumption) apply simp |
|
729 |
done |
|
730 |
||
731 |
||
732 |
lemma fst_mono: "A \<subseteq> B \<Longrightarrow> fst ` A \<subseteq> fst ` B" by fast |
|
733 |
||
734 |
lemma wf_syscls: |
|
735 |
"set SystemClasses \<subseteq> set G \<Longrightarrow> wf_syscls G" |
|
736 |
apply (drule fst_mono) |
|
737 |
apply (simp add: SystemClasses_def wf_syscls_def) |
|
738 |
apply (simp add: ObjectC_def) |
|
739 |
apply (rule allI, case_tac x) |
|
740 |
apply (auto simp add: NullPointerC_def ClassCastC_def OutOfMemoryC_def) |
|
741 |
done |
|
742 |
||
8011 | 743 |
end |