equal
deleted
inserted
replaced
6 |
6 |
7 subsection "Constant Propagation" |
7 subsection "Constant Propagation" |
8 |
8 |
9 datatype cval = Const val | Any |
9 datatype cval = Const val | Any |
10 |
10 |
11 fun rep_cval where |
11 fun \<gamma>_cval where |
12 "rep_cval (Const n) = {n}" | |
12 "\<gamma>_cval (Const n) = {n}" | |
13 "rep_cval (Any) = UNIV" |
13 "\<gamma>_cval (Any) = UNIV" |
14 |
14 |
15 fun plus_cval where |
15 fun plus_cval where |
16 "plus_cval (Const m) (Const n) = Const(m+n)" | |
16 "plus_cval (Const m) (Const n) = Const(m+n)" | |
17 "plus_cval _ _ = Any" |
17 "plus_cval _ _ = Any" |
18 |
18 |
50 qed |
50 qed |
51 |
51 |
52 end |
52 end |
53 |
53 |
54 |
54 |
55 interpretation Val_abs rep_cval Const plus_cval |
55 interpretation Val_abs \<gamma>_cval Const plus_cval |
56 defines aval'_const is aval' |
56 defines aval'_const is aval' |
57 proof |
57 proof |
58 case goal1 thus ?case |
58 case goal1 thus ?case |
59 by(cases a, cases b, simp, simp, cases b, simp, simp) |
59 by(cases a, cases b, simp, simp, cases b, simp, simp) |
60 next |
60 next |
64 next |
64 next |
65 case goal4 thus ?case |
65 case goal4 thus ?case |
66 by(auto simp: plus_cval_cases split: cval.split) |
66 by(auto simp: plus_cval_cases split: cval.split) |
67 qed |
67 qed |
68 |
68 |
69 interpretation Abs_Int rep_cval Const plus_cval |
69 interpretation Abs_Int \<gamma>_cval Const plus_cval |
70 defines AI_const is AI |
70 defines AI_const is AI |
71 and step_const is step' |
71 and step_const is step' |
72 proof qed |
72 proof qed |
73 |
73 |
74 |
74 |
75 text{* Monotonicity: *} |
75 text{* Monotonicity: *} |
76 |
76 |
77 interpretation Abs_Int_mono rep_cval Const plus_cval |
77 interpretation Abs_Int_mono \<gamma>_cval Const plus_cval |
78 proof |
78 proof |
79 case goal1 thus ?case |
79 case goal1 thus ?case |
80 by(auto simp: plus_cval_cases split: cval.split) |
80 by(auto simp: plus_cval_cases split: cval.split) |
81 qed |
81 qed |
82 |
82 |