author | nipkow |
Tue, 15 Sep 2015 17:09:13 +0200 | |
changeset 61179 | 16775cad1a5c |
parent 58310 | 91ea607a34d8 |
child 61671 | 20d4cd2ceab2 |
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 |
||
58310 | 9 |
datatype const = Const val | Any |
47613 | 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 |
||
51826 | 23 |
instantiation const :: semilattice_sup_top |
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 |
|
51802 | 30 |
fun sup_const where "x \<squnion> y = (if x=y then x else Any)" |
47613 | 31 |
|
32 |
definition "\<top> = Any" |
|
33 |
||
34 |
instance |
|
61179 | 35 |
proof (standard, goal_cases) |
36 |
case 1 thus ?case by (rule less_const_def) |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
37 |
next |
61179 | 38 |
case (2 x) show ?case by (cases x) simp_all |
47613 | 39 |
next |
61179 | 40 |
case (3 x y z) thus ?case by(cases z, cases y, cases x, simp_all) |
47613 | 41 |
next |
61179 | 42 |
case (4 x y) thus ?case by(cases x, cases y, simp_all, cases y, simp_all) |
47613 | 43 |
next |
61179 | 44 |
case (6 x y) thus ?case by(cases x, cases y, simp_all) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51036
diff
changeset
|
45 |
next |
61179 | 46 |
case (5 x y) thus ?case by(cases y, cases x, simp_all) |
47613 | 47 |
next |
61179 | 48 |
case (7 x y z) thus ?case by(cases z, cases y, cases x, simp_all) |
47613 | 49 |
next |
61179 | 50 |
case 8 thus ?case by(simp add: top_const_def) |
47613 | 51 |
qed |
52 |
||
53 |
end |
|
54 |
||
55 |
||
55599
6535c537b243
aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents:
52504
diff
changeset
|
56 |
permanent_interpretation Val_semilattice |
47613 | 57 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
61179 | 58 |
proof (standard, goal_cases) |
59 |
case (1 a b) thus ?case |
|
47613 | 60 |
by(cases a, cases b, simp, simp, cases b, simp, simp) |
61 |
next |
|
61179 | 62 |
case 2 show ?case by(simp add: top_const_def) |
47613 | 63 |
next |
61179 | 64 |
case 3 show ?case by simp |
47613 | 65 |
next |
61179 | 66 |
case 4 thus ?case by(auto simp: plus_const_cases split: const.split) |
47613 | 67 |
qed |
68 |
||
55599
6535c537b243
aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents:
52504
diff
changeset
|
69 |
permanent_interpretation Abs_Int |
47613 | 70 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
55600
3c7610b8dcfc
more convenient syntax for permanent interpretation
haftmann
parents:
55599
diff
changeset
|
71 |
defining AI_const = AI and step_const = step' and aval'_const = aval' |
47613 | 72 |
.. |
73 |
||
74 |
||
75 |
subsubsection "Tests" |
|
76 |
||
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51389
diff
changeset
|
77 |
definition "steps c i = (step_const \<top> ^^ i) (bot c)" |
47613 | 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)" |
|
50995 | 83 |
value "show_acom (the(AI_const test1_const))" |
47613 | 84 |
|
50995 | 85 |
value "show_acom (the(AI_const test2_const))" |
86 |
value "show_acom (the(AI_const test3_const))" |
|
47613 | 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)" |
50995 | 93 |
value "show_acom (the(AI_const test4_const))" |
47613 | 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)" |
50995 | 102 |
value "show_acom (the(AI_const test5_const))" |
47613 | 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)" |
|
50995 | 118 |
value "show_acom (the(AI_const test6_const))" |
47613 | 119 |
|
120 |
||
121 |
text{* Monotonicity: *} |
|
122 |
||
55599
6535c537b243
aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents:
52504
diff
changeset
|
123 |
permanent_interpretation Abs_Int_mono |
47613 | 124 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
61179 | 125 |
proof (standard, goal_cases) |
126 |
case 1 thus ?case by(auto simp: plus_const_cases split: const.split) |
|
47613 | 127 |
qed |
128 |
||
129 |
text{* Termination: *} |
|
130 |
||
51803 | 131 |
definition m_const :: "const \<Rightarrow> nat" where |
132 |
"m_const x = (if x = Any then 0 else 1)" |
|
47613 | 133 |
|
55599
6535c537b243
aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
haftmann
parents:
52504
diff
changeset
|
134 |
permanent_interpretation Abs_Int_measure |
47613 | 135 |
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
49433 | 136 |
and m = m_const and h = "1" |
61179 | 137 |
proof (standard, goal_cases) |
138 |
case 1 thus ?case by(auto simp: m_const_def split: const.splits) |
|
47613 | 139 |
next |
61179 | 140 |
case 2 thus ?case by(auto simp: m_const_def less_const_def split: const.splits) |
47613 | 141 |
qed |
142 |
||
143 |
thm AI_Some_measure |
|
144 |
||
145 |
end |