author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46714  a7ca72710dfe 
child 51717  9e7d1c139569 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Evaln.thy 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

2 
Author: David von Oheimb and Norbert Schirmer 
12854  3 
*) 
4 
header {* Operational evaluation (bigstep) semantics of Java expressions and 

5 
statements 

6 
*} 

7 

16417  8 
theory Evaln imports TypeSafe begin 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

9 

12854  10 

11 
text {* 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

12 
Variant of @{term eval} relation with counter for bounded recursive depth. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

13 
In principal @{term evaln} could replace @{term eval}. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

14 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

15 
Validity of the axiomatic semantics builds on @{term evaln}. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

16 
For recursive method calls the axiomatic semantics rule assumes the method ok 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

17 
to derive a proof for the body. To prove the method rule sound we need to 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

18 
perform induction on the recursion depth. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

19 
For the completeness proof of the axiomatic semantics the notion of the most 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

20 
general formula is used. The most general formula right now builds on the 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

21 
ordinary evaluation relation @{term eval}. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

22 
So sometimes we have to switch between @{term evaln} and @{term eval} and vice 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

23 
versa. To make 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

24 
this switch easy @{term evaln} also does all the technical accessibility tests 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

25 
@{term check_field_access} and @{term check_method_access} like @{term eval}. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

26 
If it would omit them @{term evaln} and @{term eval} would only be equivalent 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

27 
for welltyped, and definitely assigned terms. 
12854  28 
*} 
29 

23747  30 
inductive 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

31 
evaln :: "[prog, state, term, nat, vals, state] \<Rightarrow> bool" 
21765  32 
("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> '(_, _')" [61,61,80,61,0,0] 60) 
33 
and evarn :: "[prog, state, var, vvar, nat, state] \<Rightarrow> bool" 

