author | nipkow |
Wed, 04 Mar 2009 10:47:20 +0100 | |
changeset 30235 | 58d147683393 |
parent 26342 | 0f65fa163304 |
child 35355 | 613e133966ea |
child 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/Conform.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
11070 | 5 |
*) |
8011 | 6 |
|
12911 | 7 |
header {* \isaheader{Conformity Relations for Type Soundness Proof} *} |
8011 | 8 |
|
16417 | 9 |
theory Conform imports State WellType Exceptions begin |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8082
diff
changeset
|
10 |
|
24783 | 11 |
types 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}" |
8011 | 12 |
|
13 |
constdefs |
|
14 |
||
11372 | 15 |
hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) |
16 |
"h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))" |
|
8011 | 17 |
|
12517 | 18 |
conf :: "'c prog => aheap => val => ty => bool" |
11372 | 19 |
("_,_ |- _ ::<= _" [51,51,51,51] 50) |
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
26342
diff
changeset
|
20 |
"G,h|-v::<=T == \<exists>T'. typeof (Option.map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T" |
8011 | 21 |
|
14134 | 22 |
lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool" |
11372 | 23 |
("_,_ |- _ [::<=] _" [51,51,51,51] 50) |
24 |
"G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)" |
|
8011 | 25 |
|
11372 | 26 |
oconf :: "'c prog => aheap => obj => bool" ("_,_ |- _ [ok]" [51,51,51] 50) |
27 |
"G,h|-obj [ok] == G,h|-snd obj[::<=]map_of (fields (G,fst obj))" |
|
8011 | 28 |
|
11372 | 29 |
hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50) |
30 |
"G|-h h [ok] == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]" |
|
13672 | 31 |
|
32 |
xconf :: "aheap \<Rightarrow> val option \<Rightarrow> bool" |
|
33 |
"xconf hp vo == preallocated hp \<and> (\<forall> v. (vo = Some v) \<longrightarrow> (\<exists> xc. v = (Addr (XcptRef xc))))" |
|
8011 | 34 |
|
24783 | 35 |
conforms :: "xstate => java_mb env' => bool" ("_ ::<= _" [51,51] 50) |
13672 | 36 |
"s::<=E == prg E|-h heap (store s) [ok] \<and> |
37 |
prg E,heap (store s)|-locals (store s)[::<=]localT E \<and> |
|
38 |
xconf (heap (store s)) (abrupt s)" |
|
8011 | 39 |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
40 |
|
11372 | 41 |
syntax (xsymbols) |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
42 |
hext :: "aheap => aheap => bool" |
11372 | 43 |
("_ \<le>| _" [51,51] 50) |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
44 |
|
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
45 |
conf :: "'c prog => aheap => val => ty => bool" |
11372 | 46 |
("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
47 |
|
14134 | 48 |
lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool" |
11372 | 49 |
("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
50 |
|
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
51 |
oconf :: "'c prog => aheap => obj => bool" |
11372 | 52 |
("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
53 |
|
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
54 |
hconf :: "'c prog => aheap => bool" |
11372 | 55 |
("_ \<turnstile>h _ \<surd>" [51,51] 50) |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
56 |
|
24783 | 57 |
conforms :: "state => java_mb env' => bool" |
11372 | 58 |
("_ ::\<preceq> _" [51,51] 50) |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
59 |
|
11026
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 |
section "hext" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
62 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
63 |
lemma hextI: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
64 |
" \<forall>a C fs . h a = Some (C,fs) --> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
65 |
(\<exists>fs'. h' a = Some (C,fs')) ==> h\<le>|h'" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
66 |
apply (unfold hext_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
67 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
68 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
69 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
70 |
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
|
71 |
apply (unfold hext_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
72 |
apply (force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
73 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
74 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
75 |
lemma hext_refl [simp]: "h\<le>|h" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
76 |
apply (rule hextI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
77 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
78 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
79 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
80 |
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
|
81 |
apply (rule hextI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
82 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
83 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
84 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
85 |
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
|
86 |
apply (rule hextI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
87 |
apply (fast dest: hext_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
88 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
89 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
90 |
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
|
91 |
apply (rule hextI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
92 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
93 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
94 |
|
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 |
section "conf" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
97 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
98 |
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
|
99 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
100 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
101 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
102 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
103 |
lemma conf_litval [rule_format (no_asm), simp]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
104 |
"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
|
105 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
106 |
apply (rule val.induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
107 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
108 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
109 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
110 |
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
|
111 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
112 |
apply (simp) |
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_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
|
116 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
117 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
118 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
119 |
|
12517 | 120 |
lemma defval_conf [rule_format (no_asm)]: |
121 |
"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
|
122 |
apply (unfold conf_def) |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14134
diff
changeset
|
123 |
apply (rule_tac y = "T" in ty.exhaust) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
124 |
apply (erule ssubst) |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14134
diff
changeset
|
125 |
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
|
126 |
apply (auto simp add: widen.null) |
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_upd_obj: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
130 |
"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
|
131 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
132 |
apply (rule val.induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
133 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
134 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
135 |
|
12517 | 136 |
lemma conf_widen [rule_format (no_asm)]: |
137 |
"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
|
138 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
139 |
apply (rule val.induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
140 |
apply (auto intro: widen_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
141 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
142 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
143 |
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
|
144 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
145 |
apply (rule val.induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
146 |
apply (auto dest: hext_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
147 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
148 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
149 |
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
|
150 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
151 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
152 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
153 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
154 |
lemma conf_RefTD [rule_format (no_asm)]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
155 |
"G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null | |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
156 |
(\<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
|
157 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
158 |
apply(induct_tac "a'") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
159 |
apply(auto) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
160 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
161 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
162 |
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
|
163 |
apply (drule conf_RefTD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
164 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
165 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
166 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
167 |
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
|
168 |
\<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
|
169 |
apply (drule conf_RefTD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
170 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
171 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
172 |
|
12951 | 173 |
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
|
174 |
(\<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
|
175 |
apply (fast dest: non_npD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
176 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
177 |
|
12517 | 178 |
lemma non_np_objD' [rule_format (no_asm)]: |
179 |
"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
|
180 |
(\<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
|
181 |
apply(rule_tac y = "t" in ref_ty.exhaust) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
182 |
apply (fast dest: conf_NullTD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
183 |
apply (fast dest: non_np_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
184 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
185 |
|
12517 | 186 |
lemma conf_list_gext_widen [rule_format (no_asm)]: |
187 |
"wf_prog wf_mb G ==> \<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> |
|
188 |
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
|
189 |
apply(induct_tac "vs") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
190 |
apply(clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
191 |
apply(clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
192 |
apply(frule list_all2_lengthD [THEN sym]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
193 |
apply(simp (no_asm_use) add: length_Suc_conv) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
194 |
apply(safe) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
195 |
apply(frule list_all2_lengthD [THEN sym]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
196 |
apply(simp (no_asm_use) add: length_Suc_conv) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
197 |
apply(clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
198 |
apply(fast elim: conf_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
199 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
200 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
201 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
202 |
section "lconf" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
203 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
204 |
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
|
205 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
206 |
apply (force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
207 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
208 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
209 |
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
|
210 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
211 |
apply (fast elim: conf_hext) |
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_upd: "!!X. [| G,h\<turnstile>l[::\<preceq>]lT; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
215 |
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
|
216 |
apply (unfold lconf_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 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
219 |
|
12517 | 220 |
lemma lconf_init_vars_lemma [rule_format (no_asm)]: |
221 |
"\<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
|
222 |
(\<forall>T. map_of fs f = Some T --> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
223 |
(\<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
|
224 |
apply( induct_tac "fs") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
225 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
226 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
227 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
228 |
lemma lconf_init_vars [intro!]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
229 |
"\<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
|
230 |
apply (unfold lconf_def init_vars_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
231 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
232 |
apply( rule lconf_init_vars_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
233 |
apply( erule_tac [3] asm_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
234 |
apply( intro strip) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
235 |
apply( erule defval_conf) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
236 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
237 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
238 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
239 |
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
|
240 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
241 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
242 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
243 |
|
12517 | 244 |
lemma lconf_ext_list [rule_format (no_asm)]: |
12888 | 245 |
"G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. distinct vns --> length Ts = length vns --> |
12517 | 246 |
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
|
247 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
248 |
apply( induct_tac "vns") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
249 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
250 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
251 |
apply( frule list_all2_lengthD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
252 |
apply( auto simp add: length_Suc_conv) |
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 |
|
13672 | 255 |
lemma lconf_restr: "\<lbrakk>lT vn = None; G, h \<turnstile> l [::\<preceq>] lT(vn\<mapsto>T)\<rbrakk> \<Longrightarrow> G, h \<turnstile> l [::\<preceq>] lT" |
256 |
apply (unfold lconf_def) |
|
257 |
apply (intro strip) |
|
258 |
apply (case_tac "n = vn") |
|
259 |
apply auto |
|
260 |
done |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
261 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
262 |
section "oconf" |
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 |
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
|
265 |
apply (unfold oconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
266 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
267 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
268 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
269 |
lemma oconf_obj: "G,h\<turnstile>(C,fs)\<surd> = |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
270 |
(\<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
|
271 |
apply (unfold oconf_def lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
272 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
273 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
274 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
275 |
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
|
276 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
277 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
278 |
section "hconf" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
279 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
280 |
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
|
281 |
apply (unfold hconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
282 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
283 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
284 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
285 |
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
|
286 |
apply (unfold hconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
287 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
288 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
289 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
290 |
|
13672 | 291 |
section "xconf" |
292 |
||
293 |
lemma xconf_raise_if: "xconf h x \<Longrightarrow> xconf h (raise_if b xcn x)" |
|
294 |
by (simp add: xconf_def raise_if_def) |
|
295 |
||
296 |
||
297 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
298 |
section "conforms" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
299 |
|
13672 | 300 |
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
|
301 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
302 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
303 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
304 |
|
13672 | 305 |
lemma conforms_localD: "(x, (h, l))::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT" |
306 |
apply (unfold conforms_def) |
|
307 |
apply (simp) |
|
308 |
done |
|
309 |
||
310 |
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
|
311 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
312 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
313 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
314 |
|
13672 | 315 |
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
|
316 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
317 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
318 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
319 |
|
13672 | 320 |
lemma conforms_restr: "\<lbrakk>lT vn = None; s ::\<preceq> (G, lT(vn\<mapsto>T)) \<rbrakk> \<Longrightarrow> s ::\<preceq> (G, lT)" |
321 |
by (simp add: conforms_def, fast intro: lconf_restr) |
|
322 |
||
323 |
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)" |
|
324 |
by (simp add: conforms_def) |
|
325 |
||
326 |
||
327 |
lemma preallocated_hext: "\<lbrakk> preallocated h; h\<le>|h'\<rbrakk> \<Longrightarrow> preallocated h'" |
|
328 |
by (simp add: preallocated_def hext_def) |
|
329 |
||
330 |
lemma xconf_hext: "\<lbrakk> xconf h vo; h\<le>|h'\<rbrakk> \<Longrightarrow> xconf h' vo" |
|
331 |
by (simp add: xconf_def preallocated_def hext_def) |
|
332 |
||
333 |
lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] |
|
334 |
==> (x,(h',l))::\<preceq>(G,lT)" |
|
335 |
by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext) |
|
336 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
337 |
|
12517 | 338 |
lemma conforms_upd_obj: |
13672 | 339 |
"[|(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] |
340 |
==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)" |
|
12517 | 341 |
apply(rule conforms_hext) |
342 |
apply auto |
|
343 |
apply(rule hconfI) |
|
344 |
apply(drule conforms_heapD) |
|
345 |
apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] |
|
26342 | 346 |
addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *}) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
347 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
348 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
349 |
lemma conforms_upd_local: |
13672 | 350 |
"[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] |
351 |
==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
352 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
353 |
apply( auto elim: lconf_upd) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
354 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
355 |
|
8011 | 356 |
end |