author | kleing |
Wed, 30 Aug 2000 21:47:39 +0200 | |
changeset 9757 | 1024a2d80ac0 |
parent 9664 | 4cae97480a6d |
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/LBVSpec.thy |
8245 | 2 |
ID: $Id$ |
3 |
Author: Gerwin Klein |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
9054 | 5 |
*) |
8245 | 6 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
7 |
header {* The Lightweight Bytecode Verifier *} |
9054 | 8 |
|
8245 | 9 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
10 |
theory LBVSpec = Step : |
8245 | 11 |
|
12 |
types |
|
13 |
certificate = "state_type option list" |
|
9664 | 14 |
class_certificate = "sig \<Rightarrow> certificate" |
15 |
prog_certificate = "cname \<Rightarrow> class_certificate" |
|
8245 | 16 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
17 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
18 |
constdefs |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
19 |
check_cert :: "[instr, jvm_prog, state_type option, certificate, p_count, p_count] |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
20 |
\<Rightarrow> bool" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
21 |
"check_cert i G s cert pc max_pc \<equiv> \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
22 |
(pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')" |
9376 | 23 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
24 |
wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
25 |
\<Rightarrow> state_type option err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
26 |
"wtl_inst i G rT s cert max_pc pc \<equiv> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
27 |
if app i G rT s \<and> check_cert i G s cert pc max_pc then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
28 |
if pc+1 mem (succs i pc) then Ok (step i G s) else Ok (cert!(pc+1)) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
29 |
else Err"; |
8245 | 30 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
31 |
lemma wtl_inst_Ok: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
32 |
"(wtl_inst i G rT s cert max_pc pc = Ok s') = |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
33 |
(app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc). |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
34 |
pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')) \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
35 |
(if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
36 |
by (auto simp add: wtl_inst_def check_cert_def set_mem_eq); |
8245 | 37 |
|
38 |
||
39 |
constdefs |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
40 |
wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
41 |
\<Rightarrow> state_type option err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
42 |
"wtl_cert i G rT s cert max_pc pc \<equiv> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
43 |
case cert!pc of |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
44 |
None \<Rightarrow> wtl_inst i G rT s cert max_pc pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
45 |
| Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
46 |
wtl_inst i G rT (Some s') cert max_pc pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
47 |
else Err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
48 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
49 |
consts |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
50 |
wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count, |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
51 |
state_type option] \<Rightarrow> state_type option err" |
8245 | 52 |
primrec |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
53 |
"wtl_inst_list [] G rT cert max_pc pc s = Ok s" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
54 |
"wtl_inst_list (i#is) G rT cert max_pc pc s = |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
55 |
(let s' = wtl_cert i G rT s cert max_pc pc in |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
56 |
strict (wtl_inst_list is G rT cert max_pc (pc+1)) s')"; |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
57 |
|
8245 | 58 |
|
59 |
constdefs |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
60 |
wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \<Rightarrow> bool" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
61 |
"wtl_method G C pTs rT mxl ins cert \<equiv> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
62 |
let max_pc = length ins |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
63 |
in |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
64 |
0 < max_pc \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
65 |
wtl_inst_list ins G rT cert max_pc 0 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
66 |
(Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err))) \<noteq> Err" |
8245 | 67 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
68 |
wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
69 |
"wtl_jvm_prog G cert \<equiv> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
70 |
wf_prog (\<lambda>G C (sig,rT,maxl,b). wtl_method G C (snd sig) rT maxl b (cert C sig)) G" |
9012 | 71 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
72 |
text {* \medskip *} |
9012 | 73 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
74 |
lemma strict_Some [simp]: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
75 |
"(strict f x = Ok y) = (\<exists> z. x = Ok z \<and> f z = Ok y)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
76 |
by (cases x, auto) |
8245 | 77 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
78 |
lemma wtl_Cons: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
79 |
"wtl_inst_list (i#is) G rT cert max_pc pc s \<noteq> Err = |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
80 |
(\<exists>s'. wtl_cert i G rT s cert max_pc pc = Ok s' \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
81 |
wtl_inst_list is G rT cert max_pc (pc+1) s' \<noteq> Err)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
82 |
by (auto simp del: split_paired_Ex) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
83 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
84 |
lemma wtl_append: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
85 |
"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = Ok s') = |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
86 |
(\<exists>s''. wtl_inst_list a G rT cert mpc pc s = Ok s'' \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
87 |
wtl_inst_list b G rT cert mpc (pc+length a) s'' = Ok s')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
88 |
(is "\<forall> s pc. ?C s pc a" is "?P a") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
89 |
proof (induct ?P a) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
90 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
91 |
show "?P []" by simp |
9012 | 92 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
93 |
fix x xs |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
94 |
assume IH: "?P xs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
95 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
96 |
show "?P (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
97 |
proof (intro allI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
98 |
fix s pc |
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 |
show "?C s pc (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
101 |
proof (cases "wtl_cert x G rT s cert mpc pc") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
102 |
case Err thus ?thesis by simp |
9183 | 103 |
next |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
104 |
fix s0 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
105 |
assume Ok: "wtl_cert x G rT s cert mpc pc = Ok s0" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
106 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
107 |
with IH |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
108 |
have "?C s0 (Suc pc) xs" by blast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
109 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
110 |
with Ok |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
111 |
show ?thesis by simp |
9183 | 112 |
qed |
113 |
qed |
|
114 |
qed |
|
9012 | 115 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
116 |
lemma wtl_take: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
117 |
"wtl_inst_list is G rT cert mpc pc s = Ok s'' ==> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
118 |
\<exists>s'. wtl_inst_list (take pc' is) G rT cert mpc pc s = Ok s'" |
9183 | 119 |
proof - |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
120 |
assume "wtl_inst_list is G rT cert mpc pc s = Ok s''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
121 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
122 |
hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mpc pc s = Ok s''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
123 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
124 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
125 |
thus ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
126 |
by (auto simp add: wtl_append simp del: append_take_drop_id) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
127 |
qed |
9012 | 128 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
129 |
lemma take_Suc: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
130 |
"\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l") |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
131 |
proof (induct l) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
132 |
show "?P []" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
133 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
134 |
fix x xs |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
135 |
assume IH: "?P xs" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
136 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
137 |
show "?P (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
138 |
proof (intro strip) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
139 |
fix n |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
140 |
assume "n < length (x#xs)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
141 |
with IH |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
142 |
show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
143 |
by - (cases n, auto) |
9183 | 144 |
qed |
145 |
qed |
|
9012 | 146 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
147 |
lemma wtl_Suc: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
148 |
"[| 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
|
149 |
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
|
150 |
Suc pc < length is |] ==> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
151 |
wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''" |
9183 | 152 |
proof - |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
153 |
assume wtt: "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
|
154 |
assume wtc: "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
|
155 |
assume pc: "Suc pc < length is" |
9012 | 156 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
157 |
hence "take (Suc pc) is = (take pc is)@[is!pc]" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
158 |
by (simp add: take_Suc) |
9012 | 159 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
160 |
with wtt wtc pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
161 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
162 |
by (simp add: wtl_append min_def) |
9183 | 163 |
qed |
9012 | 164 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
165 |
lemma wtl_all: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
166 |
"[| 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
|
167 |
pc < length is |] ==> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
168 |
\<exists>s' s''. 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
|
169 |
wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" |
9183 | 170 |
proof - |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
171 |
assume all: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err" |
9012 | 172 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
173 |
assume pc: "pc < length is" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
174 |
hence "0 < length (drop pc is)" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
175 |
then |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
176 |
obtain i r where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
177 |
Cons: "drop pc is = i#r" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
178 |
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
|
179 |
hence "i#r = drop pc is" .. |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
180 |
with all |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
181 |
have take: "wtl_inst_list (take pc is@i#r) G rT cert (length is) 0 s \<noteq> Err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
182 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
183 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
184 |
from pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
185 |
have "is!pc = drop pc is ! 0" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
186 |
with Cons |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
187 |
have "is!pc = i" by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
188 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
189 |
with take pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
190 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
191 |
by (auto simp add: wtl_append min_def) |
9183 | 192 |
qed |
9012 | 193 |
|
9183 | 194 |
end |