34 
("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60) 

35 
and eval_n:: "[prog, state, expr, val, nat, state] \<Rightarrow> bool" 

36 
("_\<turnstile>_ \<midarrow>_\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60) 

37 
and evalsn :: "[prog, state, expr list, val list, nat, state] \<Rightarrow> bool" 

38 
("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

39 
and execn :: "[prog, state, stmt, nat, state] \<Rightarrow> bool" 
21765  40 
("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _" [61,61,65, 61,61] 60) 
41 
for G :: prog 

42 
where 

12854  43 

21765  44 
"G\<turnstile>s \<midarrow>c \<midarrow>n\<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In1r c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit> , s')" 
45 
 "G\<turnstile>s \<midarrow>e\<succ>v \<midarrow>n\<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v , s')" 

46 
 "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In2 e\<succ>\<midarrow>n\<rightarrow> (In2 vf, s')" 

47 
 "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<midarrow>n\<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In3 e\<succ>\<midarrow>n\<rightarrow> (In3 v , s')" 

12854  48 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

49 
{* propagation of abrupt completion *} 
12854  50 

28524  51 
 Abrupt: "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t,(Some xc,s))" 
12854  52 

53 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

54 
{* evaluation of variables *} 
12854  55 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

56 
 LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s" 
12854  57 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

58 
 FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e\<succ>a\<midarrow>n\<rightarrow> s2; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

59 
(v,s2') = fvar statDeclC stat fn a s2; 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

60 
s3 = check_field_access G accC statDeclC fn stat a s2'\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

61 
G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s3" 
12854  62 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

63 
 AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1\<succ>a\<midarrow>n\<rightarrow> s1 ; G\<turnstile>s1 \<midarrow>e2\<succ>i\<midarrow>n\<rightarrow> s2; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

64 
(v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

65 
G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'" 
12854  66 

67 

68 

69 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

70 
{* evaluation of expressions *} 
12854  71 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

72 
 NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

73 
G\<turnstile> s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

74 
G\<turnstile>Norm s0 \<midarrow>NewC C\<succ>Addr a\<midarrow>n\<rightarrow> s2" 
12854  75 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

76 
 NewA: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e\<succ>i'\<midarrow>n\<rightarrow> s2; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

77 
G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

78 
G\<turnstile>Norm s0 \<midarrow>New T[e]\<succ>Addr a\<midarrow>n\<rightarrow> s3" 
12854  79 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

80 
 Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<midarrow>n\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

81 
s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

82 
G\<turnstile>Norm s0 \<midarrow>Cast T e\<succ>v\<midarrow>n\<rightarrow> s2" 
12854  83 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

84 
 Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<midarrow>n\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

85 
b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

86 
G\<turnstile>Norm s0 \<midarrow>e InstOf T\<succ>Bool b\<midarrow>n\<rightarrow> s1" 
12854  87 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

88 
 Lit: "G\<turnstile>Norm s \<midarrow>Lit v\<succ>v\<midarrow>n\<rightarrow> Norm s" 
12854  89 

21765  90 
 UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

91 
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

92 

21765  93 
 BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1\<succ>v1\<midarrow>n\<rightarrow> s1; 
13384  94 
G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip)) 
95 
\<succ>\<midarrow>n\<rightarrow> (In1 v2,s2)\<rbrakk> 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

96 
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

97 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

98 
 Super: "G\<turnstile>Norm s \<midarrow>Super\<succ>val_this s\<midarrow>n\<rightarrow> Norm s" 
12854  99 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

100 
 Acc: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

101 
G\<turnstile>Norm s0 \<midarrow>Acc va\<succ>v\<midarrow>n\<rightarrow> s1" 
12854  102 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

103 
 Ass: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1; 
12854  104 
G\<turnstile> s1 \<midarrow>e\<succ>v \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

105 
G\<turnstile>Norm s0 \<midarrow>va:=e\<succ>v\<midarrow>n\<rightarrow> assign f v s2" 
12854  106 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

107 
 Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0\<succ>b\<midarrow>n\<rightarrow> s1; 
12854  108 
G\<turnstile> s1 \<midarrow>(if the_Bool b then e1 else e2)\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

109 
G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2\<succ>v\<midarrow>n\<rightarrow> s2" 
12854  110 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

111 
 Call: 
12854  112 
"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2; 
113 
D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

114 
s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2; 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

115 
s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3; 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

116 
G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>\<succ>v\<midarrow>n\<rightarrow> s4 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

117 
\<rbrakk> 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

118 
\<Longrightarrow> 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

119 
G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s4)" 
12854  120 

21765  121 
 Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

122 
G\<turnstile>Norm s0 \<midarrow>Methd D sig\<succ>v\<midarrow>Suc n\<rightarrow> s1" 
12854  123 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

124 
 Body: "\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2; 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

125 
s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

126 
abrupt s2 = Some (Jump (Cont l))) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

127 
then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

128 
else s2)\<rbrakk>\<Longrightarrow> 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

129 
G\<turnstile>Norm s0 \<midarrow>Body D c 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

130 
\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s3" 
12854  131 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

132 
{* evaluation of expression lists *} 
12854  133 

21765  134 
 Nil: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

135 
"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0" 
12854  136 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

137 
 Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e \<succ> v \<midarrow>n\<rightarrow> s1; 
12854  138 
G\<turnstile> s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

139 
G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2" 
12854  140 

141 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

142 
{* execution of statements *} 
12854  143 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

144 
 Skip: "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s" 
12854  145 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

146 
 Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

147 
G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1" 
12854  148 

21765  149 
 Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow> 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

150 
G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1" 
12854  151 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

152 
 Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

153 
G\<turnstile> s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

154 
G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2" 
12854  155 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

156 
 If: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<midarrow>n\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

157 
G\<turnstile> s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

158 
G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2" 
12854  159 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

160 
 Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<midarrow>n\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

161 
if the_Bool b 
12854  162 
then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
163 
G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

164 
else s3 = s1\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

165 
G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3" 
12854  166 

21765  167 
 Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)" 
12854  168 

21765  169 
 Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

170 
G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1" 
12854  171 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

172 
 Try: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

173 
if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk> 
12854  174 
\<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

175 
G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3" 
12854  176 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

177 
 Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1); 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

178 
G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2; 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

