author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 32960  69916a850301 
child 54863  82acc20ded73 
permissions  rwrr 
11376  1 
(* Title: HOL/NanoJava/OpSem.thy 
2 
Author: David von Oheimb 

3 
Copyright 2001 Technische Universitaet Muenchen 

4 
*) 

5 

6 
header "Operational Evaluation Semantics" 

7 

16417  8 
theory OpSem imports State begin 
11376  9 

23755  10 
inductive 
11 
exec :: "[state,stmt, nat,state] => bool" ("_ __\<rightarrow> _" [98,90, 65,98] 89) 

12 
and eval :: "[state,expr,val,nat,state] => bool" ("_ _\<succ>__\<rightarrow> _"[98,95,99,65,98] 89) 

13 
where 

14 
Skip: " s Skipn\<rightarrow> s" 

15 

16 
 Comp: "[ s0 c1n\<rightarrow> s1; s1 c2n\<rightarrow> s2 ] ==> 

17 
s0 c1;; c2n\<rightarrow> s2" 

11376  18 

23755  19 
 Cond: "[ s0 e\<succ>vn\<rightarrow> s1; s1 (if v\<noteq>Null then c1 else c2)n\<rightarrow> s2 ] ==> 
20 
s0 If(e) c1 Else c2n\<rightarrow> s2" 

11376  21 

23755  22 
 LoopF:" s0<x> = Null ==> 
23 
s0 While(x) cn\<rightarrow> s0" 

24 
 LoopT:"[ s0<x> \<noteq> Null; s0 cn\<rightarrow> s1; s1 While(x) cn\<rightarrow> s2 ] ==> 

25 
s0 While(x) cn\<rightarrow> s2" 

11476  26 

23755  27 
 LAcc: " s LAcc x\<succ>s<x>n\<rightarrow> s" 
28 

29 
 LAss: " s e\<succ>vn\<rightarrow> s' ==> 

30 
s x:==en\<rightarrow> lupd(x\<mapsto>v) s'" 

11376  31 

23755  32 
 FAcc: " s e\<succ>Addr an\<rightarrow> s' ==> 
33 
s e..f\<succ>get_field s' a fn\<rightarrow> s'" 

11476  34 

23755  35 
 FAss: "[ s0 e1\<succ>Addr an\<rightarrow> s1; s1 e2\<succ>vn\<rightarrow> s2 ] ==> 
36 
s0 e1..f:==e2n\<rightarrow> upd_obj a f v s2" 

11476  37 

23755  38 
 NewC: " new_Addr s = Addr a ==> 
39 
s new C\<succ>Addr an\<rightarrow> new_obj a C s" 

11376  40 

23755  41 
 Cast: "[ s e\<succ>vn\<rightarrow> s'; 
11476  42 
case v of Null => True  Addr a => obj_class s' a \<preceq>C C ] ==> 
23755  43 
s Cast C e\<succ>vn\<rightarrow> s'" 
11376  44 

23755  45 
 Call: "[ s0 e1\<succ>an\<rightarrow> s1; s1 e2\<succ>pn\<rightarrow> s2; 
46 
lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) Meth (C,m)n\<rightarrow> s3 

47 
] ==> s0 {C}e1..m(e2)\<succ>s3<Res>n\<rightarrow> set_locs s2 s3" 

11376  48 

23755  49 
 Meth: "[ s<This> = Addr a; D = obj_class s a; D\<preceq>C C; 
50 
init_locs D m s Impl (D,m)n\<rightarrow> s' ] ==> 

51 
s Meth (C,m)n\<rightarrow> s'" 

11376  52 

23755  53 
 Impl: " s body Cm n\<rightarrow> s' ==> 
54 
s Impl CmSuc n\<rightarrow> s'" 

11376  55 

11476  56 

11376  57 
inductive_cases exec_elim_cases': 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

58 
"s Skip n\<rightarrow> t" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

