author | streckem |
Wed, 23 Oct 2002 16:09:02 +0200 | |
changeset 13672 | b95d12325b51 |
parent 12951 | a9fdcb71d252 |
child 14025 | d9b155757dc8 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/JTypeSafe.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
11070 | 5 |
*) |
8011 | 6 |
|
12911 | 7 |
header {* \isaheader{Type Safety Proof} *} |
8011 | 8 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
9 |
theory JTypeSafe = Eval + Conform: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
10 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
11 |
declare split_beta [simp] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
12 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
13 |
lemma NewC_conforms: |
13672 | 14 |
"[|h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> |
15 |
(x,(h(a\<mapsto>(C,(init_vars (fields (G,C))))), l))::\<preceq>(G, lT)" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
16 |
apply( erule conforms_upd_obj) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
17 |
apply( unfold oconf_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
18 |
apply( auto dest!: fields_is_type) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
19 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
20 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
21 |
lemma Cast_conf: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
22 |
"[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>Class C; G\<turnstile>C\<preceq>? D; cast_ok G D h v|] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
23 |
==> G,h\<turnstile>v::\<preceq>Class D" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
24 |
apply (unfold cast_ok_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
25 |
apply( case_tac "v = Null") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
26 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
27 |
apply( drule widen_RefT) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
28 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
29 |
apply( drule (1) non_npD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
30 |
apply( auto intro!: conf_AddrI simp add: obj_ty_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
31 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
32 |
|
13672 | 33 |
|
34 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
35 |
lemma FAcc_type_sound: |
13672 | 36 |
"[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (x,(h,l))::\<preceq>(G,lT); |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
37 |
x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
38 |
G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
39 |
apply( drule np_NoneD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
40 |
apply( erule conjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
41 |
apply( erule (1) notE impE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
42 |
apply( drule non_np_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
43 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
44 |
apply( drule conforms_heapD [THEN hconfD]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
45 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
46 |
apply( drule (2) widen_cfs_fields) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
47 |
apply( drule (1) oconf_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
48 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
49 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
50 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
51 |
lemma FAss_type_sound: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
52 |
"[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
53 |
(G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
54 |
(G, lT)\<turnstile>aa::Class C; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
55 |
field (G,C) fn = Some (fd, ft); h''\<le>|h'; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
56 |
x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>|h; |
13672 | 57 |
Norm (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
58 |
h''\<le>|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and> |
13672 | 59 |
Norm(h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
60 |
G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
61 |
apply( drule np_NoneD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
62 |
apply( erule conjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
63 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
64 |
apply( drule non_np_objD) |
12951 | 65 |
apply( assumption) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
66 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
67 |
apply( simp (no_asm_use)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
68 |
apply( frule (1) hext_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
69 |
apply( erule exE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
70 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
71 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
72 |
apply( rule conjI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
73 |
apply( fast elim: hext_trans hext_upd_obj) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
74 |
apply( rule conjI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
75 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
76 |
apply( fast elim: conf_upd_obj [THEN iffD2]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
77 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
78 |
apply( rule conforms_upd_obj) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
79 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
80 |
apply( rule_tac [2] hextI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
81 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
82 |
apply( force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
83 |
apply( rule oconf_hext) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
84 |
apply( erule_tac [2] hext_upd_obj) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
85 |
apply( drule (2) widen_cfs_fields) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
86 |
apply( rule oconf_obj [THEN iffD2]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
87 |
apply( simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
88 |
apply( intro strip) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
89 |
apply( case_tac "(aaa, b) = (fn, fd)") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
90 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
91 |
apply( fast intro: conf_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
92 |
apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
93 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
94 |
|
13672 | 95 |
|
96 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
97 |
lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
98 |
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; |
12888 | 99 |
length pTs' = length pns; distinct pns; |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
100 |
Ball (set lvars) (split (\<lambda>vn. is_type G)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
101 |
|] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
102 |
apply (unfold wf_mhead_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
103 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
104 |
apply( rule lconf_ext_list) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
105 |
apply( rule Ball_set_table [THEN lconf_init_vars]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
106 |
apply( force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
107 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
108 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
109 |
apply( erule (2) conf_list_gext_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
110 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
111 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
112 |
lemma Call_type_sound: |
13672 | 113 |
"[| wf_java_prog G; a' \<noteq> Null; Norm (h, l)::\<preceq>(G, lT); class G C = Some y; |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
114 |
max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\<le>|xh; xh\<le>|h; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
115 |
list_all2 (conf G h) pvs pTsa; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
116 |
(md, rT, pns, lvars, blk, res) = |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
117 |
the (method (G,fst (the (h (the_Addr a')))) (mn, pTs')); |
13672 | 118 |
\<forall>lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) --> |
119 |
(G, lT)\<turnstile>blk\<surd> --> h\<le>|xi \<and> (xcptb, xi, xl)::\<preceq>(G, lT); |
|
120 |
\<forall>lT. (xcptb,xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T --> |
|
121 |
xi\<le>|h' \<and> (x',h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T)); |
|
122 |
G,xh\<turnstile>a'::\<preceq> Class C |
|
123 |
|] ==> |
|
124 |
xc\<le>|h' \<and> (x',(h', l))::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
125 |
apply( drule max_spec2mheads) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
126 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
127 |
apply( drule (2) non_np_objD') |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
128 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
129 |
apply( frule (1) hext_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
130 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
131 |
apply( drule (3) Call_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
132 |
apply( clarsimp simp add: wf_java_mdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
133 |
apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl) |
13672 | 134 |
apply( drule spec, erule impE, erule_tac [2] notE impE, tactic "assume_tac 2") |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
135 |
apply( rule conformsI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
136 |
apply( erule conforms_heapD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
137 |
apply( rule lconf_ext) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
138 |
apply( force elim!: Call_lemma2) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
139 |
apply( erule conf_hext, erule (1) conf_obj_AddrI) |
13672 | 140 |
apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl) |
141 |
apply (simp add: conforms_def) |
|
142 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
143 |
apply( erule conjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
144 |
apply( drule spec, erule (1) impE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
145 |
apply( drule spec, erule (1) impE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
146 |
apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
147 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
148 |
apply( rule conjI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
149 |
apply( fast intro: hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
150 |
apply( rule conjI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
151 |
apply( rule_tac [2] impI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
152 |
apply( erule_tac [2] notE impE, tactic "assume_tac 2") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
153 |
apply( frule_tac [2] conf_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
154 |
apply( tactic "assume_tac 4") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
155 |
apply( tactic "assume_tac 2") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
156 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
157 |
apply( fast elim!: widen_trans) |
13672 | 158 |
apply (rule conforms_xcpt_change) |
159 |
apply( rule conforms_hext) apply assumption |
|
160 |
(* apply( erule conforms_hext)*) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
161 |
apply( erule (1) hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
162 |
apply( erule conforms_heapD) |
13672 | 163 |
apply (simp add: conforms_def) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
164 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
165 |
|
13672 | 166 |
|
167 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
168 |
declare split_if [split del] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
169 |
declare fun_upd_apply [simp del] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
170 |
declare fun_upd_same [simp] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
171 |
ML{* |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
172 |
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac, |
12517 | 173 |
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)])) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
174 |
*} |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
175 |
ML{* |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
176 |
Unify.search_bound := 40; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
177 |
Unify.trace_bound := 40 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
178 |
*} |
13672 | 179 |
|
180 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
181 |
theorem eval_evals_exec_type_sound: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
182 |
"wf_java_prog G ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
183 |
(G\<turnstile>(x,(h,l)) -e \<succ>v -> (x', (h',l')) --> |
13672 | 184 |
(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e :: T --> |
185 |
h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v ::\<preceq> T )))) \<and> |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
186 |
(G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) --> |
13672 | 187 |
(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts --> |
188 |
h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and> |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
189 |
(G\<turnstile>(x,(h,l)) -c -> (x', (h',l')) --> |
13672 | 190 |
(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (G,lT)\<turnstile>c \<surd> --> |
191 |
h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT)))" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
192 |
apply( rule eval_evals_exec_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
193 |
apply( unfold c_hupd_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
194 |
|
12517 | 195 |
-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
196 |
apply( simp_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
197 |
apply( tactic "ALLGOALS strip_tac") |
12517 | 198 |
apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") |
199 |
THEN_ALL_NEW Full_simp_tac) *}) |
|
200 |
apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])") |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
201 |
|
12517 | 202 |
-- "Level 7" |
203 |
-- "15 NewC" |
|
13672 | 204 |
apply (drule sym) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
205 |
apply( drule new_AddrD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
206 |
apply( erule disjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
207 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
208 |
apply( simp (no_asm_simp)) |
13672 | 209 |
apply (rule conforms_xcpt_change, assumption) |
210 |
apply (simp (no_asm_simp) add: xconf_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
211 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
212 |
apply( rule conjI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
213 |
apply( force elim!: NewC_conforms) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
214 |
apply( rule conf_obj_AddrI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
215 |
apply( rule_tac [2] rtrancl_refl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
216 |
apply( simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
217 |
|
12517 | 218 |
-- "for Cast" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
219 |
defer 1 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
220 |
|
12517 | 221 |
-- "14 Lit" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
222 |
apply( erule conf_litval) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
223 |
|
12517 | 224 |
-- "13 BinOp" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
225 |
apply (tactic "forward_hyp_tac") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
226 |
apply (tactic "forward_hyp_tac") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
227 |
apply( rule conjI, erule (1) hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
228 |
apply( erule conjI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
229 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
230 |
apply( drule eval_no_xcpt) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
231 |
apply( simp split add: binop.split) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
232 |
|
12517 | 233 |
-- "12 LAcc" |
13672 | 234 |
apply simp |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
235 |
apply( fast elim: conforms_localD [THEN lconfD]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
236 |
|
12517 | 237 |
-- "for FAss" |
238 |
apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") |
|
239 |
THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*}) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
240 |
|
12517 | 241 |
-- "for if" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
242 |
apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*}) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
243 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
244 |
apply (tactic "forward_hyp_tac") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
245 |
|
12517 | 246 |
-- "11+1 if" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
247 |
prefer 8 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
248 |
apply( fast intro: hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
249 |
prefer 8 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
250 |
apply( fast intro: hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
251 |
|
12517 | 252 |
-- "10 Expr" |
13672 | 253 |
prefer 7 |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
254 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
255 |
|
12517 | 256 |
-- "9 ???" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
257 |
apply( simp_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
258 |
|
12517 | 259 |
-- "8 Cast" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
260 |
prefer 8 |
13672 | 261 |
apply (rule conjI) |
262 |
apply (fast intro: conforms_xcpt_change xconf_raise_if) |
|
263 |
||
264 |
apply clarify |
|
265 |
apply (drule raise_if_NoneD) |
|
266 |
apply (clarsimp) |
|
267 |
apply (rule Cast_conf) |
|
268 |
apply assumption+ |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
269 |
|
12517 | 270 |
-- "7 LAss" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
271 |
apply (fold fun_upd_def) |
12517 | 272 |
apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") |
273 |
THEN_ALL_NEW Full_simp_tac) 1 *}) |
|
13672 | 274 |
apply (intro strip) |
275 |
apply (case_tac E) |
|
276 |
apply (simp) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
277 |
apply( blast intro: conforms_upd_local conf_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
278 |
|
12517 | 279 |
-- "6 FAcc" |
13672 | 280 |
apply (rule conjI) |
281 |
apply (simp add: np_def) |
|
282 |
apply (fast intro: conforms_xcpt_change xconf_raise_if) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
283 |
apply( fast elim!: FAcc_type_sound) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
284 |
|
12517 | 285 |
-- "5 While" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
286 |
prefer 5 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
287 |
apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
288 |
apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
289 |
apply(force elim: hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
290 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
291 |
apply (tactic "forward_hyp_tac") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
292 |
|
13672 | 293 |
-- "4 Cond" |
294 |
prefer 4 |
|
295 |
apply (case_tac "the_Bool v") |
|
296 |
apply simp |
|
297 |
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) |
|
298 |
apply simp |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
299 |
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
300 |
|
12517 | 301 |
-- "3 ;;" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
302 |
prefer 3 |
13672 | 303 |
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) |
304 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
305 |
|
12517 | 306 |
-- "2 FAss" |
13672 | 307 |
apply (subgoal_tac "(np a' x1, ab, ba) ::\<preceq> (G, lT)") |
308 |
prefer 2 |
|
309 |
apply (simp add: np_def) |
|
310 |
apply (fast intro: conforms_xcpt_change xconf_raise_if) |
|
311 |
apply( case_tac "x2") |
|
312 |
-- "x2 = None" |
|
313 |
apply (simp) |
|
314 |
apply (tactic forward_hyp_tac, clarify) |
|
315 |
apply( drule eval_no_xcpt) |
|
316 |
apply( erule FAss_type_sound, rule HOL.refl, assumption+) |
|
317 |
-- "x2 = Some a" |
|
318 |
apply ( simp (no_asm_simp)) |
|
319 |
apply( fast intro: hext_trans) |
|
320 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
321 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
322 |
apply( tactic prune_params_tac) |
12517 | 323 |
-- "Level 52" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
324 |
|
12517 | 325 |
-- "1 Call" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
326 |
apply( case_tac "x") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
327 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
328 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
329 |
apply( drule exec_xcpt) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
330 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
331 |
apply( drule_tac eval_xcpt) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
332 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
333 |
apply( fast elim: hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
334 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
335 |
apply( drule evals_no_xcpt) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
336 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
337 |
apply( case_tac "a' = Null") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
338 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
339 |
apply( drule exec_xcpt) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
340 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
341 |
apply( drule eval_xcpt) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
342 |
apply( simp) |
13672 | 343 |
apply (rule conjI) |
344 |
apply( fast elim: hext_trans) |
|
345 |
apply (rule conforms_xcpt_change, assumption) apply (simp (no_asm_simp) add: xconf_def) |
|
346 |
apply(clarsimp) |
|
347 |
||
348 |
apply( drule ty_expr_is_type, simp) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
349 |
apply(clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
350 |
apply(unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
351 |
apply(clarsimp) |
13672 | 352 |
|
11644
3dfde687f0d7
Removed some unfoldings of defs after declaring wf_java_prog as syntax
streckem
parents:
11070
diff
changeset
|
353 |
apply(rule Call_type_sound); |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
354 |
prefer 11 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
355 |
apply blast |
11644
3dfde687f0d7
Removed some unfoldings of defs after declaring wf_java_prog as syntax
streckem
parents:
11070
diff
changeset
|
356 |
apply (simp (no_asm_simp))+ |
13672 | 357 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
358 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
359 |
ML{* |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
360 |
Unify.search_bound := 20; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
361 |
Unify.trace_bound := 20 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
362 |
*} |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
363 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
364 |
lemma eval_type_sound: "!!E s s'. |
13672 | 365 |
[| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T |] |
366 |
==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
367 |
apply( simp (no_asm_simp) only: split_tupled_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
368 |
apply (drule eval_evals_exec_type_sound |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
369 |
[THEN conjunct1, THEN mp, THEN spec, THEN mp]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
370 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
371 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
372 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
373 |
lemma exec_type_sound: "!!E s s'. |
13672 | 374 |
[| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd> |] |
375 |
==> (x',s')::\<preceq>E" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
376 |
apply( simp (no_asm_simp) only: split_tupled_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
377 |
apply (drule eval_evals_exec_type_sound |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
378 |
[THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
379 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
380 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
381 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
382 |
theorem all_methods_understood: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
383 |
"[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; |
13672 | 384 |
(x,s)::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
385 |
method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
386 |
apply( drule (4) eval_type_sound) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
387 |
apply(clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
388 |
apply( frule widen_methd) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
389 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
390 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
391 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
392 |
apply( drule non_npD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
393 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
394 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
395 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
396 |
declare split_beta [simp del] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
397 |
declare fun_upd_apply [simp] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
398 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
399 |
end |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
400 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
401 |