author | paulson |
Fri, 15 Sep 2000 15:30:50 +0200 | |
changeset 9970 | dfe4747c8318 |
parent 9941 | fe05af7ec816 |
child 10042 | 7164dc0d24d8 |
permissions | -rw-r--r-- |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
1 |
(* Title: HOL/MicroJava/BV/BVLCorrect.thy |
8245 | 2 |
ID: $Id$ |
3 |
Author: Gerwin Klein |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
9054 | 5 |
*) |
8245 | 6 |
|
9054 | 7 |
header {* Correctness of the LBV *} |
8245 | 8 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
9 |
theory LBVCorrect = BVSpec + LBVSpec: |
8245 | 10 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
11 |
lemmas [simp del] = split_paired_Ex split_paired_All |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
12 |
|
8245 | 13 |
constdefs |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
14 |
fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> bool" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
15 |
"fits phi is G rT s0 cert \<equiv> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
16 |
(\<forall>pc s1. pc < length is \<longrightarrow> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
17 |
(wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 \<longrightarrow> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
18 |
(case cert!pc of None \<Rightarrow> phi!pc = s1 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
19 |
| Some t \<Rightarrow> phi!pc = Some t)))" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
20 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
21 |
constdefs |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
22 |
make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> method_type" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
23 |
"make_phi is G rT s0 cert \<equiv> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
24 |
map (\<lambda>pc. case cert!pc of |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
25 |
None \<Rightarrow> val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
26 |
| Some t \<Rightarrow> Some t) [0..length is(]" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
27 |
|
9012 | 28 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
29 |
lemma fitsD_None: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
30 |
"\<lbrakk>fits phi is G rT s0 cert; pc < length is; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
31 |
wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
32 |
cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
33 |
by (auto simp add: fits_def) |
9012 | 34 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
35 |
lemma fitsD_Some: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
36 |
"\<lbrakk>fits phi is G rT s0 cert; pc < length is; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
37 |
wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
38 |
cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
39 |
by (auto simp add: fits_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
40 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
41 |
lemma make_phi_Some: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
42 |
"[| pc < length is; cert!pc = Some t |] ==> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
43 |
make_phi is G rT s0 cert ! pc = Some t" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
44 |
by (simp add: make_phi_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
45 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
46 |
lemma make_phi_None: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
47 |
"[| pc < length is; cert!pc = None |] ==> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
48 |
make_phi is G rT s0 cert ! pc = |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
49 |
val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
50 |
by (simp add: make_phi_def) |
9012 | 51 |
|
52 |
lemma exists_phi: |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
53 |
"\<exists>phi. fits phi is G rT s0 cert" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
54 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
55 |
have "fits (make_phi is G rT s0 cert) is G rT s0 cert" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
56 |
by (auto simp add: fits_def make_phi_Some make_phi_None |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
57 |
split: option.splits) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
58 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
59 |
thus ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
60 |
by blast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
61 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
62 |
|
9012 | 63 |
lemma fits_lemma1: |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
64 |
"[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |] |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
65 |
==> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
66 |
proof (intro strip) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
67 |
fix pc t |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
68 |
assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
69 |
then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
70 |
obtain s'' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
71 |
"wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
72 |
by (blast dest: wtl_take) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
73 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
74 |
assume "fits phi is G rT s cert" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
75 |
"pc < length is" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
76 |
"cert ! pc = Some t" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
77 |
ultimately |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
78 |
show "phi!pc = Some t" by (auto dest: fitsD_Some) |
9580 | 79 |
qed |
9012 | 80 |
|
81 |
||
82 |
lemma wtl_suc_pc: |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
83 |
"[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
84 |
wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
85 |
wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
86 |
fits phi is G rT s cert; Suc pc < length is |] ==> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
87 |
G \<turnstile> s'' <=' phi ! Suc pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
88 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
89 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
90 |
assume all: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
91 |
assume fits: "fits phi is G rT s cert" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
92 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
93 |
assume wtl: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
94 |
wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
95 |
pc: "Suc pc < length is" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
96 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
97 |
hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
98 |
by (rule wtl_Suc) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
99 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
100 |
from all |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
101 |
have app: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
102 |
"wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert (length is) 0 s \<noteq> Err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
103 |
by simp |
9012 | 104 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
105 |
from pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
106 |
have "0 < length (drop (Suc pc) is)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
107 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
108 |
then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
109 |
obtain l ls where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
110 |
"drop (Suc pc) is = l#ls" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
111 |
by (auto simp add: neq_Nil_conv simp del: length_drop) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
112 |
with app wts pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
113 |
obtain x where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
114 |
"wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
115 |
by (auto simp add: wtl_append min_def simp del: append_take_drop_id) |
9012 | 116 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
117 |
hence c1: "\<And>t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
118 |
by (simp add: wtl_cert_def split: if_splits) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
119 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
120 |
from fits pc wts |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
121 |
have c2: "\<And>t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
122 |
by - (drule fitsD_Some, auto) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
123 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
124 |
from fits pc wts |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
125 |
have c3: "cert!Suc pc = None ==> phi!Suc pc = s''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
126 |
by (rule fitsD_None) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
127 |
ultimately |
9012 | 128 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
129 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
130 |
by - (cases "cert ! Suc pc", auto) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
131 |
qed |
9012 | 132 |
|
9376 | 133 |
|
9012 | 134 |
lemma wtl_fits_wt: |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
135 |
"[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
136 |
fits phi is G rT s cert; pc < length is |] ==> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
137 |
wt_instr (is!pc) G rT phi (length is) pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
138 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
139 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
140 |
assume fits: "fits phi is G rT s cert" |
9012 | 141 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
142 |
assume pc: "pc < length is" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
143 |
wtl: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
144 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
145 |
then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
146 |
obtain s' s'' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
147 |
w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
148 |
c: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
149 |
by - (drule wtl_all, auto) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
150 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
151 |
from fits wtl pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
152 |
have cert_Some: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
153 |
"\<And>t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
154 |
by (auto dest: fits_lemma1) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
155 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
156 |
from fits wtl pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
157 |
have cert_None: "cert!pc = None ==> phi!pc = s'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
158 |
by - (drule fitsD_None) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
159 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
160 |
from pc c cert_None cert_Some |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
161 |
have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = Ok s''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
162 |
by (auto simp add: wtl_cert_def split: if_splits option.splits) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
163 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
164 |
{ fix pc' |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
165 |
assume pc': "pc' \<in> set (succs (is!pc) pc)" |
9012 | 166 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
167 |
with wti |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
168 |
have less: "pc' < length is" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
169 |
by (simp add: wtl_inst_Ok) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
170 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
171 |
have "G \<turnstile> step (is!pc) G (phi!pc) <=' phi ! pc'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
172 |
proof (cases "pc' = Suc pc") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
173 |
case False |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
174 |
with wti pc' |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
175 |
have G: "G \<turnstile> step (is ! pc) G (phi ! pc) <=' cert ! pc'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
176 |
by (simp add: wtl_inst_Ok) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
177 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
178 |
hence "cert!pc' = None ==> step (is ! pc) G (phi ! pc) = None" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
179 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
180 |
hence "cert!pc' = None ==> ?thesis" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
181 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
182 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
183 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
184 |
{ fix t |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
185 |
assume "cert!pc' = Some t" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
186 |
with less |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
187 |
have "phi!pc' = cert!pc'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
188 |
by (simp add: cert_Some) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
189 |
with G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
190 |
have ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
191 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
192 |
} |
9012 | 193 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
194 |
ultimately |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
195 |
show ?thesis by blast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
196 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
197 |
case True |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
198 |
with pc' wti |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
199 |
have "step (is ! pc) G (phi ! pc) = s''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
200 |
by (simp add: wtl_inst_Ok) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
201 |
also |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
202 |
from w c fits pc wtl |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
203 |
have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
204 |
by - (drule wtl_suc_pc) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
205 |
with True less |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
206 |
have "G \<turnstile> s'' <=' phi ! Suc pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
207 |
by blast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
208 |
finally |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
209 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
210 |
by (simp add: True) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
211 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
212 |
} |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
213 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
214 |
with wti |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
215 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
216 |
by (auto simp add: wtl_inst_Ok wt_instr_def) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
217 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
218 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
219 |
|
9012 | 220 |
|
221 |
lemma fits_first: |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
222 |
"[| 0 < length is; wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
223 |
fits phi is G rT s cert |] ==> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
224 |
G \<turnstile> s <=' phi ! 0" |
9580 | 225 |
proof - |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
226 |
assume wtl: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
227 |
assume fits: "fits phi is G rT s cert" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
228 |
assume pc: "0 < length is" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
229 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
230 |
from wtl |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
231 |
have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = Ok s" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
232 |
by simp |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
233 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
234 |
with fits pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
235 |
have "cert!0 = None ==> phi!0 = s" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
236 |
by (rule fitsD_None) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
237 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
238 |
from fits pc wt0 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
239 |
have "\<And>t. cert!0 = Some t ==> phi!0 = cert!0" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
240 |
by - (drule fitsD_Some, auto) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
241 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
242 |
from pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
243 |
obtain x xs where "is = x#xs" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
244 |
by (simp add: neq_Nil_conv) (elim, rule that) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
245 |
with wtl |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
246 |
obtain s' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
247 |
"wtl_cert x G rT s cert (length is) 0 = Ok s'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
248 |
by simp (elim, rule that, simp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
249 |
hence |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
250 |
"\<And>t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
251 |
by (simp add: wtl_cert_def split: if_splits) |
9012 | 252 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
253 |
ultimately |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
254 |
show ?thesis |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
255 |
by - (cases "cert!0", auto) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
256 |
qed |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
257 |
|
8245 | 258 |
|
9012 | 259 |
lemma wtl_method_correct: |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
260 |
"wtl_method G C pTs rT mxl ins cert ==> \<exists> phi. wt_method G C pTs rT mxl ins phi" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
261 |
proof (unfold wtl_method_def, simp only: Let_def, elim conjE) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
262 |
let "?s0" = "Some ([], Ok (Class C) # map Ok pTs @ replicate mxl Err)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
263 |
assume pc: "0 < length ins" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
264 |
assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
265 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
266 |
obtain phi where fits: "fits phi ins G rT ?s0 cert" |
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
267 |
by (rule exists_phi [elim_format]) blast |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
268 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
269 |
with wtl |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
270 |
have allpc: |
9580 | 271 |
"\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
272 |
by (blast intro: wtl_fits_wt) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
273 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
274 |
from pc wtl fits |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
275 |
have "wt_start G C pTs mxl phi" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
276 |
by (unfold wt_start_def) (rule fits_first) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
277 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
278 |
with pc allpc |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
279 |
show ?thesis by (auto simp add: wt_method_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
280 |
qed |
9012 | 281 |
|
282 |
lemma unique_set: |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
283 |
"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
284 |
a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'" |
9580 | 285 |
by (induct "l") auto |
9012 | 286 |
|
287 |
lemma unique_epsilon: |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
288 |
"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
289 |
(\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)" |
9580 | 290 |
by (auto simp add: unique_set) |
9012 | 291 |
|
292 |
theorem wtl_correct: |
|
9580 | 293 |
"wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi" |
294 |
proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI) |
|
9012 | 295 |
|
9580 | 296 |
assume wtl_prog: "wtl_jvm_prog G cert" |
297 |
thus "ObjectC \<in> set G" by (simp add: wtl_jvm_prog_def wf_prog_def) |
|
9012 | 298 |
|
9580 | 299 |
from wtl_prog |
300 |
show uniqueG: "unique G" by (simp add: wtl_jvm_prog_def wf_prog_def) |
|
9012 | 301 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
302 |
show "\<exists>Phi. Ball (set G) (wf_cdecl (\<lambda>G C (sig,rT,maxl,b). |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
303 |
wt_method G C (snd sig) rT maxl b (Phi C sig)) G)" |
9580 | 304 |
(is "\<exists>Phi. ?Q Phi") |
305 |
proof (intro exI) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
306 |
let "?Phi" = "\<lambda> C sig. |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
307 |
let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
308 |
(sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
309 |
in \<epsilon> phi. wt_method G C (snd sig) rT maxl b phi" |
9580 | 310 |
from wtl_prog |
311 |
show "?Q ?Phi" |
|
312 |
proof (unfold wf_cdecl_def, intro) |
|
313 |
fix x a b aa ba ab bb m |
|
314 |
assume 1: "x \<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \<in> set bb" |
|
315 |
with wtl_prog |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
316 |
show "wf_mdecl (\<lambda>G C (sig,rT,maxl,b). |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
317 |
wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
318 |
proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def, |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
319 |
elim conjE) |
9580 | 320 |
apply_end (drule bspec, assumption, simp, elim conjE) |
321 |
assume "\<forall>(sig,rT,mb)\<in>set bb. wf_mhead G sig rT \<and> |
|
322 |
(\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb" |
|
323 |
"unique bb" |
|
324 |
with 1 uniqueG |
|
325 |
show "(\<lambda>(sig,rT,mb). |
|
326 |
wf_mhead G sig rT \<and> |
|
327 |
(\<lambda>(maxl,b). |
|
9012 | 328 |
wt_method G a (snd sig) rT maxl b |
9580 | 329 |
((\<lambda>(C,x,y,mdecls). |
330 |
(\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b)) |
|
331 |
(\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig)) |
|
332 |
(\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m" |
|
9012 | 333 |
by - (drule bspec, assumption, |
9580 | 334 |
clarsimp dest!: wtl_method_correct, |
9970 | 335 |
clarsimp intro!: someI simp add: unique_epsilon) |
9580 | 336 |
qed |
337 |
qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def) |
|
338 |
qed |
|
339 |
qed |
|
9012 | 340 |
|
341 |
||
9580 | 342 |
end |