12516

1 
(* Title: HOL/MicroJava/BV/Effect.thy


2 
ID: $Id$


3 
Author: Gerwin Klein


4 
Copyright 2000 Technische Universitaet Muenchen


5 
*)


6 

12911

7 
header {* \isaheader{Effect of Instructions on the State Type} *}

12516

8 

15481

9 
theory Effect


10 
imports JVMType "../JVM/JVMExceptions"


11 
begin


12 

12516

13 


14 
types


15 
succ_type = "(p_count \<times> state_type option) list"


16 


17 
text {* Program counter of successor instructions: *}


18 
consts

13006

19 
succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list"

12516

20 
primrec


21 
"succs (Load idx) pc = [pc+1]"


22 
"succs (Store idx) pc = [pc+1]"


23 
"succs (LitPush v) pc = [pc+1]"


24 
"succs (Getfield F C) pc = [pc+1]"


25 
"succs (Putfield F C) pc = [pc+1]"


26 
"succs (New C) pc = [pc+1]"


27 
"succs (Checkcast C) pc = [pc+1]"


28 
"succs Pop pc = [pc+1]"


29 
"succs Dup pc = [pc+1]"


30 
"succs Dup_x1 pc = [pc+1]"


31 
"succs Dup_x2 pc = [pc+1]"


32 
"succs Swap pc = [pc+1]"


33 
"succs IAdd pc = [pc+1]"


34 
"succs (Ifcmpeq b) pc = [pc+1, nat (int pc + b)]"


35 
"succs (Goto b) pc = [nat (int pc + b)]"


36 
"succs Return pc = [pc]"


37 
"succs (Invoke C mn fpTs) pc = [pc+1]"


38 
"succs Throw pc = [pc]"


39 


40 
text "Effect of instruction on the state type:"


41 
consts

13006

42 
eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"

12516

43 


44 
recdef eff' "{}"


45 
"eff' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)"


46 
"eff' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])"


47 
"eff' (LitPush v, G, (ST, LT)) = (the (typeof (\<lambda>v. None) v) # ST, LT)"


48 
"eff' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)"


49 
"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)"


50 
"eff' (New C, G, (ST,LT)) = (Class C # ST, LT)"


51 
"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)"


52 
"eff' (Pop, G, (ts#ST,LT)) = (ST,LT)"


53 
"eff' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)"


54 
"eff' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)"


55 
"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)"


56 
"eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)"


57 
"eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT))


58 
= (PrimT Integer#ST,LT)"


59 
"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)"


60 
"eff' (Goto b, G, s) = s"


61 
 "Return has no successor instruction in the same method"


62 
"eff' (Return, G, s) = s"


63 
 "Throw always terminates abruptly"


64 
"eff' (Throw, G, s) = s"


65 
"eff' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST


66 
in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))"


67 


68 


69 
consts


70 
match_any :: "jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list"


71 
primrec


72 
"match_any G pc [] = []"


73 
"match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e;


74 
es' = match_any G pc es


75 
in


76 
if start_pc <= pc \<and> pc < end_pc then catch_type#es' else es')"


77 

12951

78 
consts

13717

79 
match :: "jvm_prog \<Rightarrow> xcpt \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list"

12951

80 
primrec


81 
"match G X pc [] = []"


82 
"match G X pc (e#es) =

13717

83 
(if match_exception_entry G (Xcpt X) pc e then [Xcpt X] else match G X pc es)"

12951

84 


85 
lemma match_some_entry:

13717

86 
"match G X pc et = (if \<exists>e \<in> set et. match_exception_entry G (Xcpt X) pc e then [Xcpt X] else [])"

12951

87 
by (induct et) auto

12516

88 


89 
consts

13006

90 
xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table \<Rightarrow> cname list"

12516

91 
recdef xcpt_names "{}"

13717

92 
"xcpt_names (Getfield F C, G, pc, et) = match G NullPointer pc et"


93 
"xcpt_names (Putfield F C, G, pc, et) = match G NullPointer pc et"


94 
"xcpt_names (New C, G, pc, et) = match G OutOfMemory pc et"


95 
"xcpt_names (Checkcast C, G, pc, et) = match G ClassCast pc et"

12516

96 
"xcpt_names (Throw, G, pc, et) = match_any G pc et"


97 
"xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et"


98 
"xcpt_names (i, G, pc, et) = []"


99 


100 


101 
constdefs


102 
xcpt_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> state_type option \<Rightarrow> exception_table \<Rightarrow> succ_type"


103 
"xcpt_eff i G pc s et ==


104 
map (\<lambda>C. (the (match_exception_table G C pc et), case s of None \<Rightarrow> None  Some s' \<Rightarrow> Some ([Class C], snd s')))