179 
s3=(if (\<exists> err. x1=Some (Error err)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

180 
then (x1,s1) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

181 
else abupd (abrupt_if (x1\<noteq>None) x1) s2)\<rbrakk> \<Longrightarrow> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

182 
G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3" 
12854  183 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

184 
 Init: "\<lbrakk>the (class G C) = c; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

185 
if inited C (globs s0) then s3 = Norm s0 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

186 
else (G\<turnstile>Norm (init_class_obj G C s0) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

187 
\<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

188 
G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
12854  189 
s3 = restore_lvars s1 s2)\<rbrakk> 
190 
\<Longrightarrow> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

191 
G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3" 
12854  192 
monos 
22218  193 
if_bool_eq_conj 
12854  194 

195 

196 
declare split_if [split del] split_if_asm [split del] 

197 
option.split [split del] option.split_asm [split del] 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

198 
not_None_eq [simp del] 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

199 
split_paired_All [simp del] split_paired_Ex [simp del] 
24019  200 
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *} 
201 

23747  202 
inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')" 
12854  203 

23747  204 
inductive_cases evaln_elim_cases: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

205 
"G\<turnstile>(Some xc, s) \<midarrow>t \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

206 
"G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<midarrow>n\<rightarrow> (x, s')" 
21765  207 
"G\<turnstile>Norm s \<midarrow>In1r (Jmp j) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
208 
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c) \<succ>\<midarrow>n\<rightarrow> (x, s')" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

209 
"G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

210 
"G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

211 
"G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
21765  212 
"G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
213 
"G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2) \<succ>\<midarrow>n\<rightarrow> (v, s')" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

214 
"G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

215 
"G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

216 
"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

217 
"G\<turnstile>Norm s \<midarrow>In1l (Super) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

218 
"G\<turnstile>Norm s \<midarrow>In1l (Acc va) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

219 
"G\<turnstile>Norm s \<midarrow>In1r (Expr e) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

220 
"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

221 
"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

222 
"G\<turnstile>Norm s \<midarrow>In1l (Body D c) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

223 
"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

224 
"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

225 
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

226 
"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

227 
"G\<turnstile>Norm s \<midarrow>In1r (Throw e) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

228 
"G\<turnstile>Norm s \<midarrow>In1l (NewC C) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

229 
"G\<turnstile>Norm s \<midarrow>In1l (New T[e]) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

230 
"G\<turnstile>Norm s \<midarrow>In1l (Ass va e) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

231 
"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

232 
"G\<turnstile>Norm s \<midarrow>In2 ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

233 
"G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

234 
"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

235 
"G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<midarrow>n\<rightarrow> (x, s')" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

236 

12854  237 
declare split_if [split] split_if_asm [split] 
238 
option.split [split] option.split_asm [split] 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

239 
not_None_eq [simp] 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

240 
split_paired_All [simp] split_paired_Ex [simp] 
24019  241 
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} 
242 

12854  243 
lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow> 
244 
(case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v)  Inr c \<Rightarrow> w = \<diamondsuit>) 

245 
 In2 e \<Rightarrow> (\<exists>v. w = In2 v)  In3 e \<Rightarrow> (\<exists>v. w = In3 v)" 

246 
apply (erule evaln_cases , auto) 

247 
apply (induct_tac "t") 

248 
apply (induct_tac "a") 

249 
apply auto 

250 
done 

251 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

252 
text {* The following simplification procedures set up the proper injections of 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

253 
terms and their corresponding values in the evaluation relation: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

254 
E.g. an expression 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

255 
(injection @{term In1l} into terms) always evaluates to ordinary values 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

256 
(injection @{term In1} into generalised values @{term vals}). 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

257 
*} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

258 

21765  259 
lemma evaln_expr_eq: "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t\<succ>v \<midarrow>n\<rightarrow> s')" 
260 
by (auto, frule evaln_Inj_elim, auto) 

261 

262 
lemma evaln_var_eq: "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s')" 

263 
by (auto, frule evaln_Inj_elim, auto) 

264 

265 
lemma evaln_exprs_eq: "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s')" 

266 
by (auto, frule evaln_Inj_elim, auto) 

267 

268 
lemma evaln_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<midarrow>n\<rightarrow> s')" 

269 
by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto) 

270 

24019  271 
simproc_setup evaln_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {* 
272 
fn _ => fn _ => fn ct => 

273 
(case Thm.term_of ct of 

274 
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE 

275 
 _ => SOME (mk_meta_eq @{thm evaln_expr_eq})) *} 

276 

