author | oheimb |
Mon, 05 Feb 2001 20:14:15 +0100 | |
changeset 11070 | cc421547e744 |
parent 11026 | a50365d21144 |
child 12517 | 360e3215f029 |
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 |
|
11070 | 7 |
header "Well-formedness of Java programs" |
8011 | 8 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
9 |
theory WellForm = TypeRel: |
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 |
|
10069 | 30 |
wf_fdecl :: "'c prog => fdecl => bool" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
31 |
"wf_fdecl G == \<lambda>(fn,ft). is_type G ft" |
8011 | 32 |
|
10069 | 33 |
wf_mhead :: "'c prog => sig => ty => bool" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
34 |
"wf_mhead G == \<lambda>(mn,pTs) rT. (\<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT" |
8011 | 35 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
36 |
wf_mdecl :: "'c wf_mb => 'c wf_mb" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
37 |
"wf_mdecl wf_mb G C == \<lambda>(sig,rT,mb). wf_mhead G sig rT \<and> wf_mb G C (sig,rT,mb)" |
8011 | 38 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
39 |
wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool" |
10042 | 40 |
"wf_cdecl wf_mb G == |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
41 |
\<lambda>(C,(D,fs,ms)). |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
42 |
(\<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
|
43 |
(\<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
|
44 |
(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
|
45 |
(\<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
|
46 |
method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))" |
8011 | 47 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
48 |
wf_prog :: "'c wf_mb => 'c prog => bool" |
10042 | 49 |
"wf_prog wf_mb G == |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
50 |
let cs = set G in ObjectC \<in> cs \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
51 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
52 |
lemma class_wf: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
53 |
"[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
54 |
apply (unfold wf_prog_def class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
55 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
56 |
apply (fast dest: map_of_SomeD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
57 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
58 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
59 |
lemma class_Object [simp]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
60 |
"wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
61 |
apply (unfold wf_prog_def ObjectC_def class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
62 |
apply (auto intro: map_of_SomeI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
63 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
64 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
65 |
lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
66 |
apply (unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
67 |
apply (simp (no_asm_simp)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
68 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
69 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
70 |
lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; wf_prog wf_mb G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
71 |
apply( frule r_into_trancl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
72 |
apply( drule subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
73 |
apply(clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
74 |
apply( drule (1) class_wf) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
75 |
apply( unfold wf_cdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
76 |
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
|
77 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
78 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
79 |
lemma wf_cdecl_supD: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
80 |
"!!r. \<lbrakk>wf_cdecl wf_mb G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
81 |
apply (unfold wf_cdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
82 |
apply (auto split add: option.split_asm) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
83 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
84 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
85 |
lemma subcls_asym: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
86 |
apply(erule tranclE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
87 |
apply(fast dest!: subcls1_wfD ) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
88 |
apply(fast dest!: subcls1_wfD intro: trancl_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
89 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
90 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
91 |
lemma subcls_irrefl: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
92 |
apply (erule trancl_trans_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
93 |
apply (auto dest: subcls1_wfD subcls_asym) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
94 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
95 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
96 |
lemma acyclic_subcls1: "wf_prog wf_mb G ==> acyclic (subcls1 G)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
97 |
apply (unfold acyclic_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
98 |
apply (fast dest: subcls_irrefl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
99 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
100 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
101 |
lemma wf_subcls1: "wf_prog wf_mb G ==> wf ((subcls1 G)^-1)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
102 |
apply (rule finite_acyclic_wf) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
103 |
apply ( subst finite_converse) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
104 |
apply ( rule finite_subcls1) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
105 |
apply (subst acyclic_converse) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
106 |
apply (erule acyclic_subcls1) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
107 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
108 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
109 |
lemma subcls_induct: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
110 |
"[|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
|
111 |
(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
112 |
proof - |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
113 |
assume p: "PROP ?P" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
114 |
assume ?A thus ?thesis apply - |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
115 |
apply(drule wf_subcls1) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
116 |
apply(drule wf_trancl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
117 |
apply(simp only: trancl_converse) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
118 |
apply(erule_tac a = C in wf_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
119 |
apply(rule p) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
120 |
apply(auto) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
121 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
122 |
qed |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
123 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
124 |
lemma subcls1_induct: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
125 |
"[|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
|
126 |
!!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
|
127 |
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
|
128 |
|] ==> P C" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
129 |
(is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
130 |
proof - |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
131 |
assume p: "PROP ?P" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
132 |
assume ?A ?B ?C thus ?thesis apply - |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
133 |
apply(unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
134 |
apply( rule impE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
135 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
136 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
137 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
138 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
139 |
apply( erule thin_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
140 |
apply( rule subcls_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
141 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
142 |
apply( rule impI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
143 |
apply( case_tac "C = Object") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
144 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
145 |
apply safe |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
146 |
apply( frule (1) class_wf) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
147 |
apply( frule (1) wf_cdecl_supD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
148 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
149 |
apply( subgoal_tac "G\<turnstile>C\<prec>C1a") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
150 |
apply( erule_tac [2] subcls1I) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
151 |
apply( rule p) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
152 |
apply (unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
153 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
154 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
155 |
qed |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
156 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
157 |
lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma]; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
158 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
159 |
lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma]; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
160 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
161 |
lemma method_Object [simp]: "wf_prog wf_mb G ==> method (G,Object) = empty" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
162 |
apply(subst method_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
163 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
164 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
165 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
166 |
lemma fields_Object [simp]: "wf_prog wf_mb G ==> fields (G,Object) = []" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
167 |
apply(subst fields_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
168 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
169 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
170 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
171 |
lemma field_Object [simp]: "wf_prog wf_mb G ==> field (G,Object) = empty" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
172 |
apply (unfold field_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
173 |
apply(simp (no_asm_simp)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
174 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
175 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
176 |
lemma subcls_C_Object: "[|is_class G C; wf_prog wf_mb G|] ==> G\<turnstile>C\<preceq>C Object" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
177 |
apply(erule subcls1_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
178 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
179 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
180 |
apply(auto dest!: wf_cdecl_supD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
181 |
apply(erule (1) rtrancl_into_rtrancl2) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
182 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
183 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
184 |
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
|
185 |
apply (unfold wf_mhead_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
186 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
187 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
188 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
189 |
lemma widen_fields_defpl': "[|is_class G C; wf_prog wf_mb G|] ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
190 |
\<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
191 |
apply( erule subcls1_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
192 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
193 |
apply( simp (no_asm_simp)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
194 |
apply( tactic "safe_tac HOL_cs") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
195 |
apply( subst fields_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
196 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
197 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
198 |
apply( simp (no_asm) split del: split_if) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
199 |
apply( rule ballI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
200 |
apply( simp (no_asm_simp) only: split_tupled_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
201 |
apply( simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
202 |
apply( erule UnE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
203 |
apply( force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
204 |
apply( erule r_into_rtrancl [THEN rtrancl_trans]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
205 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
206 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
207 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
208 |
lemma widen_fields_defpl: "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
209 |
G\<turnstile>C\<preceq>C fd" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
210 |
apply( drule (1) widen_fields_defpl') |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
211 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
212 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
213 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
214 |
lemma unique_fields: "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
215 |
apply( erule subcls1_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
216 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
217 |
apply( safe dest!: wf_cdecl_supD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
218 |
apply( simp (no_asm_simp)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
219 |
apply( drule subcls1_wfD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
220 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
221 |
apply( subst fields_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
222 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
223 |
apply( rotate_tac -1) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
224 |
apply( frule class_wf) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
225 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
226 |
apply( simp add: wf_cdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
227 |
apply( erule unique_append) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
228 |
apply( rule unique_map_inj) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
229 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
230 |
apply (rule injI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
231 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
232 |
apply(auto dest!: widen_fields_defpl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
233 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
234 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
235 |
lemma fields_mono_lemma [rule_format (no_asm)]: "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
236 |
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
|
237 |
apply(erule converse_rtrancl_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
238 |
apply( safe dest!: subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
239 |
apply(subst fields_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
240 |
apply( auto) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
241 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
242 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
243 |
lemma fields_mono: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
244 |
"\<lbrakk>map_of (fields (G,C)) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; wf_prog wf_mb G\<rbrakk> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
245 |
\<Longrightarrow> map_of (fields (G,D)) fn = Some f" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
246 |
apply (rule map_of_SomeI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
247 |
apply (erule (1) unique_fields) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
248 |
apply (erule (1) fields_mono_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
249 |
apply (erule map_of_SomeD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
250 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
251 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
252 |
lemma widen_cfs_fields: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
253 |
"[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; wf_prog wf_mb G|]==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
254 |
map_of (fields (G,D)) (fn, fd) = Some fT" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
255 |
apply (drule field_fields) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
256 |
apply (drule rtranclD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
257 |
apply safe |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
258 |
apply (frule subcls_is_class) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
259 |
apply (drule trancl_into_rtrancl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
260 |
apply (fast dest: fields_mono) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
261 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
262 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
263 |
lemma method_wf_mdecl [rule_format (no_asm)]: "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
264 |
method (G,C) sig = Some (md,mh,m) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
265 |
--> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
266 |
apply( erule subcls1_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
267 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
268 |
apply( force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
269 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
270 |
apply( frule_tac C = C in method_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
271 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
272 |
apply( rotate_tac -1) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
273 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
274 |
apply( drule override_SomeD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
275 |
apply( erule disjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
276 |
apply( erule_tac V = "?P --> ?Q" in thin_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
277 |
apply (frule map_of_SomeD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
278 |
apply (clarsimp simp add: wf_cdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
279 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
280 |
apply( rule rtrancl_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
281 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
282 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
283 |
apply( rule r_into_rtrancl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
284 |
apply( fast intro: subcls1I) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
285 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
286 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
287 |
lemma subcls_widen_methd [rule_format (no_asm)]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
288 |
"[|G\<turnstile>T\<preceq>C T'; wf_prog wf_mb G|] ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
289 |
\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) --> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
290 |
(\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \<and> G\<turnstile>rT'\<preceq>rT)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
291 |
apply( drule rtranclD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
292 |
apply( erule disjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
293 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
294 |
apply( erule conjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
295 |
apply( erule trancl_trans_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
296 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
297 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
298 |
apply( drule spec, drule spec, drule spec, erule (1) impE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
299 |
apply( fast elim: widen_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
300 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
301 |
apply( drule subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
302 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
303 |
apply( subst method_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
304 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
305 |
apply( unfold override_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
306 |
apply( simp (no_asm_simp) del: split_paired_Ex) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
307 |
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
|
308 |
apply( erule exE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
309 |
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
|
310 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
311 |
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
|
312 |
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
|
313 |
apply( simp_all (no_asm_simp) del: split_paired_Ex) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
314 |
apply( drule (1) class_wf) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
315 |
apply( simp (no_asm_simp) only: split_tupled_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
316 |
apply( unfold wf_cdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
317 |
apply( drule map_of_SomeD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
318 |
apply auto |
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 subtype_widen_methd: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
322 |
"[| 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
|
323 |
method (G,D) sig = Some (md, rT, b) |] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
324 |
==> \<exists>mD' rT' b'. method (G,C) 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
|
325 |
apply(auto dest: subcls_widen_methd method_wf_mdecl simp add: wf_mdecl_def wf_mhead_def split_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
326 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
327 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
328 |
lemma method_in_md [rule_format (no_asm)]: "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
329 |
apply (erule (1) subcls1_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
330 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
331 |
apply (erule conjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
332 |
apply (subst method_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
333 |
apply (assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
334 |
apply (assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
335 |
apply (clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
336 |
apply (erule_tac "x" = "Da" in allE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
337 |
apply (clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
338 |
apply (simp add: map_of_map) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
339 |
apply (clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
340 |
apply (subst method_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
341 |
apply (assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
342 |
apply (assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
343 |
apply (simp add: override_def map_of_map split add: option.split) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
344 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
345 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
346 |
lemma widen_methd: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
347 |
"[| 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
|
348 |
==> \<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
|
349 |
apply( drule subcls_widen_methd) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
350 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
351 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
352 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
353 |
lemma Call_lemma: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
354 |
"[|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
|
355 |
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
|
356 |
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
|
357 |
apply( drule (2) widen_methd) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
358 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
359 |
apply( frule subcls_is_class2) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
360 |
apply (unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
361 |
apply (simp (no_asm_simp)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
362 |
apply( drule method_wf_mdecl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
363 |
apply( unfold wf_mdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
364 |
apply( unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
365 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
366 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
367 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
368 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
369 |
lemma fields_is_type_lemma [rule_format (no_asm)]: "[|is_class G C; wf_prog wf_mb G|] ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
370 |
\<forall>f\<in>set (fields (G,C)). is_type G (snd f)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
371 |
apply( erule (1) subcls1_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
372 |
apply( simp (no_asm_simp)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
373 |
apply( subst fields_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
374 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
375 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
376 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
377 |
apply( safe) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
378 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
379 |
apply( force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
380 |
apply( drule (1) class_wf) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
381 |
apply( unfold wf_cdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
382 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
383 |
apply( drule (1) bspec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
384 |
apply( unfold wf_fdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
385 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
386 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
387 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
388 |
lemma fields_is_type: "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
389 |
is_type G f" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
390 |
apply(drule map_of_SomeD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
391 |
apply(drule (2) fields_is_type_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
392 |
apply(auto) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
393 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
394 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
395 |
lemma methd: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
396 |
"[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
397 |
==> 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
|
398 |
proof - |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
399 |
assume wf: "wf_prog wf_mb G" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
400 |
assume C: "(C,S,fs,mdecls) \<in> set G" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
401 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
402 |
assume m: "(sig,rT,code) \<in> set mdecls" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
403 |
moreover |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
404 |
from wf |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
405 |
have "class G Object = Some (arbitrary, [], [])" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
406 |
by simp |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
407 |
moreover |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
408 |
from wf C |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
409 |
have c: "class G C = Some (S,fs,mdecls)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
410 |
by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
411 |
ultimately |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
412 |
have O: "C \<noteq> Object" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
413 |
by auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
414 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
415 |
from wf C |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
416 |
have "unique mdecls" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
417 |
by (unfold wf_prog_def wf_cdecl_def) auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
418 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
419 |
hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
420 |
by - (induct mdecls, auto) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
421 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
422 |
with m |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
423 |
have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
424 |
by (force intro: map_of_SomeI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
425 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
426 |
with wf C m c O |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
427 |
show ?thesis |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
428 |
by (auto simp add: is_class_def dest: method_rec) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset
|
429 |
qed |
8011 | 430 |
|
431 |
end |