105 
(xcpt_names (i,G,pc,et))"


106 


107 
norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"


108 
"norm_eff i G == option_map (\<lambda>s. eff' (i,G,s))"


109 

13006

110 
eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type"

12516

111 
"eff i G pc et s == (map (\<lambda>pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)"


112 

12772

113 
constdefs


114 
isPrimT :: "ty \<Rightarrow> bool"


115 
"isPrimT T == case T of PrimT T' \<Rightarrow> True  RefT T' \<Rightarrow> False"


116 


117 
isRefT :: "ty \<Rightarrow> bool"


118 
"isRefT T == case T of PrimT T' \<Rightarrow> False  RefT T' \<Rightarrow> True"


119 


120 
lemma isPrimT [simp]:


121 
"isPrimT T = (\<exists>T'. T = PrimT T')" by (simp add: isPrimT_def split: ty.splits)


122 


123 
lemma isRefT [simp]:


124 
"isRefT T = (\<exists>T'. T = RefT T')" by (simp add: isRefT_def split: ty.splits)


125 


126 


127 
lemma "list_all2 P a b \<Longrightarrow> \<forall>(x,y) \<in> set (zip a b). P x y"


128 
by (simp add: list_all2_def)


129 

12516

130 


131 
text "Conditions under which eff is applicable:"


132 
consts

13006

133 
app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type \<Rightarrow> bool"

12516

134 


135 
recdef app' "{}"

12974

136 
"app' (Load idx, G, pc, maxs, rT, s) =


137 
(idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)"


138 
"app' (Store idx, G, pc, maxs, rT, (ts#ST, LT)) =


139 
(idx < length LT)"


140 
"app' (LitPush v, G, pc, maxs, rT, s) =


141 
(length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)"


142 
"app' (Getfield F C, G, pc, maxs, rT, (oT#ST, LT)) =


143 
(is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>


144 
G \<turnstile> oT \<preceq> (Class C))"


145 
"app' (Putfield F C, G, pc, maxs, rT, (vT#oT#ST, LT)) =


146 
(is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>


147 
G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))"


148 
"app' (New C, G, pc, maxs, rT, s) =


149 
(is_class G C \<and> length (fst s) < maxs)"


150 
"app' (Checkcast C, G, pc, maxs, rT, (RefT rt#ST,LT)) =


151 
(is_class G C)"


152 
"app' (Pop, G, pc, maxs, rT, (ts#ST,LT)) =


153 
True"


154 
"app' (Dup, G, pc, maxs, rT, (ts#ST,LT)) =


155 
(1+length ST < maxs)"


156 
"app' (Dup_x1, G, pc, maxs, rT, (ts1#ts2#ST,LT)) =


157 
(2+length ST < maxs)"


158 
"app' (Dup_x2, G, pc, maxs, rT, (ts1#ts2#ts3#ST,LT)) =


159 
(3+length ST < maxs)"


160 
"app' (Swap, G, pc, maxs, rT, (ts1#ts2#ST,LT)) =


161 
True"


162 
"app' (IAdd, G, pc, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT)) =


163 
True"


164 
"app' (Ifcmpeq b, G, pc, maxs, rT, (ts#ts'#ST,LT)) =


165 
(0 \<le> int pc + b \<and> (isPrimT ts \<and> ts' = ts \<or> isRefT ts \<and> isRefT ts'))"


166 
"app' (Goto b, G, pc, maxs, rT, s) =


167 
(0 \<le> int pc + b)"


168 
"app' (Return, G, pc, maxs, rT, (T#ST,LT)) =


169 
(G \<turnstile> T \<preceq> rT)"


170 
"app' (Throw, G, pc, maxs, rT, (T#ST,LT)) =


171 
isRefT T"


172 
"app' (Invoke C mn fpTs, G, pc, maxs, rT, s) =


173 
(length fpTs < length (fst s) \<and>


174 
(let apTs = rev (take (length fpTs) (fst s));


175 
X = hd (drop (length fpTs) (fst s))


176 
in


177 
G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and>


178 
list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))"

12772

179 

12974

180 
"app' (i,G, pc,maxs,rT,s) = False"

12516

181 


182 
constdefs


183 
xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool"


184 
"xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C"


185 

13006

186 
app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> bool"


187 
"app i G maxs rT pc et s == case s of None \<Rightarrow> True  Some t \<Rightarrow> app' (i,G,pc,maxs,rT,t) \<and> xcpt_app i G pc et"

12516

188 


189 

13066

190 
lemma match_any_match_table:


191 
"C \<in> set (match_any G pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"


192 
apply (induct et)


193 
apply simp