59 
"s c1;; c2 n\<rightarrow> t" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

60 
"s If(e) c1 Else c2n\<rightarrow> t" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

61 
"s While(x) c n\<rightarrow> t" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

62 
"s x:==e n\<rightarrow> t" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

63 
"s e1..f:==e2 n\<rightarrow> t" 
11508  64 
inductive_cases Meth_elim_cases: "s Meth Cm n\<rightarrow> t" 
65 
inductive_cases Impl_elim_cases: "s Impl Cm n\<rightarrow> t" 

11376  66 
lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases 
11476  67 
inductive_cases eval_elim_cases: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

68 
"s new C \<succ>vn\<rightarrow> t" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

69 
"s Cast C e \<succ>vn\<rightarrow> t" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

70 
"s LAcc x \<succ>vn\<rightarrow> t" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

71 
"s e..f \<succ>vn\<rightarrow> t" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23755
diff
changeset

72 
"s {C}e1..m(e2) \<succ>vn\<rightarrow> t" 
11376  73 

11476  74 
lemma exec_eval_mono [rule_format]: 
75 
"(s c n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s c m\<rightarrow> t)) \<and> 

76 
(s e\<succ>vn\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s e\<succ>vm\<rightarrow> t))" 

77 
apply (rule exec_eval.induct) 

78 
prefer 14 (* Impl *) 

11376  79 
apply clarify 
80 
apply (rename_tac n) 

81 
apply (case_tac n) 

11508  82 
apply (blast intro:exec_eval.intros)+ 
11376  83 
done 
11476  84 
lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format] 
85 
lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format] 

86 

87 
lemma exec_exec_max: "\<lbrakk>s1 c1 n1 \<rightarrow> t1 ; s2 c2 n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 

88 
s1 c1max n1 n2\<rightarrow> t1 \<and> s2 c2max n1 n2\<rightarrow> t2" 

89 
by (fast intro: exec_mono le_maxI1 le_maxI2) 

11376  90 

11476  91 
lemma eval_exec_max: "\<lbrakk>s1 c n1 \<rightarrow> t1 ; s2 e\<succ>v n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
92 
s1 cmax n1 n2\<rightarrow> t1 \<and> s2 e\<succ>vmax n1 n2\<rightarrow> t2" 

93 
by (fast intro: eval_mono exec_mono le_maxI1 le_maxI2) 

94 

95 
lemma eval_eval_max: "\<lbrakk>s1 e1\<succ>v1 n1 \<rightarrow> t1 ; s2 e2\<succ>v2 n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 

96 
s1 e1\<succ>v1max n1 n2\<rightarrow> t1 \<and> s2 e2\<succ>v2max n1 n2\<rightarrow> t2" 

97 
by (fast intro: eval_mono le_maxI1 le_maxI2) 

98 

99 
lemma eval_eval_exec_max: 

100 
"\<lbrakk>s1 e1\<succ>v1n1\<rightarrow> t1; s2 e2\<succ>v2n2\<rightarrow> t2; s3 cn3\<rightarrow> t3\<rbrakk> \<Longrightarrow> 

101 
s1 e1\<succ>v1max (max n1 n2) n3\<rightarrow> t1 \<and> 

102 
s2 e2\<succ>v2max (max n1 n2) n3\<rightarrow> t2 \<and> 

103 
s3 c max (max n1 n2) n3\<rightarrow> t3" 

104 
apply (drule (1) eval_eval_max, erule thin_rl) 

105 
by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2) 

11376  106 

11565  107 
lemma Impl_body_eq: "(\<lambda>t. \<exists>n. Z Impl Mn\<rightarrow> t) = (\<lambda>t. \<exists>n. Z body Mn\<rightarrow> t)" 
11376  108 
apply (rule ext) 
11476  109 
apply (fast elim: exec_elim_cases intro: exec_eval.Impl) 
11376  110 
done 
111 

112 
end 