277 
simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {* 

278 
fn _ => fn _ => fn ct => 

279 
(case Thm.term_of ct of 

280 
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE 

281 
 _ => SOME (mk_meta_eq @{thm evaln_var_eq})) *} 

12854  282 

24019  283 
simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {* 
284 
fn _ => fn _ => fn ct => 

285 
(case Thm.term_of ct of 

286 
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE 

287 
 _ => SOME (mk_meta_eq @{thm evaln_exprs_eq})) *} 

12854  288 

24019  289 
simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {* 
290 
fn _ => fn _ => fn ct => 

291 
(case Thm.term_of ct of 

292 
(_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE 

293 
 _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *} 

294 

27226  295 
ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *} 
12854  296 
declare evaln_AbruptIs [intro!] 
297 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

298 
lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

299 
proof  
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

300 
{ fix s t v s' 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

301 
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

302 
normal: "normal s" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

303 
callee: "t=In1l (Callee l e)" 
21765  304 
then have "False" by induct auto 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

305 
} 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

306 
then show ?thesis 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
39159
diff
changeset

307 
by (cases s') fastforce 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

308 
qed 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

309 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

310 
lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

311 
proof  
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

312 
{ fix s t v s' 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

313 
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

314 
normal: "normal s" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

315 
callee: "t=In1l (InsInitE c e)" 
21765  316 
then have "False" by induct auto 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

317 
} 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

318 
then show ?thesis 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
39159
diff
changeset

319 
by (cases s') fastforce 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

320 
qed 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

321 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

322 
lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

323 
proof  
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

324 
{ fix s t v s' 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

325 
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

326 
normal: "normal s" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

327 
callee: "t=In2 (InsInitV c w)" 
21765  328 
then have "False" by induct auto 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

329 
} 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

330 
then show ?thesis 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
39159
diff
changeset

331 
by (cases s') fastforce 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

332 
qed 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

333 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

334 
lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

335 
proof  
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

336 
{ fix s t v s' 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

337 
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

338 
normal: "normal s" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

339 
callee: "t=In1r (FinA a c)" 
21765  340 
then have "False" by induct auto 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

341 
} 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

342 
then show ?thesis 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
39159
diff
changeset

343 
by (cases s') fastforce 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

344 
qed 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset

345 

12854  346 
lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
28524  347 
fst s = Some xc \<longrightarrow> s' = s \<and> v = undefined3 e" 
12854  348 
apply (erule evaln_cases , auto) 
349 
done 

350 

351 
lemma evaln_abrupt: 

352 
"\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and> 

28524  353 
w=undefined3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (undefined3 e,(Some xc,s)))" 
12854  354 
apply auto 
355 
apply (frule evaln_abrupt_lemma, auto)+ 

356 
done 

357 

24019  358 
simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = {* 
359 
fn _ => fn _ => fn ct => 

360 
(case Thm.term_of ct of 

24165  361 
(_ $ _ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some},_) $ _)$ _)) 
24019  362 
=> NONE 
363 
 _ => SOME (mk_meta_eq @{thm evaln_abrupt})) 

12854  364 
*} 
365 

28524  366 
lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v\<succ>(if normal s then v else undefined)\<midarrow>n\<rightarrow> s" 
12854  367 
apply (case_tac "s", case_tac "a = None") 
368 
by (auto intro!: evaln.Lit) 

369 

370 
lemma CondI: 

371 
"\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e\<succ>b\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 

28524  372 
G\<turnstile>s \<midarrow>e ? e1 : e2\<succ>(if normal s1 then v else undefined)\<midarrow>n\<rightarrow> s2" 
12854  373 
apply (case_tac "s", case_tac "a = None") 
374 
by (auto intro!: evaln.Cond) 

375 

376 
lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s" 

377 
apply (case_tac "s", case_tac "a = None") 

378 
by (auto intro!: evaln.Skip) 

379 

380 
lemma evaln_ExprI: "G\<turnstile>s \<midarrow>e\<succ>v\<midarrow>n\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<midarrow>n\<rightarrow> s'" 

381 
apply (case_tac "s", case_tac "a = None") 

382 
by (auto intro!: evaln.Expr) 

383 

384 
lemma evaln_CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2" 

385 
apply (case_tac "s", case_tac "a = None") 