194 
apply simp


195 
apply clarify


196 
apply (simp split: split_if_asm)


197 
apply (auto simp add: match_exception_entry_def)


198 
done


199 


200 
lemma match_X_match_table:


201 
"C \<in> set (match G X pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"


202 
apply (induct et)


203 
apply simp


204 
apply (simp split: split_if_asm)


205 
done


206 


207 
lemma xcpt_names_in_et:


208 
"C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow>


209 
\<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"


210 
apply (cases i)


211 
apply (auto dest!: match_any_match_table match_X_match_table


212 
dest: match_exception_table_in_et)


213 
done


214 


215 

13006

216 
lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"

12516

217 
proof (cases a)


218 
fix x xs assume "a = x#xs" "2 < length a"


219 
thus ?thesis by  (cases xs, simp, cases "tl xs", auto)


220 
qed auto


221 

13006

222 
lemma 2: "\<not>(2 < length a) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"

12516

223 
proof ;


224 
assume "\<not>(2 < length a)"


225 
hence "length a < (Suc (Suc (Suc 0)))" by simp


226 
hence * : "length a = 0 \<or> length a = Suc 0 \<or> length a = Suc (Suc 0)"


227 
by (auto simp add: less_Suc_eq)


228 


229 
{


230 
fix x


231 
assume "length x = Suc 0"


232 
hence "\<exists> l. x = [l]" by  (cases x, auto)


233 
} note 0 = this


234 

13006

235 
have "length a = Suc (Suc 0) \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)

12516

236 
with * show ?thesis by (auto dest: 0)


237 
qed


238 


239 
lemmas [simp] = app_def xcpt_app_def


240 


241 
text {*


242 
\medskip


243 
simp rules for @{term app}


244 
*}


245 
lemma appNone[simp]: "app i G maxs rT pc et None = True" by simp


246 


247 


248 
lemma appLoad[simp]:


249 
"(app (Load idx) G maxs rT pc et (Some s)) = (\<exists>ST LT. s = (ST,LT) \<and> idx < length LT \<and> LT!idx \<noteq> Err \<and> length ST < maxs)"


250 
by (cases s, simp)


251 


252 
lemma appStore[simp]:


253 
"(app (Store idx) G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"


254 
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)


255 


256 
lemma appLitPush[simp]:


257 
"(app (LitPush v) G maxs rT pc et (Some s)) = (\<exists>ST LT. s = (ST,LT) \<and> length ST < maxs \<and> typeof (\<lambda>v. None) v \<noteq> None)"


258 
by (cases s, simp)


259 


260 
lemma appGetField[simp]:


261 
"(app (Getfield F C) G maxs rT pc et (Some s)) =


262 
(\<exists> oT vT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and>

13717

263 
field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (Class C) \<and> (\<forall>x \<in> set (match G NullPointer pc et). is_class G x))"

12516

264 
by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)


265 


266 
lemma appPutField[simp]:


267 
"(app (Putfield F C) G maxs rT pc et (Some s)) =


268 
(\<exists> vT vT' oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and>

12951

269 
field (G,C) F = Some (C, vT') \<and> G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> vT' \<and>

13717

270 
(\<forall>x \<in> set (match G NullPointer pc et). is_class G x))"

12516

271 
by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)


272 


273 
lemma appNew[simp]:


274 
"(app (New C) G maxs rT pc et (Some s)) =

12951

275 
(\<exists>ST LT. s=(ST,LT) \<and> is_class G C \<and> length ST < maxs \<and>

13717

276 
(\<forall>x \<in> set (match G OutOfMemory pc et). is_class G x))"

12516

277 
by (cases s, simp)


278 


279 
lemma appCheckcast[simp]:


280 
"(app (Checkcast C) G maxs rT pc et (Some s)) =

12951

281 
(\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and>

13717

282 
(\<forall>x \<in> set (match G ClassCast pc et). is_class G x))"

12516

283 
by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)


284 


285 
lemma appPop[simp]:


286 
"(app Pop G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))"


287 
by (cases s, cases "2 <length (fst s)", auto dest: 1 2)


288 


289 


290 
lemma appDup[simp]:


291 
"(app Dup G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT) \<and> 1+length ST < maxs)"


292 
by (cases s, cases "2 <length (fst s)", auto dest: 1 2)


293 


294 


295 
lemma appDup_x1[simp]:


296 
"(app Dup_x1 G maxs rT pc et (Some s)) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 2+length ST < maxs)"


297 
by (cases s, cases "2 <length (fst s)", auto dest: 1 2)


298 


299 


300 
lemma appDup_x2[simp]:


301 
"(app Dup_x2 G maxs rT pc et (Some s)) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT) \<and> 3+length ST < maxs)"


