47613
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
theory Abs_Int1_const
|
|
4 |
imports Abs_Int1
|
|
5 |
begin
|
|
6 |
|
|
7 |
subsection "Constant Propagation"
|
|
8 |
|
|
9 |
datatype const = Const val | Any
|
|
10 |
|
|
11 |
fun \<gamma>_const where
|
|
12 |
"\<gamma>_const (Const n) = {n}" |
|
|
13 |
"\<gamma>_const (Any) = UNIV"
|
|
14 |
|
|
15 |
fun plus_const where
|
|
16 |
"plus_const (Const m) (Const n) = Const(m+n)" |
|
|
17 |
"plus_const _ _ = Any"
|
|
18 |
|
|
19 |
lemma plus_const_cases: "plus_const a1 a2 =
|
|
20 |
(case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
|
|
21 |
by(auto split: prod.split const.split)
|
|
22 |
|
49396
|
23 |
instantiation const :: semilattice
|
47613
|
24 |
begin
|
|
25 |
|
|
26 |
fun le_const where
|
|
27 |
"_ \<sqsubseteq> Any = True" |
|
|
28 |
"Const n \<sqsubseteq> Const m = (n=m)" |
|
|
29 |
"Any \<sqsubseteq> Const _ = False"
|
|
30 |
|
|
31 |
fun join_const where
|
|
32 |
"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
|
|
33 |
"_ \<squnion> _ = Any"
|
|
34 |
|
|
35 |
definition "\<top> = Any"
|
|
36 |
|
|
37 |
instance
|
|
38 |
proof
|
|
39 |
case goal1 thus ?case by (cases x) simp_all
|
|
40 |
next
|
|
41 |
case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
|
|
42 |
next
|
|
43 |
case goal3 thus ?case by(cases x, cases y, simp_all)
|
|
44 |
next
|
|
45 |
case goal4 thus ?case by(cases y, cases x, simp_all)
|
|
46 |
next
|
|
47 |
case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
|
|
48 |
next
|
|
49 |
case goal6 thus ?case by(simp add: Top_const_def)
|
|
50 |
qed
|
|
51 |
|
|
52 |
end
|
|
53 |
|
|
54 |
|
|
55 |
interpretation Val_abs
|
|
56 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
|
|
57 |
proof
|
|
58 |
case goal1 thus ?case
|
|
59 |
by(cases a, cases b, simp, simp, cases b, simp, simp)
|
|
60 |
next
|
|
61 |
case goal2 show ?case by(simp add: Top_const_def)
|
|
62 |
next
|
|
63 |
case goal3 show ?case by simp
|
|
64 |
next
|
|
65 |
case goal4 thus ?case
|
|
66 |
by(auto simp: plus_const_cases split: const.split)
|
|
67 |
qed
|
|
68 |
|
|
69 |
interpretation Abs_Int
|
|
70 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
|
|
71 |
defines AI_const is AI and step_const is step' and aval'_const is aval'
|
|
72 |
..
|
|
73 |
|
|
74 |
|
|
75 |
subsubsection "Tests"
|
|
76 |
|
|
77 |
definition "steps c i = (step_const(top c) ^^ i) (bot c)"
|
|
78 |
|
|
79 |
value "show_acom (steps test1_const 0)"
|
|
80 |
value "show_acom (steps test1_const 1)"
|
|
81 |
value "show_acom (steps test1_const 2)"
|
|
82 |
value "show_acom (steps test1_const 3)"
|
|
83 |
value "show_acom_opt (AI_const test1_const)"
|
|
84 |
|
|
85 |
value "show_acom_opt (AI_const test2_const)"
|
|
86 |
value "show_acom_opt (AI_const test3_const)"
|
|
87 |
|
|
88 |
value "show_acom (steps test4_const 0)"
|
|
89 |
value "show_acom (steps test4_const 1)"
|
|
90 |
value "show_acom (steps test4_const 2)"
|
|
91 |
value "show_acom (steps test4_const 3)"
|
49188
|
92 |
value "show_acom (steps test4_const 4)"
|
47613
|
93 |
value "show_acom_opt (AI_const test4_const)"
|
|
94 |
|
|
95 |
value "show_acom (steps test5_const 0)"
|
|
96 |
value "show_acom (steps test5_const 1)"
|
|
97 |
value "show_acom (steps test5_const 2)"
|
|
98 |
value "show_acom (steps test5_const 3)"
|
|
99 |
value "show_acom (steps test5_const 4)"
|
|
100 |
value "show_acom (steps test5_const 5)"
|
49188
|
101 |
value "show_acom (steps test5_const 6)"
|
47613
|
102 |
value "show_acom_opt (AI_const test5_const)"
|
|
103 |
|
|
104 |
value "show_acom (steps test6_const 0)"
|
|
105 |
value "show_acom (steps test6_const 1)"
|
|
106 |
value "show_acom (steps test6_const 2)"
|
|
107 |
value "show_acom (steps test6_const 3)"
|
|
108 |
value "show_acom (steps test6_const 4)"
|
|
109 |
value "show_acom (steps test6_const 5)"
|
|
110 |
value "show_acom (steps test6_const 6)"
|
|
111 |
value "show_acom (steps test6_const 7)"
|
|
112 |
value "show_acom (steps test6_const 8)"
|
|
113 |
value "show_acom (steps test6_const 9)"
|
|
114 |
value "show_acom (steps test6_const 10)"
|
|
115 |
value "show_acom (steps test6_const 11)"
|
49188
|
116 |
value "show_acom (steps test6_const 12)"
|
|
117 |
value "show_acom (steps test6_const 13)"
|
47613
|
118 |
value "show_acom_opt (AI_const test6_const)"
|
|
119 |
|
|
120 |
|
|
121 |
text{* Monotonicity: *}
|
|
122 |
|
|
123 |
interpretation Abs_Int_mono
|
|
124 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
|
|
125 |
proof
|
|
126 |
case goal1 thus ?case
|
|
127 |
by(auto simp: plus_const_cases split: const.split)
|
|
128 |
qed
|
|
129 |
|
|
130 |
text{* Termination: *}
|
|
131 |
|
|
132 |
definition "m_const x = (case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)"
|
|
133 |
|
|
134 |
interpretation Abs_Int_measure
|
|
135 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
|
|
136 |
and m = m_const and h = "2"
|
|
137 |
proof
|
|
138 |
case goal1 thus ?case by(auto simp: m_const_def split: const.splits)
|
|
139 |
next
|
|
140 |
case goal2 thus ?case by(auto simp: m_const_def split: const.splits)
|
|
141 |
next
|
|
142 |
case goal3 thus ?case by(auto simp: m_const_def split: const.splits)
|
|
143 |
qed
|
|
144 |
|
|
145 |
thm AI_Some_measure
|
|
146 |
|
|
147 |
end
|