386 
by (auto intro!: evaln.Comp) 

387 

388 
lemma evaln_IfI: 

389 
"\<lbrakk>G\<turnstile>s \<midarrow>e\<succ>v\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 

390 
G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2" 

391 
apply (case_tac "s", case_tac "a = None") 

392 
by (auto intro!: evaln.If) 

393 

394 
lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 

395 
by (erule evaln_cases, auto) 

396 

397 
lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')" 

398 
apply auto 

399 
done 

400 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

401 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

402 

13384  403 

404 
section {* evaln implies eval *} 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

405 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

406 
lemma evaln_eval: 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

407 
assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

408 
shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

409 
using evaln 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

410 
proof (induct) 
24727
dd9ea6b72eb9
adapted variable order for inductive cases (determined by read_specification *before* expanding abbreviations);
wenzelm
parents:
24165
diff
changeset

411 
case (Loop s0 e b n s1 c s2 l s3) 
23350  412 
note `G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<rightarrow> s1` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

413 
moreover 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

414 
have "if the_Bool b 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

415 
then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

416 
G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

417 
else s3 = s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

418 
using Loop.hyps by simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

419 
ultimately show ?case by (rule eval.Loop) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

420 
next 
21765  421 
case (Try s0 c1 n s1 s2 C vn c2 s3) 
23350  422 
note `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

423 
moreover 
23350  424 
note `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

425 
moreover 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

426 
have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

427 
using Try.hyps by simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

428 
ultimately show ?case by (rule eval.Try) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

429 
next 
21765  430 
case (Init C c s0 s3 n s1 s2) 
23350  431 
note `the (class G C) = c` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

432 
moreover 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

433 
have "if inited C (globs s0) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

434 
then s3 = Norm s0 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

435 
else G\<turnstile>Norm ((init_class_obj G C) s0) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

436 
\<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

437 
G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2 \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

438 
s3 = (set_lvars (locals (store s1))) s2" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

439 
using Init.hyps by simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

440 
ultimately show ?case by (rule eval.Init) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

441 
qed (rule eval.intros,(assumption+  assumption?))+ 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

442 

99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

443 
lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

444 
apply (frule Suc_le_D) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

445 
apply fast 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

446 
done 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

447 

99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

448 
lemma evaln_nonstrict [rule_format (no_asm), elim]: 
21765  449 
"G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')" 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

450 
apply (erule evaln.induct) 
39159  451 
apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma}, 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

452 
REPEAT o smp_tac 1, 
39159  453 
resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *}) 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

454 
(* 3 subgoals *) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

455 
apply (auto split del: split_if) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

456 
done 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

457 

99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

458 
lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]] 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

459 

21765  460 
lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2')\<rbrakk> \<Longrightarrow> 
461 
G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1') \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2')" 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

462 
by (fast intro: le_maxI1 le_maxI2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

463 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

464 
corollary evaln_max2E [consumes 2]: 
21765  465 
"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); 
466 
\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1');G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2') \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

467 
by (drule (1) evaln_max2) simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

468 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

469 

99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

470 
lemma evaln_max3: 
21765  471 
"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3')\<rbrakk> \<Longrightarrow> 
472 
G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1') \<and> 

473 
G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and> 

474 
G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')" 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

475 
apply (drule (1) evaln_max2, erule thin_rl) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

476 
apply (fast intro!: le_maxI1 le_maxI2) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

477 
done 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

478 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

479 
corollary evaln_max3E: 
21765  480 
"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3'); 
481 
\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1'); 

482 
G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2'); 

483 
G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3') 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

484 
\<rbrakk> \<Longrightarrow> P 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

485 
\<rbrakk> \<Longrightarrow> P" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

486 
by (drule (2) evaln_max3) simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

487 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

488 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

489 
lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

490 
proof  
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

491 
have "n2 \<le> max n2 n3" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

492 
by (rule le_maxI1) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

493 
also 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

494 
have "max n2 n3 \<le> max n1 (max n2 n3)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

495 
by (rule le_maxI2) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

496 
finally 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

497 
show ?thesis . 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

498 
qed 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

499 

99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

500 
lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

501 
proof  
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

502 
have "n3 \<le> max n2 n3" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

503 
by (rule le_maxI2) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

