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 |
|
|
9 |
theory TypeRel = Decl:
|
|
10 |
|
|
11 |
consts
|
|
12 |
widen :: "(ty \<times> ty ) set" (* widening *)
|
|
13 |
subcls1 :: "(cname \<times> cname) set" (* subclass *)
|
|
14 |
|
|
15 |
syntax (xsymbols)
|
|
16 |
widen :: "[ty , ty ] => bool" ("_ \<preceq> _" [71,71] 70)
|
|
17 |
subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _" [71,71] 70)
|
|
18 |
subcls :: "[cname, cname] => bool" ("_ \<preceq>C _" [71,71] 70)
|
|
19 |
syntax
|
|
20 |
widen :: "[ty , ty ] => bool" ("_ <= _" [71,71] 70)
|
|
21 |
subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
|
|
22 |
subcls :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70)
|
|
23 |
|
|
24 |
translations
|
|
25 |
"C \<prec>C1 D" == "(C,D) \<in> subcls1"
|
|
26 |
"C \<preceq>C D" == "(C,D) \<in> subcls1^*"
|
|
27 |
"S \<preceq> T" == "(S,T) \<in> widen"
|
|
28 |
|
|
29 |
consts
|
|
30 |
method :: "cname => (mname \<leadsto> methd)"
|
|
31 |
field :: "cname => (vnam \<leadsto> ty)"
|
|
32 |
|
|
33 |
|
|
34 |
text {* The rest of this theory is not actually used. *}
|
|
35 |
|
|
36 |
defs
|
|
37 |
(* direct subclass relation *)
|
|
38 |
subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
|
|
39 |
|
|
40 |
inductive widen intros (*widening, viz. method invocation conversion,
|
|
41 |
i.e. sort of syntactic subtyping *)
|
|
42 |
refl [intro!, simp]: "T \<preceq> T"
|
|
43 |
subcls : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
|
|
44 |
null [intro!]: "NT \<preceq> R"
|
|
45 |
|
|
46 |
lemma subcls1D:
|
|
47 |
"C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)"
|
|
48 |
apply (unfold subcls1_def)
|
|
49 |
apply auto
|
|
50 |
done
|
|
51 |
|
|
52 |
lemma subcls1I: "\<lbrakk>class C = Some m; super m = D; C \<noteq> Object\<rbrakk> \<Longrightarrow> C\<prec>C1D"
|
|
53 |
apply (unfold subcls1_def)
|
|
54 |
apply auto
|
|
55 |
done
|
|
56 |
|
|
57 |
lemma subcls1_def2:
|
|
58 |
"subcls1 = (\<Sigma>C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
|
|
59 |
apply (unfold subcls1_def is_class_def)
|
|
60 |
apply auto
|
|
61 |
done
|
|
62 |
|
|
63 |
lemma finite_subcls1: "finite subcls1"
|
|
64 |
apply(subst subcls1_def2)
|
|
65 |
apply(rule finite_SigmaI [OF finite_is_class])
|
|
66 |
apply(rule_tac B = "{super (the (class C))}" in finite_subset)
|
|
67 |
apply auto
|
|
68 |
done
|
|
69 |
|
|
70 |
constdefs
|
|
71 |
|
|
72 |
ws_prog :: "bool"
|
|
73 |
"ws_prog \<equiv> \<forall>(C,c)\<in>set Prog. C\<noteq>Object \<longrightarrow>
|
|
74 |
is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
|
|
75 |
|
|
76 |
lemma ws_progD: "\<lbrakk>class C = Some c; C\<noteq>Object; ws_prog\<rbrakk> \<Longrightarrow>
|
|
77 |
is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
|
|
78 |
apply (unfold ws_prog_def class_def)
|
|
79 |
apply (drule_tac map_of_SomeD)
|
|
80 |
apply auto
|
|
81 |
done
|
|
82 |
|
|
83 |
lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}"
|
|
84 |
by (fast dest: subcls1D ws_progD)
|
|
85 |
|
|
86 |
(* context (theory "Transitive_Closure") *)
|
|
87 |
lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
|
|
88 |
apply (rule allI)
|
|
89 |
apply (erule irrefl_tranclI)
|
|
90 |
done
|
|
91 |
|
|
92 |
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
|
|
93 |
|
|
94 |
lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1; ws_prog\<rbrakk> \<Longrightarrow> x \<noteq> y"
|
|
95 |
apply (rule irrefl_trancl_rD)
|
|
96 |
apply (rule subcls1_irrefl_lemma2)
|
|
97 |
apply auto
|
|
98 |
done
|
|
99 |
|
|
100 |
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
|
|
101 |
|
|
102 |
lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)"
|
|
103 |
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
|
|
104 |
|
|
105 |
|
|
106 |
consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<leadsto> 'b)"
|
|
107 |
|
|
108 |
recdef class_rec "subcls1\<inverse>"
|
|
109 |
"class_rec C = (\<lambda>f. case class C of None \<Rightarrow> arbitrary
|
|
110 |
| Some m \<Rightarrow> if wf (subcls1\<inverse>)
|
|
111 |
then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m)
|
|
112 |
else arbitrary)"
|
|
113 |
(hints intro: subcls1I)
|
|
114 |
|
|
115 |
lemma class_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
|
|
116 |
class_rec C f = (if C = Object then empty else class_rec (super m) f) ++
|
|
117 |
map_of (f m)";
|
|
118 |
apply (drule wf_subcls1)
|
|
119 |
apply (rule class_rec.simps [THEN trans [THEN fun_cong]])
|
|
120 |
apply assumption
|
|
121 |
apply simp
|
|
122 |
done
|
|
123 |
|
|
124 |
(* methods of a class, with inheritance and hiding *)
|
|
125 |
defs method_def: "method C \<equiv> class_rec C methods"
|
|
126 |
|
|
127 |
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
|
|
128 |
method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
|
|
129 |
apply (unfold method_def)
|
|
130 |
apply (erule (1) class_rec [THEN trans]);
|
|
131 |
apply simp
|
|
132 |
done
|
|
133 |
|
|
134 |
|
|
135 |
(* fields of a class, with inheritance and hiding *)
|
|
136 |
defs field_def: "field C \<equiv> class_rec C fields"
|
|
137 |
|
|
138 |
lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
|
|
139 |
field C = (if C=Object then empty else field (super m)) ++ map_of (fields m)"
|
|
140 |
apply (unfold field_def)
|
|
141 |
apply (erule (1) class_rec [THEN trans]);
|
|
142 |
apply simp
|
|
143 |
done
|
|
144 |
|
|
145 |
end
|