author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46206  d3d62b528487 
child 52847  820339715ffe 
permissions  rwrr 
8011  1 
(* Title: HOL/MicroJava/J/Conform.thy 
2 
Author: David von Oheimb 

3 
Copyright 1999 Technische Universitaet Muenchen 

11070  4 
*) 
8011  5 

12911  6 
header {* \isaheader{Conformity Relations for Type Soundness Proof} *} 
8011  7 

16417  8 
theory Conform imports State WellType Exceptions begin 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8082
diff
changeset

9 

42463  10 
type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  "same as @{text env} of @{text WellType.thy}" 
8011  11 

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

12 
definition hext :: "aheap => aheap => bool" ("_ <= _" [51,51] 50) where 
11372  13 
"h<=h' == \<forall>a C fs. h a = Some(C,fs) > (\<exists>fs'. h' a = Some(C,fs'))" 
8011  14 

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

15 
definition conf :: "'c prog => aheap => val => ty => bool" 
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
30235
diff
changeset

16 
("_,_  _ ::<= _" [51,51,51,51] 50) where 
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
26342
diff
changeset

17 
"G,hv::<=T == \<exists>T'. typeof (Option.map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T" 
8011  18 

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

19 
definition lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool" 
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
30235
diff
changeset

20 
("_,_  _ [::<=] _" [51,51,51,51] 50) where 
11372  21 
"G,hvs[::<=]Ts == \<forall>n T. Ts n = Some T > (\<exists>v. vs n = Some v \<and> G,hv::<=T)" 
8011  22 

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

23 
definition oconf :: "'c prog => aheap => obj => bool" ("_,_  _ [ok]" [51,51,51] 50) where 
11372  24 
"G,hobj [ok] == G,hsnd obj[::<=]map_of (fields (G,fst obj))" 
8011  25 

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

26 
definition hconf :: "'c prog => aheap => bool" ("_ h _ [ok]" [51,51] 50) where 
11372  27 
"Gh h [ok] == \<forall>a obj. h a = Some obj > G,hobj [ok]" 
13672  28 

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

29 
definition xconf :: "aheap \<Rightarrow> val option \<Rightarrow> bool" where 
13672  30 
"xconf hp vo == preallocated hp \<and> (\<forall> v. (vo = Some v) \<longrightarrow> (\<exists> xc. v = (Addr (XcptRef xc))))" 
8011  31 

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

32 
definition conforms :: "xstate => java_mb env' => bool" ("_ ::<= _" [51,51] 50) where 
13672  33 
"s::<=E == prg Eh heap (store s) [ok] \<and> 
34 
prg E,heap (store s)locals (store s)[::<=]localT E \<and> 

35 
xconf (heap (store s)) (abrupt s)" 

8011  36 

10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

37 

35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
30235
diff
changeset

38 
notation (xsymbols) 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
30235
diff
changeset

39 
hext ("_ \<le> _" [51,51] 50) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
30235
diff
changeset

40 
conf ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
30235
diff
changeset

41 
lconf ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
30235
diff
changeset

42 
oconf ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
30235
diff
changeset

43 
hconf ("_ \<turnstile>h _ \<surd>" [51,51] 50) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
30235
diff
changeset

44 
conforms ("_ ::\<preceq> _" [51,51] 50) 
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

45 

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

46 

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

47 
section "hext" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

48 

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

49 
lemma hextI: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

50 
" \<forall>a C fs . h a = Some (C,fs) > 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