504 
also 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

505 
have "max n2 n3 \<le> max n1 (max n2 n3)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

506 
by (rule le_maxI2) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

507 
finally 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

508 
show ?thesis . 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

509 
qed 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

510 

24019  511 
declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]] 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

512 

13384  513 
section {* eval implies evaln *} 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

514 
lemma eval_evaln: 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

515 
assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

516 
shows "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

517 
using eval 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

518 
proof (induct) 
21765  519 
case (Abrupt xc s t) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

520 
obtain n where 
28524  521 
"G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t, (Some xc, s))" 
17589  522 
by (iprover intro: evaln.Abrupt) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

523 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

524 
next 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

525 
case Skip 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

526 
show ?case by (blast intro: evaln.Skip) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

527 
next 
21765  528 
case (Expr s0 e v s1) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

529 
then obtain n where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

530 
"G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<midarrow>n\<rightarrow> s1" 
17589  531 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

532 
then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

533 
by (rule evaln.Expr) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

534 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

535 
next 
21765  536 
case (Lab s0 c s1 l) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

537 
then obtain n where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

538 
"G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1" 
17589  539 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

540 
then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

541 
by (rule evaln.Lab) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

542 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

543 
next 
21765  544 
case (Comp s0 c1 s1 c2 s2) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

545 
then obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

546 
"G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

547 
"G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2" 
17589  548 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

549 
then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

550 
by (blast intro: evaln.Comp dest: evaln_max2 ) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

551 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

552 
next 
21765  553 
case (If s0 e b s1 c1 c2 s2) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

554 
then obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

555 
"G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<midarrow>n1\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

556 
"G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2" 
17589  557 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

558 
then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

