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