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