author | wenzelm |
Fri, 02 Aug 2013 12:17:55 +0200 | |
changeset 52847 | 820339715ffe |
parent 46206 | d3d62b528487 |
child 55466 | 786edc984c98 |
permissions | -rw-r--r-- |
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
re-structuring 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,h|-v::<=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,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=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,h|-obj [ok] == G,h|-snd 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 |
"G|-h h [ok] == \<forall>a obj. h a = Some obj --> G,h|-obj [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 E|-h 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 |
|
52847 | 140 |
lemma conf_RefTD [rule_format]: |
141 |
"G,h\<turnstile>a'::\<preceq>RefT T \<Longrightarrow> a' = Null \<or> |
|
11026
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)" |
52847 | 143 |
unfolding conf_def by (induct a') auto |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
144 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
145 |
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
|
146 |
apply (drule conf_RefTD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
147 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
148 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
149 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
150 |
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
|
151 |
\<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
|
152 |
apply (drule conf_RefTD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
153 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
154 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
155 |
|
12951 | 156 |
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
|
157 |
(\<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
|
158 |
apply (fast dest: non_npD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
159 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
160 |
|
12517 | 161 |
lemma non_np_objD' [rule_format (no_asm)]: |
162 |
"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
|
163 |
(\<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
|
164 |
apply(rule_tac y = "t" in ref_ty.exhaust) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
165 |
apply (fast dest: conf_NullTD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
166 |
apply (fast dest: non_np_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
167 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
168 |
|
12517 | 169 |
lemma conf_list_gext_widen [rule_format (no_asm)]: |
170 |
"wf_prog wf_mb G ==> \<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> |
|
171 |
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
|
172 |
apply(induct_tac "vs") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
173 |
apply(clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
174 |
apply(clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
175 |
apply(frule list_all2_lengthD [THEN sym]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
176 |
apply(simp (no_asm_use) add: length_Suc_conv) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
177 |
apply(safe) |
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(clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
181 |
apply(fast elim: conf_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
182 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
183 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
184 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
185 |
section "lconf" |
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 |
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
|
188 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
189 |
apply (force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
190 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
191 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
192 |
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
|
193 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
194 |
apply (fast elim: conf_hext) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
195 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
196 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
197 |
lemma lconf_upd: "!!X. [| G,h\<turnstile>l[::\<preceq>]lT; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
198 |
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
|
199 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
200 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
201 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
202 |
|
12517 | 203 |
lemma lconf_init_vars_lemma [rule_format (no_asm)]: |
204 |
"\<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
|
205 |
(\<forall>T. map_of fs f = Some T --> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
206 |
(\<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
|
207 |
apply( induct_tac "fs") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
208 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
209 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
210 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
211 |
lemma lconf_init_vars [intro!]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
212 |
"\<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
|
213 |
apply (unfold lconf_def init_vars_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
214 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
215 |
apply( rule lconf_init_vars_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
216 |
apply( erule_tac [3] asm_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
217 |
apply( intro strip) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
218 |
apply( erule defval_conf) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
219 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
220 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
221 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
222 |
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
|
223 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
224 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
225 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
226 |
|
12517 | 227 |
lemma lconf_ext_list [rule_format (no_asm)]: |
12888 | 228 |
"G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. distinct vns --> length Ts = length vns --> |
12517 | 229 |
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
|
230 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
231 |
apply( induct_tac "vns") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
232 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
233 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
234 |
apply( frule list_all2_lengthD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
235 |
apply( auto simp add: length_Suc_conv) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
236 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
237 |
|
13672 | 238 |
lemma lconf_restr: "\<lbrakk>lT vn = None; G, h \<turnstile> l [::\<preceq>] lT(vn\<mapsto>T)\<rbrakk> \<Longrightarrow> G, h \<turnstile> l [::\<preceq>] lT" |
239 |
apply (unfold lconf_def) |
|
240 |
apply (intro strip) |
|
241 |
apply (case_tac "n = vn") |
|
242 |
apply auto |
|
243 |
done |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
244 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
245 |
section "oconf" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
246 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
247 |
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
|
248 |
apply (unfold oconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
249 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
250 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
251 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
252 |
lemma oconf_obj: "G,h\<turnstile>(C,fs)\<surd> = |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
253 |
(\<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
|
254 |
apply (unfold oconf_def lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
255 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
256 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
257 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
258 |
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
|
259 |
|
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 |
section "hconf" |
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 |
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
|
264 |
apply (unfold hconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
265 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
266 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
267 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
268 |
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
|
269 |
apply (unfold hconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
270 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
271 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
272 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
273 |
|
13672 | 274 |
section "xconf" |
275 |
||
276 |
lemma xconf_raise_if: "xconf h x \<Longrightarrow> xconf h (raise_if b xcn x)" |
|
277 |
by (simp add: xconf_def raise_if_def) |
|
278 |
||
279 |
||
280 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
281 |
section "conforms" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
282 |
|
13672 | 283 |
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
|
284 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
285 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
286 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
287 |
|
13672 | 288 |
lemma conforms_localD: "(x, (h, l))::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT" |
289 |
apply (unfold conforms_def) |
|
290 |
apply (simp) |
|
291 |
done |
|
292 |
||
293 |
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
|
294 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
295 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
296 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
297 |
|
13672 | 298 |
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
|
299 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
300 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
301 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
302 |
|
13672 | 303 |
lemma conforms_restr: "\<lbrakk>lT vn = None; s ::\<preceq> (G, lT(vn\<mapsto>T)) \<rbrakk> \<Longrightarrow> s ::\<preceq> (G, lT)" |
304 |
by (simp add: conforms_def, fast intro: lconf_restr) |
|
305 |
||
306 |
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)" |
|
307 |
by (simp add: conforms_def) |
|
308 |
||
309 |
||
310 |
lemma preallocated_hext: "\<lbrakk> preallocated h; h\<le>|h'\<rbrakk> \<Longrightarrow> preallocated h'" |
|
311 |
by (simp add: preallocated_def hext_def) |
|
312 |
||
313 |
lemma xconf_hext: "\<lbrakk> xconf h vo; h\<le>|h'\<rbrakk> \<Longrightarrow> xconf h' vo" |
|
314 |
by (simp add: xconf_def preallocated_def hext_def) |
|
315 |
||
316 |
lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] |
|
317 |
==> (x,(h',l))::\<preceq>(G,lT)" |
|
52847 | 318 |
by (fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext) |
13672 | 319 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
320 |
|
12517 | 321 |
lemma conforms_upd_obj: |
13672 | 322 |
"[|(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] |
323 |
==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)" |
|
12517 | 324 |
apply(rule conforms_hext) |
325 |
apply auto |
|
326 |
apply(rule hconfI) |
|
327 |
apply(drule conforms_heapD) |
|
46206 | 328 |
apply(auto elim: oconf_hext dest: hconfD) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
329 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
330 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
331 |
lemma conforms_upd_local: |
13672 | 332 |
"[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] |
333 |
==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
334 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
335 |
apply( auto elim: lconf_upd) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
336 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
337 |
|
8011 | 338 |
end |