author | kleing |
Wed, 09 Aug 2000 11:53:00 +0200 | |
changeset 9559 | 1f99296758c2 |
parent 9549 | 40d64cb4f4e6 |
child 9580 | d955914193e0 |
permissions | -rw-r--r-- |
8388 | 1 |
(* Title: HOL/MicroJava/BV/LBVComplete.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gerwin Klein |
|
4 |
Copyright 2000 Technische Universitaet Muenchen |
|
9054 | 5 |
*) |
8388 | 6 |
|
9054 | 7 |
header {* Completeness of the LBV *} |
8388 | 8 |
|
9559 | 9 |
theory LBVComplete = BVSpec + LBVSpec + StepMono: |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
10 |
|
8388 | 11 |
|
12 |
constdefs |
|
13 |
is_approx :: "['a option list, 'a list] \\<Rightarrow> bool" |
|
14 |
"is_approx a b \\<equiv> length a = length b \\<and> (\\<forall> n. n < length a \\<longrightarrow> |
|
15 |
(a!n = None \\<or> a!n = Some (b!n)))" |
|
16 |
||
17 |
contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool" |
|
18 |
"contains_dead ins cert phi pc \\<equiv> |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
19 |
Suc pc \\<notin> succs (ins!pc) pc \\<and> Suc pc < length phi \\<longrightarrow> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
20 |
cert ! (Suc pc) = Some (phi ! Suc pc)" |
8388 | 21 |
|
22 |
contains_targets :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool" |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
23 |
"contains_targets ins cert phi pc \\<equiv> ( |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
24 |
\\<forall> pc' \\<in> succs (ins!pc) pc. pc' \\<noteq> Suc pc \\<and> pc' < length phi \\<longrightarrow> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
25 |
cert!pc' = Some (phi!pc'))" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
26 |
|
8388 | 27 |
|
9012 | 28 |
fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool" |
29 |
"fits ins cert phi \\<equiv> is_approx cert phi \\<and> length ins < length phi \\<and> |
|
30 |
(\\<forall> pc. pc < length ins \\<longrightarrow> |
|
31 |
contains_dead ins cert phi pc \\<and> |
|
32 |
contains_targets ins cert phi pc)" |
|
33 |
||
8388 | 34 |
is_target :: "[instr list, p_count] \\<Rightarrow> bool" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
35 |
"is_target ins pc \\<equiv> \\<exists> pc'. pc' < length ins \\<and> pc \\<in> succs (ins!pc') pc'" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
36 |
|
8388 | 37 |
maybe_dead :: "[instr list, p_count] \\<Rightarrow> bool" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
38 |
"maybe_dead ins pc \\<equiv> \\<exists> pc'. pc = pc'+1 \\<and> pc \\<notin> succs (ins!pc') pc'" |
8388 | 39 |
|
40 |
mdot :: "[instr list, p_count] \\<Rightarrow> bool" |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
41 |
"mdot ins pc \\<equiv> maybe_dead ins pc \\<or> is_target ins pc" |
8388 | 42 |
|
43 |
||
44 |
consts |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
45 |
option_filter_n :: "['a list, nat \\<Rightarrow> bool, nat] \\<Rightarrow> 'a option list" |
8388 | 46 |
primrec |
47 |
"option_filter_n [] P n = []" |
|
48 |
"option_filter_n (h#t) P n = (if (P n) then Some h # option_filter_n t P (n+1) |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
49 |
else None # option_filter_n t P (n+1))" |
8388 | 50 |
|
51 |
constdefs |
|
52 |
option_filter :: "['a list, nat \\<Rightarrow> bool] \\<Rightarrow> 'a option list" |
|
53 |
"option_filter l P \\<equiv> option_filter_n l P 0" |
|
54 |
||
55 |
make_cert :: "[instr list, method_type] \\<Rightarrow> certificate" |
|
56 |
"make_cert ins phi \\<equiv> option_filter phi (mdot ins)" |
|
57 |
||
58 |
make_Cert :: "[jvm_prog, prog_type] \\<Rightarrow> prog_certificate" |
|
59 |
"make_Cert G Phi \\<equiv> \\<lambda> C sig. |
|
60 |
let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in |
|
61 |
let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
62 |
make_cert b (Phi C sig)" |
8388 | 63 |
|
9012 | 64 |
|
9559 | 65 |
lemmas [simp del] = split_paired_Ex |
66 |
||
67 |
lemma length_ofn [rulify]: "\\<forall>n. length (option_filter_n l P n) = length l" |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
68 |
by (induct l) auto |
9012 | 69 |
|
70 |
||
9559 | 71 |
lemma is_approx_option_filter: "is_approx (option_filter l P) l" |
72 |
proof - |
|
73 |
{ |
|
74 |
fix a n |
|
75 |
have "\\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a") |
|
76 |
proof (induct a) |
|
77 |
show "?P []" by (auto simp add: is_approx_def) |
|
78 |
||
79 |
fix l ls |
|
80 |
assume Cons: "?P ls" |
|
9012 | 81 |
|
9559 | 82 |
show "?P (l#ls)" |
83 |
proof (unfold is_approx_def, intro allI conjI impI) |
|
84 |
fix n |
|
85 |
show "length (option_filter_n (l # ls) P n) = length (l # ls)" |
|
86 |
by (simp only: length_ofn) |
|
87 |
||
88 |
fix m |
|
89 |
assume "m < length (option_filter_n (l # ls) P n)" |
|
90 |
hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp |
|
91 |
||
92 |
show "option_filter_n (l # ls) P n ! m = None \\<or> |
|
93 |
option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)" |
|
94 |
proof (cases "m") |
|
95 |
assume "m = 0" |
|
96 |
with m show ?thesis by simp |
|
97 |
next |
|
98 |
fix m' assume Suc: "m = Suc m'" |
|
99 |
from Cons |
|
100 |
show ?thesis |
|
101 |
proof (unfold is_approx_def, elim allE impE conjE) |
|
102 |
from m Suc |
|
103 |
show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn) |
|
104 |
||
105 |
assume "option_filter_n ls P (Suc n) ! m' = None \\<or> |
|
106 |
option_filter_n ls P (Suc n) ! m' = Some (ls ! m')" |
|
107 |
with m Suc |
|
108 |
show ?thesis by auto |
|
109 |
qed |
|
110 |
qed |
|
9376 | 111 |
qed |
112 |
qed |
|
9559 | 113 |
} |
114 |
||
115 |
thus ?thesis |
|
116 |
by (auto simp add: option_filter_def) |
|
9376 | 117 |
qed |
9012 | 118 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
119 |
lemma option_filter_Some: |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
120 |
"\\<lbrakk>n < length l; P n\\<rbrakk> \\<Longrightarrow> option_filter l P ! n = Some (l!n)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
121 |
proof - |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
122 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
123 |
assume 1: "n < length l" "P n" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
124 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
125 |
have "\\<forall>n n'. n < length l \\<longrightarrow> P (n+n') \\<longrightarrow> option_filter_n l P n' ! n = Some (l!n)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
126 |
(is "?P l") |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
127 |
proof (induct l) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
128 |
show "?P []" by simp |
9012 | 129 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
130 |
fix l ls assume Cons: "?P ls" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
131 |
show "?P (l#ls)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
132 |
proof (intro) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
133 |
fix n n' |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
134 |
assume l: "n < length (l # ls)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
135 |
assume P: "P (n + n')" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
136 |
show "option_filter_n (l # ls) P n' ! n = Some ((l # ls) ! n)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
137 |
proof (cases "n") |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
138 |
assume "n=0" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
139 |
with P show ?thesis by simp |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
140 |
next |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
141 |
fix m assume "n = Suc m" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
142 |
with l P Cons |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
143 |
show ?thesis by simp |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
144 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
145 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
146 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
147 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
148 |
with 1 |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
149 |
show ?thesis by (auto simp add: option_filter_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
150 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
151 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
152 |
lemma option_filter_contains_dead: |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
153 |
"contains_dead ins (option_filter phi (mdot ins)) phi pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
154 |
by (auto intro: option_filter_Some simp add: contains_dead_def mdot_def maybe_dead_def) |
9012 | 155 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
156 |
lemma option_filter_contains_targets: |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
157 |
"pc < length ins \\<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
158 |
proof (unfold contains_targets_def, clarsimp) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
159 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
160 |
fix pc' |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
161 |
assume "pc < length ins" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
162 |
"pc' \\<in> succs (ins ! pc) pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
163 |
"pc' \\<noteq> Suc pc" and |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
164 |
pc': "pc' < length phi" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
165 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
166 |
hence "is_target ins pc'" by (auto simp add: is_target_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
167 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
168 |
with pc' |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
169 |
show "option_filter phi (mdot ins) ! pc' = Some (phi ! pc')" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
170 |
by (auto intro: option_filter_Some simp add: mdot_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
171 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
172 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
173 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
174 |
lemma fits_make_cert: |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
175 |
"length ins < length phi \\<Longrightarrow> fits ins (make_cert ins phi) phi" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
176 |
proof - |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
177 |
assume l: "length ins < length phi" |
9012 | 178 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
179 |
thus "fits ins (make_cert ins phi) phi" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
180 |
proof (unfold fits_def make_cert_def, intro conjI allI impI) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
181 |
show "is_approx (option_filter phi (mdot ins)) phi" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
182 |
by (rule is_approx_option_filter) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
183 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
184 |
show "length ins < length phi" . |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
185 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
186 |
fix pc |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
187 |
show "contains_dead ins (option_filter phi (mdot ins)) phi pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
188 |
by (rule option_filter_contains_dead) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
189 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
190 |
assume "pc < length ins" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
191 |
thus "contains_targets ins (option_filter phi (mdot ins)) phi pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
192 |
by (rule option_filter_contains_targets) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
193 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
194 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
195 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
196 |
lemma fitsD: |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
197 |
"\\<lbrakk>fits ins cert phi; pc' \\<in> succs (ins!pc) pc; pc' \\<noteq> Suc pc; pc < length ins; pc' < length ins\\<rbrakk> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
198 |
\\<Longrightarrow> cert!pc' = Some (phi!pc')" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
199 |
by (clarsimp simp add: fits_def contains_dead_def contains_targets_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
200 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
201 |
lemma fitsD2: |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
202 |
"\\<lbrakk>fits ins cert phi; Suc pc \\<notin> succs (ins!pc) pc; pc < length ins\\<rbrakk> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
203 |
\\<Longrightarrow> cert ! Suc pc = Some (phi ! Suc pc)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
204 |
by (clarsimp simp add: fits_def contains_dead_def contains_targets_def) |
9012 | 205 |
|
206 |
||
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
207 |
lemma wtl_inst_mono: |
9559 | 208 |
"\\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; |
9012 | 209 |
G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
210 |
\\<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"; |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
211 |
proof - |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
212 |
assume pc: "pc < length ins" "i = ins!pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
213 |
assume wtl: "wtl_inst i G rT s1 s1' cert mpc pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
214 |
assume fits: "fits ins cert phi" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
215 |
assume G: "G \\<turnstile> s2 <=s s1" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
216 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
217 |
let "?step s" = "step (i, G, s)" |
9012 | 218 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
219 |
from wtl G |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
220 |
have app: "app (i, G, rT, s2)" by (auto simp add: wtl_inst_def app_mono) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
221 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
222 |
from wtl G |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
223 |
have step: "succs i pc \\<noteq> {} \\<Longrightarrow> G \\<turnstile> the (?step s2) <=s the (?step s1)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
224 |
by - (drule step_mono, auto simp add: wtl_inst_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
225 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
226 |
with app |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
227 |
have some: "succs i pc \\<noteq> {} \\<Longrightarrow> ?step s2 \\<noteq> None" by (simp add: app_step_some) |
9012 | 228 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
229 |
{ |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
230 |
fix pc' |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
231 |
assume 0: "pc' \\<in> succs i pc" "pc' \\<noteq> pc+1" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
232 |
hence "succs i pc \\<noteq> {}" by auto |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
233 |
hence "G \\<turnstile> the (?step s2) <=s the (?step s1)" by (rule step) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
234 |
also |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
235 |
from wtl 0 |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
236 |
have "G \\<turnstile> the (?step s1) <=s the (cert!pc')" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
237 |
by (auto simp add: wtl_inst_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
238 |
finally |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
239 |
have "G\\<turnstile> the (?step s2) <=s the (cert!pc')" . |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
240 |
} note cert = this |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
241 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
242 |
have "\\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \\<and> G \\<turnstile> s2' <=s s1'" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
243 |
proof (cases "pc+1 \\<in> succs i pc") |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
244 |
case True |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
245 |
with wtl |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
246 |
have s1': "s1' = the (?step s1)" by (simp add: wtl_inst_def) |
9012 | 247 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
248 |
have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \\<and> G \\<turnstile> (the (?step s2)) <=s s1'" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
249 |
(is "?wtl \\<and> ?G") |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
250 |
proof |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
251 |
from True s1' |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
252 |
show ?G by (auto intro: step) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
253 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
254 |
from True app wtl |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
255 |
show ?wtl |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
256 |
by (clarsimp intro: cert simp add: wtl_inst_def) |
9376 | 257 |
qed |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
258 |
thus ?thesis by blast |
9376 | 259 |
next |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
260 |
case False |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
261 |
with wtl |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
262 |
have "s1' = the (cert ! Suc pc)" by (simp add: wtl_inst_def) |
9012 | 263 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
264 |
with False app wtl |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
265 |
have "wtl_inst i G rT s2 s1' cert mpc pc \\<and> G \\<turnstile> s1' <=s s1'" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
266 |
by (clarsimp intro: cert simp add: wtl_inst_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
267 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
268 |
thus ?thesis by blast |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
269 |
qed |
9012 | 270 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
271 |
with pc show ?thesis by simp |
9376 | 272 |
qed |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
273 |
|
9559 | 274 |
|
275 |
lemma wtl_option_mono: |
|
276 |
"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; |
|
277 |
pc < length ins; G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> |
|
278 |
\\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')" |
|
279 |
proof - |
|
280 |
assume wtl: "wtl_inst_option i G rT s1 s1' cert mpc pc" and |
|
281 |
fits: "fits ins cert phi" "pc < length ins" |
|
282 |
"G \\<turnstile> s2 <=s s1" "i = ins!pc" |
|
283 |
||
284 |
show ?thesis |
|
285 |
proof (cases "cert!pc") |
|
286 |
case None |
|
287 |
with wtl fits; |
|
288 |
show ?thesis; |
|
289 |
by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+); |
|
290 |
next |
|
291 |
case Some |
|
292 |
with wtl fits; |
|
293 |
||
294 |
have G: "G \\<turnstile> s2 <=s a" |
|
295 |
by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+) |
|
296 |
||
297 |
from Some wtl |
|
298 |
have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def) |
|
299 |
||
300 |
with G fits |
|
301 |
have "\\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')" |
|
302 |
by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+); |
|
303 |
||
304 |
with Some G; |
|
305 |
show ?thesis; by (simp add: wtl_inst_option_def); |
|
306 |
qed |
|
307 |
qed |
|
308 |
||
309 |
||
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
310 |
|
9012 | 311 |
lemma wt_instr_imp_wtl_inst: |
312 |
"\\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi; |
|
313 |
pc < length ins; length ins = max_pc\\<rbrakk> \\<Longrightarrow> |
|
314 |
\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc"; |
|
9376 | 315 |
proof - |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
316 |
assume wt: "wt_instr (ins!pc) G rT phi max_pc pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
317 |
assume fits: "fits ins cert phi" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
318 |
assume pc: "pc < length ins" "length ins = max_pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
319 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
320 |
from wt |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
321 |
have app: "app (ins!pc, G, rT, phi!pc)" by (simp add: wt_instr_def); |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
322 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
323 |
from wt pc |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
324 |
have pc': "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> pc' < length ins" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
325 |
by (simp add: wt_instr_def) |
9376 | 326 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
327 |
let ?s' = "the (step (ins!pc,G, phi!pc))" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
328 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
329 |
from wt |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
330 |
have G: "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> G \\<turnstile> ?s' <=s phi ! pc'" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
331 |
by (simp add: wt_instr_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
332 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
333 |
from wt fits pc |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
334 |
have cert: "!!pc'. \\<lbrakk>pc' \\<in> succs (ins!pc) pc; pc' < max_pc; pc' \\<noteq> pc+1\\<rbrakk> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
335 |
\\<Longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> ?s' <=s the (cert!pc')" |
9559 | 336 |
by (auto dest: fitsD simp add: wt_instr_def) |
9012 | 337 |
|
9376 | 338 |
show ?thesis |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
339 |
proof (cases "pc+1 \\<in> succs (ins!pc) pc") |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
340 |
case True |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
341 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
342 |
have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \\<and> G \\<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \\<and> ?G") |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
343 |
proof |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
344 |
from True |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
345 |
show "G \\<turnstile> ?s' <=s phi ! Suc pc" by (simp add: G) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
346 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
347 |
from True fits app pc cert pc' |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
348 |
show "?wtl" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
349 |
by (auto simp add: wtl_inst_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
350 |
qed |
9012 | 351 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
352 |
thus ?thesis by blast |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
353 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
354 |
next |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
355 |
let ?s'' = "the (cert ! Suc pc)" |
9012 | 356 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
357 |
case False |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
358 |
with fits app pc cert pc' |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
359 |
have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \\<and> G \\<turnstile> ?s'' <=s phi ! Suc pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
360 |
by (auto dest: fitsD2 simp add: wtl_inst_def) |
9012 | 361 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
362 |
thus ?thesis by blast |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
363 |
qed |
9376 | 364 |
qed |
9012 | 365 |
|
366 |
||
367 |
lemma wt_instr_imp_wtl_option: |
|
368 |
"\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; max_pc = length ins\\<rbrakk> \\<Longrightarrow> |
|
369 |
\\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc"; |
|
9376 | 370 |
proof - |
9012 | 371 |
assume fits : "fits ins cert phi" "pc < length ins" |
372 |
and "wt_instr (ins!pc) G rT phi max_pc pc" |
|
373 |
"max_pc = length ins"; |
|
374 |
||
375 |
hence * : "\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc"; |
|
376 |
by - (rule wt_instr_imp_wtl_inst, simp+); |
|
377 |
||
378 |
show ?thesis; |
|
379 |
proof (cases "cert ! pc"); |
|
380 |
case None; |
|
381 |
with *; |
|
382 |
show ?thesis; by (simp add: wtl_inst_option_def); |
|
383 |
||
384 |
next; |
|
385 |
case Some; |
|
386 |
||
387 |
from fits; |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
388 |
have "pc < length phi"; by (clarsimp simp add: fits_def); |
9012 | 389 |
with fits Some; |
390 |
have "cert ! pc = Some (phi!pc)"; by (auto simp add: fits_def is_approx_def); |
|
391 |
||
392 |
with *; |
|
393 |
show ?thesis; by (simp add: wtl_inst_option_def); |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
394 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
395 |
qed |
9012 | 396 |
|
9376 | 397 |
|
9559 | 398 |
text {* |
399 |
\medskip |
|
400 |
Main induction over the instruction list. |
|
401 |
*} |
|
9012 | 402 |
|
403 |
theorem wt_imp_wtl_inst_list: |
|
9559 | 404 |
"\\<forall> pc. (\\<forall>pc'. pc' < length all_ins \\<longrightarrow> wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \\<longrightarrow> |
405 |
fits all_ins cert phi \\<longrightarrow> |
|
406 |
(\\<exists>l. pc = length l \\<and> all_ins = l@ins) \\<longrightarrow> |
|
407 |
pc < length all_ins \\<longrightarrow> |
|
9012 | 408 |
(\\<forall> s. (G \\<turnstile> s <=s (phi!pc)) \\<longrightarrow> |
9559 | 409 |
(\\<exists>s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))" |
410 |
(is "\\<forall>pc. ?wt \\<longrightarrow> ?fits \\<longrightarrow> ?l pc ins \\<longrightarrow> ?len pc \\<longrightarrow> ?wtl pc ins" is "\\<forall>pc. ?C pc ins" is "?P ins") |
|
411 |
proof (induct "?P" "ins") |
|
412 |
case Nil |
|
413 |
show "?P []" by simp |
|
414 |
next |
|
415 |
fix i ins' |
|
416 |
assume Cons: "?P ins'" |
|
9012 | 417 |
|
9559 | 418 |
show "?P (i#ins')" |
419 |
proof (intro allI impI, elim exE conjE) |
|
420 |
fix pc s l |
|
421 |
assume wt : "\\<forall>pc'. pc' < length all_ins \\<longrightarrow> |
|
422 |
wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'" |
|
423 |
assume fits: "fits all_ins cert phi" |
|
424 |
assume G : "G \\<turnstile> s <=s phi ! pc" |
|
425 |
assume l : "pc < length all_ins" |
|
9012 | 426 |
|
9559 | 427 |
assume pc : "all_ins = l@i#ins'" "pc = length l" |
428 |
hence i : "all_ins ! pc = i" |
|
429 |
by (simp add: nth_append) |
|
9012 | 430 |
|
9559 | 431 |
from l wt |
432 |
have "wt_instr (all_ins!pc) G rT phi (length all_ins) pc" by blast |
|
9012 | 433 |
|
9559 | 434 |
with fits l |
435 |
obtain s1 where |
|
436 |
"wtl_inst_option (all_ins!pc) G rT (phi!pc) s1 cert (length all_ins) pc" and |
|
437 |
s1: "G \\<turnstile> s1 <=s phi ! (Suc pc)" |
|
438 |
by - (drule wt_instr_imp_wtl_option, assumption+, simp, elim exE conjE, simp) |
|
439 |
||
440 |
with fits l |
|
441 |
obtain s2 where |
|
442 |
o: "wtl_inst_option (all_ins!pc) G rT s s2 cert (length all_ins) pc" |
|
443 |
and "G \\<turnstile> s2 <=s s1" |
|
444 |
by - (drule wtl_option_mono, assumption+, simp, elim exE conjE, rule that) |
|
9012 | 445 |
|
9559 | 446 |
with s1 |
447 |
have G': "G \\<turnstile> s2 <=s phi ! (Suc pc)" |
|
448 |
by - (rule sup_state_trans, auto) |
|
9012 | 449 |
|
9559 | 450 |
from Cons |
451 |
have "?C (Suc pc) ins'" by blast |
|
452 |
with wt fits pc |
|
453 |
have IH: "?len (Suc pc) \\<longrightarrow> ?wtl (Suc pc) ins'" by auto |
|
9012 | 454 |
|
9559 | 455 |
show "\\<exists>s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc" |
456 |
proof (cases "?len (Suc pc)") |
|
457 |
case False |
|
458 |
with pc |
|
459 |
have "ins' = []" by simp |
|
460 |
with i o |
|
461 |
show ?thesis by auto |
|
462 |
next |
|
463 |
case True |
|
464 |
with IH |
|
465 |
have "?wtl (Suc pc) ins'" by blast |
|
466 |
with G' |
|
467 |
obtain s' where |
|
468 |
"wtl_inst_list ins' G rT s2 s' cert (length all_ins) (Suc pc)" |
|
469 |
by - (elim allE impE, auto) |
|
470 |
with i o |
|
471 |
show ?thesis by auto |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
472 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
473 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
474 |
qed |
9559 | 475 |
|
9012 | 476 |
|
477 |
lemma fits_imp_wtl_method_complete: |
|
9559 | 478 |
"\\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins cert" |
9012 | 479 |
by (simp add: wt_method_def wtl_method_def del: split_paired_Ex) |
480 |
(rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex); |
|
481 |
||
482 |
||
483 |
lemma wtl_method_complete: |
|
484 |
"\\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)"; |
|
485 |
proof -; |
|
486 |
assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G"; |
|
487 |
||
488 |
hence "fits ins (make_cert ins phi) phi"; |
|
489 |
by - (rule fits_make_cert, simp add: wt_method_def); |
|
490 |
||
491 |
with *; |
|
492 |
show ?thesis; by - (rule fits_imp_wtl_method_complete); |
|
493 |
qed; |
|
494 |
||
495 |
lemma unique_set: |
|
496 |
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'"; |
|
497 |
by (induct "l") auto; |
|
498 |
||
499 |
lemma unique_epsilon: |
|
500 |
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)"; |
|
501 |
by (auto simp add: unique_set); |
|
502 |
||
503 |
||
504 |
theorem wtl_complete: "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)"; |
|
505 |
proof (simp only: wt_jvm_prog_def); |
|
506 |
||
507 |
assume wfprog: "wf_prog (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G"; |
|
508 |
||
509 |
thus ?thesis; |
|
510 |
proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto); |
|
511 |
fix a aa ab b ac ba ad ae bb; |
|
512 |
assume 1 : "\\<forall>(C,sc,fs,ms)\\<in>set G. |
|
513 |
Ball (set fs) (wf_fdecl G) \\<and> |
|
514 |
unique fs \\<and> |
|
515 |
(\\<forall>(sig,rT,mb)\\<in>set ms. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \\<and> |
|
516 |
unique ms \\<and> |
|
517 |
(case sc of None \\<Rightarrow> C = Object |
|
518 |
| Some D \\<Rightarrow> |
|
519 |
is_class G D \\<and> |
|
520 |
(D, C) \\<notin> (subcls1 G)^* \\<and> |
|
521 |
(\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))" |
|
522 |
"(a, aa, ab, b) \\<in> set G"; |
|
523 |
||
524 |
assume uG : "unique G"; |
|
525 |
assume b : "((ac, ba), ad, ae, bb) \\<in> set b"; |
|
526 |
||
527 |
from 1; |
|
528 |
show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"; |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
529 |
proof (rule bspec [elimify], clarsimp); |
9012 | 530 |
assume ub : "unique b"; |
531 |
assume m: "\\<forall>(sig,rT,mb)\\<in>set b. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb"; |
|
532 |
from m b; |
|
533 |
show ?thesis; |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
534 |
proof (rule bspec [elimify], clarsimp); |
9012 | 535 |
assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"; |
536 |
with wfprog uG ub b 1; |
|
537 |
show ?thesis; |
|
538 |
by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon); |
|
539 |
qed; |
|
540 |
qed; |
|
541 |
qed; |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
542 |
qed |
9012 | 543 |
|
9559 | 544 |
lemmas [simp] = split_paired_Ex |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
545 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
546 |
end |