9 |
9 |
10 theory Typing_Framework_err = Typing_Framework: |
10 theory Typing_Framework_err = Typing_Framework: |
11 |
11 |
12 constdefs |
12 constdefs |
13 |
13 |
14 dynamic_wt :: "'s ord => 's err step_type => 's err list => bool" |
14 dynamic_wt :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool" |
15 "dynamic_wt r step ts == wt_step (Err.le r) Err step ts" |
15 "dynamic_wt r step ts == wt_step (Err.le r) Err step ts" |
16 |
16 |
17 static_wt :: "'s ord => (nat => 's => bool) => 's step_type => 's list => bool" |
17 static_wt :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" |
18 "static_wt r app step ts == |
18 "static_wt r app step ts == |
19 \<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)" |
19 \<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)" |
20 |
20 |
21 map_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'c) list" |
21 map_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'c) list" |
22 "map_snd f == map (\<lambda>(x,y). (x, f y))" |
22 "map_snd f == map (\<lambda>(x,y). (x, f y))" |
26 |
26 |
27 err_step :: "(nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type" |
27 err_step :: "(nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type" |
28 "err_step app step p t == case t of Err \<Rightarrow> map_err (step p arbitrary) | OK t' \<Rightarrow> |
28 "err_step app step p t == case t of Err \<Rightarrow> map_err (step p arbitrary) | OK t' \<Rightarrow> |
29 if app p t' then map_snd OK (step p t') else map_err (step p t')" |
29 if app p t' then map_snd OK (step p t') else map_err (step p t')" |
30 |
30 |
31 non_empty :: "'s step_type => bool" |
31 non_empty :: "'s step_type \<Rightarrow> bool" |
32 "non_empty step == \<forall>p t. step p t \<noteq> []" |
32 "non_empty step == \<forall>p t. step p t \<noteq> []" |
33 |
33 |
34 |
34 |
35 lemmas err_step_defs = err_step_def map_snd_def map_err_def |
35 lemmas err_step_defs = err_step_def map_snd_def map_err_def |
36 |
36 |
37 lemma non_emptyD: |
37 lemma non_emptyD: |
38 "non_empty step ==> \<exists>q t'. (q,t') \<in> set(step p t)" |
38 "non_empty step \<Longrightarrow> \<exists>q t'. (q,t') \<in> set(step p t)" |
39 proof (unfold non_empty_def) |
39 proof (unfold non_empty_def) |
40 assume "\<forall>p t. step p t \<noteq> []" |
40 assume "\<forall>p t. step p t \<noteq> []" |
41 hence "step p t \<noteq> []" by blast |
41 hence "step p t \<noteq> []" by blast |
42 then obtain x xs where "step p t = x#xs" |
42 then obtain x xs where "step p t = x#xs" |
43 by (auto simp add: neq_Nil_conv) |
43 by (auto simp add: neq_Nil_conv) |
45 thus ?thesis by (cases x) blast |
45 thus ?thesis by (cases x) blast |
46 qed |
46 qed |
47 |
47 |
48 |
48 |
49 lemma dynamic_imp_static: |
49 lemma dynamic_imp_static: |
50 "[| bounded step (size ts); non_empty step; |
50 "\<lbrakk> bounded step (size ts); non_empty step; |
51 dynamic_wt r (err_step app step) ts |] |
51 dynamic_wt r (err_step app step) ts \<rbrakk> |
52 ==> static_wt r app step (map ok_val ts)" |
52 \<Longrightarrow> static_wt r app step (map ok_val ts)" |
53 proof (unfold static_wt_def, intro strip, rule conjI) |
53 proof (unfold static_wt_def, intro strip, rule conjI) |
54 |
54 |
55 assume b: "bounded step (size ts)" |
55 assume b: "bounded step (size ts)" |
56 assume n: "non_empty step" |
56 assume n: "non_empty step" |
57 assume wt: "dynamic_wt r (err_step app step) ts" |
57 assume wt: "dynamic_wt r (err_step app step) ts" |
110 qed |
110 qed |
111 qed |
111 qed |
112 |
112 |
113 |
113 |
114 lemma static_imp_dynamic: |
114 lemma static_imp_dynamic: |
115 "[| static_wt r app step ts; bounded step (size ts) |] |
115 "\<lbrakk> static_wt r app step ts; bounded step (size ts) \<rbrakk> |
116 ==> dynamic_wt r (err_step app step) (map OK ts)" |
116 \<Longrightarrow> dynamic_wt r (err_step app step) (map OK ts)" |
117 proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI) |
117 proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI) |
118 assume bounded: "bounded step (size ts)" |
118 assume bounded: "bounded step (size ts)" |
119 assume static: "static_wt r app step ts" |
119 assume static: "static_wt r app step ts" |
120 fix p assume "p < length (map OK ts)" |
120 fix p assume "p < length (map OK ts)" |
121 hence p: "p < length ts" by simp |
121 hence p: "p < length ts" by simp |