|
1 (* Title: HOL/BCV/DFA_Framework.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TUM |
|
5 |
|
6 The relationship between dataflow analysis and a welltyped-insruction predicate. |
|
7 *) |
|
8 |
|
9 header "Dataflow Analysis Framework" |
|
10 |
|
11 theory DFA_Framework = Listn: |
|
12 |
|
13 constdefs |
|
14 |
|
15 stable :: "'s ord => |
|
16 (nat => 's => 's) |
|
17 => (nat => nat list) => 's list => nat => bool" |
|
18 "stable r step succs ss p == !q:set(succs p). step p (ss!p) <=_r ss!q" |
|
19 |
|
20 stables :: "'s ord => (nat => 's => 's) |
|
21 => (nat => nat list) => 's list => bool" |
|
22 "stables r step succs ss == !p<size ss. stable r step succs ss p" |
|
23 |
|
24 is_dfa :: "'s ord |
|
25 => ('s list => 's list) |
|
26 => (nat => 's => 's) |
|
27 => (nat => nat list) |
|
28 => nat => 's set => bool" |
|
29 "is_dfa r dfa step succs n A == !ss : list n A. |
|
30 dfa ss : list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss & |
|
31 (!ts: list n A. ss <=[r] ts & stables r step succs ts |
|
32 --> dfa ss <=[r] ts)" |
|
33 |
|
34 is_bcv :: "'s ord => 's => (nat => 's => 's) => (nat => nat list) |
|
35 => nat => 's set => ('s list => 's list) => bool" |
|
36 "is_bcv r T step succs n A bcv == !ss : list n A. |
|
37 (!p<n. (bcv ss)!p ~= T) = |
|
38 (? ts: list n A. ss <=[r] ts & welltyping r T step succs ts)" |
|
39 |
|
40 welltyping :: |
|
41 "'s ord => 's => (nat => 's => 's) => (nat => nat list) => 's list => bool" |
|
42 "welltyping r T step succs ts == |
|
43 !p<size(ts). ts!p ~= T & stable r step succs ts p" |
|
44 |
|
45 |
|
46 lemma is_dfaD: |
|
47 "[| is_dfa r dfa step succs n A; ss : list n A |] ==> |
|
48 dfa ss:list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss & |
|
49 (!ts: list n A. stables r step succs ts & ss <=[r] ts |
|
50 --> dfa ss <=[r] ts)" |
|
51 by (simp add: is_dfa_def) |
|
52 |
|
53 |
|
54 lemma is_bcv_dfa: |
|
55 "[| order r; top r T; is_dfa r dfa step succs n A |] |
|
56 ==> is_bcv r T step succs n A dfa" |
|
57 apply (unfold is_bcv_def welltyping_def stables_def) |
|
58 apply clarify |
|
59 apply (drule is_dfaD) |
|
60 apply assumption |
|
61 apply clarify |
|
62 apply (rule iffI) |
|
63 apply (rule bexI) |
|
64 apply (rule conjI) |
|
65 apply assumption |
|
66 apply (simp add: stables_def) |
|
67 apply assumption |
|
68 apply clarify |
|
69 apply (simp add: imp_conjR all_conj_distrib stables_def |
|
70 cong: conj_cong) |
|
71 apply (drule_tac x = ts in bspec) |
|
72 apply assumption |
|
73 apply (force dest: le_listD) |
|
74 done |
|
75 |
|
76 end |