111 |
111 |
112 lemma comp_subcls1: "subcls1 (comp G) = subcls1 G" |
112 lemma comp_subcls1: "subcls1 (comp G) = subcls1 G" |
113 by (auto simp add: subcls1_def2 comp_classname comp_is_class) |
113 by (auto simp add: subcls1_def2 comp_classname comp_is_class) |
114 |
114 |
115 lemma comp_widen: "widen (comp G) = widen G" |
115 lemma comp_widen: "widen (comp G) = widen G" |
116 apply (simp add: expand_fun_eq) |
116 apply (simp add: ext_iff) |
117 apply (intro allI iffI) |
117 apply (intro allI iffI) |
118 apply (erule widen.cases) |
118 apply (erule widen.cases) |
119 apply (simp_all add: comp_subcls1 widen.null) |
119 apply (simp_all add: comp_subcls1 widen.null) |
120 apply (erule widen.cases) |
120 apply (erule widen.cases) |
121 apply (simp_all add: comp_subcls1 widen.null) |
121 apply (simp_all add: comp_subcls1 widen.null) |
122 done |
122 done |
123 |
123 |
124 lemma comp_cast: "cast (comp G) = cast G" |
124 lemma comp_cast: "cast (comp G) = cast G" |
125 apply (simp add: expand_fun_eq) |
125 apply (simp add: ext_iff) |
126 apply (intro allI iffI) |
126 apply (intro allI iffI) |
127 apply (erule cast.cases) |
127 apply (erule cast.cases) |
128 apply (simp_all add: comp_subcls1 cast.widen cast.subcls) |
128 apply (simp_all add: comp_subcls1 cast.widen cast.subcls) |
129 apply (rule cast.widen) apply (simp add: comp_widen) |
129 apply (rule cast.widen) apply (simp add: comp_widen) |
130 apply (erule cast.cases) |
130 apply (erule cast.cases) |
131 apply (simp_all add: comp_subcls1 cast.widen cast.subcls) |
131 apply (simp_all add: comp_subcls1 cast.widen cast.subcls) |
132 apply (rule cast.widen) apply (simp add: comp_widen) |
132 apply (rule cast.widen) apply (simp add: comp_widen) |
133 done |
133 done |
134 |
134 |
135 lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G" |
135 lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G" |
136 by (simp add: expand_fun_eq cast_ok_def comp_widen) |
136 by (simp add: ext_iff cast_ok_def comp_widen) |
137 |
137 |
138 |
138 |
139 lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)" |
139 lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)" |
140 by (simp add: compClass_def split_beta) |
140 by (simp add: compClass_def split_beta) |
141 |
141 |
169 apply (simp add: wf_syscls_def comp_def compClass_def split_beta) |
169 apply (simp add: wf_syscls_def comp_def compClass_def split_beta) |
170 apply (simp only: image_compose [THEN sym]) |
170 apply (simp only: image_compose [THEN sym]) |
171 apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls). |
171 apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls). |
172 (C, cno, fdls, map (compMethod G C) jmdls))) = fst") |
172 (C, cno, fdls, map (compMethod G C) jmdls))) = fst") |
173 apply (simp del: image_compose) |
173 apply (simp del: image_compose) |
174 apply (simp add: expand_fun_eq split_beta) |
174 apply (simp add: ext_iff split_beta) |
175 done |
175 done |
176 |
176 |
177 |
177 |
178 lemma comp_ws_prog: "ws_prog (comp G) = ws_prog G" |
178 lemma comp_ws_prog: "ws_prog (comp G) = ws_prog G" |
179 apply (rule sym) |
179 apply (rule sym) |
320 (s, Object, m)) |
320 (s, Object, m)) |
321 (S, Object, snd x))))) |
321 (S, Object, snd x))))) |
322 = (\<lambda>x. (fst x, Object, fst (snd x), |
322 = (\<lambda>x. (fst x, Object, fst (snd x), |
323 snd (snd (compMethod G Object (S, snd x)))))") |
323 snd (snd (compMethod G Object (S, snd x)))))") |
324 apply (simp only:) |
324 apply (simp only:) |
325 apply (simp add: expand_fun_eq) |
325 apply (simp add: ext_iff) |
326 apply (intro strip) |
326 apply (intro strip) |
327 apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)") |
327 apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)") |
328 apply (simp only:) |
328 apply (simp only:) |
329 apply (simp add: compMethod_def split_beta) |
329 apply (simp add: compMethod_def split_beta) |
330 apply (rule inv_f_eq) |
330 apply (rule inv_f_eq) |