13 definition subcls1 :: "(cname \<times> cname) set" |
13 definition subcls1 :: "(cname \<times> cname) set" |
14 where |
14 where |
15 "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}" |
15 "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}" |
16 |
16 |
17 abbreviation |
17 abbreviation |
18 subcls1_syntax :: "[cname, cname] => bool" ("_ \<prec>C1 _" [71,71] 70) |
18 subcls1_syntax :: "[cname, cname] => bool" (\<open>_ \<prec>C1 _\<close> [71,71] 70) |
19 where "C \<prec>C1 D == (C,D) \<in> subcls1" |
19 where "C \<prec>C1 D == (C,D) \<in> subcls1" |
20 abbreviation |
20 abbreviation |
21 subcls_syntax :: "[cname, cname] => bool" ("_ \<preceq>C _" [71,71] 70) |
21 subcls_syntax :: "[cname, cname] => bool" (\<open>_ \<preceq>C _\<close> [71,71] 70) |
22 where "C \<preceq>C D \<equiv> (C,D) \<in> subcls1\<^sup>*" |
22 where "C \<preceq>C D \<equiv> (C,D) \<in> subcls1\<^sup>*" |
23 |
23 |
24 |
24 |
25 subsection "Declarations and properties not used in the meta theory" |
25 subsection "Declarations and properties not used in the meta theory" |
26 |
26 |
27 text\<open>Widening, viz. method invocation conversion\<close> |
27 text\<open>Widening, viz. method invocation conversion\<close> |
28 inductive |
28 inductive |
29 widen :: "ty => ty => bool" ("_ \<preceq> _" [71,71] 70) |
29 widen :: "ty => ty => bool" (\<open>_ \<preceq> _\<close> [71,71] 70) |
30 where |
30 where |
31 refl [intro!, simp]: "T \<preceq> T" |
31 refl [intro!, simp]: "T \<preceq> T" |
32 | subcls: "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D" |
32 | subcls: "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D" |
33 | null [intro!]: "NT \<preceq> R" |
33 | null [intro!]: "NT \<preceq> R" |
34 |
34 |