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