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