author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44037  25011c3a5c3d 
child 47632  50f9f699b2d7 
permissions  rwrr 
8011  1 
(* Title: HOL/MicroJava/J/Eval.thy 
2 
Author: David von Oheimb 

3 
Copyright 1999 Technische Universitaet Muenchen 

11070  4 
*) 
8011  5 

12911  6 
header {* \isaheader{Operational Evaluation (big step) Semantics} *} 
8011  7 

16417  8 
theory Eval imports State WellType begin 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

9 

13672  10 

11 
 "Auxiliary notions" 

12 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset

13 
definition fits :: "java_mb prog \<Rightarrow> state \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60) where 
13672  14 
"G,s\<turnstile>a' fits T \<equiv> case T of PrimT T' \<Rightarrow> False  RefT T' \<Rightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T" 
15 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset

16 
definition catch :: "java_mb prog \<Rightarrow> xstate \<Rightarrow> cname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where 
13672  17 
"G,s\<turnstile>catch C\<equiv> case abrupt s of None \<Rightarrow> False  Some a \<Rightarrow> G,store s\<turnstile> a fits Class C" 
18 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset

19 
definition lupd :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_\<mapsto>_')"[10,10]1000) where 
13672  20 
"lupd vn v \<equiv> \<lambda> (hp,loc). (hp, (loc(vn\<mapsto>v)))" 
21 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset

22 
definition new_xcpt_var :: "vname \<Rightarrow> xstate \<Rightarrow> xstate" where 
13672  23 
"new_xcpt_var vn \<equiv> \<lambda>(x,s). Norm (lupd(vn\<mapsto>the x) s)" 
24 

25 

26 
 "Evaluation relations" 

27 

23757  28 
inductive 
10056  29 
eval :: "[java_mb prog,xstate,expr,val,xstate] => bool " 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

30 
("_ \<turnstile> _ _\<succ>_> _" [51,82,60,82,82] 81) 
22271  31 
and evals :: "[java_mb prog,xstate,expr list, 
10056  32 
val list,xstate] => bool " 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

33 
("_ \<turnstile> _ _[\<succ>]_> _" [51,82,60,51,82] 81) 
22271  34 
and exec :: "[java_mb prog,xstate,stmt, xstate] => bool " 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

35 
("_ \<turnstile> _ _> _" [51,82,60,82] 81) 
22271  36 
for G :: "java_mb prog" 
37 
where 

8011  38 

22271  39 
 "evaluation of expressions" 
8011  40 

28524  41 
XcptE:"G\<turnstile>(Some xc,s) e\<succ>undefined> (Some xc,s)"  "cf. 15.5" 
8011  42 

12517  43 
 "cf. 15.8.1" 
22271  44 
 NewC: "[ h = heap s; (a,x) = new_Addr h; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

45 
h'= h(a\<mapsto>(C,init_vars (fields (G,C)))) ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

46 
G\<turnstile>Norm s NewC C\<succ>Addr a> c_hupd h' (x,s)" 
8011  47 

12517  48 
 "cf. 15.15" 
22271  49 
 Cast: "[ G\<turnstile>Norm s0 e\<succ>v> (x1,s1); 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

50 
x2 = raise_if (\<not> cast_ok G C (heap s1) v) ClassCast x1 ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

51 
G\<turnstile>Norm s0 Cast C e\<succ>v> (x2,s1)" 
8011  52 

12517  53 
 "cf. 15.7.1" 
22271  54 
 Lit: "G\<turnstile>Norm s Lit v\<succ>v> Norm s" 
8011  55 

22271  56 
 BinOp:"[ G\<turnstile>Norm s e1\<succ>v1> s1; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

57 
G\<turnstile>s1 e2\<succ>v2> s2; 
10056  58 
v = (case bop of Eq => Bool (v1 = v2) 
59 
 Add => Intg (the_Intg v1 + the_Intg v2)) ] ==> 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

60 
G\<turnstile>Norm s BinOp bop e1 e2\<succ>v> s2" 
9240  61 

12517  62 
 "cf. 15.13.1, 15.2" 
22271  63 
 LAcc: "G\<turnstile>Norm s LAcc v\<succ>the (locals s v)> Norm s" 
8011  64 

12517  65 
 "cf. 15.25.1" 
22271  66 
 LAss: "[ G\<turnstile>Norm s e\<succ>v> (x,(h,l)); 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

67 
l' = (if x = None then l(va\<mapsto>v) else l) ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

68 
G\<turnstile>Norm s va::=e\<succ>v> (x,(h,l'))" 
8011  69 

12517  70 
 "cf. 15.10.1, 15.2" 
22271  71 
 FAcc: "[ G\<turnstile>Norm s0 e\<succ>a'> (x1,s1); 
10056  72 
v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) ] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

