5 *) |
5 *) |
6 |
6 |
7 header {* Effect of instructions on the state type *} |
7 header {* Effect of instructions on the state type *} |
8 |
8 |
9 |
9 |
10 theory Step = Convert : |
10 theory Step = Convert: |
11 |
11 |
12 |
12 |
13 text "Effect of instruction on the state type:" |
13 text "Effect of instruction on the state type:" |
14 consts |
14 consts |
15 step :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type option" |
15 step' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type" |
16 |
16 |
17 recdef step "{}" |
17 recdef step' "{}" |
18 "step (Load idx, G, (ST, LT)) = Some (the (LT ! idx) # ST, LT)" |
18 "step' (Load idx, G, (ST, LT)) = (val (LT ! idx) # ST, LT)" |
19 "step (Store idx, G, (ts#ST, LT)) = Some (ST, LT[idx:= Some ts])" |
19 "step' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= Ok ts])" |
20 "step (Bipush i, G, (ST, LT)) = Some (PrimT Integer # ST, LT)" |
20 "step' (Bipush i, G, (ST, LT)) = (PrimT Integer # ST, LT)" |
21 "step (Aconst_null, G, (ST, LT)) = Some (NT#ST,LT)" |
21 "step' (Aconst_null, G, (ST, LT)) = (NT#ST,LT)" |
22 "step (Getfield F C, G, (oT#ST, LT)) = Some (snd (the (field (G,C) F)) # ST, LT)" |
22 "step' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)" |
23 "step (Putfield F C, G, (vT#oT#ST, LT)) = Some (ST,LT)" |
23 "step' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)" |
24 "step (New C, G, (ST,LT)) = Some (Class C # ST, LT)" |
24 "step' (New C, G, (ST,LT)) = (Class C # ST, LT)" |
25 "step (Checkcast C, G, (RefT rt#ST,LT)) = Some (Class C # ST,LT)" |
25 "step' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)" |
26 "step (Pop, G, (ts#ST,LT)) = Some (ST,LT)" |
26 "step' (Pop, G, (ts#ST,LT)) = (ST,LT)" |
27 "step (Dup, G, (ts#ST,LT)) = Some (ts#ts#ST,LT)" |
27 "step' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)" |
28 "step (Dup_x1, G, (ts1#ts2#ST,LT)) = Some (ts1#ts2#ts1#ST,LT)" |
28 "step' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)" |
29 "step (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = Some (ts1#ts2#ts3#ts1#ST,LT)" |
29 "step' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)" |
30 "step (Swap, G, (ts1#ts2#ST,LT)) = Some (ts2#ts1#ST,LT)" |
30 "step' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)" |
31 "step (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) |
31 "step' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) |
32 = Some (PrimT Integer#ST,LT)" |
32 = (PrimT Integer#ST,LT)" |
33 "step (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = Some (ST,LT)" |
33 "step' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)" |
34 "step (Goto b, G, s) = Some s" |
34 "step' (Goto b, G, s) = s" |
35 "step (Return, G, (T#ST,LT)) = None" (* Return has no successor instruction in the same method *) |
35 (* Return has no successor instruction in the same method: *) |
36 "step (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST in |
36 (* "step' (Return, G, (T#ST,LT)) = None" *) |
37 Some (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" |
37 "step' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST |
38 |
38 in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" |
39 "step (i,G,s) = None" |
39 |
|
40 (* "step' (i,G,s) = None" *) |
|
41 |
|
42 constdefs |
|
43 step :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option" |
|
44 "step i G \<equiv> opt_map (\<lambda>s. step' (i,G,s))" |
40 |
45 |
41 |
46 |
42 text "Conditions under which step is applicable:" |
47 text "Conditions under which step is applicable:" |
43 consts |
48 consts |
44 app :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool" |
49 app' :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool" |
45 |
50 |
46 recdef app "{}" |
51 recdef app' "{}" |
47 "app (Load idx, G, rT, s) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> None)" |
52 "app' (Load idx, G, rT, s) = (idx < length (snd s) \<and> |
48 "app (Store idx, G, rT, (ts#ST, LT)) = (idx < length LT)" |
53 (snd s) ! idx \<noteq> Err)" |
49 "app (Bipush i, G, rT, s) = True" |
54 "app' (Store idx, G, rT, (ts#ST, LT)) = (idx < length LT)" |
50 "app (Aconst_null, G, rT, s) = True" |
55 "app' (Bipush i, G, rT, s) = True" |
51 "app (Getfield F C, G, rT, (oT#ST, LT)) = (is_class G C \<and> |
56 "app' (Aconst_null, G, rT, s) = True" |
|
57 "app' (Getfield F C, G, rT, (oT#ST, LT)) = (is_class G C \<and> |
52 field (G,C) F \<noteq> None \<and> |
58 field (G,C) F \<noteq> None \<and> |
53 fst (the (field (G,C) F)) = C \<and> |
59 fst (the (field (G,C) F)) = C \<and> |
54 G \<turnstile> oT \<preceq> (Class C))" |
60 G \<turnstile> oT \<preceq> (Class C))" |
55 "app (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \<and> |
61 "app' (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \<and> |
56 field (G,C) F \<noteq> None \<and> |
62 field (G,C) F \<noteq> None \<and> |
57 fst (the (field (G,C) F)) = C \<and> |
63 fst (the (field (G,C) F)) = C \<and> |
58 G \<turnstile> oT \<preceq> (Class C) \<and> |
64 G \<turnstile> oT \<preceq> (Class C) \<and> |
59 G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" |
65 G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" |
60 "app (New C, G, rT, s) = (is_class G C)" |
66 "app' (New C, G, rT, s) = (is_class G C)" |
61 "app (Checkcast C, G, rT, (RefT rt#ST,LT)) = (is_class G C)" |
67 "app' (Checkcast C, G, rT, (RefT rt#ST,LT)) = (is_class G C)" |
62 "app (Pop, G, rT, (ts#ST,LT)) = True" |
68 "app' (Pop, G, rT, (ts#ST,LT)) = True" |
63 "app (Dup, G, rT, (ts#ST,LT)) = True" |
69 "app' (Dup, G, rT, (ts#ST,LT)) = True" |
64 "app (Dup_x1, G, rT, (ts1#ts2#ST,LT)) = True" |
70 "app' (Dup_x1, G, rT, (ts1#ts2#ST,LT)) = True" |
65 "app (Dup_x2, G, rT, (ts1#ts2#ts3#ST,LT)) = True" |
71 "app' (Dup_x2, G, rT, (ts1#ts2#ts3#ST,LT)) = True" |
66 "app (Swap, G, rT, (ts1#ts2#ST,LT)) = True" |
72 "app' (Swap, G, rT, (ts1#ts2#ST,LT)) = True" |
67 "app (IAdd, G, rT, (PrimT Integer#PrimT Integer#ST,LT)) |
73 "app' (IAdd, G, rT, (PrimT Integer#PrimT Integer#ST,LT)) |
68 = True" |
74 = True" |
69 "app (Ifcmpeq b, G, rT, (ts1#ts2#ST,LT)) = ((\<exists> p. ts1 = PrimT p \<and> ts1 = PrimT p) \<or> |
75 "app' (Ifcmpeq b, G, rT, (ts#ts'#ST,LT)) = ((\<exists>p. ts = PrimT p \<and> ts' = PrimT p) \<or> |
70 (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r'))" |
76 (\<exists>r r'. ts = RefT r \<and> ts' = RefT r'))" |
71 "app (Goto b, G, rT, s) = True" |
77 "app' (Goto b, G, rT, s) = True" |
72 "app (Return, G, rT, (T#ST,LT)) = (G \<turnstile> T \<preceq> rT)" |
78 "app' (Return, G, rT, (T#ST,LT)) = (G \<turnstile> T \<preceq> rT)" |
73 app_invoke: |
79 "app' (Invoke C mn fpTs, G, rT, s) = |
74 "app (Invoke C mn fpTs, G, rT, s) = (length fpTs < length (fst s) \<and> |
80 (length fpTs < length (fst s) \<and> |
75 (let |
81 (let apTs = rev (take (length fpTs) (fst s)); |
76 apTs = rev (take (length fpTs) (fst s)); |
82 X = hd (drop (length fpTs) (fst s)) |
77 X = hd (drop (length fpTs) (fst s)) |
83 in |
78 in |
84 G \<turnstile> X \<preceq> Class C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and> |
79 G \<turnstile> X \<preceq> Class C \<and> |
85 (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT)))" |
80 (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> |
86 |
81 method (G,C) (mn,fpTs) \<noteq> None |
87 "app' (i,G,rT,s) = False" |
82 ))" |
88 |
83 |
89 |
84 "app (i,G,rT,s) = False" |
90 constdefs |
85 |
91 app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> ty \<Rightarrow> state_type option \<Rightarrow> bool" |
|
92 "app i G rT s \<equiv> case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,rT,t)" |
86 |
93 |
87 text {* program counter of successor instructions: *} |
94 text {* program counter of successor instructions: *} |
88 |
95 |
89 consts |
96 consts |
90 succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count set" |
97 succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list" |
91 |
98 |
92 primrec |
99 primrec |
93 "succs (Load idx) pc = {pc+1}" |
100 "succs (Load idx) pc = [pc+1]" |
94 "succs (Store idx) pc = {pc+1}" |
101 "succs (Store idx) pc = [pc+1]" |
95 "succs (Bipush i) pc = {pc+1}" |
102 "succs (Bipush i) pc = [pc+1]" |
96 "succs (Aconst_null) pc = {pc+1}" |
103 "succs (Aconst_null) pc = [pc+1]" |
97 "succs (Getfield F C) pc = {pc+1}" |
104 "succs (Getfield F C) pc = [pc+1]" |
98 "succs (Putfield F C) pc = {pc+1}" |
105 "succs (Putfield F C) pc = [pc+1]" |
99 "succs (New C) pc = {pc+1}" |
106 "succs (New C) pc = [pc+1]" |
100 "succs (Checkcast C) pc = {pc+1}" |
107 "succs (Checkcast C) pc = [pc+1]" |
101 "succs Pop pc = {pc+1}" |
108 "succs Pop pc = [pc+1]" |
102 "succs Dup pc = {pc+1}" |
109 "succs Dup pc = [pc+1]" |
103 "succs Dup_x1 pc = {pc+1}" |
110 "succs Dup_x1 pc = [pc+1]" |
104 "succs Dup_x2 pc = {pc+1}" |
111 "succs Dup_x2 pc = [pc+1]" |
105 "succs Swap pc = {pc+1}" |
112 "succs Swap pc = [pc+1]" |
106 "succs IAdd pc = {pc+1}" |
113 "succs IAdd pc = [pc+1]" |
107 "succs (Ifcmpeq b) pc = {pc+1, nat (int pc + b)}" |
114 "succs (Ifcmpeq b) pc = [pc+1, nat (int pc + b)]" |
108 "succs (Goto b) pc = {nat (int pc + b)}" |
115 "succs (Goto b) pc = [nat (int pc + b)]" |
109 "succs Return pc = {}" |
116 "succs Return pc = []" |
110 "succs (Invoke C mn fpTs) pc = {pc+1}" |
117 "succs (Invoke C mn fpTs) pc = [pc+1]" |
111 |
118 |
112 |
119 |
113 lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)" |
120 lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)" |
114 proof (cases a) |
121 proof (cases a) |
115 fix x xs assume "a = x#xs" "2 < length a" |
122 fix x xs assume "a = x#xs" "2 < length a" |
132 with * show ?thesis by (auto dest: 0) |
140 with * show ?thesis by (auto dest: 0) |
133 qed |
141 qed |
134 |
142 |
135 text {* |
143 text {* |
136 \medskip |
144 \medskip |
137 simp rules for \isa{app} without patterns, better suited for proofs: |
145 simp rules for @{term app} |
138 *} |
146 *} |
|
147 lemma appNone[simp]: |
|
148 "app i G rT None = True" |
|
149 by (simp add: app_def) |
|
150 |
|
151 |
|
152 |
|
153 lemma appLoad[simp]: |
|
154 "(app (Load idx) G rT (Some s)) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err)" |
|
155 by (simp add: app_def) |
|
156 |
139 lemma appStore[simp]: |
157 lemma appStore[simp]: |
140 "app (Store idx, G, rT, s) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)" |
158 "(app (Store idx) G rT (Some s)) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)" |
141 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
159 by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) |
142 |
160 |
|
161 lemma appBipush[simp]: |
|
162 "(app (Bipush i) G rT (Some s)) = True" |
|
163 by (simp add: app_def) |
|
164 |
|
165 lemma appAconst[simp]: |
|
166 "(app Aconst_null G rT (Some s)) = True" |
|
167 by (simp add: app_def) |
143 |
168 |
144 lemma appGetField[simp]: |
169 lemma appGetField[simp]: |
145 "app (Getfield F C, G, rT, s) = (\<exists> oT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and> |
170 "(app (Getfield F C) G rT (Some s)) = |
146 fst (the (field (G,C) F)) = C \<and> |
171 (\<exists> oT vT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and> |
147 field (G,C) F \<noteq> None \<and> G \<turnstile> oT \<preceq> (Class C))" |
172 field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (Class C))" |
148 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
173 by (cases s, cases "2 < length (fst s)", auto dest!: 1 2 simp add: app_def) |
149 |
|
150 |
174 |
151 lemma appPutField[simp]: |
175 lemma appPutField[simp]: |
152 "app (Putfield F C, G, rT, s) = (\<exists> vT oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and> |
176 "(app (Putfield F C) G rT (Some s)) = |
153 field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and> |
177 (\<exists> vT vT' oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and> |
154 G \<turnstile> oT \<preceq> (Class C) \<and> |
178 field (G,C) F = Some (C, vT') \<and> G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> vT')" |
155 G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" |
179 by (cases s, cases "2 < length (fst s)", auto dest!: 1 2 simp add: app_def) |
156 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
180 |
157 |
181 lemma appNew[simp]: |
|
182 "(app (New C) G rT (Some s)) = is_class G C" |
|
183 by (simp add: app_def) |
158 |
184 |
159 lemma appCheckcast[simp]: |
185 lemma appCheckcast[simp]: |
160 "app (Checkcast C, G, rT, s) = (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C)" |
186 "(app (Checkcast C) G rT (Some s)) = (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C)" |
161 by (cases s, cases "fst s", simp, cases "hd (fst s)", auto) |
187 by (cases s, cases "fst s", simp add: app_def) |
|
188 (cases "hd (fst s)", auto simp add: app_def) |
162 |
189 |
163 lemma appPop[simp]: |
190 lemma appPop[simp]: |
164 "app (Pop, G, rT, s) = (\<exists>ts ST LT. s = (ts#ST,LT))" |
191 "(app Pop G rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))" |
165 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
192 by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) |
166 |
193 |
167 |
194 |
168 lemma appDup[simp]: |
195 lemma appDup[simp]: |
169 "app (Dup, G, rT, s) = (\<exists>ts ST LT. s = (ts#ST,LT))" |
196 "(app Dup G rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))" |
170 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
197 by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) |
171 |
198 |
172 |
199 |
173 lemma appDup_x1[simp]: |
200 lemma appDup_x1[simp]: |
174 "app (Dup_x1, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" |
201 "(app Dup_x1 G rT (Some s)) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" |
175 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
202 by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) |
176 |
203 |
177 |
204 |
178 lemma appDup_x2[simp]: |
205 lemma appDup_x2[simp]: |
179 "app (Dup_x2, G, rT, s) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))" |
206 "(app Dup_x2 G rT (Some s)) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))" |
180 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
207 by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) |
181 |
208 |
182 |
209 |
183 lemma appSwap[simp]: |
210 lemma appSwap[simp]: |
184 "app (Swap, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" |
211 "app Swap G rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" |
185 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
212 by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) |
186 |
213 |
187 |
214 |
188 lemma appIAdd[simp]: |
215 lemma appIAdd[simp]: |
189 "app (IAdd, G, rT, s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" (is "?app s = ?P s") |
216 "app IAdd G rT (Some s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" |
|
217 (is "?app s = ?P s") |
190 proof (cases (open) s) |
218 proof (cases (open) s) |
191 case Pair |
219 case Pair |
192 have "?app (a,b) = ?P (a,b)" |
220 have "?app (a,b) = ?P (a,b)" |
193 proof (cases "a") |
221 proof (cases "a") |
194 fix t ts assume a: "a = t#ts" |
222 fix t ts assume a: "a = t#ts" |
203 fix t' ts' assume t': "ts = t' # ts'" |
231 fix t' ts' assume t': "ts = t' # ts'" |
204 show ?thesis |
232 show ?thesis |
205 proof (cases t') |
233 proof (cases t') |
206 fix p' assume "t' = PrimT p'" |
234 fix p' assume "t' = PrimT p'" |
207 with t' ip p a |
235 with t' ip p a |
208 show ?thesis by - (cases p', auto) |
236 show ?thesis by - (cases p', auto simp add: app_def) |
209 qed (auto simp add: a p ip t') |
237 qed (auto simp add: a p ip t' app_def) |
210 qed (auto simp add: a p ip) |
238 qed (auto simp add: a p ip app_def) |
211 qed (auto simp add: a p) |
239 qed (auto simp add: a p app_def) |
212 qed (auto simp add: a) |
240 qed (auto simp add: a app_def) |
213 qed auto |
241 qed (auto simp add: app_def) |
214 with Pair show ?thesis by simp |
242 with Pair show ?thesis by simp |
215 qed |
243 qed |
216 |
244 |
217 |
245 |
218 lemma appIfcmpeq[simp]: |
246 lemma appIfcmpeq[simp]: |
219 "app (Ifcmpeq b, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> |
247 "app (Ifcmpeq b) G rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> |
220 ((\<exists> p. ts1 = PrimT p \<and> ts1 = PrimT p) \<or> |
248 ((\<exists> p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or> (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))" |
221 (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))" |
249 by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) |
222 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
|
223 |
250 |
224 |
251 |
225 lemma appReturn[simp]: |
252 lemma appReturn[simp]: |
226 "app (Return, G, rT, s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))" |
253 "app Return G rT (Some s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))" |
227 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
254 by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def) |
228 |
255 |
|
256 lemma appGoto[simp]: |
|
257 "app (Goto branch) G rT (Some s) = True" |
|
258 by (simp add: app_def) |
229 |
259 |
230 lemma appInvoke[simp]: |
260 lemma appInvoke[simp]: |
231 "app (Invoke C mn fpTs, G, rT, s) = (\<exists>apTs X ST LT. |
261 "app (Invoke C mn fpTs) G rT (Some s) = (\<exists>apTs X ST LT mD' rT' b'. |
232 s = ((rev apTs) @ (X # ST), LT) \<and> |
262 s = ((rev apTs) @ (X # ST), LT) \<and> length apTs = length fpTs \<and> |
233 length apTs = length fpTs \<and> |
263 G \<turnstile> X \<preceq> Class C \<and> (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> |
234 G \<turnstile> X \<preceq> Class C \<and> |
264 method (G,C) (mn,fpTs) = Some (mD', rT', b'))" (is "?app s = ?P s") |
235 (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> |
|
236 method (G,C) (mn,fpTs) \<noteq> None)" (is "?app s = ?P s") |
|
237 proof (cases (open) s) |
265 proof (cases (open) s) |
238 case Pair |
266 case Pair |
239 have "?app (a,b) \<Longrightarrow> ?P (a,b)" |
267 have "?app (a,b) \<Longrightarrow> ?P (a,b)" |
240 proof - |
268 proof - |
241 assume app: "?app (a,b)" |
269 assume app: "?app (a,b)" |
242 hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> length fpTs < length a" |
270 hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> |
243 (is "?a \<and> ?l") by auto |
271 length fpTs < length a" (is "?a \<and> ?l") |
244 hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") by auto |
272 by (auto simp add: app_def) |
245 hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" by (auto simp add: min_def) |
273 hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") |
246 hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST" by blast |
274 by auto |
247 hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []" by blast |
275 hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" |
248 hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> (\<exists>X ST'. ST = X#ST')" by (simp add: neq_Nil_conv) |
276 by (auto simp add: min_def) |
249 hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs" by blast |
277 hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST" |
|
278 by blast |
|
279 hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []" |
|
280 by blast |
|
281 hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> |
|
282 (\<exists>X ST'. ST = X#ST')" |
|
283 by (simp add: neq_Nil_conv) |
|
284 hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs" |
|
285 by blast |
250 with app |
286 with app |
251 show ?thesis by auto blast |
287 show ?thesis by (auto simp add: app_def) blast |
252 qed |
288 qed |
253 with Pair have "?app s \<Longrightarrow> ?P s" by simp |
289 with Pair have "?app s \<Longrightarrow> ?P s" by simp |
254 thus ?thesis by auto |
290 thus ?thesis by (auto simp add: app_def) |
255 qed |
291 qed |
256 |
292 |
257 lemmas [simp del] = app_invoke |
293 lemma step_Some: |
258 |
294 "step i G (Some s) \<noteq> None" |
259 |
295 by (simp add: step_def) |
260 lemma app_step_some: |
296 |
261 "\<lbrakk>app (i,G,rT,s); succs i pc \<noteq> {}\<rbrakk> \<Longrightarrow> step (i,G,s) \<noteq> None"; |
297 lemma step_None [simp]: |
262 by (cases s, cases i, auto) |
298 "step i G None = None" |
|
299 by (simp add: step_def) |
263 |
300 |
264 end |
301 end |