559 
by (blast intro: evaln.If dest: evaln_max2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

560 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

561 
next 
21765  562 
case (Loop s0 e b s1 c s2 l s3) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

563 
from Loop.hyps obtain n1 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

564 
"G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<midarrow>n1\<rightarrow> s1" 
17589  565 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

566 
moreover from Loop.hyps obtain n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

567 
"if the_Bool b 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

568 
then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

569 
G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

570 
else s3 = s1" 
17589  571 
by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

572 
ultimately 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

573 
have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

574 
apply  
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

575 
apply (rule evaln.Loop) 
17589  576 
apply (iprover intro: evaln_nonstrict intro: le_maxI1) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

577 
apply (auto intro: evaln_nonstrict intro: le_maxI2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

578 
done 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

579 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

580 
next 
21765  581 
case (Jmp s j) 
26932  582 
fix n have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

583 
by (rule evaln.Jmp) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

584 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

585 
next 
21765  586 
case (Throw s0 e a s1) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

587 
then obtain n where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

588 
"G\<turnstile>Norm s0 \<midarrow>e\<succ>a\<midarrow>n\<rightarrow> s1" 
17589  589 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

590 
then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

591 
by (rule evaln.Throw) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

592 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

593 
next 
21765  594 
case (Try s0 c1 s1 s2 catchC vn c2 s3) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

595 
from Try.hyps obtain n1 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

596 
"G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1" 
17589  597 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

598 
moreover 
23350  599 
note sxalloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

600 
moreover 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

601 
from Try.hyps obtain n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

602 
"if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
39159
diff
changeset

603 
by fastforce 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

604 
ultimately 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

605 
have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

606 
by (auto intro!: evaln.Try le_maxI1 le_maxI2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

607 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

608 
next 
21765  609 
case (Fin s0 c1 x1 s1 c2 s2 s3) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

610 
from Fin obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

611 
"G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

612 
"G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2" 
17589  613 
by iprover 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

614 
moreover 
23350  615 
note s3 = `s3 = (if \<exists>err. x1 = Some (Error err) 
616 
then (x1, s1) 

617 
else abupd (abrupt_if (x1 \<noteq> None) x1) s2)` 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

618 
ultimately 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

619 
have 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

620 
"G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

621 
by (blast intro: evaln.Fin dest: evaln_max2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

622 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

623 
next 
21765  624 
case (Init C c s0 s3 s1 s2) 
23350  625 
note cls = `the (class G C) = c` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

626 
moreover from Init.hyps obtain n where 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

627 
"if inited C (globs s0) then s3 = Norm s0 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

628 
else (G\<turnstile>Norm (init_class_obj G C s0) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

629 
\<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

630 
G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

631 
s3 = restore_lvars s1 s2)" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

632 
by (auto intro: evaln_nonstrict le_maxI1 le_maxI2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

633 
ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

634 
by (rule evaln.Init) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

635 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

636 
next 
21765  637 
case (NewC s0 C s1 a s2) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

638 
then obtain n where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

639 
"G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1" 
17589  640 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

641 
with NewC 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

642 
have "G\<turnstile>Norm s0 \<midarrow>NewC C\<succ>Addr a\<midarrow>n\<rightarrow> s2" 
17589  643 
by (iprover intro: evaln.NewC) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

644 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

645 
next 
21765  646 
case (NewA s0 T s1 e i s2 a s3) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

647 
then obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

648 
"G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

649 
"G\<turnstile>s1 \<midarrow>e\<succ>i\<midarrow>n2\<rightarrow> s2" 
17589  650 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

651 
moreover 
23350  652 
note `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

653 
ultimately 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

654 
have "G\<turnstile>Norm s0 \<midarrow>New T[e]\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

655 
by (blast intro: evaln.NewA dest: evaln_max2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

656 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

657 
next 
21765  658 
case (Cast s0 e v s1 s2 castT) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

659 
then obtain n where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

660 
"G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<midarrow>n\<rightarrow> s1" 
17589  661 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

662 
moreover 
23350  663 
note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

664 
ultimately 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

665 
have "G\<turnstile>Norm s0 \<midarrow>Cast castT e\<succ>v\<midarrow>n\<rightarrow> s2" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

666 
by (rule evaln.Cast) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

667 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

668 
next 
21765  669 
case (Inst s0 e v s1 b T) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

670 
then obtain n where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

671 
"G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<midarrow>n\<rightarrow> s1" 
17589  672 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

673 
moreover 
23350  674 
note `b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

675 
ultimately 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

676 
have "G\<turnstile>Norm s0 \<midarrow>e InstOf T\<succ>Bool b\<midarrow>n\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

677 
by (rule evaln.Inst) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

678 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

679 
next 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

680 
case (Lit s v) 
26932  681 
fix n have "G\<turnstile>Norm s \<midarrow>Lit v\<succ>v\<midarrow>n\<rightarrow> Norm s" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

682 
by (rule evaln.Lit) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

683 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

684 
next 
21765  685 
case (UnOp s0 e v s1 unop) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

686 
then obtain n where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

687 
"G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<midarrow>n\<rightarrow> s1" 
17589  688 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

689 
hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

690 
by (rule evaln.UnOp) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

691 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

692 
next 
21765  693 
case (BinOp s0 e1 v1 s1 binop e2 v2 s2) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

694 
then obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

695 
"G\<turnstile>Norm s0 \<midarrow>e1\<succ>v1\<midarrow>n1\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

696 
"G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2 
13384  697 
else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)" 
17589  698 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

699 
hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

700 
\<rightarrow> s2" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

701 
by (blast intro!: evaln.BinOp dest: evaln_max2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

702 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

703 
next 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

704 
case (Super s ) 
26932  705 
fix n have "G\<turnstile>Norm s \<midarrow>Super\<succ>val_this s\<midarrow>n\<rightarrow> Norm s" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

706 
by (rule evaln.Super) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

707 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

708 
next 
21765  709 
case (Acc s0 va v f s1) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

710 
then obtain n where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

711 
"G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1" 
17589  712 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

713 
then 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

714 
have "G\<turnstile>Norm s0 \<midarrow>Acc va\<succ>v\<midarrow>n\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

715 
by (rule evaln.Acc) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

716 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

717 
next 
21765  718 
case (Ass s0 var w f s1 e v s2) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

719 
then obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

720 
"G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

721 
"G\<turnstile>s1 \<midarrow>e\<succ>v\<midarrow>n2\<rightarrow> s2" 
17589  722 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

723 
then 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

724 
have "G\<turnstile>Norm s0 \<midarrow>var:=e\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

725 
by (blast intro: evaln.Ass dest: evaln_max2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

726 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

727 
next 
21765  728 
case (Cond s0 e0 b s1 e1 e2 v s2) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

729 
then obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

730 
"G\<turnstile>Norm s0 \<midarrow>e0\<succ>b\<midarrow>n1\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

731 
"G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)\<succ>v\<midarrow>n2\<rightarrow> s2" 
17589  732 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

733 
then 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

734 
have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2\<succ>v\<midarrow>max n1 n2\<rightarrow> s2" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

735 
by (blast intro: evaln.Cond dest: evaln_max2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

736 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

737 
next 
21765  738 
case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

739 
then obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

740 
"G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<midarrow>n1\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

741 
"G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2" 
17589  742 
by iprover 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

743 
moreover 
23350  744 
note `invDeclC = invocation_declclass G mode (store s2) a' statT 
745 
\<lparr>name=mn,parTs=pTs'\<rparr>` 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

746 
moreover 
23350  747 
note `s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

748 
moreover 
23350  749 
note `s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

750 
moreover 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

751 
from Call.hyps 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

752 
obtain m where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

753 
"G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>\<succ>v\<midarrow>m\<rightarrow> s4" 
17589  754 
by iprover 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

755 
ultimately 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

756 
have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

757 
(set_lvars (locals (store s2))) s4" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

758 
by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

759 
thus ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

760 
next 
21765  761 
case (Methd s0 D sig v s1) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

762 
then obtain n where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

763 
"G\<turnstile>Norm s0 \<midarrow>body G D sig\<succ>v\<midarrow>n\<rightarrow> s1" 
17589  764 
by iprover 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

765 
then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig\<succ>v\<midarrow>Suc n\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

766 
by (rule evaln.Methd) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

767 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

768 
next 
21765  769 
case (Body s0 D s1 c s2 s3) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

770 
from Body.hyps obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

771 
evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

772 
evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2" 
17589  773 
by (iprover) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

774 
moreover 
23350  775 
note `s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

776 
fst s2 = Some (Jump (Cont l)) 
23350  777 
then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
778 
else s2)` 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

779 
ultimately 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

780 
have 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

781 
"G\<turnstile>Norm s0 \<midarrow>Body D c\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

782 
\<rightarrow> abupd (absorb Ret) s3" 
17589  783 
by (iprover intro: evaln.Body dest: evaln_max2) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

784 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

785 
next 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

786 
case (LVar s vn ) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

787 
obtain n where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

788 
"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s" 
17589  789 
by (iprover intro: evaln.LVar) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

790 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

791 
next 
21765  792 
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

793 
then obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

794 
"G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

795 
"G\<turnstile>s1 \<midarrow>e\<succ>a\<midarrow>n2\<rightarrow> s2" 
17589  796 
by iprover 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

797 
moreover 
23350  798 
note `s3 = check_field_access G accC statDeclC fn stat a s2'` 
799 
and `(v, s2') = fvar statDeclC stat fn a s2` 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

800 
ultimately 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

801 
have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3" 
17589  802 
by (iprover intro: evaln.FVar dest: evaln_max2) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

803 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

804 
next 
21765  805 
case (AVar s0 e1 a s1 e2 i s2 v s2') 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

806 
then obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

807 
"G\<turnstile>Norm s0 \<midarrow>e1\<succ>a\<midarrow>n1\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

808 
"G\<turnstile>s1 \<midarrow>e2\<succ>i\<midarrow>n2\<rightarrow> s2" 
17589  809 
by iprover 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

810 
moreover 
23350  811 
note `(v, s2') = avar G i a s2` 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

812 
ultimately 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

813 
have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

814 
by (blast intro!: evaln.AVar dest: evaln_max2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

815 
then show ?case .. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

816 
next 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

817 
case (Nil s0) 
17589  818 
show ?case by (iprover intro: evaln.Nil) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

819 
next 
21765  820 
case (Cons s0 e v s1 es vs s2) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

821 
then obtain n1 n2 where 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

822 
"G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<midarrow>n1\<rightarrow> s1" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

823 
"G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2" 
17589  824 
by iprover 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

825 
then 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

826 
have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

827 
by (blast intro!: evaln.Cons dest: evaln_max2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

828 
then show ?case .. 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

829 
qed 
26932  830 

12854  831 
end 