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