51 
(\<exists>fs'. h' a = Some (C,fs')) ==> h\<le>h'" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

52 
apply (unfold hext_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

55 

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

56 
lemma hext_objD: "[h\<le>h'; h a = Some (C,fs) ] ==> \<exists>fs'. h' a = Some (C,fs')" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

57 
apply (unfold hext_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

58 
apply (force) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

60 

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

61 
lemma hext_refl [simp]: "h\<le>h" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

62 
apply (rule hextI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

65 

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

66 
lemma hext_new [simp]: "h a = None ==> h\<le>h(a\<mapsto>x)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

67 
apply (rule hextI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

70 

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

71 
lemma hext_trans: "[h\<le>h'; h'\<le>h''] ==> h\<le>h''" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

72 
apply (rule hextI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

73 
apply (fast dest: hext_objD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

75 

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

76 
lemma hext_upd_obj: "h a = Some (C,fs) ==> h\<le>h(a\<mapsto>(C,fs'))" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

77 
apply (rule hextI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

80 

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

81 

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

82 
section "conf" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

83 

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

84 
lemma conf_Null [simp]: "G,h\<turnstile>Null::\<preceq>T = G\<turnstile>RefT NullT\<preceq>T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

85 
apply (unfold conf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

86 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

88 

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

89 
lemma conf_litval [rule_format (no_asm), simp]: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

90 
"typeof (\<lambda>v. None) v = Some T > G,h\<turnstile>v::\<preceq>T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

91 
apply (unfold conf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

92 
apply (rule val.induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

95 

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

96 
lemma conf_AddrI: "[h a = Some obj; G\<turnstile>obj_ty obj\<preceq>T] ==> G,h\<turnstile>Addr a::\<preceq>T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

97 
apply (unfold conf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

98 
apply (simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

100 

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

101 
lemma conf_obj_AddrI: "[h a = Some (C,fs); G\<turnstile>C\<preceq>C D] ==> G,h\<turnstile>Addr a::\<preceq> Class D" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

102 
apply (unfold conf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

103 
apply (simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

105 

12517  106 
lemma defval_conf [rule_format (no_asm)]: 
107 
"is_type G T > G,h\<turnstile>default_val T::\<preceq>T" 

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

108 
apply (unfold conf_def) 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14134
diff
changeset

109 
apply (rule_tac y = "T" in ty.exhaust) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

110 
apply (erule ssubst) 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14134
diff
changeset

111 
apply (rule_tac y = "prim_ty" in prim_ty.exhaust) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

112 
apply (auto simp add: widen.null) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

114 

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

115 
lemma conf_upd_obj: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

116 
"h a = Some (C,fs) ==> (G,h(a\<mapsto>(C,fs'))\<turnstile>x::\<preceq>T) = (G,h\<turnstile>x::\<preceq>T)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

117 
apply (unfold conf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

118 
apply (rule val.induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

121 

12517  122 
lemma conf_widen [rule_format (no_asm)]: 
123 
"wf_prog wf_mb G ==> G,h\<turnstile>x::\<preceq>T > G\<turnstile>T\<preceq>T' > G,h\<turnstile>x::\<preceq>T'" 

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

124 
apply (unfold conf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

125 
apply (rule val.induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

126 
apply (auto intro: widen_trans) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

128 

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

129 
lemma conf_hext [rule_format (no_asm)]: "h\<le>h' ==> G,h\<turnstile>v::\<preceq>T > G,h'\<turnstile>v::\<preceq>T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

130 
apply (unfold conf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

131 
apply (rule val.induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

132 
apply (auto dest: hext_objD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

134 

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

135 
lemma new_locD: "[h a = None; G,h\<turnstile>Addr t::\<preceq>T] ==> t\<noteq>a" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

136 
apply (unfold conf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

139 

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

140 
lemma conf_RefTD [rule_format (no_asm)]: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

141 
"G,h\<turnstile>a'::\<preceq>RefT T > a' = Null  
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

142 
(\<exists>a obj T'. a' = Addr a \<and> h a = Some obj \<and> obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

143 
apply (unfold conf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

144 
apply(induct_tac "a'") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

145 
apply(auto) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

147 

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

148 
lemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

149 
apply (drule conf_RefTD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

152 

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

153 
lemma non_npD: "[a' \<noteq> Null; G,h\<turnstile>a'::\<preceq>RefT t] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

154 
\<exists>a C fs. a' = Addr a \<and> h a = Some (C,fs) \<and> G\<turnstile>Class C\<preceq>RefT t" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

155 
apply (drule conf_RefTD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

158 

12951  159 
lemma non_np_objD: "!!G. [a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

160 
(\<exists>a C' fs. a' = Addr a \<and> h a = Some (C',fs) \<and> G\<turnstile>C'\<preceq>C C)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

161 
apply (fast dest: non_npD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

163 

12517  164 
lemma non_np_objD' [rule_format (no_asm)]: 
165 
"a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t > 

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

166 
(\<exists>a C fs. a' = Addr a \<and> h a = Some (C,fs) \<and> G\<turnstile>Class C\<preceq>RefT t)" 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14134
diff
changeset

167 
apply(rule_tac y = "t" in ref_ty.exhaust) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

168 
apply (fast dest: conf_NullTD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

169 
apply (fast dest: non_np_objD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

171 

12517  172 
lemma conf_list_gext_widen [rule_format (no_asm)]: 
173 
"wf_prog wf_mb G ==> \<forall>Ts Ts'. list_all2 (conf G h) vs Ts > 

174 
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts' > list_all2 (conf G h) vs Ts'" 

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

175 
apply(induct_tac "vs") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

176 
apply(clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

177 
apply(clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

178 
apply(frule list_all2_lengthD [THEN sym]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

179 
apply(simp (no_asm_use) add: length_Suc_conv) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

180 
apply(safe) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

181 
apply(frule list_all2_lengthD [THEN sym]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

182 
apply(simp (no_asm_use) add: length_Suc_conv) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

183 
apply(clarify) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

186 

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

187 

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

188 
section "lconf" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

189 

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

190 
lemma lconfD: "[ G,h\<turnstile>vs[::\<preceq>]Ts; Ts n = Some T ] ==> G,h\<turnstile>(the (vs n))::\<preceq>T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

191 
apply (unfold lconf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

192 
apply (force) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

194 

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

195 
lemma lconf_hext [elim]: "[ G,h\<turnstile>l[::\<preceq>]L; h\<le>h' ] ==> G,h'\<turnstile>l[::\<preceq>]L" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

196 
apply (unfold lconf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

197 
apply (fast elim: conf_hext) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

199 

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

200 
lemma lconf_upd: "!!X. [ G,h\<turnstile>l[::\<preceq>]lT; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

201 
G,h\<turnstile>v::\<preceq>T; lT va = Some T ] ==> G,h\<turnstile>l(va\<mapsto>v)[::\<preceq>]lT" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

202 
apply (unfold lconf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

205 

12517  206 
lemma lconf_init_vars_lemma [rule_format (no_asm)]: 
207 
"\<forall>x. P x > R (dv x) x ==> (\<forall>x. map_of fs f = Some x > P x) > 

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

208 
(\<forall>T. map_of fs f = Some T > 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

209 
(\<exists>v. map_of (map (\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \<and> R v T))" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

210 
apply( induct_tac "fs") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

213 

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

214 
lemma lconf_init_vars [intro!]: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

215 
"\<forall>n. \<forall>T. map_of fs n = Some T > is_type G T ==> G,h\<turnstile>init_vars fs[::\<preceq>]map_of fs" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

216 
apply (unfold lconf_def init_vars_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

218 
apply( rule lconf_init_vars_lemma) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

219 
apply( erule_tac [3] asm_rl) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

220 
apply( intro strip) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

221 
apply( erule defval_conf) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

224 

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

225 
lemma lconf_ext: "[G,s\<turnstile>l[::\<preceq>]L; G,s\<turnstile>v::\<preceq>T] ==> G,s\<turnstile>l(vn\<mapsto>v)[::\<preceq>]L(vn\<mapsto>T)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

226 
apply (unfold lconf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

229 

12517  230 
lemma lconf_ext_list [rule_format (no_asm)]: 
12888  231 
"G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. distinct vns > length Ts = length vns > 
12517  232 
list_all2 (\<lambda>v T. G,h\<turnstile>v::\<preceq>T) vs Ts > G,h\<turnstile>l(vns[\<mapsto>]vs)[::\<preceq>]L(vns[\<mapsto>]Ts)" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

233 
apply (unfold lconf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

234 
apply( induct_tac "vns") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

235 
apply( clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

236 
apply( clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

237 
apply( frule list_all2_lengthD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

238 
apply( auto simp add: length_Suc_conv) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

240 

13672  241 
lemma lconf_restr: "\<lbrakk>lT vn = None; G, h \<turnstile> l [::\<preceq>] lT(vn\<mapsto>T)\<rbrakk> \<Longrightarrow> G, h \<turnstile> l [::\<preceq>] lT" 
242 
apply (unfold lconf_def) 

243 
apply (intro strip) 

244 
apply (case_tac "n = vn") 

245 
apply auto 

246 
done 

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

247 

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

248 
section "oconf" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

249 

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

250 
lemma oconf_hext: "G,h\<turnstile>obj\<surd> ==> h\<le>h' ==> G,h'\<turnstile>obj\<surd>" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

251 
apply (unfold oconf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

254 

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

255 
lemma oconf_obj: "G,h\<turnstile>(C,fs)\<surd> = 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

256 
(\<forall>T f. map_of(fields (G,C)) f = Some T > (\<exists>v. fs f = Some v \<and> G,h\<turnstile>v::\<preceq>T))" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

257 
apply (unfold oconf_def lconf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

260 

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

261 
lemmas oconf_objD = oconf_obj [THEN iffD1, THEN spec, THEN spec, THEN mp] 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

262 

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

263 

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

264 
section "hconf" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

265 

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

266 
lemma hconfD: "[G\<turnstile>h h\<surd>; h a = Some obj] ==> G,h\<turnstile>obj\<surd>" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

267 
apply (unfold hconf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

270 

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

271 
lemma hconfI: "\<forall>a obj. h a=Some obj > G,h\<turnstile>obj\<surd> ==> G\<turnstile>h h\<surd>" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

272 
apply (unfold hconf_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

275 

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

276 

13672  277 
section "xconf" 
278 

279 
lemma xconf_raise_if: "xconf h x \<Longrightarrow> xconf h (raise_if b xcn x)" 

280 
by (simp add: xconf_def raise_if_def) 

281 

282 

283 

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

284 
section "conforms" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

285 

13672  286 
lemma conforms_heapD: "(x, (h, l))::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

287 
apply (unfold conforms_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

288 
apply (simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

290 

13672  291 
lemma conforms_localD: "(x, (h, l))::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT" 
292 
apply (unfold conforms_def) 

293 
apply (simp) 

294 
done 

295 

296 
lemma conforms_xcptD: "(x, (h, l))::\<preceq>(G, lT) ==> xconf h x" 

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

297 
apply (unfold conforms_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

298 
apply (simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

300 

13672  301 
lemma conformsI: "[G\<turnstile>h h\<surd>; G,h\<turnstile>l[::\<preceq>]lT; xconf h x] ==> (x, (h, l))::\<preceq>(G, lT)" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

302 
apply (unfold conforms_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

305 

13672  306 
lemma conforms_restr: "\<lbrakk>lT vn = None; s ::\<preceq> (G, lT(vn\<mapsto>T)) \<rbrakk> \<Longrightarrow> s ::\<preceq> (G, lT)" 
307 
by (simp add: conforms_def, fast intro: lconf_restr) 

308 

309 
lemma conforms_xcpt_change: "\<lbrakk> (x, (h,l))::\<preceq> (G, lT); xconf h x \<longrightarrow> xconf h x' \<rbrakk> \<Longrightarrow> (x', (h,l))::\<preceq> (G, lT)" 

310 
by (simp add: conforms_def) 

311 

312 

313 
lemma preallocated_hext: "\<lbrakk> preallocated h; h\<le>h'\<rbrakk> \<Longrightarrow> preallocated h'" 

314 
by (simp add: preallocated_def hext_def) 

315 

316 
lemma xconf_hext: "\<lbrakk> xconf h vo; h\<le>h'\<rbrakk> \<Longrightarrow> xconf h' vo" 

317 
by (simp add: xconf_def preallocated_def hext_def) 

318 

319 
lemma conforms_hext: "[(x,(h,l))::\<preceq>(G,lT); h\<le>h'; G\<turnstile>h h'\<surd> ] 

320 
==> (x,(h',l))::\<preceq>(G,lT)" 

321 
by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext) 

322 

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

323 

12517  324 
lemma conforms_upd_obj: 
13672  325 
"[(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>h(a\<mapsto>obj)] 
326 
==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)" 

12517  327 
apply(rule conforms_hext) 
328 
apply auto 

329 
apply(rule hconfI) 

330 
apply(drule conforms_heapD) 

46206  331 
apply(auto elim: oconf_hext dest: hconfD) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

333 

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

334 
lemma conforms_upd_local: 
13672  335 
"[(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T] 
336 
==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)" 

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

337 
apply (unfold conforms_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

338 
apply( auto elim: lconf_upd) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

340 

8011  341 
end 