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