equal
deleted
inserted
replaced
11 |
11 |
12 constdefs |
12 constdefs |
13 |
13 |
14 dynamic_wt :: "'s ord => (nat => 's err => 's err) => (nat => nat list) => |
14 dynamic_wt :: "'s ord => (nat => 's err => 's err) => (nat => nat list) => |
15 's err list => bool" |
15 's err list => bool" |
16 "dynamic_wt r step succs ts == welltyping (Err.le r) Err step succs ts" |
16 "dynamic_wt r step succs ts == wt_step (Err.le r) Err step succs ts" |
17 |
17 |
18 static_wt :: "'s ord => (nat => 's => bool) => |
18 static_wt :: "'s ord => (nat => 's => bool) => |
19 (nat => 's => 's) => (nat => nat list) => 's list => bool" |
19 (nat => 's => 's) => (nat => nat list) => 's list => bool" |
20 "static_wt r app step succs ts == |
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)" |
21 !p < size ts. app p (ts!p) & (!q:set(succs p). step p (ts!p) <=_r ts!q)" |
53 assume "p < length (map ok_val ts)" |
53 assume "p < length (map ok_val ts)" |
54 hence lp: "p < length ts" by simp |
54 hence lp: "p < length ts" by simp |
55 |
55 |
56 from wt lp |
56 from wt lp |
57 have [intro?]: "!!p. p < length ts ==> ts ! p ~= Err" |
57 have [intro?]: "!!p. p < length ts ==> ts ! p ~= Err" |
58 by (unfold dynamic_wt_def welltyping_def) simp |
58 by (unfold dynamic_wt_def wt_step_def) simp |
59 |
59 |
60 show app: "app p (map ok_val ts ! p)" |
60 show app: "app p (map ok_val ts ! p)" |
61 proof - |
61 proof - |
62 from n |
62 from n |
63 obtain q where q: "q:set(succs p)" |
63 obtain q where q: "q:set(succs p)" |
65 |
65 |
66 from wt lp q |
66 from wt lp q |
67 obtain s where |
67 obtain s where |
68 OKp: "ts ! p = OK s" and |
68 OKp: "ts ! p = OK s" and |
69 less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q" |
69 less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q" |
70 by (unfold dynamic_wt_def welltyping_def stable_def) |
70 by (unfold dynamic_wt_def wt_step_def stable_def) |
71 (auto iff: not_Err_eq) |
71 (auto iff: not_Err_eq) |
72 |
72 |
73 from lp b q |
73 from lp b q |
74 have lq: "q < length ts" |
74 have lq: "q < length ts" |
75 by (unfold bounded_def) blast |
75 by (unfold bounded_def) blast |
94 |
94 |
95 from wt lp q |
95 from wt lp q |
96 obtain s where |
96 obtain s where |
97 OKp: "ts ! p = OK s" and |
97 OKp: "ts ! p = OK s" and |
98 less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q" |
98 less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q" |
99 by (unfold dynamic_wt_def welltyping_def stable_def) |
99 by (unfold dynamic_wt_def wt_step_def stable_def) |
100 (auto iff: not_Err_eq) |
100 (auto iff: not_Err_eq) |
101 |
101 |
102 from lp b q |
102 from lp b q |
103 have lq: "q < length ts" |
103 have lq: "q < length ts" |
104 by (unfold bounded_def) blast |
104 by (unfold bounded_def) blast |
115 |
115 |
116 |
116 |
117 lemma static_imp_dynamic: |
117 lemma static_imp_dynamic: |
118 "[| static_wt r app step succs ts; bounded succs (size ts) |] |
118 "[| static_wt r app step succs ts; bounded succs (size ts) |] |
119 ==> dynamic_wt r (err_step app step) succs (map OK ts)" |
119 ==> dynamic_wt r (err_step app step) succs (map OK ts)" |
120 proof (unfold dynamic_wt_def welltyping_def, intro strip, rule conjI) |
120 proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI) |
121 assume bounded: "bounded succs (size ts)" |
121 assume bounded: "bounded succs (size ts)" |
122 assume static: "static_wt r app step succs ts" |
122 assume static: "static_wt r app step succs ts" |
123 fix p assume "p < length (map OK ts)" |
123 fix p assume "p < length (map OK ts)" |
124 hence p: "p < length ts" by simp |
124 hence p: "p < length ts" by simp |
125 thus "map OK ts ! p \<noteq> Err" by simp |
125 thus "map OK ts ! p \<noteq> Err" by simp |