73 
G\<turnstile>Norm s0 {T}e..fn\<succ>v> (np a' x1,s1)" 
8011  74 

12517  75 
 "cf. 15.25.1" 
22271  76 
 FAss: "[ G\<turnstile> Norm s0 e1\<succ>a'> (x1,s1); a = the_Addr a'; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

77 
G\<turnstile>(np a' x1,s1) e2\<succ>v > (x2,s2); 
10056  78 
h = heap s2; (c,fs) = the (h a); 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

79 
h' = h(a\<mapsto>(c,(fs((fn,T)\<mapsto>v)))) ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

80 
G\<turnstile>Norm s0 {T}e1..fn:=e2\<succ>v> c_hupd h' (x2,s2)" 
8011  81 

12517  82 
 "cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15" 
22271  83 
 Call: "[ G\<turnstile>Norm s0 e\<succ>a'> s1; a = the_Addr a'; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

84 
G\<turnstile>s1 ps[\<succ>]pvs> (x,(h,l)); dynT = fst (the (h a)); 
10056  85 
(md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs)); 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

86 
G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) blk> s3; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

87 
G\<turnstile> s3 res\<succ>v > (x4,s4) ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

88 
G\<turnstile>Norm s0 {C}e..mn({pTs}ps)\<succ>v> (x4,(heap s4,l))" 
8011  89 

90 

12517  91 
 "evaluation of expression lists" 
92 

93 
 "cf. 15.5" 

28524  94 
 XcptEs:"G\<turnstile>(Some xc,s) e[\<succ>]undefined> (Some xc,s)" 
8011  95 

12517  96 
 "cf. 15.11.???" 
22271  97 
 Nil: "G\<turnstile>Norm s0 [][\<succ>][]> Norm s0" 
8011  98 

12517  99 
 "cf. 15.6.4" 
22271  100 
 Cons: "[ G\<turnstile>Norm s0 e \<succ> v > s1; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

101 
G\<turnstile> s1 es[\<succ>]vs> s2 ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

102 
G\<turnstile>Norm s0 e#es[\<succ>]v#vs> s2" 
8011  103 

104 

12517  105 
 "execution of statements" 
106 

107 
 "cf. 14.1" 

22271  108 
 XcptS:"G\<turnstile>(Some xc,s) c> (Some xc,s)" 
8011  109 

12517  110 
 "cf. 14.5" 
22271  111 
 Skip: "G\<turnstile>Norm s Skip> Norm s" 
8011  112 

12517  113 
 "cf. 14.7" 
22271  114 
 Expr: "[ G\<turnstile>Norm s0 e\<succ>v> s1 ] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

115 
G\<turnstile>Norm s0 Expr e> s1" 
8011  116 

12517  117 
 "cf. 14.2" 
22271  118 
 Comp: "[ G\<turnstile>Norm s0 c1> s1; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

119 
G\<turnstile> s1 c2> s2] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

120 
G\<turnstile>Norm s0 c1;; c2> s2" 
8011  121 

12517  122 
 "cf. 14.8.2" 
22271  123 
 Cond: "[ G\<turnstile>Norm s0 e\<succ>v> s1; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

124 
G\<turnstile> s1 (if the_Bool v then c1 else c2)> s2] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

125 
G\<turnstile>Norm s0 If(e) c1 Else c2> s2" 
8011  126 

12517  127 
 "cf. 14.10, 14.10.1" 
22271  128 
 LoopF:"[ G\<turnstile>Norm s0 e\<succ>v> s1; \<not>the_Bool v ] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

129 
G\<turnstile>Norm s0 While(e) c> s1" 
22271  130 
 LoopT:"[ G\<turnstile>Norm s0 e\<succ>v> s1; the_Bool v; 
12517  131 
G\<turnstile>s1 c> s2; G\<turnstile>s2 While(e) c> s3 ] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

132 
G\<turnstile>Norm s0 While(e) c> s3" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

133 

12517  134 

11040  135 
lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)] 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

136 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

137 
lemma NewCI: "[new_Addr (heap s) = (a,x); 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

138 
s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

139 
G\<turnstile>Norm s NewC C\<succ>Addr a> s'" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

