11229
|
1 |
(* Title: HOL/MicroJava/BV/Typing_Framework_err.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gerwin Klein
|
|
4 |
Copyright 2000 TUM
|
|
5 |
|
|
6 |
*)
|
|
7 |
|
|
8 |
header "Static and Dynamic Welltyping"
|
|
9 |
|
|
10 |
theory Typing_Framework_err = Typing_Framework:
|
|
11 |
|
|
12 |
constdefs
|
|
13 |
|
|
14 |
dynamic_wt :: "'s ord => (nat => 's err => 's err) => (nat => nat list) =>
|
|
15 |
's err list => bool"
|
11299
|
16 |
"dynamic_wt r step succs ts == wt_step (Err.le r) Err step succs ts"
|
11229
|
17 |
|
|
18 |
static_wt :: "'s ord => (nat => 's => bool) =>
|
|
19 |
(nat => 's => 's) => (nat => nat list) => 's list => bool"
|
|
20 |
"static_wt r app step succs ts ==
|
|
21 |
!p < size ts. app p (ts!p) & (!q:set(succs p). step p (ts!p) <=_r ts!q)"
|
|
22 |
|
|
23 |
err_step :: "(nat => 's => bool) => (nat => 's => 's) =>
|
|
24 |
(nat => 's err => 's err)"
|
|
25 |
"err_step app step p == lift (%t. if app p t then OK (step p t) else Err)"
|
|
26 |
|
|
27 |
non_empty :: "(nat => nat list) => bool"
|
|
28 |
"non_empty succs == !p. succs p ~= []"
|
|
29 |
|
|
30 |
|
|
31 |
lemma non_emptyD:
|
|
32 |
"non_empty succs ==> ? q. q:set(succs p)"
|
|
33 |
proof (unfold non_empty_def)
|
|
34 |
assume "!p. succs p ~= []"
|
|
35 |
hence "succs p ~= []" ..
|
|
36 |
then obtain x xs where "succs p = x#xs"
|
|
37 |
by (auto simp add: neq_Nil_conv)
|
|
38 |
thus ?thesis
|
|
39 |
by auto
|
|
40 |
qed
|
|
41 |
|
|
42 |
lemma dynamic_imp_static:
|
|
43 |
"[| bounded succs (size ts); non_empty succs;
|
|
44 |
dynamic_wt r (err_step app step) succs ts |]
|
|
45 |
==> static_wt r app step succs (map ok_val ts)"
|
|
46 |
proof (unfold static_wt_def, intro strip, rule conjI)
|
|
47 |
|
|
48 |
assume b: "bounded succs (size ts)"
|
|
49 |
assume n: "non_empty succs"
|
|
50 |
assume wt: "dynamic_wt r (err_step app step) succs ts"
|
|
51 |
|
|
52 |
fix p
|
|
53 |
assume "p < length (map ok_val ts)"
|
|
54 |
hence lp: "p < length ts" by simp
|
|
55 |
|
|
56 |
from wt lp
|
|
57 |
have [intro?]: "!!p. p < length ts ==> ts ! p ~= Err"
|
11299
|
58 |
by (unfold dynamic_wt_def wt_step_def) simp
|
11229
|
59 |
|
|
60 |
show app: "app p (map ok_val ts ! p)"
|
|
61 |
proof -
|
|
62 |
from n
|
|
63 |
obtain q where q: "q:set(succs p)"
|
|
64 |
by (auto dest: non_emptyD)
|
|
65 |
|
|
66 |
from wt lp q
|
|
67 |
obtain s where
|
|
68 |
OKp: "ts ! p = OK s" and
|
|
69 |
less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
|
11299
|
70 |
by (unfold dynamic_wt_def wt_step_def stable_def)
|
11229
|
71 |
(auto iff: not_Err_eq)
|
|
72 |
|
|
73 |
from lp b q
|
|
74 |
have lq: "q < length ts"
|
|
75 |
by (unfold bounded_def) blast
|
|
76 |
hence "ts!q ~= Err" ..
|
|
77 |
then
|
|
78 |
obtain s' where OKq: "ts ! q = OK s'"
|
|
79 |
by (auto iff: not_Err_eq)
|
|
80 |
|
|
81 |
with OKp less
|
|
82 |
have "app p s"
|
|
83 |
by (simp add: err_step_def lift_def split: err.split_asm split_if_asm)
|
|
84 |
|
|
85 |
with lp OKp
|
|
86 |
show ?thesis
|
|
87 |
by simp
|
|
88 |
qed
|
|
89 |
|
|
90 |
show "!q:set(succs p). step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
|
|
91 |
proof (intro strip)
|
|
92 |
fix q
|
|
93 |
assume q: "q:set (succs p)"
|
|
94 |
|
|
95 |
from wt lp q
|
|
96 |
obtain s where
|
|
97 |
OKp: "ts ! p = OK s" and
|
|
98 |
less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
|
11299
|
99 |
by (unfold dynamic_wt_def wt_step_def stable_def)
|
11229
|
100 |
(auto iff: not_Err_eq)
|
|
101 |
|
|
102 |
from lp b q
|
|
103 |
have lq: "q < length ts"
|
|
104 |
by (unfold bounded_def) blast
|
|
105 |
hence "ts!q ~= Err" ..
|
|
106 |
then
|
|
107 |
obtain s' where OKq: "ts ! q = OK s'"
|
|
108 |
by (auto iff: not_Err_eq)
|
|
109 |
|
|
110 |
from lp lq OKp OKq app less
|
|
111 |
show "step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
|
|
112 |
by (simp add: err_step_def lift_def)
|
|
113 |
qed
|
|
114 |
qed
|
|
115 |
|
|
116 |
|
|
117 |
lemma static_imp_dynamic:
|
|
118 |
"[| static_wt r app step succs ts; bounded succs (size ts) |]
|
|
119 |
==> dynamic_wt r (err_step app step) succs (map OK ts)"
|
11299
|
120 |
proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI)
|
11229
|
121 |
assume bounded: "bounded succs (size ts)"
|
|
122 |
assume static: "static_wt r app step succs ts"
|
|
123 |
fix p assume "p < length (map OK ts)"
|
|
124 |
hence p: "p < length ts" by simp
|
|
125 |
thus "map OK ts ! p \<noteq> Err" by simp
|
|
126 |
{ fix q
|
|
127 |
assume q: "q : set (succs p)"
|
|
128 |
with p static obtain
|
|
129 |
"app p (ts ! p)" "step p (ts ! p) <=_r ts ! q"
|
|
130 |
by (unfold static_wt_def) blast
|
|
131 |
moreover
|
|
132 |
from q p bounded
|
|
133 |
have "q < size ts" by (unfold bounded_def) blast
|
|
134 |
hence "map OK ts ! q = OK (ts!q)" by simp
|
|
135 |
moreover
|
|
136 |
have "p < size ts" by (rule p)
|
|
137 |
ultimately
|
|
138 |
have "err_step app step p (map OK ts ! p) <=_(Err.le r) map OK ts ! q"
|
|
139 |
by (simp add: err_step_def lift_def)
|
|
140 |
}
|
|
141 |
thus "stable (Err.le r) (err_step app step) succs (map OK ts) p"
|
|
142 |
by (unfold stable_def) blast
|
|
143 |
qed
|
|
144 |
|
|
145 |
end
|