author | wenzelm |
Wed, 24 Feb 2010 22:09:50 +0100 | |
changeset 35355 | 613e133966ea |
parent 30235 | 58d147683393 |
child 35417 | 47ee18b6ae32 |
permissions | -rwxr-xr-x |
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 |
|
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
30235
diff
changeset
|
41 |
notation (xsymbols) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
30235
diff
changeset
|
42 |
hext ("_ \<le>| _" [51,51] 50) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
30235
diff
changeset
|
43 |
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
|
44 |
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
|
45 |
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
|
46 |
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
|
47 |
conforms ("_ ::\<preceq> _" [51,51] 50) |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
48 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
49 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
50 |
section "hext" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
51 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
52 |
lemma hextI: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
53 |
" \<forall>a C fs . h a = Some (C,fs) --> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
54 |
(\<exists>fs'. h' a = Some (C,fs')) ==> h\<le>|h'" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
55 |
apply (unfold hext_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
56 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
57 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
58 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
59 |
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
|
60 |
apply (unfold hext_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
61 |
apply (force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
62 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
63 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
64 |
lemma hext_refl [simp]: "h\<le>|h" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
65 |
apply (rule hextI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
66 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
67 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
68 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
69 |
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
|
70 |
apply (rule hextI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
71 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
72 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
73 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
74 |
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
|
75 |
apply (rule hextI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
76 |
apply (fast dest: hext_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
77 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
78 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
79 |
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
|
80 |
apply (rule hextI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
81 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
82 |
done |
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 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
85 |
section "conf" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
86 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
87 |
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
|
88 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
89 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
90 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
91 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
92 |
lemma conf_litval [rule_format (no_asm), simp]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
93 |
"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
|
94 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
95 |
apply (rule val.induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
96 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
97 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
98 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
99 |
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
|
100 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
101 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
102 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
103 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
104 |
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
|
105 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
106 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
107 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
108 |
|
12517 | 109 |
lemma defval_conf [rule_format (no_asm)]: |
110 |
"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
|
111 |
apply (unfold conf_def) |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14134
diff
changeset
|
112 |
apply (rule_tac y = "T" in ty.exhaust) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
113 |
apply (erule ssubst) |
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
14134
diff
changeset
|
114 |
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
|
115 |
apply (auto simp add: widen.null) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
116 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
117 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
118 |
lemma conf_upd_obj: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
119 |
"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
|
120 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
121 |
apply (rule val.induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
122 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
123 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
124 |
|
12517 | 125 |
lemma conf_widen [rule_format (no_asm)]: |
126 |
"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
|
127 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
128 |
apply (rule val.induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
129 |
apply (auto intro: widen_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
130 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
131 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
132 |
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
|
133 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
134 |
apply (rule val.induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
135 |
apply (auto dest: hext_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
136 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
137 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
138 |
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
|
139 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
140 |
apply auto |
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_RefTD [rule_format (no_asm)]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
144 |
"G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null | |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
145 |
(\<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
|
146 |
apply (unfold conf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
147 |
apply(induct_tac "a'") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
148 |
apply(auto) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
149 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
150 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
151 |
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
|
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 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
156 |
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
|
157 |
\<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
|
158 |
apply (drule conf_RefTD) |
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 |
|
12951 | 162 |
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
|
163 |
(\<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
|
164 |
apply (fast dest: non_npD) |
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 |
|
12517 | 167 |
lemma non_np_objD' [rule_format (no_asm)]: |
168 |
"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
|
169 |
(\<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
|
170 |
apply(rule_tac y = "t" in ref_ty.exhaust) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
171 |
apply (fast dest: conf_NullTD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
172 |
apply (fast dest: non_np_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
173 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
174 |
|
12517 | 175 |
lemma conf_list_gext_widen [rule_format (no_asm)]: |
176 |
"wf_prog wf_mb G ==> \<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> |
|
177 |
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
|
178 |
apply(induct_tac "vs") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
179 |
apply(clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
180 |
apply(clarsimp) |
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(safe) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
184 |
apply(frule list_all2_lengthD [THEN sym]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
185 |
apply(simp (no_asm_use) add: length_Suc_conv) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
186 |
apply(clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
187 |
apply(fast elim: conf_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
188 |
done |
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 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
191 |
section "lconf" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
192 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
193 |
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
|
194 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
195 |
apply (force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
196 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
197 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
198 |
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
|
199 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
200 |
apply (fast elim: conf_hext) |
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 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
203 |
lemma lconf_upd: "!!X. [| G,h\<turnstile>l[::\<preceq>]lT; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
204 |
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
|
205 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
206 |
apply auto |
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 |
|
12517 | 209 |
lemma lconf_init_vars_lemma [rule_format (no_asm)]: |
210 |
"\<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
|
211 |
(\<forall>T. map_of fs f = Some T --> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
212 |
(\<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
|
213 |
apply( induct_tac "fs") |
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 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
216 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
217 |
lemma lconf_init_vars [intro!]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
218 |
"\<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
|
219 |
apply (unfold lconf_def init_vars_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
220 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
221 |
apply( rule lconf_init_vars_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
222 |
apply( erule_tac [3] asm_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
223 |
apply( intro strip) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
224 |
apply( erule defval_conf) |
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_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
|
229 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
230 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
231 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
232 |
|
12517 | 233 |
lemma lconf_ext_list [rule_format (no_asm)]: |
12888 | 234 |
"G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. distinct vns --> length Ts = length vns --> |
12517 | 235 |
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
|
236 |
apply (unfold lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
237 |
apply( induct_tac "vns") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
238 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
239 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
240 |
apply( frule list_all2_lengthD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
241 |
apply( auto simp add: length_Suc_conv) |
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 |
|
13672 | 244 |
lemma lconf_restr: "\<lbrakk>lT vn = None; G, h \<turnstile> l [::\<preceq>] lT(vn\<mapsto>T)\<rbrakk> \<Longrightarrow> G, h \<turnstile> l [::\<preceq>] lT" |
245 |
apply (unfold lconf_def) |
|
246 |
apply (intro strip) |
|
247 |
apply (case_tac "n = vn") |
|
248 |
apply auto |
|
249 |
done |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
250 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
251 |
section "oconf" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
252 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
253 |
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
|
254 |
apply (unfold oconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
255 |
apply (fast) |
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 |
lemma oconf_obj: "G,h\<turnstile>(C,fs)\<surd> = |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
259 |
(\<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
|
260 |
apply (unfold oconf_def lconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
261 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
262 |
done |
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 |
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
|
265 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
266 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
267 |
section "hconf" |
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 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
|
270 |
apply (unfold hconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
271 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
272 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
273 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
274 |
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
|
275 |
apply (unfold hconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
276 |
apply (fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
277 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
278 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
279 |
|
13672 | 280 |
section "xconf" |
281 |
||
282 |
lemma xconf_raise_if: "xconf h x \<Longrightarrow> xconf h (raise_if b xcn x)" |
|
283 |
by (simp add: xconf_def raise_if_def) |
|
284 |
||
285 |
||
286 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
287 |
section "conforms" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
288 |
|
13672 | 289 |
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
|
290 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
291 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
292 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
293 |
|
13672 | 294 |
lemma conforms_localD: "(x, (h, l))::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT" |
295 |
apply (unfold conforms_def) |
|
296 |
apply (simp) |
|
297 |
done |
|
298 |
||
299 |
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
|
300 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
301 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
302 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
303 |
|
13672 | 304 |
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
|
305 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
306 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
307 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
308 |
|
13672 | 309 |
lemma conforms_restr: "\<lbrakk>lT vn = None; s ::\<preceq> (G, lT(vn\<mapsto>T)) \<rbrakk> \<Longrightarrow> s ::\<preceq> (G, lT)" |
310 |
by (simp add: conforms_def, fast intro: lconf_restr) |
|
311 |
||
312 |
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)" |
|
313 |
by (simp add: conforms_def) |
|
314 |
||
315 |
||
316 |
lemma preallocated_hext: "\<lbrakk> preallocated h; h\<le>|h'\<rbrakk> \<Longrightarrow> preallocated h'" |
|
317 |
by (simp add: preallocated_def hext_def) |
|
318 |
||
319 |
lemma xconf_hext: "\<lbrakk> xconf h vo; h\<le>|h'\<rbrakk> \<Longrightarrow> xconf h' vo" |
|
320 |
by (simp add: xconf_def preallocated_def hext_def) |
|
321 |
||
322 |
lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] |
|
323 |
==> (x,(h',l))::\<preceq>(G,lT)" |
|
324 |
by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext) |
|
325 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
326 |
|
12517 | 327 |
lemma conforms_upd_obj: |
13672 | 328 |
"[|(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] |
329 |
==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)" |
|
12517 | 330 |
apply(rule conforms_hext) |
331 |
apply auto |
|
332 |
apply(rule hconfI) |
|
333 |
apply(drule conforms_heapD) |
|
334 |
apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] |
|
26342 | 335 |
addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *}) |
11026
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 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
338 |
lemma conforms_upd_local: |
13672 | 339 |
"[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] |
340 |
==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
341 |
apply (unfold conforms_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
342 |
apply( auto elim: lconf_upd) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
343 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
344 |
|
8011 | 345 |
end |