author | kuncar |
Wed, 15 May 2013 12:10:39 +0200 | |
changeset 51994 | 82cc2aeb7d13 |
parent 51974 | 9c80e62161a5 |
child 52504 | 52cd8bebc3b6 |
permissions | -rw-r--r-- |
47613 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory Abs_Int2_ivl |
|
51390 | 4 |
imports Abs_Int2 |
47613 | 5 |
begin |
6 |
||
7 |
subsection "Interval Analysis" |
|
8 |
||
51913 | 9 |
text{* Drop @{const Fin} around numerals on output: *} |
10 |
translations |
|
11 |
"_Numeral i" <= "CONST Fin(_Numeral i)" |
|
12 |
"0" <= "CONST Fin 0" |
|
13 |
"1" <= "CONST Fin 1" |
|
14 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
15 |
type_synonym eint = "int extended" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
16 |
type_synonym eint2 = "eint * eint" |
51245 | 17 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
18 |
definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
19 |
"\<gamma>_rep p = (let (l,h) = p in {i. l \<le> Fin i \<and> Fin i \<le> h})" |
47613 | 20 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
21 |
definition eq_ivl :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
22 |
"eq_ivl p1 p2 = (\<gamma>_rep p1 = \<gamma>_rep p2)" |
47613 | 23 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
24 |
lemma refl_eq_ivl[simp]: "eq_ivl p p" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
25 |
by(auto simp: eq_ivl_def) |
51245 | 26 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
27 |
quotient_type ivl = eint2 / eq_ivl |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
28 |
by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def) |
47613 | 29 |
|
51924 | 30 |
abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_, _]") where |
31 |
"[l,h] == abs_ivl(l,h)" |
|
51871 | 32 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
33 |
lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
34 |
by(simp add: eq_ivl_def) |
47613 | 35 |
|
51924 | 36 |
lemma \<gamma>_ivl_nice: "\<gamma>_ivl[l,h] = {i. l \<le> Fin i \<and> Fin i \<le> h}" |
51871 | 37 |
by transfer (simp add: \<gamma>_rep_def) |
47613 | 38 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
39 |
lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
40 |
by(auto simp: eq_ivl_def) |
51245 | 41 |
|
51887 | 42 |
lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" |
43 |
is "\<lambda>i (l,h). l \<le> Fin i \<and> Fin i \<le> h" |
|
44 |
by(auto simp: eq_ivl_def \<gamma>_rep_def) |
|
47613 | 45 |
|
51924 | 46 |
lemma in_ivl_nice: "in_ivl i [l,h] = (l \<le> Fin i \<and> Fin i \<le> h)" |
51887 | 47 |
by transfer simp |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
48 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
49 |
definition is_empty_rep :: "eint2 \<Rightarrow> bool" where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
50 |
"is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)" |
47613 | 51 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
52 |
lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j} | (Fin i,Pinf) => {i..} | |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
53 |
(Minf,Fin i) \<Rightarrow> {..i} | (Minf,Pinf) \<Rightarrow> UNIV | _ \<Rightarrow> {})" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
54 |
by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits) |
51245 | 55 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
56 |
lift_definition is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
57 |
apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
58 |
apply(auto simp: not_less less_eq_extended_cases split: extended.splits) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
59 |
done |
51245 | 60 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
61 |
lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
62 |
by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits) |
51245 | 63 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
64 |
definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)" |
51245 | 65 |
|
51994 | 66 |
lift_definition empty_ivl :: ivl is empty_rep . |
51245 | 67 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
68 |
lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
69 |
by(auto simp add: is_empty_rep_def empty_rep_def) |
47613 | 70 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
71 |
lemma is_empty_rep_iff: "is_empty_rep p = (\<gamma>_rep p = {})" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
72 |
by(auto simp add: \<gamma>_rep_cases is_empty_rep_def split: prod.splits extended.splits) |
47613 | 73 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
74 |
declare is_empty_rep_iff[THEN iffD1, simp] |
47613 | 75 |
|
76 |
||
51826 | 77 |
instantiation ivl :: semilattice_sup_top |
47613 | 78 |
begin |
79 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
80 |
definition le_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
81 |
"le_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
82 |
if is_empty_rep(l1,h1) then True else |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
83 |
if is_empty_rep(l2,h2) then False else l1 \<ge> l2 & h1 \<le> h2)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
84 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
85 |
lemma le_iff_subset: "le_rep p1 p2 \<longleftrightarrow> \<gamma>_rep p1 \<subseteq> \<gamma>_rep p2" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
86 |
apply rule |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
87 |
apply(auto simp: is_empty_rep_def le_rep_def \<gamma>_rep_def split: if_splits prod.splits)[1] |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
88 |
apply(auto simp: is_empty_rep_def \<gamma>_rep_cases le_rep_def) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
89 |
apply(auto simp: not_less split: extended.splits) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
90 |
done |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
91 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
92 |
lift_definition less_eq_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool" is le_rep |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
93 |
by(auto simp: eq_ivl_def le_iff_subset) |
47613 | 94 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
95 |
definition less_ivl where "i1 < i2 = (i1 \<le> i2 \<and> \<not> i2 \<le> (i1::ivl))" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
96 |
|
51874 | 97 |
lemma le_ivl_iff_subset: "iv1 \<le> iv2 \<longleftrightarrow> \<gamma>_ivl iv1 \<subseteq> \<gamma>_ivl iv2" |
98 |
by transfer (rule le_iff_subset) |
|
99 |
||
51389 | 100 |
definition sup_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where |
101 |
"sup_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
102 |
else let (l1,h1) = p1; (l2,h2) = p2 in (min l1 l2, max h1 h2))" |
47613 | 103 |
|
51389 | 104 |
lift_definition sup_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is sup_rep |
105 |
by(auto simp: eq_ivl_iff sup_rep_def) |
|
47613 | 106 |
|
51994 | 107 |
lift_definition top_ivl :: ivl is "(Minf,Pinf)" . |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
108 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
109 |
lemma is_empty_min_max: |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
110 |
"\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
111 |
by(auto simp add: is_empty_rep_def max_def min_def split: if_splits) |
47613 | 112 |
|
113 |
instance |
|
114 |
proof |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
115 |
case goal1 show ?case by (rule less_ivl_def) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
116 |
next |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
117 |
case goal2 show ?case by transfer (simp add: le_rep_def split: prod.splits) |
47613 | 118 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
119 |
case goal3 thus ?case by transfer (auto simp: le_rep_def split: if_splits) |
47613 | 120 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
121 |
case goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits) |
47613 | 122 |
next |
51389 | 123 |
case goal5 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
124 |
next |
51389 | 125 |
case goal6 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max) |
47613 | 126 |
next |
51389 | 127 |
case goal7 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def) |
47613 | 128 |
next |
51389 | 129 |
case goal8 show ?case by transfer (simp add: le_rep_def is_empty_rep_def) |
47613 | 130 |
qed |
131 |
||
132 |
end |
|
133 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
134 |
text{* Implement (naive) executable equality: *} |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
135 |
instantiation ivl :: equal |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
136 |
begin |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
137 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
138 |
definition equal_ivl where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
139 |
"equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
140 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
141 |
instance |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
142 |
proof |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
143 |
case goal1 show ?case by(simp add: equal_ivl_def eq_iff) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
144 |
qed |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
145 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
146 |
end |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
147 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
148 |
lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> x < Pinf) = (x = Pinf)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
149 |
by(simp add: not_less) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
150 |
lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> Minf < x) = (x = Minf)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
151 |
by(simp add: not_less) |
47613 | 152 |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
153 |
instantiation ivl :: bounded_lattice |
47613 | 154 |
begin |
155 |
||
51389 | 156 |
definition inf_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where |
157 |
"inf_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))" |
|
47613 | 158 |
|
51389 | 159 |
lemma \<gamma>_inf_rep: "\<gamma>_rep(inf_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2" |
160 |
by(auto simp:inf_rep_def \<gamma>_rep_cases split: prod.splits extended.splits) |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
161 |
|
51389 | 162 |
lift_definition inf_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is inf_rep |
163 |
by(auto simp: \<gamma>_inf_rep eq_ivl_def) |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
164 |
|
51874 | 165 |
lemma \<gamma>_inf: "\<gamma>_ivl (iv1 \<sqinter> iv2) = \<gamma>_ivl iv1 \<inter> \<gamma>_ivl iv2" |
166 |
by transfer (rule \<gamma>_inf_rep) |
|
167 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
168 |
definition "\<bottom> = empty_ivl" |
47613 | 169 |
|
170 |
instance |
|
171 |
proof |
|
51874 | 172 |
case goal1 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset) |
173 |
next |
|
174 |
case goal2 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset) |
|
51389 | 175 |
next |
51874 | 176 |
case goal3 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset) |
47613 | 177 |
next |
51874 | 178 |
case goal4 show ?case |
179 |
unfolding bot_ivl_def by transfer (auto simp: le_iff_subset) |
|
47613 | 180 |
qed |
181 |
||
182 |
end |
|
183 |
||
51245 | 184 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
185 |
lemma eq_ivl_empty: "eq_ivl p empty_rep = is_empty_rep p" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
186 |
by (metis eq_ivl_iff is_empty_empty_rep) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
187 |
|
51924 | 188 |
lemma le_ivl_nice: "[l1,h1] \<le> [l2,h2] \<longleftrightarrow> |
189 |
(if [l1,h1] = \<bottom> then True else |
|
190 |
if [l2,h2] = \<bottom> then False else l1 \<ge> l2 & h1 \<le> h2)" |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
191 |
unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
192 |
|
51924 | 193 |
lemma sup_ivl_nice: "[l1,h1] \<squnion> [l2,h2] = |
194 |
(if [l1,h1] = \<bottom> then [l2,h2] else |
|
195 |
if [l2,h2] = \<bottom> then [l1,h1] else [min l1 l2,max h1 h2])" |
|
51389 | 196 |
unfolding bot_ivl_def by transfer (simp add: sup_rep_def eq_ivl_empty) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
197 |
|
51924 | 198 |
lemma inf_ivl_nice: "[l1,h1] \<sqinter> [l2,h2] = [max l1 l2,min h1 h2]" |
51389 | 199 |
by transfer (simp add: inf_rep_def) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
200 |
|
51924 | 201 |
lemma top_ivl_nice: "\<top> = [-\<infinity>,\<infinity>]" |
51870 | 202 |
by (simp add: top_ivl_def) |
203 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
204 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
205 |
instantiation ivl :: plus |
47613 | 206 |
begin |
207 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
208 |
definition plus_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
209 |
"plus_rep p1 p2 = |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
210 |
(if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
211 |
let (l1,h1) = p1; (l2,h2) = p2 in (l1+l2, h1+h2))" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
212 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
213 |
lift_definition plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is plus_rep |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
214 |
by(auto simp: plus_rep_def eq_ivl_iff) |
51245 | 215 |
|
216 |
instance .. |
|
217 |
end |
|
218 |
||
51924 | 219 |
lemma plus_ivl_nice: "[l1,h1] + [l2,h2] = |
220 |
(if [l1,h1] = \<bottom> \<or> [l2,h2] = \<bottom> then \<bottom> else [l1+l2 , h1+h2])" |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
221 |
unfolding bot_ivl_def by transfer (auto simp: plus_rep_def eq_ivl_empty) |
51245 | 222 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
223 |
lemma uminus_eq_Minf[simp]: "-x = Minf \<longleftrightarrow> x = Pinf" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
224 |
by(cases x) auto |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
225 |
lemma uminus_eq_Pinf[simp]: "-x = Pinf \<longleftrightarrow> x = Minf" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
226 |
by(cases x) auto |
47613 | 227 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
228 |
lemma uminus_le_Fin_iff: "- x \<le> Fin(-y) \<longleftrightarrow> Fin y \<le> (x::'a::ordered_ab_group_add extended)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
229 |
by(cases x) auto |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
230 |
lemma Fin_uminus_le_iff: "Fin(-y) \<le> -x \<longleftrightarrow> x \<le> ((Fin y)::'a::ordered_ab_group_add extended)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
231 |
by(cases x) auto |
51245 | 232 |
|
233 |
instantiation ivl :: uminus |
|
234 |
begin |
|
235 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
236 |
definition uminus_rep :: "eint2 \<Rightarrow> eint2" where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
237 |
"uminus_rep p = (let (l,h) = p in (-h, -l))" |
51245 | 238 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
239 |
lemma \<gamma>_uminus_rep: "i : \<gamma>_rep p \<Longrightarrow> -i \<in> \<gamma>_rep(uminus_rep p)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
240 |
by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
241 |
split: prod.split) |
51261 | 242 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
243 |
lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
244 |
by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
245 |
(auto simp: Icc_eq_Icc split: extended.splits) |
51261 | 246 |
|
247 |
instance .. |
|
248 |
end |
|
249 |
||
51874 | 250 |
lemma \<gamma>_uminus: "i : \<gamma>_ivl iv \<Longrightarrow> -i \<in> \<gamma>_ivl(- iv)" |
251 |
by transfer (rule \<gamma>_uminus_rep) |
|
252 |
||
51924 | 253 |
lemma uminus_nice: "-[l,h] = [-h,-l]" |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
254 |
by transfer (simp add: uminus_rep_def) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
255 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
256 |
instantiation ivl :: minus |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
257 |
begin |
51882 | 258 |
|
259 |
definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where |
|
260 |
"(iv1::ivl) - iv2 = iv1 + -iv2" |
|
261 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
262 |
instance .. |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
263 |
end |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
264 |
|
47613 | 265 |
|
51974 | 266 |
definition inv_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where |
267 |
"inv_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv - iv2), iv2 \<sqinter> (iv - iv1))" |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
268 |
|
51882 | 269 |
definition above_rep :: "eint2 \<Rightarrow> eint2" where |
270 |
"above_rep p = (if is_empty_rep p then empty_rep else let (l,h) = p in (l,\<infinity>))" |
|
271 |
||
272 |
definition below_rep :: "eint2 \<Rightarrow> eint2" where |
|
273 |
"below_rep p = (if is_empty_rep p then empty_rep else let (l,h) = p in (-\<infinity>,h))" |
|
274 |
||
275 |
lift_definition above :: "ivl \<Rightarrow> ivl" is above_rep |
|
276 |
by(auto simp: above_rep_def eq_ivl_iff) |
|
277 |
||
278 |
lift_definition below :: "ivl \<Rightarrow> ivl" is below_rep |
|
279 |
by(auto simp: below_rep_def eq_ivl_iff) |
|
280 |
||
281 |
lemma \<gamma>_aboveI: "i \<in> \<gamma>_ivl iv \<Longrightarrow> i \<le> j \<Longrightarrow> j \<in> \<gamma>_ivl(above iv)" |
|
282 |
by transfer |
|
283 |
(auto simp add: above_rep_def \<gamma>_rep_cases is_empty_rep_def |
|
284 |
split: extended.splits) |
|
47613 | 285 |
|
51882 | 286 |
lemma \<gamma>_belowI: "i : \<gamma>_ivl iv \<Longrightarrow> j \<le> i \<Longrightarrow> j : \<gamma>_ivl(below iv)" |
287 |
by transfer |
|
288 |
(auto simp add: below_rep_def \<gamma>_rep_cases is_empty_rep_def |
|
289 |
split: extended.splits) |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
290 |
|
51974 | 291 |
definition inv_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where |
292 |
"inv_less_ivl res iv1 iv2 = |
|
51882 | 293 |
(if res |
51924 | 294 |
then (iv1 \<sqinter> (below iv2 - [Fin 1,Fin 1]), |
295 |
iv2 \<sqinter> (above iv1 + [Fin 1,Fin 1])) |
|
51882 | 296 |
else (iv1 \<sqinter> above iv2, iv2 \<sqinter> below iv1))" |
297 |
||
51924 | 298 |
lemma above_nice: "above[l,h] = (if [l,h] = \<bottom> then \<bottom> else [l,\<infinity>])" |
51882 | 299 |
unfolding bot_ivl_def by transfer (simp add: above_rep_def eq_ivl_empty) |
300 |
||
51924 | 301 |
lemma below_nice: "below[l,h] = (if [l,h] = \<bottom> then \<bottom> else [-\<infinity>,h])" |
51882 | 302 |
unfolding bot_ivl_def by transfer (simp add: below_rep_def eq_ivl_empty) |
47613 | 303 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
304 |
lemma add_mono_le_Fin: |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
305 |
"\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
306 |
by(drule (1) add_mono) simp |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
307 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
308 |
lemma add_mono_Fin_le: |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
309 |
"\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
310 |
by(drule (1) add_mono) simp |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
311 |
|
47613 | 312 |
interpretation Val_abs |
51245 | 313 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
47613 | 314 |
proof |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
315 |
case goal1 thus ?case by transfer (simp add: le_iff_subset) |
47613 | 316 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
317 |
case goal2 show ?case by transfer (simp add: \<gamma>_rep_def) |
47613 | 318 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
319 |
case goal3 show ?case by transfer (simp add: \<gamma>_rep_def) |
47613 | 320 |
next |
321 |
case goal4 thus ?case |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
322 |
apply transfer |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
323 |
apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
324 |
by(auto simp: empty_rep_def is_empty_rep_def) |
47613 | 325 |
qed |
326 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
327 |
|
47613 | 328 |
interpretation Val_abs1_gamma |
51245 | 329 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
47613 | 330 |
defines aval_ivl is aval' |
331 |
proof |
|
51874 | 332 |
case goal1 show ?case by(simp add: \<gamma>_inf) |
47613 | 333 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
334 |
case goal2 show ?case unfolding bot_ivl_def by transfer simp |
47613 | 335 |
qed |
336 |
||
337 |
interpretation Val_abs1 |
|
51245 | 338 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
47613 | 339 |
and test_num' = in_ivl |
51974 | 340 |
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl |
47613 | 341 |
proof |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
342 |
case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def) |
47613 | 343 |
next |
51874 | 344 |
case goal2 thus ?case |
51974 | 345 |
unfolding inv_plus_ivl_def minus_ivl_def |
51874 | 346 |
apply(clarsimp simp add: \<gamma>_inf) |
347 |
using gamma_plus'[of "i1+i2" _ "-i1"] gamma_plus'[of "i1+i2" _ "-i2"] |
|
348 |
by(simp add: \<gamma>_uminus) |
|
47613 | 349 |
next |
350 |
case goal3 thus ?case |
|
51974 | 351 |
unfolding inv_less_ivl_def minus_ivl_def |
51882 | 352 |
apply(clarsimp simp add: \<gamma>_inf split: if_splits) |
353 |
using gamma_plus'[of "i1+1" _ "-1"] gamma_plus'[of "i2 - 1" _ "1"] |
|
354 |
apply(simp add: \<gamma>_belowI[of i2] \<gamma>_aboveI[of i1] |
|
355 |
uminus_ivl.abs_eq uminus_rep_def \<gamma>_ivl_nice) |
|
356 |
apply(simp add: \<gamma>_aboveI[of i2] \<gamma>_belowI[of i1]) |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
357 |
done |
47613 | 358 |
qed |
359 |
||
360 |
interpretation Abs_Int1 |
|
51245 | 361 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
47613 | 362 |
and test_num' = in_ivl |
51974 | 363 |
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl |
364 |
defines inv_aval_ivl is inv_aval'' |
|
365 |
and inv_bval_ivl is inv_bval'' |
|
47613 | 366 |
and step_ivl is step' |
367 |
and AI_ivl is AI |
|
368 |
and aval_ivl' is aval'' |
|
369 |
.. |
|
370 |
||
371 |
||
372 |
text{* Monotonicity: *} |
|
373 |
||
51882 | 374 |
lemma mono_plus_ivl: "iv1 \<le> iv2 \<Longrightarrow> iv3 \<le> iv4 \<Longrightarrow> iv1+iv3 \<le> iv2+(iv4::ivl)" |
375 |
apply transfer |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
376 |
apply(auto simp: plus_rep_def le_iff_subset split: if_splits) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
377 |
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
378 |
|
51882 | 379 |
lemma mono_minus_ivl: "iv1 \<le> iv2 \<Longrightarrow> -iv1 \<le> -(iv2::ivl)" |
380 |
apply transfer |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
381 |
apply(auto simp: uminus_rep_def le_iff_subset split: if_splits prod.split) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
382 |
by(auto simp: \<gamma>_rep_cases split: extended.splits) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51261
diff
changeset
|
383 |
|
51882 | 384 |
lemma mono_above: "iv1 \<le> iv2 \<Longrightarrow> above iv1 \<le> above iv2" |
385 |
apply transfer |
|
386 |
apply(auto simp: above_rep_def le_iff_subset split: if_splits prod.split) |
|
387 |
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits) |
|
388 |
||
389 |
lemma mono_below: "iv1 \<le> iv2 \<Longrightarrow> below iv1 \<le> below iv2" |
|
390 |
apply transfer |
|
391 |
apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split) |
|
392 |
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits) |
|
393 |
||
47613 | 394 |
interpretation Abs_Int1_mono |
51245 | 395 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
47613 | 396 |
and test_num' = in_ivl |
51974 | 397 |
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl |
47613 | 398 |
proof |
51882 | 399 |
case goal1 thus ?case by (rule mono_plus_ivl) |
47613 | 400 |
next |
51882 | 401 |
case goal2 thus ?case |
51974 | 402 |
unfolding inv_plus_ivl_def minus_ivl_def less_eq_prod_def |
51882 | 403 |
by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_minus_ivl) |
404 |
next |
|
405 |
case goal3 thus ?case |
|
51974 | 406 |
unfolding less_eq_prod_def inv_less_ivl_def minus_ivl_def |
51882 | 407 |
by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_above mono_below) |
47613 | 408 |
qed |
409 |
||
410 |
||
411 |
subsubsection "Tests" |
|
412 |
||
51036 | 413 |
value "show_acom_opt (AI_ivl test1_ivl)" |
47613 | 414 |
|
415 |
text{* Better than @{text AI_const}: *} |
|
51036 | 416 |
value "show_acom_opt (AI_ivl test3_const)" |
417 |
value "show_acom_opt (AI_ivl test4_const)" |
|
418 |
value "show_acom_opt (AI_ivl test6_const)" |
|
47613 | 419 |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
420 |
definition "steps c i = (step_ivl \<top> ^^ i) (bot c)" |
47613 | 421 |
|
51036 | 422 |
value "show_acom_opt (AI_ivl test2_ivl)" |
47613 | 423 |
value "show_acom (steps test2_ivl 0)" |
424 |
value "show_acom (steps test2_ivl 1)" |
|
425 |
value "show_acom (steps test2_ivl 2)" |
|
49188 | 426 |
value "show_acom (steps test2_ivl 3)" |
47613 | 427 |
|
51036 | 428 |
text{* Fixed point reached in 2 steps. |
47613 | 429 |
Not so if the start value of x is known: *} |
430 |
||
51036 | 431 |
value "show_acom_opt (AI_ivl test3_ivl)" |
47613 | 432 |
value "show_acom (steps test3_ivl 0)" |
433 |
value "show_acom (steps test3_ivl 1)" |
|
434 |
value "show_acom (steps test3_ivl 2)" |
|
435 |
value "show_acom (steps test3_ivl 3)" |
|
436 |
value "show_acom (steps test3_ivl 4)" |
|
49188 | 437 |
value "show_acom (steps test3_ivl 5)" |
47613 | 438 |
|
439 |
text{* Takes as many iterations as the actual execution. Would diverge if |
|
440 |
loop did not terminate. Worse still, as the following example shows: even if |
|
441 |
the actual execution terminates, the analysis may not. The value of y keeps |
|
442 |
decreasing as the analysis is iterated, no matter how long: *} |
|
443 |
||
444 |
value "show_acom (steps test4_ivl 50)" |
|
445 |
||
446 |
text{* Relationships between variables are NOT captured: *} |
|
51036 | 447 |
value "show_acom_opt (AI_ivl test5_ivl)" |
47613 | 448 |
|
449 |
text{* Again, the analysis would not terminate: *} |
|
450 |
value "show_acom (steps test6_ivl 50)" |
|
451 |
||
452 |
end |