64 Xcpt ClassCast, Xcpt OutOfMemory, Object}" |
64 Xcpt ClassCast, Xcpt OutOfMemory, Object}" |
65 by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs) |
65 by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs) |
66 |
66 |
67 text {* The subclass releation spelled out: *} |
67 text {* The subclass releation spelled out: *} |
68 lemma subcls1: |
68 lemma subcls1: |
69 "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object), |
69 "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object), |
70 (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})" |
70 (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}" |
71 apply (simp add: subcls1_def2) |
71 apply (simp add: subcls1_def2) |
72 apply (simp add: name_defs class_defs system_defs E_def class_def) |
72 apply (simp add: name_defs class_defs system_defs E_def class_def) |
73 apply (auto simp: expand_fun_eq) |
73 apply (simp add: Sigma_def) |
|
74 apply auto |
74 done |
75 done |
75 |
76 |
76 text {* The subclass relation is acyclic; hence its converse is well founded: *} |
77 text {* The subclass relation is acyclic; hence its converse is well founded: *} |
77 lemma notin_rtrancl: |
78 lemma notin_rtrancl: |
78 "r\<^sup>*\<^sup>* a b \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. \<not> r a y) \<Longrightarrow> False" |
79 "(a, b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a, y) \<notin> r) \<Longrightarrow> False" |
79 by (auto elim: converse_rtranclpE) |
80 by (auto elim: converse_rtranclE) |
80 |
81 |
81 lemma acyclic_subcls1_E: "acyclicP (subcls1 E)" |
82 lemma acyclic_subcls1_E: "acyclic (subcls1 E)" |
82 apply (rule acyclicI [to_pred]) |
83 apply (rule acyclicI) |
83 apply (simp add: subcls1) |
84 apply (simp add: subcls1) |
84 apply (auto dest!: tranclpD) |
85 apply (auto dest!: tranclD) |
85 apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes) |
86 apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes) |
86 done |
87 done |
87 |
88 |
88 lemma wf_subcls1_E: "wfP ((subcls1 E)\<inverse>\<inverse>)" |
89 lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)" |
89 apply (rule finite_acyclic_wf_converse [to_pred]) |
90 apply (rule finite_acyclic_wf_converse) |
90 apply (simp add: subcls1 del: insert_iff) |
91 apply (simp add: subcls1 del: insert_iff) |
91 apply (rule acyclic_subcls1_E) |
92 apply (rule acyclic_subcls1_E) |
92 done |
93 done |
93 |
94 |
94 text {* Method and field lookup: *} |
95 text {* Method and field lookup: *} |