author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 35416  d8d7d1b785af 
child 61361  8b5f00202e1a 
permissions  rwrr 
13672  1 
(* Title: HOL/MicroJava/J/Exceptions.thy 
2 
Author: Gerwin Klein, Martin Strecker 

3 
Copyright 2002 Technische Universitaet Muenchen 

4 
*) 

5 

16417  6 
theory Exceptions imports State begin 
13672  7 

8 
text {* a new, blank object with default values in all fields: *} 

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

9 
definition blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" where 
13672  10 
"blank G C \<equiv> (C,init_vars (fields(G,C)))" 
11 

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

12 
definition start_heap :: "'c prog \<Rightarrow> aheap" where 
13672  13 
"start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) 
14 
(XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) 

15 
(XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" 

16 

17 

35102  18 
abbreviation 
13672  19 
cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname" 
35102  20 
where "cname_of hp v == fst (the (hp (the_Addr v)))" 
13672  21 

22 

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

23 
definition preallocated :: "aheap \<Rightarrow> bool" where 
13672  24 
"preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)" 
25 

26 
lemma preallocatedD: 

27 
"preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)" 

28 
by (unfold preallocated_def) fast 

29 

30 
lemma preallocatedE [elim?]: 

31 
"preallocated hp \<Longrightarrow> (\<And>fs. hp (XcptRef x) = Some (Xcpt x, fs) \<Longrightarrow> P hp) \<Longrightarrow> P hp" 

32 
by (fast dest: preallocatedD) 

33 

34 
lemma cname_of_xcp: 

35 
"raise_if b x None = Some xcp \<Longrightarrow> preallocated hp 

36 
\<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x" 

37 
proof  

38 
assume "raise_if b x None = Some xcp" 

39 
hence "xcp = Addr (XcptRef x)" 

40 
by (simp add: raise_if_def split: split_if_asm) 

41 
moreover 

42 
assume "preallocated hp" 

43 
then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" .. 

44 
ultimately 

45 
show ?thesis by simp 

46 
qed 

47 

48 
lemma preallocated_start: 

49 
"preallocated (start_heap G)" 

50 
apply (unfold preallocated_def) 

51 
apply (unfold start_heap_def) 

52 
apply (rule allI) 

53 
apply (case_tac x) 

54 
apply (auto simp add: blank_def) 

55 
done 

56 

57 

58 

59 
end 

60 