author | nipkow |
Wed, 17 Apr 2013 21:11:01 +0200 | |
changeset 51711 | df3426139651 |
parent 51389 | 8a9f0503b1c0 |
child 51801 | 1006b9b08d73 |
permissions | -rw-r--r-- |
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 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
26 |
fun less_eq_const where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
27 |
"_ \<le> Any = True" | |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
28 |
"Const n \<le> Const m = (n=m)" | |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
29 |
"Any \<le> Const _ = False" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
30 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
31 |
definition "a < (b::const) = (a \<le> b & ~ b \<le> a)" |
47613 | 32 |
|
51389 | 33 |
fun sup_const where |
47613 | 34 |
"Const m \<squnion> Const n = (if n=m then Const m else Any)" | |
35 |
"_ \<squnion> _ = Any" |
|
36 |
||
37 |
definition "\<top> = Any" |
|
38 |
||
39 |
instance |
|
40 |
proof |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
41 |
case goal1 thus ?case by (rule less_const_def) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
42 |
next |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
43 |
case goal2 show ?case by (cases x) simp_all |
47613 | 44 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
45 |
case goal3 thus ?case by(cases z, cases y, cases x, simp_all) |
47613 | 46 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
47 |
case goal4 thus ?case by(cases x, cases y, simp_all, cases y, simp_all) |
47613 | 48 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
49 |
case goal6 thus ?case by(cases x, cases y, simp_all) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
50 |
next |
51389 | 51 |
case goal5 thus ?case by(cases y, cases x, simp_all) |
47613 | 52 |
next |
51389 | 53 |
case goal7 thus ?case by(cases z, cases y, cases x, simp_all) |
47613 | 54 |
next |
51389 | 55 |
case goal8 thus ?case by(simp add: top_const_def) |
47613 | 56 |
qed |
57 |
||
58 |
end |
|
59 |
||
60 |
||
61 |
interpretation Val_abs |
|
62 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
|
63 |
proof |
|
64 |
case goal1 thus ?case |
|
65 |
by(cases a, cases b, simp, simp, cases b, simp, simp) |
|
66 |
next |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
67 |
case goal2 show ?case by(simp add: top_const_def) |
47613 | 68 |
next |
69 |
case goal3 show ?case by simp |
|
70 |
next |
|
71 |
case goal4 thus ?case |
|
72 |
by(auto simp: plus_const_cases split: const.split) |
|
73 |
qed |
|
74 |
||
75 |
interpretation Abs_Int |
|
76 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
|
77 |
defines AI_const is AI and step_const is step' and aval'_const is aval' |
|
78 |
.. |
|
79 |
||
80 |
||
81 |
subsubsection "Tests" |
|
82 |
||
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51389
diff
changeset
|
83 |
definition "steps c i = (step_const \<top> ^^ i) (bot c)" |
47613 | 84 |
|
85 |
value "show_acom (steps test1_const 0)" |
|
86 |
value "show_acom (steps test1_const 1)" |
|
87 |
value "show_acom (steps test1_const 2)" |
|
88 |
value "show_acom (steps test1_const 3)" |
|
50995 | 89 |
value "show_acom (the(AI_const test1_const))" |
47613 | 90 |
|
50995 | 91 |
value "show_acom (the(AI_const test2_const))" |
92 |
value "show_acom (the(AI_const test3_const))" |
|
47613 | 93 |
|
94 |
value "show_acom (steps test4_const 0)" |
|
95 |
value "show_acom (steps test4_const 1)" |
|
96 |
value "show_acom (steps test4_const 2)" |
|
97 |
value "show_acom (steps test4_const 3)" |
|
49188 | 98 |
value "show_acom (steps test4_const 4)" |
50995 | 99 |
value "show_acom (the(AI_const test4_const))" |
47613 | 100 |
|
101 |
value "show_acom (steps test5_const 0)" |
|
102 |
value "show_acom (steps test5_const 1)" |
|
103 |
value "show_acom (steps test5_const 2)" |
|
104 |
value "show_acom (steps test5_const 3)" |
|
105 |
value "show_acom (steps test5_const 4)" |
|
106 |
value "show_acom (steps test5_const 5)" |
|
49188 | 107 |
value "show_acom (steps test5_const 6)" |
50995 | 108 |
value "show_acom (the(AI_const test5_const))" |
47613 | 109 |
|
110 |
value "show_acom (steps test6_const 0)" |
|
111 |
value "show_acom (steps test6_const 1)" |
|
112 |
value "show_acom (steps test6_const 2)" |
|
113 |
value "show_acom (steps test6_const 3)" |
|
114 |
value "show_acom (steps test6_const 4)" |
|
115 |
value "show_acom (steps test6_const 5)" |
|
116 |
value "show_acom (steps test6_const 6)" |
|
117 |
value "show_acom (steps test6_const 7)" |
|
118 |
value "show_acom (steps test6_const 8)" |
|
119 |
value "show_acom (steps test6_const 9)" |
|
120 |
value "show_acom (steps test6_const 10)" |
|
121 |
value "show_acom (steps test6_const 11)" |
|
49188 | 122 |
value "show_acom (steps test6_const 12)" |
123 |
value "show_acom (steps test6_const 13)" |
|
50995 | 124 |
value "show_acom (the(AI_const test6_const))" |
47613 | 125 |
|
126 |
||
127 |
text{* Monotonicity: *} |
|
128 |
||
129 |
interpretation Abs_Int_mono |
|
130 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
|
131 |
proof |
|
132 |
case goal1 thus ?case |
|
133 |
by(auto simp: plus_const_cases split: const.split) |
|
134 |
qed |
|
135 |
||
136 |
text{* Termination: *} |
|
137 |
||
138 |
definition "m_const x = (case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)" |
|
139 |
||
140 |
interpretation Abs_Int_measure |
|
141 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
|
49433 | 142 |
and m = m_const and h = "1" |
47613 | 143 |
proof |
144 |
case goal1 thus ?case by(auto simp: m_const_def split: const.splits) |
|
145 |
next |
|
51372 | 146 |
case goal2 thus ?case by(auto simp: m_const_def less_const_def split: const.splits) |
47613 | 147 |
qed |
148 |
||
149 |
thm AI_Some_measure |
|
150 |
||
151 |
end |