author | haftmann |
Mon, 01 Mar 2010 13:40:23 +0100 | |
changeset 35416 | d8d7d1b785af |
parent 35102 | cc7a0b9f938c |
child 41589 | bbd861837ebc |
permissions | -rw-r--r-- |
11376 | 1 |
(* Title: HOL/NanoJava/TypeRel.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 2001 Technische Universitaet Muenchen |
|
5 |
*) |
|
6 |
||
7 |
header "Type relations" |
|
8 |
||
16417 | 9 |
theory TypeRel imports Decl begin |
11376 | 10 |
|
11 |
consts |
|
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11376
diff
changeset
|
12 |
subcls1 :: "(cname \<times> cname) set" --{* subclass *} |
11376 | 13 |
|
35102 | 14 |
abbreviation |
15 |
subcls1_syntax :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70) |
|
16 |
where "C <=C1 D == (C,D) \<in> subcls1" |
|
17 |
abbreviation |
|
18 |
subcls_syntax :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70) |
|
19 |
where "C <=C D == (C,D) \<in> subcls1^*" |
|
11376 | 20 |
|
35102 | 21 |
notation (xsymbols) |
22 |
subcls1_syntax ("_ \<prec>C1 _" [71,71] 70) and |
|
23 |
subcls_syntax ("_ \<preceq>C _" [71,71] 70) |
|
11376 | 24 |
|
25 |
consts |
|
14134 | 26 |
method :: "cname => (mname \<rightharpoonup> methd)" |
27 |
field :: "cname => (fname \<rightharpoonup> ty)" |
|
11376 | 28 |
|
29 |
||
11565 | 30 |
subsection "Declarations and properties not used in the meta theory" |
11376 | 31 |
|
11565 | 32 |
text{* Direct subclass relation *} |
11376 | 33 |
defs |
34 |
subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}" |
|
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11376
diff
changeset
|
35 |
|
11565 | 36 |
text{* Widening, viz. method invocation conversion *} |
23755 | 37 |
inductive |
38 |
widen :: "ty => ty => bool" ("_ \<preceq> _" [71,71] 70) |
|
39 |
where |
|
40 |
refl [intro!, simp]: "T \<preceq> T" |
|
41 |
| subcls: "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D" |
|
42 |
| null [intro!]: "NT \<preceq> R" |
|
11376 | 43 |
|
44 |
lemma subcls1D: |
|
45 |
"C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)" |
|
46 |
apply (unfold subcls1_def) |
|
47 |
apply auto |
|
48 |
done |
|
49 |
||
50 |
lemma subcls1I: "\<lbrakk>class C = Some m; super m = D; C \<noteq> Object\<rbrakk> \<Longrightarrow> C\<prec>C1D" |
|
51 |
apply (unfold subcls1_def) |
|
52 |
apply auto |
|
53 |
done |
|
54 |
||
55 |
lemma subcls1_def2: |
|
14952
47455995693d
removal of x-symbol syntax <Sigma> for dependent products
paulson
parents:
14171
diff
changeset
|
56 |
"subcls1 = |
47455995693d
removal of x-symbol syntax <Sigma> for dependent products
paulson
parents:
14171
diff
changeset
|
57 |
(SIGMA C: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})" |
11376 | 58 |
apply (unfold subcls1_def is_class_def) |
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
28524
diff
changeset
|
59 |
apply (auto split:split_if_asm) |
11376 | 60 |
done |
61 |
||
62 |
lemma finite_subcls1: "finite subcls1" |
|
63 |
apply(subst subcls1_def2) |
|
64 |
apply(rule finite_SigmaI [OF finite_is_class]) |
|
65 |
apply(rule_tac B = "{super (the (class C))}" in finite_subset) |
|
66 |
apply auto |
|
67 |
done |
|
68 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
69 |
definition ws_prog :: "bool" where |
11376 | 70 |
"ws_prog \<equiv> \<forall>(C,c)\<in>set Prog. C\<noteq>Object \<longrightarrow> |
71 |
is_class (super c) \<and> (super c,C)\<notin>subcls1^+" |
|
72 |
||
73 |
lemma ws_progD: "\<lbrakk>class C = Some c; C\<noteq>Object; ws_prog\<rbrakk> \<Longrightarrow> |
|
74 |
is_class (super c) \<and> (super c,C)\<notin>subcls1^+" |
|
75 |
apply (unfold ws_prog_def class_def) |
|
76 |
apply (drule_tac map_of_SomeD) |
|
77 |
apply auto |
|
78 |
done |
|
79 |
||
80 |
lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}" |
|
81 |
by (fast dest: subcls1D ws_progD) |
|
82 |
||
13867 | 83 |
(* irrefl_tranclI in Transitive_Closure.thy is more general *) |
11376 | 84 |
lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+" |
13867 | 85 |
by(blast elim: tranclE dest: trancl_into_rtrancl) |
86 |
||
11376 | 87 |
|
88 |
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI'] |
|
89 |
||
90 |
lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1; ws_prog\<rbrakk> \<Longrightarrow> x \<noteq> y" |
|
91 |
apply (rule irrefl_trancl_rD) |
|
92 |
apply (rule subcls1_irrefl_lemma2) |
|
93 |
apply auto |
|
94 |
done |
|
95 |
||
96 |
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard] |
|
97 |
||
98 |
lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)" |
|
99 |
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic) |
|
100 |
||
101 |
||
14134 | 102 |
consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<rightharpoonup> 'b)" |
11376 | 103 |
|
11626 | 104 |
recdef (permissive) class_rec "subcls1\<inverse>" |
28524 | 105 |
"class_rec C = (\<lambda>f. case class C of None \<Rightarrow> undefined |
11376 | 106 |
| Some m \<Rightarrow> if wf (subcls1\<inverse>) |
107 |
then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m) |
|
28524 | 108 |
else undefined)" |
11376 | 109 |
(hints intro: subcls1I) |
110 |
||
111 |
lemma class_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> |
|
112 |
class_rec C f = (if C = Object then empty else class_rec (super m) f) ++ |
|
113 |
map_of (f m)"; |
|
114 |
apply (drule wf_subcls1) |
|
115 |
apply (rule class_rec.simps [THEN trans [THEN fun_cong]]) |
|
116 |
apply assumption |
|
117 |
apply simp |
|
118 |
done |
|
119 |
||
11565 | 120 |
--{* Methods of a class, with inheritance and hiding *} |
11376 | 121 |
defs method_def: "method C \<equiv> class_rec C methods" |
122 |
||
123 |
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> |
|
124 |
method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)" |
|
125 |
apply (unfold method_def) |
|
126 |
apply (erule (1) class_rec [THEN trans]); |
|
127 |
apply simp |
|
128 |
done |
|
129 |
||
130 |
||
11565 | 131 |
--{* Fields of a class, with inheritance and hiding *} |
12264
9c356e2da72f
renamed "fields" to "flds" (avoid clash with new "fields" operation);
wenzelm
parents:
11626
diff
changeset
|
132 |
defs field_def: "field C \<equiv> class_rec C flds" |
11376 | 133 |
|
12264
9c356e2da72f
renamed "fields" to "flds" (avoid clash with new "fields" operation);
wenzelm
parents:
11626
diff
changeset
|
134 |
lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> |
9c356e2da72f
renamed "fields" to "flds" (avoid clash with new "fields" operation);
wenzelm
parents:
11626
diff
changeset
|
135 |
field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)" |
11376 | 136 |
apply (unfold field_def) |
137 |
apply (erule (1) class_rec [THEN trans]); |
|
138 |
apply simp |
|
139 |
done |
|
140 |
||
141 |
end |