140 
apply (simp (no_asm_simp)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

141 
apply (rule eval_evals_exec.NewC) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

142 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

143 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

144 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

145 
lemma eval_evals_exec_no_xcpt: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

146 
"!!s s'. (G\<turnstile>(x,s) e \<succ> v > (x',s') > x'=None > x=None) \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

147 
(G\<turnstile>(x,s) es[\<succ>]vs> (x',s') > x'=None > x=None) \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

148 
(G\<turnstile>(x,s) c > (x',s') > x'=None > x=None)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

149 
apply(simp (no_asm_simp) only: split_tupled_all) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

150 
apply(rule eval_evals_exec_induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

151 
apply(unfold c_hupd_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

152 
apply(simp_all) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

153 
done 
10828
b207d6d1bedc
improved evaluation judgment syntax; modified Loop rule
oheimb
parents:
10763
diff
changeset

154 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

155 
lemma eval_no_xcpt: "G\<turnstile>(x,s) e\<succ>v> (None,s') ==> x=None" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

156 
apply (drule eval_evals_exec_no_xcpt [THEN conjunct1, THEN mp]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

157 
apply (fast) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

158 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

159 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

160 
lemma evals_no_xcpt: "G\<turnstile>(x,s) e[\<succ>]v> (None,s') ==> x=None" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

161 
apply (drule eval_evals_exec_no_xcpt [THEN conjunct2, THEN conjunct1, THEN mp]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

162 
apply (fast) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

163 
done 
8011  164 

14141  165 
lemma exec_no_xcpt: "G \<turnstile> (x, s) c> (None, s') 
166 
\<Longrightarrow> x = None" 

167 
apply (drule eval_evals_exec_no_xcpt [THEN conjunct2 [THEN conjunct2], rule_format]) 

168 
apply simp+ 

169 
done 

170 

171 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

172 
lemma eval_evals_exec_xcpt: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

173 
"!!s s'. (G\<turnstile>(x,s) e \<succ> v > (x',s') > x=Some xc > x'=Some xc \<and> s'=s) \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

174 
(G\<turnstile>(x,s) es[\<succ>]vs> (x',s') > x=Some xc > x'=Some xc \<and> s'=s) \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

175 
(G\<turnstile>(x,s) c > (x',s') > x=Some xc > x'=Some xc \<and> s'=s)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

176 
apply (simp (no_asm_simp) only: split_tupled_all) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

177 
apply (rule eval_evals_exec_induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

178 
apply (unfold c_hupd_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

179 
apply (simp_all) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

180 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

181 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

182 
lemma eval_xcpt: "G\<turnstile>(Some xc,s) e\<succ>v> (x',s') ==> x'=Some xc \<and> s'=s" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

183 
apply (drule eval_evals_exec_xcpt [THEN conjunct1, THEN mp]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

184 
apply (fast) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

185 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

186 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

187 
lemma exec_xcpt: "G\<turnstile>(Some xc,s) s0> (x',s') ==> x'=Some xc \<and> s'=s" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

188 
apply (drule eval_evals_exec_xcpt [THEN conjunct2, THEN conjunct2, THEN mp]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

189 
apply (fast) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

190 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10927
diff
changeset

191 

44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

192 

25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

193 
lemma eval_LAcc_code: "G\<turnstile>Norm (h, l) LAcc v\<succ>the (l v)> Norm (h, l)" 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

194 
using LAcc[of G "(h, l)" v] by simp 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

195 

25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

196 
lemma eval_Call_code: 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

197 
"[ G\<turnstile>Norm s0 e\<succ>a'> s1; a = the_Addr a'; 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

198 
G\<turnstile>s1 ps[\<succ>]pvs> (x,(h,l)); dynT = fst (the (h a)); 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

199 
(md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs)); 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

200 
G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) blk> s3; 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

201 
G\<turnstile> s3 res\<succ>v > (x4,(h4, l4)) ] ==> 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

202 
G\<turnstile>Norm s0 {C}e..mn({pTs}ps)\<succ>v> (x4,(h4,l))" 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

203 
using Call[of G s0 e a' s1 a ps pvs x h l dynT md rT pns lvars blk res mn pTs s3 v x4 "(h4, l4)" C] 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

204 
by simp 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

205 

25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

206 
lemmas [code_pred_intro] = XcptE NewC Cast Lit BinOp 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

207 
lemmas [code_pred_intro LAcc_code] = eval_LAcc_code 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

208 
lemmas [code_pred_intro] = LAss FAcc FAss 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

209 
lemmas [code_pred_intro Call_code] = eval_Call_code 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

210 
lemmas [code_pred_intro] = XcptEs Nil Cons XcptS Skip Expr Comp Cond LoopF 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

211 
lemmas [code_pred_intro LoopT_code] = LoopT 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

212 

25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

213 
code_pred 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

214 
(modes: 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

215 
eval: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> o \<Rightarrow> bool 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

216 
and 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

217 
evals: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> o \<Rightarrow> bool 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

218 
and 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

219 
exec: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool) 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

220 
eval 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

221 
proof  
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

222 
case eval 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

223 
from eval.prems show thesis 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

224 
proof(cases (no_simp)) 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

225 
case LAcc with LAcc_code show ?thesis by auto 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

226 
next 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

227 
case (Call a b c d e f g h i j k l m n o p q r s t u v s4) 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

228 
with Call_code show ?thesis 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

229 
by(cases "s4")(simp, (erule meta_allE meta_impErule conjI refl assumption)+) 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

230 
qed(erule (3) that[OF refl]assumption)+ 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

231 
next 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

232 
case evals 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

233 
from evals.prems show thesis 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

234 
by(cases (no_simp))(erule (3) that[OF refl]assumption)+ 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

235 
next 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

236 
case exec 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

237 
from exec.prems show thesis 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

238 
proof(cases (no_simp)) 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

239 
case LoopT thus ?thesis by(rule LoopT_code[OF refl]) 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

240 
qed(erule (2) that[OF refl]assumption)+ 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

241 
qed 
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
35416
diff
changeset

242 

11642  243 
end 