302 
by (cases s, cases "2 <length (fst s)", auto dest: 1 2)


303 


304 


305 
lemma appSwap[simp]:


306 
"app Swap G maxs rT pc et (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"


307 
by (cases s, cases "2 <length (fst s)", auto dest: 1 2)


308 


309 


310 
lemma appIAdd[simp]:


311 
"app IAdd G maxs rT pc et (Some s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))"


312 
(is "?app s = ?P s")


313 
proof (cases (open) s)


314 
case Pair


315 
have "?app (a,b) = ?P (a,b)"


316 
proof (cases "a")


317 
fix t ts assume a: "a = t#ts"


318 
show ?thesis


319 
proof (cases t)


320 
fix p assume p: "t = PrimT p"


321 
show ?thesis


322 
proof (cases p)


323 
assume ip: "p = Integer"


324 
show ?thesis


325 
proof (cases ts)


326 
fix t' ts' assume t': "ts = t' # ts'"


327 
show ?thesis


328 
proof (cases t')


329 
fix p' assume "t' = PrimT p'"


330 
with t' ip p a


331 
show ?thesis by  (cases p', auto)


332 
qed (auto simp add: a p ip t')


333 
qed (auto simp add: a p ip)


334 
qed (auto simp add: a p)


335 
qed (auto simp add: a)


336 
qed auto


337 
with Pair show ?thesis by simp


338 
qed


339 


340 


341 
lemma appIfcmpeq[simp]:

12974

342 
"app (Ifcmpeq b) G maxs rT pc et (Some s) =


343 
(\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 0 \<le> int pc + b \<and>


344 
((\<exists> p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or> (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))"

12772

345 
by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)

12516

346 


347 
lemma appReturn[simp]:


348 
"app Return G maxs rT pc et (Some s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))"


349 
by (cases s, cases "2 <length (fst s)", auto dest: 1 2)


350 


351 
lemma appGoto[simp]:

12974

352 
"app (Goto b) G maxs rT pc et (Some s) = (0 \<le> int pc + b)"

12516

353 
by simp


354 


355 
lemma appThrow[simp]:


356 
"app Throw G maxs rT pc et (Some s) =


357 
(\<exists>T ST LT r. s=(T#ST,LT) \<and> T = RefT r \<and> (\<forall>C \<in> set (match_any G pc et). is_class G C))"


358 
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)


359 


360 
lemma appInvoke[simp]:


361 
"app (Invoke C mn fpTs) G maxs rT pc et (Some s) = (\<exists>apTs X ST LT mD' rT' b'.


362 
s = ((rev apTs) @ (X # ST), LT) \<and> length apTs = length fpTs \<and> is_class G C \<and>


363 
G \<turnstile> X \<preceq> Class C \<and> (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>


364 
method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and>


365 
(\<forall>C \<in> set (match_any G pc et). is_class G C))" (is "?app s = ?P s")


366 
proof (cases (open) s)

12772

367 
note list_all2_def [simp]

12516

368 
case Pair

13006

369 
have "?app (a,b) \<Longrightarrow> ?P (a,b)"

12516

370 
proof 


371 
assume app: "?app (a,b)"


372 
hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and>


373 
length fpTs < length a" (is "?a \<and> ?l")


374 
by (auto simp add: app_def)


375 
hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l")


376 
by auto


377 
hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs"


378 
by (auto simp add: min_def)


379 
hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST"


380 
by blast


381 
hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []"


382 
by blast


383 
hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and>


384 
(\<exists>X ST'. ST = X#ST')"


385 
by (simp add: neq_Nil_conv)


386 
hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs"


387 
by blast


388 
with app


389 
show ?thesis by (unfold app_def, clarsimp) blast


390 
qed


391 
with Pair

12772

392 
have "?app s \<Longrightarrow> ?P s" by (simp only:)

12516

393 
moreover

12772

394 
have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp simp add: min_def)

12516

395 
ultimately

12772

396 
show ?thesis by (rule iffI)

12516

397 
qed


398 


399 
lemma effNone:


400 
"(pc', s') \<in> set (eff i G pc et None) \<Longrightarrow> s' = None"


401 
by (auto simp add: eff_def xcpt_eff_def norm_eff_def)


402 

12772

403 


404 
text {* some helpers to make the specification directly executable: *}


405 
declare list_all2_Nil [code]


406 
declare list_all2_Cons [code]


407 


408 
lemma xcpt_app_lemma [code]:


409 
"xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))"

17088

410 
by (simp add: list_all_iff)

12772

411 

12516

412 
lemmas [simp del] = app_def xcpt_app_def


413 


414 
end
